# HG changeset patch
# User blanchet
# Date 1346326925 -7200
# Node ID 487427a02beeeb41bb1cf595f7aa380921f966ec
# Parent  fc3b9b49c92dd3286578aa5ddbd4817d415aa1fa
generate "disc_distinct" theorems

diff -r fc3b9b49c92d -r 487427a02bee src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 11:31:47 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 13:42:05 2012 +0200
@@ -29,10 +29,13 @@
 val split_asmN = "split_asm"
 val weak_case_cong_thmsN = "weak_case_cong"
 
-fun index_of_triangle_row _ 0 = 0
-  | index_of_triangle_row n j = index_of_triangle_row n (j - 1) + n - j;
+fun mk_half_pairs [] = []
+  | mk_half_pairs (x :: xs) = fold_rev (cons o pair x) xs (mk_half_pairs xs);
 
-fun index_of_triangle_cell n j k = index_of_triangle_row n j + k - (j + 1);
+fun index_of_half_row _ 0 = 0
+  | index_of_half_row n j = index_of_half_row n (j - 1) + n - j;
+
+fun index_of_half_cell n j k = index_of_half_row n j + k - (j + 1);
 
 fun prepare_sugar prep_term (((raw_ctrs, raw_caseof), disc_names), sel_namess) no_defs_lthy =
   let
@@ -57,24 +60,22 @@
     fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
 
     fun mk_ctr Ts ctr =
-      let
-        val Ts0 = snd (dest_Type (body_type (fastype_of ctr)));
-      in
+      let val Ts0 = snd (dest_Type (body_type (fastype_of ctr))) in
         Term.subst_atomic_types (Ts0 ~~ Ts) ctr
       end;
 
-    fun mk_caseof T =
-      let
-        val (binders, body) = strip_type (fastype_of caseof0);
-      in
-        Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ As)) caseof0
+    fun mk_caseof Ts T =
+      let val (binders, body) = strip_type (fastype_of caseof0) in
+        Term.subst_atomic_types ((body, T) :: (snd (dest_Type (List.last binders)) ~~ Ts)) caseof0
       end;
 
     val T = Type (T_name, As);
     val ctrs = map (mk_ctr As) ctrs0;
     val ctr_Tss = map (binder_types o fastype_of) ctrs;
 
-    val caseofB = mk_caseof B;
+    val ms = map length ctr_Tss;
+
+    val caseofB = mk_caseof As B;
     val caseofB_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
 
     val (((((xss, yss), fs), (v, v')), p), _) = no_defs_lthy |>
@@ -98,32 +99,37 @@
       HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (Binding.name_of b, T --> HOLogic.boolT) $ v,
         exist_xs_v_eq_ctr));
 
-    fun sel_spec b x xs xctr k =
+    fun sel_spec b x xs k =
       let val T' = fastype_of x in
         HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (Binding.name_of b, T --> T') $ v,
-            Term.list_comb (mk_caseof T', mk_caseof_args k xs x T') $ v))
+            Term.list_comb (mk_caseof As T', mk_caseof_args k xs x T') $ v))
       end;
 
-    val (((discs0, (_, disc_defs0)), (selss0, (_, sel_defss0))), (lthy', lthy)) =
+    val (((raw_discs, (_, raw_disc_defs)), (raw_selss, (_, raw_sel_defss))), (lthy', lthy)) =
       no_defs_lthy
       |> apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn exist_xs_v_eq_ctr =>
         Specification.definition (SOME (b, NONE, NoSyn),
           ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr))) disc_names exist_xs_v_eq_ctrs
-      ||>> apfst (apsnd split_list o split_list) o fold_map4 (fn bs => fn xs => fn xctr => fn k =>
+      ||>> apfst (apsnd split_list o split_list) o fold_map3 (fn bs => fn xs => fn k =>
         apfst (apsnd split_list o split_list) o fold_map2 (fn b => fn x =>
           Specification.definition (SOME (b, NONE, NoSyn),
-            ((Thm.def_binding b, []), sel_spec b x xs xctr k))) bs xs) sel_namess xss xctrs
-            ks
+            ((Thm.def_binding b, []), sel_spec b x xs k))) bs xs) sel_namess xss ks
       ||> `Local_Theory.restore;
 
     (*transforms defined frees into consts (and more)*)
     val phi = Proof_Context.export_morphism lthy lthy';
 
-    val disc_defs = map (Morphism.thm phi) disc_defs0;
-    val sel_defss = map (map (Morphism.thm phi)) sel_defss0;
+    val disc_defs = map (Morphism.thm phi) raw_disc_defs;
+    val sel_defss = map (map (Morphism.thm phi)) raw_sel_defss;
+
+    val discs0 = map (Morphism.term phi) raw_discs;
+    val selss0 = map (map (Morphism.term phi)) raw_selss;
 
-    val discs = map (Morphism.term phi) discs0;
-    val selss = map (map (Morphism.term phi)) selss0;
+    fun mk_disc_or_sel Ts t =
+      Term.subst_atomic_types (snd (dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+
+    val discs = map (mk_disc_or_sel As) discs0;
+    val selss = map (map (mk_disc_or_sel As)) selss0;
 
     val goal_exhaust =
       let
@@ -146,22 +152,15 @@
       end;
 
     val goal_half_distincts =
-      let
-        fun mk_goal t u = HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (t, u)));
-        fun mk_goals [] = []
-          | mk_goals (t :: ts) = fold_rev (cons o mk_goal t) ts (mk_goals ts);
-      in
-        mk_goals xctrs
-      end;
+      map (HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_eq) (mk_half_pairs xctrs);
 
     val goal_cases =
       let
         val lhs0 = Term.list_comb (caseofB, eta_fs);
-        fun mk_goal k xctr xs f =
-          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs0 $ xctr, Term.list_comb (f, xs)))
-          |> tap (tracing o prefix "HERE: " o PolyML.makestring)(*###*);
+        fun mk_goal xctr xs f =
+          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs0 $ xctr, Term.list_comb (f, xs)));
       in
-        map4 mk_goal ks xctrs xss fs
+        map3 mk_goal xctrs xss fs
       end;
 
     val goals = [[goal_exhaust], goal_injects, goal_half_distincts, goal_cases];
@@ -183,7 +182,7 @@
 
         val sel_thms =
           let
-            fun mk_thm k xs goal_case case_thm x sel sel_def =
+            fun mk_thm k xs goal_case case_thm x sel_def =
               let
                 val T = fastype_of x;
                 val cTs =
@@ -194,28 +193,54 @@
                 Local_Defs.fold lthy [sel_def]
                   (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm)
               end;
-            fun mk_thms k xs goal_case case_thm sels sel_defs =
-              map3 (mk_thm k xs goal_case case_thm) xs sels sel_defs;
+            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 (map6 mk_thms ks xss goal_cases case_thms selss sel_defss)
+            flat (map5 mk_thms ks xss goal_cases case_thms sel_defss)
           end;
 
+        val discI_thms =
+          map2 (fn m => fn disc_def => funpow m (fn thm => exI RS thm) (disc_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]})))
+            ms disc_defs;
+
         val disc_thms =
           let
             fun get_distinct_thm k k' =
-              if k > k' then nth half_distinct_thms (index_of_triangle_cell n (k' - 1) (k - 1))
-              else nth other_half_distinct_thms (index_of_triangle_cell n (k' - 1) (k' - 1))
-            fun mk_thm ((k, m), disc_def) k' =
-              if k = k' then
-                refl RS (funpow m (fn thm => exI RS thm) (disc_def RS iffD2))
-              else
-                get_distinct_thm k k' RS (funpow m (fn thm => allI RS thm)
-                  (Local_Defs.unfold lthy @{thms not_ex} (disc_def RS @{thm ssubst[of _ _ Not]})));
+              if k > k' then nth half_distinct_thms (index_of_half_cell n (k' - 1) (k - 1))
+              else nth other_half_distinct_thms (index_of_half_cell n (k' - 1) (k' - 1))
+            fun mk_thm ((k, discI), not_disc) k' =
+              if k = k' then refl RS discI else get_distinct_thm k k' RS not_disc;
           in
-            map_product mk_thm (ks ~~ map length ctr_Tss ~~ disc_defs) ks
+            map_product mk_thm (ks ~~ discI_thms ~~ not_disc_thms) ks
           end;
 
-        val disc_disjoint_thms = [];
+        val disc_disjoint_thms =
+          let
+            fun get_disc_thm k k' = nth disc_thms ((k' - 1) * n + (k - 1));
+            fun mk_goal ((_, disc), (_, disc')) =
+              Logic.mk_implies (HOLogic.mk_Trueprop (disc $ v),
+                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 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')))
+              half_pairs goal_halves;
+
+            val goal_other_halves = map (mk_goal o swap) half_pairs;
+            val other_half_thms =
+              map2 (prove o mk_other_half_disc_disjoint_tac) half_thms goal_other_halves;
+          in
+            half_thms @ other_half_thms
+          end;
 
         val disc_exhaust_thms = [];
 
diff -r fc3b9b49c92d -r 487427a02bee src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 11:31:47 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Thu Aug 30 13:42:05 2012 +0200
@@ -8,6 +8,8 @@
 signature BNF_SUGAR_TACTICS =
 sig
   val mk_nchotomy_tac: int -> thm -> tactic
+  val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic
+  val mk_other_half_disc_disjoint_tac: thm -> tactic
 end;
 
 structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
@@ -19,4 +21,13 @@
   (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'
+   REPEAT_DETERM_N m o etac exE THEN'
+   hyp_subst_tac THEN'
+   rtac disc'_thm) 1;
+
+fun mk_other_half_disc_disjoint_tac half_thm =
+  (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
+
 end;