implemented "mk_inject_tac"
authorblanchet
Tue Sep 04 16:17:22 2012 +0200 (2012-09-04)
changeset 491261bbd7a37fc29
parent 49125 5fc5211cf104
child 49127 f7326a0d7f19
implemented "mk_inject_tac"
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 15:51:32 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 16:17:22 2012 +0200
     1.3 @@ -107,21 +107,22 @@
     1.4  
     1.5      val eqs = map dest_TFree Bs ~~ sum_prod_TsBs;
     1.6  
     1.7 -    val ((raw_flds, raw_unfs, fld_unfs, unf_flds), lthy') = fp_bnf construct bs eqs lthy;
     1.8 +    val ((raw_unfs, raw_flds, unf_flds, fld_unfs, fld_injects), lthy') =
     1.9 +      fp_bnf construct bs eqs lthy;
    1.10  
    1.11 -    fun mk_fld_or_unf get_foldedT Ts t =
    1.12 +    fun mk_unf_or_fld get_foldedT Ts t =
    1.13        let val Type (_, Ts0) = get_foldedT (fastype_of t) in
    1.14          Term.subst_atomic_types (Ts0 ~~ Ts) t
    1.15        end;
    1.16  
    1.17 -    val mk_fld = mk_fld_or_unf range_type;
    1.18 -    val mk_unf = mk_fld_or_unf domain_type;
    1.19 +    val mk_unf = mk_unf_or_fld domain_type;
    1.20 +    val mk_fld = mk_unf_or_fld range_type;
    1.21  
    1.22 +    val unfs = map (mk_unf As) raw_unfs;
    1.23      val flds = map (mk_fld As) raw_flds;
    1.24 -    val unfs = map (mk_unf As) raw_unfs;
    1.25  
    1.26 -    fun wrap_type ((((((((T, fld), unf), fld_unf), unf_fld), ctr_names), ctr_Tss), disc_names),
    1.27 -        sel_namess) no_defs_lthy =
    1.28 +    fun wrap_type (((((((((T, fld), unf), fld_unf), unf_fld), fld_inject), ctr_names), ctr_Tss),
    1.29 +        disc_names), sel_namess) no_defs_lthy =
    1.30        let
    1.31          val n = length ctr_names;
    1.32          val ks = 1 upto n;
    1.33 @@ -178,11 +179,15 @@
    1.34          fun exhaust_tac {context = ctxt, ...} =
    1.35            mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm';
    1.36  
    1.37 -        (* ### *)
    1.38 +        val inject_tacss =
    1.39 +          map2 (fn 0 => K []
    1.40 +                 | _ => fn ctr_def => [fn {context = ctxt, ...} =>
    1.41 +                     mk_inject_tac ctxt ctr_def fld_inject])
    1.42 +            ms ctr_defs;
    1.43 +
    1.44 +        (*###*)
    1.45          fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
    1.46  
    1.47 -        val inject_tacss = map (fn 0 => [] | _ => [cheat_tac]) ms;
    1.48 -
    1.49          val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);
    1.50  
    1.51          val case_tacs = map (K cheat_tac) ks;
    1.52 @@ -193,8 +198,8 @@
    1.53        end;
    1.54    in
    1.55      lthy'
    1.56 -    |> fold wrap_type (Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ ctr_namess ~~ ctr_Tsss ~~
    1.57 -      disc_namess ~~ sel_namesss)
    1.58 +    |> fold wrap_type (Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ctr_namess ~~
    1.59 +      ctr_Tsss ~~ disc_namess ~~ sel_namesss)
    1.60    end;
    1.61  
    1.62  fun data_cmd info specs lthy =
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 15:51:32 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 16:17:22 2012 +0200
     2.3 @@ -10,6 +10,7 @@
     2.4    val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
     2.5    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     2.6      -> tactic
     2.7 +  val mk_inject_tac: Proof.context -> thm -> thm -> tactic
     2.8  end;
     2.9  
    2.10  structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
    2.11 @@ -33,4 +34,10 @@
    2.12       SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
    2.13       atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
    2.14  
    2.15 +fun mk_inject_tac ctxt ctr_def fld_inject =
    2.16 +  Local_Defs.unfold_tac ctxt [ctr_def] THEN
    2.17 +  rtac (fld_inject RS ssubst) 1 THEN
    2.18 +  Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN
    2.19 +  rtac refl 1;
    2.20 +
    2.21  end;
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 15:51:32 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 16:17:22 2012 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  signature BNF_GFP =
     3.5  sig
     3.6    val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
     3.7 -    (term list * term list * thm list * thm list) * local_theory
     3.8 +    (term list * term list * thm list * thm list * thm list) * local_theory
     3.9  end;
    3.10  
    3.11  structure BNF_GFP : BNF_GFP =
    3.12 @@ -2989,7 +2989,7 @@
    3.13              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    3.14            bs thmss)
    3.15    in
    3.16 -    ((flds, unfs, fld_unf_thms, unf_fld_thms),
    3.17 +    ((unfs, flds, unf_fld_thms, fld_unf_thms, fld_inject_thms),
    3.18        lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    3.19    end;
    3.20  
     4.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 15:51:32 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 16:17:22 2012 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  signature BNF_LFP =
     4.5  sig
     4.6    val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
     4.7 -    (term list * term list * thm list * thm list) * local_theory
     4.8 +    (term list * term list * thm list * thm list * thm list) * local_theory
     4.9  end;
    4.10  
    4.11  structure BNF_LFP : BNF_LFP =
    4.12 @@ -1812,7 +1812,7 @@
    4.13              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    4.14            bs thmss)
    4.15    in
    4.16 -    ((flds, unfs, fld_unf_thms, unf_fld_thms),
    4.17 +    ((unfs, flds, unf_fld_thms, fld_unf_thms, fld_inject_thms),
    4.18        lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    4.19    end;
    4.20