author  wenzelm 
Mon, 20 Oct 1997 10:48:22 +0200  
changeset 3935  52c14fe8f16b 
parent 3837  d7f033c74b38 
child 4347  d683b7898c61 
permissions  rwrr 
1459  1 
(* Title: CCL/ccl 
0  2 
ID: $Id$ 
1459  3 
Author: Martin Coen, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
For ccl.thy. 

7 
*) 

8 

9 
open CCL; 

10 

11 
val ccl_data_defs = [apply_def,fix_def]; 

12 

1963  13 
val CCL_ss = set_ss addsimps [po_refl RS P_iff_T]; 
0  14 

15 
(*** Congruence Rules ***) 

16 

17 
(*similar to AP_THM in Gordon's HOL*) 

757  18 
qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)" 
0  19 
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); 
20 

21 
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) 

757  22 
qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)" 
0  23 
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); 
24 

3837  25 
goal CCL.thy "(ALL x. f(x) = g(x)) > (%x. f(x)) = (%x. g(x))"; 
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

26 
by (simp_tac (CCL_ss addsimps [eq_iff]) 1); 
0  27 
by (fast_tac (set_cs addIs [po_abstractn]) 1); 
1087  28 
bind_thm("abstractn", standard (allI RS (result() RS mp))); 
0  29 

30 
fun type_of_terms (Const("Trueprop",_) $ 

31 
(Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t; 

32 

33 
fun abs_prems thm = 

34 
let fun do_abs n thm (Type ("fun", [_,t])) = do_abs n (abstractn RSN (n,thm)) t 

35 
 do_abs n thm _ = thm 

36 
fun do_prems n [] thm = thm 

37 
 do_prems n (x::xs) thm = do_prems (n+1) xs (do_abs n thm (type_of_terms x)); 

38 
in do_prems 1 (prems_of thm) thm 

39 
end; 

40 

41 
val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot]; 

42 

43 
(*** Termination and Divergence ***) 

44 

45 
goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <> ~ t = bot"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

46 
by (rtac iff_refl 1); 
757  47 
qed "Trm_iff"; 
0  48 

49 
goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <> t = bot"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

50 
by (rtac iff_refl 1); 
757  51 
qed "Dvg_iff"; 
0  52 

53 
(*** Constructors are injective ***) 

54 

55 
val prems = goal CCL.thy 

56 
"[ x=a; y=b; x=y ] ==> a=b"; 

57 
by (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals])))); 

757  58 
qed "eq_lemma"; 
0  59 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

60 
fun mk_inj_rl thy rews s = 
0  61 
let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]); 
62 
val inj_lemmas = flat (map mk_inj_lemmas rews); 

63 
val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE 

64 
eresolve_tac inj_lemmas 1 ORELSE 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

65 
asm_simp_tac (CCL_ss addsimps rews) 1) 
0  66 
in prove_goal thy s (fn _ => [tac]) 
67 
end; 

68 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

69 
val ccl_injs = map (mk_inj_rl CCL.thy caseBs) 
0  70 
["<a,b> = <a',b'> <> (a=a' & b=b')", 
3837  71 
"(lam x. b(x) = lam x. b'(x)) <> ((ALL z. b(z)=b'(z)))"]; 
0  72 

73 
val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE; 

74 

75 
(*** Constructors are distinct ***) 

76 

77 
local 

78 
fun pairs_of f x [] = [] 

79 
 pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys); 

80 

81 
fun mk_combs ff [] = [] 

82 
 mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs; 

83 

84 
(* Doesn't handle binder types correctly *) 

85 
fun saturate thy sy name = 

86 
let fun arg_str 0 a s = s 

87 
 arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")" 

88 
 arg_str n a s = arg_str (n1) a ("," ^ a ^ (chr((ord "a")+n1)) ^ s); 

89 
val sg = sign_of thy; 

3935  90 
val T = case Sign.const_type sg (Sign.intern_const (sign_of thy) sy) of 
1459  91 
None => error(sy^" not declared")  Some(T) => T; 
0  92 
val arity = length (fst (strip_type T)); 
93 
in sy ^ (arg_str arity name "") end; 

94 

95 
fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b"); 

96 

97 
val lemma = prove_goal CCL.thy "t=t' > case(t,b,c,d,e) = case(t',b,c,d,e)" 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

98 
(fn _ => [simp_tac CCL_ss 1]) RS mp; 
0  99 
fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL 
100 
[distinctness RS notE,sym RS (distinctness RS notE)]; 

101 
in 

102 
fun mk_lemmas rls = flat (map mk_lemma (mk_combs pair rls)); 

103 
fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs; 

104 
end; 

105 

106 

107 
val caseB_lemmas = mk_lemmas caseBs; 

108 

109 
val ccl_dstncts = 

110 
let fun mk_raw_dstnct_thm rls s = 

111 
prove_goal CCL.thy s (fn _=> [rtac notI 1,eresolve_tac rls 1]) 

112 
in map (mk_raw_dstnct_thm caseB_lemmas) 

113 
(mk_dstnct_rls CCL.thy ["bot","true","false","pair","lambda"]) end; 

114 

115 
fun mk_dstnct_thms thy defs inj_rls xs = 

116 
let fun mk_dstnct_thm rls s = prove_goalw thy defs s 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

117 
(fn _ => [simp_tac (CCL_ss addsimps (rls@inj_rls)) 1]) 
0  118 
in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end; 
119 

120 
fun mkall_dstnct_thms thy defs i_rls xss = flat (map (mk_dstnct_thms thy defs i_rls) xss); 

121 

122 
(*** Rewriting and Proving ***) 

123 

124 
fun XH_to_I rl = rl RS iffD2; 

125 
fun XH_to_D rl = rl RS iffD1; 

126 
val XH_to_E = make_elim o XH_to_D; 

127 
val XH_to_Is = map XH_to_I; 

128 
val XH_to_Ds = map XH_to_D; 

129 
val XH_to_Es = map XH_to_E; 

130 

131 
val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts; 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

132 
val ccl_ss = CCL_ss addsimps ccl_rews; 
0  133 

134 
val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) 

135 
addSDs (XH_to_Ds ccl_injs); 

136 

137 
(****** Facts from gfp Definition of [= and = ******) 

138 

139 
val major::prems = goal Set.thy "[ A=B; a:B <> P ] ==> a:A <> P"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

140 
by (resolve_tac (prems RL [major RS ssubst]) 1); 
757  141 
qed "XHlemma1"; 
0  142 

3837  143 
goal CCL.thy "(P(t,t') <> Q) > (<t,t'> : {p. EX t t'. p=<t,t'> & P(t,t')} <> Q)"; 
0  144 
by (fast_tac ccl_cs 1); 
1087  145 
bind_thm("XHlemma2", result() RS mp); 
0  146 

147 
(*** PreOrder ***) 

148 

3837  149 
goalw CCL.thy [POgen_def,SIM_def] "mono(%X. POgen(X))"; 
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

150 
by (rtac monoI 1); 
0  151 
by (safe_tac ccl_cs); 
152 
by (REPEAT_SOME (resolve_tac [exI,conjI,refl])); 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

153 
by (ALLGOALS (simp_tac ccl_ss)); 
0  154 
by (ALLGOALS (fast_tac set_cs)); 
757  155 
qed "POgen_mono"; 
0  156 

157 
goalw CCL.thy [POgen_def,SIM_def] 

158 
"<t,t'> : POgen(R) <> t= bot  (t=true & t'=true)  (t=false & t'=false)  \ 

3837  159 
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R)  \ 
160 
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

161 
by (rtac (iff_refl RS XHlemma2) 1); 
757  162 
qed "POgenXH"; 
0  163 

164 
goal CCL.thy 

165 
"t [= t' <> t=bot  (t=true & t'=true)  (t=false & t'=false)  \ 

3837  166 
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & a [= a' & b [= b')  \ 
167 
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))"; 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

168 
by (simp_tac (ccl_ss addsimps [PO_iff]) 1); 
0  169 
br (rewrite_rule [POgen_def,SIM_def] 
170 
(POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

171 
by (rtac (iff_refl RS XHlemma2) 1); 
757  172 
qed "poXH"; 
0  173 

174 
goal CCL.thy "bot [= b"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

175 
by (rtac (poXH RS iffD2) 1); 
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

176 
by (simp_tac ccl_ss 1); 
757  177 
qed "po_bot"; 
0  178 

179 
goal CCL.thy "a [= bot > a=bot"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

180 
by (rtac impI 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

181 
by (dtac (poXH RS iffD1) 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

182 
by (etac rev_mp 1); 
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

183 
by (simp_tac ccl_ss 1); 
1087  184 
bind_thm("bot_poleast", result() RS mp); 
0  185 

186 
goal CCL.thy "<a,b> [= <a',b'> <> a [= a' & b [= b'"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

187 
by (rtac (poXH RS iff_trans) 1); 
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

188 
by (simp_tac ccl_ss 1); 
0  189 
by (fast_tac ccl_cs 1); 
757  190 
qed "po_pair"; 
0  191 

3837  192 
goal CCL.thy "lam x. f(x) [= lam x. f'(x) <> (ALL x. f(x) [= f'(x))"; 
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

193 
by (rtac (poXH RS iff_trans) 1); 
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

194 
by (simp_tac ccl_ss 1); 
0  195 
by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1)); 
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

196 
by (asm_simp_tac ccl_ss 1); 
0  197 
by (fast_tac ccl_cs 1); 
757  198 
qed "po_lam"; 
0  199 

200 
val ccl_porews = [po_bot,po_pair,po_lam]; 

201 

202 
val [p1,p2,p3,p4,p5] = goal CCL.thy 

3837  203 
"[ t [= t'; a [= a'; b [= b'; !!x y. c(x,y) [= c'(x,y); \ 
204 
\ !!u. d(u) [= d'(u) ] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

205 
by (rtac (p1 RS po_cong RS po_trans) 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

206 
by (rtac (p2 RS po_cong RS po_trans) 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

207 
by (rtac (p3 RS po_cong RS po_trans) 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

208 
by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1); 
3837  209 
by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] 
0  210 
(p5 RS po_abstractn RS po_cong RS po_trans) 1); 
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

211 
by (rtac po_refl 1); 
757  212 
qed "case_pocong"; 
0  213 

214 
val [p1,p2] = goalw CCL.thy ccl_data_defs 

215 
"[ f [= f'; a [= a' ] ==> f ` a [= f' ` a'"; 

216 
by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1)); 

757  217 
qed "apply_pocong"; 
0  218 

219 

3837  220 
val prems = goal CCL.thy "~ lam x. b(x) [= bot"; 
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

221 
by (rtac notI 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

222 
by (dtac bot_poleast 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

223 
by (etac (distinctness RS notE) 1); 
757  224 
qed "npo_lam_bot"; 
0  225 

226 
val eq1::eq2::prems = goal CCL.thy 

227 
"[ x=a; y=b; x[=y ] ==> a[=b"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

228 
by (rtac (eq1 RS subst) 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

229 
by (rtac (eq2 RS subst) 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

230 
by (resolve_tac prems 1); 
757  231 
qed "po_lemma"; 
0  232 

3837  233 
goal CCL.thy "~ <a,b> [= lam x. f(x)"; 
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

234 
by (rtac notI 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

235 
by (rtac (npo_lam_bot RS notE) 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

236 
by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1); 
0  237 
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); 
757  238 
qed "npo_pair_lam"; 
0  239 

3837  240 
goal CCL.thy "~ lam x. f(x) [= <a,b>"; 
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

241 
by (rtac notI 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

242 
by (rtac (npo_lam_bot RS notE) 1); 
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

243 
by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1); 
0  244 
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); 
757  245 
qed "npo_lam_pair"; 
0  246 

247 
fun mk_thm s = prove_goal CCL.thy s (fn _ => 

248 
[rtac notI 1,dtac case_pocong 1,etac rev_mp 5, 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

249 
ALLGOALS (simp_tac ccl_ss), 
0  250 
REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]); 
251 

252 
val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm 

253 
["~ true [= false", "~ false [= true", 

254 
"~ true [= <a,b>", "~ <a,b> [= true", 

3837  255 
"~ true [= lam x. f(x)","~ lam x. f(x) [= true", 
0  256 
"~ false [= <a,b>", "~ <a,b> [= false", 
3837  257 
"~ false [= lam x. f(x)","~ lam x. f(x) [= false"]; 
0  258 

259 
(* Coinduction for [= *) 

260 

261 
val prems = goal CCL.thy "[ <t,u> : R; R <= POgen(R) ] ==> t [= u"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

262 
by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1); 
0  263 
by (REPEAT (ares_tac prems 1)); 
757  264 
qed "po_coinduct"; 
0  265 

266 
fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i; 

267 

268 
(*************** EQUALITY *******************) 

269 

3837  270 
goalw CCL.thy [EQgen_def,SIM_def] "mono(%X. EQgen(X))"; 
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

271 
by (rtac monoI 1); 
0  272 
by (safe_tac set_cs); 
273 
by (REPEAT_SOME (resolve_tac [exI,conjI,refl])); 

8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

274 
by (ALLGOALS (simp_tac ccl_ss)); 
0  275 
by (ALLGOALS (fast_tac set_cs)); 
757  276 
qed "EQgen_mono"; 
0  277 

278 
goalw CCL.thy [EQgen_def,SIM_def] 

279 
"<t,t'> : EQgen(R) <> (t=bot & t'=bot)  (t=true & t'=true)  \ 

280 
\ (t=false & t'=false)  \ 

3837  281 
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R)  \ 
282 
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

283 
by (rtac (iff_refl RS XHlemma2) 1); 
757  284 
qed "EQgenXH"; 
0  285 

286 
goal CCL.thy 

287 
"t=t' <> (t=bot & t'=bot)  (t=true & t'=true)  (t=false & t'=false)  \ 

3837  288 
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & a=a' & b=b')  \ 
289 
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))"; 

0  290 
by (subgoal_tac 
291 
"<t,t'> : EQ <> (t=bot & t'=bot)  (t=true & t'=true)  (t=false & t'=false)  \ 

3837  292 
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : EQ & <b,b'> : EQ)  \ 
293 
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1); 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

294 
by (etac rev_mp 1); 
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

295 
by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1); 
0  296 
br (rewrite_rule [EQgen_def,SIM_def] 
297 
(EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

298 
by (rtac (iff_refl RS XHlemma2) 1); 
757  299 
qed "eqXH"; 
0  300 

301 
val prems = goal CCL.thy "[ <t,u> : R; R <= EQgen(R) ] ==> t = u"; 

642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

302 
by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1); 
0  303 
by (REPEAT (ares_tac prems 1)); 
757  304 
qed "eq_coinduct"; 
0  305 

306 
val prems = goal CCL.thy 

3837  307 
"[ <t,u> : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) ] ==> t = u"; 
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
611
diff
changeset

308 
by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1); 
0  309 
by (REPEAT (ares_tac (EQgen_mono::prems) 1)); 
757  310 
qed "eq_coinduct3"; 
0  311 

312 
fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i; 

313 
fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i; 

314 

315 
(*** Untyped Case Analysis and Other Facts ***) 

316 

3837  317 
goalw CCL.thy [apply_def] "(EX f. t=lam x. f(x)) > t = lam x.(t ` x)"; 
0  318 
by (safe_tac ccl_cs); 
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset

319 
by (simp_tac ccl_ss 1); 
1087  320 
bind_thm("cond_eta", result() RS mp); 
0  321 

3837  322 
goal CCL.thy "(t=bot)  (t=true)  (t=false)  (EX a b. t=<a,b>)  (EX f. t=lam x. f(x))"; 
0  323 
by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1); 
324 
by (fast_tac set_cs 1); 

757  325 
qed "exhaustion"; 
0  326 

327 
val prems = goal CCL.thy 

3837  328 
"[ P(bot); P(true); P(false); !!x y. P(<x,y>); !!b. P(lam x. b(x)) ] ==> P(t)"; 
0  329 
by (cut_facts_tac [exhaustion] 1); 
330 
by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst])); 

757  331 
qed "term_case"; 
0  332 

333 
fun term_case_tac a i = res_inst_tac [("t",a)] term_case i; 