theory Ex07 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" proof (induction rule: sec_type2.induct) case (Seq2 c\<^sub>1 l\<^sub>1 c\<^sub>2 l\<^sub>2) then show ?case using Seq2' Subsumption2' by simp next case (If2 b l\<^sub>1 l\<^sub>2 c\<^sub>1 c\<^sub>2) then show ?case by (auto intro: sec_type2'.intros simp: Subsumption2') qed (auto intro: sec_type2'.intros) lemma "\' c : l \ \l' \ l. \ c : l'" proof (induction rule: sec_type2'.induct) case (Seq2' c\<^sub>1 l c\<^sub>2) then obtain l1 l2 where "l1\l" "\ c\<^sub>1 : l1" "l2\l" "\ c\<^sub>2 : l2" by auto moreover from \l \ l1\ \l \ l2\ have "l \ min l1 l2" by linarith ultimately show ?case using Seq2[of c\<^sub>1 l1 c\<^sub>2 l2] by blast next case (If2' b l c\<^sub>1 c\<^sub>2) then show ?case sorry next case (While2' b l c) then show ?case by (fastforce intro: sec_type2.intros) next case (Subsumption2' c l l') then show ?case using le_trans by blast 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" lemma AA_idem: "AA c (AA c A) = AA c A" sorry lemma AA_sound_gen: " (c, s) \ t \ \(x, a) \ A. s x = aval a s \ \(x, a) \ AA c A. t x = aval a t" proof (induction arbitrary: A rule: big_step_induct) case (Seq c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3) then show ?case by (fastforce split: prod.splits) next case (WhileTrue b s\<^sub>1 c s\<^sub>2 s\<^sub>3) from WhileTrue have "\(x,a) \ AA c A. s\<^sub>2 x = aval a s\<^sub>2" by simp with WhileTrue 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" by (simp add: AA_idem) ultimately show ?case by simp qed auto theorem AA_sound: "(c, s) \ t \ \(x, a) \ AA c {}. t x = aval a t" using AA_sound_gen by force fun gen :: "com \ (vname \ aexp) set" and kill :: "com \ (vname \ aexp) set" where "gen _ = undefined" 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" sorry end