implemented "mk_exhaust_tac"
authorblanchet
Tue Sep 04 15:51:32 2012 +0200 (2012-09-04)
changeset 491255fc5211cf104
parent 49124 968e1b7de057
child 49126 1bbd7a37fc29
implemented "mk_exhaust_tac"
src/HOL/Codatatype/BNF_Library.thy
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_gfp_util.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
src/HOL/Codatatype/Tools/bnf_tactics.ML
src/HOL/Codatatype/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/Codatatype/BNF_Library.thy	Tue Sep 04 14:21:11 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_Library.thy	Tue Sep 04 15:51:32 2012 +0200
     1.3 @@ -17,6 +17,19 @@
     1.4  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
     1.5  by (erule iffI) (erule contrapos_pn)
     1.6  
     1.7 +lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
     1.8 +
     1.9 +lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by auto
    1.10 +
    1.11 +lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
    1.12 +by presburger
    1.13 +
    1.14 +lemma case_unit: "(case u of () => f) = f"
    1.15 +by (cases u) (hypsubst, rule unit.cases)
    1.16 +
    1.17 +lemma All_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
    1.18 +by presburger
    1.19 +
    1.20  lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    1.21  by blast
    1.22  
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 14:21:11 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 15:51:32 2012 +0200
     2.3 @@ -166,13 +166,21 @@
     2.4              Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
     2.5                mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unf_T, T]) (certify lthy fld)
     2.6                  (certify lthy unf) fld_unf unf_fld)
     2.7 +            |> Thm.close_derivation
     2.8            end;
     2.9  
    2.10 +        val sumEN_thm = mk_sumEN n;
    2.11 +        val sumEN_thm' =
    2.12 +          let val cTs = map (SOME o certifyT lthy) prod_Ts in
    2.13 +            Local_Defs.unfold lthy @{thms all_unit_eq} (Drule.instantiate' cTs [] sumEN_thm)
    2.14 +          end;
    2.15 +
    2.16 +        fun exhaust_tac {context = ctxt, ...} =
    2.17 +          mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm';
    2.18 +
    2.19          (* ### *)
    2.20          fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
    2.21  
    2.22 -        val exhaust_tac = cheat_tac;
    2.23 -
    2.24          val inject_tacss = map (fn 0 => [] | _ => [cheat_tac]) ms;
    2.25  
    2.26          val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 14:21:11 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 15:51:32 2012 +0200
     3.3 @@ -7,6 +7,7 @@
     3.4  
     3.5  signature BNF_FP_SUGAR_TACTICS =
     3.6  sig
     3.7 +  val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
     3.8    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     3.9      -> tactic
    3.10  end;
    3.11 @@ -14,8 +15,17 @@
    3.12  structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
    3.13  struct
    3.14  
    3.15 +open BNF_Tactics
    3.16  open BNF_Util
    3.17  
    3.18 +fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
    3.19 +  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN
    3.20 +  rtac sumEN' 1 THEN
    3.21 +  Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
    3.22 +  EVERY' (map2 (fn k => fn m =>
    3.23 +     select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' etac @{thm meta_mp}) k THEN'
    3.24 +     atac) (1 upto n) ms) 1;
    3.25 +
    3.26  fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
    3.27    (rtac iffI THEN'
    3.28     EVERY' (map3 (fn cTs => fn cx => fn th =>
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 04 14:21:11 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 04 15:51:32 2012 +0200
     4.3 @@ -85,6 +85,8 @@
     4.4    val mk_Field: term -> term
     4.5    val mk_union: term * term -> term
     4.6  
     4.7 +  val mk_sumEN: int -> thm
     4.8 +
     4.9    val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
    4.10  
    4.11    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
    4.12 @@ -210,6 +212,15 @@
    4.13        if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
    4.14    in split limit 1 th end;
    4.15  
    4.16 +local
    4.17 +  fun mk_sumEN' 1 = @{thm obj_sum_step}
    4.18 +    | mk_sumEN' n = mk_sumEN' (n - 1) RSN (2, @{thm obj_sum_step});
    4.19 +in
    4.20 +  fun mk_sumEN 1 = @{thm obj_sum_base}
    4.21 +    | mk_sumEN 2 = @{thm sumE}
    4.22 +    | mk_sumEN n = (mk_sumEN' (n - 2) RSN (2, @{thm obj_sumE})) OF replicate n (impI RS allI);
    4.23 +end;
    4.24 +
    4.25  fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
    4.26    [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
    4.27  
     5.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 14:21:11 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 15:51:32 2012 +0200
     5.3 @@ -9,8 +9,8 @@
     5.4  
     5.5  signature BNF_GFP =
     5.6  sig
     5.7 -  val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> Proof.context ->
     5.8 -    (term list * term list * thm list * thm list) * Proof.context
     5.9 +  val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
    5.10 +    (term list * term list * thm list * thm list) * local_theory
    5.11  end;
    5.12  
    5.13  structure BNF_GFP : BNF_GFP =
     6.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Tue Sep 04 14:21:11 2012 +0200
     6.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML	Tue Sep 04 15:51:32 2012 +0200
     6.3 @@ -40,7 +40,6 @@
     6.4  
     6.5    val mk_specN: int -> thm -> thm
     6.6    val mk_sum_casesN: int -> int -> thm
     6.7 -  val mk_sumEN: int -> thm
     6.8  
     6.9    val mk_InN_Field: int -> int -> thm
    6.10    val mk_InN_inject: int -> int -> thm
    6.11 @@ -218,15 +217,6 @@
    6.12    | mk_sum_casesN 2 2 = @{thm sum.cases(2)}
    6.13    | mk_sum_casesN n m = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (m - 1)];
    6.14  
    6.15 -local
    6.16 -  fun mk_sumEN' 1 = @{thm obj_sum_step}
    6.17 -    | mk_sumEN' n = mk_sumEN' (n - 1) RSN (2, @{thm obj_sum_step});
    6.18 -in
    6.19 -  fun mk_sumEN 1 = @{thm obj_sum_base}
    6.20 -    | mk_sumEN 2 = @{thm sumE}
    6.21 -    | mk_sumEN n = (mk_sumEN' (n - 2) RSN (2, @{thm obj_sumE})) OF replicate n (impI RS allI);
    6.22 -end;
    6.23 -
    6.24  fun mk_rec_simps n rec_thm defs = map (fn i =>
    6.25    map (fn def => def RS rec_thm RS mk_nthI n i RS fun_cong) defs) (1 upto n);
    6.26  
     7.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 14:21:11 2012 +0200
     7.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 15:51:32 2012 +0200
     7.3 @@ -8,8 +8,8 @@
     7.4  
     7.5  signature BNF_LFP =
     7.6  sig
     7.7 -  val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> Proof.context ->
     7.8 -    (term list * term list * thm list * thm list) * Proof.context
     7.9 +  val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
    7.10 +    (term list * term list * thm list * thm list) * local_theory
    7.11  end;
    7.12  
    7.13  structure BNF_LFP : BNF_LFP =
     8.1 --- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Tue Sep 04 14:21:11 2012 +0200
     8.2 +++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Tue Sep 04 15:51:32 2012 +0200
     8.3 @@ -10,6 +10,7 @@
     8.4  sig
     8.5    val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
     8.6    val fo_rtac: thm -> Proof.context -> int -> tactic
     8.7 +  val subst_asm_tac: Proof.context -> thm list -> int -> tactic
     8.8    val subst_tac: Proof.context -> thm list -> int -> tactic
     8.9    val substs_tac: Proof.context -> thm list -> int -> tactic
    8.10  
    8.11 @@ -70,6 +71,7 @@
    8.12    end);
    8.13  
    8.14  (*unlike "unfold_tac", succeeds when the RHS contains schematic variables not in the LHS*)
    8.15 +fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
    8.16  fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
    8.17  fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
    8.18  
     9.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 14:21:11 2012 +0200
     9.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 15:51:32 2012 +0200
     9.3 @@ -303,6 +303,7 @@
     9.4                mk_not_other_disc_def_tac ctxt (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
     9.5                  exhaust_thm')
     9.6              |> singleton (Proof_Context.export names_lthy lthy)
     9.7 +            |> Thm.close_derivation
     9.8            end;
     9.9  
    9.10          val has_not_other_disc_def =