--- a/src/CCL/CCL.thy Thu Jul 23 20:05:20 2009 +0200
+++ b/src/CCL/CCL.thy Thu Jul 23 21:59:56 2009 +0200
@@ -151,7 +151,8 @@
lemmas ccl_data_defs = apply_def fix_def
- and [simp] = po_refl
+
+declare po_refl [simp]
subsection {* Congruence Rules *}
@@ -190,7 +191,7 @@
fun mk_inj_rl thy rews s =
let
fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
- val inj_lemmas = List.concat (map mk_inj_lemmas rews)
+ val inj_lemmas = maps mk_inj_lemmas rews
val tac = REPEAT (ares_tac [iffI, allI, conjI] 1 ORELSE
eresolve_tac inj_lemmas 1 ORELSE
asm_simp_tac (Simplifier.theory_context thy @{simpset} addsimps rews) 1)
@@ -240,7 +241,7 @@
fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
[distinctness RS notE,sym RS (distinctness RS notE)]
in
- fun mk_lemmas rls = List.concat (map mk_lemma (mk_combs pair rls))
+ fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
end
@@ -261,7 +262,7 @@
(fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
-fun mkall_dstnct_thms thy defs i_rls xss = List.concat (map (mk_dstnct_thms thy defs i_rls) xss)
+fun mkall_dstnct_thms thy defs i_rls xss = maps (mk_dstnct_thms thy defs i_rls) xss
(*** Rewriting and Proving ***)
@@ -384,25 +385,25 @@
apply (rule po_refl npo_lam_bot)+
done
-ML {*
-
-local
- fun mk_thm s = prove_goal @{theory} s (fn _ =>
- [rtac notI 1, dtac @{thm case_pocong} 1, etac rev_mp 5,
- ALLGOALS (simp_tac @{simpset}),
- REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)])
-in
+lemma npo_rls1:
+ "~ true [= false"
+ "~ false [= true"
+ "~ true [= <a,b>"
+ "~ <a,b> [= true"
+ "~ true [= lam x. f(x)"
+ "~ lam x. f(x) [= true"
+ "~ false [= <a,b>"
+ "~ <a,b> [= false"
+ "~ false [= lam x. f(x)"
+ "~ lam x. f(x) [= false"
+ by (tactic {*
+ REPEAT (rtac notI 1 THEN
+ dtac @{thm case_pocong} 1 THEN
+ etac rev_mp 5 THEN
+ ALLGOALS (simp_tac @{simpset}) THEN
+ REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)) *})
-val npo_rls = [@{thm npo_pair_lam}, @{thm npo_lam_pair}] @ map mk_thm
- ["~ true [= false", "~ false [= true",
- "~ true [= <a,b>", "~ <a,b> [= true",
- "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
- "~ false [= <a,b>", "~ <a,b> [= false",
- "~ false [= lam x. f(x)","~ lam x. f(x) [= false"]
-end;
-
-bind_thms ("npo_rls", npo_rls);
-*}
+lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1
subsection {* Coinduction for @{text "[="} *}