equal
deleted
inserted
replaced
144 |
144 |
145 theorem prop2: |
145 theorem prop2: |
146 assumes ab: "a \<noteq> b" and bar: "bar xs" |
146 assumes ab: "a \<noteq> b" and bar: "bar xs" |
147 shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar |
147 shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar |
148 proof induct |
148 proof induct |
149 fix xs zs assume "good xs" and "T a xs zs" |
149 fix xs zs assume "T a xs zs" and "good xs" |
150 show "bar zs" by (rule bar1) (rule lemma3) |
150 hence "good zs" by (rule lemma3) |
|
151 then show "bar zs" by (rule bar1) |
151 next |
152 next |
152 fix xs ys |
153 fix xs ys |
153 assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" |
154 assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" |
154 assume "bar ys" |
155 assume "bar ys" |
155 thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" |
156 thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" |
156 proof induct |
157 proof induct |
157 fix ys zs assume "good ys" and "T b ys zs" |
158 fix ys zs assume "T b ys zs" and "good ys" |
158 show "bar zs" by (rule bar1) (rule lemma3) |
159 then have "good zs" by (rule lemma3) |
|
160 then show "bar zs" by (rule bar1) |
159 next |
161 next |
160 fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs" |
162 fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs" |
161 and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs" |
163 and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs" |
162 show "bar zs" |
164 show "bar zs" |
163 proof (rule bar2) |
165 proof (rule bar2) |
187 theorem prop3: |
189 theorem prop3: |
188 assumes bar: "bar xs" |
190 assumes bar: "bar xs" |
189 shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar |
191 shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar |
190 proof induct |
192 proof induct |
191 fix xs zs |
193 fix xs zs |
192 assume "good xs" and "R a xs zs" |
194 assume "R a xs zs" and "good xs" |
193 show "bar zs" by (rule bar1) (rule lemma2) |
195 then have "good zs" by (rule lemma2) |
|
196 then show "bar zs" by (rule bar1) |
194 next |
197 next |
195 fix xs zs |
198 fix xs zs |
196 assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs" |
199 assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs" |
197 and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs" |
200 and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs" |
198 show "bar zs" |
201 show "bar zs" |
297 proof induct |
300 proof induct |
298 case bar1 |
301 case bar1 |
299 thus ?case by iprover |
302 thus ?case by iprover |
300 next |
303 next |
301 case (bar2 ws) |
304 case (bar2 ws) |
302 have "is_prefix (f (length ws) # ws) f" by simp |
305 from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp |
303 thus ?case by (iprover intro: bar2) |
306 thus ?case by (iprover intro: bar2) |
304 qed |
307 qed |
305 |
308 |
306 theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs" |
309 theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs" |
307 using higman |
310 using higman |