--- 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",
--- 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;
--- 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 _ =>