src/HOLCF/Tools/Domain/domain_theorems.ML
 changeset 35599 20670f5564e9 parent 35597 e4331b99b03f child 35601 50ba5010b876
```--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 14:50:37 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 15:25:59 2010 -0800
@@ -440,7 +440,7 @@
fun prove_coinduction
(comp_dnam, eqs : eq list)
(take_lemmas : thm list)
-    (thy : theory) : thm * theory =
+    (thy : theory) : theory =
let

val dnames = map (fst o fst) eqs;
@@ -580,9 +580,10 @@
in pg [] goal (K tacs) end;
end; (* local *)

-in
-  (coind, thy)
-end;
+       |> snd o PureThy.add_thmss [((Binding.name "coind", [coind]), [])]
+       |> Sign.parent_path
+end; (* let *)

fun comp_theorems (comp_dnam, eqs: eq list) thy =
let
@@ -591,8 +592,6 @@
val dnames = map (fst o fst) eqs;
val comp_dname = Sign.full_bname thy comp_dnam;

-val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
-
(* ----- getting the composite axiom and definitions ------------------------ *)

(* Test for indirect recursion *)
@@ -603,9 +602,10 @@
fun indirect_eq (_, cons) = exists indirect_con cons;
in
val is_indirect = exists indirect_eq eqs;
-  val _ = if is_indirect
-          then message "Definition uses indirect recursion."
-          else ();
+  val _ =
+      if is_indirect
+      then message "Indirect recursion detected, skipping proofs of (co)induction rules"
+      else message ("Proving induction properties of domain "^comp_dname^" ...");
end;

@@ -638,13 +638,14 @@
if is_indirect then thy else
prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy;

-val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy;
+val thy =
+    if is_indirect then thy else
+    prove_coinduction (comp_dnam, eqs) take_lemmas thy;