theory Ex03_Tut_Sol imports "HOL-IMP.ASM" begin inductive star :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" for r where refl: "star r x x" | step: "r x y \ star r y z \ star r x z" lemma star_prepend: "\r x y; star r y z\ \ star r x z" by (rule step) lemma star_append: "\ star r x y; r y z \ \ star r x z" by (induct rule: star.induct) (auto intro: star.intros) inductive star' :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" for r where refl': "star' r x x" | step': "\star' r x y; r y z\ \ star' r x z" lemma star'_prepend: "\star' r y z; r x y\ \ star' r x z" apply (induction rule: star'.induct) apply (auto intro: star'.intros) done lemma "star r x y = star' r x y" proof assume "star r x y" thus "star' r x y" by induct (auto intro: star'.intros star'_prepend) next assume "star' r x y" thus "star r x y" by induct (auto intro: star.intros star_append) qed fun exec1 :: "instr \ state \ stack \ stack option" where "exec1 (LOADI n) _ stk = Some (n # stk)" | "exec1 (LOAD x) s stk = Some (s(x) # stk)" | "exec1 ADD _ stk = (case stk of a # b # c \ Some ((a + b) # c) | _ \ None)" fun exec :: "instr list \ state \ stack \ stack option" where "exec [] _ stk = Some stk" | "exec (i # ins) s stk = (case exec1 i s stk of Some stk \ exec ins s stk | None \ None)" lemma exec_append[simp]: "exec (ins1 @ ins2) s stk = (case exec ins1 s stk of Some stk \ exec ins2 s stk | None \ None)" apply(induction ins1 arbitrary: stk) apply (auto split: option.split) done theorem exec_comp: "exec (comp a) s stk = Some (aval a s # stk)" apply(induction a arbitrary: stk) apply (auto) done lemma assumes total: "\ x y. T x y \ T y x" and anti: "\ x y. A x y \ A y x \ x = y" and subset: "\ x y. T x y \ A x y" shows "A x y \ T x y" (* using assms by blast *) proof fix x y assume "A x y" from total have "T x y \ T y x" by simp then show "T x y" proof assume "T x y" then show ?thesis . next assume "T y x" with subset have "A y x" by simp with \A x y\ anti have "x = y" by simp with \T y x\ show ?thesis by simp qed qed end