transfer rule for map (not yet registered as a transfer rule)
authortraytel
Mon Jul 22 21:12:15 2013 +0200 (2013-07-22)
changeset 52719480a3479fa47
parent 52718 0faf89b8d928
child 52720 fdc04f9bf906
transfer rule for map (not yet registered as a transfer rule)
src/HOL/BNF/BNF.thy
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
src/HOL/BNF/Tools/bnf_util.ML
     1.1 --- a/src/HOL/BNF/BNF.thy	Sun Jul 21 14:02:33 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF.thy	Mon Jul 22 21:12:15 2013 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  imports More_BNFs
     1.5  begin
     1.6  
     1.7 -hide_const (open) Gr Grp collect fsts snds setl setr 
     1.8 +hide_const (open) vimagep Gr Grp collect fsts snds setl setr 
     1.9    convol thePull pick_middlep fstOp sndOp csquare inver
    1.10    image2 relImage relInvImage prefCl PrefCl Succ Shift shift
    1.11  
     2.1 --- a/src/HOL/BNF/BNF_Def.thy	Sun Jul 21 14:02:33 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_Def.thy	Mon Jul 22 21:12:15 2013 +0200
     2.3 @@ -197,6 +197,21 @@
     2.4    ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
     2.5  unfolding Func_def by (auto elim: the_inv_into_f_f)
     2.6  
     2.7 +definition vimagep where
     2.8 +  "vimagep f g R = (\<lambda>x y. R (f x) (g y))"
     2.9 +
    2.10 +lemma vimagepI: "R (f x) (g y) \<Longrightarrow> vimagep f g R x y"
    2.11 +  unfolding vimagep_def by -
    2.12 +
    2.13 +lemma vimagepD: "vimagep f g R x y \<Longrightarrow> R (f x) (g y)"
    2.14 +  unfolding vimagep_def by -
    2.15 +
    2.16 +lemma fun_rel_iff_leq_vimagep: "(fun_rel R S) f g = (R \<le> vimagep f g S)"
    2.17 +  unfolding fun_rel_def vimagep_def by auto
    2.18 +
    2.19 +lemma convol_image_vimagep: "<f o fst, g o snd> ` Collect (split (vimagep f g R)) \<subseteq> Collect (split R)"
    2.20 +  unfolding vimagep_def convol_def by auto
    2.21 +
    2.22  ML_file "Tools/bnf_def_tactics.ML"
    2.23  ML_file "Tools/bnf_def.ML"
    2.24  
     3.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Sun Jul 21 14:02:33 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Jul 22 21:12:15 2013 +0200
     3.3 @@ -57,6 +57,7 @@
     3.4    val map_def_of_bnf: bnf -> thm
     3.5    val map_id'_of_bnf: bnf -> thm
     3.6    val map_id_of_bnf: bnf -> thm
     3.7 +  val map_transfer_of_bnf: bnf -> thm
     3.8    val map_wppull_of_bnf: bnf -> thm
     3.9    val map_wpull_of_bnf: bnf -> thm
    3.10    val rel_def_of_bnf: bnf -> thm
    3.11 @@ -185,6 +186,7 @@
    3.12    map_comp': thm lazy,
    3.13    map_cong: thm lazy,
    3.14    map_id': thm lazy,
    3.15 +  map_transfer: thm lazy,
    3.16    map_wppull: thm lazy,
    3.17    rel_eq: thm lazy,
    3.18    rel_flip: thm lazy,
    3.19 @@ -198,8 +200,8 @@
    3.20  };
    3.21  
    3.22  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
    3.23 -    map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map' rel_cong rel_mono rel_mono_strong
    3.24 -    rel_Grp rel_conversep rel_OO = {
    3.25 +    map_comp' map_cong map_id' map_transfer map_wppull rel_eq rel_flip set_map' rel_cong rel_mono
    3.26 +    rel_mono_strong rel_Grp rel_conversep rel_OO = {
    3.27    bd_Card_order = bd_Card_order,
    3.28    bd_Cinfinite = bd_Cinfinite,
    3.29    bd_Cnotzero = bd_Cnotzero,
    3.30 @@ -211,6 +213,7 @@
    3.31    map_comp' = map_comp',
    3.32    map_cong = map_cong,
    3.33    map_id' = map_id',
    3.34 +  map_transfer = map_transfer,
    3.35    map_wppull = map_wppull,
    3.36    rel_eq = rel_eq,
    3.37    rel_flip = rel_flip,
    3.38 @@ -234,6 +237,7 @@
    3.39    map_comp',
    3.40    map_cong,
    3.41    map_id',
    3.42 +  map_transfer,
    3.43    map_wppull,
    3.44    rel_eq,
    3.45    rel_flip,
    3.46 @@ -255,6 +259,7 @@
    3.47      map_comp' = Lazy.map f map_comp',
    3.48      map_cong = Lazy.map f map_cong,
    3.49      map_id' = Lazy.map f map_id',
    3.50 +    map_transfer = Lazy.map f map_transfer,
    3.51      map_wppull = Lazy.map f map_wppull,
    3.52      rel_eq = Lazy.map f rel_eq,
    3.53      rel_flip = Lazy.map f rel_flip,
    3.54 @@ -367,6 +372,7 @@
    3.55  val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
    3.56  val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
    3.57  val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
    3.58 +val map_transfer_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
    3.59  val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
    3.60  val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
    3.61  val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
    3.62 @@ -492,6 +498,7 @@
    3.63  val map_comp'N = "map_comp'";
    3.64  val map_cong0N = "map_cong0";
    3.65  val map_congN = "map_cong";
    3.66 +val map_transferN = "map_transfer";
    3.67  val map_wpullN = "map_wpull";
    3.68  val rel_eqN = "rel_eq";
    3.69  val rel_flipN = "rel_flip";
    3.70 @@ -665,11 +672,15 @@
    3.71      val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
    3.72      val pred2RT's = map2 mk_pred2T Bs' As';
    3.73      val self_pred2RTs = map2 mk_pred2T As' As';
    3.74 +    val transfer_domRTs = map2 mk_pred2T As' B1Ts;
    3.75 +    val transfer_ranRTs = map2 mk_pred2T Bs' B2Ts;
    3.76  
    3.77      val CA' = mk_bnf_T As' CA;
    3.78      val CB' = mk_bnf_T Bs' CA;
    3.79      val CC' = mk_bnf_T Cs CA;
    3.80      val CRs' = mk_bnf_T RTs CA;
    3.81 +    val CB1 = mk_bnf_T B1Ts CA;
    3.82 +    val CB2 = mk_bnf_T B2Ts CA;
    3.83  
    3.84      val bnf_map_AsAs = mk_bnf_map As' As';
    3.85      val bnf_map_AsBs = mk_bnf_map As' Bs';
    3.86 @@ -681,10 +692,11 @@
    3.87      val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
    3.88  
    3.89      val pre_names_lthy = lthy;
    3.90 -    val (((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), ys), As),
    3.91 +    val ((((((((((((((((((((((((((fs, f_transfers), gs), hs), x), y), (z, z')), zs), ys), As),
    3.92        As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
    3.93 -      names_lthy) = pre_names_lthy
    3.94 +      transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
    3.95        |> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
    3.96 +      ||>> mk_Frees "g" (map2 (curry (op -->)) B1Ts B2Ts)
    3.97        ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
    3.98        ||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
    3.99        ||>> yield_singleton (mk_Frees "x") CA'
   3.100 @@ -706,7 +718,9 @@
   3.101        ||>> mk_Frees "b" As'
   3.102        ||>> mk_Frees' "R" pred2RTs
   3.103        ||>> mk_Frees "R" pred2RTs
   3.104 -      ||>> mk_Frees "S" pred2RTsBsCs;
   3.105 +      ||>> mk_Frees "S" pred2RTsBsCs
   3.106 +      ||>> mk_Frees "R" transfer_domRTs
   3.107 +      ||>> mk_Frees "S" transfer_ranRTs;
   3.108  
   3.109      val fs_copy = map2 (retype_free o fastype_of) fs gs;
   3.110      val x_copy = retype_free CA' y;
   3.111 @@ -746,6 +760,7 @@
   3.112      fun mk_bnf_rel RTs CA' CB' = normalize_rel lthy RTs CA' CB' bnf_rel;
   3.113  
   3.114      val rel = mk_bnf_rel pred2RTs CA' CB';
   3.115 +    val relAsAs = mk_bnf_rel self_pred2RTs CA' CA';
   3.116  
   3.117      val _ = case no_reflexive (raw_map_def :: raw_set_defs @ [raw_bd_def] @
   3.118          raw_wit_defs @ [raw_rel_def]) of
   3.119 @@ -812,8 +827,6 @@
   3.120          val prems = map HOLogic.mk_Trueprop
   3.121            (map8 mk_wpull Xs B1s B2s f1s f2s (replicate live NONE) p1s p2s);
   3.122          val CX = mk_bnf_T domTs CA;
   3.123 -        val CB1 = mk_bnf_T B1Ts CA;
   3.124 -        val CB2 = mk_bnf_T B2Ts CA;
   3.125          val bnf_sets_CX = map2 (normalize_set (map (mk_bnf_T domTs) CA_params)) domTs bnf_sets;
   3.126          val bnf_sets_CB1 = map2 (normalize_set (map (mk_bnf_T B1Ts) CA_params)) B1Ts bnf_sets;
   3.127          val bnf_sets_CB2 = map2 (normalize_set (map (mk_bnf_T B2Ts) CA_params)) B2Ts bnf_sets;
   3.128 @@ -956,8 +969,6 @@
   3.129                [HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   3.130                  (map8 mk_wpull Xs B1s B2s f1s f2s (map SOME (e1s ~~ e2s)) p1s p2s))];
   3.131              val CX = mk_bnf_T domTs CA;
   3.132 -            val CB1 = mk_bnf_T B1Ts CA;
   3.133 -            val CB2 = mk_bnf_T B2Ts CA;
   3.134              val bnf_sets_CX =
   3.135                map2 (normalize_set (map (mk_bnf_T domTs) CA_params)) domTs bnf_sets;
   3.136              val bnf_sets_CB1 =
   3.137 @@ -1034,13 +1045,11 @@
   3.138          val rel_cong = Lazy.lazy mk_rel_cong;
   3.139  
   3.140          fun mk_rel_eq () =
   3.141 -          let val relAsAs = mk_bnf_rel self_pred2RTs CA' CA' in
   3.142 -            Goal.prove_sorry lthy [] []
   3.143 -              (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
   3.144 -                HOLogic.eq_const CA'))
   3.145 -              (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms)))
   3.146 -            |> Thm.close_derivation
   3.147 -          end;
   3.148 +          Goal.prove_sorry lthy [] []
   3.149 +            (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
   3.150 +              HOLogic.eq_const CA'))
   3.151 +            (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms)))
   3.152 +          |> Thm.close_derivation;
   3.153  
   3.154          val rel_eq = Lazy.lazy mk_rel_eq;
   3.155  
   3.156 @@ -1130,10 +1139,30 @@
   3.157  
   3.158          val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
   3.159  
   3.160 +        fun mk_map_transfer () =
   3.161 +          let
   3.162 +            fun mk_prem R S f g = HOLogic.mk_Trueprop (mk_fun_rel R S $ f $ g);
   3.163 +            val prems = map4 mk_prem transfer_domRs transfer_ranRs fs f_transfers;
   3.164 +            val relA = Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs);
   3.165 +            val relB = Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs);
   3.166 +            val mapf = Term.list_comb (bnf_map_AsBs, fs);
   3.167 +            val mapg = Term.list_comb (mk_bnf_map B1Ts B2Ts, f_transfers);
   3.168 +            val concl = HOLogic.mk_Trueprop (mk_fun_rel relA relB $ mapf $ mapg);
   3.169 +          in
   3.170 +            Goal.prove_sorry lthy [] []
   3.171 +              (fold_rev Logic.all (fs @ f_transfers @ transfer_domRs @ transfer_ranRs)
   3.172 +                (Logic.list_implies (prems, concl)))
   3.173 +              (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel)
   3.174 +                (map Lazy.force set_map') (#map_cong0 axioms) (Lazy.force map_comp'))
   3.175 +            |> Thm.close_derivation
   3.176 +          end;
   3.177 +
   3.178 +        val map_transfer = Lazy.lazy mk_map_transfer;
   3.179 +
   3.180          val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
   3.181  
   3.182          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
   3.183 -          in_mono in_rel map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map'
   3.184 +          in_mono in_rel map_comp' map_cong map_id' map_transfer map_wppull rel_eq rel_flip set_map'
   3.185            rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
   3.186  
   3.187          val wits = map2 mk_witness bnf_wits wit_thms;
   3.188 @@ -1160,6 +1189,7 @@
   3.189                      (in_relN, [Lazy.force (#in_rel facts)]),
   3.190                      (map_compN, [#map_comp axioms]),
   3.191                      (map_idN, [#map_id axioms]),
   3.192 +                    (map_transferN, [Lazy.force (#map_transfer facts)]),
   3.193                      (map_wpullN, [#map_wpull axioms]),
   3.194                      (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
   3.195                      (set_mapN, #set_map axioms),
     4.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sun Jul 21 14:02:33 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Mon Jul 22 21:12:15 2013 +0200
     4.3 @@ -28,6 +28,9 @@
     4.4    val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
     4.5    val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
     4.6  
     4.7 +  val mk_map_transfer_tac: thm -> thm -> thm list -> thm -> thm ->
     4.8 +    {prems: thm list, context: Proof.context} -> tactic
     4.9 +
    4.10    val mk_in_bd_tac: int -> thm -> thm -> thm -> thm list -> thm list -> thm -> thm -> thm -> thm ->
    4.11      {prems: 'a, context: Proof.context} -> tactic
    4.12  end;
    4.13 @@ -208,6 +211,25 @@
    4.14      EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
    4.15        CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
    4.16  
    4.17 +fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp'
    4.18 +  {context = ctxt, prems = _} =
    4.19 +  let
    4.20 +    val n = length set_map's;
    4.21 +  in
    4.22 +    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimagep} THEN
    4.23 +    HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
    4.24 +      rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
    4.25 +      REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
    4.26 +      rtac @{thm vimagepI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    4.27 +      CONJ_WRAP' (fn thm =>
    4.28 +        etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimagep]]}))
    4.29 +      set_map's,
    4.30 +      rtac conjI,
    4.31 +      EVERY' (map (fn convol =>
    4.32 +        rtac (box_equals OF [map_cong0, map_comp' RS sym, map_comp' RS sym]) THEN'
    4.33 +        REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
    4.34 +  end;
    4.35 +
    4.36  fun mk_in_bd_tac live map_comp' map_id' map_cong0 set_map's set_bds
    4.37    bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} =
    4.38    if live = 0 then
     5.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Sun Jul 21 14:02:33 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Mon Jul 22 21:12:15 2013 +0200
     5.3 @@ -107,6 +107,7 @@
     5.4    val mk_cprod: term -> term -> term
     5.5    val mk_csum: term -> term -> term
     5.6    val mk_dir_image: term -> term -> term
     5.7 +  val mk_fun_rel: term -> term -> term
     5.8    val mk_image: term -> term
     5.9    val mk_in: term list -> term list -> typ -> term
    5.10    val mk_leq: term -> term -> term
    5.11 @@ -512,6 +513,12 @@
    5.12    let val (T, U) = dest_funT (fastype_of f);
    5.13    in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end;
    5.14  
    5.15 +fun mk_fun_rel R S =
    5.16 +  let
    5.17 +    val ((RA, RB), RT) = `dest_pred2T (fastype_of R);
    5.18 +    val ((SA, SB), ST) = `dest_pred2T (fastype_of S);
    5.19 +  in Const (@{const_name fun_rel}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
    5.20 +
    5.21  (*FIXME: "x"?*)
    5.22  (*(nth sets i) must be of type "T --> 'ai set"*)
    5.23  fun mk_in As sets T =