BNF relators preserve reflexivity
authortraytel
Mon Mar 16 23:05:56 2015 +0100 (2015-03-16)
changeset 5972664c2bb331035
parent 59725 e5dc7e7744f0
child 59727 3a1141d56bf1
BNF relators preserve reflexivity
src/HOL/BNF_Def.thy
src/HOL/Lifting.thy
src/HOL/Tools/BNF/bnf_def.ML
     1.1 --- a/src/HOL/BNF_Def.thy	Mon Mar 16 23:00:38 2015 +0100
     1.2 +++ b/src/HOL/BNF_Def.thy	Mon Mar 16 23:05:56 2015 +0100
     1.3 @@ -228,6 +228,12 @@
     1.4  lemma comp_apply_eq: "f (g x) = h (k x) \<Longrightarrow> (f \<circ> g) x = (h \<circ> k) x"
     1.5    unfolding comp_apply by assumption
     1.6  
     1.7 +lemma refl_ge_eq: "(\<And>x. R x x) \<Longrightarrow> op = \<le> R"
     1.8 +  by auto
     1.9 +
    1.10 +lemma ge_eq_refl: "op = \<le> R \<Longrightarrow> R x x"
    1.11 +  by auto
    1.12 +
    1.13  ML_file "Tools/BNF/bnf_util.ML"
    1.14  ML_file "Tools/BNF/bnf_tactics.ML"
    1.15  ML_file "Tools/BNF/bnf_def_tactics.ML"
     2.1 --- a/src/HOL/Lifting.thy	Mon Mar 16 23:00:38 2015 +0100
     2.2 +++ b/src/HOL/Lifting.thy	Mon Mar 16 23:05:56 2015 +0100
     2.3 @@ -376,9 +376,6 @@
     2.4  lemma reflp_ge_eq:
     2.5    "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
     2.6  
     2.7 -lemma ge_eq_refl:
     2.8 -  "R \<ge> op= \<Longrightarrow> R x x" by blast
     2.9 -
    2.10  text {* Proving a parametrized correspondence relation *}
    2.11  
    2.12  definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
     3.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 16 23:00:38 2015 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 16 23:05:56 2015 +0100
     3.3 @@ -81,6 +81,7 @@
     3.4    val rel_mono_of_bnf: bnf -> thm
     3.5    val rel_mono_strong0_of_bnf: bnf -> thm
     3.6    val rel_mono_strong_of_bnf: bnf -> thm
     3.7 +  val rel_refl_of_bnf: bnf -> thm
     3.8    val rel_transfer_of_bnf: bnf -> thm
     3.9    val rel_eq_of_bnf: bnf -> thm
    3.10    val rel_flip_of_bnf: bnf -> thm
    3.11 @@ -250,13 +251,14 @@
    3.12    rel_Grp: thm lazy,
    3.13    rel_conversep: thm lazy,
    3.14    rel_OO: thm lazy,
    3.15 +  rel_refl: thm lazy,
    3.16    rel_transfer: thm lazy
    3.17  };
    3.18  
    3.19  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
    3.20      inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident
    3.21      map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong
    3.22 -    rel_transfer rel_Grp rel_conversep rel_OO set_transfer = {
    3.23 +    set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer = {
    3.24    bd_Card_order = bd_Card_order,
    3.25    bd_Cinfinite = bd_Cinfinite,
    3.26    bd_Cnotzero = bd_Cnotzero,
    3.27 @@ -286,6 +288,7 @@
    3.28    rel_Grp = rel_Grp,
    3.29    rel_conversep = rel_conversep,
    3.30    rel_OO = rel_OO,
    3.31 +  rel_refl = rel_refl,
    3.32    set_transfer = set_transfer};
    3.33  
    3.34  fun map_facts f {
    3.35 @@ -318,6 +321,7 @@
    3.36    rel_Grp,
    3.37    rel_conversep,
    3.38    rel_OO,
    3.39 +  rel_refl,
    3.40    set_transfer} =
    3.41    {bd_Card_order = f bd_Card_order,
    3.42      bd_Cinfinite = f bd_Cinfinite,
    3.43 @@ -348,6 +352,7 @@
    3.44      rel_Grp = Lazy.map f rel_Grp,
    3.45      rel_conversep = Lazy.map f rel_conversep,
    3.46      rel_OO = Lazy.map f rel_OO,
    3.47 +    rel_refl = Lazy.map f rel_refl,
    3.48      set_transfer = Lazy.map (map f) set_transfer};
    3.49  
    3.50  val morph_facts = map_facts o Morphism.thm;
    3.51 @@ -479,6 +484,7 @@
    3.52  val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
    3.53  val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
    3.54  val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
    3.55 +val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf;
    3.56  val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
    3.57  val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
    3.58  val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
    3.59 @@ -654,14 +660,15 @@
    3.60  val set_map0N = "set_map0";
    3.61  val set_mapN = "set_map";
    3.62  val set_bdN = "set_bd";
    3.63 -val set_transferN = "set_transfer"
    3.64 +val set_transferN = "set_transfer";
    3.65  val rel_GrpN = "rel_Grp";
    3.66  val rel_conversepN = "rel_conversep";
    3.67 -val rel_mapN = "rel_map"
    3.68 -val rel_monoN = "rel_mono"
    3.69 -val rel_mono_strong0N = "rel_mono_strong0"
    3.70 -val rel_mono_strongN = "rel_mono_strong"
    3.71 -val rel_transferN = "rel_transfer"
    3.72 +val rel_mapN = "rel_map";
    3.73 +val rel_monoN = "rel_mono";
    3.74 +val rel_mono_strong0N = "rel_mono_strong0";
    3.75 +val rel_mono_strongN = "rel_mono_strong";
    3.76 +val rel_reflN = "rel_refl";
    3.77 +val rel_transferN = "rel_transfer";
    3.78  val rel_comppN = "rel_compp";
    3.79  val rel_compp_GrpN = "rel_compp_Grp";
    3.80  
    3.81 @@ -732,6 +739,7 @@
    3.82             (rel_mapN, Lazy.force (#rel_map facts), []),
    3.83             (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
    3.84             (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []),
    3.85 +           (rel_reflN, [Lazy.force (#rel_refl facts)], []),
    3.86             (rel_transferN, [Lazy.force (#rel_transfer facts)], []),
    3.87             (set_mapN, map Lazy.force (#set_map facts), []),
    3.88             (set_transferN, Lazy.force (#set_transfer facts), [])]
    3.89 @@ -1406,6 +1414,11 @@
    3.90  
    3.91          val rel_map = Lazy.lazy mk_rel_map;
    3.92  
    3.93 +        fun mk_rel_refl () = @{thm ge_eq_refl[OF ord_eq_le_trans]} OF
    3.94 +          [Lazy.force rel_eq RS sym, Lazy.force rel_mono OF (replicate live @{thm refl_ge_eq})];
    3.95 +
    3.96 +        val rel_refl = Lazy.lazy mk_rel_refl;
    3.97 +
    3.98          fun mk_map_transfer () =
    3.99            let
   3.100              val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
   3.101 @@ -1494,7 +1507,7 @@
   3.102          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
   3.103            in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0
   3.104            map_ident map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
   3.105 -          rel_mono_strong rel_transfer rel_Grp rel_conversep rel_OO set_transfer;
   3.106 +          rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer;
   3.107  
   3.108          val wits = map2 mk_witness bnf_wits wit_thms;
   3.109