equal
deleted
inserted
replaced
86 apply safe |
86 apply safe |
87 apply (drule ListsXH [THEN iffD1]) |
87 apply (drule ListsXH [THEN iffD1]) |
88 apply (tactic "EQgen_tac @{context} [] 1") |
88 apply (tactic "EQgen_tac @{context} [] 1") |
89 prefer 2 |
89 prefer 2 |
90 apply blast |
90 apply blast |
91 apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1 |
91 apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1 |
92 THEN EQgen_tac @{context} [] 1) *}) |
92 THEN EQgen_tac @{context} [] 1) *}) |
93 done |
93 done |
94 |
94 |
95 |
95 |
96 subsection {* Appending anything to an infinite list doesn't alter it *} |
96 subsection {* Appending anything to an infinite list doesn't alter it *} |
133 |
133 |
134 lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)" |
134 lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)" |
135 apply (tactic {* eq_coinduct3_tac @{context} |
135 apply (tactic {* eq_coinduct3_tac @{context} |
136 "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*}) |
136 "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*}) |
137 apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong]) |
137 apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong]) |
138 apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *}) |
138 apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *}) |
139 apply (subst napply_f, assumption) |
139 apply (subst napply_f, assumption) |
140 apply (rule_tac f1 = f in napplyBsucc [THEN subst]) |
140 apply (rule_tac f1 = f in napplyBsucc [THEN subst]) |
141 apply blast |
141 apply blast |
142 done |
142 done |
143 |
143 |