src/HOL/Tools/BNF/bnf_def.ML
changeset 57981 81baacfd56e8
parent 57970 eaa986cd285a
child 58093 6f37a300c82b
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 14:19:23 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 15:03:22 2014 +0200
     1.3 @@ -60,6 +60,7 @@
     1.4    val map_comp_of_bnf: bnf -> thm
     1.5    val map_cong0_of_bnf: bnf -> thm
     1.6    val map_cong_of_bnf: bnf -> thm
     1.7 +  val map_cong_simp_of_bnf: bnf -> thm
     1.8    val map_def_of_bnf: bnf -> thm
     1.9    val map_id0_of_bnf: bnf -> thm
    1.10    val map_id_of_bnf: bnf -> thm
    1.11 @@ -227,6 +228,7 @@
    1.12    inj_map_strong: thm lazy,
    1.13    map_comp: thm lazy,
    1.14    map_cong: thm lazy,
    1.15 +  map_cong_simp: thm lazy,
    1.16    map_id: thm lazy,
    1.17    map_ident0: thm lazy,
    1.18    map_ident: thm lazy,
    1.19 @@ -245,9 +247,9 @@
    1.20  };
    1.21  
    1.22  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
    1.23 -    inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
    1.24 -    rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp
    1.25 -    rel_conversep rel_OO = {
    1.26 +    inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident
    1.27 +    map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong
    1.28 +    rel_Grp rel_conversep rel_OO = {
    1.29    bd_Card_order = bd_Card_order,
    1.30    bd_Cinfinite = bd_Cinfinite,
    1.31    bd_Cnotzero = bd_Cnotzero,
    1.32 @@ -260,6 +262,7 @@
    1.33    inj_map_strong = inj_map_strong,
    1.34    map_comp = map_comp,
    1.35    map_cong = map_cong,
    1.36 +  map_cong_simp = map_cong_simp,
    1.37    map_id = map_id,
    1.38    map_ident0 = map_ident0,
    1.39    map_ident = map_ident,
    1.40 @@ -289,6 +292,7 @@
    1.41    inj_map_strong,
    1.42    map_comp,
    1.43    map_cong,
    1.44 +  map_cong_simp,
    1.45    map_id,
    1.46    map_ident0,
    1.47    map_ident,
    1.48 @@ -316,6 +320,7 @@
    1.49      inj_map_strong = Lazy.map f inj_map_strong,
    1.50      map_comp = Lazy.map f map_comp,
    1.51      map_cong = Lazy.map f map_cong,
    1.52 +    map_cong_simp = Lazy.map f map_cong_simp,
    1.53      map_id = Lazy.map f map_id,
    1.54      map_ident0 = Lazy.map f map_ident0,
    1.55      map_ident = Lazy.map f map_ident,
    1.56 @@ -446,6 +451,7 @@
    1.57  val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf;
    1.58  val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
    1.59  val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
    1.60 +val map_cong_simp_of_bnf = Lazy.force o #map_cong_simp o #facts o rep_bnf;
    1.61  val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
    1.62  val le_rel_OO_of_bnf = #le_rel_OO o #axioms o rep_bnf;
    1.63  val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
    1.64 @@ -619,6 +625,7 @@
    1.65  val map_compN = "map_comp";
    1.66  val map_cong0N = "map_cong0";
    1.67  val map_congN = "map_cong";
    1.68 +val map_cong_simpN = "map_cong_simp";
    1.69  val map_transferN = "map_transfer";
    1.70  val rel_eqN = "rel_eq";
    1.71  val rel_flipN = "rel_flip";
    1.72 @@ -689,6 +696,7 @@
    1.73             (map_compN, [Lazy.force (#map_comp facts)], []),
    1.74             (map_cong0N, [#map_cong0 axioms], []),
    1.75             (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
    1.76 +           (map_cong_simpN, [Lazy.force (#map_cong_simp facts)], []),
    1.77             (map_idN, [Lazy.force (#map_id facts)], []),
    1.78             (map_id0N, [#map_id0 axioms], []),
    1.79             (map_identN, [Lazy.force (#map_ident facts)], []),
    1.80 @@ -1011,13 +1019,13 @@
    1.81          fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
    1.82        end;
    1.83  
    1.84 -    fun mk_map_cong_prem x z set f f_copy =
    1.85 -      Logic.all z (Logic.mk_implies
    1.86 +    fun mk_map_cong_prem mk_implies x z set f f_copy =
    1.87 +      Logic.all z (mk_implies
    1.88          (mk_Trueprop_mem (z, set $ x), mk_Trueprop_eq (f $ z, f_copy $ z)));
    1.89  
    1.90      val map_cong0_goal =
    1.91        let
    1.92 -        val prems = map4 (mk_map_cong_prem x) zs bnf_sets_As fs fs_copy;
    1.93 +        val prems = map4 (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy;
    1.94          val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
    1.95            Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
    1.96        in
    1.97 @@ -1147,20 +1155,23 @@
    1.98          val map_ident = Lazy.lazy (fn () => mk_map_ident lthy (Lazy.force map_id));
    1.99          val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
   1.100  
   1.101 -        fun mk_map_cong () =
   1.102 +        fun mk_map_cong mk_implies () =
   1.103            let
   1.104              val prem0 = mk_Trueprop_eq (x, x_copy);
   1.105 -            val prems = map4 (mk_map_cong_prem x_copy) zs bnf_sets_As fs fs_copy;
   1.106 +            val prems = map4 (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy;
   1.107              val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
   1.108                Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy);
   1.109              val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
   1.110                (Logic.list_implies (prem0 :: prems, eq));
   1.111            in
   1.112 -            Goal.prove_sorry lthy [] [] goal (fn _ => mk_map_cong_tac lthy (#map_cong0 axioms))
   1.113 +            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
   1.114 +              unfold_thms_tac lthy @{thms simp_implies_def} THEN
   1.115 +              mk_map_cong_tac lthy (#map_cong0 axioms))
   1.116              |> Thm.close_derivation
   1.117            end;
   1.118  
   1.119 -        val map_cong = Lazy.lazy mk_map_cong;
   1.120 +        val map_cong = Lazy.lazy (mk_map_cong Logic.mk_implies);
   1.121 +        val map_cong_simp = Lazy.lazy (mk_map_cong (fn (a, b) => @{term simp_implies} $ a $ b));
   1.122  
   1.123          fun mk_inj_map () =
   1.124            let
   1.125 @@ -1416,8 +1427,8 @@
   1.126          val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
   1.127  
   1.128          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
   1.129 -          in_mono in_rel inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident
   1.130 -          map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
   1.131 +          in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0
   1.132 +          map_ident map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
   1.133            rel_mono_strong rel_Grp rel_conversep rel_OO;
   1.134  
   1.135          val wits = map2 mk_witness bnf_wits wit_thms;