theory tut05
imports "~~/src/HOL/IMP/Big_Step"
begin
lemma equivI:
assumes "\s t. (c,s) \ t \ (c',s) \ t"
assumes "\s t. (c',s) \ t \ (c,s) \ t"
shows "c \ c'"
using assms by blast
lemma "IF And b1 b2 THEN c1 ELSE c2 \ IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2"
(is "?lhs \ ?rhs")
proof (rule equivI)
fix s t
assume "(?lhs,s) \ t"
from this show "(?rhs,s) \ t"
proof cases
case IfTrue
from this have 1: "bval b1 s" and 2: "bval b2 s" by (auto split: split_if_asm)
from this show ?thesis
apply -
apply (rule Big_Step.IfTrue)
apply (assumption)
apply (rule Big_Step.IfTrue)
apply (assumption)
by (rule IfTrue)
next
case IfFalse
hence "\bval b1 s \ \bval b2 s" by auto
moreover {
assume "\bval b1 s"
have ?thesis apply (rule Big_Step.IfFalse) by fact+
} moreover {
assume "bval b1 s" "\bval b2 s"
have ?thesis apply (rule IfTrue) apply fact apply (rule Big_Step.IfFalse) by fact+
} ultimately show ?thesis by blast
qed
next
fix s t
assume "(?rhs,s) \ t"
thus "(?lhs,s) \ t"
by (auto split: split_if_asm simp: IfTrue IfFalse)
qed
lemma "WHILE And b1 b2 DO c \ WHILE b1 DO WHILE b2 DO c"
oops
lemma "WHILE And b1 b2 DO c \ WHILE b1 DO c;; WHILE And b1 b2 DO c"
oops
definition Or :: "bexp \ bexp \ bexp" where
"Or b1 b2 = Not (And (Not b1 ) (Not b2 ))"
lemma while_not_c:
assumes "(WHILE b DO c,s) \ t"
shows "\bval b t"
using assms
thm big_step_induct
apply (induction "WHILE b DO c" _ _ arbitrary: b c rule: big_step_induct)
apply auto
done
lemma "WHILE Or b1 b2 DO c \ WHILE Or b1 b2 DO c;; WHILE b1 DO c"
apply (auto simp: Or_def)
apply (rule Seq)
apply assumption
apply (drule while_not_c)
apply (auto)
apply (frule while_not_c)
apply auto
done