author blanchet Wed, 26 Sep 2012 10:00:59 +0200 changeset 49588 9b72d207617b parent 49587 33cf557c7849 child 49589 71aa74965bc9
export "dtor_map_coinduct" theorems, since they're used in one example
 src/HOL/BNF/Examples/Process.thy file | annotate | diff | comparison | revisions src/HOL/BNF/Examples/TreeFI.thy file | annotate | diff | comparison | revisions src/HOL/BNF/Tools/bnf_gfp.ML file | annotate | diff | comparison | revisions
```--- 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])```
```--- 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)"```
```--- 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
[])```