Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Resid/Substitution.ML
changeset 5527 38928c4a8eb2
parent 5514 324e1560a5c9
child 6046 2c8a8be36c94 
--- a/src/ZF/Resid/Substitution.ML	Mon Sep 21 23:25:27 1998 +0200
+++ b/src/ZF/Resid/Substitution.ML	Tue Sep 22 13:48:32 1998 +0200
@@ -44,29 +44,29 @@
 (* ------------------------------------------------------------------------- *)
 Goalw [lift_rec_def] 
     "[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "lift_rec_Var";
 
 Goalw [lift_rec_def] 
     "[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "lift_rec_le";
 
 Goalw [lift_rec_def] 
     "[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "lift_rec_gt";
 
 Goalw [lift_rec_def] 
     "[|n:nat; k:nat|]==>   \
 \        lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
-by (Asm_full_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "lift_rec_Fun";
 
 Goalw [lift_rec_def] 
     "[|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);
+by (Asm_simp_tac 1);
 qed "lift_rec_App";
 
 (* ------------------------------------------------------------------------- *)
@@ -76,59 +76,57 @@
 Goalw [subst_rec_def] 
     "[|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);
+by (asm_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
 qed "subst_Var";
 
 Goalw [subst_rec_def] 
     "[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u";
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
 qed "subst_eq";
 
 Goalw [subst_rec_def] 
     "[|n:nat; u:redexes; p:nat; p<n|]==>  \
 \        subst_rec(u,Var(n),p) = Var(n #- 1)";
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
 qed "subst_gt";
 
 Goalw [subst_rec_def] 
     "[|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);
+by (asm_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
 qed "subst_lt";
 
 Goalw [subst_rec_def] 
     "[|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);
+by (Asm_simp_tac 1);
 qed "subst_Fun";
 
 Goalw [subst_rec_def] 
     "[|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);
+by (Asm_simp_tac 1);
 qed "subst_App";
 
-fun addsplit ss = (ss setloop (split_inside_tac [split_if]) 
-                addsimps [lift_rec_Var,subst_Var]);
-
+Addsimps [subst_Fun, subst_App];
 
 Goal "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
-by (eresolve_tac [redexes.induct] 1);
-by (ALLGOALS(asm_full_simp_tac 
-    ((addsplit (simpset())) addsimps [lift_rec_Fun,lift_rec_App])));
+by (etac redexes.induct 1);
+by (ALLGOALS
+    (asm_simp_tac (simpset() addsimps [lift_rec_Var,
+					    lift_rec_Fun, lift_rec_App])));
 qed "lift_rec_type_a";
 val lift_rec_type = lift_rec_type_a RS bspec;
 
 Goal "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 
-    ((addsplit (simpset())) addsimps [subst_Fun,subst_App,
-                       lift_rec_type])));
+by (etac redexes.induct 1);
+by (ALLGOALS(asm_simp_tac 
+    (simpset() addsimps [subst_Var, lift_rec_type])));
 qed "subst_type_a";
 val subst_type = subst_type_a RS bspec RS bspec;
 
 
-Addsimps [subst_eq, subst_gt, subst_lt, subst_Fun, subst_App, subst_type,
+Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
 	  lift_rec_le, lift_rec_gt, lift_rec_Fun, lift_rec_App,
 	  lift_rec_type];
 
@@ -139,11 +137,11 @@
 
 Goal "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) THEN (ALLGOALS Asm_simp_tac));
+by ((etac redexes.induct 1) THEN (ALLGOALS Asm_simp_tac));
 by Safe_tac;
-by (excluded_middle_tac "n < xa" 1);
-by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
-by (ALLGOALS (asm_full_simp_tac (addsplit (simpset()) addsimps [leI])));
+by (case_tac "n < xa" 1);
+by ((forward_tac [lt_trans2] 1) THEN (assume_tac 1));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
 qed "lift_lift_rec";
 
 
@@ -156,24 +154,25 @@
 \      ALL n:nat. ALL m:nat. ALL u: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 ((eresolve_tac [redexes.induct] 1)
+by ((etac redexes.induct 1)
     THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift]))));
 by Safe_tac;
 by (excluded_middle_tac "n < x" 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("j","n")] leE 1);
-by (asm_full_simp_tac ((addsplit (simpset())) 
-                        addsimps [leI,gt_pred,succ_pred]) 1);
+by (asm_simp_tac (simpset() setloop (split_inside_tac [split_if])
+			 addsimps [lift_rec_Var,subst_Var,
+				   leI,gt_pred,succ_pred]) 1);
 by (hyp_subst_tac 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_simp_tac 1);
 by (forw_inst_tac [("j","x")] lt_trans2 1);
 by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
+by (asm_simp_tac (simpset() addsimps [leI]) 1);
 qed "lift_rec_subst_rec";
 
 Goal "[|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);
+by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
 qed "lift_subst";
 
 
@@ -181,43 +180,40 @@
 \      ALL n:nat. ALL m:nat. ALL u: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 ((eresolve_tac [redexes.induct] 1)
-    THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift]))));
+by (etac redexes.induct 1
+    THEN ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])));
 by Safe_tac;
 by (excluded_middle_tac "n < x" 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("i","x")] leE 1);
 by (forward_tac  [lt_trans1] 1 THEN assume_tac 1);
-by (ALLGOALS(asm_full_simp_tac 
+by (ALLGOALS(asm_simp_tac 
              (simpset() addsimps [succ_pred,leI,gt_pred])));
 by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
-by (excluded_middle_tac "n < xa" 1);
-by (asm_full_simp_tac (simpset()) 1);
-by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
+by (case_tac "n < xa" 1);
+by (Asm_full_simp_tac 2);
+by (asm_simp_tac (simpset() addsimps [leI]) 1);
 qed "lift_rec_subst_rec_lt";
 
 
 Goal "u:redexes ==>  \
 \       ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) =  u";
-by ((eresolve_tac [redexes.induct] 1)
-    THEN (ALLGOALS Asm_simp_tac));
-by Safe_tac;
-by (excluded_middle_tac "n < x" 1);
-(* x <= n  *)
-by (asm_full_simp_tac (simpset()) 1);
-by (asm_full_simp_tac (simpset()) 1);
+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 --> \
 \    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 ((eresolve_tac [redexes.induct] 1) THEN 
-     (ALLGOALS(asm_simp_tac (simpset() addsimps 
-                             [lift_lift RS sym,lift_rec_subst_rec_lt]))));
+by (etac redexes.induct 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps 
+			   [lift_lift RS sym,lift_rec_subst_rec_lt])));
 by Safe_tac;
 by (excluded_middle_tac "n  le succ(xa)" 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_full_simp_tac 1);
 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
 by (etac leE 1);
 by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2);
@@ -226,10 +222,9 @@
     (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1);
 by (eres_inst_tac [("i","n")] leE 1);
-by (asm_full_simp_tac 
-    (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2);
+by (asm_simp_tac (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2);
 by (excluded_middle_tac "n < x" 1);
-by (asm_full_simp_tac (simpset()) 1);
+by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("j","n")] leE 1);
 by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
 by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1);
@@ -257,18 +252,19 @@
 Goal "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);
-by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps 
-            ([lift_rec_preserve_comp,comp_refl]))));
+by (ALLGOALS
+    (asm_simp_tac
+     (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))";
-by (eresolve_tac [Sreg.induct] 1);
-by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()))));
+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))";
-by (eresolve_tac [Sreg.induct] 1);
-by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps 
-            [lift_rec_preserve_reg])));
+by (etac Sreg.induct 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_Var,
+						    lift_rec_preserve_reg])));
 qed "subst_rec_preserve_reg";
isabelle