theory Lsg03 imports Main begin text {* Setup to allow case on option in inductive *} lemma option_case_mono[mono]: "\ none_case \ none_case'; \y. some_case y \ some_case' y \ \ (case (x :: 'a option) of None \ none_case | Some y \ some_case y) \ (case x of None \ none_case' | Some y \ some_case' y)" by (auto split: option.split) section {* Basic definitions *} datatype instr = Set int | Add int | Mul int | Load string | Store string type_synonym vals = "string \ int" record state = vals :: vals accu :: int err :: bool type_synonym block = "instr list" fun mark_err :: "state \ state" where "mark_err s = (s \ err := True \)" (* define exec here *) fun init :: "(string \ int) \ int \ state" where "init vs a = \ vals = vs, accu = a, err = False \" lemma "exec (init [''x'' \ 3, ''y'' \ 4] 0) [ Load ''x'', Add 3 ] \ vals = [''x'' \ 3, ''y'' \ 4], accu= 6, err = False \" oops lemma "exec (init [''x'' \ 3, ''y'' \ 4] 0) [ Load ''x'', Mul 2, Store ''y'', Set 0 ] (\ vals = [''x'' \ 3, ''y'' \ 6], accu=0, err=False\)" oops lemma "exec (init [''x'' \ 3, ''y'' \ 4] 0) [ Load ''z'', Mul 2 ] (\ vals = [''x'' \ 3, ''y'' \ 4], accu=0, err=True\)" oops lemma "exec (init [''x'' \ 3, ''y'' \ 4] 0) [ Load ''x'', Add 3 ] \ vals = [''x'' \ 3, ''y'' \ 4], accu = 6, err = False\" oops (* define block_vars here *) lemma exec_success1: "\ exec s b s'; block_vars b \ dom (vals s); \ err s \ \ \ err s'" oops lemma exec_success2: "\ exec s b s'; block_vars b \ dom (vals s); \ err s \ \ \ err s'" oops lemma exec_success3: "\ exec s b s'; \ err s' \ \ block_vars b \ dom (vals s)" oops lemma exec_terminates: "\s. \s'. exec s b s'" oops lemma exec_success4: "\ block_vars b \ dom (vals s); \ err s \ \ \s'. exec s b s' \ \ err s'" apply (insert exec_terminates) apply (drule_tac x=b in meta_spec) apply (drule_tac x=s in spec) apply clarify apply (frule exec_success1) apply assumption+ apply fast done end