theory Solution06_1
imports Main "HOL-IMP.Big_Step"
begin
section "Program Equivalence"
subsection "Part 1"
lemma "IF And b1 b2 THEN c1 ELSE c2 \ IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2"
proof -
let ?c1 = "IF And b1 b2 THEN c1 ELSE c2"
let ?c2 = "IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2"
have "(?c2, s) \ t" if a: "(?c1, s) \ t" for s t
proof (cases "bval b1 s \ bval b2 s")
case True
then show ?thesis using a by auto
next
case False
then show ?thesis using a by auto
qed
moreover
have "(?c1, s) \ t" if a: "(?c2, s) \ t" for s t
using a
by fastforce
ultimately
show ?thesis by auto
qed
text "With Sledgehammer:"
lemma "IF And b1 b2 THEN c1 ELSE c2 \ IF b1 THEN IF b2 THEN c1 ELSE c2 ELSE c2"
using IfTrue by fastforce
subsection "Part 2"
text "This pair is not equivalent. See the counterexample in the proof below."
lemma "\b1 b2 c. \ WHILE And b1 b2 DO c \ WHILE b1 DO WHILE b2 DO c"
proof -
let ?b1 = "Less (V ''a'') (N 1)" \\a < 1\
let ?b2 = "Less (V ''a'') (N 2)" \\a < 2\
let ?c = "''a'' ::= Plus (V ''a'') (N 1)"
let ?s = "<''a'' := 0>"
have "(WHILE And ?b1 ?b2 DO ?c, ?s) \ <''a'' := 1>"
apply (rule WhileTrue)
apply simp
apply (rule Assign)
apply simp
apply (rule WhileFalse)
apply simp
done
moreover
have "(WHILE ?b1 DO WHILE ?b2 DO ?c, ?s) \ <''a'' := 2>"
apply (rule WhileTrue)
apply simp
apply (rule WhileTrue)
apply simp
apply (rule Assign)
apply simp
apply (rule WhileTrue)
apply simp
apply (rule Assign)
apply simp
apply (rule WhileFalse)
apply simp
apply (rule WhileFalse)
apply simp
done
ultimately
show ?thesis
by (smt big_step_determ fun_upd_eqD)
qed
subsection "Part 3"
lemma "\b1 b2 c. \ WHILE And b1 b2 DO c \ WHILE b1 DO c ;; WHILE And b1 b2 DO c"
proof -
let ?b1 = "Less (V ''a'') (N 2)" \\a < 2\
let ?b2 = "Less (V ''a'') (N 1)" \\a < 1\
let ?c = "''a'' ::= N 4"
let ?s = "<''a'' := 1>"
have "(WHILE And ?b1 ?b2 DO ?c, ?s) \ <''a'' := 1>"
apply (rule WhileFalse)
apply simp
done
moreover
have "(WHILE ?b1 DO ?c ;; WHILE And ?b1 ?b2 DO ?c, ?s) \ <''a'' := 4>"
apply (rule Seq)
apply (rule WhileTrue)
apply simp
apply (rule Assign)
apply simp
apply (rule WhileFalse)
apply simp
apply (rule WhileFalse)
apply simp
done
ultimately
show ?thesis
by (smt big_step_determ fun_upd_eqD)
qed
subsection "Part 4"
definition Or :: "bexp \ bexp \ bexp" where
"Or b1 b2 = Not (And (Not b1) (Not b2))"
text "We need a lemma for this."
lemma While_end: "(WHILE b DO c, s) \ t \ \bval b t"
by (induction "WHILE b DO c" s t rule: big_step_induct) auto
lemma "WHILE Or b1 b2 DO c \ WHILE Or b1 b2 DO c;; WHILE b1 DO c"
proof -
have "\ bval b1 s" if *: "\ bval (Or b1 b2) s" for s
using * by (auto simp: Or_def)
then show ?thesis
by (blast intro!: While_end)
qed
end