generate 'inj_map_strong' for BNFs
authordesharna
Mon Aug 18 14:09:09 2014 +0200 (2014-08-18)
changeset 57970eaa986cd285a
parent 57969 1e7b9579b14f
child 57971 07e81758788d
generate 'inj_map_strong' for BNFs
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:49:47 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 14:09:09 2014 +0200
     1.3 @@ -55,6 +55,7 @@
     1.4    val in_mono_of_bnf: bnf -> thm
     1.5    val in_rel_of_bnf: bnf -> thm
     1.6    val inj_map_of_bnf: bnf -> thm
     1.7 +  val inj_map_strong_of_bnf: bnf -> thm
     1.8    val map_comp0_of_bnf: bnf -> thm
     1.9    val map_comp_of_bnf: bnf -> thm
    1.10    val map_cong0_of_bnf: bnf -> thm
    1.11 @@ -223,6 +224,7 @@
    1.12    in_mono: thm lazy,
    1.13    in_rel: thm lazy,
    1.14    inj_map: thm lazy,
    1.15 +  inj_map_strong: thm lazy,
    1.16    map_comp: thm lazy,
    1.17    map_cong: thm lazy,
    1.18    map_id: thm lazy,
    1.19 @@ -243,8 +245,9 @@
    1.20  };
    1.21  
    1.22  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
    1.23 -    inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
    1.24 -    rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp rel_conversep rel_OO = {
    1.25 +    inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
    1.26 +    rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp
    1.27 +    rel_conversep rel_OO = {
    1.28    bd_Card_order = bd_Card_order,
    1.29    bd_Cinfinite = bd_Cinfinite,
    1.30    bd_Cnotzero = bd_Cnotzero,
    1.31 @@ -254,6 +257,7 @@
    1.32    in_mono = in_mono,
    1.33    in_rel = in_rel,
    1.34    inj_map = inj_map,
    1.35 +  inj_map_strong = inj_map_strong,
    1.36    map_comp = map_comp,
    1.37    map_cong = map_cong,
    1.38    map_id = map_id,
    1.39 @@ -282,6 +286,7 @@
    1.40    in_mono,
    1.41    in_rel,
    1.42    inj_map,
    1.43 +  inj_map_strong,
    1.44    map_comp,
    1.45    map_cong,
    1.46    map_id,
    1.47 @@ -308,6 +313,7 @@
    1.48      in_mono = Lazy.map f in_mono,
    1.49      in_rel = Lazy.map f in_rel,
    1.50      inj_map = Lazy.map f inj_map,
    1.51 +    inj_map_strong = Lazy.map f inj_map_strong,
    1.52      map_comp = Lazy.map f map_comp,
    1.53      map_cong = Lazy.map f map_cong,
    1.54      map_id = Lazy.map f map_id,
    1.55 @@ -430,6 +436,7 @@
    1.56  val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
    1.57  val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
    1.58  val inj_map_of_bnf = Lazy.force o #inj_map o #facts o rep_bnf;
    1.59 +val inj_map_strong_of_bnf = Lazy.force o #inj_map_strong o #facts o rep_bnf;
    1.60  val map_def_of_bnf = #map_def o #defs o rep_bnf;
    1.61  val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
    1.62  val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
    1.63 @@ -604,6 +611,7 @@
    1.64  val in_monoN = "in_mono";
    1.65  val in_relN = "in_rel";
    1.66  val inj_mapN = "inj_map";
    1.67 +val inj_map_strongN = "inj_map_strong";
    1.68  val map_id0N = "map_id0";
    1.69  val map_idN = "map_id";
    1.70  val map_identN = "map_ident";
    1.71 @@ -677,6 +685,7 @@
    1.72        let
    1.73          val notes =
    1.74            [(inj_mapN, [Lazy.force (#inj_map facts)], []),
    1.75 +           (inj_map_strongN, [Lazy.force (#inj_map_strong facts)], []),
    1.76             (map_compN, [Lazy.force (#map_comp facts)], []),
    1.77             (map_cong0N, [#map_cong0 axioms], []),
    1.78             (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
    1.79 @@ -956,16 +965,19 @@
    1.80      fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
    1.81  
    1.82      val pre_names_lthy = lthy;
    1.83 -    val ((((((((((((((((((fs, gs), hs), is), x), y), zs), ys), As),
    1.84 +    val (((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), zs), zs'), ys), As),
    1.85        As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs),
    1.86        transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
    1.87        |> mk_Frees "f" (map2 (curry op -->) As' Bs')
    1.88 +      ||>> mk_Frees "f" (map2 (curry op -->) As' Bs')
    1.89        ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
    1.90        ||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
    1.91        ||>> mk_Frees "i" (map2 (curry op -->) As' Cs)
    1.92        ||>> yield_singleton (mk_Frees "x") CA'
    1.93 +      ||>> yield_singleton (mk_Frees "x") CA'
    1.94        ||>> yield_singleton (mk_Frees "y") CB'
    1.95        ||>> mk_Frees "z" As'
    1.96 +      ||>> mk_Frees "z" As'
    1.97        ||>> mk_Frees "y" Bs'
    1.98        ||>> mk_Frees "A" (map HOLogic.mk_setT As')
    1.99        ||>> mk_Frees "A" (map HOLogic.mk_setT As')
   1.100 @@ -1346,12 +1358,13 @@
   1.101                   mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y];
   1.102              val goals = map2 mk_goal lhss rhss;
   1.103            in
   1.104 -            Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   1.105 +            goals
   1.106 +            |> map (fn goal => Goal.prove_sorry lthy [] [] goal
   1.107                (fn {context = ctxt, prems = _} =>
   1.108                   mk_rel_map0_tac ctxt live (Lazy.force rel_OO) (Lazy.force rel_conversep)
   1.109 -                  (Lazy.force rel_Grp) (Lazy.force map_id))
   1.110 -            |> Conjunction.elim_balanced (length goals)
   1.111 -            |> map (unfold_thms lthy @{thms vimage2p_def id_apply})
   1.112 +                  (Lazy.force rel_Grp) (Lazy.force map_id)))
   1.113 +            |> map (unfold_thms lthy @{thms vimage2p_def[of id, unfolded id_apply]
   1.114 +                 vimage2p_def[of _ id, unfolded id_apply]})
   1.115              |> map Thm.close_derivation
   1.116            end;
   1.117  
   1.118 @@ -1376,12 +1389,36 @@
   1.119  
   1.120          val map_transfer = Lazy.lazy mk_map_transfer;
   1.121  
   1.122 +        fun mk_inj_map_strong () =
   1.123 +          let
   1.124 +            val assms = map5 (fn setA => fn z => fn f => fn z' => fn f' =>
   1.125 +              fold_rev Logic.all [z, z']
   1.126 +                (Logic.mk_implies (mk_Trueprop_mem (z, setA $ x),
   1.127 +                   Logic.mk_implies (mk_Trueprop_mem (z', setA $ x'),
   1.128 +                     Logic.mk_implies (mk_Trueprop_eq (f $ z, f' $ z'),
   1.129 +                       mk_Trueprop_eq (z, z')))))) bnf_sets_As zs fs zs' fs';
   1.130 +            val concl = Logic.mk_implies
   1.131 +              (mk_Trueprop_eq
   1.132 +                 (Term.list_comb (bnf_map_AsBs, fs) $ x,
   1.133 +                  Term.list_comb (bnf_map_AsBs, fs') $ x'),
   1.134 +               mk_Trueprop_eq (x, x'));
   1.135 +            val goal = fold_rev Logic.all (x :: x' :: fs @ fs')
   1.136 +              (fold_rev (curry Logic.mk_implies) assms concl);
   1.137 +          in
   1.138 +            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
   1.139 +              mk_inj_map_strong_tac ctxt (Lazy.force rel_eq) (Lazy.force rel_map)
   1.140 +                (Lazy.force rel_mono_strong))
   1.141 +            |> Thm.close_derivation
   1.142 +          end;
   1.143 +
   1.144 +        val inj_map_strong = Lazy.lazy mk_inj_map_strong;
   1.145 +
   1.146          val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
   1.147  
   1.148          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
   1.149 -          in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
   1.150 -          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp
   1.151 -          rel_conversep rel_OO;
   1.152 +          in_mono in_rel inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident
   1.153 +          map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
   1.154 +          rel_mono_strong rel_Grp rel_conversep rel_OO;
   1.155  
   1.156          val wits = map2 mk_witness bnf_wits wit_thms;
   1.157  
     2.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Aug 18 13:49:47 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Aug 18 14:09:09 2014 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  sig
     2.5    val mk_collect_set_map_tac: thm list -> tactic
     2.6    val mk_in_mono_tac: int -> tactic
     2.7 +  val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic
     2.8    val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic
     2.9    val mk_map_id: thm -> thm
    2.10    val mk_map_ident: Proof.context -> thm -> thm
    2.11 @@ -70,6 +71,17 @@
    2.12          REPEAT_DETERM_N n o atac))
    2.13    end;
    2.14  
    2.15 +fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
    2.16 +  let
    2.17 +    val rel_eq' = rel_eq RS @{thm predicate2_eqD};
    2.18 +    val rel_maps' = map (fn thm => thm RS iffD1) rel_maps;
    2.19 +  in
    2.20 +    HEADGOAL (dtac (rel_eq' RS iffD2) THEN' rtac (rel_eq' RS iffD1)) THEN
    2.21 +    EVERY (map (HEADGOAL o dtac) rel_maps') THEN
    2.22 +    HEADGOAL (etac rel_mono_strong) THEN
    2.23 +    TRYALL (Goal.assume_rule_tac ctxt)
    2.24 +  end;
    2.25 +
    2.26  fun mk_collect_set_map_tac set_map0s =
    2.27    (rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
    2.28    EVERY' (map (fn set_map0 =>
    2.29 @@ -197,7 +209,7 @@
    2.30          REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
    2.31          in_tac @{thm fstOp_in},
    2.32          rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
    2.33 -        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, 
    2.34 +        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply,
    2.35            rtac ballE, rtac subst,
    2.36            rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
    2.37            etac set_mp, atac],
    2.38 @@ -252,10 +264,10 @@
    2.39      let
    2.40        val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1};
    2.41        val inserts =
    2.42 -        map (fn set_bd => 
    2.43 +        map (fn set_bd =>
    2.44            iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF
    2.45              [set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]])
    2.46 -        set_bds;        
    2.47 +        set_bds;
    2.48      in
    2.49        EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm cprod_cinfinite_bound},
    2.50          rtac (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac @{thm card_of_Card_order},