# HG changeset patch # User huffman # Date 1267308286 28800 # Node ID 3d8acfae6fb89162d7969dbef50c56ac116aff53 # Parent deaf221c4a59f61dfc4de2f37c946918a3bd9155 move proofs of when_rews intro domain_constructors.ML diff -r deaf221c4a59 -r 3d8acfae6fb8 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 10:12:47 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 14:04:46 2010 -0800 @@ -12,6 +12,7 @@ -> typ * (binding * (bool * binding option * typ) list * mixfix) list -> term * term -> thm * thm + -> thm -> theory -> { con_consts : term list, con_betas : thm list, @@ -23,6 +24,7 @@ injects : thm list, dist_les : thm list, dist_eqs : thm list, + cases : thm list, sel_rews : thm list } * theory; end; @@ -267,6 +269,12 @@ val simple_ss : simpset = HOL_basic_ss addsimps simp_thms; +val beta_ss = + HOL_basic_ss + addsimps simp_thms + addsimps [@{thm beta_cfun}] + addsimprocs [@{simproc cont_proc}]; + fun define_consts (specs : (binding * term * mixfix) list) (thy : theory) @@ -571,6 +579,76 @@ end; (******************************************************************************) +(**************** definition and theorems for case combinator *****************) +(******************************************************************************) + +fun add_case_combinator + (spec : (term * (bool * typ) list) list) + (lhsT : typ) + (dname : string) + (case_def : thm) + (con_betas : thm list) + (casedist : thm) + (iso_locale : thm) + (thy : theory) = + let + + (* prove rep/abs rules *) + val rep_strict = iso_locale RS @{thm iso.rep_strict}; + val abs_inverse = iso_locale RS @{thm iso.abs_iso}; + + (* calculate function arguments of case combinator *) + val resultT = TVar (("'a",0), @{sort pcpo}); + val fTs = map (fn (_, args) => map snd args -->> resultT) spec; + val fns = Datatype_Prop.indexify_names (map (K "f") spec); + val fs = map Free (fns ~~ fTs); + val caseT = fTs -->> (lhsT ->> resultT); + + (* TODO: move definition of case combinator here *) + val case_bind = Binding.name (dname ^ "_when"); + val case_const = Const (Sign.full_name thy case_bind, caseT); + val case_app = list_ccomb (case_const, fs); + + (* prove beta reduction rule for case combinator *) + val case_beta = beta_of_def thy case_def; + + (* prove strictness of case combinator *) + val case_strict = + let + val defs = [case_beta, mk_meta_eq rep_strict]; + val lhs = case_app ` mk_bottom lhsT; + val goal = mk_trp (mk_eq (lhs, mk_bottom resultT)); + val tacs = [resolve_tac @{thms sscase1 ssplit1 strictify1} 1]; + in prove thy defs goal (K tacs) end; + + (* prove rewrites for case combinator *) + local + fun one_case (con, args) f = + let + val Ts = map snd args; + val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + val assms = map (mk_trp o mk_defined) nonlazy; + val lhs = case_app ` list_ccomb (con, vs); + val rhs = list_ccomb (f, vs); + val concl = mk_trp (mk_eq (lhs, rhs)); + val goal = Logic.list_implies (assms, concl); + val defs = case_beta :: con_betas; + val rules1 = @{thms sscase2 sscase3 ssplit2 fup2 ID1}; + val rules2 = @{thms con_defined_iff_rules}; + val rules = abs_inverse :: rules1 @ rules2; + val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]; + in prove thy defs goal (K tacs) end; + in + val case_apps = map2 one_case spec fs; + end + + in + (case_strict :: case_apps, thy) + end + +(******************************************************************************) (************** definitions and theorems for selector functions ***************) (******************************************************************************) @@ -722,6 +800,7 @@ spec : (binding * (bool * binding option * typ) list * mixfix) list) (rep_const : term, abs_const : term) (rep_iso_thm : thm, abs_iso_thm : thm) + (case_def : thm) (thy : theory) = let @@ -741,7 +820,18 @@ in add_constructors con_spec abs_const iso_locale thy end; - val {con_consts, con_betas, ...} = con_result; + val {con_consts, con_betas, casedist, ...} = con_result; + + (* define case combinator *) + val (cases : thm list, thy) = + let + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con c (b, args, mx) = (c, map prep_arg args); + val case_spec = map2 prep_con con_consts spec; + in + add_case_combinator case_spec lhsT dname + case_def con_betas casedist iso_locale thy + end; (* TODO: enable this earlier *) val thy = Sign.add_path dname thy; @@ -762,13 +852,14 @@ { con_consts = con_consts, con_betas = con_betas, exhaust = #exhaust con_result, - casedist = #casedist con_result, + casedist = casedist, con_compacts = #con_compacts con_result, con_rews = #con_rews con_result, inverts = #inverts con_result, injects = #injects con_result, dist_les = #dist_les con_result, dist_eqs = #dist_eqs con_result, + cases = cases, sel_rews = sel_thms }; in (result, thy) diff -r deaf221c4a59 -r 3d8acfae6fb8 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 10:12:47 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 14:04:46 2010 -0800 @@ -73,8 +73,6 @@ val iso_rep_iso = @{thm iso.rep_iso}; val iso_abs_strict = @{thm iso.abs_strict}; val iso_rep_strict = @{thm iso.rep_strict}; -val iso_abs_defin' = @{thm iso.abs_defin'}; -val iso_rep_defin' = @{thm iso.rep_defin'}; val iso_abs_defined = @{thm iso.abs_defined}; val iso_rep_defined = @{thm iso.rep_defined}; val iso_compact_abs = @{thm iso.compact_abs}; @@ -161,16 +159,6 @@ val axs_dis_def = map (get_def dis_name) cons; val axs_mat_def = map (get_def mat_name) cons; val axs_pat_def = map (get_def pat_name) cons; -(* - val axs_sel_def = - let - fun def_of_sel sel = ga (sel^"_def") dname; - fun def_of_arg arg = Option.map def_of_sel (sel_of arg); - fun defs_of_con (_, _, args) = map_filter def_of_arg args; - in - maps defs_of_con cons - end; -*) val ax_copy_def = ga "copy_def" dname; end; (* local *) @@ -195,13 +183,14 @@ val (result, thy) = Domain_Constructors.add_domain_constructors (Long_Name.base_name dname) dom_eqn - (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy; + (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) ax_when_def thy; val con_appls = #con_betas result; val {exhaust, casedist, ...} = result; val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result; val {sel_rews, ...} = result; - +val when_rews = #cases result; +val when_strict = hd when_rews; (* ----- theorems concerning the isomorphism -------------------------------- *) @@ -215,66 +204,8 @@ val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso]; val abs_strict = ax_rep_iso RS (allI RS retraction_strict); val rep_strict = ax_abs_iso RS (allI RS retraction_strict); -val abs_defin' = iso_locale RS iso_abs_defin'; -val rep_defin' = iso_locale RS iso_rep_defin'; val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict]; -(* ----- generating beta reduction rules from definitions-------------------- *) - -val _ = trace " Proving beta reduction rules..."; - -local - fun arglist (Const _ $ Abs (s, _, t)) = - let - val (vars,body) = arglist t; - in (s :: vars, body) end - | arglist t = ([], t); - fun bind_fun vars t = Library.foldr mk_All (vars, t); - fun bound_vars 0 = [] - | bound_vars i = Bound (i-1) :: bound_vars (i - 1); -in - fun appl_of_def def = - let - val (_ $ con $ lam) = concl_of def; - val (vars, rhs) = arglist lam; - val lhs = list_ccomb (con, bound_vars (length vars)); - val appl = bind_fun vars (lhs == rhs); - val cs = ContProc.cont_thms lam; - val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs; - in pg (def::betas) appl (K [rtac reflexive_thm 1]) end; -end; - -val _ = trace "Proving when_appl..."; -val when_appl = appl_of_def ax_when_def; - -local - fun bind_fun t = Library.foldr mk_All (when_funs cons, t); - fun bound_fun i _ = Bound (length cons - i); - val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons); -in - val _ = trace " Proving when_strict..."; - val when_strict = - let - val axs = [when_appl, mk_meta_eq rep_strict]; - val goal = bind_fun (mk_trp (strict when_app)); - val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1]; - in pg axs goal (K tacs) end; - - val _ = trace " Proving when_apps..."; - val when_apps = - let - fun one_when n (con, _, args) = - let - val axs = when_appl :: con_appls; - val goal = bind_fun (lift_defined %: (nonlazy args, - mk_trp (when_app`(con_app con args) === - list_ccomb (bound_fun n 0, map %# args)))); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1]; - in pg axs goal (K tacs) end; - in mapn one_when 1 cons end; -end; -val when_rews = when_strict :: when_apps; - (* ----- theorems concerning the constructors, discriminators and selectors - *) local