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