(*<*) theory ex12 imports Main "HOL-IMP.Small_Step" "HOL-IMP.Sem_Equiv" "HOL-IMP.Vars" begin (*>*) text \\ExerciseSheet{12}{27.01.2020}\ text \ \Exercise{Inverse Analysis} Consider a simple sign analysis based on this abstract domain: \ datatype sign = None | Neg | Pos0 | Any fun \ :: "sign \ val set" where "\ None = {}" | "\ Neg = {i. i < 0}" | "\ Pos0 = {i. i \ 0}" | "\ Any = UNIV" text\ Define inverse analyses for ``@{text"+"}'' and ``@{text"<"}'' and prove the required correctness properties: \ fun inv_plus' :: "sign \ sign \ sign \ sign * sign" (*<*)where "inv_plus' Any a1 a2 = (a1,a2)" | "inv_plus' None a1 a2 = (None,None)" | "inv_plus' a None a2 = (None,None)" | "inv_plus' a a1 None = (None,None)" | "inv_plus' Pos0 Neg Any = (Neg,Pos0)" | "inv_plus' Pos0 Any Neg = (Pos0,Neg)" | "inv_plus' Pos0 Neg Neg = (None,None)" | "inv_plus' Pos0 a1 a2 = (a1,a2)" | "inv_plus' Neg Pos0 Any = (Pos0,Neg)" | "inv_plus' Neg Any Pos0 = (Neg,Pos0)" | "inv_plus' Neg Pos0 Pos0 = (None,None)" | "inv_plus' Neg a1 a2 = (a1,a2)" (*>*) fun inv_plus1 where "inv_plus1 Neg Neg = Any" | "inv_plus1 Neg Pos0 = Neg" | "inv_plus1 Pos0 Neg = Pos0" | "inv_plus1 Pos0 Pos0 = Any" | "inv_plus1 None _ = None" | "inv_plus1 _ None = None" | "inv_plus1 Any _ = Any" | "inv_plus1 _ Any = Any" fun meet where "meet Any x = x" | "meet x Any = x" | "meet Pos0 Pos0 = Pos0" | "meet Neg Neg = Neg" | "meet _ _ = None" definition inv_plus2 where "inv_plus2 v v1 v2 = (meet v1 (inv_plus1 v v2), meet v2 (inv_plus1 v v1))" lemma "\ inv_plus2 a a1 a2 = (a1',a2'); i1 \ \ a1; i2 \ \ a2; i1+i2 \ \ a \ \ i1 \ \ a1' \ i2 \ \ a2' " unfolding inv_plus2_def apply (cases a; cases a1; cases a2) apply auto done lemma "\ inv_plus' a a1 a2 = (a1',a2'); i1 \ \ a1; i2 \ \ a2; i1+i2 \ \ a \ \ i1 \ \ a1' \ i2 \ \ a2' " (*<*) by (induction a a1 a2 rule: inv_plus'.induct) auto (*>*) fun inv_less' :: "bool \ sign \ sign \ sign * sign" (*<*)where "inv_less' _ None _ = (None,None)" | "inv_less' _ _ None = (None,None)" | "inv_less' True Pos0 Neg = (None,None)" | "inv_less' True Pos0 Any = (Pos0,Pos0)" | "inv_less' True Any Neg = (Neg,Neg)" | "inv_less' True a1 a2 = (a1,a2)" | "inv_less' False Neg Pos0 = (None,None)" | "inv_less' False Any Pos0 = (Pos0,Pos0)" | "inv_less' False Neg Any = (Neg,Neg)" | "inv_less' False a1 a2 = (a1,a2)" (*>*) lemma "\ inv_less' bv a1 a2 = (a1',a2'); i1 \ \ a1; i2 \ \ a2; (i1 \ i1 \ \ a1' \ i2 \ \ a2'" (*<*) by (induction bv a1 a2 rule: inv_less'.induct) auto (*>*) text \ \Exercise{Command Equivalence} Recall the notion of \emph{command equivalence}: @{text [display] "c\<^sub>1 \ c\<^sub>2 \ (\s t. (c\<^sub>1, s) \ t \ (c\<^sub>2, s) \ t)"} \ (*<*) fun is_SKIP where "is_SKIP SKIP \ True" | "is_SKIP (x ::= a) \ False" | "is_SKIP (c\<^sub>1 ;; c\<^sub>2) \ is_SKIP c\<^sub>1 \ is_SKIP c\<^sub>2" | "is_SKIP (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \ is_SKIP c\<^sub>1 \ is_SKIP c\<^sub>2" | "is_SKIP (WHILE b DO c) \ False" lemma assumes "is_SKIP c" shows "c \ SKIP" \<^cancel>\using assms apply (induction c rule: is_SKIP.induct) apply auto apply fastforce+ apply blast done\ using \is_SKIP c\ proof (induction c rule: is_SKIP.induct) case 1 then show ?case by simp next case (2 x a) from \is_SKIP (x ::= a)\ have False by simp then show ?case by auto next case (3 c\<^sub>1 c\<^sub>2) from \is_SKIP (c\<^sub>1;; c\<^sub>2)\ have "is_SKIP c\<^sub>1" "is_SKIP c\<^sub>2" by auto with 3 have *: "c\<^sub>1 \ SKIP" "c\<^sub>2 \ SKIP" by auto show ?case proof safe fix s t s\<^sub>2 assume A: "(c\<^sub>1, s) \ s\<^sub>2" "(c\<^sub>2, s\<^sub>2) \ t" from A(1) *(1) have "s\<^sub>2 = s" by auto moreover from A(2) *(2) have "t = s\<^sub>2" by auto ultimately show "(SKIP, s) \ t" by auto next fix s t from * have "(c\<^sub>1, s) \ s" "(c\<^sub>2, s) \ s" by auto then show "(c\<^sub>1;; c\<^sub>2, s) \ s" by auto qed next case (4 b c\<^sub>1 c\<^sub>2) from \is_SKIP (IF b THEN c\<^sub>1 ELSE c\<^sub>2)\ have "is_SKIP c\<^sub>1" "is_SKIP c\<^sub>2" by auto with 4 have *: "c\<^sub>1 \ SKIP" "c\<^sub>2 \ SKIP" by auto { fix s have "(IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ s" using * by (cases "bval b s"; force) } with 4 show ?case by auto next case (5 b c) then have False by simp then show ?case by auto qed lemma big_step_simps: "(SKIP, s) \ t \ s = t" "(WHILE b DO c, s) \ t \ (if bval b s then (c ;; WHILE b DO c, s) \ t else s = t)" "(c ;; d, s) \ t \ (\s'. (c, s) \ s' \ (d, s') \ t)" "(IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \ t \ (if bval b s then (c\<^sub>1, s) \ t else (c\<^sub>2, s) \ t)" by auto lemma assumes "is_SKIP c" shows "c \ SKIP" using assms by (induct c) (auto simp: big_step_simps) lemma aux: "c \ SKIP \ (c,s) \ t \ s=t" by auto lemma sim_SKIPI: assumes "\s t. (c,s) \ t \ s=t" shows "c \ SKIP" using assms by auto lemma simSKIP_eq: "c \ SKIP \ (\s t. (c,s) \ t \ s=t)" by auto lemma assumes "is_SKIP c" shows "c \ SKIP" using assms proof (induction c) case (Seq c1 c2) note Seq.IH from \is_SKIP (c1;;c2)\ have "is_SKIP c1" "is_SKIP c2" by simp_all with Seq.IH have "c1\SKIP" "c2\SKIP" by auto show "c1;;c2 \ SKIP" proof (rule sim_SKIPI) fix s t have "(c1;; c2,s) \ t \ (\sh. (c1,s) \ sh \ (c2,sh) \ t)" apply (rule) apply (erule big_step.cases; simp) apply (rule exI; intro conjI; assumption) apply clarify apply (rule big_step.Seq; assumption) done also from aux[OF \c1\SKIP\] aux[OF \c2\SKIP\] have "\ \ s=t" by simp finally show "(c1;; c2, s) \ t \ (s = t)" . qed next case (If b c1 c2) note If.IH from \is_SKIP (IF b THEN c1 ELSE c2)\ have "is_SKIP c1" "is_SKIP c2" by simp_all with If.IH have "c1\SKIP" "c2\SKIP" by auto show "(IF b THEN c1 ELSE c2) \ SKIP" proof (rule sim_SKIPI, rule) fix s t assume "(IF b THEN c1 ELSE c2, s) \ t" hence "(c1,s) \ t \ (c2,s) \ t" by (cases; simp) with aux[OF \c1\SKIP\] aux[OF \c2\SKIP\] show "s=t" by simp next fix s t::state assume "s=t" with aux[OF \c1\SKIP\] aux[OF \c2\SKIP\] have "(c1,s) \ t" "(c2,s) \ t" by auto thus "(IF b THEN c1 ELSE c2, s) \ t" apply (cases "bval b s") apply (erule (1) big_step.IfTrue) apply (erule (1) big_step.IfFalse) done qed qed auto lemma not_sim: "(c\<^sub>1, s) \ t\<^sub>1 \ (c\<^sub>2, s) \ t\<^sub>2 \ \ (\x. t\<^sub>1 x = t\<^sub>2 x) \ \ (c\<^sub>1 \ c\<^sub>2)" by (metis big_step_determ) lemma equiv_up_to_if2: "bval b \ c \ c\<^sub>1 \ (\x. \ bval b x) \ c \ c\<^sub>2 \ c \ (IF b THEN c\<^sub>1 ELSE c\<^sub>2)" by (auto simp: equiv_up_to_def big_step_simps) lemma big_step_imp_eq_on: "(c, s) \ t \ s = t on - lvars c" by (induct rule: big_step_induct) auto lemma big_step_imp_bval_eq: "lvars c \ vars b = {} \ (c, s) \ t \ bval b s = bval b t" by (auto intro!: bval_eq_if_eq_on_vars dest: big_step_imp_eq_on) definition W where "W b\<^sub>1 b\<^sub>2 c\<^sub>1 c\<^sub>2 \ (WHILE b\<^sub>1 DO IF b\<^sub>2 THEN c\<^sub>1 ELSE c\<^sub>2) \ (IF b\<^sub>2 THEN WHILE b\<^sub>1 DO c\<^sub>1 ELSE WHILE b\<^sub>1 DO c\<^sub>2)" notepad begin define b\<^sub>1 where "b\<^sub>1 \ Not (Less (V ''x'') (N 0))" define b\<^sub>2 where "b\<^sub>2 \ Less (N 0) (V ''x'')" define c\<^sub>1 where "c\<^sub>1 \ ''x'' ::= N (-1)" define c\<^sub>2 where "c\<^sub>2 \ ''x'' ::= N 1" define s :: "vname \ val" where "s \ <''x'':=0>" have "(WHILE b\<^sub>1 DO IF b\<^sub>2 THEN c\<^sub>1 ELSE c\<^sub>2, s) \ <''x'':=-1>" unfolding b\<^sub>1_def b\<^sub>2_def c\<^sub>1_def c\<^sub>2_def s_def by fastforce (* Does not terminate *) have "\s t. \ (IF b\<^sub>2 THEN WHILE b\<^sub>1 DO c\<^sub>1 ELSE WHILE b\<^sub>1 DO c\<^sub>2, s) \ t" sorry end lemma WIF_eq_IFW: assumes "(lvars c\<^sub>1 \ lvars c\<^sub>2) \ vars b\<^sub>2 = {}" shows "W b\<^sub>1 b\<^sub>2 c\<^sub>1 c\<^sub>2" proof - have l: "lvars c\<^sub>1 \ vars b\<^sub>2 = {}" "lvars c\<^sub>2 \ vars b\<^sub>2 = {}" using assms by auto show ?thesis unfolding W_def by (intro equiv_up_to_if2 equiv_up_to_while_weak) (auto dest!: l[THEN big_step_imp_bval_eq]) qed (*>*) text \ \<^enum> Define a function @{text "is_SKIP :: com \ bool"} which holds on commands equivalent to @{const SKIP}. The function @{term is_SKIP} should be as precise as possible, but it should not analyse arithmetic or boolean expressions. Prove: @{term "is_SKIP c \ c \ SKIP"}\\ \<^enum> The following command equivalence is wrong. Give a counterexample in the form of concrete instances for @{text "b\<^sub>1"}, @{text "b\<^sub>2"}, @{text "c\<^sub>1"}, @{text "c\<^sub>2"}, and a state @{text s}. \\ \begin{equation} \begin{array}{l} @{term "WHILE b\<^sub>1 DO (IF b\<^sub>2 THEN c\<^sub>1 ELSE c\<^sub>2)"} \\ @{text "\ IF b\<^sub>2 THEN (WHILE b\<^sub>1 DO c\<^sub>1) ELSE (WHILE b\<^sub>1 DO c\<^sub>2)"} \end{array} \tag{@{text "*"}} \end{equation} \<^enum> Define a condition @{text P} on @{text "b\<^sub>1"}, @{text "b\<^sub>2"}, @{text "c\<^sub>1"}, and @{text "c\<^sub>2"} such that the previous statement @{text "(*)"} holds, i.e.\ @{text "P b\<^sub>1 b\<^sub>2 c\<^sub>1 c\<^sub>2 \ (*)"} Your condition should be as precise as possible, but only using: \begin{itemize} \item @{text "lvars :: com \ vname set"} (all left variables, i.e.\ written variables), \item @{text "rvars :: com \ vname set"} (all right variables, i.e.\ all read variables), \item @{text "vars :: bexp \ vname set"} (all variables in a condition), and \item boolean connectives and set operations \end{itemize} \ (*<*) end (*>*)