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 

3954

14 
reset global_names;


15 

0

16 
print_depth 1;


17 

3578

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

0

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


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

1004

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


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

2866

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

0

24 

2469

25 
use_thy "IFOL";

0

26 

2866

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

0

28 
structure Hypsubst_Data =


29 
struct

1004

30 
structure Simplifier = Simplifier


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


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


33 
val eq_reflection = eq_reflection

0

34 
val imp_intr = impI


35 
val rev_mp = rev_mp


36 
val subst = subst


37 
val sym = sym


38 
end;


39 


40 
structure Hypsubst = HypsubstFun(Hypsubst_Data);


41 
open Hypsubst;


42 

2469

43 

97

44 
use "intprover.ML";

0

45 

2469

46 
use_thy "FOL";

0

47 

1523

48 
qed_goal "ex1_functional" FOL.thy

666

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

731

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

0

51 


52 


53 
print_depth 8;


54 

1459

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