# HG changeset patch # User huffman # Date 1257193583 28800 # Node ID 45c5c3c51918ef3e6e717af3dbcb524a2766b628 # Parent 7d2c6e7f91bd07cbacdc3ddcd6e2424c78f75be9 domain package no longer uses cfst/csnd/cpair diff -r 7d2c6e7f91bd -r 45c5c3c51918 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Nov 02 19:56:06 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Nov 02 12:26:23 2009 -0800 @@ -66,7 +66,7 @@ Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); val copy_def = - let fun r i = cproj (Bound 0) eqs i; + let fun r i = proj (Bound 0) eqs i; in ("copy_def", %%:(dname^"_copy") == /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end; @@ -128,12 +128,12 @@ (* ----- axiom and definitions concerning induction ------------------------- *) - val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n + val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n `%x_name === %:x_name)); val take_def = ("take_def", %%:(dname^"_take") == - mk_lam("n",cproj + mk_lam("n",proj (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); val finite_def = ("finite_def", diff -r 7d2c6e7f91bd -r 45c5c3c51918 src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Mon Nov 02 19:56:06 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Mon Nov 02 12:26:23 2009 -0800 @@ -94,7 +94,6 @@ val mk_iterate : term * term * term -> term; val mk_fail : term; val mk_return : term -> term; - val cproj : term -> 'a list -> int -> term; val list_ccomb : term * term list -> term; (* val con_app : string -> ('a * 'b * string) list -> term; @@ -312,8 +311,6 @@ fun mk_compact t = %%: @{const_name compact} $ t; val ID = %%: @{const_name ID}; fun mk_strictify t = %%: @{const_name strictify}`t; -fun mk_cfst t = %%: @{const_name cfst}`t; -fun mk_csnd t = %%: @{const_name csnd}`t; (*val csplitN = "Cprod.csplit";*) (*val sfstN = "Sprod.sfst";*) (*val ssndN = "Sprod.ssnd";*) @@ -344,7 +341,6 @@ | prj f1 _ x (_::y::ys) 0 = f1 x y | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; -fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x; fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T); @@ -353,7 +349,7 @@ val UU = %%: @{const_name UU}; fun strict f = f`UU === UU; fun defined t = t ~= UU; -fun cpair (t,u) = %%: @{const_name cpair}`t`u; +fun cpair (t,u) = %%: @{const_name Pair} $ t $ u; fun spair (t,u) = %%: @{const_name spair}`t`u; fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) | mk_ctuple ts = foldr1 cpair ts; diff -r 7d2c6e7f91bd -r 45c5c3c51918 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Nov 02 19:56:06 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon Nov 02 12:26:23 2009 -0800 @@ -33,6 +33,8 @@ val antisym_less_inverse = @{thm below_antisym_inverse}; val beta_cfun = @{thm beta_cfun}; val cfun_arg_cong = @{thm cfun_arg_cong}; +val ch2ch_fst = @{thm ch2ch_fst}; +val ch2ch_snd = @{thm ch2ch_snd}; val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL}; val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR}; val chain_iterate = @{thm chain_iterate}; @@ -43,6 +45,14 @@ val compact_up = @{thm compact_up}; val contlub_cfun_arg = @{thm contlub_cfun_arg}; val contlub_cfun_fun = @{thm contlub_cfun_fun}; +val contlub_fst = @{thm contlub_fst}; +val contlub_snd = @{thm contlub_snd}; +val contlubE = @{thm contlubE}; +val cont_const = @{thm cont_const}; +val cont_id = @{thm cont_id}; +val cont2cont_fst = @{thm cont2cont_fst}; +val cont2cont_snd = @{thm cont2cont_snd}; +val cont2cont_Rep_CFun = @{thm cont2cont_Rep_CFun}; val fix_def2 = @{thm fix_def2}; val injection_eq = @{thm injection_eq}; val injection_less = @{thm injection_below}; @@ -116,7 +126,7 @@ val chain_tac = REPEAT_DETERM o resolve_tac - [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL]; + [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL, ch2ch_fst, ch2ch_snd]; (* ----- general proofs ----------------------------------------------------- *) @@ -589,7 +599,7 @@ val lhs = dc_copy`%"f"`(con_app con args); fun one_rhs arg = if DatatypeAux.is_rec_type (dtyp_of arg) - then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg) + then Domain_Axioms.copy_of_dtyp (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg) else (%# arg); val rhs = con_app2 con one_rhs args; val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); @@ -836,12 +846,14 @@ val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; + val rules = [contlub_fst RS contlubE RS ssubst, + contlub_snd RS contlubE RS ssubst]; fun tacf {prems, context} = [ res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, stac fix_def2 1, REPEAT (CHANGED - (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)), + (resolve_tac rules 1 THEN chain_tac 1)), stac contlub_cfun_fun 1, stac contlub_cfun_fun 2, rtac lub_equal 3, @@ -955,6 +967,9 @@ fun one_adm n _ = mk_trp (mk_adm (%:(P_name n))); fun concf n dn = %:(P_name n) $ %:(x_name n); in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; + val cont_rules = + [cont_id, cont_const, cont2cont_Rep_CFun, + cont2cont_fst, cont2cont_snd]; fun tacf {prems, context} = map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ quant_tac context 1, @@ -963,13 +978,14 @@ REPEAT_DETERM ( TRY (rtac adm_conj 1) THEN rtac adm_subst 1 THEN - cont_tacR 1 THEN resolve_tac prems 1), + REPEAT (resolve_tac cont_rules 1) THEN + resolve_tac prems 1), strip_tac 1, rtac (rewrite_rule axs_take_def finite_ind) 1, ind_prems_tac prems]; val ind = (pg'' thy [] goal tacf handle ERROR _ => - (warning "Cannot prove infinite induction rule"; refl)); + (warning "Cannot prove infinite induction rule"; TrueI)); in (finites, ind) end ) handle THM _ =>