added cproj', and therefore extended prj
tried to fix polymorphism problem for take_defs. A full solution will require
significant changes.
--- a/src/HOLCF/domain/axioms.ML Tue Mar 24 15:54:42 1998 +0100
+++ b/src/HOLCF/domain/axioms.ML Tue Mar 24 15:57:18 1998 +0100
@@ -37,8 +37,8 @@
fun con_def outer recu m n (_,args) = let
fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id)
- (if recu andalso is_rec arg then (cproj (Bound z)
- (length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x));
+ (if recu andalso is_rec arg then (cproj (Bound z) eqs
+ (rec_of arg))`Bound(z-x) else Bound(z-x));
fun parms [] = %%"ONE"
| parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs);
fun inj y 1 _ = y
@@ -72,11 +72,10 @@
(* ----- axiom and definitions concerning induction ------------------------- *)
- fun cproj' T = cproj T (length eqs) n;
- val reach_ax = ("reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
+ val reach_ax = ("reach", mk_trp(cproj (%%"fix"`%%(comp_dname^"_copy")) eqs n
`%x_name === %x_name));
- val take_def = ("take_def",%%(dname^"_take") == mk_lam("n",cproj'
- (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
+ val take_def = ("take_def",%%(dname^"_take") == mk_lam("n",cproj'
+ (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU") eqs n));
val finite_def = ("finite_def",%%(dname^"_finite") == mk_lam(x_name,
mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
@@ -113,7 +112,7 @@
val rec_idxs = (recs_cnt-1) downto 0;
val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
(allargs~~((allargs_cnt-1) downto 0)));
- fun rel_app i ra = proj (Bound(allargs_cnt+2)) (length eqs) (rec_of ra) $
+ fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $
Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj(
Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1),
@@ -121,7 +120,7 @@
in foldr mk_ex (allvns, foldr mk_conj
(map (defined o Bound) nonlazy_idxs,capps)) end;
fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
- proj (Bound 2) (length eqs) n $ Bound 1 $ Bound 0,
+ proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
::map one_con cons))));
in foldr' mk_conj (mapn one_comp 0 eqs)end ));
--- a/src/HOLCF/domain/theorems.ML Tue Mar 24 15:54:42 1998 +0100
+++ b/src/HOLCF/domain/theorems.ML Tue Mar 24 15:57:18 1998 +0100
@@ -55,6 +55,14 @@
rtac rev_contrapos 1,
etac (antisym_less_inverse RS conjunct1) 1,
resolve_tac prems 1]);
+(*
+infixr 0 y;
+val b = 0;
+fun _ y t = by t;
+fun g defs t = let val sg = sign_of thy;
+ val ct = Thm.cterm_of sg (inferT sg t);
+ in goalw_cterm defs ct end;
+*)
in
@@ -63,14 +71,6 @@
val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
val pg = pg' thy;
-(*
-infixr 0 y;
-val b = 0;
-fun _ y t = by t;
-fun g defs t = let val sg = sign_of thy;
- val ct = Thm.cterm_of sg (inferT sg t);
- in goalw_cterm defs ct end;
-*)
(* ----- getting the axioms and definitions --------------------------------- *)
@@ -309,7 +309,7 @@
val copy_apps = map (fn (con,args) => pg [ax_copy_def]
(lift_defined % (nonlazy_rec args,
mk_trp(dc_copy`%"f"`(con_app con args) ===
- (con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
+ (con_app2 con (app_rec_arg (cproj (%"f") eqs)) args))))
(map (case_UU_tac (abs_strict::when_strict::con_stricts)
1 o vname)
(filter (fn a => not (is_rec a orelse is_lazy a)) args)
@@ -554,7 +554,7 @@
strip_tac 1,
rtac (rewrite_rule axs_take_def finite_ind) 1,
ind_prems_tac prems])
-)
+ handle ERROR => (warning "Cannot prove infinite induction rule"; refl))
end; (* local *)
(* ----- theorem concerning coinduction ------------------------------------- *)
@@ -563,10 +563,10 @@
val xs = mapn (fn n => K (x_name n)) 1 dnames;
fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
val take_ss = HOL_ss addsimps take_rews;
- val sproj = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")");
+ val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
- foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $
+ foldr mk_imp (mapn (fn n => K(proj (%"R") eqs n $
bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
foldr' mk_conj (mapn (fn n => fn dn =>
(dc_take dn $ %"n" `bnd_arg n 0 ===
@@ -578,7 +578,7 @@
flat(mapn (fn n => fn x => [
rotate_tac (n+1) 1,
etac all2E 1,
- eres_inst_tac [("P1", sproj "R" n_eqs n^
+ eres_inst_tac [("P1", sproj "R" eqs n^
" "^x^" "^x^"'")](mp RS disjE) 1,
TRY(safe_tac HOL_cs),
REPEAT(CHANGED(asm_simp_tac take_ss 1))])
@@ -586,7 +586,7 @@
in
val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===>
foldr (op ===>) (mapn (fn n => fn x =>
- mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
+ mk_trp(proj (%"R") eqs n $ %x $ %(x^"'"))) 0 xs,
mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
TRY(safe_tac HOL_cs)] @
flat(map (fn take_lemma => [