# HG changeset patch
# User huffman
# Date 1267725699 28800
# Node ID ee5df989b7c4e540f645e88002efa14ef76ad65a
# Parent  bd8b50e76e94a09038e99282af2ed586f39d1c26
move coinduction-related stuff into function prove_coindunction

diff -r bd8b50e76e94 -r ee5df989b7c4 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Mar 04 08:12:39 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Mar 04 10:01:39 2010 -0800
@@ -196,15 +196,20 @@
         pat_rews @ dist_les @ dist_eqs)
 end; (* let *)
 
-fun comp_theorems (comp_dnam, eqs: eq list) thy =
+fun prove_coinduction
+    (comp_dnam, eqs : eq list)
+    (take_lemmas : thm list)
+    (thy : theory) : thm * theory =
 let
-val map_tab = Domain_Take_Proofs.get_map_tab thy;
 
 val dnames = map (fst o fst) eqs;
-val conss  = map  snd        eqs;
 val comp_dname = Sign.full_bname thy comp_dnam;
+fun dc_take dn = %%:(dn^"_take");
+val x_name = idx_name dnames "x"; 
+val n_eqs = length eqs;
 
-val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+val take_rews =
+    maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
 
 (* ----- define bisimulation predicate -------------------------------------- *)
 
@@ -280,6 +285,74 @@
         ||> Sign.parent_path;
 end; (* local *)
 
+(* ----- theorem concerning coinduction ------------------------------------- *)
+
+local
+  val pg = pg' thy;
+  val xs = mapn (fn n => K (x_name n)) 1 dnames;
+  fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
+  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
+  val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+  val _ = trace " Proving coind_lemma...";
+  val coind_lemma =
+    let
+      fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
+      fun mk_eqn n dn =
+        (dc_take dn $ %:"n" ` bnd_arg n 0) ===
+        (dc_take dn $ %:"n" ` bnd_arg n 1);
+      fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
+      val goal =
+        mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
+          Library.foldr mk_all2 (xs,
+            Library.foldr mk_imp (mapn mk_prj 0 dnames,
+              foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
+      fun x_tacs ctxt n x = [
+        rotate_tac (n+1) 1,
+        etac all2E 1,
+        eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
+        TRY (safe_tac HOL_cs),
+        REPEAT (CHANGED (asm_simp_tac take_ss 1))];
+      fun tacs ctxt = [
+        rtac impI 1,
+        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
+        simp_tac take_ss 1,
+        safe_tac HOL_cs] @
+        flat (mapn (x_tacs ctxt) 0 xs);
+    in pg [ax_bisim_def] goal tacs end;
+in
+  val _ = trace " Proving coind...";
+  val coind = 
+    let
+      fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
+      fun mk_eqn x = %:x === %:(x^"'");
+      val goal =
+        mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
+          Logic.list_implies (mapn mk_prj 0 xs,
+            mk_trp (foldr1 mk_conj (map mk_eqn xs)));
+      val tacs =
+        TRY (safe_tac HOL_cs) ::
+        maps (fn take_lemma => [
+          rtac take_lemma 1,
+          cut_facts_tac [coind_lemma] 1,
+          fast_tac HOL_cs 1])
+        take_lemmas;
+    in pg [] goal (K tacs) end;
+end; (* local *)
+
+in
+  (coind, thy)
+end;
+
+fun comp_theorems (comp_dnam, eqs: eq list) thy =
+let
+val map_tab = Domain_Take_Proofs.get_map_tab thy;
+
+val dnames = map (fst o fst) eqs;
+val conss  = map  snd        eqs;
+val comp_dname = Sign.full_bname thy comp_dnam;
+
+val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+
 val pg = pg' thy;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
@@ -556,58 +629,7 @@
 
 end; (* local *)
 
-(* ----- theorem concerning coinduction ------------------------------------- *)
-
-local
-  val xs = mapn (fn n => K (x_name n)) 1 dnames;
-  fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
-  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
-  val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
-  val _ = trace " Proving coind_lemma...";
-  val coind_lemma =
-    let
-      fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
-      fun mk_eqn n dn =
-        (dc_take dn $ %:"n" ` bnd_arg n 0) ===
-        (dc_take dn $ %:"n" ` bnd_arg n 1);
-      fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
-      val goal =
-        mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
-          Library.foldr mk_all2 (xs,
-            Library.foldr mk_imp (mapn mk_prj 0 dnames,
-              foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
-      fun x_tacs ctxt n x = [
-        rotate_tac (n+1) 1,
-        etac all2E 1,
-        eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
-        TRY (safe_tac HOL_cs),
-        REPEAT (CHANGED (asm_simp_tac take_ss 1))];
-      fun tacs ctxt = [
-        rtac impI 1,
-        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
-        simp_tac take_ss 1,
-        safe_tac HOL_cs] @
-        flat (mapn (x_tacs ctxt) 0 xs);
-    in pg [ax_bisim_def] goal tacs end;
-in
-  val _ = trace " Proving coind...";
-  val coind = 
-    let
-      fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
-      fun mk_eqn x = %:x === %:(x^"'");
-      val goal =
-        mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
-          Logic.list_implies (mapn mk_prj 0 xs,
-            mk_trp (foldr1 mk_conj (map mk_eqn xs)));
-      val tacs =
-        TRY (safe_tac HOL_cs) ::
-        maps (fn take_lemma => [
-          rtac take_lemma 1,
-          cut_facts_tac [coind_lemma] 1,
-          fast_tac HOL_cs 1])
-        take_lemmas;
-    in pg [] goal (K tacs) end;
-end; (* local *)
+val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy;
 
 val inducts = Project_Rule.projections (ProofContext.init thy) ind;
 fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);