theory Exercise08 imports Complex_Main "HOL-IMP.Sec_Type_Expr" begin declare [[names_short]] section "Security type systems" (* definitions from Sec_Typing copied here to avoid Sledgehammer finding lemmas that are not allowed here *) inductive sec_type :: "nat \ com \ bool" ("(_/ \ _)" [0,0] 50) where Skip: "l \ SKIP" | Assign: "\ sec x \ sec a; sec x \ l \ \ l \ x ::= a" | Seq: "\ l \ c\<^sub>1; l \ c\<^sub>2 \ \ l \ c\<^sub>1;;c\<^sub>2" | If: "\ max (sec b) l \ c\<^sub>1; max (sec b) l \ c\<^sub>2 \ \ l \ IF b THEN c\<^sub>1 ELSE c\<^sub>2" | While: "max (sec b) l \ c \ l \ WHILE b DO c" 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\<^sub>1; \ c\<^sub>2 : l\<^sub>2 \ \ \ c\<^sub>1;;c\<^sub>2 : min l\<^sub>1 l\<^sub>2 " | If2: "\ sec b \ min l\<^sub>1 l\<^sub>2; \ c\<^sub>1 : l\<^sub>1; \ c\<^sub>2 : l\<^sub>2 \ \ \ IF b THEN c\<^sub>1 ELSE c\<^sub>2 : min l\<^sub>1 l\<^sub>2" | While2: "\ sec b \ l; \ c : l \ \ \ WHILE b DO c : l" lemma bottom_up_impl_top_down: "\ c : l \ l \ c" sorry lemma top_down_impl_bottom_up: "l \ c \ \ l' \ l. \ c : l'" sorry section "Explicit type coercions" datatype val = Iv int | Rv real type_synonym vname = string type_synonym state = "vname \ val" datatype aexp = Ic int | Rc real | Real aexp | V vname | Plus aexp aexp datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp (* copy necessary parts from the Types theory *) (* define aelab, belab *) (* prove aprogress, apreservation, bprogress *) end