# HG changeset patch # User kleing # Date 1363187035 -3600 # Node ID bdf772742e5ab8f58bf2cdae3e90cdd1a562591a # Parent c475a3983431479e1ac5fa184c4377b23ee85607# Parent deb59caefdb3c244823e66439ae53dbe86806e88 merged diff -r deb59caefdb3 -r bdf772742e5a src/HOL/IMP/Sec_Typing.thy --- a/src/HOL/IMP/Sec_Typing.thy Wed Mar 13 14:33:15 2013 +0100 +++ b/src/HOL/IMP/Sec_Typing.thy Wed Mar 13 16:03:55 2013 +0100 @@ -5,6 +5,7 @@ subsection "Syntax Directed Typing" +text_raw{*\snip{sectypeDef}{0}{2}{% *} inductive sec_type :: "nat \ com \ bool" ("(_/ \ _)" [0,0] 50) where Skip: "l \ SKIP" | @@ -16,6 +17,7 @@ "\ max (sec b) l \ c\<^isub>1; max (sec b) l \ c\<^isub>2 \ \ l \ IF b THEN c\<^isub>1 ELSE c\<^isub>2" | While: "max (sec b) l \ c \ l \ WHILE b DO c" +text_raw{*}%endsnip*} code_pred (expected_modes: i => i => bool) sec_type . @@ -181,6 +183,7 @@ computation by an antimonotonicity rule. We introduce the standard system now and show the equivalence with our formulation. *} +text_raw{*\snip{sectypepDef}{0}{2}{% *} inductive sec_type' :: "nat \ com \ bool" ("(_/ \'' _)" [0,0] 50) where Skip': "l \' SKIP" | @@ -194,6 +197,7 @@ "\ sec b \ l; l \' c \ \ l \' WHILE b DO c" | anti_mono': "\ l \' c; l' \ l \ \ l' \' c" +text_raw{*}%endsnip*} lemma sec_type_sec_type': "l \ c \ l \' c" apply(induction rule: sec_type.induct) @@ -215,6 +219,7 @@ subsection "A Bottom-Up Typing System" +text_raw{*\snip{sectypebDef}{0}{2}{% *} inductive sec_type2 :: "com \ level \ bool" ("(\ _ : _)" [0,0] 50) where Skip2: "\ SKIP : l" | @@ -227,6 +232,7 @@ \ \ IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" | While2: "\ sec b \ l; \ c : l \ \ \ WHILE b DO c : l" +text_raw{*}%endsnip*} lemma sec_type2_sec_type': "\ c : l \ l \' c"