author  wenzelm 
Mon, 20 Oct 1997 11:06:01 +0200  
changeset 3942  1f1c1f524d19 
parent 3836  f1a1817659e6 
child 4024  3c056eab237c 
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 

3942  15 
reset global_names; 
16 

3511  17 
print_depth 1; 
72  18 

98  19 
use_thy "IFOLP"; 
20 
use_thy "FOLP"; 

0  21 

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

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

26 

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

28 

29 
structure Hypsubst_Data = 

30 
struct 

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

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

33 

34 
val imp_intr = impI 

35 

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

37 
val rev_cut_eq = prove_goal IFOLP.thy 

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

41 
val rev_mp = rev_mp 

42 
val subst = subst 

43 
val sym = sym 

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; 
176  81 

1459  82 
val FOLP_build_completed = (); (*indicate successful build*) 