generate property 'rel_mono_strong' for BNFs
authordesharna
Mon Aug 18 13:46:26 2014 +0200 (2014-08-18)
changeset 5796800e9c6d367e7
parent 57967 e6d2e998c30f
child 57969 1e7b9579b14f
generate property 'rel_mono_strong' for BNFs
src/HOL/Tools/BNF/bnf_def.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:46:22 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:46:26 2014 +0200
     1.3 @@ -74,6 +74,7 @@
     1.4    val rel_conversep_of_bnf: bnf -> thm
     1.5    val rel_mono_of_bnf: bnf -> thm
     1.6    val rel_mono_strong0_of_bnf: bnf -> thm
     1.7 +  val rel_mono_strong_of_bnf: bnf -> thm
     1.8    val rel_eq_of_bnf: bnf -> thm
     1.9    val rel_flip_of_bnf: bnf -> thm
    1.10    val set_bd_of_bnf: bnf -> thm list
    1.11 @@ -235,6 +236,7 @@
    1.12    rel_map: thm list lazy,
    1.13    rel_mono: thm lazy,
    1.14    rel_mono_strong0: thm lazy,
    1.15 +  rel_mono_strong: thm lazy,
    1.16    rel_Grp: thm lazy,
    1.17    rel_conversep: thm lazy,
    1.18    rel_OO: thm lazy
    1.19 @@ -242,7 +244,7 @@
    1.20  
    1.21  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
    1.22      inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
    1.23 -    rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO = {
    1.24 +    rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp rel_conversep rel_OO = {
    1.25    bd_Card_order = bd_Card_order,
    1.26    bd_Cinfinite = bd_Cinfinite,
    1.27    bd_Cnotzero = bd_Cnotzero,
    1.28 @@ -265,6 +267,7 @@
    1.29    rel_map = rel_map,
    1.30    rel_mono = rel_mono,
    1.31    rel_mono_strong0 = rel_mono_strong0,
    1.32 +  rel_mono_strong = rel_mono_strong,
    1.33    rel_Grp = rel_Grp,
    1.34    rel_conversep = rel_conversep,
    1.35    rel_OO = rel_OO};
    1.36 @@ -292,6 +295,7 @@
    1.37    rel_map,
    1.38    rel_mono,
    1.39    rel_mono_strong0,
    1.40 +  rel_mono_strong,
    1.41    rel_Grp,
    1.42    rel_conversep,
    1.43    rel_OO} =
    1.44 @@ -317,6 +321,7 @@
    1.45      rel_map = Lazy.map (map f) rel_map,
    1.46      rel_mono = Lazy.map f rel_mono,
    1.47      rel_mono_strong0 = Lazy.map f rel_mono_strong0,
    1.48 +    rel_mono_strong = Lazy.map f rel_mono_strong,
    1.49      rel_Grp = Lazy.map f rel_Grp,
    1.50      rel_conversep = Lazy.map f rel_conversep,
    1.51      rel_OO = Lazy.map f rel_OO};
    1.52 @@ -446,6 +451,7 @@
    1.53  val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
    1.54  val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
    1.55  val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
    1.56 +val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
    1.57  val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
    1.58  val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
    1.59  val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
    1.60 @@ -616,6 +622,7 @@
    1.61  val rel_mapN = "rel_map"
    1.62  val rel_monoN = "rel_mono"
    1.63  val rel_mono_strong0N = "rel_mono_strong0"
    1.64 +val rel_mono_strongN = "rel_mono_strong"
    1.65  val rel_comppN = "rel_compp";
    1.66  val rel_compp_GrpN = "rel_compp_Grp";
    1.67  
    1.68 @@ -656,6 +663,7 @@
    1.69             (map_comp0N, [#map_comp0 axioms]),
    1.70             (map_transferN, [Lazy.force (#map_transfer facts)]),
    1.71             (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
    1.72 +           (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
    1.73             (set_map0N, #set_map0 axioms),
    1.74             (set_bdN, #set_bd axioms)] @
    1.75            (witNs ~~ wit_thmss_of_bnf bnf)
    1.76 @@ -1319,6 +1327,10 @@
    1.77  
    1.78          val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
    1.79  
    1.80 +        fun mk_rel_mono_strong () = Object_Logic.rulify lthy (Lazy.force rel_mono_strong0)
    1.81 +
    1.82 +        val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
    1.83 +
    1.84          fun mk_rel_map () =
    1.85            let
    1.86              fun mk_goal lhs rhs =
    1.87 @@ -1368,7 +1380,8 @@
    1.88  
    1.89          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
    1.90            in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
    1.91 -          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO;
    1.92 +          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp
    1.93 +          rel_conversep rel_OO;
    1.94  
    1.95          val wits = map2 mk_witness bnf_wits wit_thms;
    1.96