theory Solution04 imports "HOL-IMP.ASM" begin section \Reflexive Transitive Closure\ 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 (induction 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" by (induction rule: star'.induct) (auto intro: star'.intros) lemma "star r x y = star' r x y" proof assume "star r x y" then show "star' r x y" by induction (auto intro: star'.intros star'_prepend) next assume "star' r x y" then show "star r x y" by induction (auto intro: star.intros star_append) qed section \Avoiding Stack Underflow\ 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#is) s stk = (case exec1 i s stk of Some stk \ exec is s stk | None \ None)" lemma exec_append[simp]: "exec (is1@is2) s stk = (case exec is1 s stk of Some stk \ exec is2 s stk | None \ None)" 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 section \A Structured Proof on Relations\ lemma structured_proof: assumes "\ x y. T x y \ T y x" and "\ x y. A x y \ A y x \ x = y" and "\ x y. T x y \ A x y" shows "A x y \ T x y" proof fix x y assume "A x y" from assms(1) 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 assms(3) have "A y x" by simp with \A x y\ assms(2) have "x = y" by simp with \T y x\ show ?thesis by simp qed qed end