equal
deleted
inserted
replaced
53 qed |
53 qed |
54 |
54 |
55 lemma while_option_stop2: |
55 lemma while_option_stop2: |
56 "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t" |
56 "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t" |
57 apply(simp add: while_option_def split: if_splits) |
57 apply(simp add: while_option_def split: if_splits) |
58 by (metis (lam_lifting) LeastI_ex) |
58 by (metis (lifting) LeastI_ex) |
59 |
59 |
60 lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t" |
60 lemma while_option_stop: "while_option b c s = Some t \<Longrightarrow> ~ b t" |
61 by(metis while_option_stop2) |
61 by(metis while_option_stop2) |
62 |
62 |
63 theorem while_option_rule: |
63 theorem while_option_rule: |