author  oheimb 
Wed, 12 Nov 1997 18:58:50 +0100  
changeset 4223  f60e3d2c81d3 
parent 4222  d7573d6d0513 
child 4349  50403e5a44c0 
permissions  rwrr 
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 

14 
print_depth 1; 

15 

4222  16 
use "$ISABELLE_HOME/src/Provers/simplifier.ML"; 
17 
use "$ISABELLE_HOME/src/Provers/splitter.ML"; 

18 
use "$ISABELLE_HOME/src/Provers/ind.ML"; 

19 
use "$ISABELLE_HOME/src/Provers/hypsubst.ML"; 

20 
use "$ISABELLE_HOME/src/Provers/classical.ML"; 

21 
use "$ISABELLE_HOME/src/Provers/blast.ML"; 

0  22 

2469  23 
use_thy "IFOL"; 
0  24 

2866  25 
(** Applying HypsubstFun to generate hyp_subst_tac **) 
0  26 
structure Hypsubst_Data = 
27 
struct 

1004  28 
structure Simplifier = Simplifier 
29 
(*Take apart an equality judgement; otherwise raise Match!*) 

4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
4096
diff
changeset

30 
fun dest_eq (Const("Trueprop",_) $ (Const("op =",T) $ t $ u)) = 
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
4096
diff
changeset

31 
(t, u, domain_type T) 
1004  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 

4223  37 
val thin_refl = prove_goal IFOL.thy 
38 
"!!X. [x=x; PROP W] ==> PROP W" (K [atac 1]); 

0  39 
end; 
40 

41 
structure Hypsubst = HypsubstFun(Hypsubst_Data); 

42 
open Hypsubst; 

43 

2469  44 

97  45 
use "intprover.ML"; 
0  46 

2469  47 
use_thy "FOL"; 
0  48 

4096  49 
use "cladata.ML"; 
50 
use "simpdata.ML"; 

51 

1523  52 
qed_goal "ex1_functional" FOL.thy 
666  53 
"!!a b c. [ EX! z. P(a,z); P(a,b); P(a,c) ] ==> b = c" 
731  54 
(fn _ => [ (deepen_tac FOL_cs 0 1) ]); 
0  55 

56 

57 
print_depth 8; 

58 

1459  59 
val FOL_build_completed = (); (*indicate successful build*) 