# HG changeset patch
# User traytel
# Date 1368007062 -7200
# Node ID f964a98877131b620dadf0cf59675ea2dc51be59
# Parent  eac9e9a45bf53b3dee46b63b28879f29aaba9660
store proper theorems even for fixed points that have no passive live variables

diff -r eac9e9a45bf5 -r f964a9887713 src/HOL/BNF/BNF_Def.thy
--- a/src/HOL/BNF/BNF_Def.thy	Wed May 08 09:45:30 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Wed May 08 11:57:42 2013 +0200
@@ -182,7 +182,7 @@
   A \<subseteq> Collect (split Q)"
   by fastforce
 
-lemma predicate2_cong: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
+lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
 by metis
 
 ML_file "Tools/bnf_def_tactics.ML"
diff -r eac9e9a45bf5 -r f964a9887713 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed May 08 09:45:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed May 08 11:57:42 2013 +0200
@@ -1095,7 +1095,7 @@
             val cts = map (SOME o certify lthy) Rs;
             val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
           in
-            unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_cong})
+            unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
             |> singleton (Proof_Context.export names_lthy pre_names_lthy)
           end;
 
diff -r eac9e9a45bf5 -r f964a9887713 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed May 08 09:45:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed May 08 11:57:42 2013 +0200
@@ -2297,12 +2297,17 @@
 
     val timer = time (timer "coinduction");
 
+    fun mk_dtor_map_DEADID_thm dtor_inject =
+      trans OF [iffD2 OF [dtor_inject, id_apply], id_apply RS sym];
+
+    fun mk_dtor_Irel_DEADID_thm dtor_inject bnf =
+      trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym;
+
     (*register new codatatypes as BNFs*)
     val (Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms, lthy) =
       if m = 0 then
-        let val dummy_thms = replicate n Drule.dummy_thm in
-          (replicate n DEADID_bnf, dummy_thms, replicate n [], dummy_thms, lthy)
-        end
+        (replicate n DEADID_bnf, map mk_dtor_map_DEADID_thm dtor_inject_thms, replicate n [],
+        map2 mk_dtor_Irel_DEADID_thm dtor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
         val gTs = map2 (curry op -->) passiveBs passiveCs;
diff -r eac9e9a45bf5 -r f964a9887713 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed May 08 09:45:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed May 08 11:57:42 2013 +0200
@@ -1360,12 +1360,17 @@
 
     val timer = time (timer "induction");
 
+    fun mk_ctor_map_DEADID_thm ctor_inject =
+      trans OF [id_apply, iffD2 OF [ctor_inject, id_apply RS sym]];
+
+    fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
+      trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
+
     (*register new datatypes as BNFs*)
     val (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
       if m = 0 then
-        let val dummy_thms = replicate n Drule.dummy_thm in
-          (replicate n DEADID_bnf, dummy_thms, replicate n [], dummy_thms, lthy)
-        end
+        (replicate n DEADID_bnf, map mk_ctor_map_DEADID_thm ctor_inject_thms, replicate n [],
+        map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
         val f1Ts = map2 (curry op -->) passiveAs passiveYs;