equal
deleted
inserted
replaced
66 shows "P t" |
66 shows "P t" |
67 proof - |
67 proof - |
68 define k where "k = (LEAST k. \<not> b ((c ^^ k) s))" |
68 define k where "k = (LEAST k. \<not> b ((c ^^ k) s))" |
69 from assms have t: "t = (c ^^ k) s" |
69 from assms have t: "t = (c ^^ k) s" |
70 by (simp add: while_option_def k_def split: if_splits) |
70 by (simp add: while_option_def k_def split: if_splits) |
71 have 1: "ALL i<k. b ((c ^^ i) s)" |
71 have 1: "\<forall>i<k. b ((c ^^ i) s)" |
72 by (auto simp: k_def dest: not_less_Least) |
72 by (auto simp: k_def dest: not_less_Least) |
73 |
73 |
74 { fix i assume "i \<le> k" then have "P ((c ^^ i) s)" |
74 { fix i assume "i \<le> k" then have "P ((c ^^ i) s)" |
75 by (induct i) (auto simp: init step 1) } |
75 by (induct i) (auto simp: init step 1) } |
76 thus "P t" by (auto simp: t) |
76 thus "P t" by (auto simp: t) |