generate "rel_as_srel" and "rel_flip" properties
authorblanchet
Sun Sep 23 14:52:53 2012 +0200 (2012-09-23)
changeset 49537fe1deee434b6
parent 49536 898aea2e7a94
child 49538 c90818b63599
generate "rel_as_srel" and "rel_flip" properties
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/Tools/bnf_def.ML
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Sun Sep 23 14:52:53 2012 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -145,7 +145,20 @@
     1.4  lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
     1.5  unfolding o_def fun_eq_iff by simp
     1.6  
     1.7 +lemma eqset_imp_iff_pair: "A = B \<Longrightarrow> (a, b) \<in> A \<longleftrightarrow> (a, b) \<in> B"
     1.8 +by (rule eqset_imp_iff)
     1.9 +
    1.10 +lemma fun_cong_pair: "f = g \<Longrightarrow> f {(a, b). R a b} = g {(a, b). R a b}"
    1.11 +by (rule fun_cong)
    1.12 +
    1.13 +lemma flip_as_converse: "{(a, b). R b a} = converse {(a, b). R a b}"
    1.14 +unfolding converse_def mem_Collect_eq prod.cases
    1.15 +apply (rule arg_cong[of _ _ "\<lambda>x. Collect (prod_case x)"])
    1.16 +apply (rule ext)+
    1.17 +apply (unfold conversep_iff)
    1.18 +by (rule refl)
    1.19 +
    1.20  ML_file "Tools/bnf_def_tactics.ML"
    1.21 -ML_file"Tools/bnf_def.ML"
    1.22 +ML_file "Tools/bnf_def.ML"
    1.23  
    1.24  end
     2.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Sun Sep 23 14:52:53 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Sun Sep 23 14:52:53 2012 +0200
     2.3 @@ -56,7 +56,9 @@
     2.4    val map_id_of_bnf: BNF -> thm
     2.5    val map_wppull_of_bnf: BNF -> thm
     2.6    val map_wpull_of_bnf: BNF -> thm
     2.7 +  val rel_as_srel_of_bnf: BNF -> thm
     2.8    val rel_def_of_bnf: BNF -> thm
     2.9 +  val rel_flip_of_bnf: BNF -> thm
    2.10    val set_bd_of_bnf: BNF -> thm list
    2.11    val set_defs_of_bnf: BNF -> thm list
    2.12    val set_natural'_of_bnf: BNF -> thm list
    2.13 @@ -182,6 +184,8 @@
    2.14    map_comp': thm lazy,
    2.15    map_id': thm lazy,
    2.16    map_wppull: thm lazy,
    2.17 +  rel_as_srel: thm lazy,
    2.18 +  rel_flip: thm lazy,
    2.19    set_natural': thm lazy list,
    2.20    srel_cong: thm lazy,
    2.21    srel_mono: thm lazy,
    2.22 @@ -192,8 +196,8 @@
    2.23  };
    2.24  
    2.25  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel
    2.26 -    map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id srel_Gr srel_converse
    2.27 -    srel_O = {
    2.28 +    map_comp' map_id' map_wppull rel_as_srel rel_flip set_natural' srel_cong srel_mono srel_Id
    2.29 +    srel_Gr srel_converse srel_O = {
    2.30    bd_Card_order = bd_Card_order,
    2.31    bd_Cinfinite = bd_Cinfinite,
    2.32    bd_Cnotzero = bd_Cnotzero,
    2.33 @@ -204,6 +208,8 @@
    2.34    map_comp' = map_comp',
    2.35    map_id' = map_id',
    2.36    map_wppull = map_wppull,
    2.37 +  rel_as_srel = rel_as_srel,
    2.38 +  rel_flip = rel_flip,
    2.39    set_natural' = set_natural',
    2.40    srel_cong = srel_cong,
    2.41    srel_mono = srel_mono,
    2.42 @@ -223,6 +229,8 @@
    2.43    map_comp',
    2.44    map_id',
    2.45    map_wppull,
    2.46 +  rel_as_srel,
    2.47 +  rel_flip,
    2.48    set_natural',
    2.49    srel_cong,
    2.50    srel_mono,
    2.51 @@ -240,6 +248,8 @@
    2.52      map_comp' = Lazy.map f map_comp',
    2.53      map_id' = Lazy.map f map_id',
    2.54      map_wppull = Lazy.map f map_wppull,
    2.55 +    rel_as_srel = Lazy.map f rel_as_srel,
    2.56 +    rel_flip = Lazy.map f rel_flip,
    2.57      set_natural' = map (Lazy.map f) set_natural',
    2.58      srel_cong = Lazy.map f srel_cong,
    2.59      srel_mono = Lazy.map f srel_mono,
    2.60 @@ -358,7 +368,9 @@
    2.61  val map_cong_of_bnf = #map_cong o #axioms o rep_bnf;
    2.62  val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
    2.63  val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
    2.64 +val rel_as_srel_of_bnf = Lazy.force o #rel_as_srel o #facts o rep_bnf;
    2.65  val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
    2.66 +val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
    2.67  val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
    2.68  val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
    2.69  val set_natural_of_bnf = #set_natural o #axioms o rep_bnf;
    2.70 @@ -490,15 +502,17 @@
    2.71  val map_comp'N = "map_comp'";
    2.72  val map_congN = "map_cong";
    2.73  val map_wpullN = "map_wpull";
    2.74 +val rel_as_srelN = "rel_as_srel";
    2.75 +val rel_flipN = "rel_flip";
    2.76 +val set_naturalN = "set_natural";
    2.77 +val set_natural'N = "set_natural'";
    2.78 +val set_bdN = "set_bd";
    2.79  val srel_IdN = "srel_Id";
    2.80  val srel_GrN = "srel_Gr";
    2.81  val srel_converseN = "srel_converse";
    2.82  val srel_monoN = "srel_mono"
    2.83  val srel_ON = "srel_comp";
    2.84  val srel_O_GrN = "srel_comp_Gr";
    2.85 -val set_naturalN = "set_natural";
    2.86 -val set_natural'N = "set_natural'";
    2.87 -val set_bdN = "set_bd";
    2.88  
    2.89  datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
    2.90  
    2.91 @@ -695,7 +709,7 @@
    2.92        ||>> mk_Frees' "S" setRTs
    2.93        ||>> mk_Frees "S" setRTs
    2.94        ||>> mk_Frees "T" setRTsBsCs
    2.95 -      ||>> mk_Frees' "Q" QTs;
    2.96 +      ||>> mk_Frees' "R" QTs;
    2.97  
    2.98      (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
    2.99      val O_Gr =
   2.100 @@ -714,11 +728,14 @@
   2.101          val y = Free (y_name, U);
   2.102        in fold_rev Term.lambda [x, y] (HOLogic.mk_mem (HOLogic.mk_prod (x, y), t)) end;
   2.103  
   2.104 +    val sQs =
   2.105 +      map3 (fn Q => fn T => fn U =>
   2.106 +          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs';
   2.107 +
   2.108      val rel_rhs = (case raw_rel_opt of
   2.109          NONE =>
   2.110          fold_rev absfree Qs' (mk_predicate_of_set (fst x') (fst y')
   2.111 -          (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, map3 (fn Q => fn T => fn U =>
   2.112 -          HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split Q) Qs As' Bs')))
   2.113 +          (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, sQs)))
   2.114        | SOME raw_rel => prep_term no_defs_lthy raw_rel);
   2.115  
   2.116      val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
   2.117 @@ -1090,11 +1107,36 @@
   2.118  
   2.119          val in_srel = mk_lazy mk_in_srel;
   2.120  
   2.121 +        val eqset_imp_iff_pair = @{thm eqset_imp_iff_pair};
   2.122 +        val mem_Collect_etc = @{thms mem_Collect_eq fst_conv snd_conv prod.cases};
   2.123 +
   2.124 +        fun mk_rel_as_srel () =
   2.125 +          unfold_thms lthy mem_Collect_etc
   2.126 +            (funpow live (fn thm => thm RS @{thm fun_cong_pair}) (bnf_srel_def RS meta_eq_to_obj_eq)
   2.127 +               RS eqset_imp_iff_pair RS sym)
   2.128 +          |> Drule.zero_var_indexes;
   2.129 +
   2.130 +        val rel_as_srel = mk_lazy mk_rel_as_srel;
   2.131 +
   2.132 +        fun mk_rel_flip () =
   2.133 +          let
   2.134 +            val srel_converse_thm = Lazy.force srel_converse;
   2.135 +            val Rs' = Term.add_vars (prop_of srel_converse_thm) [];
   2.136 +            val cts = map (pairself (certify lthy)) (map Var Rs' ~~ sQs);
   2.137 +            val srel_converse_thm' = Drule.cterm_instantiate cts srel_converse_thm;
   2.138 +          in
   2.139 +            unfold_thms lthy (bnf_srel_def :: @{thm converse_iff} :: mem_Collect_etc)
   2.140 +              (srel_converse_thm' RS eqset_imp_iff_pair)
   2.141 +            |> Drule.zero_var_indexes |> Thm.generalize ([], map fst Qs') 1
   2.142 +          end;
   2.143 +
   2.144 +        val rel_flip = mk_lazy mk_rel_flip;
   2.145 +
   2.146          val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
   2.147  
   2.148          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong
   2.149 -          in_mono in_srel map_comp' map_id' map_wppull set_natural' srel_cong srel_mono srel_Id
   2.150 -          srel_Gr srel_converse srel_O;
   2.151 +          in_mono in_srel map_comp' map_id' map_wppull rel_as_srel rel_flip set_natural' srel_cong
   2.152 +          srel_mono srel_Id srel_Gr srel_converse srel_O;
   2.153  
   2.154          val wits = map2 mk_witness bnf_wits wit_thms;
   2.155  
   2.156 @@ -1141,6 +1183,8 @@
   2.157                      [(map_comp'N, [Lazy.force (#map_comp' facts)]),
   2.158                      (map_congN, [#map_cong axioms]),
   2.159                      (map_id'N, [Lazy.force (#map_id' facts)]),
   2.160 +                    (rel_as_srelN, [Lazy.force (#rel_as_srel facts)]),
   2.161 +                    (rel_flipN, [Lazy.force (#rel_flip facts)]),
   2.162                      (set_natural'N, map Lazy.force (#set_natural' facts)),
   2.163                      (srel_O_GrN, srel_O_Grs),
   2.164                      (srel_IdN, [Lazy.force (#srel_Id facts)]),