18 *} |
18 *} |
19 |
19 |
20 classes prog < "term" |
20 classes prog < "term" |
21 defaultsort prog |
21 defaultsort prog |
22 |
22 |
23 arities fun :: (prog, prog) prog |
23 arities "fun" :: (prog, prog) prog |
24 |
24 |
25 typedecl i |
25 typedecl i |
26 arities i :: prog |
26 arities i :: prog |
27 |
27 |
28 |
28 |
29 consts |
29 consts |
30 (*** Evaluation Judgement ***) |
30 (*** Evaluation Judgement ***) |
31 "--->" :: "[i,i]=>prop" (infixl 20) |
31 Eval :: "[i,i]=>prop" (infixl "--->" 20) |
32 |
32 |
33 (*** Bisimulations for pre-order and equality ***) |
33 (*** Bisimulations for pre-order and equality ***) |
34 "[=" :: "['a,'a]=>o" (infixl 50) |
34 po :: "['a,'a]=>o" (infixl "[=" 50) |
35 SIM :: "[i,i,i set]=>o" |
35 SIM :: "[i,i,i set]=>o" |
36 POgen :: "i set => i set" |
36 POgen :: "i set => i set" |
37 EQgen :: "i set => i set" |
37 EQgen :: "i set => i set" |
38 PO :: "i set" |
38 PO :: "i set" |
39 EQ :: "i set" |
39 EQ :: "i set" |
42 true :: "i" |
42 true :: "i" |
43 false :: "i" |
43 false :: "i" |
44 pair :: "[i,i]=>i" ("(1<_,/_>)") |
44 pair :: "[i,i]=>i" ("(1<_,/_>)") |
45 lambda :: "(i=>i)=>i" (binder "lam " 55) |
45 lambda :: "(i=>i)=>i" (binder "lam " 55) |
46 "case" :: "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i" |
46 "case" :: "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i" |
47 "`" :: "[i,i]=>i" (infixl 56) |
47 "apply" :: "[i,i]=>i" (infixl "`" 56) |
48 bot :: "i" |
48 bot :: "i" |
49 "fix" :: "(i=>i)=>i" |
49 "fix" :: "(i=>i)=>i" |
50 |
50 |
51 (*** Defined Predicates ***) |
51 (*** Defined Predicates ***) |
52 Trm :: "i => o" |
52 Trm :: "i => o" |
186 |
186 |
187 lemma eq_lemma: "[| x=a; y=b; x=y |] ==> a=b" |
187 lemma eq_lemma: "[| x=a; y=b; x=y |] ==> a=b" |
188 by simp |
188 by simp |
189 |
189 |
190 ML {* |
190 ML {* |
191 local |
191 fun mk_inj_rl thy rews s = |
192 val arg_cong = thm "arg_cong"; |
192 let |
193 val eq_lemma = thm "eq_lemma"; |
193 fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})] |
194 val ss = simpset_of (the_context ()); |
194 val inj_lemmas = List.concat (map mk_inj_lemmas rews) |
195 in |
195 val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE |
196 fun mk_inj_rl thy rews s = |
196 eresolve_tac inj_lemmas 1 ORELSE |
197 let |
197 asm_simp_tac (Simplifier.theory_context thy @{simpset} addsimps rews) 1) |
198 fun mk_inj_lemmas r = [arg_cong] RL [r RS (r RS eq_lemma)] |
198 in prove_goal thy s (fn _ => [tac]) end |
199 val inj_lemmas = List.concat (map mk_inj_lemmas rews) |
|
200 val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE |
|
201 eresolve_tac inj_lemmas 1 ORELSE |
|
202 asm_simp_tac (Simplifier.theory_context thy ss addsimps rews) 1) |
|
203 in prove_goal thy s (fn _ => [tac]) end |
|
204 end |
|
205 *} |
199 *} |
206 |
200 |
207 ML {* |
201 ML {* |
208 bind_thms ("ccl_injs", |
202 bind_thms ("ccl_injs", |
209 map (mk_inj_rl (the_context ()) (thms "caseBs")) |
203 map (mk_inj_rl @{theory} @{thms caseBs}) |
210 ["<a,b> = <a',b'> <-> (a=a' & b=b')", |
204 ["<a,b> = <a',b'> <-> (a=a' & b=b')", |
211 "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"]) |
205 "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"]) |
212 *} |
206 *} |
213 |
207 |
214 |
208 |