author huffman Thu Oct 14 13:28:31 2010 -0700 (2010-10-14) changeset 40016 2eff1cbc1ccb parent 40015 2fda96749081 child 40017 575d3aa1f3c5
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
```     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.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.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.119 +        ((Binding.qualified true "take_rews" dbind, take_apps),
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.175 -
4.176 -in
4.177 -  thy
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)
```