theory tut06 imports Main "~~/src/HOL/IMP/Big_Step" "~~/src/HOL/IMP/Small_Step" begin definition Or :: "bexp \ bexp \ bexp" where "Or b1 b2 = Not (And (Not b1) (Not b2))" term "IF And b1 b2 THEN c1 ELSE c2 \ IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2" term "WHILE And b1 b2 DO c \ WHILE b1 DO WHILE b2 DO c" term "WHILE And b1 b2 DO c \ WHILE b1 DO c;; WHILE And b1 b2 DO c" term "~ (WHILE And (Bc True) (Bc False) DO c \ WHILE (Bc True) DO c;; WHILE And (Bc True) (Bc False) DO c)" thm big_step_induct thm big_step.induct lemma cond_after_while: "(WHILE b DO c, s) \ t \ \ bval b t" proof (induction "WHILE b DO c" s t rule: big_step_induct) case WhileFalse then show ?case . next case (WhileTrue s\<^sub>1 s\<^sub>2 s\<^sub>3) then show ?case by simp qed lemma "WHILE Or b1 b2 DO c \ WHILE Or b1 b2 DO c;; WHILE b1 DO c" unfolding Or_def using cond_after_while by force+ lemma "IF And b1 b2 THEN c1 ELSE c2 \ IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2" (is "?a \ ?c") proof - { fix s t { assume A: "(?a, s) \ t" have "(?c, s) \ t" proof (cases "bval b1 s \ bval b2 s") case True with A show ?thesis by auto next case False with A show ?thesis by auto qed } moreover { assume "(?c, s) \ t" then have "(?a, s) \ t" by auto } ultimately have "(?a, s) \ t \ (?c, s) \ t" by blast } then show ?thesis by simp qed end