src/CCL/Term.thy

   napplyBzero napplyBsucc
 
 
 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 *}
 
 ML {*

 *}
 
 
 subsection {* Rules for pre-order @{text "[="} *}
 
-ML {*
-
-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);
-*}
+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)
+
 
 subsection {* Rewriting and Proving *}
 
 ML {*
   bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});