--- a/src/CCL/CCL.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/CCL.ML Mon Jun 22 15:18:02 1998 +0200
@@ -22,7 +22,7 @@
qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
-goal CCL.thy "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
+Goal "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
by (fast_tac (set_cs addIs [po_abstractn]) 1);
bind_thm("abstractn", standard (allI RS (result() RS mp)));
@@ -42,11 +42,11 @@
(*** Termination and Divergence ***)
-goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
+Goalw [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
by (rtac iff_refl 1);
qed "Trm_iff";
-goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
+Goalw [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
by (rtac iff_refl 1);
qed "Dvg_iff";
@@ -140,13 +140,13 @@
by (resolve_tac (prems RL [major RS ssubst]) 1);
qed "XHlemma1";
-goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> & P(t,t')} <-> Q)";
+Goal "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> & P(t,t')} <-> Q)";
by (fast_tac ccl_cs 1);
bind_thm("XHlemma2", result() RS mp);
(*** Pre-Order ***)
-goalw CCL.thy [POgen_def,SIM_def] "mono(%X. POgen(X))";
+Goalw [POgen_def,SIM_def] "mono(%X. POgen(X))";
by (rtac monoI 1);
by (safe_tac ccl_cs);
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
@@ -154,14 +154,14 @@
by (ALLGOALS (fast_tac set_cs));
qed "POgen_mono";
-goalw CCL.thy [POgen_def,SIM_def]
+Goalw [POgen_def,SIM_def]
"<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true) | (t=false & t'=false) | \
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
by (rtac (iff_refl RS XHlemma2) 1);
qed "POgenXH";
-goal CCL.thy
+Goal
"t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & a [= a' & b [= b') | \
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
@@ -171,24 +171,24 @@
by (rtac (iff_refl RS XHlemma2) 1);
qed "poXH";
-goal CCL.thy "bot [= b";
+Goal "bot [= b";
by (rtac (poXH RS iffD2) 1);
by (simp_tac ccl_ss 1);
qed "po_bot";
-goal CCL.thy "a [= bot --> a=bot";
+Goal "a [= bot --> a=bot";
by (rtac impI 1);
by (dtac (poXH RS iffD1) 1);
by (etac rev_mp 1);
by (simp_tac ccl_ss 1);
bind_thm("bot_poleast", result() RS mp);
-goal CCL.thy "<a,b> [= <a',b'> <-> a [= a' & b [= b'";
+Goal "<a,b> [= <a',b'> <-> a [= a' & b [= b'";
by (rtac (poXH RS iff_trans) 1);
by (simp_tac ccl_ss 1);
qed "po_pair";
-goal CCL.thy "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
+Goal "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
by (rtac (poXH RS iff_trans) 1);
by (simp_tac ccl_ss 1);
by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
@@ -229,14 +229,14 @@
by (resolve_tac prems 1);
qed "po_lemma";
-goal CCL.thy "~ <a,b> [= lam x. f(x)";
+Goal "~ <a,b> [= lam x. f(x)";
by (rtac notI 1);
by (rtac (npo_lam_bot RS notE) 1);
by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
qed "npo_pair_lam";
-goal CCL.thy "~ lam x. f(x) [= <a,b>";
+Goal "~ lam x. f(x) [= <a,b>";
by (rtac notI 1);
by (rtac (npo_lam_bot RS notE) 1);
by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
@@ -266,7 +266,7 @@
(*************** EQUALITY *******************)
-goalw CCL.thy [EQgen_def,SIM_def] "mono(%X. EQgen(X))";
+Goalw [EQgen_def,SIM_def] "mono(%X. EQgen(X))";
by (rtac monoI 1);
by (safe_tac set_cs);
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
@@ -274,7 +274,7 @@
by (ALLGOALS (fast_tac set_cs));
qed "EQgen_mono";
-goalw CCL.thy [EQgen_def,SIM_def]
+Goalw [EQgen_def,SIM_def]
"<t,t'> : EQgen(R) <-> (t=bot & t'=bot) | (t=true & t'=true) | \
\ (t=false & t'=false) | \
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | \
@@ -282,7 +282,7 @@
by (rtac (iff_refl RS XHlemma2) 1);
qed "EQgenXH";
-goal CCL.thy
+Goal
"t=t' <-> (t=bot & t'=bot) | (t=true & t'=true) | (t=false & t'=false) | \
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & a=a' & b=b') | \
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))";
@@ -313,12 +313,12 @@
(*** Untyped Case Analysis and Other Facts ***)
-goalw CCL.thy [apply_def] "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
+Goalw [apply_def] "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
by (safe_tac ccl_cs);
by (simp_tac ccl_ss 1);
bind_thm("cond_eta", result() RS mp);
-goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
+Goal "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
by (fast_tac set_cs 1);
qed "exhaustion";
--- a/src/CCL/Fix.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Fix.ML Mon Jun 22 15:18:02 1998 +0200
@@ -44,7 +44,7 @@
(*** Lemmas for Inclusive Predicates ***)
-goal Fix.thy "INCL(%x.~ a(x) [= t)";
+Goal "INCL(%x.~ a(x) [= t)";
by (rtac inclI 1);
by (dtac bspec 1);
by (rtac zeroT 1);
@@ -67,7 +67,7 @@
by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
qed "ball_INCL";
-goal Fix.thy "INCL(%x. a(x) = (b(x)::'a::prog))";
+Goal "INCL(%x. a(x) = (b(x)::'a::prog))";
by (simp_tac (term_ss addsimps [eq_iff]) 1);
by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
qed "eq_INCL";
@@ -76,11 +76,11 @@
(* Fixed points of idgen *)
-goal Fix.thy "idgen(fix(idgen)) = fix(idgen)";
+Goal "idgen(fix(idgen)) = fix(idgen)";
by (rtac (fixB RS sym) 1);
qed "fix_idgenfp";
-goalw Fix.thy [idgen_def] "idgen(lam x. x) = lam x. x";
+Goalw [idgen_def] "idgen(lam x. x) = lam x. x";
by (simp_tac term_ss 1);
by (rtac (term_case RS allI) 1);
by (ALLGOALS (simp_tac term_ss));
@@ -161,7 +161,7 @@
by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
qed "id_least_idgen";
-goal Fix.thy "fix(idgen) = lam x. x";
+Goal "fix(idgen) = lam x. x";
by (fast_tac (term_cs addIs [eq_iff RS iffD2,
id_idgenfp RS fix_least_idgen,
fix_idgenfp RS id_least_idgen]) 1);
--- a/src/CCL/Hered.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Hered.ML Mon Jun 22 15:18:02 1998 +0200
@@ -12,18 +12,18 @@
(*** Hereditary Termination ***)
-goalw Hered.thy [HTTgen_def] "mono(%X. HTTgen(X))";
+Goalw [HTTgen_def] "mono(%X. HTTgen(X))";
by (rtac monoI 1);
by (fast_tac set_cs 1);
qed "HTTgen_mono";
-goalw Hered.thy [HTTgen_def]
+Goalw [HTTgen_def]
"t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | \
\ (EX f. t=lam x. f(x) & (ALL x. f(x) : A))";
by (fast_tac set_cs 1);
qed "HTTgenXH";
-goal Hered.thy
+Goal
"t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
\ (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
by (rtac (rewrite_rule [HTTgen_def]
@@ -33,24 +33,24 @@
(*** Introduction Rules for HTT ***)
-goal Hered.thy "~ bot : HTT";
+Goal "~ bot : HTT";
by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
qed "HTT_bot";
-goal Hered.thy "true : HTT";
+Goal "true : HTT";
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
qed "HTT_true";
-goal Hered.thy "false : HTT";
+Goal "false : HTT";
by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
qed "HTT_false";
-goal Hered.thy "<a,b> : HTT <-> a : HTT & b : HTT";
+Goal "<a,b> : HTT <-> a : HTT & b : HTT";
by (rtac (HTTXH RS iff_trans) 1);
by (fast_tac term_cs 1);
qed "HTT_pair";
-goal Hered.thy "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
+Goal "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
by (rtac (HTTXH RS iff_trans) 1);
by (simp_tac term_ss 1);
by (safe_tac term_cs);
@@ -112,11 +112,11 @@
(*** Formation Rules for Types ***)
-goal Hered.thy "Unit <= HTT";
+Goal "Unit <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
qed "UnitF";
-goal Hered.thy "Bool <= HTT";
+Goal "Bool <= HTT";
by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
qed "BoolF";
@@ -136,14 +136,14 @@
(*** exhaution rule for type-former ***)
(*Proof by induction - needs induction rule for type*)
-goal Hered.thy "Nat <= HTT";
+Goal "Nat <= HTT";
by (simp_tac (term_ss addsimps [subsetXH]) 1);
by (safe_tac set_cs);
by (etac Nat_ind 1);
by (ALLGOALS (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD]))));
val NatF = result();
-goal Hered.thy "Nat <= HTT";
+Goal "Nat <= HTT";
by (safe_tac set_cs);
by (etac HTT_coinduct3 1);
by (fast_tac (set_cs addIs HTTgenIs
--- a/src/CCL/Set.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Set.ML Mon Jun 22 15:18:02 1998 +0200
@@ -116,7 +116,7 @@
qed_goal "subset_refl" Set.thy "A <= A"
(fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
-goal Set.thy "!!A B C. [| A<=B; B<=C |] ==> A<=C";
+Goal "!!A B C. [| A<=B; B<=C |] ==> A<=C";
by (rtac subsetI 1);
by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
qed "subset_trans";
@@ -163,7 +163,7 @@
by (REPEAT (resolve_tac (refl::prems) 1));
qed "setup_induction";
-goal Set.thy "{x. x:A} = A";
+Goal "{x. x:A} = A";
by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE etac CollectD 1));
qed "trivial_set";
@@ -234,7 +234,7 @@
(*** Empty sets ***)
-goalw Set.thy [empty_def] "{x. False} = {}";
+Goalw [empty_def] "{x. False} = {}";
by (rtac refl 1);
qed "empty_eq";
@@ -252,7 +252,7 @@
(*** Singleton sets ***)
-goalw Set.thy [singleton_def] "a : {a}";
+Goalw [singleton_def] "a : {a}";
by (rtac CollectI 1);
by (rtac refl 1);
qed "singletonI";
--- a/src/CCL/Term.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Term.ML Mon Jun 22 15:18:02 1998 +0200
@@ -21,33 +21,33 @@
(*** Beta Rules, including strictness ***)
-goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
+Goalw [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
by (res_inst_tac [("t","t")] term_case 1);
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
bind_thm("letB", result() RS mp);
-goalw Term.thy [let_def] "let x be bot in f(x) = bot";
+Goalw [let_def] "let x be bot in f(x) = bot";
by (rtac caseBbot 1);
qed "letBabot";
-goalw Term.thy [let_def] "let x be t in bot = bot";
+Goalw [let_def] "let x be t in bot = bot";
by (resolve_tac ([caseBbot] RL [term_case]) 1);
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
qed "letBbbot";
-goalw Term.thy [apply_def] "(lam x. b(x)) ` a = b(a)";
+Goalw [apply_def] "(lam x. b(x)) ` a = b(a)";
by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
qed "applyB";
-goalw Term.thy [apply_def] "bot ` a = bot";
+Goalw [apply_def] "bot ` a = bot";
by (rtac caseBbot 1);
qed "applyBbot";
-goalw Term.thy [fix_def] "fix(f) = f(fix(f))";
+Goalw [fix_def] "fix(f) = f(fix(f))";
by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
qed "fixB";
-goalw Term.thy [letrec_def]
+Goalw [letrec_def]
"letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))";
by (resolve_tac [fixB RS ssubst] 1 THEN
resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
--- a/src/CCL/Trancl.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Trancl.ML Mon Jun 22 15:18:02 1998 +0200
@@ -27,7 +27,7 @@
(** Identity relation **)
-goalw Trancl.thy [id_def] "<a,a> : id";
+Goalw [id_def] "<a,a> : id";
by (rtac CollectI 1);
by (rtac exI 1);
by (rtac refl 1);
@@ -77,7 +77,7 @@
(** The relation rtrancl **)
-goal Trancl.thy "mono(%s. id Un (r O s))";
+Goal "mono(%s. id Un (r O s))";
by (rtac monoI 1);
by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
qed "rtrancl_fun_mono";
@@ -85,7 +85,7 @@
val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
(*Reflexivity of rtrancl*)
-goal Trancl.thy "<a,a> : r^*";
+Goal "<a,a> : r^*";
by (stac rtrancl_unfold 1);
by (fast_tac comp_cs 1);
qed "rtrancl_refl";
@@ -133,7 +133,7 @@
qed "rtrancl_induct";
(*transitivity of transitive closure!! -- by induction.*)
-goal Trancl.thy "trans(r^*)";
+Goal "trans(r^*)";
by (rtac transI 1);
by (res_inst_tac [("b","z")] rtrancl_induct 1);
by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
@@ -200,7 +200,7 @@
(*Transitivity of r^+.
Proved by unfolding since it uses transitivity of rtrancl. *)
-goalw Trancl.thy [trancl_def] "trans(r^+)";
+Goalw [trancl_def] "trans(r^+)";
by (rtac transI 1);
by (REPEAT (etac compEpair 1));
by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
--- a/src/CCL/Type.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Type.ML Mon Jun 22 15:18:02 1998 +0200
@@ -108,11 +108,11 @@
(*** Monotonicity ***)
-goal Type.thy "mono (%X. X)";
+Goal "mono (%X. X)";
by (REPEAT (ares_tac [monoI] 1));
qed "idM";
-goal Type.thy "mono(%X. A)";
+Goal "mono(%X. A)";
by (REPEAT (ares_tac [monoI,subset_refl] 1));
qed "constM";
@@ -156,18 +156,18 @@
(*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
-goal Type.thy "mono(%X. Unit+X)";
+Goal "mono(%X. Unit+X)";
by (REPEAT (ares_tac [PlusM,constM,idM] 1));
qed "NatM";
bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
-goal Type.thy "mono(%X.(Unit+Sigma(A,%y. X)))";
+Goal "mono(%X.(Unit+Sigma(A,%y. X)))";
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
qed "ListM";
bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
-goal Type.thy "mono(%X.({} + Sigma(A,%y. X)))";
+Goal "mono(%X.({} + Sigma(A,%y. X)))";
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
qed "IListsM";
bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
--- a/src/CCL/Wfd.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Wfd.ML Mon Jun 22 15:18:02 1998 +0200
@@ -63,7 +63,7 @@
(*** Lexicographic Ordering ***)
-goalw Wfd.thy [lex_def]
+Goalw [lex_def]
"p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
by (fast_tac ccl_cs 1);
qed "lexXH";
@@ -109,7 +109,7 @@
(*** Mapping ***)
-goalw Wfd.thy [wmap_def]
+Goalw [wmap_def]
"p : wmap(f,r) <-> (EX x y. p=<x,y> & <f(x),f(y)> : r)";
by (fast_tac ccl_cs 1);
qed "wmapXH";
@@ -175,18 +175,18 @@
by (rtac Empty_wf 1);
qed "wf_wf";
-goalw Wfd.thy [NatPR_def] "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)";
+Goalw [NatPR_def] "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)";
by (fast_tac set_cs 1);
qed "NatPRXH";
-goalw Wfd.thy [ListPR_def] "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
+Goalw [ListPR_def] "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
by (fast_tac set_cs 1);
qed "ListPRXH";
val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));
-goalw Wfd.thy [Wfd_def] "Wfd(NatPR)";
+Goalw [Wfd_def] "Wfd(NatPR)";
by (safe_tac set_cs);
by (wfd_strengthen_tac "%x. x:Nat" 1);
by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
@@ -194,7 +194,7 @@
by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
qed "NatPR_wf";
-goalw Wfd.thy [Wfd_def] "Wfd(ListPR(A))";
+Goalw [Wfd_def] "Wfd(ListPR(A))";
by (safe_tac set_cs);
by (wfd_strengthen_tac "%x. x:List(A)" 1);
by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
--- a/src/CCL/ex/Stream.ML Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/ex/Stream.ML Mon Jun 22 15:18:02 1998 +0200
@@ -84,12 +84,12 @@
(* fun iter1(f,a) = a$iter1(f,f(a)) *)
(* fun iter2(f,a) = a$map(f,iter2(f,a)) *)
-goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
+Goalw [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
by (rtac (letrecB RS trans) 1);
by (simp_tac term_ss 1);
qed "iter1B";
-goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
+Goalw [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
by (rtac (letrecB RS trans) 1);
by (rtac refl 1);
qed "iter2B";
@@ -101,7 +101,7 @@
by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
qed "iter2Blemma";
-goal Stream.thy "iter1(f,a) = iter2(f,a)";
+Goal "iter1(f,a) = iter2(f,a)";
by (eq_coinduct3_tac
"{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
1);