added cproj', and therefore extended prj
authoroheimb
Tue Mar 24 15:57:18 1998 +0100 (1998-03-24)
changeset 4755843b5f159c7e
parent 4754 2c090aef2ca2
child 4756 329c09e15991
added cproj', and therefore extended prj
tried to fix polymorphism problem for take_defs. A full solution will require
significant changes.
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/domain/axioms.ML	Tue Mar 24 15:54:42 1998 +0100
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Tue Mar 24 15:57:18 1998 +0100
     1.3 @@ -37,8 +37,8 @@
     1.4  
     1.5    fun con_def outer recu m n (_,args) = let
     1.6       fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id)
     1.7 -			(if recu andalso is_rec arg then (cproj (Bound z) 
     1.8 -			(length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x));
     1.9 +			(if recu andalso is_rec arg then (cproj (Bound z) eqs
    1.10 +				  (rec_of arg))`Bound(z-x) else Bound(z-x));
    1.11       fun parms [] = %%"ONE"
    1.12       |   parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs);
    1.13       fun inj y 1 _ = y
    1.14 @@ -72,11 +72,10 @@
    1.15  
    1.16  (* ----- axiom and definitions concerning induction ------------------------- *)
    1.17  
    1.18 -  fun cproj' T = cproj T (length eqs) n;
    1.19 -  val reach_ax = ("reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
    1.20 +  val reach_ax = ("reach", mk_trp(cproj (%%"fix"`%%(comp_dname^"_copy")) eqs n
    1.21  					`%x_name === %x_name));
    1.22 -  val take_def = ("take_def",%%(dname^"_take") == mk_lam("n",cproj'
    1.23 -		    (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
    1.24 +  val take_def = ("take_def",%%(dname^"_take") == mk_lam("n",cproj' 
    1.25 +	     (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU") eqs n));
    1.26    val finite_def = ("finite_def",%%(dname^"_finite") == mk_lam(x_name,
    1.27  	mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
    1.28  
    1.29 @@ -113,7 +112,7 @@
    1.30  	val rec_idxs    = (recs_cnt-1) downto 0;
    1.31  	val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg)
    1.32  					 (allargs~~((allargs_cnt-1) downto 0)));
    1.33 -	fun rel_app i ra = proj (Bound(allargs_cnt+2)) (length eqs) (rec_of ra) $ 
    1.34 +	fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
    1.35  			   Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
    1.36  	val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj(
    1.37  	   Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1),
    1.38 @@ -121,7 +120,7 @@
    1.39          in foldr mk_ex (allvns, foldr mk_conj 
    1.40  			      (map (defined o Bound) nonlazy_idxs,capps)) end;
    1.41        fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
    1.42 -	 		proj (Bound 2) (length eqs) n $ Bound 1 $ Bound 0,
    1.43 +	 		proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
    1.44           		foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
    1.45  					::map one_con cons))));
    1.46      in foldr' mk_conj (mapn one_comp 0 eqs)end ));
     2.1 --- a/src/HOLCF/domain/theorems.ML	Tue Mar 24 15:54:42 1998 +0100
     2.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Mar 24 15:57:18 1998 +0100
     2.3 @@ -55,6 +55,14 @@
     2.4                                  rtac rev_contrapos 1,
     2.5                                  etac (antisym_less_inverse RS conjunct1) 1,
     2.6                                  resolve_tac prems 1]);
     2.7 +(*
     2.8 +infixr 0 y;
     2.9 +val b = 0;
    2.10 +fun _ y t = by t;
    2.11 +fun g defs t = let val sg = sign_of thy;
    2.12 +                     val ct = Thm.cterm_of sg (inferT sg t);
    2.13 +                 in goalw_cterm defs ct end;
    2.14 +*)
    2.15  
    2.16  in
    2.17  
    2.18 @@ -63,14 +71,6 @@
    2.19  
    2.20  val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
    2.21  val pg = pg' thy;
    2.22 -(*
    2.23 -infixr 0 y;
    2.24 -val b = 0;
    2.25 -fun _ y t = by t;
    2.26 -fun g defs t = let val sg = sign_of thy;
    2.27 -                     val ct = Thm.cterm_of sg (inferT sg t);
    2.28 -                 in goalw_cterm defs ct end;
    2.29 -*)
    2.30  
    2.31  
    2.32  (* ----- getting the axioms and definitions --------------------------------- *)
    2.33 @@ -309,7 +309,7 @@
    2.34  val copy_apps = map (fn (con,args) => pg [ax_copy_def]
    2.35                      (lift_defined % (nonlazy_rec args,
    2.36                          mk_trp(dc_copy`%"f"`(con_app con args) ===
    2.37 -                (con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
    2.38 +                (con_app2 con (app_rec_arg (cproj (%"f") eqs)) args))))
    2.39                          (map (case_UU_tac (abs_strict::when_strict::con_stricts)
    2.40                                   1 o vname)
    2.41                           (filter (fn a => not (is_rec a orelse is_lazy a)) args)
    2.42 @@ -554,7 +554,7 @@
    2.43                                  strip_tac 1,
    2.44                                  rtac (rewrite_rule axs_take_def finite_ind) 1,
    2.45                                  ind_prems_tac prems])
    2.46 -)
    2.47 +  handle ERROR => (warning "Cannot prove infinite induction rule"; refl))
    2.48  end; (* local *)
    2.49  
    2.50  (* ----- theorem concerning coinduction ------------------------------------- *)
    2.51 @@ -563,10 +563,10 @@
    2.52    val xs = mapn (fn n => K (x_name n)) 1 dnames;
    2.53    fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
    2.54    val take_ss = HOL_ss addsimps take_rews;
    2.55 -  val sproj   = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")");
    2.56 +  val sproj   = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
    2.57    val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
    2.58                  foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
    2.59 -                  foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $ 
    2.60 +                  foldr mk_imp (mapn (fn n => K(proj (%"R") eqs n $ 
    2.61                                        bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
    2.62                      foldr' mk_conj (mapn (fn n => fn dn => 
    2.63                                  (dc_take dn $ %"n" `bnd_arg n 0 === 
    2.64 @@ -578,7 +578,7 @@
    2.65                                  flat(mapn (fn n => fn x => [
    2.66                                    rotate_tac (n+1) 1,
    2.67                                    etac all2E 1,
    2.68 -                                  eres_inst_tac [("P1", sproj "R" n_eqs n^
    2.69 +                                  eres_inst_tac [("P1", sproj "R" eqs n^
    2.70                                          " "^x^" "^x^"'")](mp RS disjE) 1,
    2.71                                    TRY(safe_tac HOL_cs),
    2.72                                    REPEAT(CHANGED(asm_simp_tac take_ss 1))]) 
    2.73 @@ -586,7 +586,7 @@
    2.74  in
    2.75  val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===>
    2.76                  foldr (op ===>) (mapn (fn n => fn x => 
    2.77 -                  mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
    2.78 +                  mk_trp(proj (%"R") eqs n $ %x $ %(x^"'"))) 0 xs,
    2.79                    mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
    2.80                                  TRY(safe_tac HOL_cs)] @
    2.81                                  flat(map (fn take_lemma => [