# HG changeset patch # User huffman # Date 1267288211 28800 # Node ID d63655b8836905a1d14cf74865a7ad2707bc0053 # Parent 5356534f880e77fa2e8d8c2addd6ed1b866c056a move proofs of casedist into domain_constructors.ML diff -r 5356534f880e -r d63655b88369 src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Fri Feb 26 10:54:52 2010 -0800 +++ b/src/HOLCF/Domain.thy Sat Feb 27 08:30:11 2010 -0800 @@ -87,7 +87,10 @@ lemma rep_defined_iff: "(rep\x = \) = (x = \)" by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms) -lemma (in iso) compact_abs_rev: "compact (abs\x) \ compact x" +lemma casedist_rule: "rep\x = \ \ P \ x = \ \ P" + by (simp add: rep_defined_iff) + +lemma compact_abs_rev: "compact (abs\x) \ compact x" proof (unfold compact_def) assume "adm (\y. \ abs\x \ y)" with cont_Rep_CFun2 @@ -249,10 +252,10 @@ use "Tools/cont_consts.ML" use "Tools/cont_proc.ML" -use "Tools/Domain/domain_constructors.ML" use "Tools/Domain/domain_library.ML" use "Tools/Domain/domain_syntax.ML" use "Tools/Domain/domain_axioms.ML" +use "Tools/Domain/domain_constructors.ML" use "Tools/Domain/domain_theorems.ML" use "Tools/Domain/domain_extender.ML" diff -r 5356534f880e -r d63655b88369 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Fri Feb 26 10:54:52 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 08:30:11 2010 -0800 @@ -15,6 +15,8 @@ -> theory -> { con_consts : term list, con_betas : thm list, + exhaust : thm, + casedist : thm, con_compacts : thm list, con_rews : thm list, inverts : thm list, @@ -43,7 +45,9 @@ val mk_snd = HOLogic.mk_snd; val mk_not = HOLogic.mk_not; val mk_conj = HOLogic.mk_conj; +val mk_disj = HOLogic.mk_disj; +fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t; (*** Basic HOLCF concepts ***) @@ -332,6 +336,9 @@ (* get theorems about rep and abs *) val abs_strict = iso_locale RS @{thm iso.abs_strict}; + (* get types of type isomorphism *) + val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const); + fun vars_of args = let val Ts = map snd args; @@ -361,6 +368,53 @@ let fun one_con con (b, args, mx) = (con, args); in map2 one_con con_consts spec end; + (* prove exhaustiveness of constructors *) + local + fun arg2typ n (true, T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo}))) + | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo})); + fun args2typ n [] = (n, oneT) + | args2typ n [arg] = arg2typ n arg + | args2typ n (arg::args) = + let + val (n1, t1) = arg2typ n arg; + val (n2, t2) = args2typ n1 args + in (n2, mk_sprodT (t1, t2)) end; + fun cons2typ n [] = (n, oneT) + | cons2typ n [con] = args2typ n (snd con) + | cons2typ n (con::cons) = + let + val (n1, t1) = args2typ n (snd con); + val (n2, t2) = cons2typ n1 cons + in (n2, mk_ssumT (t1, t2)) end; + val ct = ctyp_of thy (snd (cons2typ 1 spec')); + val thm1 = instantiate' [SOME ct] [] @{thm exh_start}; + val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1; + val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2; + + val x = Free ("x", lhsT); + fun one_con (con, args) = + let + val Ts = map snd args; + val ns = Name.variant_list ["x"] (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + val eqn = mk_eq (x, list_ccomb (con, vs)); + val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy); + in Library.foldr mk_ex (vs, conj) end; + val goal = mk_trp (foldr1 mk_disj (mk_undef x :: map one_con spec')); + (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) + val tacs = [ + rtac (iso_locale RS @{thm iso.casedist_rule}) 1, + rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})], + rtac thm3 1]; + in + val exhaust = prove thy con_betas goal (K tacs); + val casedist = + (exhaust RS @{thm exh_casedist0}) + |> rewrite_rule @{thms exh_casedists} + |> Drule.export_without_context; + end; + (* prove compactness rules for constructors *) val con_compacts = let @@ -459,6 +513,8 @@ { con_consts = con_consts, con_betas = con_betas, + exhaust = exhaust, + casedist = casedist, con_compacts = con_compacts, con_rews = con_rews, inverts = inverts, @@ -631,8 +687,7 @@ val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff}; (* define constructor functions *) - val ({con_consts, con_betas, con_compacts, con_rews, inverts, injects}, - thy) = + val (con_result, thy) = let fun prep_arg (lazy, sel, T) = (lazy, T); fun prep_con (b, args, mx) = (b, map prep_arg args, mx); @@ -640,6 +695,7 @@ in add_constructors con_spec abs_const iso_locale thy end; + val {con_consts, con_betas, ...} = con_result; (* TODO: enable this earlier *) val thy = Sign.add_path dname thy; @@ -659,10 +715,12 @@ val result = { con_consts = con_consts, con_betas = con_betas, - con_compacts = con_compacts, - con_rews = con_rews, - inverts = inverts, - injects = injects, + exhaust = #exhaust con_result, + casedist = #casedist con_result, + con_compacts = #con_compacts con_result, + con_rews = #con_rews con_result, + inverts = #inverts con_result, + injects = #injects con_result, sel_rews = sel_thms }; in (result, thy) diff -r 5356534f880e -r d63655b88369 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Feb 26 10:54:52 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 08:30:11 2010 -0800 @@ -198,11 +198,10 @@ (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy; val con_appls = #con_betas result; -val con_compacts = #con_compacts result; -val con_rews = #con_rews result; -val sel_rews = #sel_rews result; -val inverts = #inverts result; -val injects = #injects result; +val {exhaust, casedist, ...} = result; +val {con_compacts, con_rews, inverts, injects, ...} = result; +val {sel_rews, ...} = result; + (* ----- theorems concerning the isomorphism -------------------------------- *) @@ -248,61 +247,6 @@ val _ = trace "Proving when_appl..."; val when_appl = appl_of_def ax_when_def; -local - fun arg2typ n arg = - let val t = TVar (("'a", n), pcpoS) - in (n + 1, if is_lazy arg then mk_uT t else t) end; - - fun args2typ n [] = (n, oneT) - | args2typ n [arg] = arg2typ n arg - | args2typ n (arg::args) = - let - val (n1, t1) = arg2typ n arg; - val (n2, t2) = args2typ n1 args - in (n2, mk_sprodT (t1, t2)) end; - - fun cons2typ n [] = (n,oneT) - | cons2typ n [con] = args2typ n (third con) - | cons2typ n (con::cons) = - let - val (n1, t1) = args2typ n (third con); - val (n2, t2) = cons2typ n1 cons - in (n2, mk_ssumT (t1, t2)) end; -in - fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons)); -end; - -local - val iso_swap = iso_locale RS iso_iso_swap; - fun one_con (con, _, args) = - let - val vns = Name.variant_list ["x"] (map vname args); - val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns)); - val eqn = %:x_name === con_app2 con %: vns; - val conj = foldr1 mk_conj (eqn :: map (defined o %:) nonlazy_vns); - in Library.foldr mk_ex (vns, conj) end; - - val conj_assoc = @{thm conj_assoc}; - val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons); - val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start; - val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1; - val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2; - - (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) - val tacs = [ - rtac disjE 1, - etac (rep_defin' RS disjI1) 2, - etac disjI2 2, - rewrite_goals_tac [mk_meta_eq iso_swap], - rtac thm3 1]; -in - val _ = trace " Proving exhaust..."; - val exhaust = pg con_appls (mk_trp exh) (K tacs); - val _ = trace " Proving casedist..."; - val casedist = - Drule.export_without_context (rewrite_rule exh_casedists (exhaust RS exh_casedist0)); -end; - local fun bind_fun t = Library.foldr mk_All (when_funs cons, t); fun bound_fun i _ = Bound (length cons - i);