# HG changeset patch
# User blanchet
# Date 1348646459 -7200
# Node ID 9b72d207617b6986de8a75f7fbe72168b36c2f36
# Parent  33cf557c7849833dcb4757c96072fc0ba84c6755
export "dtor_map_coinduct" theorems, since they're used in one example

diff -r 33cf557c7849 -r 9b72d207617b src/HOL/BNF/Examples/Process.thy
--- a/src/HOL/BNF/Examples/Process.thy	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Examples/Process.thy	Wed Sep 26 10:00:59 2012 +0200
@@ -75,7 +75,7 @@
 Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> (\<phi> p p' \<or> p = p')" and
 Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
 shows "p = p'"
-proof(intro mp[OF process.dtor_rel_strong_coinduct, of \<phi>, OF _ phi], clarify)
+proof(intro mp[OF process.dtor_strong_coinduct, of \<phi>, OF _ phi], clarify)
   fix p p'  assume \<phi>: "\<phi> p p'"
   show "pre_process_rel (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_dtor p) (process_dtor p')"
   proof(cases rule: process.exhaust[of p])
diff -r 33cf557c7849 -r 9b72d207617b src/HOL/BNF/Examples/TreeFI.thy
--- a/src/HOL/BNF/Examples/TreeFI.thy	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Wed Sep 26 10:00:59 2012 +0200
@@ -52,7 +52,7 @@
    lengthh (sub a) = lengthh (sub b) \<and>
    (\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))"
 shows "x = y"
-proof (rule mp[OF treeFI.dtor_coinduct, of phi, OF _ *])
+proof (rule mp[OF treeFI.dtor_map_coinduct, of phi, OF _ *])
   fix a b :: "'a treeFI"
   let ?zs = "zipp (sub a) (sub b)"
   let ?z = "(lab a, ?zs)"
diff -r 33cf557c7849 -r 9b72d207617b src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -2969,11 +2969,11 @@
 
       val common_notes =
         [(dtor_coinductN, [dtor_coinduct_thm]),
+        (dtor_map_coinductN, [dtor_map_coinduct_thm]),
+        (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
         (dtor_strong_coinductN, [dtor_strong_coinduct_thm])] @
         (if note_all then
-           [(dtor_map_coinductN, [dtor_map_coinduct_thm]),
-           (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
-           (dtor_srel_coinductN, [dtor_srel_coinduct_thm]),
+           [(dtor_srel_coinductN, [dtor_srel_coinduct_thm]),
            (dtor_srel_strong_coinductN, [dtor_srel_strong_coinduct_thm])]
          else
            [])