theory Ex07_Tut_Sol imports "HOL-IMP.Small_Step" "HOL-IMP.Def_Init" "HOL-IMP.Sec_Typing" begin inductive sec_type2' :: "com \ level \ bool" ("(\'' _ : _)" [0,0] 50) where Skip2': "\' SKIP : l" | Assign2': "sec x \ sec a \ \' x ::= a : sec x" | Seq2': "\ \' c\<^sub>1 : l; \' c\<^sub>2 : l \ \ \' c\<^sub>1 ;; c\<^sub>2 : l" | If2': "\ sec b \ l; \' c\<^sub>1 : l; \' c\<^sub>2 : l \ \ \' IF b THEN c\<^sub>1 ELSE c\<^sub>2 : l" | While2': "\ sec b \ l; \' c : l \ \ \' WHILE b DO c : l" | Subsumption2': "\ \' c : l; l' \ l \ \ \' c : l'" lemma "\ c : l \ \' c : l" by (induction rule: sec_type2.induct) (auto intro: sec_type2'.intros simp: Subsumption2') lemma "\' c : l \ \l' \ l. \ c : l'" proof (induct rule: sec_type2'.induct) case (Seq2' c\<^sub>1 l c\<^sub>2) then obtain l\<^sub>1 l\<^sub>2 where "l\<^sub>1 \ l" "\ c\<^sub>1 : l\<^sub>1" "l\<^sub>2 \ l" "\ c\<^sub>2 : l\<^sub>2" by auto then show ?case using Seq2[of c\<^sub>1 l\<^sub>1 c\<^sub>2 l\<^sub>2] by (auto split: if_splits simp: min_def) next case (If2' b l c\<^sub>1 c\<^sub>2) then obtain l\<^sub>1 l\<^sub>2 where def: "l\<^sub>1 \ l" "\ c\<^sub>1 : l\<^sub>1" "l\<^sub>2 \ l" "\ c\<^sub>2 : l\<^sub>2" by auto with If2'.hyps(1) have "sec b \ min l\<^sub>1 l\<^sub>2" by linarith with def show ?case using If2[of b l\<^sub>1 l\<^sub>2 c\<^sub>1 c\<^sub>2] by (auto split: if_splits simp: min_def) next case (Subsumption2' c l l') then show ?case using order_trans by auto qed (auto intro!: sec_type2.intros) fun AA :: "com \ (vname \ aexp) set \ (vname \ aexp) set" where "AA SKIP A = A" | "AA (x ::= a) A = (if x \ vars a then {(x, a)} else {}) \ {(x', a'). (x', a') \ A \ x \ {x'} \ vars a'}" | "AA (c\<^sub>1;; c\<^sub>2) A = (AA c\<^sub>2 \ AA c\<^sub>1) A" | "AA (IF b THEN c\<^sub>1 ELSE c\<^sub>2) A = AA c\<^sub>1 A \ AA c\<^sub>2 A" | "AA (WHILE b DO c) A = A \ AA c A" theorem AA_sound: "(c, s) \ s' \ \(x, a) \ AA c {}. s' x = aval a s'" oops lemma AA_idem: "AA c (AA c A) = AA c A" sorry lemma AA_sound_aux: "(c, s) \ s' \ \ (x, a) \ A. s x = aval a s \ \ (x, a) \ AA c A. s' x = aval a s'" proof (induct arbitrary: A rule: big_step_induct) case (WhileTrue b s\<^sub>1 c s\<^sub>2 s\<^sub>3) then have "\(x, a) \ AA (WHILE b DO c) (AA c A). s\<^sub>3 x = aval a s\<^sub>3" by presburger moreover have "AA (WHILE b DO c) (AA c A) = (AA c A) \ AA c (AA c A)" by simp moreover have "AA c (AA c A) = AA c A" by (simp add: AA_idem) ultimately show ?case by simp qed (fastforce split: if_splits)+ theorem AA_sound: "(c, s) \ s' \ \(x, a) \ AA c {}. s' x = aval a s'" using AA_sound_aux[where A="{}"] by auto fun gen :: "com \ (vname \ aexp) set" and kill :: "com \ (vname \ aexp) set" where "gen SKIP = {}" | "gen (x ::= a) = (if x \ vars a then {(x, a)} else {})" | "gen (c1;; c2) = (gen c1 - kill c2) \ gen c2" | "gen (IF b THEN c1 ELSE c2) = gen c1 \ gen c2" | "gen (WHILE b DO c) = {}" | "kill SKIP = {}" | "kill (x ::= a) = {(x', a'). (x = x' \ a \ a') \ x \ vars a'}" | "kill (c1;; c2) = (kill c1 - gen c2) \ kill c2" | "kill (IF b THEN c1 ELSE c2) = kill c1 \ kill c2" | "kill (WHILE b DO c) = kill c" lemma "gen (''x''::=N 5;; ''x''::= N 6) = {(''x'',N 6)}" by simp lemma "(''x'', N 6) \ kill (''x''::=N 5;; ''x''::= N 6)" by simp lemma AA_gen_kill: "AA c A = (A \ gen c) - kill c" by (induction c arbitrary: A) auto lemma AA_idem': "AA c (AA c A) = AA c A" apply (simp add: AA_gen_kill) apply auto done end