author huffman Thu Oct 14 09:34:00 2010 -0700 (2010-10-14) changeset 40013 9db8fb58fddc parent 40012 f13341a45407 child 40014 7469b323e260
```     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 09:28:05 2010 -0700
1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 09:34:00 2010 -0700
1.3 @@ -98,66 +98,30 @@
1.4    InductTacs.case_tac ctxt (v^"=UU") i THEN
1.5    asm_simp_tac (HOLCF_ss addsimps rews) i;
1.6
1.7 -(* ----- general proofs ----------------------------------------------------- *)
1.8 -
1.9 -val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
1.10 +(******************************************************************************)
1.11 +(***************************** proofs about take ******************************)
1.12 +(******************************************************************************)
1.13
1.14 -fun theorems
1.15 +fun take_theorems
1.16      (((dname, _), cons) : eq, eqs : eq list)
1.17 -    (dbind : binding)
1.18 -    (spec : (binding * (bool * binding option * typ) list * mixfix) list)
1.19      (iso_info : Domain_Take_Proofs.iso_info)
1.20      (take_info : Domain_Take_Proofs.take_induct_info)
1.21 +    (result)
1.22      (thy : theory) =
1.23  let
1.24 -
1.25 -val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
1.26 -val map_tab = Domain_Take_Proofs.get_map_tab thy;
1.27 -
1.28 -
1.29 -(* ----- getting the axioms and definitions --------------------------------- *)
1.30 -
1.31 -val ax_abs_iso = #abs_inverse iso_info;
1.32 -val ax_rep_iso = #rep_inverse iso_info;
1.33 +  val map_tab = Domain_Take_Proofs.get_map_tab thy;
1.34
1.35 -val abs_const = #abs_const iso_info;
1.36 -val rep_const = #rep_const iso_info;
1.37 -
1.38 -local
1.39 -  fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
1.40 -in
1.41 -  val ax_take_0      = ga "take_0" dname;
1.42 -  val ax_take_strict = ga "take_strict" dname;
1.43 -end; (* local *)
1.44 -
1.45 -val {take_Suc_thms, deflation_take_thms, ...} = take_info;
1.46 -
1.47 -(* ----- define constructors ------------------------------------------------ *)
1.48 +  val ax_abs_iso = #abs_inverse iso_info;
1.49 +  val {take_Suc_thms, deflation_take_thms, ...} = take_info;
1.50 +  val con_appls = #con_betas result;
1.51
1.52 -val (result, thy) =
1.53 -    Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
1.54 -
1.55 -val con_appls = #con_betas result;
1.56 -val {nchotomy, exhaust, ...} = result;
1.57 -val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
1.58 -val {sel_rews, ...} = result;
1.59 -val when_rews = #cases result;
1.60 -val when_strict = hd when_rews;
1.61 -val dis_rews = #dis_rews result;
1.62 -val mat_rews = #match_rews result;
1.63 +  local
1.64 +    fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
1.65 +  in
1.66 +    val ax_take_0      = ga "take_0" dname;
1.67 +    val ax_take_strict = ga "take_strict" dname;
1.68 +  end;
1.69
1.70 -(* ----- theorems concerning the isomorphism -------------------------------- *)
1.71 -
1.72 -val pg = pg' thy;
1.73 -
1.74 -val retraction_strict = @{thm retraction_strict};
1.75 -val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
1.76 -val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
1.77 -val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
1.78 -
1.79 -(* ----- theorems concerning one induction step ----------------------------- *)
1.80 -
1.81 -local
1.82    fun dc_take dn = %%:(dn^"_take");
1.83    val dnames = map (fst o fst) eqs;
1.84    val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
1.85 @@ -186,12 +150,55 @@
1.86            [ax_abs_iso] @ @{thms take_con_rules}
1.87            @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
1.88        val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
1.89 -    in pg con_appls goal (K tacs) end;
1.90 +    in pg' thy con_appls goal (K tacs) end;
1.91    val take_apps = map one_take_app cons;
1.92 +  val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
1.93  in
1.94 -  val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
1.95 +  take_rews
1.96  end;
1.97
1.98 +(* ----- general proofs ----------------------------------------------------- *)
1.99 +
1.100 +val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
1.101 +
1.102 +fun theorems
1.103 +    (eq as ((dname, _), cons) : eq, eqs : eq list)
1.104 +    (dbind : binding)
1.105 +    (spec : (binding * (bool * binding option * typ) list * mixfix) list)
1.106 +    (iso_info : Domain_Take_Proofs.iso_info)
1.107 +    (take_info : Domain_Take_Proofs.take_induct_info)
1.108 +    (thy : theory) =
1.109 +let
1.110 +
1.111 +val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
1.112 +
1.113 +(* ----- define constructors ------------------------------------------------ *)
1.114 +
1.115 +val (result, thy) =
1.116 +    Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
1.117 +
1.118 +val {nchotomy, exhaust, ...} = result;
1.119 +val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
1.120 +val {sel_rews, ...} = result;
1.121 +val when_rews = #cases result;
1.122 +val when_strict = hd when_rews;
1.123 +val dis_rews = #dis_rews result;
1.124 +val mat_rews = #match_rews result;
1.125 +
1.126 +(* ----- theorems concerning the isomorphism -------------------------------- *)
1.127 +
1.128 +val ax_abs_iso = #abs_inverse iso_info;
1.129 +val ax_rep_iso = #rep_inverse iso_info;
1.130 +
1.131 +val retraction_strict = @{thm retraction_strict};
1.132 +val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
1.133 +val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
1.134 +val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
1.135 +
1.136 +(* ----- theorems concerning one induction step ----------------------------- *)
1.137 +
1.138 +val take_rews = take_theorems (eq, eqs) iso_info take_info result thy;
1.139 +
1.140  val case_ns =
1.141      "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
1.142
```