generate 'rel_map' theorem for BNFs
authordesharna
Thu Aug 14 13:20:54 2014 +0200 (2014-08-14)
changeset 57932c29659f77f8d
parent 57931 4e2cbff02f23
child 57933 f620851148a9
generate 'rel_map' theorem for BNFs
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Aug 13 22:29:43 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Aug 14 13:20:54 2014 +0200
     1.3 @@ -232,6 +232,7 @@
     1.4    rel_flip: thm lazy,
     1.5    set_map: thm lazy list,
     1.6    rel_cong: thm lazy,
     1.7 +  rel_map: thm list lazy,
     1.8    rel_mono: thm lazy,
     1.9    rel_mono_strong: thm lazy,
    1.10    rel_Grp: thm lazy,
    1.11 @@ -241,7 +242,7 @@
    1.12  
    1.13  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
    1.14      inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
    1.15 -    rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
    1.16 +    rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
    1.17    bd_Card_order = bd_Card_order,
    1.18    bd_Cinfinite = bd_Cinfinite,
    1.19    bd_Cnotzero = bd_Cnotzero,
    1.20 @@ -261,6 +262,7 @@
    1.21    rel_flip = rel_flip,
    1.22    set_map = set_map,
    1.23    rel_cong = rel_cong,
    1.24 +  rel_map = rel_map,
    1.25    rel_mono = rel_mono,
    1.26    rel_mono_strong = rel_mono_strong,
    1.27    rel_Grp = rel_Grp,
    1.28 @@ -287,6 +289,7 @@
    1.29    rel_flip,
    1.30    set_map,
    1.31    rel_cong,
    1.32 +  rel_map,
    1.33    rel_mono,
    1.34    rel_mono_strong,
    1.35    rel_Grp,
    1.36 @@ -311,6 +314,7 @@
    1.37      rel_flip = Lazy.map f rel_flip,
    1.38      set_map = map (Lazy.map f) set_map,
    1.39      rel_cong = Lazy.map f rel_cong,
    1.40 +    rel_map = Lazy.map (map f) rel_map,
    1.41      rel_mono = Lazy.map f rel_mono,
    1.42      rel_mono_strong = Lazy.map f rel_mono_strong,
    1.43      rel_Grp = Lazy.map f rel_Grp,
    1.44 @@ -609,6 +613,7 @@
    1.45  val set_bdN = "set_bd";
    1.46  val rel_GrpN = "rel_Grp";
    1.47  val rel_conversepN = "rel_conversep";
    1.48 +val rel_mapN = "rel_map"
    1.49  val rel_monoN = "rel_mono"
    1.50  val rel_mono_strongN = "rel_mono_strong"
    1.51  val rel_comppN = "rel_compp";
    1.52 @@ -676,6 +681,7 @@
    1.53             (rel_eqN, [Lazy.force (#rel_eq facts)], []),
    1.54             (rel_flipN, [Lazy.force (#rel_flip facts)], []),
    1.55             (rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
    1.56 +           (rel_mapN, Lazy.force (#rel_map facts), []),
    1.57             (rel_monoN, [Lazy.force (#rel_mono facts)], []),
    1.58             (set_mapN, map Lazy.force (#set_map facts), [])]
    1.59            |> filter_out (null o #2)
    1.60 @@ -920,6 +926,7 @@
    1.61      val pred2RTs = map2 mk_pred2T As' Bs';
    1.62      val pred2RTsAsCs = map2 mk_pred2T As' Cs;
    1.63      val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
    1.64 +    val pred2RTsCsBs = map2 mk_pred2T Cs Bs';
    1.65      val pred2RT's = map2 mk_pred2T Bs' As';
    1.66      val self_pred2RTs = map2 mk_pred2T As' As';
    1.67      val transfer_domRTs = map2 mk_pred2T As' B1Ts;
    1.68 @@ -941,12 +948,13 @@
    1.69      fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
    1.70  
    1.71      val pre_names_lthy = lthy;
    1.72 -    val (((((((((((((((fs, gs), hs), x), y), zs), ys), As),
    1.73 -      As_copy), bs), Rs), Rs_copy), Ss),
    1.74 +    val ((((((((((((((((((fs, gs), hs), is), x), y), zs), ys), As),
    1.75 +      As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs),
    1.76        transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
    1.77        |> mk_Frees "f" (map2 (curry op -->) As' Bs')
    1.78        ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
    1.79        ||>> mk_Frees "h" (map2 (curry op -->) As' Ts)
    1.80 +      ||>> mk_Frees "i" (map2 (curry op -->) As' Cs)
    1.81        ||>> yield_singleton (mk_Frees "x") CA'
    1.82        ||>> yield_singleton (mk_Frees "y") CB'
    1.83        ||>> mk_Frees "z" As'
    1.84 @@ -957,6 +965,8 @@
    1.85        ||>> mk_Frees "R" pred2RTs
    1.86        ||>> mk_Frees "R" pred2RTs
    1.87        ||>> mk_Frees "S" pred2RTsBsCs
    1.88 +      ||>> mk_Frees "S" pred2RTsAsCs
    1.89 +      ||>> mk_Frees "S" pred2RTsCsBs
    1.90        ||>> mk_Frees "R" transfer_domRTs
    1.91        ||>> mk_Frees "S" transfer_ranRTs;
    1.92  
    1.93 @@ -1022,6 +1032,7 @@
    1.94  
    1.95      val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
    1.96      val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
    1.97 +    val relCsBs = mk_bnf_rel pred2RTsCsBs CC' CB';
    1.98      val rel_OO_lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
    1.99      val rel_OO_rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
   1.100      val le_rel_OO_goal =
   1.101 @@ -1308,6 +1319,32 @@
   1.102  
   1.103          val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
   1.104  
   1.105 +        fun mk_rel_map () =
   1.106 +          let
   1.107 +            fun mk_goal lhs rhs =
   1.108 +              fold_rev Logic.all ([x, y] @ S_CsBs @ S_AsCs @ is @ gs) (mk_Trueprop_eq (lhs, rhs));
   1.109 +
   1.110 +            val lhss =
   1.111 +              [Term.list_comb (relCsBs, S_CsBs) $ (Term.list_comb (bnf_map_AsCs, is) $ x) $ y,
   1.112 +               Term.list_comb (relAsCs, S_AsCs) $ x $ (Term.list_comb (bnf_map_BsCs, gs) $ y)];
   1.113 +            val rhss =
   1.114 +              [Term.list_comb (rel, map3 (fn f => fn P => fn T =>
   1.115 +                 mk_vimage2p f (HOLogic.id_const T) $ P) is S_CsBs Bs') $ x $ y,
   1.116 +               Term.list_comb (rel, map3 (fn f => fn P => fn T =>
   1.117 +                 mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y];
   1.118 +            val goals = map2 mk_goal lhss rhss;
   1.119 +          in
   1.120 +            Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   1.121 +              (fn {context = ctxt, prems = _} =>
   1.122 +                 mk_rel_map0_tac ctxt live (Lazy.force rel_OO) (Lazy.force rel_conversep)
   1.123 +                  (Lazy.force rel_Grp) (Lazy.force map_id))
   1.124 +            |> Conjunction.elim_balanced (length goals)
   1.125 +            |> map (unfold_thms lthy @{thms vimage2p_def id_apply})
   1.126 +            |> map Thm.close_derivation
   1.127 +          end;
   1.128 +
   1.129 +        val rel_map = Lazy.lazy mk_rel_map;
   1.130 +
   1.131          fun mk_map_transfer () =
   1.132            let
   1.133              val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
   1.134 @@ -1331,7 +1368,7 @@
   1.135  
   1.136          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
   1.137            in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
   1.138 -          rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
   1.139 +          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
   1.140  
   1.141          val wits = map2 mk_witness bnf_wits wit_thms;
   1.142  
     2.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Wed Aug 13 22:29:43 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Aug 14 13:20:54 2014 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4    val mk_rel_OO_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
     2.5    val mk_rel_conversep_tac: thm -> thm -> tactic
     2.6    val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
     2.7 +  val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
     2.8    val mk_rel_mono_tac: thm list -> thm -> tactic
     2.9    val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
    2.10  
    2.11 @@ -118,6 +119,26 @@
    2.12      rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI,
    2.13      CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id0])) 1;
    2.14  
    2.15 +fun mk_rel_map0_tac ctxt live rel_compp rel_conversep rel_Grp map_id =
    2.16 +  if live = 0 then
    2.17 +    HEADGOAL (Goal.conjunction_tac) THEN
    2.18 +    unfold_thms_tac ctxt @{thms id_apply} THEN
    2.19 +    ALLGOALS (rtac refl)
    2.20 +  else
    2.21 +    let
    2.22 +      val ks = 1 upto live;
    2.23 +    in
    2.24 +      Goal.conjunction_tac 1 THEN
    2.25 +      unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
    2.26 +      TRYALL (EVERY' [rtac iffI, rtac @{thm relcomppI}, rtac @{thm GrpI},
    2.27 +        resolve_tac [map_id, refl], rtac CollectI,
    2.28 +        CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, rtac @{thm relcomppI}, atac,
    2.29 +        rtac @{thm conversepI}, rtac @{thm GrpI}, resolve_tac [map_id, refl], rtac CollectI,
    2.30 +        CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks,
    2.31 +        REPEAT_DETERM o eresolve_tac @{thms relcomppE conversepE GrpE},
    2.32 +        dtac (trans OF [sym, map_id]), hyp_subst_tac ctxt, atac])
    2.33 +    end;
    2.34 +
    2.35  fun mk_rel_mono_tac rel_OO_Grps in_mono =
    2.36    let
    2.37      val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Aug 13 22:29:43 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Aug 14 13:20:54 2014 +0200
     3.3 @@ -471,7 +471,7 @@
     3.4    #>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop))
     3.5    ##> (fn thm => Thm.permute_prems 0 (~nn)
     3.6      (if nn = 1 then thm RS prop
     3.7 -     else funpow nn (fn thm => Local_Defs.unfold lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
     3.8 +     else funpow nn (fn thm => unfold_thms lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
     3.9  
    3.10  fun mk_induct_attrs ctrss =
    3.11    let
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Aug 13 22:29:43 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Aug 14 13:20:54 2014 +0200
     4.3 @@ -1592,7 +1592,7 @@
     4.4      val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
     4.5        `split_conj_thm (split_conj_prems n
     4.6          (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
     4.7 -        |> Local_Defs.unfold lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
     4.8 +        |> unfold_thms lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric]
     4.9             case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
    4.10          OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]});
    4.11  
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Aug 13 22:29:43 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Aug 14 13:20:54 2014 +0200
     5.3 @@ -1197,7 +1197,7 @@
     5.4      val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
     5.5        `split_conj_thm (split_conj_prems n
     5.6          (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
     5.7 -        |> Local_Defs.unfold lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @
     5.8 +        |> unfold_thms lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @
     5.9             map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
    5.10  
    5.11      val timer = time (timer "rec definitions & thms");