author  clasohm 
Mon, 29 Jan 1996 13:58:15 +0100  
changeset 1459  d12da312eff4 
parent 1361  90d615b599d9 
child 2237  f01ac387e82b 
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 

393  15 
init_thy_reader(); 
72  16 

0  17 
print_depth 1; 
98  18 
use_thy "IFOLP"; 
19 
use_thy "FOLP"; 

0  20 

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

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

25 

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

27 

28 
structure Hypsubst_Data = 

29 
struct 

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

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

32 

33 
val imp_intr = impI 

34 

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

36 
val rev_cut_eq = prove_goal IFOLP.thy 

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

40 
val rev_mp = rev_mp 

41 
val subst = subst 

42 
val sym = sym 

43 
end; 

44 

45 
structure Hypsubst = HypsubstFun(Hypsubst_Data); 

46 
open Hypsubst; 

47 

98  48 
use "intprover.ML"; 
0  49 

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

51 
structure Classical_Data = 

52 
struct 

53 
val sizef = size_of_thm 

54 
val mp = mp 

55 
val not_elim = notE 

56 
val swap = swap 

57 
val hyp_subst_tacs=[hyp_subst_tac] 

58 
end; 

59 

60 
structure Cla = ClassicalFun(Classical_Data); 

61 
open Cla; 

62 

63 
(*Propositional rules 

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

65 
run about 7% slower than with iffE*) 

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

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

68 

69 
(*Quantifier rules*) 

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

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

72 

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

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

75 

76 
use "simpdata.ML"; 

77 

78 
use "../Pure/install_pp.ML"; 

79 
print_depth 8; 

176  80 

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