Renamed functions % and %% to avoid clash with syntax for proof terms.
--- a/src/HOLCF/domain/axioms.ML Fri Aug 31 16:25:53 2001 +0200
+++ b/src/HOLCF/domain/axioms.ML Fri Aug 31 16:26:55 2001 +0200
@@ -22,62 +22,62 @@
(* ----- axioms and definitions concerning the isomorphism ------------------ *)
- val dc_abs = %%(dname^"_abs");
- val dc_rep = %%(dname^"_rep");
+ val dc_abs = %%:(dname^"_abs");
+ val dc_rep = %%:(dname^"_rep");
val x_name'= "x";
val x_name = idx_name eqs x_name' (n+1);
val dnam = Sign.base_name dname;
- val abs_iso_ax = ("abs_iso" ,mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
- val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
+ val abs_iso_ax = ("abs_iso" ,mk_trp(dc_rep`(dc_abs`%x_name')=== %:x_name'));
+ val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %:x_name'));
- val when_def = ("when_def",%%(dname^"_when") ==
+ val when_def = ("when_def",%%:(dname^"_when") ==
foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
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)
+ 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) 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 parms [] = %%:"ONE"
+ | parms vs = foldr'(fn(x,t)=> %%:"spair"`x`t)(mapn (idxs(length vs))1 vs);
fun inj y 1 _ = y
- | inj y _ 0 = %%"sinl"`y
- | inj y i j = %%"sinr"`(inj y (i-1) (j-1));
+ | inj y _ 0 = %%:"sinl"`y
+ | inj y i j = %%:"sinr"`(inj y (i-1) (j-1));
in foldr /\# (args, outer (inj (parms args) m n)) end;
- val copy_def = ("copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo
- foldl (op `) (%%(dname^"_when") ,
+ val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo
+ foldl (op `) (%%:(dname^"_when") ,
mapn (con_def Id true (length cons)) 0 cons)));
(* -- definitions concerning the constructors, discriminators and selectors - *)
val con_defs = mapn (fn n => fn (con,args) => (extern_name con ^"_def",
- %%con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons;
+ %%:con == con_def (fn t => dc_abs`t) false (length cons) n (con,args))) 0 cons;
val dis_defs = let
- fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) ==
- mk_cRep_CFun(%%(dname^"_when"),map
+ fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
+ mk_cRep_CFun(%%:(dname^"_when"),map
(fn (con',args) => (foldr /\#
- (args,if con'=con then %%"TT" else %%"FF"))) cons))
+ (args,if con'=con then %%:"TT" else %%:"FF"))) cons))
in map ddef cons end;
val sel_defs = let
- fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) ==
- mk_cRep_CFun(%%(dname^"_when"),map
- (fn (con',args) => if con'<>con then %%"UU" else
+ fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) ==
+ mk_cRep_CFun(%%:(dname^"_when"),map
+ (fn (con',args) => if con'<>con then %%:"UU" else
foldr /\# (args,Bound (length args - n))) cons));
in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
(* ----- axiom and definitions concerning induction ------------------------- *)
- 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") eqs n));
- val finite_def = ("finite_def",%%(dname^"_finite") == mk_lam(x_name,
- mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+ 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") eqs n));
+ val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
+ mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
in (dnam,
[abs_iso_ax, rep_iso_ax, reach_ax],
@@ -94,10 +94,10 @@
val comp_dname = Sign.full_name (sign_of thy') comp_dnam;
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
- fun copy_app dname = %%(dname^"_copy")`Bound 0;
- val copy_def = ("copy_def" , %%(comp_dname^"_copy") ==
+ fun copy_app dname = %%:(dname^"_copy")`Bound 0;
+ val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
/\"f"(foldr' cpair (map copy_app dnames)));
- val bisim_def = ("bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
+ val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R",
let
fun one_con (con,args) = let
val nonrec_args = filter_out is_rec args;
@@ -116,8 +116,8 @@
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_cRep_CFun(%%con,map (bound_arg allvns) vns1),
- Bound(allargs_cnt+0)===mk_cRep_CFun(%%con,map (bound_arg allvns) vns2)));
+ Bound(allargs_cnt+1)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns1),
+ Bound(allargs_cnt+0)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns2)));
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(
--- a/src/HOLCF/domain/library.ML Fri Aug 31 16:25:53 2001 +0200
+++ b/src/HOLCF/domain/library.ML Fri Aug 31 16:26:55 2001 +0200
@@ -108,9 +108,9 @@
(* ----- support for term expressions ----- *)
-fun % s = Free(s,dummyT);
-fun %# arg = %(vname arg);
-fun %% s = Const(s,dummyT);
+fun %: s = Free(s,dummyT);
+fun %# arg = %:(vname arg);
+fun %%: s = Const(s,dummyT);
local open HOLogic in
val mk_trp = mk_Trueprop;
@@ -120,36 +120,36 @@
fun mk_lam (x,T) = Abs(x,dummyT,T);
fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
local
- fun sg [s] = %s
- | sg (s::ss) = %%"_classes" $ %s $ sg ss
+ fun sg [s] = %:s
+ | sg (s::ss) = %%:"_classes" $ %:s $ sg ss
| sg _ = Imposs "library:sg";
- fun sf [] = %%"_emptysort"
- | sf s = %%"_sort" $ sg s
- fun tf (Type (s,args)) = foldl (op $) (%s,map tf args)
- | tf (TFree(s,sort)) = %%"_ofsort" $ %s $ sf sort
+ fun sf [] = %%:"_emptysort"
+ | sf s = %%:"_sort" $ sg s
+ fun tf (Type (s,args)) = foldl (op $) (%:s,map tf args)
+ | tf (TFree(s,sort)) = %%:"_ofsort" $ %:s $ sf sort
| tf _ = Imposs "library:tf";
in
-fun mk_constrain (typ,T) = %%"_constrain" $ T $ tf typ;
-fun mk_constrainall (x,typ,P) = %%"All" $ (%%"_constrainAbs" $ mk_lam(x,P) $ tf typ);
+fun mk_constrain (typ,T) = %%:"_constrain" $ T $ tf typ;
+fun mk_constrainall (x,typ,P) = %%:"All" $ (%%:"_constrainAbs" $ mk_lam(x,P) $ tf typ);
end;
fun mk_ex (x,P) = mk_exists (x,dummyT,P);
end;
-fun mk_All (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *)
+fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
-infixr 0 ===>;fun S ===> T = %%"==>" $ S $ T;
+infixr 0 ===>;fun S ===> T = %%:"==>" $ S $ T;
infixr 0 ==>;fun S ==> T = mk_trp S ===> mk_trp T;
-infix 0 ==; fun S == T = %%"==" $ S $ T;
-infix 1 ===; fun S === T = %%"op =" $ S $ T;
+infix 0 ==; fun S == T = %%:"==" $ S $ T;
+infix 1 ===; fun S === T = %%:"op =" $ S $ T;
infix 1 ~=; fun S ~= T = mk_not (S === T);
-infix 1 <<; fun S << T = %%"op <<" $ S $ T;
+infix 1 <<; fun S << T = %%:"op <<" $ S $ T;
infix 1 ~<<; fun S ~<< T = mk_not (S << T);
-infix 9 ` ; fun f` x = %%"Rep_CFun" $ f $ x;
-infix 9 `% ; fun f`% s = f` % s;
-infix 9 `%%; fun f`%%s = f` %%s;
+infix 9 ` ; fun f` x = %%:"Rep_CFun" $ f $ x;
+infix 9 `% ; fun f`% s = f` %: s;
+infix 9 `%%; fun f`%%s = f` %%:s;
fun mk_cRep_CFun (F,As) = foldl (op `) (F,As);
-fun con_app2 con f args = mk_cRep_CFun(%%con,map f args);
+fun con_app2 con f args = mk_cRep_CFun(%%:con,map f args);
fun con_app con = con_app2 con %#;
fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y;
fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
@@ -158,21 +158,21 @@
| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to
avoid type varaibles *)
-fun proj x = prj (fn S => K(%%"fst" $S)) (fn S => K(%%"snd" $S)) x;
-fun cproj x = prj (fn S => K(%%"cfst"`S)) (fn S => K(%%"csnd"`S)) x;
+fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
+fun cproj x = prj (fn S => K(%%:"cfst"`S)) (fn S => K(%%:"csnd"`S)) x;
fun cproj' T eqs = prj
(fn S => fn t => Const("cfst",mk_prodT(dummyT,t)->>dummyT)`S)
(fn S => fn t => Const("csnd",mk_prodT(t,dummyT)->>dummyT)`S)
T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
-fun /\ v T = %%"Abs_CFun" $ mk_lam(v,T);
+fun /\ v T = %%:"Abs_CFun" $ mk_lam(v,T);
fun /\# (arg,T) = /\ (vname arg) T;
-infixr 9 oo; fun S oo T = %%"cfcomp"`S`T;
-val UU = %%"UU";
+infixr 9 oo; fun S oo T = %%:"cfcomp"`S`T;
+val UU = %%:"UU";
fun strict f = f`UU === UU;
fun defined t = t ~= UU;
-fun cpair (S,T) = %%"cpair"`S`T;
+fun cpair (S,T) = %%:"cpair"`S`T;
fun lift_defined f = lift (fn x => defined (f x));
fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
@@ -192,14 +192,14 @@
fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n))
| one_fun n (_,args) = let
val l2 = length args;
- fun idxs m arg = (if is_lazy arg then fn x=> %%"fup"`%%"ID"`x
+ fun idxs m arg = (if is_lazy arg then fn x=> %%:"fup"`%%"ID"`x
else Id) (Bound(l2-m));
in cont_eta_contract (foldr''
- (fn (a,t) => %%"ssplit"`(/\# (a,t)))
+ (fn (a,t) => %%:"ssplit"`(/\# (a,t)))
(args,
fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
) end;
in (if length cons = 1 andalso length(snd(hd cons)) <= 1
- then fn t => %%"strictify"`t else Id)
- (foldr' (fn (x,y)=> %%"sscase"`x`y) (mapn one_fun 1 cons)) end;
+ then fn t => %%:"strictify"`t else Id)
+ (foldr' (fn (x,y)=> %%:"sscase"`x`y) (mapn one_fun 1 cons)) end;
end; (* struct *)
--- a/src/HOLCF/domain/theorems.ML Fri Aug 31 16:25:53 2001 +0200
+++ b/src/HOLCF/domain/theorems.ML Fri Aug 31 16:26:55 2001 +0200
@@ -80,31 +80,31 @@
(* ----- theorems concerning the isomorphism -------------------------------- *)
-val dc_abs = %%(dname^"_abs");
-val dc_rep = %%(dname^"_rep");
-val dc_copy = %%(dname^"_copy");
+val dc_abs = %%:(dname^"_abs");
+val dc_rep = %%:(dname^"_rep");
+val dc_copy = %%:(dname^"_copy");
val x_name = "x";
val (rep_strict, abs_strict) = let
val r = ax_rep_iso RS (ax_abs_iso RS (allI RSN(2,allI RS iso_strict)))
in (r RS conjunct1, r RS conjunct2) end;
-val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%x_name === UU)) [
+val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%:x_name === UU)) [
res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
etac ssubst 1, rtac rep_strict 1];
-val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%x_name === UU)) [
+val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%:x_name === UU)) [
res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
etac ssubst 1, rtac abs_strict 1];
val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
local
-val iso_swap = pg [] (dc_rep`%"x" === %"y" ==> %"x" === dc_abs`%"y") [
+val iso_swap = pg [] (dc_rep`%"x" === %:"y" ==> %:"x" === dc_abs`%"y") [
dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
etac (ax_rep_iso RS subst) 1];
fun exh foldr1 cn quant foldr2 var = let
fun one_con (con,args) = let val vns = map vname args in
- foldr quant (vns, foldr2 ((%x_name === con_app2 con (var vns) vns)::
+ foldr quant (vns, foldr2 ((%:x_name === con_app2 con (var vns) vns)::
map (defined o (var vns)) (nonlazy args))) end
- in foldr1 ((cn(%x_name===UU))::map one_con cons) end;
+ in foldr1 ((cn(%:x_name===UU))::map one_con cons) end;
in
val casedist = let
fun common_tac thm = rtac thm 1 THEN contr_tac 1;
@@ -131,10 +131,10 @@
prod_tac args THEN sum_rest_tac p) THEN
sum_tac cons' prems
| sum_tac _ _ = Imposs "theorems:sum_tac";
- in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
- (fn T => T ==> %"P") mk_All
+ in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%:"P")))
+ (fn T => T ==> %:"P") mk_All
(fn l => foldr (op ===>) (map mk_trp l,
- mk_trp(%"P")))
+ mk_trp(%:"P")))
bound_arg)
(fn prems => [
cut_facts_tac [excluded_middle] 1,
@@ -148,7 +148,7 @@
rewrite_goals_tac axs_con_def THEN
simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
else sum_tac cons (tl prems)])end;
-val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
+val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %:)))[
rtac casedist 1,
DETERM_UNTIL_SOLVED(fast_tac HOL_cs 1)];
end;
@@ -156,7 +156,7 @@
local
fun bind_fun t = foldr mk_All (when_funs cons,t);
fun bound_fun i _ = Bound (length cons - i);
- val when_app = foldl (op `) (%%(dname^"_when"), mapn bound_fun 1 cons);
+ val when_app = foldl (op `) (%%:(dname^"_when"), mapn bound_fun 1 cons);
val when_appl = pg [ax_when_def] (bind_fun(mk_trp(when_app`%x_name ===
when_body cons (fn (m,n)=> bound_fun (n-m) 0)`(dc_rep`%x_name))))[
simp_tac HOLCF_ss 1];
@@ -164,7 +164,7 @@
val when_strict = pg [] (bind_fun(mk_trp(strict when_app))) [
simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
val when_apps = let fun one_when n (con,args) = pg axs_con_def
- (bind_fun (lift_defined % (nonlazy args,
+ (bind_fun (lift_defined %: (nonlazy args,
mk_trp(when_app`(con_app con args) ===
mk_cRep_CFun(bound_fun n 0,map %# args)))))[
asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
@@ -176,16 +176,16 @@
val dis_rews = let
val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp(
- strict(%%(dis_name con)))) [
+ strict(%%:(dis_name con)))) [
simp_tac (HOLCF_ss addsimps when_rews) 1]) cons;
val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def
- (lift_defined % (nonlazy args,
- (mk_trp((%%(dis_name c))`(con_app con args) ===
- %%(if con=c then "TT" else "FF"))))) [
+ (lift_defined %: (nonlazy args,
+ (mk_trp((%%:(dis_name c))`(con_app con args) ===
+ %%:(if con=c then "TT" else "FF"))))) [
asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
- val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==>
- defined(%%(dis_name con)`%x_name)) [
+ val dis_defins = map (fn (con,args) => pg [] (defined(%:x_name) ==>
+ defined(%%:(dis_name con)`%x_name)) [
rtac casedist 1,
contr_tac 1,
DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac
@@ -199,23 +199,23 @@
asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
) (nonlazy args)) cons);
val con_defins = map (fn (con,args) => pg []
- (lift_defined % (nonlazy args,
+ (lift_defined %: (nonlazy args,
mk_trp(defined(con_app con args)))) ([
rtac rev_contrapos 1,
eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
val con_rews = con_stricts @ con_defins;
-val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%sel))) [
+val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%:sel))) [
simp_tac (HOLCF_ss addsimps when_rews) 1];
in flat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end;
val sel_apps = let fun one_sel c n sel = map (fn (con,args) =>
let val nlas = nonlazy args;
val vns = map vname args;
- in pg axs_sel_def (lift_defined %
+ in pg axs_sel_def (lift_defined %:
(filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
- mk_trp((%%sel)`(con_app con args) ===
- (if con=c then %(nth_elem(n,vns)) else UU))))
+ mk_trp((%%:sel)`(con_app con args) ===
+ (if con=c then %:(nth_elem(n,vns)) else UU))))
( (if con=c then []
else map(case_UU_tac(when_rews@con_stricts)1) nlas)
@(if con=c andalso ((nth_elem(n,vns)) mem nlas)
@@ -224,8 +224,8 @@
@ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
in flat(map (fn (c,args) =>
flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
-val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==>
- defined(%%(sel_of arg)`%x_name)) [
+val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%:x_name)==>
+ defined(%%:(sel_of arg)`%x_name)) [
rtac casedist 1,
contr_tac 1,
DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac
@@ -235,7 +235,7 @@
val distincts_le = let
fun dist (con1, args1) (con2, args2) = pg []
- (lift_defined % ((nonlazy args1),
+ (lift_defined %: ((nonlazy args1),
(mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
rtac rev_contrapos 1,
eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
@@ -270,7 +270,7 @@
fun append s = upd_vname(fn v => v^s);
val (largs,rargs) = (args, map (append "'") args);
in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
- lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
+ lift_defined %: ((nonlazy largs),lift_defined %: ((nonlazy rargs),
mk_trp (foldr' mk_conj
(ListPair.map rel
(map %# largs, map %# rargs)))))) end;
@@ -298,9 +298,9 @@
asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
cfst_strict,csnd_strict]) 1];
val copy_apps = map (fn (con,args) => pg [ax_copy_def]
- (lift_defined % (nonlazy_rec args,
+ (lift_defined %: (nonlazy_rec args,
mk_trp(dc_copy`%"f"`(con_app con args) ===
- (con_app2 con (app_rec_arg (cproj (%"f") 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)
@@ -356,7 +356,7 @@
val copy_rews = flat (map (gts "copy_rews") dnames);
end; (* local *)
-fun dc_take dn = %%(dn^"_take");
+fun dc_take dn = %%:(dn^"_take");
val x_name = idx_name dnames "x";
val P_name = idx_name dnames "P";
val n_eqs = length eqs;
@@ -369,19 +369,19 @@
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
- strict(dc_take dn $ %"n")) eqs))) ([
+ strict(dc_take dn $ %:"n")) eqs))) ([
nat_ind_tac "n" 1,
simp_tac iterate_Cprod_ss 1,
asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
val take_stricts' = rewrite_rule copy_take_defs take_stricts;
- val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0")
+ val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%:"0")
`%x_name n === UU))[
simp_tac iterate_Cprod_ss 1]) 1 dnames;
val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj
(flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all
- (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
- con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
+ (map vname args,(dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args) ===
+ con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %:"n"))
args)) cons) eqs)))) ([
simp_tac iterate_Cprod_ss 1,
nat_ind_tac "n" 1,
@@ -401,9 +401,9 @@
local
fun one_con p (con,args) = foldr mk_All (map vname args,
lift_defined (bound_arg (map vname args)) (nonlazy args,
- lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
- (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args))));
- fun one_eq ((p,cons),concl) = (mk_trp(%p $ UU) ===>
+ lift (fn arg => %:(P_name (1+rec_of arg)) $ bound_arg args arg)
+ (filter is_rec args,mk_trp(%:p $ con_app2 con (bound_arg args) args))));
+ fun one_eq ((p,cons),concl) = (mk_trp(%:p $ UU) ===>
foldr (op ===>) (map (one_con p) cons,concl));
fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss,
mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
@@ -437,8 +437,8 @@
val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
end;
in (* local *)
-val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$
- (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [
+val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %:(P_name n)$
+ (dc_take dn $ %:"n" `%(x_name n)))) (fn prems => [
quant_tac 1,
simp_tac HOL_ss 1,
nat_ind_tac "n" 1,
@@ -462,7 +462,7 @@
val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n",
mk_trp(dc_take dn $ Bound 0 `%(x_name n) ===
dc_take dn $ Bound 0 `%(x_name n^"'")))
- ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
+ ===> mk_trp(%:(x_name n) === %:(x_name n^"'"))) (fn prems => [
res_inst_tac[("t",x_name n )](ax_reach RS subst) 1,
res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
stac fix_def2 1,
@@ -479,9 +479,9 @@
val (finites,ind) = if is_finite then
let
- fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x");
- val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===>
- mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
+ fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
+ val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%:"x")) ===>
+ mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %:"x" === UU),
take_enough dn)) ===> mk_trp(take_enough dn)) [
etac disjE 1,
etac notE 1,
@@ -512,7 +512,7 @@
cons))
1 (conss~~cases)));
val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp(
- %%(dn^"_finite") $ %"x"))[
+ %%:(dn^"_finite") $ %:"x"))[
case_UU_tac take_rews 1 "x",
eresolve_tac finite_lemmas1a 1,
step_tac HOL_cs 1,
@@ -521,7 +521,7 @@
fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
in
(finites,
- pg'' thy[](ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))(fn prems =>
+ pg'' thy[](ind_term (fn n => fn dn => %:(P_name n) $ %:(x_name n)))(fn prems =>
TRY(safe_tac HOL_cs) ::
flat (map (fn (finite,fin_ind) => [
rtac(rewrite_rule axs_finite_def finite RS exE)1,
@@ -532,8 +532,8 @@
) end (* let *) else
(mapn (fn n => fn dn => read_instantiate_sg (sign_of thy)
[("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
- pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%"adm" $ %(P_name n))))
- 1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n))))
+ pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%:"adm" $ %:(P_name n))))
+ 1 dnames, ind_term (fn n => fn dn => %:(P_name n) $ %:(x_name n))))
(fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1)
axs_reach @ [
quant_tac 1,
@@ -555,13 +555,13 @@
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 => K("fst("^s^")")) (fn s => K("snd("^s^")"));
- val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
+ 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") 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 ===
- (dc_take dn $ %"n" `bnd_arg n 1)))0 dnames))))))
+ (dc_take dn $ %:"n" `bnd_arg n 0 ===
+ (dc_take dn $ %:"n" `bnd_arg n 1)))0 dnames))))))
([ rtac impI 1,
nat_ind_tac "n" 1,
simp_tac take_ss 1,
@@ -575,10 +575,10 @@
REPEAT(CHANGED(asm_simp_tac take_ss 1))])
0 xs));
in
-val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===>
+val coind = pg [] (mk_trp(%%:(comp_dname^"_bisim") $ %:"R") ===>
foldr (op ===>) (mapn (fn n => fn x =>
- mk_trp(proj (%"R") eqs n $ %x $ %(x^"'"))) 0 xs,
- mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) 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 => [
rtac take_lemma 1,