remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
authorhuffman
Thu Oct 14 13:28:31 2010 -0700 (2010-10-14)
changeset 400162eff1cbc1ccb
parent 40015 2fda96749081
child 40017 575d3aa1f3c5
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 10:16:46 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 13:28:31 2010 -0700
     1.3 @@ -854,6 +854,7 @@
     1.4      (thy : theory) =
     1.5    let
     1.6      val dname = Binding.name_of dbind;
     1.7 +    val _ = writeln ("Proving isomorphism properties of domain "^dname^" ...");
     1.8  
     1.9      (* retrieve facts about rep/abs *)
    1.10      val lhsT = #absT iso_info;
    1.11 @@ -865,6 +866,7 @@
    1.12      val abs_strict = iso_locale RS @{thm iso.abs_strict};
    1.13      val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
    1.14      val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
    1.15 +    val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict];
    1.16  
    1.17      (* qualify constants and theorems with domain name *)
    1.18      val thy = Sign.add_path dname thy;
    1.19 @@ -878,7 +880,8 @@
    1.20        in
    1.21          add_constructors con_spec abs_const iso_locale thy
    1.22        end;
    1.23 -    val {con_consts, con_betas, exhaust, ...} = con_result;
    1.24 +    val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews,
    1.25 +          inverts, injects, dist_les, dist_eqs} = con_result;
    1.26  
    1.27      (* define case combinator *)
    1.28      val ((case_const : typ -> term, cases : thm list), thy) =
    1.29 @@ -928,17 +931,43 @@
    1.30      (* restore original signature path *)
    1.31      val thy = Sign.parent_path thy;
    1.32  
    1.33 +    (* bind theorem names in global theory *)
    1.34 +    val (_, thy) =
    1.35 +      let
    1.36 +        fun qualified name = Binding.qualified true name dbind;
    1.37 +        val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
    1.38 +        val dname = fst (dest_Type lhsT);
    1.39 +        val simp = Simplifier.simp_add;
    1.40 +        val case_names = Rule_Cases.case_names names;
    1.41 +        val cases_type = Induct.cases_type dname;
    1.42 +      in
    1.43 +        Global_Theory.add_thmss [
    1.44 +          ((qualified "iso_rews"  , iso_rews    ), [simp]),
    1.45 +          ((qualified "nchotomy"  , [nchotomy]  ), []),
    1.46 +          ((qualified "exhaust"   , [exhaust]   ), [case_names, cases_type]),
    1.47 +          ((qualified "when_rews" , cases       ), [simp]),
    1.48 +          ((qualified "compacts"  , compacts    ), [simp]),
    1.49 +          ((qualified "con_rews"  , con_rews    ), [simp]),
    1.50 +          ((qualified "sel_rews"  , sel_thms    ), [simp]),
    1.51 +          ((qualified "dis_rews"  , dis_thms    ), [simp]),
    1.52 +          ((qualified "dist_les"  , dist_les    ), [simp]),
    1.53 +          ((qualified "dist_eqs"  , dist_eqs    ), [simp]),
    1.54 +          ((qualified "inverts"   , inverts     ), [simp]),
    1.55 +          ((qualified "injects"   , injects     ), [simp]),
    1.56 +          ((qualified "match_rews", match_thms  ), [simp])] thy
    1.57 +      end;
    1.58 +
    1.59      val result =
    1.60        { con_consts = con_consts,
    1.61          con_betas = con_betas,
    1.62 -        nchotomy = #nchotomy con_result,
    1.63 +        nchotomy = nchotomy,
    1.64          exhaust = exhaust,
    1.65 -        compacts = #compacts con_result,
    1.66 -        con_rews = #con_rews con_result,
    1.67 -        inverts = #inverts con_result,
    1.68 -        injects = #injects con_result,
    1.69 -        dist_les = #dist_les con_result,
    1.70 -        dist_eqs = #dist_eqs con_result,
    1.71 +        compacts = compacts,
    1.72 +        con_rews = con_rews,
    1.73 +        inverts = inverts,
    1.74 +        injects = injects,
    1.75 +        dist_les = dist_les,
    1.76 +        dist_eqs = dist_eqs,
    1.77          cases = cases,
    1.78          sel_rews = sel_thms,
    1.79          dis_rews = dis_thms,
     2.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 10:16:46 2010 -0700
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 13:28:31 2010 -0700
     2.3 @@ -189,18 +189,18 @@
     2.4      val eqs : eq list =
     2.5          map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
     2.6  
     2.7 -    val ((rewss, take_rews), theorems_thy) =
     2.8 +    val (constr_infos, thy) =
     2.9          thy
    2.10 -          |> fold_map (fn (((dbind, eq), (_,cs)), info) =>
    2.11 -                Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
    2.12 -             (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
    2.13 -          ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
    2.14 +          |> fold_map (fn ((dbind, (_,cs)), info) =>
    2.15 +                Domain_Constructors.add_domain_constructors dbind cs info)
    2.16 +             (dbinds ~~ eqs' ~~ iso_infos);
    2.17 +
    2.18 +    val (take_rews, theorems_thy) =
    2.19 +        thy
    2.20 +          |> Domain_Theorems.comp_theorems (comp_dbind, eqs)
    2.21 +              (dbinds ~~ map snd eqs') iso_infos take_info constr_infos;
    2.22    in
    2.23      theorems_thy
    2.24 -      |> Global_Theory.add_thmss
    2.25 -           [((Binding.qualified true "rews" comp_dbind,
    2.26 -              flat rewss @ take_rews), [])]
    2.27 -      |> snd
    2.28    end;
    2.29  
    2.30  fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
     3.1 --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Oct 14 10:16:46 2010 -0700
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Oct 14 13:28:31 2010 -0700
     3.3 @@ -303,7 +303,7 @@
     3.4          val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
     3.5          val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
     3.6        in
     3.7 -        add_qualified_thm "take_0" (dbind, take_0_thm) thy
     3.8 +        add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy
     3.9        end;
    3.10      val (take_0_thms, thy) =
    3.11        fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy;
    3.12 @@ -373,7 +373,7 @@
    3.13              Drule.zero_var_indexes
    3.14                (@{thm deflation_strict} OF [deflation_take]);
    3.15        in
    3.16 -        add_qualified_thm "take_strict" (dbind, take_strict_thm) thy
    3.17 +        add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy
    3.18        end;
    3.19      val (take_strict_thms, thy) =
    3.20        fold_map prove_take_strict
     4.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 10:16:46 2010 -0700
     4.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:28:31 2010 -0700
     4.3 @@ -9,17 +9,12 @@
     4.4  
     4.5  signature DOMAIN_THEOREMS =
     4.6  sig
     4.7 -  val theorems:
     4.8 -      Domain_Library.eq * Domain_Library.eq list ->
     4.9 -      binding ->
    4.10 -      (binding * (bool * binding option * typ) list * mixfix) list ->
    4.11 -      Domain_Take_Proofs.iso_info ->
    4.12 -      Domain_Take_Proofs.take_induct_info ->
    4.13 -      theory -> thm list * theory;
    4.14 -
    4.15    val comp_theorems :
    4.16        binding * Domain_Library.eq list ->
    4.17 +      (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
    4.18 +      Domain_Take_Proofs.iso_info list ->
    4.19        Domain_Take_Proofs.take_induct_info ->
    4.20 +      Domain_Constructors.constr_info list ->
    4.21        theory -> thm list * theory
    4.22  
    4.23    val quiet_mode: bool Unsynchronized.ref;
    4.24 @@ -103,131 +98,66 @@
    4.25  (******************************************************************************)
    4.26  
    4.27  fun take_theorems
    4.28 -    (((dname, _), cons) : eq, eqs : eq list)
    4.29 -    (iso_info : Domain_Take_Proofs.iso_info)
    4.30 +    (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    4.31 +    (iso_infos : Domain_Take_Proofs.iso_info list)
    4.32      (take_info : Domain_Take_Proofs.take_induct_info)
    4.33 -    (result : Domain_Constructors.constr_info)
    4.34 -    (thy : theory) =
    4.35 +    (constr_infos : Domain_Constructors.constr_info list)
    4.36 +    (thy : theory) : thm list list * theory =
    4.37  let
    4.38 -  val map_tab = Domain_Take_Proofs.get_map_tab thy;
    4.39 +  open HOLCF_Library;
    4.40  
    4.41 -  val ax_abs_iso = #abs_inverse iso_info;
    4.42 -  val {take_Suc_thms, deflation_take_thms, ...} = take_info;
    4.43 -  val con_appls = #con_betas result;
    4.44 -
    4.45 -  local
    4.46 -    fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
    4.47 -  in
    4.48 -    val ax_take_0      = ga "take_0" dname;
    4.49 -    val ax_take_strict = ga "take_strict" dname;
    4.50 -  end;
    4.51 -
    4.52 -  fun dc_take dn = %%:(dn^"_take");
    4.53 -  val dnames = map (fst o fst) eqs;
    4.54 +  val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info;
    4.55    val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
    4.56  
    4.57 -  fun copy_of_dtyp tab r dt =
    4.58 -      if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
    4.59 -  and copy tab r (Datatype_Aux.DtRec i) = r i
    4.60 -    | copy tab r (Datatype_Aux.DtTFree a) = ID
    4.61 -    | copy tab r (Datatype_Aux.DtType (c, ds)) =
    4.62 -      case Symtab.lookup tab c of
    4.63 -        SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
    4.64 -      | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
    4.65 +  val n = Free ("n", @{typ nat});
    4.66 +  val n' = @{const Suc} $ n;
    4.67  
    4.68 -  fun one_take_app (con, args) =
    4.69 +  local
    4.70 +    val newTs = map #absT iso_infos;
    4.71 +    val subs = newTs ~~ map (fn t => t $ n) take_consts;
    4.72 +    fun is_ID (Const (c, _)) = (c = @{const_name ID})
    4.73 +      | is_ID _              = false;
    4.74 +  in
    4.75 +    fun map_of_arg v T =
    4.76 +      let val m = Domain_Take_Proofs.map_of_typ thy subs T;
    4.77 +      in if is_ID m then v else mk_capply (m, v) end;
    4.78 +  end
    4.79 +
    4.80 +  fun prove_take_apps
    4.81 +      ((((dbind, spec), iso_info), take_const), constr_info) thy =
    4.82      let
    4.83 -      fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    4.84 -      fun one_rhs arg =
    4.85 -          if Datatype_Aux.is_rec_type (dtyp_of arg)
    4.86 -          then copy_of_dtyp map_tab
    4.87 -                 mk_take (dtyp_of arg) ` (%# arg)
    4.88 -          else (%# arg);
    4.89 -      val lhs = (dc_take dname $ (%%: @{const_name Suc} $ %:"n")) ` (con_app con args);
    4.90 -      val rhs = con_app2 con one_rhs args;
    4.91 -      val goal = mk_trp (lhs === rhs);
    4.92 -      val rules =
    4.93 -          [ax_abs_iso] @ @{thms take_con_rules}
    4.94 -          @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
    4.95 -      val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
    4.96 -    in pg' thy con_appls goal (K tacs) end;
    4.97 -  val take_apps = map one_take_app cons;
    4.98 -  val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
    4.99 +      val {con_consts, con_betas, ...} = constr_info;
   4.100 +      val {abs_inverse, ...} = iso_info;
   4.101 +      fun prove_take_app (con_const : term) (bind, args, mx) =
   4.102 +        let
   4.103 +          val Ts = map (fn (_, _, T) => T) args;
   4.104 +          val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
   4.105 +          val vs = map Free (ns ~~ Ts);
   4.106 +          val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
   4.107 +          val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts);
   4.108 +          val goal = mk_trp (mk_eq (lhs, rhs));
   4.109 +          val rules =
   4.110 +              [abs_inverse] @ con_betas @ @{thms take_con_rules}
   4.111 +              @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
   4.112 +          val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   4.113 +        in
   4.114 +          Goal.prove_global thy [] [] goal (K tac)
   4.115 +        end;
   4.116 +      val take_apps = map2 prove_take_app con_consts spec;
   4.117 +    in
   4.118 +      yield_singleton Global_Theory.add_thmss
   4.119 +        ((Binding.qualified true "take_rews" dbind, take_apps),
   4.120 +        [Simplifier.simp_add]) thy
   4.121 +    end;
   4.122  in
   4.123 -  take_rews
   4.124 +  fold_map prove_take_apps
   4.125 +    (specs ~~ iso_infos ~~ take_consts ~~ constr_infos) thy
   4.126  end;
   4.127  
   4.128  (* ----- general proofs ----------------------------------------------------- *)
   4.129  
   4.130  val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
   4.131  
   4.132 -fun theorems
   4.133 -    (eq as ((dname, _), cons) : eq, eqs : eq list)
   4.134 -    (dbind : binding)
   4.135 -    (spec : (binding * (bool * binding option * typ) list * mixfix) list)
   4.136 -    (iso_info : Domain_Take_Proofs.iso_info)
   4.137 -    (take_info : Domain_Take_Proofs.take_induct_info)
   4.138 -    (thy : theory) =
   4.139 -let
   4.140 -
   4.141 -val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
   4.142 -
   4.143 -(* ----- define constructors ------------------------------------------------ *)
   4.144 -
   4.145 -val (result, thy) =
   4.146 -    Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
   4.147 -
   4.148 -val {nchotomy, exhaust, ...} = result;
   4.149 -val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
   4.150 -val {sel_rews, ...} = result;
   4.151 -val when_rews = #cases result;
   4.152 -val when_strict = hd when_rews;
   4.153 -val dis_rews = #dis_rews result;
   4.154 -val mat_rews = #match_rews result;
   4.155 -
   4.156 -(* ----- theorems concerning the isomorphism -------------------------------- *)
   4.157 -
   4.158 -val ax_abs_iso = #abs_inverse iso_info;
   4.159 -val ax_rep_iso = #rep_inverse iso_info;
   4.160 -
   4.161 -val retraction_strict = @{thm retraction_strict};
   4.162 -val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
   4.163 -val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
   4.164 -val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
   4.165 -
   4.166 -(* ----- theorems concerning one induction step ----------------------------- *)
   4.167 -
   4.168 -val take_rews = take_theorems (eq, eqs) iso_info take_info result thy;
   4.169 -
   4.170 -val case_ns =
   4.171 -    "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
   4.172 -
   4.173 -fun qualified name = Binding.qualified true name dbind;
   4.174 -val simp = Simplifier.simp_add;
   4.175 -
   4.176 -in
   4.177 -  thy
   4.178 -  |> Global_Theory.add_thmss [
   4.179 -     ((qualified "iso_rews"  , iso_rews    ), [simp]),
   4.180 -     ((qualified "nchotomy"  , [nchotomy]  ), []),
   4.181 -     ((qualified "exhaust"   , [exhaust]   ),
   4.182 -      [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
   4.183 -     ((qualified "when_rews" , when_rews   ), [simp]),
   4.184 -     ((qualified "compacts"  , compacts    ), [simp]),
   4.185 -     ((qualified "con_rews"  , con_rews    ), [simp]),
   4.186 -     ((qualified "sel_rews"  , sel_rews    ), [simp]),
   4.187 -     ((qualified "dis_rews"  , dis_rews    ), [simp]),
   4.188 -     ((qualified "dist_les"  , dist_les    ), [simp]),
   4.189 -     ((qualified "dist_eqs"  , dist_eqs    ), [simp]),
   4.190 -     ((qualified "inverts"   , inverts     ), [simp]),
   4.191 -     ((qualified "injects"   , injects     ), [simp]),
   4.192 -     ((qualified "take_rews" , take_rews   ), [simp]),
   4.193 -     ((qualified "match_rews", mat_rews    ), [simp])]
   4.194 -  |> snd
   4.195 -  |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
   4.196 -      dist_les @ dist_eqs)
   4.197 -end; (* let *)
   4.198 -
   4.199  (******************************************************************************)
   4.200  (****************************** induction rules *******************************)
   4.201  (******************************************************************************)
   4.202 @@ -440,6 +370,7 @@
   4.203  
   4.204  fun prove_coinduction
   4.205      (comp_dbind : binding, eqs : eq list)
   4.206 +    (take_rews : thm list)
   4.207      (take_lemmas : thm list)
   4.208      (thy : theory) : theory =
   4.209  let
   4.210 @@ -450,9 +381,6 @@
   4.211  val x_name = idx_name dnames "x"; 
   4.212  val n_eqs = length eqs;
   4.213  
   4.214 -val take_rews =
   4.215 -    maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
   4.216 -
   4.217  (* ----- define bisimulation predicate -------------------------------------- *)
   4.218  
   4.219  local
   4.220 @@ -581,7 +509,10 @@
   4.221  
   4.222  fun comp_theorems
   4.223      (comp_dbind : binding, eqs : eq list)
   4.224 +    (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
   4.225 +    (iso_infos : Domain_Take_Proofs.iso_info list)
   4.226      (take_info : Domain_Take_Proofs.take_induct_info)
   4.227 +    (constr_infos : Domain_Constructors.constr_info list)
   4.228      (thy : theory) =
   4.229  let
   4.230  val map_tab = Domain_Take_Proofs.get_map_tab thy;
   4.231 @@ -607,10 +538,12 @@
   4.232  
   4.233  (* theorems about take *)
   4.234  
   4.235 -val take_lemmas = #take_lemma_thms take_info;
   4.236 +val (take_rewss, thy) =
   4.237 +    take_theorems specs iso_infos take_info constr_infos thy;
   4.238  
   4.239 -val take_rews =
   4.240 -    maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
   4.241 +val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;
   4.242 +
   4.243 +val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss;
   4.244  
   4.245  (* prove induction rules, unless definition is indirect recursive *)
   4.246  val thy =
   4.247 @@ -619,7 +552,7 @@
   4.248  
   4.249  val thy =
   4.250      if is_indirect then thy else
   4.251 -    prove_coinduction (comp_dbind, eqs) take_lemmas thy;
   4.252 +    prove_coinduction (comp_dbind, eqs) take_rews take_lemma_thms thy;
   4.253  
   4.254  in
   4.255    (take_rews, thy)