# HG changeset patch
# User blanchet
# Date 1346331159 -7200
# Node ID d0f4f113e43de77c303be15c75566df1ef55e4a8
# Parent  f0ecfa9575a94f37bbe31fb545de53d0424b432c
generate "ctr_sels" theorems

diff -r f0ecfa9575a9 -r d0f4f113e43d src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 14:27:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 14:52:39 2012 +0200
@@ -181,7 +181,7 @@
             Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
           end;
 
-        val sel_thms =
+        val sel_thmss =
           let
             fun mk_thm k xs goal_case case_thm x sel_def =
               let
@@ -197,15 +197,15 @@
             fun mk_thms k xs goal_case case_thm sel_defs =
               map2 (mk_thm k xs goal_case case_thm) xs sel_defs;
           in
-            flat (map5 mk_thms ks xss goal_cases case_thms sel_defss)
+            map5 mk_thms ks xss goal_cases case_thms sel_defss
           end;
 
+        val discD_thms = map (fn def => def RS iffD1) disc_defs;
         val discI_thms =
-          map2 (fn m => fn disc_def => funpow m (fn thm => exI RS thm) (disc_def RS iffD2))
-            ms disc_defs;
+          map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs;
         val not_disc_thms =
-          map2 (fn m => fn disc_def => funpow m (fn thm => allI RS thm)
-                  (Local_Defs.unfold lthy @{thms not_ex} (disc_def RS @{thm ssubst[of _ _ Not]})))
+          map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
+                  (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
             ms disc_defs;
 
         val disc_thms =
@@ -227,13 +227,13 @@
                 HOLogic.mk_Trueprop (HOLogic.mk_not (disc' $ v))));
             fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
 
-            val bundles = ks ~~ ms ~~ disc_defs ~~ discs;
+            val bundles = ks ~~ ms ~~ discD_thms ~~ discs;
             val half_pairs = mk_half_pairs bundles;
 
             val goal_halves = map mk_goal half_pairs;
             val half_thms =
-              map2 (fn ((((k, m), disc_def), _), (((k', _), _), _)) =>
-                prove (mk_half_disc_disjoint_tac m disc_def (get_disc_thm k k')))
+              map2 (fn ((((k, m), discD), _), (((k', _), _), _)) =>
+                prove (mk_half_disc_disjoint_tac m discD (get_disc_thm k k')))
               half_pairs goal_halves;
 
             val goal_other_halves = map (mk_goal o swap) half_pairs;
@@ -251,7 +251,19 @@
             Skip_Proof.prove lthy [] [] goal (fn _ => mk_disc_exhaust_tac n exhaust_thm discI_thms)
           end;
 
-        val ctr_sel_thms = [];
+        val ctr_sel_thms =
+          let
+            fun mk_goal ctr disc sels =
+              Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
+                HOLogic.mk_Trueprop (HOLogic.mk_eq ((null sels ? swap)
+                  (Term.list_comb (ctr, map (fn sel => sel $ v) sels), v)))));
+            val goals = map3 mk_goal ctrs discs selss;
+          in
+            map4 (fn goal => fn m => fn discD => fn sel_thms =>
+              Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+                mk_ctr_sel_tac ctxt m discD sel_thms))
+              goals ms discD_thms sel_thmss
+          end;
 
         val case_disc_thms = [];
 
@@ -281,7 +293,7 @@
         |> note exhaustN [exhaust_thm]
         |> note injectN inject_thms
         |> note nchotomyN [nchotomy_thm]
-        |> note selsN sel_thms
+        |> note selsN (flat sel_thmss)
         |> note splitN split_thms
         |> note split_asmN split_asm_thms
         |> note weak_case_cong_thmsN [weak_case_cong_thms]
diff -r f0ecfa9575a9 -r d0f4f113e43d src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 14:27:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 14:52:39 2012 +0200
@@ -7,6 +7,7 @@
 
 signature BNF_SUGAR_TACTICS =
 sig
+  val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
   val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
@@ -23,8 +24,8 @@
   (rtac allI THEN' rtac exhaust THEN'
    EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
 
-fun mk_half_disc_disjoint_tac m disc_def disc'_thm =
-  (dtac (disc_def RS iffD1) THEN'
+fun mk_half_disc_disjoint_tac m discD disc'_thm =
+  (dtac discD THEN'
    REPEAT_DETERM_N m o etac exE THEN'
    hyp_subst_tac THEN'
    rtac disc'_thm) 1;
@@ -37,4 +38,14 @@
    EVERY' (map2 (fn k => fn discI =>
      dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
 
+fun mk_ctr_sel_tac ctxt m discD sel_thms =
+  (dtac discD THEN'
+   (if m = 0 then
+      atac
+    else
+      REPEAT_DETERM_N m o etac exE THEN'
+      hyp_subst_tac THEN'
+      K (Local_Defs.unfold_tac ctxt sel_thms) THEN'
+      rtac refl)) 1;
+
 end;