# HG changeset patch
# User blanchet
# Date 1346766692 -7200
# Node ID 5fc5211cf1041174c4baa6c3f421522e8cca9d21
# Parent  968e1b7de057957b7fc801e2a4d9fabdb1237f51
implemented "mk_exhaust_tac"

diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/BNF_Library.thy
--- a/src/HOL/Codatatype/BNF_Library.thy	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Library.thy	Tue Sep 04 15:51:32 2012 +0200
@@ -17,6 +17,19 @@
 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
 by (erule iffI) (erule contrapos_pn)
 
+lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
+
+lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by auto
+
+lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
+by presburger
+
+lemma case_unit: "(case u of () => f) = f"
+by (cases u) (hypsubst, rule unit.cases)
+
+lemma All_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
+by presburger
+
 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
 by blast
 
diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -166,13 +166,21 @@
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
               mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unf_T, T]) (certify lthy fld)
                 (certify lthy unf) fld_unf unf_fld)
+            |> Thm.close_derivation
           end;
 
+        val sumEN_thm = mk_sumEN n;
+        val sumEN_thm' =
+          let val cTs = map (SOME o certifyT lthy) prod_Ts in
+            Local_Defs.unfold lthy @{thms all_unit_eq} (Drule.instantiate' cTs [] sumEN_thm)
+          end;
+
+        fun exhaust_tac {context = ctxt, ...} =
+          mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm';
+
         (* ### *)
         fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
 
-        val exhaust_tac = cheat_tac;
-
         val inject_tacss = map (fn 0 => [] | _ => [cheat_tac]) ms;
 
         val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);
diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -7,6 +7,7 @@
 
 signature BNF_FP_SUGAR_TACTICS =
 sig
+  val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
   val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     -> tactic
 end;
@@ -14,8 +15,17 @@
 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
 struct
 
+open BNF_Tactics
 open BNF_Util
 
+fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
+  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN
+  rtac sumEN' 1 THEN
+  Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
+  EVERY' (map2 (fn k => fn m =>
+     select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' etac @{thm meta_mp}) k THEN'
+     atac) (1 upto n) ms) 1;
+
 fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
   (rtac iffI THEN'
    EVERY' (map3 (fn cTs => fn cx => fn th =>
diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -85,6 +85,8 @@
   val mk_Field: term -> term
   val mk_union: term * term -> term
 
+  val mk_sumEN: int -> thm
+
   val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
@@ -210,6 +212,15 @@
       if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
   in split limit 1 th end;
 
+local
+  fun mk_sumEN' 1 = @{thm obj_sum_step}
+    | mk_sumEN' n = mk_sumEN' (n - 1) RSN (2, @{thm obj_sum_step});
+in
+  fun mk_sumEN 1 = @{thm obj_sum_base}
+    | mk_sumEN 2 = @{thm sumE}
+    | mk_sumEN n = (mk_sumEN' (n - 2) RSN (2, @{thm obj_sumE})) OF replicate n (impI RS allI);
+end;
+
 fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
   [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
 
diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -9,8 +9,8 @@
 
 signature BNF_GFP =
 sig
-  val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> Proof.context ->
-    (term list * term list * thm list * thm list) * Proof.context
+  val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
+    (term list * term list * thm list * thm list) * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/Tools/bnf_gfp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -40,7 +40,6 @@
 
   val mk_specN: int -> thm -> thm
   val mk_sum_casesN: int -> int -> thm
-  val mk_sumEN: int -> thm
 
   val mk_InN_Field: int -> int -> thm
   val mk_InN_inject: int -> int -> thm
@@ -218,15 +217,6 @@
   | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
   | mk_sum_casesN n m = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (m - 1)];
 
-local
-  fun mk_sumEN' 1 = @{thm obj_sum_step}
-    | mk_sumEN' n = mk_sumEN' (n - 1) RSN (2, @{thm obj_sum_step});
-in
-  fun mk_sumEN 1 = @{thm obj_sum_base}
-    | mk_sumEN 2 = @{thm sumE}
-    | mk_sumEN n = (mk_sumEN' (n - 2) RSN (2, @{thm obj_sumE})) OF replicate n (impI RS allI);
-end;
-
 fun mk_rec_simps n rec_thm defs = map (fn i =>
   map (fn def => def RS rec_thm RS mk_nthI n i RS fun_cong) defs) (1 upto n);
 
diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -8,8 +8,8 @@
 
 signature BNF_LFP =
 sig
-  val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> Proof.context ->
-    (term list * term list * thm list * thm list) * Proof.context
+  val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
+    (term list * term list * thm list * thm list) * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/Tools/bnf_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -10,6 +10,7 @@
 sig
   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
   val fo_rtac: thm -> Proof.context -> int -> tactic
+  val subst_asm_tac: Proof.context -> thm list -> int -> tactic
   val subst_tac: Proof.context -> thm list -> int -> tactic
   val substs_tac: Proof.context -> thm list -> int -> tactic
 
@@ -70,6 +71,7 @@
   end);
 
 (*unlike "unfold_tac", succeeds when the RHS contains schematic variables not in the LHS*)
+fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
 fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
 fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
 
diff -r 968e1b7de057 -r 5fc5211cf104 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 15:51:32 2012 +0200
@@ -303,6 +303,7 @@
               mk_not_other_disc_def_tac ctxt (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
                 exhaust_thm')
             |> singleton (Proof_Context.export names_lthy lthy)
+            |> Thm.close_derivation
           end;
 
         val has_not_other_disc_def =