# HG changeset patch # User oheimb # Date 890751438 -3600 # Node ID 843b5f159c7ec1791b471b2a2b8842927c04093f # Parent 2c090aef2ca2c9314d13b52977dfbe50ae12163a added cproj', and therefore extended prj tried to fix polymorphism problem for take_defs. A full solution will require significant changes. diff -r 2c090aef2ca2 -r 843b5f159c7e src/HOLCF/domain/axioms.ML --- 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 )); diff -r 2c090aef2ca2 -r 843b5f159c7e src/HOLCF/domain/theorems.ML --- 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 => [