src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 40016 2eff1cbc1ccb
parent 40014 7469b323e260
child 40017 575d3aa1f3c5
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 10:16:46 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:28:31 2010 -0700
     1.3 @@ -9,17 +9,12 @@
     1.4  
     1.5  signature DOMAIN_THEOREMS =
     1.6  sig
     1.7 -  val theorems:
     1.8 -      Domain_Library.eq * Domain_Library.eq list ->
     1.9 -      binding ->
    1.10 -      (binding * (bool * binding option * typ) list * mixfix) list ->
    1.11 -      Domain_Take_Proofs.iso_info ->
    1.12 -      Domain_Take_Proofs.take_induct_info ->
    1.13 -      theory -> thm list * theory;
    1.14 -
    1.15    val comp_theorems :
    1.16        binding * Domain_Library.eq list ->
    1.17 +      (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
    1.18 +      Domain_Take_Proofs.iso_info list ->
    1.19        Domain_Take_Proofs.take_induct_info ->
    1.20 +      Domain_Constructors.constr_info list ->
    1.21        theory -> thm list * theory
    1.22  
    1.23    val quiet_mode: bool Unsynchronized.ref;
    1.24 @@ -103,131 +98,66 @@
    1.25  (******************************************************************************)
    1.26  
    1.27  fun take_theorems
    1.28 -    (((dname, _), cons) : eq, eqs : eq list)
    1.29 -    (iso_info : Domain_Take_Proofs.iso_info)
    1.30 +    (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    1.31 +    (iso_infos : Domain_Take_Proofs.iso_info list)
    1.32      (take_info : Domain_Take_Proofs.take_induct_info)
    1.33 -    (result : Domain_Constructors.constr_info)
    1.34 -    (thy : theory) =
    1.35 +    (constr_infos : Domain_Constructors.constr_info list)
    1.36 +    (thy : theory) : thm list list * theory =
    1.37  let
    1.38 -  val map_tab = Domain_Take_Proofs.get_map_tab thy;
    1.39 +  open HOLCF_Library;
    1.40  
    1.41 -  val ax_abs_iso = #abs_inverse iso_info;
    1.42 -  val {take_Suc_thms, deflation_take_thms, ...} = take_info;
    1.43 -  val con_appls = #con_betas result;
    1.44 -
    1.45 -  local
    1.46 -    fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
    1.47 -  in
    1.48 -    val ax_take_0      = ga "take_0" dname;
    1.49 -    val ax_take_strict = ga "take_strict" dname;
    1.50 -  end;
    1.51 -
    1.52 -  fun dc_take dn = %%:(dn^"_take");
    1.53 -  val dnames = map (fst o fst) eqs;
    1.54 +  val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info;
    1.55    val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
    1.56  
    1.57 -  fun copy_of_dtyp tab r dt =
    1.58 -      if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
    1.59 -  and copy tab r (Datatype_Aux.DtRec i) = r i
    1.60 -    | copy tab r (Datatype_Aux.DtTFree a) = ID
    1.61 -    | copy tab r (Datatype_Aux.DtType (c, ds)) =
    1.62 -      case Symtab.lookup tab c of
    1.63 -        SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
    1.64 -      | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
    1.65 +  val n = Free ("n", @{typ nat});
    1.66 +  val n' = @{const Suc} $ n;
    1.67  
    1.68 -  fun one_take_app (con, args) =
    1.69 +  local
    1.70 +    val newTs = map #absT iso_infos;
    1.71 +    val subs = newTs ~~ map (fn t => t $ n) take_consts;
    1.72 +    fun is_ID (Const (c, _)) = (c = @{const_name ID})
    1.73 +      | is_ID _              = false;
    1.74 +  in
    1.75 +    fun map_of_arg v T =
    1.76 +      let val m = Domain_Take_Proofs.map_of_typ thy subs T;
    1.77 +      in if is_ID m then v else mk_capply (m, v) end;
    1.78 +  end
    1.79 +
    1.80 +  fun prove_take_apps
    1.81 +      ((((dbind, spec), iso_info), take_const), constr_info) thy =
    1.82      let
    1.83 -      fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    1.84 -      fun one_rhs arg =
    1.85 -          if Datatype_Aux.is_rec_type (dtyp_of arg)
    1.86 -          then copy_of_dtyp map_tab
    1.87 -                 mk_take (dtyp_of arg) ` (%# arg)
    1.88 -          else (%# arg);
    1.89 -      val lhs = (dc_take dname $ (%%: @{const_name Suc} $ %:"n")) ` (con_app con args);
    1.90 -      val rhs = con_app2 con one_rhs args;
    1.91 -      val goal = mk_trp (lhs === rhs);
    1.92 -      val rules =
    1.93 -          [ax_abs_iso] @ @{thms take_con_rules}
    1.94 -          @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
    1.95 -      val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
    1.96 -    in pg' thy con_appls goal (K tacs) end;
    1.97 -  val take_apps = map one_take_app cons;
    1.98 -  val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
    1.99 +      val {con_consts, con_betas, ...} = constr_info;
   1.100 +      val {abs_inverse, ...} = iso_info;
   1.101 +      fun prove_take_app (con_const : term) (bind, args, mx) =
   1.102 +        let
   1.103 +          val Ts = map (fn (_, _, T) => T) args;
   1.104 +          val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
   1.105 +          val vs = map Free (ns ~~ Ts);
   1.106 +          val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
   1.107 +          val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts);
   1.108 +          val goal = mk_trp (mk_eq (lhs, rhs));
   1.109 +          val rules =
   1.110 +              [abs_inverse] @ con_betas @ @{thms take_con_rules}
   1.111 +              @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
   1.112 +          val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   1.113 +        in
   1.114 +          Goal.prove_global thy [] [] goal (K tac)
   1.115 +        end;
   1.116 +      val take_apps = map2 prove_take_app con_consts spec;
   1.117 +    in
   1.118 +      yield_singleton Global_Theory.add_thmss
   1.119 +        ((Binding.qualified true "take_rews" dbind, take_apps),
   1.120 +        [Simplifier.simp_add]) thy
   1.121 +    end;
   1.122  in
   1.123 -  take_rews
   1.124 +  fold_map prove_take_apps
   1.125 +    (specs ~~ iso_infos ~~ take_consts ~~ constr_infos) thy
   1.126  end;
   1.127  
   1.128  (* ----- general proofs ----------------------------------------------------- *)
   1.129  
   1.130  val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
   1.131  
   1.132 -fun theorems
   1.133 -    (eq as ((dname, _), cons) : eq, eqs : eq list)
   1.134 -    (dbind : binding)
   1.135 -    (spec : (binding * (bool * binding option * typ) list * mixfix) list)
   1.136 -    (iso_info : Domain_Take_Proofs.iso_info)
   1.137 -    (take_info : Domain_Take_Proofs.take_induct_info)
   1.138 -    (thy : theory) =
   1.139 -let
   1.140 -
   1.141 -val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
   1.142 -
   1.143 -(* ----- define constructors ------------------------------------------------ *)
   1.144 -
   1.145 -val (result, thy) =
   1.146 -    Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
   1.147 -
   1.148 -val {nchotomy, exhaust, ...} = result;
   1.149 -val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
   1.150 -val {sel_rews, ...} = result;
   1.151 -val when_rews = #cases result;
   1.152 -val when_strict = hd when_rews;
   1.153 -val dis_rews = #dis_rews result;
   1.154 -val mat_rews = #match_rews result;
   1.155 -
   1.156 -(* ----- theorems concerning the isomorphism -------------------------------- *)
   1.157 -
   1.158 -val ax_abs_iso = #abs_inverse iso_info;
   1.159 -val ax_rep_iso = #rep_inverse iso_info;
   1.160 -
   1.161 -val retraction_strict = @{thm retraction_strict};
   1.162 -val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
   1.163 -val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
   1.164 -val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
   1.165 -
   1.166 -(* ----- theorems concerning one induction step ----------------------------- *)
   1.167 -
   1.168 -val take_rews = take_theorems (eq, eqs) iso_info take_info result thy;
   1.169 -
   1.170 -val case_ns =
   1.171 -    "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
   1.172 -
   1.173 -fun qualified name = Binding.qualified true name dbind;
   1.174 -val simp = Simplifier.simp_add;
   1.175 -
   1.176 -in
   1.177 -  thy
   1.178 -  |> Global_Theory.add_thmss [
   1.179 -     ((qualified "iso_rews"  , iso_rews    ), [simp]),
   1.180 -     ((qualified "nchotomy"  , [nchotomy]  ), []),
   1.181 -     ((qualified "exhaust"   , [exhaust]   ),
   1.182 -      [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
   1.183 -     ((qualified "when_rews" , when_rews   ), [simp]),
   1.184 -     ((qualified "compacts"  , compacts    ), [simp]),
   1.185 -     ((qualified "con_rews"  , con_rews    ), [simp]),
   1.186 -     ((qualified "sel_rews"  , sel_rews    ), [simp]),
   1.187 -     ((qualified "dis_rews"  , dis_rews    ), [simp]),
   1.188 -     ((qualified "dist_les"  , dist_les    ), [simp]),
   1.189 -     ((qualified "dist_eqs"  , dist_eqs    ), [simp]),
   1.190 -     ((qualified "inverts"   , inverts     ), [simp]),
   1.191 -     ((qualified "injects"   , injects     ), [simp]),
   1.192 -     ((qualified "take_rews" , take_rews   ), [simp]),
   1.193 -     ((qualified "match_rews", mat_rews    ), [simp])]
   1.194 -  |> snd
   1.195 -  |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
   1.196 -      dist_les @ dist_eqs)
   1.197 -end; (* let *)
   1.198 -
   1.199  (******************************************************************************)
   1.200  (****************************** induction rules *******************************)
   1.201  (******************************************************************************)
   1.202 @@ -440,6 +370,7 @@
   1.203  
   1.204  fun prove_coinduction
   1.205      (comp_dbind : binding, eqs : eq list)
   1.206 +    (take_rews : thm list)
   1.207      (take_lemmas : thm list)
   1.208      (thy : theory) : theory =
   1.209  let
   1.210 @@ -450,9 +381,6 @@
   1.211  val x_name = idx_name dnames "x"; 
   1.212  val n_eqs = length eqs;
   1.213  
   1.214 -val take_rews =
   1.215 -    maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
   1.216 -
   1.217  (* ----- define bisimulation predicate -------------------------------------- *)
   1.218  
   1.219  local
   1.220 @@ -581,7 +509,10 @@
   1.221  
   1.222  fun comp_theorems
   1.223      (comp_dbind : binding, eqs : eq list)
   1.224 +    (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
   1.225 +    (iso_infos : Domain_Take_Proofs.iso_info list)
   1.226      (take_info : Domain_Take_Proofs.take_induct_info)
   1.227 +    (constr_infos : Domain_Constructors.constr_info list)
   1.228      (thy : theory) =
   1.229  let
   1.230  val map_tab = Domain_Take_Proofs.get_map_tab thy;
   1.231 @@ -607,10 +538,12 @@
   1.232  
   1.233  (* theorems about take *)
   1.234  
   1.235 -val take_lemmas = #take_lemma_thms take_info;
   1.236 +val (take_rewss, thy) =
   1.237 +    take_theorems specs iso_infos take_info constr_infos thy;
   1.238  
   1.239 -val take_rews =
   1.240 -    maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
   1.241 +val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;
   1.242 +
   1.243 +val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss;
   1.244  
   1.245  (* prove induction rules, unless definition is indirect recursive *)
   1.246  val thy =
   1.247 @@ -619,7 +552,7 @@
   1.248  
   1.249  val thy =
   1.250      if is_indirect then thy else
   1.251 -    prove_coinduction (comp_dbind, eqs) take_lemmas thy;
   1.252 +    prove_coinduction (comp_dbind, eqs) take_rews take_lemma_thms thy;
   1.253  
   1.254  in
   1.255    (take_rews, thy)