speed improvements for the domain package
authorhuffman
Sat Apr 16 00:17:52 2005 +0200 (2005-04-16)
changeset 1574264eae3513064
parent 15741 29a78517543f
child 15743 814eed210b82
speed improvements for the domain package
src/HOLCF/HOLCF.thy
src/HOLCF/IsaMakefile
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/HOLCF.thy	Sat Apr 16 00:16:44 2005 +0200
     1.2 +++ b/src/HOLCF/HOLCF.thy	Sat Apr 16 00:17:52 2005 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  *)
     1.5  
     1.6  theory HOLCF
     1.7 -imports Sprod Ssum Up Lift Discrete One Tr
     1.8 +imports Sprod Ssum Up Lift Discrete One Tr Domain
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOLCF/IsaMakefile	Sat Apr 16 00:16:44 2005 +0200
     2.2 +++ b/src/HOLCF/IsaMakefile	Sat Apr 16 00:17:52 2005 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4  
     2.5  $(OUT)/HOLCF: $(OUT)/HOL Cfun.ML Cfun.thy \
     2.6    Cont.ML Cont.thy Cprod.ML Cprod.thy \
     2.7 -  Discrete.thy Fix.ML Fix.thy FunCpo.ML \
     2.8 +  Discrete.thy Domain.thy Fix.ML Fix.thy FunCpo.ML \
     2.9    FunCpo.thy HOLCF.ML HOLCF.thy Lift.ML \
    2.10    Lift.thy One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy \
    2.11    ROOT.ML Sprod.ML Sprod.thy \
     3.1 --- a/src/HOLCF/domain/theorems.ML	Sat Apr 16 00:16:44 2005 +0200
     3.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Apr 16 00:17:52 2005 +0200
     3.3 @@ -1,6 +1,7 @@
     3.4  (*  Title:      HOLCF/domain/theorems.ML
     3.5      ID:         $Id$
     3.6      Author:     David von Oheimb
     3.7 +                New proofs/tactics by Brian Huffman
     3.8  
     3.9  Proof generator for domain section.
    3.10  *)
    3.11 @@ -26,8 +27,6 @@
    3.12  fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf 
    3.13                                  | prems=> (cut_facts_tac prems 1)::tacsf);
    3.14  
    3.15 -local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
    3.16 -val kill_neq_tac = dtac trueI2 end;
    3.17  fun case_UU_tac rews i v =      case_tac (v^"=UU") i THEN
    3.18                                  asm_simp_tac (HOLCF_ss addsimps rews) i;
    3.19  
    3.20 @@ -62,7 +61,6 @@
    3.21  val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
    3.22  val pg = pg' thy;
    3.23  
    3.24 -
    3.25  (* ----- getting the axioms and definitions --------------------------------- *)
    3.26  
    3.27  local fun ga s dn = get_thm thy (dn ^ "." ^ s, NONE) in
    3.28 @@ -84,89 +82,117 @@
    3.29  val dc_copy = %%:(dname^"_copy");
    3.30  val x_name = "x";
    3.31  
    3.32 -val (rep_strict, abs_strict) = let 
    3.33 -         val r = ax_rep_iso RS (ax_abs_iso RS (allI  RSN(2,allI RS iso_strict)))
    3.34 -               in (r RS conjunct1, r RS conjunct2) end;
    3.35 -val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%:x_name === UU)) [
    3.36 -                           res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
    3.37 -                                etac ssubst 1, rtac rep_strict 1];
    3.38 -val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%:x_name === UU)) [
    3.39 -                           res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
    3.40 -                                etac ssubst 1, rtac abs_strict 1];
    3.41 +val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
    3.42 +val abs_strict = iso_locale RS iso_abs_strict;
    3.43 +val rep_strict = iso_locale RS iso_rep_strict;
    3.44 +val abs_defin' = iso_locale RS iso_abs_defin';
    3.45 +val rep_defin' = iso_locale RS iso_rep_defin';
    3.46  val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
    3.47  
    3.48 +(* ----- generating beta reduction rules from definitions-------------------- *)
    3.49 +
    3.50 +local
    3.51 +  fun k NONE = cont_const | k (SOME x) = x;
    3.52 +  
    3.53 +  fun ap NONE NONE = NONE
    3.54 +  |   ap x    y    = SOME (standard (cont2cont_Rep_CFun OF [k x, k y]));
    3.55 +
    3.56 +  fun var 0 = [SOME cont_id]
    3.57 +  |   var n = NONE :: var (n-1);
    3.58 +
    3.59 +  fun zip []      []      = []
    3.60 +  |   zip []      (y::ys) = (ap NONE y   ) :: zip [] ys
    3.61 +  |   zip (x::xs) []      = (ap x    NONE) :: zip xs []
    3.62 +  |   zip (x::xs) (y::ys) = (ap x    y   ) :: zip xs ys
    3.63 +
    3.64 +  fun lam [] = ([], cont_const)
    3.65 +  |   lam (x::ys) = let val x' = k x
    3.66 +                        val Lx = x' RS cont2cont_LAM
    3.67 +                    in  (map (fn y => SOME (k y RS Lx)) ys, x')
    3.68 +                    end;
    3.69 +
    3.70 +  fun term_conts (Bound n) = (var n, [])
    3.71 +  |   term_conts (Const _) = ([],[])
    3.72 +  |   term_conts (Const _ $ Abs (_,_,t)) = let
    3.73 +          val (cs,ls) = term_conts t
    3.74 +          val (cs',l) = lam cs
    3.75 +          in  (cs',l::ls)
    3.76 +          end
    3.77 +  |   term_conts (Const _ $ f $ t)
    3.78 +         = (zip (fst (term_conts f)) (fst (term_conts t)), [])
    3.79 +  |   term_conts t = let val dummy = prin t in ([],[]) end;
    3.80 +
    3.81 +  fun arglist (Const _ $ Abs (s,_,t)) = let
    3.82 +        val (vars,body) = arglist t
    3.83 +        in  (s :: vars, body) end
    3.84 +  |   arglist t = ([],t);
    3.85 +  fun bind_fun vars t = Library.foldr mk_All (vars,t);
    3.86 +  fun bound_vars 0 = [] | bound_vars i = (Bound (i-1) :: bound_vars (i-1));
    3.87 +in
    3.88 +  fun appl_of_def def = let
    3.89 +        val (_ $ con $ lam) = concl_of def
    3.90 +        val (vars, rhs) = arglist lam
    3.91 +        val lhs = Library.foldl (op `) (con, bound_vars (length vars));
    3.92 +        val appl = bind_fun vars (lhs == rhs)
    3.93 +        val ([],cs) = term_conts lam
    3.94 +        val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs
    3.95 +        in pg (def::betas) appl [rtac reflexive_thm 1] end;
    3.96 +end;
    3.97 +
    3.98 +val when_appl = appl_of_def ax_when_def;
    3.99 +val con_appls = map appl_of_def axs_con_def;
   3.100 +
   3.101 +local
   3.102 +  fun arg2typ n arg = let val t = TVar (("'a",n),["Pcpo.pcpo"])
   3.103 +                      in (n+1, if is_lazy arg then mk_uT t else t) end;
   3.104 +  fun args2typ n [] = (n,oneT)
   3.105 +  |   args2typ n [arg] = arg2typ n arg
   3.106 +  |   args2typ n (arg::args) = let val (n1,t1) = arg2typ n arg;
   3.107 +                                   val (n2,t2) = args2typ n1 args
   3.108 +			       in  (n2, mk_sprodT (t1, t2)) end;
   3.109 +  fun cons2typ n [] = (n,oneT)
   3.110 +  |   cons2typ n [con] = args2typ n (snd con)
   3.111 +  |   cons2typ n (con::cons) = let val (n1,t1) = args2typ n (snd con);
   3.112 +                                   val (n2,t2) = cons2typ n1 cons
   3.113 +			       in  (n2, mk_ssumT (t1, t2)) end;
   3.114 +in
   3.115 +  fun cons2ctyp cons = ctyp_of (sign_of thy) (snd (cons2typ 1 cons));
   3.116 +end;
   3.117 +
   3.118  local 
   3.119 -val iso_swap = pg [] (dc_rep`%"x" === %:"y" ==> %:"x" === dc_abs`%"y") [
   3.120 -                            dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
   3.121 -                            etac (ax_rep_iso RS subst) 1];
   3.122 -fun exh foldr1 cn quant foldr2 var = let
   3.123 +  val iso_swap = iso_locale RS iso_iso_swap;
   3.124    fun one_con (con,args) = let val vns = map vname args in
   3.125 -    Library.foldr quant (vns, foldr2 ((%:x_name === con_app2 con (var vns) vns)::
   3.126 -                              map (defined o (var vns)) (nonlazy args))) end
   3.127 -  in foldr1 ((cn(%:x_name===UU))::map one_con cons) end;
   3.128 +    Library.foldr mk_ex (vns, foldr' mk_conj ((%:x_name === con_app2 con %: vns)::
   3.129 +                              map (defined o %:) (nonlazy args))) end;
   3.130 +  val exh = foldr' mk_disj ((%:x_name===UU)::map one_con cons);
   3.131 +  val my_ctyp = cons2ctyp cons;
   3.132 +  val thm1 = instantiate' [SOME my_ctyp] [] exh_start;
   3.133 +  val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
   3.134 +  val thm3 = rewrite_rule [mk_meta_eq conj_assoc] thm2;
   3.135  in
   3.136 -val casedist = let 
   3.137 -            fun common_tac thm = rtac thm 1 THEN contr_tac 1;
   3.138 -            fun unit_tac true = common_tac upE1
   3.139 -            |   unit_tac _    = all_tac;
   3.140 -            fun prod_tac []          = common_tac oneE
   3.141 -            |   prod_tac [arg]       = unit_tac (is_lazy arg)
   3.142 -            |   prod_tac (arg::args) = 
   3.143 -                                common_tac sprodE THEN
   3.144 -                                kill_neq_tac 1 THEN
   3.145 -                                unit_tac (is_lazy arg) THEN
   3.146 -                                prod_tac args;
   3.147 -            fun sum_rest_tac p = SELECT_GOAL(EVERY[
   3.148 -                                rtac p 1,
   3.149 -                                rewrite_goals_tac axs_con_def,
   3.150 -                                dtac iso_swap 1,
   3.151 -                                simp_tac HOLCF_ss 1,
   3.152 -                                DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
   3.153 -            fun sum_tac [(_,args)]       [p]        = 
   3.154 -                                prod_tac args THEN sum_rest_tac p
   3.155 -            |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
   3.156 -                                common_tac ssumE THEN
   3.157 -                                kill_neq_tac 1 THEN kill_neq_tac 2 THEN
   3.158 -                                prod_tac args THEN sum_rest_tac p) THEN
   3.159 -                                sum_tac cons' prems
   3.160 -            |   sum_tac _ _ = Imposs "theorems:sum_tac";
   3.161 -          in pg'' thy [] (exh (fn l => Library.foldr (op ===>) (l,mk_trp(%:"P")))
   3.162 -                              (fn T => T ==> %:"P") mk_All
   3.163 -                              (fn l => Library.foldr (op ===>) (map mk_trp l,
   3.164 -                                                            mk_trp(%:"P")))
   3.165 -                              bound_arg)
   3.166 -                             (fn prems => [
   3.167 -                                cut_facts_tac [excluded_middle] 1,
   3.168 -                                etac disjE 1,
   3.169 -                                rtac (hd prems) 2,
   3.170 -                                etac rep_defin' 2,
   3.171 -                                if length cons = 1 andalso 
   3.172 -                                   length (snd(hd cons)) = 1 andalso 
   3.173 -                                   not(is_lazy(hd(snd(hd cons))))
   3.174 -                                then rtac (hd (tl prems)) 1 THEN atac 2 THEN
   3.175 -                                     rewrite_goals_tac axs_con_def THEN
   3.176 -                                     simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
   3.177 -                                else sum_tac cons (tl prems)])end;
   3.178 -val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %:)))[
   3.179 -                                rtac casedist 1,
   3.180 -                                DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)];
   3.181 +val exhaust = pg con_appls (mk_trp exh)[
   3.182 +(* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
   3.183 +			rtac disjE 1,
   3.184 +			etac (rep_defin' RS disjI1) 2,
   3.185 +			etac disjI2 2,
   3.186 +			rewrite_goals_tac [mk_meta_eq iso_swap],
   3.187 +			rtac thm3 1];
   3.188 +val casedist = standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   3.189  end;
   3.190  
   3.191  local 
   3.192    fun bind_fun t = Library.foldr mk_All (when_funs cons,t);
   3.193    fun bound_fun i _ = Bound (length cons - i);
   3.194    val when_app  = Library.foldl (op `) (%%:(dname^"_when"), mapn bound_fun 1 cons);
   3.195 -  val when_appl = pg [ax_when_def] (bind_fun(mk_trp(when_app`%x_name ===
   3.196 -             when_body cons (fn (m,n)=> bound_fun (n-m) 0)`(dc_rep`%x_name))))[
   3.197 -                                simp_tac HOLCF_ss 1];
   3.198  in
   3.199 -val when_strict = pg [] (bind_fun(mk_trp(strict when_app))) [
   3.200 -                        simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
   3.201 -val when_apps = let fun one_when n (con,args) = pg axs_con_def 
   3.202 +val when_strict = pg [when_appl, mk_meta_eq rep_strict]
   3.203 +			(bind_fun(mk_trp(strict when_app)))
   3.204 +			[resolve_tac [sscase1,ssplit1,strictify1] 1];
   3.205 +val when_apps = let fun one_when n (con,args) = pg (when_appl :: con_appls)
   3.206                  (bind_fun (lift_defined %: (nonlazy args, 
   3.207                  mk_trp(when_app`(con_app con args) ===
   3.208                         mk_cRep_CFun(bound_fun n 0,map %# args)))))[
   3.209 -                asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
   3.210 +                asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
   3.211          in mapn one_when 1 cons end;
   3.212  end;
   3.213  val when_rews = when_strict::when_apps;
   3.214 @@ -176,7 +202,7 @@
   3.215  val dis_rews = let
   3.216    val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp(
   3.217                               strict(%%:(dis_name con)))) [
   3.218 -                                simp_tac (HOLCF_ss addsimps when_rews) 1]) cons;
   3.219 +                                rtac when_strict 1]) cons;
   3.220    val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def
   3.221                     (lift_defined %: (nonlazy args,
   3.222                          (mk_trp((%%:(dis_name c))`(con_app con args) ===
   3.223 @@ -192,7 +218,7 @@
   3.224  in dis_stricts @ dis_defins @ dis_apps end;
   3.225  
   3.226  val con_stricts = List.concat(map (fn (con,args) => map (fn vn =>
   3.227 -                        pg (axs_con_def) 
   3.228 +                        pg con_appls
   3.229                             (mk_trp(con_app2 con (fn arg => if vname arg = vn 
   3.230                                          then UU else %# arg) args === UU))[
   3.231                                  asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
   3.232 @@ -304,7 +330,7 @@
   3.233                                   1 o vname)
   3.234                           (List.filter (fn a => not (is_rec a orelse is_lazy a)) args)
   3.235                          @[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
   3.236 -                          simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;
   3.237 +                          simp_tac (HOLCF_ss addsimps con_appls) 1]))cons;
   3.238  val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
   3.239                                          (con_app con args) ===UU))
   3.240       (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
   3.241 @@ -587,7 +613,6 @@
   3.242                                  take_lemmas));
   3.243  end; (* local *)
   3.244  
   3.245 -
   3.246  in thy |> Theory.add_path comp_dnam
   3.247         |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
   3.248  		("take_rews"  , take_rews  ),