add function take_theorems
authorhuffman
Thu Oct 14 09:34:00 2010 -0700 (2010-10-14)
changeset 400139db8fb58fddc
parent 40012 f13341a45407
child 40014 7469b323e260
add function take_theorems
src/HOLCF/Tools/Domain/domain_theorems.ML
     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