# HG changeset patch
# User wenzelm
# Date 1248380437 -7200
# Node ID 9721e8e4d48c3a9eb06648fe2eafc0bda3eef78c
# Parent  a0e57fb1b930a4aecd92c693541798aa6155a262
eliminated adhoc ML code;

diff -r a0e57fb1b930 -r 9721e8e4d48c src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Thu Jul 23 21:59:56 2009 +0200
+++ b/src/CCL/CCL.thy	Thu Jul 23 22:20:37 2009 +0200
@@ -188,22 +188,25 @@
   by simp
 
 ML {*
-  fun mk_inj_rl thy rews s =
+  fun inj_rl_tac ctxt rews i =
     let
       fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
       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)
-    in prove_goal thy s (fn _ => [tac]) end  
+    in
+      CHANGED (REPEAT (ares_tac [iffI, allI, conjI] i ORELSE
+        eresolve_tac inj_lemmas i ORELSE
+        asm_simp_tac (simpset_of ctxt addsimps rews) i))
+    end;
 *}
 
-ML {*
-  bind_thms ("ccl_injs",
-    map (mk_inj_rl @{theory} @{thms caseBs})
-      ["<a,b> = <a',b'> <-> (a=a' & b=b')",
-       "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"])
-*}
+method_setup inj_rl = {*
+  Attrib.thms >> (fn rews => fn ctxt => SIMPLE_METHOD' (inj_rl_tac ctxt rews))
+*} ""
+
+lemma ccl_injs:
+  "<a,b> = <a',b'> <-> (a=a' & b=b')"
+  "!!b b'. (lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"
+  by (inj_rl caseBs)
 
 
 lemma pair_inject: "<a,b> = <a',b'> \<Longrightarrow> (a = a' \<Longrightarrow> b = b' \<Longrightarrow> R) \<Longrightarrow> R"
@@ -273,7 +276,7 @@
 val XH_to_Ds = map XH_to_D
 val XH_to_Es = map XH_to_E;
 
-bind_thms ("ccl_rews", @{thms caseBs} @ ccl_injs @ ccl_dstncts);
+bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
 bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [notE]);
 bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
 *}
@@ -413,11 +416,6 @@
    apply assumption+
   done
 
-ML {*
-  fun po_coinduct_tac ctxt s i =
-    res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
-*}
-
 
 subsection {* Equality *}
 
diff -r a0e57fb1b930 -r 9721e8e4d48c src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Thu Jul 23 21:59:56 2009 +0200
+++ b/src/CCL/Hered.thy	Thu Jul 23 22:20:37 2009 +0200
@@ -95,23 +95,12 @@
   apply assumption
   done
 
-ML {*
-  fun HTT_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
-*}
-
 lemma HTT_coinduct3:
   "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT"
   apply (erule HTTgen_mono [THEN [3] HTT_def [THEN def_coinduct3]])
   apply assumption
   done
 
-ML {*
-val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
-
-fun HTT_coinduct3_tac ctxt s i =
-  res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
-*}
-
 lemma HTTgenIs:
   "true : HTTgen(R)"
   "false : HTTgen(R)"
diff -r a0e57fb1b930 -r 9721e8e4d48c src/CCL/Term.thy
--- a/src/CCL/Term.thy	Thu Jul 23 21:59:56 2009 +0200
+++ b/src/CCL/Term.thy	Thu Jul 23 22:20:37 2009 +0200
@@ -273,15 +273,12 @@
 
 subsection {* Constructors are injective *}
 
-ML {*
-bind_thms ("term_injs", map (mk_inj_rl @{theory}
-  [@{thm applyB}, @{thm splitB}, @{thm whenBinl}, @{thm whenBinr},
-    @{thm ncaseBsucc}, @{thm lcaseBcons}])
-    ["(inl(a) = inl(a')) <-> (a=a')",
-     "(inr(a) = inr(a')) <-> (a=a')",
-     "(succ(a) = succ(a')) <-> (a=a')",
-     "(a$b = a'$b') <-> (a=a' & b=b')"])
-*}
+lemma term_injs:
+  "(inl(a) = inl(a')) <-> (a=a')"
+  "(inr(a) = inr(a')) <-> (a=a')"
+  "(succ(a) = succ(a')) <-> (a=a')"
+  "(a$b = a'$b') <-> (a=a' & b=b')"
+  by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons)
 
 
 subsection {* Constructors are distinct *}
@@ -295,24 +292,13 @@
 
 subsection {* Rules for pre-order @{text "[="} *}
 
-ML {*
+lemma term_porews:
+  "inl(a) [= inl(a') <-> a [= a'"
+  "inr(b) [= inr(b') <-> b [= b'"
+  "succ(n) [= succ(n') <-> n [= n'"
+  "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"
+  by (simp_all add: data_defs ccl_porews)
 
-local
-  fun mk_thm s =
-    Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s)
-      (fn _ =>
-        rewrite_goals_tac @{thms data_defs} THEN
-        simp_tac (@{simpset} addsimps @{thms ccl_porews}) 1);
-in
-  val term_porews =
-    map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
-      "inr(b) [= inr(b') <-> b [= b'",
-      "succ(n) [= succ(n') <-> n [= n'",
-      "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"]
-end;
-
-bind_thms ("term_porews", term_porews);
-*}
 
 subsection {* Rewriting and Proving *}