--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Jun 22 17:12:27 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Jun 22 17:13:09 1998 +0200
@@ -18,15 +18,15 @@
(* Map *)
(* ---------------------------------------------------------------- *)
-goal thy "Map f`UU =UU";
+Goal "Map f`UU =UU";
by (simp_tac (simpset() addsimps [Map_def]) 1);
qed"Map_UU";
-goal thy "Map f`nil =nil";
+Goal "Map f`nil =nil";
by (simp_tac (simpset() addsimps [Map_def]) 1);
qed"Map_nil";
-goal thy "Map f`(x>>xs)=(f x) >> Map f`xs";
+Goal "Map f`(x>>xs)=(f x) >> Map f`xs";
by (simp_tac (simpset() addsimps [Map_def, Cons_def,flift2_def]) 1);
qed"Map_cons";
@@ -34,15 +34,15 @@
(* Filter *)
(* ---------------------------------------------------------------- *)
-goal thy "Filter P`UU =UU";
+Goal "Filter P`UU =UU";
by (simp_tac (simpset() addsimps [Filter_def]) 1);
qed"Filter_UU";
-goal thy "Filter P`nil =nil";
+Goal "Filter P`nil =nil";
by (simp_tac (simpset() addsimps [Filter_def]) 1);
qed"Filter_nil";
-goal thy "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)";
+Goal "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)";
by (simp_tac (simpset() addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
qed"Filter_cons";
@@ -50,15 +50,15 @@
(* Forall *)
(* ---------------------------------------------------------------- *)
-goal thy "Forall P UU";
+Goal "Forall P UU";
by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
qed"Forall_UU";
-goal thy "Forall P nil";
+Goal "Forall P nil";
by (simp_tac (simpset() addsimps [Forall_def,sforall_def]) 1);
qed"Forall_nil";
-goal thy "Forall P (x>>xs)= (P x & Forall P xs)";
+Goal "Forall P (x>>xs)= (P x & Forall P xs)";
by (simp_tac (simpset() addsimps [Forall_def, sforall_def,
Cons_def,flift2_def]) 1);
qed"Forall_cons";
@@ -68,7 +68,7 @@
(* ---------------------------------------------------------------- *)
-goal thy "(x>>xs) @@ y = x>>(xs @@y)";
+Goal "(x>>xs) @@ y = x>>(xs @@y)";
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Conc_cons";
@@ -76,15 +76,15 @@
(* Takewhile *)
(* ---------------------------------------------------------------- *)
-goal thy "Takewhile P`UU =UU";
+Goal "Takewhile P`UU =UU";
by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
qed"Takewhile_UU";
-goal thy "Takewhile P`nil =nil";
+Goal "Takewhile P`nil =nil";
by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
qed"Takewhile_nil";
-goal thy "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)";
+Goal "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)";
by (simp_tac (simpset() addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
qed"Takewhile_cons";
@@ -92,15 +92,15 @@
(* Dropwhile *)
(* ---------------------------------------------------------------- *)
-goal thy "Dropwhile P`UU =UU";
+Goal "Dropwhile P`UU =UU";
by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
qed"Dropwhile_UU";
-goal thy "Dropwhile P`nil =nil";
+Goal "Dropwhile P`nil =nil";
by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
qed"Dropwhile_nil";
-goal thy "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)";
+Goal "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)";
by (simp_tac (simpset() addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
qed"Dropwhile_cons";
@@ -109,15 +109,15 @@
(* ---------------------------------------------------------------- *)
-goal thy "Last`UU =UU";
+Goal "Last`UU =UU";
by (simp_tac (simpset() addsimps [Last_def]) 1);
qed"Last_UU";
-goal thy "Last`nil =UU";
+Goal "Last`nil =UU";
by (simp_tac (simpset() addsimps [Last_def]) 1);
qed"Last_nil";
-goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)";
+Goal "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)";
by (simp_tac (simpset() addsimps [Last_def, Cons_def]) 1);
by (res_inst_tac [("x","xs")] seq.casedist 1);
by (Asm_simp_tac 1);
@@ -129,15 +129,15 @@
(* Flat *)
(* ---------------------------------------------------------------- *)
-goal thy "Flat`UU =UU";
+Goal "Flat`UU =UU";
by (simp_tac (simpset() addsimps [Flat_def]) 1);
qed"Flat_UU";
-goal thy "Flat`nil =nil";
+Goal "Flat`nil =nil";
by (simp_tac (simpset() addsimps [Flat_def]) 1);
qed"Flat_nil";
-goal thy "Flat`(x##xs)= x @@ (Flat`xs)";
+Goal "Flat`(x##xs)= x @@ (Flat`xs)";
by (simp_tac (simpset() addsimps [Flat_def, Cons_def]) 1);
qed"Flat_cons";
@@ -146,7 +146,7 @@
(* Zip *)
(* ---------------------------------------------------------------- *)
-goal thy "Zip = (LAM t1 t2. case t1 of \
+Goal "Zip = (LAM t1 t2. case t1 of \
\ nil => nil \
\ | x##xs => (case t2 of \
\ nil => UU \
@@ -162,29 +162,29 @@
by (Simp_tac 1);
qed"Zip_unfold";
-goal thy "Zip`UU`y =UU";
+Goal "Zip`UU`y =UU";
by (stac Zip_unfold 1);
by (Simp_tac 1);
qed"Zip_UU1";
-goal thy "!! x. x~=nil ==> Zip`x`UU =UU";
+Goal "!! x. x~=nil ==> Zip`x`UU =UU";
by (stac Zip_unfold 1);
by (Simp_tac 1);
by (res_inst_tac [("x","x")] seq.casedist 1);
by (REPEAT (Asm_full_simp_tac 1));
qed"Zip_UU2";
-goal thy "Zip`nil`y =nil";
+Goal "Zip`nil`y =nil";
by (stac Zip_unfold 1);
by (Simp_tac 1);
qed"Zip_nil";
-goal thy "Zip`(x>>xs)`nil= UU";
+Goal "Zip`(x>>xs)`nil= UU";
by (stac Zip_unfold 1);
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Zip_cons_nil";
-goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys";
+Goal "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys";
by (rtac trans 1);
by (stac Zip_unfold 1);
by (Simp_tac 1);
@@ -218,7 +218,7 @@
Can Filter with HOL predicate directly be defined as fixpoint ?
-goal thy "Filter2 P = (LAM tr. case tr of \
+Goal "Filter2 P = (LAM tr. case tr of \
\ nil => nil \
\ | x##xs => (case x of Undef => UU | Def y => \
\ (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))";
@@ -239,18 +239,18 @@
section "Cons";
-goal thy "a>>s = (Def a)##s";
+Goal "a>>s = (Def a)##s";
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Cons_def2";
-goal thy "x = UU | x = nil | (? a s. x = a >> s)";
+Goal "x = UU | x = nil | (? a s. x = a >> s)";
by (simp_tac (simpset() addsimps [Cons_def2]) 1);
by (cut_facts_tac [seq.exhaust] 1);
by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
qed"Seq_exhaust";
-goal thy "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s ==> P |] ==> P";
+Goal "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s ==> P |] ==> P";
by (cut_inst_tac [("x","x")] Seq_exhaust 1);
by (etac disjE 1);
by (Asm_full_simp_tac 1);
@@ -268,36 +268,36 @@
THEN Asm_full_simp_tac (i+1)
THEN Asm_full_simp_tac i;
-goal thy "a>>s ~= UU";
+Goal "a>>s ~= UU";
by (stac Cons_def2 1);
by (resolve_tac seq.con_rews 1);
by (rtac Def_not_UU 1);
qed"Cons_not_UU";
-goal thy "~(a>>x) << UU";
+Goal "~(a>>x) << UU";
by (rtac notI 1);
by (dtac antisym_less 1);
by (Simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [Cons_not_UU]) 1);
qed"Cons_not_less_UU";
-goal thy "~a>>s << nil";
+Goal "~a>>s << nil";
by (stac Cons_def2 1);
by (resolve_tac seq.rews 1);
by (rtac Def_not_UU 1);
qed"Cons_not_less_nil";
-goal thy "a>>s ~= nil";
+Goal "a>>s ~= nil";
by (stac Cons_def2 1);
by (resolve_tac seq.rews 1);
qed"Cons_not_nil";
-goal thy "nil ~= a>>s";
+Goal "nil ~= a>>s";
by (simp_tac (simpset() addsimps [Cons_def2]) 1);
qed"Cons_not_nil2";
-goal thy "(a>>s = b>>t) = (a = b & s = t)";
+Goal "(a>>s = b>>t) = (a = b & s = t)";
by (simp_tac (HOL_ss addsimps [Cons_def2]) 1);
by (stac (hd lift.inject RS sym) 1);
back(); back();
@@ -305,7 +305,7 @@
by (REPEAT(rtac Def_not_UU 1));
qed"Cons_inject_eq";
-goal thy "(a>>s<<b>>t) = (a = b & s<<t)";
+Goal "(a>>s<<b>>t) = (a = b & s<<t)";
by (simp_tac (simpset() addsimps [Cons_def2]) 1);
by (stac (Def_inject_less_eq RS sym) 1);
back();
@@ -319,7 +319,7 @@
by (etac monofun_cfun_arg 1);
qed"Cons_inject_less_eq";
-goal thy "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
+Goal "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"seq_take_Cons";
@@ -327,7 +327,7 @@
Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
(* Instead of adding UU_neq_Cons every equation UU~=x could be changed to x~=UU *)
-goal thy "UU ~= x>>xs";
+Goal "UU ~= x>>xs";
by (res_inst_tac [("s1","UU"),("t1","x>>xs")] (sym RS rev_contrapos) 1);
by (REPEAT (Simp_tac 1));
qed"UU_neq_Cons";
@@ -339,14 +339,14 @@
section "induction";
-goal thy "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
+Goal "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
by (etac seq.ind 1);
by (REPEAT (atac 1));
by (def_tac 1);
by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Seq_induct";
-goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] \
+Goal "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] \
\ ==> seq_finite x --> P x";
by (etac seq_finite_ind 1);
by (REPEAT (atac 1));
@@ -354,7 +354,7 @@
by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
qed"Seq_FinitePartial_ind";
-goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
+Goal "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
by (etac sfinite.induct 1);
by (assume_tac 1);
by (def_tac 1);
@@ -386,11 +386,11 @@
section "HD,TL";
-goal thy "HD`(x>>y) = Def x";
+Goal "HD`(x>>y) = Def x";
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"HD_Cons";
-goal thy "TL`(x>>y) = y";
+Goal "TL`(x>>y) = y";
by (simp_tac (simpset() addsimps [Cons_def]) 1);
qed"TL_Cons";
@@ -400,16 +400,16 @@
section "Finite, Partial, Infinite";
-goal thy "Finite (a>>xs) = Finite xs";
+Goal "Finite (a>>xs) = Finite xs";
by (simp_tac (simpset() addsimps [Cons_def2,Finite_cons]) 1);
qed"Finite_Cons";
Addsimps [Finite_Cons];
-goal thy "!! x. Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
+Goal "!! x. Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
by (Seq_Finite_induct_tac 1);
qed"FiniteConc_1";
-goal thy "!! z. Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
+Goal "!! z. Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
by (Seq_Finite_induct_tac 1);
(* nil*)
by (strip_tac 1);
@@ -425,7 +425,7 @@
by (Asm_full_simp_tac 1);
qed"FiniteConc_2";
-goal thy "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
+Goal "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
by (rtac iffI 1);
by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
by (rtac refl 1);
@@ -436,11 +436,11 @@
Addsimps [FiniteConc];
-goal thy "!! s. Finite s ==> Finite (Map f`s)";
+Goal "!! s. Finite s ==> Finite (Map f`s)";
by (Seq_Finite_induct_tac 1);
qed"FiniteMap1";
-goal thy "!! s. Finite s ==> ! t. (s = Map f`t) --> Finite t";
+Goal "!! s. Finite s ==> ! t. (s = Map f`t) --> Finite t";
by (Seq_Finite_induct_tac 1);
by (strip_tac 1);
by (Seq_case_simp_tac "t" 1);
@@ -451,7 +451,7 @@
by (Asm_full_simp_tac 1);
qed"FiniteMap2";
-goal thy "Finite (Map f`s) = Finite s";
+Goal "Finite (Map f`s) = Finite s";
by Auto_tac;
by (etac (FiniteMap2 RS spec RS mp) 1);
by (rtac refl 1);
@@ -459,7 +459,7 @@
qed"Map2Finite";
-goal thy "!! s. Finite s ==> Finite (Filter P`s)";
+Goal "!! s. Finite s ==> Finite (Filter P`s)";
by (Seq_Finite_induct_tac 1);
qed"FiniteFilter";
@@ -473,7 +473,7 @@
Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction
to Finite_flat *)
-goal thy "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
+Goal "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
by (Seq_Finite_induct_tac 1);
by (strip_tac 1);
by (etac conjE 1);
@@ -485,7 +485,7 @@
qed_spec_mp"Finite_flat";
-goal thy "adm(%(x:: 'a Seq).Finite x)";
+Goal "adm(%(x:: 'a Seq).Finite x)";
by (rtac admI2 1);
by (eres_inst_tac [("x","0")] allE 1);
back();
@@ -506,15 +506,15 @@
section "Conc";
-goal thy "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)";
+Goal "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)";
by (Seq_Finite_induct_tac 1);
qed"Conc_cong";
-goal thy "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z";
+Goal "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z";
by (Seq_induct_tac "x" [] 1);
qed"Conc_assoc";
-goal thy "s@@ nil = s";
+Goal "s@@ nil = s";
by (res_inst_tac[("x","s")] seq.ind 1);
by (Simp_tac 1);
by (Simp_tac 1);
@@ -525,12 +525,12 @@
Addsimps [nilConc];
(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
-goal thy "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
+Goal "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
by (Seq_case_simp_tac "x" 1);
by Auto_tac;
qed"nil_is_Conc";
-goal thy "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
+Goal "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
by (Seq_case_simp_tac "x" 1);
by Auto_tac;
qed"nil_is_Conc2";
@@ -540,11 +540,11 @@
section "Last";
-goal thy "!! s. Finite s ==> s~=nil --> Last`s~=UU";
+Goal "!! s. Finite s ==> s~=nil --> Last`s~=UU";
by (Seq_Finite_induct_tac 1);
qed"Finite_Last1";
-goal thy "!! s. Finite s ==> Last`s=UU --> s=nil";
+Goal "!! s. Finite s ==> Last`s=UU --> s=nil";
by (Seq_Finite_induct_tac 1);
by (fast_tac HOL_cs 1);
qed"Finite_Last2";
@@ -556,11 +556,11 @@
section "Filter, Conc";
-goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
+Goal "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
by (Seq_induct_tac "s" [Filter_def] 1);
qed"FilterPQ";
-goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
+Goal "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1);
qed"FilterConc";
@@ -568,24 +568,24 @@
section "Map";
-goal thy "Map f`(Map g`s) = Map (f o g)`s";
+Goal "Map f`(Map g`s) = Map (f o g)`s";
by (Seq_induct_tac "s" [] 1);
qed"MapMap";
-goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
+Goal "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
by (Seq_induct_tac "x" [] 1);
qed"MapConc";
-goal thy "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
+Goal "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
by (Seq_induct_tac "x" [] 1);
qed"MapFilter";
-goal thy "nil = (Map f`s) --> s= nil";
+Goal "nil = (Map f`s) --> s= nil";
by (Seq_case_simp_tac "s" 1);
qed"nilMap";
-goal thy "Forall P (Map f`s) = Forall (P o f) s";
+Goal "Forall P (Map f`s) = Forall (P o f) s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"ForallMap";
@@ -597,30 +597,30 @@
section "Forall";
-goal thy "Forall P ys & (! x. P x --> Q x) \
+Goal "Forall P ys & (! x. P x --> Q x) \
\ --> Forall Q ys";
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
qed"ForallPForallQ1";
bind_thm ("ForallPForallQ",impI RSN (2,allI RSN (2,conjI RS (ForallPForallQ1 RS mp))));
-goal thy "(Forall P x & Forall P y) --> Forall P (x @@ y)";
+Goal "(Forall P x & Forall P y) --> Forall P (x @@ y)";
by (Seq_induct_tac "x" [Forall_def,sforall_def] 1);
qed"Forall_Conc_impl";
-goal thy "!! x. Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
+Goal "!! x. Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
by (Seq_Finite_induct_tac 1);
qed"Forall_Conc";
Addsimps [Forall_Conc];
-goal thy "Forall P s --> Forall P (TL`s)";
+Goal "Forall P s --> Forall P (TL`s)";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"ForallTL1";
bind_thm ("ForallTL",ForallTL1 RS mp);
-goal thy "Forall P s --> Forall P (Dropwhile Q`s)";
+Goal "Forall P s --> Forall P (Dropwhile Q`s)";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"ForallDropwhile1";
@@ -629,7 +629,7 @@
(* only admissible in t, not if done in s *)
-goal thy "! s. Forall P s --> t<<s --> Forall P t";
+Goal "! s. Forall P s --> t<<s --> Forall P t";
by (Seq_induct_tac "t" [Forall_def,sforall_def] 1);
by (strip_tac 1);
by (Seq_case_simp_tac "sa" 1);
@@ -640,12 +640,12 @@
bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
-goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
+Goal "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
by Auto_tac;
qed"Forall_postfixclosed";
-goal thy "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q`tr = Filter R`tr";
+Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q`tr = Filter R`tr";
by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1);
qed"ForallPFilterQR1";
@@ -657,12 +657,12 @@
section "Forall, Filter";
-goal thy "Forall P (Filter P`x)";
+Goal "Forall P (Filter P`x)";
by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
qed"ForallPFilterP";
(* holds also in other direction, then equal to forallPfilterP *)
-goal thy "Forall P x --> Filter P`x = x";
+Goal "Forall P x --> Filter P`x = x";
by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
qed"ForallPFilterPid1";
@@ -670,7 +670,7 @@
(* holds also in other direction *)
-goal thy "!! ys . Finite ys ==> \
+Goal "!! ys . Finite ys ==> \
\ Forall (%x. ~P x) ys --> Filter P`ys = nil ";
by (Seq_Finite_induct_tac 1);
qed"ForallnPFilterPnil1";
@@ -679,7 +679,7 @@
(* holds also in other direction *)
-goal thy "!! P. ~Finite ys & Forall (%x. ~P x) ys \
+Goal "!! P. ~Finite ys & Forall (%x. ~P x) ys \
\ --> Filter P`ys = UU ";
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
qed"ForallnPFilterPUU1";
@@ -689,7 +689,7 @@
(* inverse of ForallnPFilterPnil *)
-goal thy "!! ys . Filter P`ys = nil --> \
+Goal "!! ys . Filter P`ys = nil --> \
\ (Forall (%x. ~P x) ys & Finite ys)";
by (res_inst_tac[("x","ys")] Seq_induct 1);
(* adm *)
@@ -706,15 +706,15 @@
(* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
-goal thy "!! ys. Finite ys ==> Filter P`ys ~= UU";
+Goal "!! ys. Finite ys ==> Filter P`ys ~= UU";
by (Seq_Finite_induct_tac 1);
qed"FilterUU_nFinite_lemma1";
-goal thy "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU";
+Goal "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU";
by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
qed"FilterUU_nFinite_lemma2";
-goal thy "!! P. Filter P`ys = UU ==> \
+Goal "!! P. Filter P`ys = UU ==> \
\ (Forall (%x. ~P x) ys & ~Finite ys)";
by (rtac conjI 1);
by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
@@ -723,14 +723,14 @@
qed"FilternPUUForallP";
-goal thy "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
+Goal "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
\ ==> Filter P`ys = nil";
by (etac ForallnPFilterPnil 1);
by (etac ForallPForallQ 1);
by Auto_tac;
qed"ForallQFilterPnil";
-goal thy "!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|] \
+Goal "!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|] \
\ ==> Filter P`ys = UU ";
by (etac ForallnPFilterPUU 1);
by (etac ForallPForallQ 1);
@@ -744,19 +744,19 @@
section "Takewhile, Forall, Filter";
-goal thy "Forall P (Takewhile P`x)";
+Goal "Forall P (Takewhile P`x)";
by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
qed"ForallPTakewhileP";
-goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
+Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
by (rtac ForallPForallQ 1);
by (rtac ForallPTakewhileP 1);
by Auto_tac;
qed"ForallPTakewhileQ";
-goal thy "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
+Goal "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
\ ==> Filter P`(Takewhile Q`ys) = nil";
by (etac ForallnPFilterPnil 1);
by (rtac ForallPForallQ 1);
@@ -764,7 +764,7 @@
by Auto_tac;
qed"FilterPTakewhileQnil";
-goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
+Goal "!! Q P. [| !!x. Q x ==> P x |] ==> \
\ Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
by (rtac ForallPFilterPid 1);
by (rtac ForallPForallQ 1);
@@ -775,28 +775,28 @@
Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
FilterPTakewhileQnil,FilterPTakewhileQid];
-goal thy "Takewhile P`(Takewhile P`s) = Takewhile P`s";
+Goal "Takewhile P`(Takewhile P`s) = Takewhile P`s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"Takewhile_idempotent";
-goal thy "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
+Goal "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"ForallPTakewhileQnP";
-goal thy "Forall P s --> Dropwhile (%x. Q x | (~P x))`s = Dropwhile Q`s";
+Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))`s = Dropwhile Q`s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"ForallPDropwhileQnP";
Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp];
-goal thy "Forall P s --> Takewhile P`(s @@ t) = s @@ (Takewhile P`t)";
+Goal "Forall P s --> Takewhile P`(s @@ t) = s @@ (Takewhile P`t)";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"TakewhileConc1";
bind_thm("TakewhileConc",TakewhileConc1 RS mp);
-goal thy "!! s. Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
+Goal "!! s. Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
by (Seq_Finite_induct_tac 1);
qed"DropwhileConc1";
@@ -809,7 +809,7 @@
section "coinductive characterizations of Filter";
-goal thy "HD`(Filter P`y) = Def x \
+Goal "HD`(Filter P`y) = Def x \
\ --> y = ((Takewhile (%x. ~P x)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
\ & Finite (Takewhile (%x. ~ P x)`y) & P x";
@@ -825,7 +825,7 @@
by (Asm_full_simp_tac 1);
qed"divide_Seq_lemma";
-goal thy "!! x. (x>>xs) << Filter P`y \
+Goal "!! x. (x>>xs) << Filter P`y \
\ ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
\ & Finite (Takewhile (%a. ~ P a)`y) & P x";
by (rtac (divide_Seq_lemma RS mp) 1);
@@ -834,14 +834,14 @@
qed"divide_Seq";
-goal thy "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)";
+Goal "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)";
(* Pay attention: is only admissible with chain-finite package to be added to
adm test *)
by (Seq_induct_tac "y" [Forall_def,sforall_def] 1);
qed"nForall_HDFilter";
-goal thy "!!y. ~Forall P y \
+Goal "!!y. ~Forall P y \
\ ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
\ Finite (Takewhile P`y) & (~ P x)";
by (dtac (nForall_HDFilter RS mp) 1);
@@ -852,7 +852,7 @@
qed"divide_Seq2";
-goal thy "!! y. ~Forall P y \
+Goal "!! y. ~Forall P y \
\ ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
by (cut_inst_tac [] divide_Seq2 1);
(*Auto_tac no longer proves it*)
@@ -867,13 +867,13 @@
section "take_lemma";
-goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
+Goal "(!n. seq_take n`x = seq_take n`x') = (x = x')";
by (rtac iffI 1);
by (resolve_tac seq.take_lemmas 1);
by Auto_tac;
qed"seq_take_lemma";
-goal thy
+Goal
" ! n. ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))";
by (Seq_induct_tac "x" [] 1);
@@ -885,7 +885,7 @@
qed"take_reduction1";
-goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
+Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
\ ==> seq_take n`(x @@ (s>>y1)) = seq_take n`(y @@ (t>>y2))";
by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
@@ -895,7 +895,7 @@
take-lemma and take_reduction for << instead of =
------------------------------------------------------------------ *)
-goal thy
+Goal
" ! n. ((! k. k < n --> seq_take k`y1 << seq_take k`y2) \
\ --> seq_take n`(x @@ (t>>y1)) << seq_take n`(x @@ (t>>y2)))";
by (Seq_induct_tac "x" [] 1);
@@ -907,7 +907,7 @@
qed"take_reduction_less1";
-goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
+Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
\ ==> seq_take n`(x @@ (s>>y1)) << seq_take n`(y @@ (t>>y2))";
by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset()));
qed"take_reduction_less";
@@ -931,7 +931,7 @@
qed"take_lemma_less1";
-goal thy "(!n. seq_take n`x << seq_take n`x') = (x << x')";
+Goal "(!n. seq_take n`x << seq_take n`x') = (x << x')";
by (rtac iffI 1);
by (rtac take_lemma_less1 1);
by Auto_tac;
@@ -942,7 +942,7 @@
take-lemma proof principles
------------------------------------------------------------------ *)
-goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
+Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
\ !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
\ ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \
\ ==> A x --> (f x)=(g x)";
@@ -950,7 +950,7 @@
by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
qed"take_lemma_principle1";
-goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
+Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
\ !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
\ ==> ! n. seq_take n`(f (s1 @@ y>>s2)) \
\ = seq_take n`(g (s1 @@ y>>s2)) |] \
@@ -970,7 +970,7 @@
to be imbuilt into the rule, as induction has to be done early and the take lemma
has to be used in the trivial direction afterwards for the (Forall Q x) case. *)
-goal thy
+Goal
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
\ !! s1 s2 y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
@@ -992,7 +992,7 @@
qed"take_lemma_induct";
-goal thy
+Goal
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
\ !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m`(f t) = seq_take m`(g t);\
\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
@@ -1044,7 +1044,7 @@
end;
-goal thy
+Goal
"!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
\ !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m`(f t h1 h2) = seq_take m`(g t h1 h2);\
\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \
@@ -1068,7 +1068,7 @@
-goal thy
+Goal
"!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \
\ !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m`(f t) = seq_take m`(g t));\
\ Forall Q s1; Finite s1; ~ Q y|] \
@@ -1097,7 +1097,7 @@
*)
-goal thy
+Goal
"!! Q. [| A UU ==> (f UU) = (g UU) ; \
\ A nil ==> (f nil) = (g nil) ; \
\ !! s y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
@@ -1131,27 +1131,27 @@
(* In general: How to do this case without the same adm problems
as for the entire proof ? *)
-goal thy "Forall (%x.~(P x & Q x)) s \
+Goal "Forall (%x.~(P x & Q x)) s \
\ --> Filter P`(Filter Q`s) =\
\ Filter (%x. P x & Q x)`s";
by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
qed"Filter_lemma1";
-goal thy "!! s. Finite s ==> \
+Goal "!! s. Finite s ==> \
\ (Forall (%x. (~P x) | (~ Q x)) s \
\ --> Filter P`(Filter Q`s) = nil)";
by (Seq_Finite_induct_tac 1);
qed"Filter_lemma2";
-goal thy "!! s. Finite s ==> \
+Goal "!! s. Finite s ==> \
\ Forall (%x. (~P x) | (~ Q x)) s \
\ --> Filter (%x. P x & Q x)`s = nil";
by (Seq_Finite_induct_tac 1);
qed"Filter_lemma3";
-goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
+Goal "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
by (res_inst_tac [("A1","%x. True")
,("Q1","%x.~(P x & Q x)"),("x1","s")]
(take_lemma_induct RS mp) 1);
@@ -1170,7 +1170,7 @@
-goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
+Goal "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
by (res_inst_tac [("A1","%x. True"), ("x1","x")]
(take_lemma_in_eq_out RS mp) 1);
by Auto_tac;