--- a/src/ZF/Resid/Substitution.ML Mon Jun 22 17:12:27 1998 +0200
+++ b/src/ZF/Resid/Substitution.ML Mon Jun 22 17:13:09 1998 +0200
@@ -42,28 +42,28 @@
(* ------------------------------------------------------------------------- *)
(* lift_rec equality rules *)
(* ------------------------------------------------------------------------- *)
-goalw Substitution.thy [lift_rec_def]
+Goalw [lift_rec_def]
"!!n.[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))";
by (Asm_full_simp_tac 1);
qed "lift_rec_Var";
-goalw Substitution.thy [lift_rec_def]
+Goalw [lift_rec_def]
"!!n.[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))";
by (Asm_full_simp_tac 1);
qed "lift_rec_le";
-goalw Substitution.thy [lift_rec_def]
+Goalw [lift_rec_def]
"!!n.[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)";
by (Asm_full_simp_tac 1);
qed "lift_rec_gt";
-goalw Substitution.thy [lift_rec_def]
+Goalw [lift_rec_def]
"!!n.[|n:nat; k:nat|]==> \
\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
by (Asm_full_simp_tac 1);
qed "lift_rec_Fun";
-goalw Substitution.thy [lift_rec_def]
+Goalw [lift_rec_def]
"!!n.[|n:nat; k:nat|]==> \
\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
by (Asm_full_simp_tac 1);
@@ -73,36 +73,36 @@
(* substitution quality rules *)
(* ------------------------------------------------------------------------- *)
-goalw Substitution.thy [subst_rec_def]
+Goalw [subst_rec_def]
"!!n.[|i:nat; k:nat; u:redexes|]==> \
\ subst_rec(u,Var(i),k) = if(k<i,Var(i#-1),if(k=i,u,Var(i)))";
by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
qed "subst_Var";
-goalw Substitution.thy [subst_rec_def]
+Goalw [subst_rec_def]
"!!n.[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u";
by (asm_full_simp_tac (simpset()) 1);
qed "subst_eq";
-goalw Substitution.thy [subst_rec_def]
+Goalw [subst_rec_def]
"!!n.[|n:nat; u:redexes; p:nat; p<n|]==> \
\ subst_rec(u,Var(n),p) = Var(n#-1)";
by (asm_full_simp_tac (simpset()) 1);
qed "subst_gt";
-goalw Substitution.thy [subst_rec_def]
+Goalw [subst_rec_def]
"!!n.[|n:nat; u:redexes; p:nat; n<p|]==> \
\ subst_rec(u,Var(n),p) = Var(n)";
by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
qed "subst_lt";
-goalw Substitution.thy [subst_rec_def]
+Goalw [subst_rec_def]
"!!n.[|p:nat; u:redexes|]==> \
\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
by (asm_full_simp_tac (simpset()) 1);
qed "subst_Fun";
-goalw Substitution.thy [subst_rec_def]
+Goalw [subst_rec_def]
"!!n.[|p:nat; u:redexes|]==> \
\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
by (asm_full_simp_tac (simpset()) 1);
@@ -112,7 +112,7 @@
addsimps [lift_rec_Var,subst_Var]);
-goal Substitution.thy
+Goal
"!!n. u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS(asm_full_simp_tac
@@ -120,7 +120,7 @@
qed "lift_rec_type_a";
val lift_rec_type = lift_rec_type_a RS bspec;
-goalw Substitution.thy []
+Goalw []
"!!n. v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS(asm_full_simp_tac
@@ -139,7 +139,7 @@
(* lift and substitution proofs *)
(* ------------------------------------------------------------------------- *)
-goalw Substitution.thy []
+Goalw []
"!!n. u:redexes ==> ALL n:nat. ALL i:nat. i le n --> \
\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
by ((eresolve_tac [redexes.induct] 1)
@@ -152,13 +152,13 @@
qed "lift_lift_rec";
-goalw Substitution.thy []
+Goalw []
"!!n.[|u:redexes; n: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 Substitution.thy
+Goal
"!!n. v:redexes ==> \
\ ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\
\ lift_rec(subst_rec(u,v,n),m) = \
@@ -178,14 +178,14 @@
by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
qed "lift_rec_subst_rec";
-goalw Substitution.thy []
+Goalw []
"!!n.[|v:redexes; u:redexes; n:nat|]==> \
\ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
by (asm_full_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
qed "lift_subst";
-goalw Substitution.thy []
+Goalw []
"!!n. v:redexes ==> \
\ ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\
\ lift_rec(subst_rec(u,v,n),m) = \
@@ -206,7 +206,7 @@
qed "lift_rec_subst_rec_lt";
-goalw Substitution.thy []
+Goalw []
"!!n. u:redexes ==> \
\ ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) = u";
by ((eresolve_tac [redexes.induct] 1)
@@ -218,7 +218,7 @@
by (asm_full_simp_tac (simpset()) 1);
qed "subst_rec_lift_rec";
-goal Substitution.thy
+Goal
"!!n. v:redexes ==> \
\ ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le n --> \
\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
@@ -249,7 +249,7 @@
qed "subst_rec_subst_rec";
-goalw Substitution.thy []
+Goalw []
"!!n.[|v:redexes; u:redexes; w:redexes; n: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);
@@ -261,13 +261,13 @@
(* ------------------------------------------------------------------------- *)
-goal Substitution.thy
+Goal
"!!n.[|n:nat; u ~ v|]==> ALL m: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 Substitution.thy
+Goal
"!!n. u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\
\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
by (etac Scomp.induct 1);
@@ -275,13 +275,13 @@
([lift_rec_preserve_comp,comp_refl]))));
qed "subst_rec_preserve_comp";
-goal Substitution.thy
+Goal
"!!n. regular(u) ==> ALL m:nat. regular(lift_rec(u,m))";
by (eresolve_tac [Sreg.induct] 1);
by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()))));
qed "lift_rec_preserve_reg";
-goal Substitution.thy
+Goal
"!!n. regular(v) ==> \
\ ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))";
by (eresolve_tac [Sreg.induct] 1);