# HG changeset patch
# User blanchet
# Date 1346338968 -7200
# Node ID 23ef2d429931f9d3af98b40bfb2f327161689521
# Parent  c2a7bedd57d85e2b90dcb27c6ffcf8da84f3ca98
generate "weak_case_cong" property

diff -r c2a7bedd57d8 -r 23ef2d429931 src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 16:50:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 17:02:48 2012 +0200
@@ -290,24 +290,29 @@
             |> singleton (Proof_Context.export names_lthy lthy)
           end;
 
-        val case_cong_thm =
+        val (case_cong_thm, weak_case_cong_thm) =
           let
             fun mk_prem xctr xs f g =
               fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
                 mk_Trueprop_eq (f, g)));
-            fun mk_caseof_term fs v = Term.list_comb (caseofB, fs) $ v;
+            fun mk_caseof_term fs = Term.list_comb (caseofB, fs);
+
+            val v_eq_w = mk_Trueprop_eq (v, w);
+            val caseof_fs = mk_caseof_term eta_fs;
+            val caseof_gs = mk_caseof_term eta_gs;
 
             val goal =
-              Logic.list_implies (mk_Trueprop_eq (v, w) :: map4 mk_prem xctrs xss fs gs,
-                 mk_Trueprop_eq (mk_caseof_term eta_fs v, mk_caseof_term eta_gs w));
+              Logic.list_implies (v_eq_w :: map4 mk_prem xctrs xss fs gs,
+                 mk_Trueprop_eq (caseof_fs $ v, caseof_gs $ w));
+            val goal_weak =
+              Logic.mk_implies (v_eq_w, mk_Trueprop_eq (caseof_fs $ v, caseof_fs $ w));
           in
-            Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_case_cong_tac ctxt exhaust_thm' case_thms)
-            |> singleton (Proof_Context.export names_lthy lthy)
+            (Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+               mk_case_cong_tac ctxt exhaust_thm' case_thms),
+             Skip_Proof.prove lthy [] [] goal_weak (K (etac arg_cong 1)))
+            |> pairself (singleton (Proof_Context.export names_lthy lthy))
           end;
 
-        val weak_case_cong_thms = TrueI;
-
         val split_thms = [];
 
         val split_asm_thms = [];
@@ -333,7 +338,7 @@
         |> note selsN (flat sel_thmss)
         |> note splitN split_thms
         |> note split_asmN split_asm_thms
-        |> note weak_case_cong_thmsN [weak_case_cong_thms]
+        |> note weak_case_cong_thmsN [weak_case_cong_thm]
       end;
   in
     (goals, after_qed, lthy')