author  nipkow 
Wed, 04 Aug 2004 11:25:08 +0200  
changeset 15106  e8cef6993701 
parent 6349  f7750d816c21 
child 17480  fd19f77dcf60 
permissions  rwrr 
1459  1 
(* Title: FOLP/ROOT 
0  2 
ID: $Id$ 
1459  3 
Author: martin Coen, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
Modifed version of Lawrence Paulson's FOL that contains proof terms. 

7 

8 
Presence of unknown proof term means that matching does not behave as expected. 

9 
*) 

10 

11 
val banner = "FirstOrder Logic with Natural Deduction with Proof Terms"; 

12 

13 
writeln banner; 

14 

3511  15 
print_depth 1; 
72  16 

98  17 
use_thy "IFOLP"; 
18 
use_thy "FOLP"; 

0  19 

1008
fa11e1e28bd3
Loads the local hypsubst.ML. No longer loads ../Provers/ind.ML,
lcp
parents:
393
diff
changeset

20 
use "hypsubst.ML"; 
0  21 
use "classical.ML"; (* Patched 'cos matching won't instantiate proof *) 
1459  22 
use "simp.ML"; (* Patched 'cos matching won't instantiate proof *) 
0  23 

24 

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

26 

27 
structure Hypsubst_Data = 

28 
struct 

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

30 
fun dest_eq (Const("Proof",_) $ (Const("op =",_) $ t $ u) $ _) = (t,u); 

31 

32 
val imp_intr = impI 

33 

34 
(*etac rev_cut_eq moves an equality to be the last premise. *) 

35 
val rev_cut_eq = prove_goal IFOLP.thy 

3836  36 
"[ p:a=b; !!x. x:a=b ==> f(x):R ] ==> ?p:R" 
0  37 
(fn prems => [ REPEAT(resolve_tac prems 1) ]); 
38 

39 
val rev_mp = rev_mp 

40 
val subst = subst 

41 
val sym = sym 

4223  42 
val thin_refl = prove_goal IFOLP.thy 
43 
"!!X. [p:x=x; PROP W] ==> PROP W" (K [atac 1]); 

0  44 
end; 
45 

46 
structure Hypsubst = HypsubstFun(Hypsubst_Data); 

47 
open Hypsubst; 

48 

98  49 
use "intprover.ML"; 
0  50 

51 
(*** Applying ClassicalFun to create a classical prover ***) 

52 
structure Classical_Data = 

53 
struct 

54 
val sizef = size_of_thm 

55 
val mp = mp 

56 
val not_elim = notE 

57 
val swap = swap 

58 
val hyp_subst_tacs=[hyp_subst_tac] 

59 
end; 

60 

61 
structure Cla = ClassicalFun(Classical_Data); 

62 
open Cla; 

63 

64 
(*Propositional rules 

65 
 iffCE might seem better, but in the examples in ex/cla 

66 
run about 7% slower than with iffE*) 

67 
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 

68 
addSEs [conjE,disjE,impCE,FalseE,iffE]; 

69 

70 
(*Quantifier rules*) 

71 
val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 

72 
addSEs [exE,ex1E] addEs [allE]; 

73 

74 
val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] 

75 
addSEs [exE,ex1E] addEs [all_dupE]; 

76 

77 
use "simpdata.ML"; 

78 

3511  79 

0  80 
print_depth 8; 