1459

1 
(* Title: FOL/ROOT

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1993 University of Cambridge


5 


6 
Adds FirstOrder Logic to a database containing pure Isabelle.


7 
Should be executed in the subdirectory FOL.


8 
*)


9 


10 
val banner = "FirstOrder Logic with Natural Deduction";


11 


12 
writeln banner;


13 

393

14 
init_thy_reader();

72

15 

0

16 
print_depth 1;


17 


18 
use "../Provers/splitter.ML";


19 
use "../Provers/ind.ML";

1004

20 
use "../Provers/hypsubst.ML";


21 
use "../Provers/classical.ML";

2866

22 
use "../Provers/blast.ML";

0

23 

2469

24 
use_thy "IFOL";

0

25 

2866

26 
(** Applying HypsubstFun to generate hyp_subst_tac **)

0

27 
structure Hypsubst_Data =


28 
struct

1004

29 
structure Simplifier = Simplifier


30 
(*Take apart an equality judgement; otherwise raise Match!*)


31 
fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u)


32 
val eq_reflection = eq_reflection

0

33 
val imp_intr = impI


34 
val rev_mp = rev_mp


35 
val subst = subst


36 
val sym = sym


37 
end;


38 


39 
structure Hypsubst = HypsubstFun(Hypsubst_Data);


40 
open Hypsubst;


41 

2469

42 

97

43 
use "intprover.ML";

0

44 

2469

45 
use_thy "FOL";

0

46 

1523

47 
qed_goal "ex1_functional" FOL.thy

666

48 
"!!a b c. [ EX! z. P(a,z); P(a,b); P(a,c) ] ==> b = c"

731

49 
(fn _ => [ (deepen_tac FOL_cs 0 1) ]);

0

50 


51 

2237

52 
init_pps ();

0

53 
print_depth 8;


54 

1459

55 
val FOL_build_completed = (); (*indicate successful build*)
