equal
deleted
inserted
replaced
91 proof (induction k arbitrary: s) |
91 proof (induction k arbitrary: s) |
92 case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0]) |
92 case 0 thus ?case by (auto simp: assms(1) intro: exI[of _ 0]) |
93 next |
93 next |
94 case (Suc k) |
94 case (Suc k) |
95 hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1) |
95 hence "\<not> b ((c^^k) (c s))" by (auto simp: funpow_swap1) |
96 then guess k by (rule exE[OF Suc.IH[of "c s"]]) |
96 from Suc.IH[OF this] obtain k where "\<not> b' ((c' ^^ k) (f (c s)))" .. |
97 with assms show ?case by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"]) |
97 with assms show ?case |
|
98 by (cases "b s") (auto simp: funpow_swap1 intro: exI[of _ "Suc k"] exI[of _ "0"]) |
98 qed |
99 qed |
99 next |
100 next |
100 fix k assume "\<not> b' ((c' ^^ k) (f s))" |
101 fix k assume "\<not> b' ((c' ^^ k) (f s))" |
101 thus "\<exists>k. \<not> b ((c ^^ k) s)" |
102 thus "\<exists>k. \<not> b ((c ^^ k) s)" |
102 proof (induction k arbitrary: s) |
103 proof (induction k arbitrary: s) |
105 case (Suc k) |
106 case (Suc k) |
106 hence *: "\<not> b' ((c'^^k) (c' (f s)))" by (auto simp: funpow_swap1) |
107 hence *: "\<not> b' ((c'^^k) (c' (f s)))" by (auto simp: funpow_swap1) |
107 show ?case |
108 show ?case |
108 proof (cases "b s") |
109 proof (cases "b s") |
109 case True |
110 case True |
110 with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp |
111 with assms(2) * have "\<not> b' ((c'^^k) (f (c s)))" by simp |
111 then guess k by (rule exE[OF Suc.IH[of "c s"]]) |
112 from Suc.IH[OF this] obtain k where "\<not> b ((c ^^ k) (c s))" .. |
112 thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"]) |
113 thus ?thesis by (auto simp: funpow_swap1 intro: exI[of _ "Suc k"]) |
113 qed (auto intro: exI[of _ "0"]) |
114 qed (auto intro: exI[of _ "0"]) |
114 qed |
115 qed |
115 next |
116 next |
116 fix k assume k: "\<not> b' ((c' ^^ k) (f s))" |
117 fix k assume k: "\<not> b' ((c' ^^ k) (f s))" |