author  berghofe 
Mon, 06 May 1996 15:21:05 +0200  
changeset 1722  bb326972ede6 
parent 1459  d12da312eff4 
child 1914  86b095835de9 
permissions  rwrr 
1459  1 
(* Title: FOL/simpdata 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
282  4 
Copyright 1994 University of Cambridge 
0  5 

6 
Simplification data for FOL 

7 
*) 

8 

9 
(*** Rewrite rules ***) 

10 

11 
fun int_prove_fun s = 

282  12 
(writeln s; 
13 
prove_goal IFOL.thy s 

14 
(fn prems => [ (cut_facts_tac prems 1), 

1459  15 
(Int.fast_tac 1) ])); 
0  16 

17 
val conj_rews = map int_prove_fun 

1459  18 
["P & True <> P", "True & P <> P", 
0  19 
"P & False <> False", "False & P <> False", 
20 
"P & P <> P", 

1459  21 
"P & ~P <> False", "~P & P <> False", 
0  22 
"(P & Q) & R <> P & (Q & R)"]; 
23 

24 
val disj_rews = map int_prove_fun 

1459  25 
["P  True <> True", "True  P <> True", 
26 
"P  False <> P", "False  P <> P", 

0  27 
"P  P <> P", 
28 
"(P  Q)  R <> P  (Q  R)"]; 

29 

30 
val not_rews = map int_prove_fun 

282  31 
["~(PQ) <> ~P & ~Q", 
1459  32 
"~ False <> True", "~ True <> False"]; 
0  33 

34 
val imp_rews = map int_prove_fun 

1459  35 
["(P > False) <> ~P", "(P > True) <> True", 
36 
"(False > P) <> True", "(True > P) <> P", 

37 
"(P > P) <> True", "(P > ~P) <> ~P"]; 

0  38 

39 
val iff_rews = map int_prove_fun 

1459  40 
["(True <> P) <> P", "(P <> True) <> P", 
0  41 
"(P <> P) <> True", 
1459  42 
"(False <> P) <> ~P", "(P <> False) <> ~P"]; 
0  43 

44 
val quant_rews = map int_prove_fun 

1459  45 
["(ALL x.P) <> P", "(EX x.P) <> P"]; 
0  46 

47 
(*These are NOT supplied by default!*) 

48 
val distrib_rews = map int_prove_fun 

282  49 
["P & (Q  R) <> P&Q  P&R", 
50 
"(Q  R) & P <> Q&P  R&P", 

0  51 
"(P  Q > R) <> (P > R) & (Q > R)"]; 
52 

784  53 
bind_thm("conj_commute", int_prove_fun "P&Q <> Q&P"); 
54 
bind_thm("disj_commute", int_prove_fun "PQ <> QP"); 

55 

282  56 
(** Conversion into rewrite rules **) 
0  57 

53  58 
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; 
59 

282  60 
(*Make atomic rewrite rules*) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

61 
fun atomize r = 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

62 
case concl_of r of 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

63 
Const("Trueprop",_) $ p => 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

64 
(case p of 
1459  65 
Const("op >",_)$_$_ => atomize(r RS mp) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

66 
 Const("op &",_)$_$_ => atomize(r RS conjunct1) @ 
1459  67 
atomize(r RS conjunct2) 
429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

68 
 Const("All",_)$_ => atomize(r RS spec) 
1459  69 
 Const("True",_) => [] (*True is DELETED*) 
70 
 Const("False",_) => [] (*should False do something?*) 

429
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

71 
 _ => [r]) 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

72 
 _ => [r]; 
888bbb4119f8
atomize: borrowed HOL version, which checks for both Trueprop
lcp
parents:
394
diff
changeset

73 

282  74 

75 
val P_iff_F = int_prove_fun "~P ==> (P <> False)"; 

76 
val iff_reflection_F = P_iff_F RS iff_reflection; 

77 

78 
val P_iff_T = int_prove_fun "P ==> (P <> True)"; 

79 
val iff_reflection_T = P_iff_T RS iff_reflection; 

80 

81 
(*Make metaequalities. The operator below is Trueprop*) 

82 
fun mk_meta_eq th = case concl_of th of 

394
432bb9995893
Modified mk_meta_eq to leave metaequlities on unchanged.
nipkow
parents:
371
diff
changeset

83 
Const("==",_)$_$_ => th 
432bb9995893
Modified mk_meta_eq to leave metaequlities on unchanged.
nipkow
parents:
371
diff
changeset

84 
 _ $ (Const("op =",_)$_$_) => th RS eq_reflection 
282  85 
 _ $ (Const("op <>",_)$_$_) => th RS iff_reflection 
86 
 _ $ (Const("Not",_)$_) => th RS iff_reflection_F 

87 
 _ => th RS iff_reflection_T; 

0  88 

89 
structure Induction = InductionFun(struct val spec=IFOL.spec end); 

90 

91 
open Simplifier Induction; 

92 

981  93 
(*Add congruence rules for = or <> (instead of ==) *) 
94 
infix 4 addcongs; 

3  95 
fun ss addcongs congs = 
282  96 
ss addeqcongs (congs RL [eq_reflection,iff_reflection]); 
97 

981  98 
(*Add a simpset to a classical set!*) 
99 
infix 4 addss; 

100 
fun cs addss ss = cs addbefore asm_full_simp_tac ss 1; 

101 

102 

282  103 
val IFOL_rews = 
104 
[refl RS P_iff_T] @ conj_rews @ disj_rews @ not_rews @ 

105 
imp_rews @ iff_rews @ quant_rews; 

3  106 

282  107 
val notFalseI = int_prove_fun "~False"; 
108 
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; 

109 

110 
val IFOL_ss = 

111 
empty_ss 

112 
setmksimps (map mk_meta_eq o atomize o gen_all) 

371
3a853818f1d2
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
lcp
parents:
282
diff
changeset

113 
setsolver (fn prems => resolve_tac (triv_rls@prems) 
1459  114 
ORELSE' assume_tac 
115 
ORELSE' etac FalseE) 

282  116 
setsubgoaler asm_simp_tac 
117 
addsimps IFOL_rews 

118 
addcongs [imp_cong]; 

0  119 

120 
(*Classical version...*) 

121 
fun prove_fun s = 

282  122 
(writeln s; 
123 
prove_goal FOL.thy s 

124 
(fn prems => [ (cut_facts_tac prems 1), 

1459  125 
(Cla.fast_tac FOL_cs 1) ])); 
745  126 

0  127 
val cla_rews = map prove_fun 
282  128 
["~(P&Q) <> ~P  ~Q", 
1459  129 
"P  ~P", "~P  P", 
130 
"~ ~ P <> P", "(~P > P) <> P"]; 

0  131 

132 
val FOL_ss = IFOL_ss addsimps cla_rews; 

133 

1088
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

134 
(*Used in ZF, perhaps elsewhere?*) 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

135 
val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y" 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

136 
(fn [prem] => [rewtac prem, rtac refl 1]); 
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

137 

0  138 
(*** case splitting ***) 
139 

1088
fc4fb6e8a636
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
lcp
parents:
981
diff
changeset

140 
qed_goal "meta_iffD" IFOL.thy "[ P==Q; Q ] ==> P" 
756  141 
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]); 
282  142 

942  143 
local val mktac = mk_case_split_tac meta_iffD 
144 
in 

145 
fun split_tac splits = mktac (map mk_meta_eq splits) 

146 
end; 

1722  147 

148 
local val mktac = mk_case_split_inside_tac meta_iffD 

149 
in 

150 
fun split_inside_tac splits = mktac (map mk_meta_eq splits) 

151 
end; 

152 

153 