--- a/src/HOL/Lex/AutoChopper.ML Thu May 14 16:50:09 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.ML Thu May 14 16:54:20 1998 +0200
@@ -34,17 +34,17 @@
qed"acc_prefix_Cons";
Addsimps [acc_prefix_Cons];
-goal thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
-by (list.induct_tac "xs" 1);
+goal thy "!st us p y ys. acc A st p xs (ys@[y]) us ~= ([],zs)";
+by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
val accept_not_Nil = result() repeat_RS spec;
Addsimps [accept_not_Nil];
goal thy
-"!st us. acc xs st [] us ([],ys) A = ([], zs) --> \
+"!st us. acc A st ([],ys) xs [] us = ([], zs) --> \
\ zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (delta A ys st))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Simp_tac 1);
by (strip_tac 1);
@@ -58,7 +58,7 @@
by (case_tac "zsa = []" 1);
by (Asm_simp_tac 1);
by (Fast_tac 1);
-bind_thm("no_acc", result() RS spec RS spec RS mp);
+qed_spec_mp "no_acc";
val [prem] = goal HOL.thy "? x. P(f(x)) ==> ? y. P(y)";
@@ -69,12 +69,12 @@
goal thy
"! r erk l rst st ys yss zs::'a list. \
-\ acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
+\ acc A st (l,rst) xs erk r = (ys#yss, zs) --> \
\ ys@concat(yss)@zs = (if acc_prefix A xs st then r@xs else erk@concat(l)@rst)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Asm_simp_tac 1);
-by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1);
by (rename_tac "vss lrst" 1);
by (Asm_simp_tac 1);
by (res_inst_tac[("xs","vss")] list_eq_cases 1);
@@ -88,16 +88,16 @@
goal thy
"! st erk r l rest ys yss zs.\
-\ acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\ acc A st (l,rest) xs erk r = (ys#yss, zs) --> \
\ (if acc_prefix A xs st \
\ then ys ~= [] \
\ else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
by (Simp_tac 1);
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Fast_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1);
by (rename_tac "vss lrst" 1);
by (Asm_simp_tac 1);
by (strip_tac 1);
@@ -111,18 +111,18 @@
goal thy
"! st erk r l rest ys yss zs. \
-\ acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\ acc A st (l,rest) xs erk r = (ys#yss, zs) --> \
\ (if acc_prefix A xs st \
\ then ? g. ys=r@g & fin A (delta A g st) \
\ else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
by (Simp_tac 1);
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Fast_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
by (strip_tac 1);
by (rtac conjI 1);
- by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+ by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1);
by (rename_tac "vss lrst" 1);
by (Asm_simp_tac 1);
by (case_tac "acc_prefix A list (next A a st)" 1);
@@ -150,22 +150,22 @@
goal thy
"! st erk r l rest ys yss zs. \
-\ acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
+\ acc A st (l,rest) xs erk r = (ys#yss, zs) --> \
\ (if acc_prefix A xs st \
-\ then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
+\ then acc A (start A) ([],concat(yss)@zs) (concat(yss)@zs) [] [] = (yss,zs) \
\ else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
by (Simp_tac 1);
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Fast_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
-by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
+by (res_inst_tac [("p","acc A (start A) ([],list) list [] []")] PairE 1);
by (rename_tac "vss lrst" 1);
by (Asm_simp_tac 1);
by (strip_tac 1);
by (case_tac "acc_prefix A list (next A a st)" 1);
by (Asm_simp_tac 1);
-by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1);
+by (subgoal_tac "acc A (start A) ([],list) list [] [] = (yss,zs)" 1);
by (Asm_simp_tac 2);
by (subgoal_tac "r@[a] ~= []" 2);
by (Fast_tac 2);
@@ -189,12 +189,12 @@
Delsimps [split_paired_All];
goal thy
"! st erk r p ys yss zs. \
-\ acc xs st erk r p A = (ys#yss, zs) --> \
+\ acc A st p xs erk r = (ys#yss, zs) --> \
\ (if acc_prefix A xs st \
\ then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (delta A as st))\
\ else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
by (Simp_tac 1);
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (Fast_tac 1);
by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);