--- a/src/ZF/Resid/Confluence.thy Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Confluence.thy Mon May 21 14:51:46 2001 +0200
@@ -13,9 +13,9 @@
defs
confluence_def "confluence(R) ==
- ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->
- (EX u.<y,u>:R & <z,u>:R))"
- strip_def "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->
- (EX u.(y =1=> u) & (z===>u)))"
+ \\<forall>x y. <x,y>:R --> (\\<forall>z.<x,z>:R -->
+ (\\<exists>u.<y,u>:R & <z,u>:R))"
+ strip_def "strip == \\<forall>x y. (x ===> y) --> (\\<forall>z.(x =1=> z) -->
+ (\\<exists>u.(y =1=> u) & (z===>u)))"
end
--- a/src/ZF/Resid/Conversion.ML Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Conversion.ML Mon May 21 14:51:46 2001 +0200
@@ -19,7 +19,7 @@
(* Church_Rosser Theorem *)
(* ------------------------------------------------------------------------- *)
-Goal "m<--->n ==> EX p.(m --->p) & (n ---> p)";
+Goal "m<--->n ==> \\<exists>p.(m --->p) & (n ---> p)";
by (etac Sconv.induct 1);
by (etac Sconv1.induct 1);
by (blast_tac (claset() addIs [red1D1,redD2]) 1);
--- a/src/ZF/Resid/Conversion.thy Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Conversion.thy Mon May 21 14:51:46 2001 +0200
@@ -29,7 +29,7 @@
domains "Sconv" <= "lambda*lambda"
intrs
one_step "m<-1->n ==> m<--->n"
- refl "m:lambda ==> m<--->m"
+ refl "m \\<in> lambda ==> m<--->m"
trans "[|m<--->n; n<--->p|] ==> m<--->p"
type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
end
--- a/src/ZF/Resid/Cube.ML Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Cube.ML Mon May 21 14:51:46 2001 +0200
@@ -15,7 +15,7 @@
(* Having more assumptions than needed -- removed below *)
Goal "v<==u ==> \
-\ regular(u) --> (ALL w. w~v --> w~u --> \
+\ regular(u) --> (\\<forall>w. w~v --> w~u --> \
\ w |> u = (w|>v) |> (u|>v))";
by (etac Ssub.induct 1);
by Auto_tac;
@@ -56,7 +56,7 @@
(* ------------------------------------------------------------------------- *)
Goal "[|w~u; w~v; regular(u); regular(v)|]==> \
-\ EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
+\ \\<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
\ regular(vu) & (w|>v)~uv & regular(uv) ";
by (subgoal_tac "u~v" 1);
by (safe_tac (claset() addSIs [exI]));
--- a/src/ZF/Resid/Redex.ML Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Redex.ML Mon May 21 14:51:46 2001 +0200
@@ -21,15 +21,15 @@
(* Equality rules for union *)
(* ------------------------------------------------------------------------- *)
-Goal "n:nat==>Var(n) un Var(n)=Var(n)";
+Goal "n \\<in> nat==>Var(n) un Var(n)=Var(n)";
by (asm_simp_tac (simpset() addsimps [union_def]) 1);
qed "union_Var";
-Goal "[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
+Goal "[|u \\<in> redexes; v \\<in> redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
by (asm_simp_tac (simpset() addsimps [union_def]) 1);
qed "union_Fun";
-Goal "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
+Goal "[|b1 \\<in> bool; b2 \\<in> bool; u1 \\<in> redexes; v1 \\<in> redexes; u2 \\<in> redexes; v2 \\<in> redexes|]==> \
\ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
by (asm_simp_tac (simpset() addsimps [union_def]) 1);
qed "union_App";
@@ -58,7 +58,7 @@
(* comp proofs *)
(* ------------------------------------------------------------------------- *)
-Goal "u:redexes ==> u ~ u";
+Goal "u \\<in> redexes ==> u ~ u";
by (etac redexes.induct 1);
by (ALLGOALS Fast_tac);
qed "comp_refl";
@@ -73,7 +73,7 @@
qed "comp_sym_iff";
-Goal "u ~ v ==> ALL w. v ~ w-->u ~ w";
+Goal "u ~ v ==> \\<forall>w. v ~ w-->u ~ w";
by (etac Scomp.induct 1);
by (ALLGOALS Fast_tac);
qed_spec_mp "comp_trans";
--- a/src/ZF/Resid/Redex.thy Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Redex.thy Mon May 21 14:51:46 2001 +0200
@@ -10,9 +10,9 @@
redexes :: i
datatype
- "redexes" = Var ("n: nat")
- | Fun ("t: redexes")
- | App ("b:bool" ,"f:redexes" , "a:redexes")
+ "redexes" = Var ("n \\<in> nat")
+ | Fun ("t \\<in> redexes")
+ | App ("b \\<in> bool" ,"f \\<in> redexes" , "a \\<in> redexes")
consts
@@ -25,19 +25,19 @@
translations
"a<==b" == "<a,b>:Ssub"
"a ~ b" == "<a,b>:Scomp"
- "regular(a)" == "a:Sreg"
+ "regular(a)" == "a \\<in> Sreg"
primrec (*explicit lambda is required because both arguments of "un" vary*)
"union_aux(Var(n)) =
- (lam t:redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
+ (\\<lambda>t \\<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
"union_aux(Fun(u)) =
- (lam t:redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
+ (\\<lambda>t \\<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
%b y z. 0, t))"
"union_aux(App(b,f,a)) =
- (lam t:redexes.
+ (\\<lambda>t \\<in> redexes.
redexes_case(%j. 0, %y. 0,
%c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
@@ -48,9 +48,9 @@
inductive
domains "Ssub" <= "redexes*redexes"
intrs
- Sub_Var "n:nat ==> Var(n)<== Var(n)"
+ Sub_Var "n \\<in> nat ==> Var(n)<== Var(n)"
Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
- Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
+ Sub_App1 "[|u1<== v1; u2<== v2; b \\<in> bool|]==>
App(0,u1,u2)<== App(b,v1,v2)"
Sub_App2 "[|u1<== v1; u2<== v2|]==>
App(1,u1,u2)<== App(1,v1,v2)"
@@ -59,16 +59,16 @@
inductive
domains "Scomp" <= "redexes*redexes"
intrs
- Comp_Var "n:nat ==> Var(n) ~ Var(n)"
+ Comp_Var "n \\<in> nat ==> Var(n) ~ Var(n)"
Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
- Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
+ Comp_App "[|u1 ~ v1; u2 ~ v2; b1 \\<in> bool; b2 \\<in> bool|]==>
App(b1,u1,u2) ~ App(b2,v1,v2)"
type_intrs "redexes.intrs@bool_typechecks"
inductive
domains "Sreg" <= "redexes"
intrs
- Reg_Var "n:nat ==> regular(Var(n))"
+ Reg_Var "n \\<in> nat ==> regular(Var(n))"
Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
Reg_App1 "[|regular(Fun(u)); regular(v)
|]==>regular(App(1,Fun(u),v))"
--- a/src/ZF/Resid/Reduction.ML Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Reduction.ML Mon May 21 14:51:46 2001 +0200
@@ -39,13 +39,13 @@
by (ALLGOALS (Asm_simp_tac ));
qed "red_Fun";
-Goal "[|n:lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
+Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
by (etac Sred.induct 1);
by (resolve_tac [Sred.trans] 3);
by (ALLGOALS (Asm_simp_tac ));
qed "red_Apll";
-Goal "[|n:lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
+Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
by (etac Sred.induct 1);
by (resolve_tac [Sred.trans] 3);
by (ALLGOALS (Asm_simp_tac ));
@@ -56,7 +56,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apll,red_Aplr]) ));
qed "red_Apl";
-Goal "[|m:lambda; m':lambda; n:lambda; n':lambda; m ---> m'; n--->n'|]==> \
+Goal "[|m \\<in> lambda; m':lambda; n \\<in> lambda; n':lambda; m ---> m'; n--->n'|]==> \
\ Apl(Fun(m),n)---> n'/m'";
by (res_inst_tac [("n","Apl(Fun(m'),n')")] Sred.trans 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apl,red_Fun]) ));
@@ -68,7 +68,7 @@
(* ------------------------------------------------------------------------- *)
-Goal "m:lambda==> m =1=> m";
+Goal "m \\<in> lambda==> m =1=> m";
by (etac lambda.induct 1);
by (ALLGOALS (Asm_simp_tac ));
qed "refl_par_red1";
@@ -96,7 +96,7 @@
(* Simulation *)
(* ------------------------------------------------------------------------- *)
-Goal "m=1=>n ==> EX v. m|>v = n & m~v & regular(v)";
+Goal "m=1=>n ==> \\<exists>v. m|>v = n & m~v & regular(v)";
by (etac Spar_red1.induct 1);
by Safe_tac;
by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
@@ -109,12 +109,12 @@
(* commuting of unmark and subst *)
(* ------------------------------------------------------------------------- *)
-Goal "u:redexes ==> ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
+Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
by (etac redexes.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
qed "unmmark_lift_rec";
-Goal "v:redexes ==> ALL k:nat. ALL u:redexes. \
+Goal "v \\<in> redexes ==> \\<forall>k \\<in> nat. \\<forall>u \\<in> redexes. \
\ unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
by (etac redexes.induct 1);
by (ALLGOALS (asm_simp_tac
@@ -134,7 +134,7 @@
by Auto_tac;
qed_spec_mp "completeness_l";
-Goal "[|u:lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
+Goal "[|u \\<in> lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
by (dtac completeness_l 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lambda_unmark]) ));
qed "completeness";
--- a/src/ZF/Resid/Reduction.thy Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Reduction.thy Mon May 21 14:51:46 2001 +0200
@@ -21,11 +21,11 @@
inductive
domains "Sred1" <= "lambda*lambda"
intrs
- beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
+ beta "[|m \\<in> lambda; n \\<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
- apl_l "[|m2:lambda; m1 -1-> n1|] ==>
+ apl_l "[|m2 \\<in> lambda; m1 -1-> n1|] ==>
Apl(m1,m2) -1-> Apl(n1,m2)"
- apl_r "[|m1:lambda; m2 -1-> n2|] ==>
+ apl_r "[|m1 \\<in> lambda; m2 -1-> n2|] ==>
Apl(m1,m2) -1-> Apl(m1,n2)"
type_intrs "red_typechecks"
@@ -33,7 +33,7 @@
domains "Sred" <= "lambda*lambda"
intrs
one_step "[|m-1->n|] ==> m--->n"
- refl "m:lambda==>m --->m"
+ refl "m \\<in> lambda==>m --->m"
trans "[|m--->n; n--->p|]==>m--->p"
type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks"
@@ -42,7 +42,7 @@
intrs
beta "[|m =1=> m';
n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
- rvar "n:nat==> Var(n) =1=> Var(n)"
+ rvar "n \\<in> nat==> Var(n) =1=> Var(n)"
rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
rapl "[|m =1=> m';
n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
--- a/src/ZF/Resid/Residuals.ML Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Residuals.ML Mon May 21 14:51:46 2001 +0200
@@ -41,12 +41,12 @@
(* residuals is a partial function *)
(* ------------------------------------------------------------------------- *)
-Goal "residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w";
+Goal "residuals(u,v,w) ==> \\<forall>w1. residuals(u,v,w1) --> w1 = w";
by (etac Sres.induct 1);
by (ALLGOALS Force_tac);
qed_spec_mp "residuals_function";
-Goal "u~v ==> regular(v) --> (EX w. residuals(u,v,w))";
+Goal "u~v ==> regular(v) --> (\\<exists>w. residuals(u,v,w))";
by (etac Scomp.induct 1);
by (ALLGOALS Fast_tac);
qed "residuals_intro";
@@ -62,7 +62,7 @@
(* Residual function *)
(* ------------------------------------------------------------------------- *)
-Goalw [res_func_def] "n:nat ==> Var(n) |> Var(n) = Var(n)";
+Goalw [res_func_def] "n \\<in> nat ==> Var(n) |> Var(n) = Var(n)";
by (Blast_tac 1);
qed "res_Var";
@@ -73,25 +73,25 @@
qed "res_Fun";
Goalw [res_func_def]
- "[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
+ "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
\ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)";
by (blast_tac (claset() addSDs [comp_resfuncD]
addIs [residuals_function]) 1);
qed "res_App";
Goalw [res_func_def]
- "[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
+ "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
\ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
by (blast_tac (claset() addSEs redexes.free_SEs
addSDs [comp_resfuncD]
addIs [residuals_function]) 1);
qed "res_redex";
-Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
+Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t \\<in> redexes";
by (etac Scomp.induct 1);
by (auto_tac (claset(),
simpset() addsimps [res_Var,res_Fun,res_App,res_redex]));
-by (dres_inst_tac [("psi", "Fun(?u) |> ?v : redexes")] asm_rl 1);
+by (dres_inst_tac [("psi", "Fun(?u) |> ?v \\<in> redexes")] asm_rl 1);
by (auto_tac (claset(),
simpset() addsimps [res_Fun]));
qed "resfunc_type";
@@ -115,7 +115,7 @@
by Auto_tac;
qed_spec_mp "sub_preserve_reg";
-Goal "[|u~v; k:nat|]==> regular(v)--> (ALL n:nat. \
+Goal "[|u~v; k \\<in> nat|]==> regular(v)--> (\\<forall>n \\<in> nat. \
\ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))";
by (etac Scomp.induct 1);
by Safe_tac;
@@ -126,15 +126,15 @@
by (Asm_full_simp_tac 1);
qed "residuals_lift_rec";
-Goal "u1~u2 ==> ALL v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
-\ (ALL n:nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
+Goal "u1~u2 ==> \\<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
+\ (\\<forall>n \\<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
\ subst_rec(v1 |> v2, u1 |> u2,n))";
by (etac Scomp.induct 1);
by Safe_tac;
by (ALLGOALS
(asm_simp_tac
(simpset() addsimps [lift_rec_Var,subst_Var,residuals_lift_rec])));
-by (dres_inst_tac [("psi", "ALL x.?P(x)")] asm_rl 1);
+by (dres_inst_tac [("psi", "\\<forall>x.?P(x)")] asm_rl 1);
by (asm_full_simp_tac (simpset() addsimps [substitution]) 1);
qed "residuals_subst_rec";
@@ -148,7 +148,7 @@
(* Residuals are comp and regular *)
(* ------------------------------------------------------------------------- *)
-Goal "u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
+Goal "u~v ==> \\<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
by (etac Scomp.induct 1);
by (ALLGOALS Force_tac);
qed_spec_mp "residuals_preserve_comp";
--- a/src/ZF/Resid/Residuals.thy Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Residuals.thy Mon May 21 14:51:46 2001 +0200
@@ -19,14 +19,14 @@
inductive
domains "Sres" <= "redexes*redexes*redexes"
intrs
- Res_Var "n:nat ==> residuals(Var(n),Var(n),Var(n))"
+ Res_Var "n \\<in> nat ==> residuals(Var(n),Var(n),Var(n))"
Res_Fun "[|residuals(u,v,w)|]==>
residuals(Fun(u),Fun(v),Fun(w))"
Res_App "[|residuals(u1,v1,w1);
- residuals(u2,v2,w2); b:bool|]==>
+ residuals(u2,v2,w2); b \\<in> bool|]==>
residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
Res_redex "[|residuals(u1,v1,w1);
- residuals(u2,v2,w2); b:bool|]==>
+ residuals(u2,v2,w2); b \\<in> bool|]==>
residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
--- a/src/ZF/Resid/Substitution.ML Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Substitution.ML Mon May 21 14:51:46 2001 +0200
@@ -9,23 +9,23 @@
(* Arithmetic extensions *)
(* ------------------------------------------------------------------------- *)
-Goal "[| p < n; n:nat|] ==> n~=p";
+Goal "[| p < n; n \\<in> nat|] ==> n\\<noteq>p";
by (Fast_tac 1);
qed "gt_not_eq";
-Goal "[|j:nat; i:nat|] ==> i < j --> succ(j #- 1) = j";
+Goal "[|j \\<in> nat; i \\<in> nat|] ==> i < j --> succ(j #- 1) = j";
by (induct_tac "j" 1);
by (Fast_tac 1);
by (Asm_simp_tac 1);
qed "succ_pred";
-Goal "[|succ(x)<n; n:nat; x:nat|] ==> x < n #- 1 ";
+Goal "[|succ(x)<n; n \\<in> nat; x \\<in> nat|] ==> x < n #- 1 ";
by (rtac succ_leE 1);
by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
qed "lt_pred";
-Goal "[|n < succ(x); p<n; p:nat; n:nat; x:nat|] ==> n #- 1 < x ";
+Goal "[|n < succ(x); p<n; p \\<in> nat; n \\<in> nat; x \\<in> nat|] ==> n #- 1 < x ";
by (rtac succ_leE 1);
by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
qed "gt_pred";
@@ -37,25 +37,25 @@
(* ------------------------------------------------------------------------- *)
(* lift_rec equality rules *)
(* ------------------------------------------------------------------------- *)
-Goal "[|n:nat; i:nat|] \
+Goal "[|n \\<in> nat; i \\<in> nat|] \
\ ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_Var";
-Goal "[|n:nat; i:nat; k:nat; k le i|] ==> lift_rec(Var(i),k) = Var(succ(i))";
+Goal "[|n \\<in> nat; i \\<in> nat; k \\<in> nat; k le i|] ==> lift_rec(Var(i),k) = Var(succ(i))";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_le";
-Goal "[|i:nat; k:nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)";
+Goal "[|i \\<in> nat; k \\<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_gt";
-Goal "[|n:nat; k:nat|] ==> \
+Goal "[|n \\<in> nat; k \\<in> nat|] ==> \
\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_Fun";
-Goal "[|n:nat; k:nat|] ==> \
+Goal "[|n \\<in> nat; k \\<in> nat|] ==> \
\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
qed "lift_rec_App";
@@ -65,32 +65,32 @@
(* substitution quality rules *)
(* ------------------------------------------------------------------------- *)
-Goal "[|i:nat; k:nat; u:redexes|] \
+Goal "[|i \\<in> nat; k \\<in> nat; u \\<in> redexes|] \
\ ==> subst_rec(u,Var(i),k) = \
\ (if k<i then Var(i #- 1) else if k=i then u else Var(i))";
by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
qed "subst_Var";
-Goal "[|n:nat; u:redexes|] ==> subst_rec(u,Var(n),n) = u";
+Goal "[|n \\<in> nat; u \\<in> redexes|] ==> subst_rec(u,Var(n),n) = u";
by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_eq";
-Goal "[|n:nat; u:redexes; p:nat; p<n|] ==> \
+Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; p<n|] ==> \
\ subst_rec(u,Var(n),p) = Var(n #- 1)";
by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_gt";
-Goal "[|n:nat; u:redexes; p:nat; n<p|] ==> \
+Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; n<p|] ==> \
\ subst_rec(u,Var(n),p) = Var(n)";
by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
qed "subst_lt";
-Goal "[|p:nat; u:redexes|] ==> \
+Goal "[|p \\<in> nat; u \\<in> redexes|] ==> \
\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_Fun";
-Goal "[|p:nat; u:redexes|] ==> \
+Goal "[|p \\<in> nat; u \\<in> redexes|] ==> \
\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
qed "subst_App";
@@ -99,14 +99,14 @@
Addsimps [subst_Fun, subst_App];
-Goal "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
+Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. lift_rec(u,k):redexes";
by (etac redexes.induct 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [lift_rec_Var,
lift_rec_Fun, lift_rec_App])));
qed_spec_mp "lift_rec_type";
-Goal "v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
+Goal "v \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. subst_rec(u,v,n):redexes";
by (etac redexes.induct 1);
by (ALLGOALS(asm_simp_tac
(simpset() addsimps [subst_Var, lift_rec_type])));
@@ -122,7 +122,7 @@
(* lift and substitution proofs *)
(* ------------------------------------------------------------------------- *)
-Goal "u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \
+Goal "u \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>i \\<in> nat. i le n --> \
\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
by (etac redexes.induct 1);
by (ALLGOALS Asm_simp_tac);
@@ -132,13 +132,13 @@
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
qed "lift_lift_rec";
-Goal "[|u:redexes; n:nat|] ==> \
+Goal "[|u \\<in> redexes; n \\<in> nat|] ==> \
\ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1);
qed "lift_lift";
-Goal "v:redexes ==> \
-\ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\
+Goal "v \\<in> redexes ==> \
+\ \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. n le m-->\
\ lift_rec(subst_rec(u,v,n),m) = \
\ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
by ((etac redexes.induct 1)
@@ -157,14 +157,14 @@
by (asm_simp_tac (simpset() addsimps [leI]) 1);
qed "lift_rec_subst_rec";
-Goal "[|v:redexes; u:redexes; n:nat|] ==> \
+Goal "[|v \\<in> redexes; u \\<in> redexes; n \\<in> nat|] ==> \
\ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
qed "lift_subst";
-Goal "v:redexes ==> \
-\ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\
+Goal "v \\<in> redexes ==> \
+\ \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. m le n-->\
\ lift_rec(subst_rec(u,v,n),m) = \
\ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
by (etac redexes.induct 1
@@ -183,16 +183,16 @@
qed "lift_rec_subst_rec_lt";
-Goal "u:redexes ==> \
-\ ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) = u";
+Goal "u \\<in> redexes ==> \
+\ \\<forall>n \\<in> nat. \\<forall>v \\<in> redexes. subst_rec(v,lift_rec(u,n),n) = u";
by (etac redexes.induct 1);
by Auto_tac;
by (case_tac "n < x" 1);
by Auto_tac;
qed "subst_rec_lift_rec";
-Goal "v:redexes ==> \
-\ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \
+Goal "v \\<in> redexes ==> \
+\ \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. \\<forall>w \\<in> redexes. m le n --> \
\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
\ subst_rec(w,subst_rec(u,v,m),n)";
by (etac redexes.induct 1);
@@ -220,7 +220,7 @@
qed "subst_rec_subst_rec";
-Goal "[|v:redexes; u:redexes; w:redexes; n:nat|] ==> \
+Goal "[|v \\<in> redexes; u \\<in> redexes; w \\<in> redexes; n \\<in> nat|] ==> \
\ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)";
by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1);
qed "substitution";
@@ -231,12 +231,12 @@
(* ------------------------------------------------------------------------- *)
-Goal "[|n:nat; u ~ v|] ==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)";
+Goal "[|n \\<in> nat; u ~ v|] ==> \\<forall>m \\<in> nat. lift_rec(u,m) ~ lift_rec(v,m)";
by (etac Scomp.induct 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl])));
qed "lift_rec_preserve_comp";
-Goal "u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\
+Goal "u2 ~ v2 ==> \\<forall>m \\<in> nat. \\<forall>u1 \\<in> redexes. \\<forall>v1 \\<in> redexes.\
\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
by (etac Scomp.induct 1);
by (ALLGOALS
@@ -244,13 +244,13 @@
(simpset() addsimps [subst_Var, lift_rec_preserve_comp, comp_refl])));
qed "subst_rec_preserve_comp";
-Goal "regular(u) ==> ALL m:nat. regular(lift_rec(u,m))";
+Goal "regular(u) ==> \\<forall>m \\<in> nat. regular(lift_rec(u,m))";
by (etac Sreg.induct 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var])));
qed "lift_rec_preserve_reg";
Goal "regular(v) ==> \
-\ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))";
+\ \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. regular(u)-->regular(subst_rec(u,v,m))";
by (etac Sreg.induct 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_Var,
lift_rec_preserve_reg])));
--- a/src/ZF/Resid/Substitution.thy Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Substitution.thy Mon May 21 14:51:46 2001 +0200
@@ -29,23 +29,23 @@
in the recursive calls ***)
primrec
- "lift_aux(Var(i)) = (lam k:nat. if i<k then Var(i) else Var(succ(i)))"
+ "lift_aux(Var(i)) = (\\<lambda>k \\<in> nat. if i<k then Var(i) else Var(succ(i)))"
- "lift_aux(Fun(t)) = (lam k:nat. Fun(lift_aux(t) ` succ(k)))"
+ "lift_aux(Fun(t)) = (\\<lambda>k \\<in> nat. Fun(lift_aux(t) ` succ(k)))"
- "lift_aux(App(b,f,a)) = (lam k:nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
+ "lift_aux(App(b,f,a)) = (\\<lambda>k \\<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
primrec
"subst_aux(Var(i)) =
- (lam r:redexes. lam k:nat. if k<i then Var(i #- 1)
+ (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. if k<i then Var(i #- 1)
else if k=i then r else Var(i))"
"subst_aux(Fun(t)) =
- (lam r:redexes. lam k:nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
+ (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
"subst_aux(App(b,f,a)) =
- (lam r:redexes. lam k:nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
+ (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
end
--- a/src/ZF/Resid/Terms.ML Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Terms.ML Mon May 21 14:51:46 2001 +0200
@@ -12,12 +12,12 @@
(* unmark lemmas *)
(* ------------------------------------------------------------------------- *)
-Goal "u:redexes ==> unmark(u):lambda";
+Goal "u \\<in> redexes ==> unmark(u):lambda";
by (etac redexes.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "unmark_type";
-Goal "u:lambda ==> unmark(u) = u";
+Goal "u \\<in> lambda ==> unmark(u) = u";
by (etac lambda.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "lambda_unmark";
@@ -27,12 +27,12 @@
(* lift and subst preserve lambda *)
(* ------------------------------------------------------------------------- *)
-Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
+Goal "v \\<in> lambda ==> \\<forall>k \\<in> nat. lift_rec(v,k):lambda";
by (etac lambda.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
qed_spec_mp "liftL_type";
-Goal "v:lambda ==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
+Goal "v \\<in> lambda ==> \\<forall>n \\<in> nat. \\<forall>u \\<in> lambda. subst_rec(u,v,n):lambda";
by (etac lambda.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
qed_spec_mp "substL_type";
--- a/src/ZF/Resid/Terms.thy Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Terms.thy Mon May 21 14:51:46 2001 +0200
@@ -18,9 +18,9 @@
inductive
domains "lambda" <= "redexes"
intrs
- Lambda_Var " n:nat ==> Var(n):lambda"
- Lambda_Fun " u:lambda ==> Fun(u):lambda"
- Lambda_App "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
+ Lambda_Var " n \\<in> nat ==> Var(n):lambda"
+ Lambda_Fun " u \\<in> lambda ==> Fun(u):lambda"
+ Lambda_App "[|u \\<in> lambda; v \\<in> lambda|]==> Apl(u,v):lambda"
type_intrs "redexes.intrs@bool_typechecks"
primrec