equal
deleted
inserted
replaced
58 |
58 |
59 lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t" |
59 lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t" |
60 by(metis while_option_stop2) |
60 by(metis while_option_stop2) |
61 |
61 |
62 theorem while_option_rule: |
62 theorem while_option_rule: |
63 assumes step: "!!s. P s ==> b s ==> P (c s)" |
63 assumes step: "!!s. P s ==> b s ==> P (c s)" |
64 and result: "while_option b c s = Some t" |
64 and result: "while_option b c s = Some t" |
65 and init: "P s" |
65 and init: "P s" |
66 shows "P t" |
66 shows "P t" |
67 proof - |
67 proof - |
68 def k == "LEAST k. ~ b ((c ^^ k) s)" |
68 define k where "k = (LEAST k. ~ 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: "ALL 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 |