theory tut04 imports Main "~~/src/HOL/IMP/ASM" begin inductive star :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" where refl: "star R x x" | step: "star R x y \ R y z \ star R x z" lemma "star R x y \ R y z \ star R x z" by (rule star.intros(2)) thm star.induct lemma star_prepend: "\star R y z; R x y\ \ star R x z" by (induction rule: star.induct) (auto intro: refl step) inductive star' :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" where refl': "star' R x x" | step': "\R x y; star' R y z\ \ star' R x z" lemma star'_append: "\star' R x y; R y z\ \ star' R x z" by (induction rule: star'.induct) (auto intro: refl' step') lemma "star R x y \ star' R x y" proof assume "star R x y" then show "star' R x y" by (induction rule: star.induct) (auto intro: refl' star'_append) next assume "star' R x y" then show "star R x y" by (induction rule: star'.induct) (auto intro: refl star_prepend) qed lemma assumes total: "\ x y. T x y \ T y x" -- "T is total" and anti: "\ x y. A x y \ A y x \ x = y" -- "A is antisymmetric" and subset: "\ x y. T x y \ A x y" -- "T is a subset of A" shows "A x y \ T x y" -- "A is a subset of T" proof - 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 "T x y" . next assume "T y x" with subset have "A y x" by simp with anti \A x y\ have "x = y" by simp with \T y x\ show "T x y" by simp qed 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 = ( if length stk \ 2 then Some ((hd2 stk + hd stk) # tl2 stk) else None)" fun exec :: "instr list \ state \ stack \ stack option" where "exec [] _ stk = Some stk" | "exec (i#is) s stk = ( case exec1 i s stk of None \ None | Some stk' \ exec is s stk')" lemma exec_append[simp]: "exec is1 s stk = Some stk' \ exec (is1@is2) s stk = exec is2 s stk'" by(induction is1 arbitrary: stk) (auto split: option.split) theorem exec_comp: "exec (comp a) s stk = Some (aval a s # stk)" by(induction a arbitrary: stk) auto end