diff --git a/UPF/Analysis.thy b/UPF/Analysis.thy index 1c81919..b416307 100644 --- a/UPF/Analysis.thy +++ b/UPF/Analysis.thy @@ -6,8 +6,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2008-2014 Achim D. Brucker, Germany - * 2009-2014 Université Paris-Sud, France + * 2008-2015 Achim D. Brucker, Germany + * 2009-2017 Université Paris-Sud, France + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -39,15 +40,14 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: Analysis.thy 10953 2014-11-24 11:23:40Z wolff $ *) section{* Properties on Policies *} theory Analysis -imports - ParallelComposition - SeqComposition + imports + ParallelComposition + SeqComposition begin text {* @@ -71,8 +71,8 @@ definition strictly_more_defined :: "('a \ 'b) \('a \ dom p)" lemma strictly_more_vs_more: "strictly_more_defined p q \ more_defined p q" -unfolding more_defined_def strictly_more_defined_def -by auto + unfolding more_defined_def strictly_more_defined_def + by auto text{* Policy p is more permissive than q: *} definition more_permissive :: "('a \ 'b) \ ('a \ 'b) \ bool" (infixl "\\<^sub>A" 60) @@ -82,58 +82,60 @@ where " p \\<^sub>A q = (\ x. (case q x of \allow y lemma more_permissive_refl : "p \\<^sub>A p " -unfolding more_permissive_def -by(auto split : option.split decision.split) - + unfolding more_permissive_def + by(auto split : option.split decision.split) + lemma more_permissive_trans : "p \\<^sub>A p' \ p' \\<^sub>A p'' \ p \\<^sub>A p''" -unfolding more_permissive_def -apply(auto split : option.split decision.split) -apply(erule_tac x = x and - P = "\x. case p'' x of \ \ True + unfolding more_permissive_def + apply(auto split : option.split decision.split) + subgoal for x y + apply(erule_tac x = x and + P = "\x. case p'' x of \ \ True | \allow y\ \ \z. p' x = \allow z\ | \deny y\ \ True" in allE) -apply(simp, elim exE) -by(erule_tac x = x in allE, simp) - + apply(simp, elim exE) + by(erule_tac x = x in allE, simp) + done text{* Policy p is more rejective than q: *} definition more_rejective :: "('a \ 'b) \ ('a \ 'b) \ bool" (infixl "\\<^sub>D" 60) -where " p \\<^sub>D q = (\ x. (case q x of \deny y\ \ (\ z. (p x = \deny z\)) + where " p \\<^sub>D q = (\ x. (case q x of \deny y\ \ (\ z. (p x = \deny z\)) | \allow y\ \ True | \ \ True))" - - + + lemma more_rejective_trans : "p \\<^sub>D p' \ p' \\<^sub>D p'' \ p \\<^sub>D p''" -unfolding more_rejective_def -apply(auto split : option.split decision.split) -apply(erule_tac x = x and - P = "\x. case p'' x of \ \ True + unfolding more_rejective_def + apply(auto split : option.split decision.split) + subgoal for x y + apply(erule_tac x = x and + P = "\x. case p'' x of \ \ True | \allow y\ \ True | \deny y\ \ \z. p' x = \deny z\" in allE) -apply(simp, elim exE) -by(erule_tac x = x in allE, simp) - + apply(simp, elim exE) + by(erule_tac x = x in allE, simp) + done lemma more_rejective_refl : "p \\<^sub>D p " -unfolding more_rejective_def -by(auto split : option.split decision.split) - - + unfolding more_rejective_def + by(auto split : option.split decision.split) + + lemma "A\<^sub>f f \\<^sub>A p" unfolding more_permissive_def allow_all_fun_def allow_pfun_def by(auto split: option.split decision.split) - + lemma "A\<^sub>I \\<^sub>A p" unfolding more_permissive_def allow_all_fun_def allow_pfun_def allow_all_id_def by(auto split: option.split decision.split) - + subsection{* Combined Data-Policy Refinement *} - + definition policy_refinement :: - "('a \ 'b) \ ('a' \ 'a) \('b' \ 'b) \ ('a' \ 'b') \ bool" - ("_ \\<^bsub>_\<^esub>\<^sub>,\<^bsub>_\<^esub> _" [50,50,50,50]50) -where "p \\<^bsub>abs\<^sub>a\<^esub>\<^sub>,\<^bsub>abs\<^sub>b\<^esub> q \ + "('a \ 'b) \ ('a' \ 'a) \('b' \ 'b) \ ('a' \ 'b') \ bool" + ("_ \\<^bsub>_\<^esub>\<^sub>,\<^bsub>_\<^esub> _" [50,50,50,50]50) + where "p \\<^bsub>abs\<^sub>a\<^esub>\<^sub>,\<^bsub>abs\<^sub>b\<^esub> q \ (\ a. case p a of \ \ True | \allow y\ \ (\ a'\{x. abs\<^sub>a x=a}. @@ -142,69 +144,72 @@ where "p \\<^bsub>abs\<^sub>a\<^esub>\<^sub>,\<^bsub>abs\<^sub>b | \deny y\ \ (\ a'\{x. abs\<^sub>a x=a}. \ b'. q a' = \deny b'\ \ abs\<^sub>b b' = y))" - + theorem polref_refl: "p \\<^bsub>id\<^esub>\<^sub>,\<^bsub>id\<^esub> p" -unfolding policy_refinement_def -by(auto split: option.split decision.split) - + unfolding policy_refinement_def + by(auto split: option.split decision.split) + theorem polref_trans: -assumes A: "p \\<^bsub>f\<^esub>\<^sub>,\<^bsub>g\<^esub> p'" -and B: "p' \\<^bsub>f'\<^esub>\<^sub>,\<^bsub>g'\<^esub> p''" -shows "p \\<^bsub>f o f'\<^esub>\<^sub>,\<^bsub>g o g'\<^esub> p''" -apply(insert A B) -unfolding policy_refinement_def -apply(auto split: option.split decision.split simp: o_def) -apply(erule_tac x="f (f' a')" in allE, simp) -apply(erule_tac x="f' a'" in allE, auto) -apply(erule_tac x=" (f' a')" in allE, auto) -apply(erule_tac x="f (f' a')" in allE, simp) -apply(erule_tac x="f' a'" in allE, auto) -apply(erule_tac x=" (f' a')" in allE, auto) -done - + assumes A: "p \\<^bsub>f\<^esub>\<^sub>,\<^bsub>g\<^esub> p'" + and B: "p' \\<^bsub>f'\<^esub>\<^sub>,\<^bsub>g'\<^esub> p''" + shows "p \\<^bsub>f o f'\<^esub>\<^sub>,\<^bsub>g o g'\<^esub> p''" + apply(insert A B) + unfolding policy_refinement_def + apply(auto split: option.split decision.split simp: o_def)[1] + subgoal for a a' + apply(erule_tac x="f (f' a')" in allE, simp)[1] + apply(erule_tac x="f' a'" in allE, auto)[1] + apply(erule_tac x=" (f' a')" in allE, auto)[1] + done + subgoal for a a' + apply(erule_tac x="f (f' a')" in allE, simp)[1] + apply(erule_tac x="f' a'" in allE, auto)[1] + apply(erule_tac x=" (f' a')" in allE, auto)[1] + done + done subsection {* Equivalence of Policies *} subsubsection{* Equivalence over domain D *} - + definition p_eq_dom :: "('a \ 'b) \ 'a set \ ('a \ 'b) \bool" ("_ \\<^bsub>_\<^esub> _" [60,60,60]60) -where "p \\<^bsub>D\<^esub> q = (\x\D. p x = q x)" - + where "p \\<^bsub>D\<^esub> q = (\x\D. p x = q x)" + text{* p and q have no conflicts *} definition no_conflicts :: "('a \ 'b) \('a \ 'b) \bool" where - "no_conflicts p q = (dom p = dom q \ (\x\(dom p). + "no_conflicts p q = (dom p = dom q \ (\x\(dom p). (case p x of \allow y\ \ (\z. q x = \allow z\) | \deny y\ \ (\z. q x = \deny z\))))" - + lemma policy_eq: assumes p_over_qA: "p \\<^sub>A q " - and q_over_pA: "q \\<^sub>A p" - and p_over_qD: "q \\<^sub>D p" - and q_over_pD: "p \\<^sub>D q" - and dom_eq: "dom p = dom q" -shows "no_conflicts p q" + and q_over_pA: "q \\<^sub>A p" + and p_over_qD: "q \\<^sub>D p" + and q_over_pD: "p \\<^sub>D q" + and dom_eq: "dom p = dom q" + shows "no_conflicts p q" apply (insert p_over_qA q_over_pA p_over_qD q_over_pD dom_eq) apply (simp add: no_conflicts_def more_permissive_def more_rejective_def - split: option.splits decision.splits) + split: option.splits decision.splits) apply (safe) - apply (metis domI domIff dom_eq) - apply (metis)+ -done - + apply (metis domI domIff dom_eq) + apply (metis)+ + done + subsubsection{* Miscellaneous *} - + lemma dom_inter: "\dom p \ dom q = {}; p x = \y\\ \ q x = \" by (auto) - + lemma dom_eq: "dom p \ dom q = {} \ p \\<^sub>A q = p \\<^sub>D q" unfolding override_A_def override_D_def by (rule ext, auto simp: dom_def split: prod.splits option.splits decision.splits ) - + lemma dom_split_alt_def : "(f, g) \ p = (dom(p \ Allow) \ (A\<^sub>f f)) \ (dom(p \ Deny) \ (D\<^sub>f g))" apply (rule ext) apply (simp add: dom_split2_def Allow_def Deny_def dom_restrict_def - deny_all_fun_def allow_all_fun_def map_add_def) + deny_all_fun_def allow_all_fun_def map_add_def) apply (simp split: option.splits decision.splits) apply (auto simp: map_add_def o_def deny_pfun_def ran_restrict_def image_def) -done + done end diff --git a/UPF/ElementaryPolicies.thy b/UPF/ElementaryPolicies.thy index d4c4eae..4b8eae2 100644 --- a/UPF/ElementaryPolicies.thy +++ b/UPF/ElementaryPolicies.thy @@ -6,8 +6,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2008-2014 Achim D. Brucker, Germany - * 2009-2014 Université Paris-Sud, France + * 2008-2015 Achim D. Brucker, Germany + * 2009-2017 Université Paris-Sud, France + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -39,13 +40,12 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: ElementaryPolicies.thy 10945 2014-11-21 12:50:43Z wolff $ *) section{* Elementary Policies *} theory ElementaryPolicies -imports - UPFCore + imports + UPFCore begin text{* In this theory, we introduce the elementary policies of UPF that build the basis @@ -86,30 +86,32 @@ notation (xsymbols) lemma AllD_norm[simp]: "deny_pfun (id o (\x. \x\)) = (\Dx. \x\)" by(simp add:id_def comp_def) - + lemma AllD_norm2[simp]: "deny_pfun (Some o id) = (\Dx. \x\)" by(simp add:id_def comp_def) - + lemma AllA_norm[simp]: "allow_pfun (id o Some) = (\Ax. \x\)" by(simp add:id_def comp_def) - + lemma AllA_norm2[simp]: "allow_pfun (Some o id) = (\Ax. \x\)" by(simp add:id_def comp_def) - + lemma AllA_apply[simp]: "(\Ax. Some (P x)) x = \allow (P x)\" by(simp add:allow_pfun_def) - + lemma AllD_apply[simp]: "(\Dx. Some (P x)) x = \deny (P x)\" by(simp add:deny_pfun_def) lemma neq_Allow_Deny: "pf \ \ \ (deny_pfun pf) \ (allow_pfun pf)" apply (erule contrapos_nn) apply (rule ext) - apply (drule_tac x=x in fun_cong) - apply (auto simp: deny_pfun_def allow_pfun_def) - apply (case_tac "pf x = \") - apply (auto) -done + subgoal for x + apply (drule_tac x=x in fun_cong) + apply (auto simp: deny_pfun_def allow_pfun_def) + apply (case_tac "pf x = \") + apply (auto) + done + done subsection{* Common Instances *} @@ -138,13 +140,11 @@ definition text{* ... and resulting properties: *} lemma "A\<^sub>I \ empty = A\<^sub>I" - apply simp - done - + by simp + lemma "A\<^sub>f f \ empty = A\<^sub>f f" - apply simp - done - + by simp + lemma "allow_pfun empty = empty" apply (rule ext) apply (simp add: allow_pfun_def) @@ -158,8 +158,7 @@ lemma allow_left_cancel :"dom pf = UNIV \ (allow_pfun pf) \ (deny_pfun pf) \ x = (deny_pfun pf)" apply (rule ext)+ - apply (auto simp: deny_pfun_def option.splits) - done + by (auto simp: deny_pfun_def option.splits) subsection{* Domain, Range, and Restrictions *} @@ -193,24 +192,28 @@ text{* However, some properties are specific to policy concepts: *} lemma sub_ran : "ran p \ Allow \ Deny" - apply (auto simp: Allow_def Deny_def ran_def full_SetCompr_eq[symmetric]) - apply (case_tac "x") - apply (simp_all) - apply (rename_tac \) - apply (erule_tac x="\" in allE) - apply (simp) - done - + apply (auto simp: Allow_def Deny_def ran_def full_SetCompr_eq[symmetric])[1] + subgoal for x a + apply (case_tac "x") + apply (simp_all) + apply (rename_tac \) + apply (erule_tac x="\" in allE) + apply (simp) + done + done + lemma dom_allow_pfun [simp]:"dom(allow_pfun f) = dom f" apply (auto simp: allow_pfun_def) - apply (case_tac "f x", simp_all) + subgoal for x y + apply (case_tac "f x", simp_all) + done done - + lemma dom_allow_all: "dom(A\<^sub>f f) = UNIV" by(auto simp: allow_all_fun_def o_def) lemma dom_deny_pfun [simp]:"dom(deny_pfun f) = dom f" - apply (auto simp: deny_pfun_def) + apply (auto simp: deny_pfun_def)[1] apply (case_tac "f x") apply (simp_all) done @@ -221,34 +224,44 @@ lemma dom_deny_all: " dom(D\<^sub>f f) = UNIV" lemma ran_allow_pfun [simp]:"ran(allow_pfun f) = allow `(ran f)" apply (simp add: allow_pfun_def ran_def) apply (rule set_eqI) - apply (auto) - apply (case_tac "f a") - apply (auto simp: image_def) - apply (rule_tac x=a in exI) - apply (simp) -done + apply (auto)[1] + subgoal for x a + apply (case_tac "f a") + apply (auto simp: image_def)[1] + apply (auto simp: image_def)[1] + done + subgoal for xa a + apply (rule_tac x=a in exI) + apply (simp) + done + done lemma ran_allow_all: "ran(A\<^sub>f id) = Allow" apply (simp add: allow_all_fun_def Allow_def o_def) apply (rule set_eqI) apply (auto simp: image_def ran_def) -done - + done + lemma ran_deny_pfun[simp]: "ran(deny_pfun f) = deny ` (ran f)" apply (simp add: deny_pfun_def ran_def) apply (rule set_eqI) - apply (auto) - apply (case_tac "f a") - apply (auto simp: image_def) - apply (rule_tac x=a in exI) - apply (simp) -done - + apply (auto)[1] + subgoal for x a + apply (case_tac "f a") + apply (auto simp: image_def)[1] + apply (auto simp: image_def)[1] + done + subgoal for xa a + apply (rule_tac x=a in exI) + apply (simp) + done + done + lemma ran_deny_all: "ran(D\<^sub>f id) = Deny" apply (simp add: deny_all_fun_def Deny_def o_def) apply (rule set_eqI) apply (auto simp: image_def ran_def) -done + done text{* @@ -272,23 +285,27 @@ where "S \ p \ (\x. if x \ S then p x else lemma dom_dom_restrict[simp] : "dom(S \ p) = S \ dom p" apply (auto simp: dom_restrict_def) - apply (case_tac "x \ S") - apply (simp_all) - apply (case_tac "x \ S") - apply (simp_all) -done + subgoal for x y + apply (case_tac "x \ S") + apply (simp_all) + done + subgoal for x y + apply (case_tac "x \ S") + apply (simp_all) + done + done lemma dom_restrict_idem[simp] : "(dom p) \ p = p" apply (rule ext) apply (auto simp: dom_restrict_def - dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]]) -done + dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]]) + done lemma dom_restrict_inter[simp] : "T \ S \ p = T \ S \ p" apply (rule ext) apply (auto simp: dom_restrict_def - dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]]) -done + dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]]) + done definition ran_restrict :: "['\\'\,'\ decision set] \ '\ \'\" (infixr "\" 55) where "p \ S \ (\x. if p x \ (Some`S) then p x else \)" @@ -299,38 +316,39 @@ where "p \2 S \ (\x. if (the (p x)) \ (S) lemma "ran_restrict = ran_restrict2" apply (rule ext)+ apply (simp add: ran_restrict_def ran_restrict2_def) - apply (case_tac "x xb") - apply simp_all - apply (metis inj_Some inj_image_mem_iff) -done - + subgoal for x xa xb + apply (case_tac "x xb") + apply simp_all + apply (metis inj_Some inj_image_mem_iff) + done + done lemma ran_ran_restrict[simp] : "ran(p \ S) = S \ ran p" by(auto simp: ran_restrict_def image_def ran_def) - + lemma ran_restrict_idem[simp] : "p \ (ran p) = p" apply (rule ext) apply (auto simp: ran_restrict_def image_def Ball_def ran_def) apply (erule contrapos_pp) apply (auto dest!: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]]) -done - + done + lemma ran_restrict_inter[simp] : "(p \ S) \ T = p \ T \ S" apply (rule ext) apply (auto simp: ran_restrict_def - dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]]) -done - + dest: neq_commute[THEN iffD1,THEN not_None_eq [THEN iffD1]]) + done + lemma ran_gen_A[simp] : "(\Ax. \P x\) \ Allow = (\Ax. \P x\)" apply (rule ext) apply (auto simp: Allow_def ran_restrict_def) -done - + done + lemma ran_gen_D[simp] : "(\Dx. \P x\) \ Deny = (\Dx. \P x\)" apply (rule ext) apply (auto simp: Deny_def ran_restrict_def) -done + done lemmas ElementaryPoliciesDefs = deny_pfun_def allow_pfun_def allow_all_fun_def deny_all_fun_def allow_all_id_def deny_all_id_def allow_all_def deny_all_def diff --git a/UPF/Monads.thy b/UPF/Monads.thy index 634e9e7..893c118 100644 --- a/UPF/Monads.thy +++ b/UPF/Monads.thy @@ -6,8 +6,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2009-2014 Univ. Paris-Sud, France - * 2009-2014 Achim D. Brucker, Germany + * 2009-2017 Univ. Paris-Sud, France + * 2009-2015 Achim D. Brucker, Germany + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -39,13 +40,12 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: Monads.thy 10922 2014-11-10 15:41:49Z wolff $ *) section {* Basic Monad Theory for Sequential Computations *} theory Monads -imports - Main + imports + Main begin subsection{* General Framework for Monad-based Sequence-Test *} @@ -109,21 +109,27 @@ text{* lemma bind_left_unit : "(x \ return a; k) = k" apply (simp add: unit_SE_def bind_SE_def) -done + done lemma bind_right_unit: "(x \ m; return x) = m" apply (simp add: unit_SE_def bind_SE_def) apply (rule ext) - apply (case_tac "m \") - apply ( simp_all) -done + subgoal for "\" + apply (case_tac "m \") + apply ( simp_all) + done + done lemma bind_assoc: "(y \ (x \ m; k); h) = (x \ m; (y \ k; h))" apply (simp add: unit_SE_def bind_SE_def) apply (rule ext) - apply (case_tac "m \", simp_all) - apply (case_tac "a", simp_all) -done + subgoal for "\" + apply (case_tac "m \", simp_all) + subgoal for a + apply (case_tac "a", simp_all) + done + done + done text{* In order to express test-sequences also on the object-level and to make our theory amenable to @@ -174,8 +180,8 @@ steps only by missing results ... *} fun mbind :: "'\ list \ ('\ \ ('o,'\) MON\<^sub>S\<^sub>E) \ ('o list,'\) MON\<^sub>S\<^sub>E" -where "mbind [] iostep \ = Some([], \)" | - "mbind (a#H) iostep \ = + where "mbind [] iostep \ = Some([], \)" | + "mbind (a#H) iostep \ = (case iostep a \ of None \ Some([], \) | Some (out, \') \ (case mbind H iostep \' of @@ -187,20 +193,26 @@ the current state is maintained, no result is reported. An alternative is the fail-strict variant @{text "mbind'"} defined below. *} lemma mbind_unit [simp]: "mbind [] f = (return [])" - by(rule ext, simp add: unit_SE_def) + by(rule ext, simp add: unit_SE_def) + lemma mbind_nofailure [simp]: "mbind S f \ \ None" apply (rule_tac x=\ in spec) apply (induct S) - apply (auto simp:unit_SE_def) - apply (case_tac "f a x") - apply ( auto) - apply (erule_tac x="b" in allE) - apply (erule exE) - apply (erule exE) - apply (simp) -done - + using mbind.simps(1) apply force + apply(simp add:unit_SE_def) + apply(safe)[1] + subgoal for a S x + apply (case_tac "f a x") + apply(simp) + apply(safe)[1] + subgoal for aa b + apply (erule_tac x="b" in allE) + apply (erule exE)+ + apply (simp) + done + done + done text{* The fail-strict version of @{text mbind'} looks as follows: *} fun mbind' :: "'\ list \ ('\ \ ('o,'\) MON\<^sub>S\<^sub>E) \ ('o list,'\) MON\<^sub>S\<^sub>E" @@ -237,12 +249,17 @@ lemma mbind_try: else (x \ mbind S F; M (the a' # x)))" apply (rule ext) apply (simp add: bind_SE_def try_SE_def) - apply (case_tac "F a x") - apply (auto) - apply (simp add: bind_SE_def try_SE_def) - apply (case_tac "mbind S F b") - apply (auto) -done + subgoal for x + apply (case_tac "F a x") + apply(simp) + apply (safe)[1] + apply (simp add: bind_SE_def try_SE_def) + subgoal for aa b + apply (case_tac "mbind S F b") + apply (auto) + done + done + done text{* On this basis, a symbolic evaluation scheme can be established that reduces @{term mbind}-code to @{term try_SE}-code and If-cascades. *} @@ -257,10 +274,10 @@ where "malt_SE S = foldr alt_SE S fail\<^sub>S\<^sub>E" notation malt_SE ("\\<^sub>S\<^sub>E") lemma malt_SE_mt [simp]: "\\<^sub>S\<^sub>E [] = fail\<^sub>S\<^sub>E" -by(simp add: malt_SE_def) + by(simp add: malt_SE_def) lemma malt_SE_cons [simp]: "\\<^sub>S\<^sub>E (a # S) = (a \\<^sub>S\<^sub>E (\\<^sub>S\<^sub>E S))" -by(simp add: malt_SE_def) + by(simp add: malt_SE_def) subsubsection{* State-Backtrack Monads *} text{*This subsection is still rudimentary and as such an interesting @@ -289,7 +306,7 @@ translations lemma bind_left_unit_SB : "(x := returns a; m) = m" apply (rule ext) apply (simp add: unit_SB_def bind_SB_def) -done + done lemma bind_right_unit_SB: "(x := m; returns x) = m" apply (rule ext) @@ -341,54 +358,59 @@ notation havoc_SBE ("havoc\<^sub>S\<^sub>B\<^sub>E") lemma bind_left_unit_SBE : "(x :\ returning a; m) = m" apply (rule ext) apply (simp add: unit_SBE_def bind_SBE_def) -done + done lemma bind_right_unit_SBE: "(x :\ m; returning x) = m" apply (rule ext) apply (simp add: unit_SBE_def bind_SBE_def) - apply (case_tac "m x") - apply (simp_all add:Let_def) - apply (rule HOL.ccontr) - apply (simp add: Set.image_iff) -done + subgoal for x + apply (case_tac "m x") + apply (simp_all add:Let_def) + apply (rule HOL.ccontr) + apply (simp add: Set.image_iff) + done + done lemmas aux = trans[OF HOL.neq_commute,OF Option.not_None_eq] lemma bind_assoc_SBE: "(y :\ (x :\ m; k); h) = (x :\ m; (y :\ k; h))" -proof (rule ext, simp add: unit_SBE_def bind_SBE_def, - case_tac "m x", simp_all add: Let_def Set.image_iff, safe) - case goal1 then show ?case - by(rule_tac x="(a, b)" in bexI, simp_all) +proof (rule ext, simp add: unit_SBE_def bind_SBE_def, rename_tac x, + case_tac "m x", simp_all add: Let_def Set.image_iff, safe,goal_cases) + case (1 x a aa b ab ba a b) + then show ?case by(rule_tac x="(a, b)" in bexI, simp_all) next - case goal2 then show ?case - apply (rule_tac x="(aa, b)" in bexI, simp_all add:split_def) - apply (erule_tac x="(aa,b)" in ballE) - apply (auto simp: aux image_def split_def intro!: rev_bexI) - done + case (2 x a aa b ab ba) + then show ?case + apply (rule_tac x="(aa, b)" in bexI, simp_all add:split_def) + apply (erule_tac x="(aa,b)" in ballE) + apply (auto simp: aux image_def split_def intro!: rev_bexI) + done next - case goal3 then show ?case - by(rule_tac x="(a, b)" in bexI, simp_all) + case (3 x a a b) + then show ?case by(rule_tac x="(a, b)" in bexI, simp_all) next - case goal4 then show ?case - apply (erule_tac Q="None = X" for X in contrapos_pp) - apply (erule_tac x="(aa,b)" and P="\ x. None \ case_prod (\out. k) x" in ballE) - apply (auto simp: aux (*Option.not_None_eq*) image_def split_def intro!: rev_bexI) - done -next - case goal5 then show ?case - apply simp apply ((erule_tac x="(ab,ba)" in ballE)+) - apply (simp_all add: aux (* Option.not_None_eq *), (erule exE)+, simp add:split_def) - apply (erule rev_bexI, case_tac "None\(\p. h(snd p))`y",auto simp:split_def) - done - + case (4 x a aa b) + then show ?case + apply (erule_tac Q="None = X" for X in contrapos_pp) + apply (erule_tac x="(aa,b)" and P="\ x. None \ case_prod (\out. k) x" in ballE) + apply (auto simp: aux image_def split_def intro!: rev_bexI) + done next - case goal6 then show ?case - apply simp apply ((erule_tac x="(a,b)" in ballE)+) - apply (simp_all add: aux (* Option.not_None_eq *), (erule exE)+, simp add:split_def) - apply (erule rev_bexI, case_tac "None\(\p. h(snd p))`y",auto simp:split_def) - done -qed - + case (5 x a aa b ab ba a b) + then show ?case apply simp apply ((erule_tac x="(ab,ba)" in ballE)+) + apply (simp_all add: aux, (erule exE)+, simp add:split_def) + apply (erule rev_bexI, case_tac "None\(\p. h(snd p))`y",auto simp:split_def) + done + +next + case (6 x a aa b a b) + then show ?case apply simp apply ((erule_tac x="(a,b)" in ballE)+) + apply (simp_all add: aux, (erule exE)+, simp add:split_def) + apply (erule rev_bexI, case_tac "None\(\p. h(snd p))`y",auto simp:split_def) + done +qed + + subsection{* Valid Test Sequences in the State Exception Monad *} text{* @@ -418,32 +440,32 @@ text{* Recall mbind\_unit for the base case. *} lemma valid_failure: "ioprog a \ = None \ (\ \ (s \ mbind (a#S) ioprog ; M s)) = (\ \ (M []))" -by(simp add: valid_SE_def unit_SE_def bind_SE_def) + by(simp add: valid_SE_def unit_SE_def bind_SE_def) lemma valid_failure': "A \ = None \ \(\ \ ((s \ A ; M s)))" -by(simp add: valid_SE_def unit_SE_def bind_SE_def) + by(simp add: valid_SE_def unit_SE_def bind_SE_def) lemma valid_successElem: (* atomic boolean Monad "Query Functions" *) "M \ = Some(f \,\) \ (\ \ M) = f \" -by(simp add: valid_SE_def unit_SE_def bind_SE_def ) + by(simp add: valid_SE_def unit_SE_def bind_SE_def ) lemma valid_success: "ioprog a \ = Some(b,\') \ (\ \ (s \ mbind (a#S) ioprog ; M s)) = (\' \ (s \ mbind S ioprog ; M (b#s)))" apply (simp add: valid_SE_def unit_SE_def bind_SE_def ) apply (cases "mbind S ioprog \'", auto) -done + done lemma valid_success'': "ioprog a \ = Some(b,\') \ (\ \ (s \ mbind (a#S) ioprog ; return (P s))) = (\' \ (s \ mbind S ioprog ; return (P (b#s))))" apply (simp add: valid_SE_def unit_SE_def bind_SE_def ) apply (cases "mbind S ioprog \'") - apply (simp_all) + apply (simp_all) apply (auto) -done + done lemma valid_success': "A \ = Some(b,\') \ (\ \ ((s \ A ; M s))) = (\' \ (M b))" by(simp add: valid_SE_def unit_SE_def bind_SE_def ) @@ -453,48 +475,47 @@ lemma valid_both: "(\ \ (s \ mbind (a#S) ioprog ; r None \ (\ \ (return (P []))) | Some(b,\') \ (\' \ (s \ mbind S ioprog ; return (P (b#s)))))" apply (case_tac "ioprog a \") - apply (simp_all add: valid_failure valid_success'' split: prod.splits) -done + apply (simp_all add: valid_failure valid_success'' split: prod.splits) + done lemma valid_propagate_1 [simp]: "(\ \ (return P)) = (P)" by(auto simp: valid_SE_def unit_SE_def) - + lemma valid_propagate_2: "\ \ ((s \ A ; M s)) \ \ v \'. the(A \) = (v,\') \ \' \ (M v)" apply (auto simp: valid_SE_def unit_SE_def bind_SE_def) apply (cases "A \") - apply (simp_all) + apply (simp_all) apply (drule_tac x="A \" and f=the in arg_cong) - apply (simp) + apply (simp) + apply (rename_tac a b aa ) apply (rule_tac x="fst aa" in exI) apply (rule_tac x="snd aa" in exI) - apply (auto) -done - - + by (auto) + lemma valid_propagate_2': "\ \ ((s \ A ; M s)) \ \ a. (A \) = Some a \ (snd a) \ (M (fst a))" apply (auto simp: valid_SE_def unit_SE_def bind_SE_def) apply (cases "A \") - apply (simp_all) + apply (simp_all) apply (simp_all split: prod.splits) apply (drule_tac x="A \" and f=the in arg_cong) apply (simp) + apply (rename_tac a b aa x1 x2) apply (rule_tac x="fst aa" in exI) apply (rule_tac x="snd aa" in exI) apply (auto) -done - - + done lemma valid_propagate_2'': "\ \ ((s \ A ; M s)) \ \ v \'. A \ = Some(v,\') \ \' \ (M v)" apply (auto simp: valid_SE_def unit_SE_def bind_SE_def) apply (cases "A \") - apply (simp_all) + apply (simp_all) apply (drule_tac x="A \" and f=the in arg_cong) apply (simp) + apply (rename_tac a b aa ) apply (rule_tac x="fst aa" in exI) apply (rule_tac x="snd aa" in exI) apply (auto) -done + done lemma valid_propoagate_3[simp]: "(\\<^sub>0 \ (\\. Some (f \, \))) = (f \\<^sub>0)" by(simp add: valid_SE_def ) @@ -513,18 +534,20 @@ lemma assert_disch3 :" \ P \ \ \ (\ \ \ (x \ assert\<^sub>S\<^sub>E P; M x)) \ P \ \ (\ \ (M True))" by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.if_split_asm) - + lemma assume_D : "(\ \ (x \ assume\<^sub>S\<^sub>E P; M x)) \ \ \. (P \ \ \ \ (M ()))" apply (auto simp: bind_SE_def assume_SE_def valid_SE_def split: HOL.if_split_asm) apply (rule_tac x="Eps P" in exI) - apply (auto) - apply (rule_tac x="True" in exI, rule_tac x="b" in exI) - apply (subst Hilbert_Choice.someI) - apply (assumption) + apply (auto)[1] + subgoal for x a b + apply (rule_tac x="True" in exI, rule_tac x="b" in exI) + apply (subst Hilbert_Choice.someI) + apply (assumption) apply (simp) + done apply (subst Hilbert_Choice.someI,assumption) apply (simp) -done + done text{* These two rule prove that the SE Monad in connection with the notion of valid sequence is @@ -532,45 +555,44 @@ text{* sets of states---to be shown below---is strictly speaking not necessary (and will therefore be discontinued in the development). *} - + lemma if_SE_D1 : "P \ \ (\ \ if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = (\ \ B\<^sub>1)" by(auto simp: if_SE_def valid_SE_def) - + lemma if_SE_D2 : "\ P \ \ (\ \ if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = (\ \ B\<^sub>2)" by(auto simp: if_SE_def valid_SE_def) - + lemma if_SE_split_asm : " (\ \ if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = ((P \ \ (\ \ B\<^sub>1)) \ (\ P \ \ (\ \ B\<^sub>2)))" by(cases "P \",auto simp: if_SE_D1 if_SE_D2) - + lemma if_SE_split : " (\ \ if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = ((P \ \ (\ \ B\<^sub>1)) \ (\ P \ \ (\ \ B\<^sub>2)))" by(cases "P \", auto simp: if_SE_D1 if_SE_D2) - + lemma [code]: "(\ \ m) = (case (m \) of None \ False | (Some (x,y)) \ x)" apply (simp add: valid_SE_def) apply (cases "m \ = None") - apply (simp_all) + apply (simp_all) apply (insert not_None_eq) apply (auto) -done - + done + subsection{* Valid Test Sequences in the State Exception Backtrack Monad *} text{* This is still an unstructured merge of executable monad concepts and specification oriented high-level properties initiating test procedures. *} - + definition valid_SBE :: "'\ \ ('a,'\) MON\<^sub>S\<^sub>B\<^sub>E \ bool" (infix "\\<^sub>S\<^sub>B\<^sub>E" 15) -where "\ \\<^sub>S\<^sub>B\<^sub>E m \ (m \ \ None)" + where "\ \\<^sub>S\<^sub>B\<^sub>E m \ (m \ \ None)" text{* This notation considers all non-failures as valid. *} - + lemma assume_assert: "(\ \\<^sub>S\<^sub>B\<^sub>E ( _ :\ assume\<^sub>S\<^sub>B\<^sub>E P ; assert\<^sub>S\<^sub>B\<^sub>E Q)) = (P \ \ Q \)" by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def) - + lemma assert_intro: "Q \ \ \ \\<^sub>S\<^sub>B\<^sub>E (assert\<^sub>S\<^sub>B\<^sub>E Q)" by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def) - - -(* legacy : lemmas valid_failure''=valid_failure *) + + end diff --git a/UPF/Normalisation.thy b/UPF/Normalisation.thy index d489001..2730764 100644 --- a/UPF/Normalisation.thy +++ b/UPF/Normalisation.thy @@ -5,8 +5,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2008-2014 Achim D. Brucker, Germany - * 2009-2014 Université Paris-Sud, France + * 2008-2015 Achim D. Brucker, Germany + * 2009-2017 Université Paris-Sud, France + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -38,203 +39,202 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: Normalisation.thy 10879 2014-10-26 11:35:31Z brucker $ *) section{* Policy Transformations *} theory Normalisation -imports - SeqComposition - ParallelComposition + imports + SeqComposition + ParallelComposition begin - + text{* This theory provides the formalisations required for the transformation of UPF policies. A typical usage scenario can be observed in the firewall case study~\cite{brucker.ea:formal-fw-testing:2014}. *} - + subsection{* Elementary Operators *} text{* We start by providing several operators and theorems useful when reasoning about a list of rules which should eventually be interpreted as combined using the standard override operator. *} - + text{* The following definition takes as argument a list of rules and returns a policy where the rules are combined using the standard override operator. *} definition list2policy::"('a \ 'b) list \ ('a \ 'b)" where "list2policy l = foldr (\ x y. (x \ y)) l \" - + text{* Determine the position of element of a list. *} fun position :: "'\ \ '\ list \ nat" where - "position a [] = 0" - |"(position a (x#xs)) = (if a = x then 1 else (Suc (position a xs)))" - + "position a [] = 0" +|"(position a (x#xs)) = (if a = x then 1 else (Suc (position a xs)))" + text{* Provides the first applied rule of a policy given as a list of rules. *} fun applied_rule where "applied_rule C a (x#xs) = (if a \ dom (C x) then (Some x) else (applied_rule C a xs))" - |"applied_rule C a [] = None" - +|"applied_rule C a [] = None" + text {* The following is used if the list is constructed backwards. *} definition applied_rule_rev where "applied_rule_rev C a x = applied_rule C a (rev x)" - + text{* The following is a typical policy transformation. It can be applied to any type of policy and removes all the rules from a policy with an empty domain. It takes two arguments: a semantic interpretation function and a list of rules. *} fun rm_MT_rules where - "rm_MT_rules C (x#xs) = (if dom (C x)= {} + "rm_MT_rules C (x#xs) = (if dom (C x)= {} then rm_MT_rules C xs else x#(rm_MT_rules C xs))" - |"rm_MT_rules C [] = []" - +|"rm_MT_rules C [] = []" + text {* The following invariant establishes that there are no rules with an empty domain in a list of rules. *} fun none_MT_rules where "none_MT_rules C (x#xs) = (dom (C x) \ {} \ (none_MT_rules C xs))" - |"none_MT_rules C [] = True" - +|"none_MT_rules C [] = True" + text{* The following related invariant establishes that the policy has not a completely empty domain. *} fun not_MT where "not_MT C (x#xs) = (if (dom (C x) = {}) then (not_MT C xs) else True)" - |"not_MT C [] = False" - +|"not_MT C [] = False" + text{* Next, a few theorems about the two invariants and the transformation: *} lemma none_MT_rules_vs_notMT: "none_MT_rules C p \ p \ [] \ not_MT C p" apply (induct p) - apply (simp_all) -done - + apply (simp_all) + done + lemma rmnMT: "none_MT_rules C (rm_MT_rules C p)" apply (induct p) - apply (simp_all) -done - + apply (simp_all) + done + lemma rmnMT2: "none_MT_rules C p \ (rm_MT_rules C p) = p" apply (induct p) - apply (simp_all) -done - + apply (simp_all) + done + lemma nMTcharn: "none_MT_rules C p = (\ r \ set p. dom (C r) \ {})" apply (induct p) - apply (simp_all) -done - + apply (simp_all) + done + lemma nMTeqSet: "set p = set s \ none_MT_rules C p = none_MT_rules C s" apply (simp add: nMTcharn) -done - + done + lemma notMTnMT: "\a \ set p; none_MT_rules C p\ \ dom (C a) \ {}" apply (simp add: nMTcharn) -done - + done + lemma none_MT_rulesconc: "none_MT_rules C (a@[b]) \ none_MT_rules C a" apply (induct a) - apply (simp_all) -done - + apply (simp_all) + done + lemma nMTtail: "none_MT_rules C p \ none_MT_rules C (tl p)" apply (induct p) - apply (simp_all) -done - + apply (simp_all) + done + lemma not_MTimpnotMT[simp]: "not_MT C p \ p \ []" apply (auto) -done - + done + lemma SR3nMT: "\ not_MT C p \ rm_MT_rules C p = []" apply (induct p) - apply (auto simp: if_splits) -done - + apply (auto simp: if_splits) + done + lemma NMPcharn: "\a \ set p; dom (C a) \ {}\ \ not_MT C p" apply (induct p) - apply (auto simp: if_splits) -done - + apply (auto simp: if_splits) + done + lemma NMPrm: "not_MT C p \ not_MT C (rm_MT_rules C p)" apply (induct p) - apply (simp_all) -done - + apply (simp_all) + done + text{* Next, a few theorems about applied\_rule: *} lemma mrconc: "applied_rule_rev C x p = Some a \ applied_rule_rev C x (b#p) = Some a" proof (induct p rule: rev_induct) -case Nil show ?case using Nil - by (simp add: applied_rule_rev_def) + case Nil show ?case using Nil + by (simp add: applied_rule_rev_def) next -case (snoc xs x) show ?case using snoc - apply (simp add: applied_rule_rev_def if_splits) - by (metis option.inject) + case (snoc xs x) show ?case using snoc + apply (simp add: applied_rule_rev_def if_splits) + by (metis option.inject) qed - + lemma mreq_end: "\applied_rule_rev C x b = Some r; applied_rule_rev C x c = Some r\ \ applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)" -by (simp add: mrconc) - + by (simp add: mrconc) + lemma mrconcNone: "applied_rule_rev C x p = None \ applied_rule_rev C x (b#p) = applied_rule_rev C x [b]" proof (induct p rule: rev_induct) -case Nil show ?case - by (simp add: applied_rule_rev_def) + case Nil show ?case + by (simp add: applied_rule_rev_def) next -case (snoc ys y) show ?case using snoc - proof (cases "x \ dom (C ys)") - case True show ?thesis using True snoc - by (auto simp: applied_rule_rev_def) - next - case False show ?thesis using False snoc - by (auto simp: applied_rule_rev_def) + case (snoc ys y) show ?case using snoc + proof (cases "x \ dom (C ys)") + case True show ?thesis using True snoc + by (auto simp: applied_rule_rev_def) + next + case False show ?thesis using False snoc + by (auto simp: applied_rule_rev_def) + qed qed -qed - + lemma mreq_endNone: "\applied_rule_rev C x b = None; applied_rule_rev C x c = None\ \ applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)" -by (metis mrconcNone) - + by (metis mrconcNone) + lemma mreq_end2: "applied_rule_rev C x b = applied_rule_rev C x c \ applied_rule_rev C x (a#b) = applied_rule_rev C x (a#c)" apply (case_tac "applied_rule_rev C x b = None") - apply (auto intro: mreq_end mreq_endNone) -done - + apply (auto intro: mreq_end mreq_endNone) + done + lemma mreq_end3: "applied_rule_rev C x p \ None \ applied_rule_rev C x (b # p) = applied_rule_rev C x (p)" -by (auto simp: mrconc) - + by (auto simp: mrconc) + lemma mrNoneMT: "\r \ set p; applied_rule_rev C x p = None\ \ x \ dom (C r)" proof (induct p rule: rev_induct) - case Nil show ?case using Nil - by (simp add: applied_rule_rev_def) - next - case (snoc y ys) show ?case using snoc + case Nil show ?case using Nil + by (simp add: applied_rule_rev_def) +next + case (snoc y ys) show ?case using snoc proof (cases "r \ set ys") - case True show ?thesis using snoc True - by (simp add: applied_rule_rev_def split: if_split_asm) - next - case False show ?thesis using snoc False - by (simp add: applied_rule_rev_def split: if_split_asm) - qed + case True show ?thesis using snoc True + by (simp add: applied_rule_rev_def split: if_split_asm) + next + case False show ?thesis using snoc False + by (simp add: applied_rule_rev_def split: if_split_asm) + qed qed - + subsection{* Distributivity of the Transformation. *} text{* @@ -259,23 +259,23 @@ fun prod_list :: "('\ \'\) \ (('\ \ \'\), (('\ \'\) list)] \ (('\ \ '\) \ 'y) \ ('x \ ('\ \ '\)) \ (('x \ 'y) list)" (infixr "\\<^sub>2\<^sub>L" 55) where "x \\<^sub>2\<^sub>L y = (\ d r. (x \\<^sub>L y) (op \\<^sub>2) d r)" - + lemma list2listNMT: "x \ [] \ map sem x \ []" apply (case_tac x) - apply (simp_all) -done - + apply (simp_all) + done + lemma two_conc: "(prod_list x (y#ys) p r d) = ((r o_f ((p x y) o d))#(prod_list x ys p r d))" -by simp + by simp text{* The following two invariants establish if the law of distributivity holds for a combinator @@ -293,136 +293,136 @@ lemma is_distr_orD: "is_distr (op \\<^sub>\\<^sub>D) d r" apply (rule allI)+ apply (rule distr_orD) apply (simp) -done - + done + lemma is_strict_orD: "is_strict (op \\<^sub>\\<^sub>D) d r" apply (simp add: is_strict_def) apply (simp add: policy_range_comp_def) -done - + done + lemma is_distr_2: "is_distr (op \\<^sub>2) d r" apply (simp add: is_distr_def) apply (rule allI)+ apply (rule distr_or2) -by simp - + by simp + lemma is_strict_2: "is_strict (op \\<^sub>2) d r" apply (simp only: is_strict_def) apply simp apply (simp add: policy_range_comp_def) -done - + done + lemma domStart: "t \ dom p1 \ (p1 \ p2) t = p1 t" apply (simp add: map_add_dom_app_simps) -done - + done + lemma notDom: "x \ dom A \ \ A x = None" apply auto -done - + done + text{* The following theorems are crucial: they establish the correctness of the distribution. *} lemma Norm_Distr_1: "((r o_f (((op \\<^sub>1) P1 (list2policy P2)) o d)) x = ((list2policy ((P1 \\<^sub>L P2) (op \\<^sub>1) r d)) x))" proof (induct P2) -case Nil show ?case - by (simp add: policy_range_comp_def list2policy_def) + case Nil show ?case + by (simp add: policy_range_comp_def list2policy_def) next -case (Cons p ps) show ?case using Cons - proof (cases "x \ dom (r o_f ((P1 \\<^sub>1 p) \ d))") - case True show ?thesis using True - by (auto simp: list2policy_def policy_range_comp_def prod_1_def - split: option.splits decision.splits prod.splits) - next - case False show ?thesis using Cons False - by (auto simp: list2policy_def policy_range_comp_def map_add_dom_app_simps(3) prod_1_def - split: option.splits decision.splits prod.splits) - qed + case (Cons p ps) show ?case using Cons + proof (cases "x \ dom (r o_f ((P1 \\<^sub>1 p) \ d))") + case True show ?thesis using True + by (auto simp: list2policy_def policy_range_comp_def prod_1_def + split: option.splits decision.splits prod.splits) + next + case False show ?thesis using Cons False + by (auto simp: list2policy_def policy_range_comp_def map_add_dom_app_simps(3) prod_1_def + split: option.splits decision.splits prod.splits) + qed qed - + lemma Norm_Distr_2: "((r o_f (((op \\<^sub>2) P1 (list2policy P2)) o d)) x = ((list2policy ((P1 \\<^sub>L P2) (op \\<^sub>2) r d)) x))"proof (induct P2) -case Nil show ?case - by (simp add: policy_range_comp_def list2policy_def) + case Nil show ?case + by (simp add: policy_range_comp_def list2policy_def) next -case (Cons p ps) show ?case using Cons - proof (cases "x \ dom (r o_f ((P1 \\<^sub>2 p) \ d))") - case True show ?thesis using True - by (auto simp: list2policy_def prod_2_def policy_range_comp_def - split: option.splits decision.splits prod.splits) - next - case False show ?thesis using Cons False - by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_2_def - split: option.splits decision.splits prod.splits) - qed + case (Cons p ps) show ?case using Cons + proof (cases "x \ dom (r o_f ((P1 \\<^sub>2 p) \ d))") + case True show ?thesis using True + by (auto simp: list2policy_def prod_2_def policy_range_comp_def + split: option.splits decision.splits prod.splits) + next + case False show ?thesis using Cons False + by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_2_def + split: option.splits decision.splits prod.splits) + qed qed - + lemma Norm_Distr_A: "((r o_f (((op \\<^sub>\\<^sub>A) P1 (list2policy P2)) o d)) x = ((list2policy ((P1 \\<^sub>L P2) (op \\<^sub>\\<^sub>A) r d)) x))" proof (induct P2) -case Nil show ?case - by (simp add: policy_range_comp_def list2policy_def) + case Nil show ?case + by (simp add: policy_range_comp_def list2policy_def) next -case (Cons p ps) show ?case using Cons - proof (cases "x \ dom (r o_f ((P1 \\<^sub>\\<^sub>A p) \ d))") - case True show ?thesis using True - by (auto simp: policy_range_comp_def list2policy_def prod_orA_def - split: option.splits decision.splits prod.splits) - next - case False show ?thesis using Cons False - by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orA_def - split: option.splits decision.splits prod.splits) - qed + case (Cons p ps) show ?case using Cons + proof (cases "x \ dom (r o_f ((P1 \\<^sub>\\<^sub>A p) \ d))") + case True show ?thesis using True + by (auto simp: policy_range_comp_def list2policy_def prod_orA_def + split: option.splits decision.splits prod.splits) + next + case False show ?thesis using Cons False + by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orA_def + split: option.splits decision.splits prod.splits) + qed qed - + lemma Norm_Distr_D: "((r o_f (((op \\<^sub>\\<^sub>D) P1 (list2policy P2)) o d)) x = ((list2policy ((P1 \\<^sub>L P2) (op \\<^sub>\\<^sub>D) r d)) x))" proof (induct P2) -case Nil show ?case - by (simp add: policy_range_comp_def list2policy_def) + case Nil show ?case + by (simp add: policy_range_comp_def list2policy_def) next -case (Cons p ps) show ?case using Cons - proof (cases "x \ dom (r o_f ((P1 \\<^sub>\\<^sub>D p) \ d))") - case True show ?thesis using True - by (auto simp: policy_range_comp_def list2policy_def prod_orD_def - split: option.splits decision.splits prod.splits) - next - case False show ?thesis using Cons False - by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orD_def - split: option.splits decision.splits prod.splits) - qed + case (Cons p ps) show ?case using Cons + proof (cases "x \ dom (r o_f ((P1 \\<^sub>\\<^sub>D p) \ d))") + case True show ?thesis using True + by (auto simp: policy_range_comp_def list2policy_def prod_orD_def + split: option.splits decision.splits prod.splits) + next + case False show ?thesis using Cons False + by (auto simp: policy_range_comp_def list2policy_def map_add_dom_app_simps(3) prod_orD_def + split: option.splits decision.splits prod.splits) + qed qed - + text {* Some domain reasoning *} lemma domSubsetDistr1: "dom A = UNIV \ dom ((\(x, y). x) o_f (A \\<^sub>1 B) o (\ x. (x,x))) = dom B" apply (rule set_eqI) apply (rule iffI) - apply (auto simp: prod_1_def policy_range_comp_def dom_def - split: decision.splits option.splits prod.splits) -done - + apply (auto simp: prod_1_def policy_range_comp_def dom_def + split: decision.splits option.splits prod.splits) + done + lemma domSubsetDistr2: "dom A = UNIV \ dom ((\(x, y). x) o_f (A \\<^sub>2 B) o (\ x. (x,x))) = dom B" apply (rule set_eqI) apply (rule iffI) - apply (auto simp: prod_2_def policy_range_comp_def dom_def - split: decision.splits option.splits prod.splits) -done - + apply (auto simp: prod_2_def policy_range_comp_def dom_def + split: decision.splits option.splits prod.splits) + done + lemma domSubsetDistrA: "dom A = UNIV \ dom ((\(x, y). x) o_f (A \\<^sub>\\<^sub>A B) o (\ x. (x,x))) = dom B" apply (rule set_eqI) apply (rule iffI) - apply (auto simp: prod_orA_def policy_range_comp_def dom_def - split: decision.splits option.splits prod.splits) -done - + apply (auto simp: prod_orA_def policy_range_comp_def dom_def + split: decision.splits option.splits prod.splits) + done + lemma domSubsetDistrD: "dom A = UNIV \ dom ((\(x, y). x) o_f (A \\<^sub>\\<^sub>D B) o (\ x. (x,x))) = dom B" apply (rule set_eqI) apply (rule iffI) apply (auto simp: prod_orD_def policy_range_comp_def dom_def - split: decision.splits option.splits prod.splits) -done + split: decision.splits option.splits prod.splits) + done end diff --git a/UPF/ParallelComposition.thy b/UPF/ParallelComposition.thy index bd2b8f0..02dd666 100644 --- a/UPF/ParallelComposition.thy +++ b/UPF/ParallelComposition.thy @@ -5,8 +5,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2008-2014 Achim D. Brucker, Germany - * 2009-2014 Université Paris-Sud, France + * 2008-2015 Achim D. Brucker, Germany + * 2009-2017 Université Paris-Sud, France + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -38,13 +39,12 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: ParallelComposition.thy 10879 2014-10-26 11:35:31Z brucker $ *) section{* Parallel Composition*} theory ParallelComposition -imports - ElementaryPolicies + imports + ElementaryPolicies begin text{* @@ -69,7 +69,7 @@ text {* *} definition prod_orA ::"['\\'\, '\ \'\] \ ('\\'\ \ '\\'\)" (infixr "\\<^sub>\\<^sub>A" 55) -where "p1 \\<^sub>\\<^sub>A p2 = + where "p1 \\<^sub>\\<^sub>A p2 = (\(x,y). (case p1 x of \allow d1\ \(case p2 y of \allow d2\ \ \allow(d1,d2)\ @@ -80,25 +80,25 @@ where "p1 \\<^sub>\\<^sub>A p2 = | \deny d2\ \ \deny (d1,d2)\ | \ \ \) | \ \ \))" - + lemma prod_orA_mt[simp]:"p \\<^sub>\\<^sub>A \ = \" apply (rule ext) apply (simp add: prod_orA_def) apply (auto) apply (simp split: option.splits decision.splits) -done + done lemma mt_prod_orA[simp]:"\ \\<^sub>\\<^sub>A p = \" apply (rule ext) apply (simp add: prod_orA_def) -done - + done + lemma prod_orA_quasi_commute: "p2 \\<^sub>\\<^sub>A p1 = (((\(x,y). (y,x)) o_f (p1 \\<^sub>\\<^sub>A p2))) o (\(a,b).(b,a))" apply (rule ext) apply (simp add: prod_orA_def policy_range_comp_def o_def) - apply (auto) + apply (auto)[1] apply (simp split: option.splits decision.splits) -done + done definition prod_orD ::"['\ \ '\, '\ \ '\] \ ('\ \ '\ \ '\ \ '\ )" (infixr "\\<^sub>\\<^sub>D" 55) where "p1 \\<^sub>\\<^sub>D p2 = @@ -116,28 +116,28 @@ where "p1 \\<^sub>\\<^sub>D p2 = lemma prod_orD_mt[simp]:"p \\<^sub>\\<^sub>D \ = \" apply (rule ext) apply (simp add: prod_orD_def) - apply (auto) + apply (auto)[1] apply (simp split: option.splits decision.splits) -done - + done + lemma mt_prod_orD[simp]:"\ \\<^sub>\\<^sub>D p = \" apply (rule ext) apply (simp add: prod_orD_def) -done - + done + lemma prod_orD_quasi_commute: "p2 \\<^sub>\\<^sub>D p1 = (((\(x,y). (y,x)) o_f (p1 \\<^sub>\\<^sub>D p2))) o (\(a,b).(b,a))" apply (rule ext) apply (simp add: prod_orD_def policy_range_comp_def o_def) - apply (auto) + apply (auto)[1] apply (simp split: option.splits decision.splits) -done + done text{* The following two combinators are by definition non-commutative, but still strict. *} - + definition prod_1 :: "['\\'\, '\ \'\] \ ('\\'\ \ '\\'\)" (infixr "\\<^sub>1" 55) -where "p1 \\<^sub>1 p2 \ + where "p1 \\<^sub>1 p2 \ (\(x,y). (case p1 x of \allow d1\\(case p2 y of \allow d2\ \ \allow(d1,d2)\ @@ -148,21 +148,21 @@ where "p1 \\<^sub>1 p2 \ | \deny d2\ \ \deny(d1,d2)\ | \ \ \) |\ \ \))" - + lemma prod_1_mt[simp]:"p \\<^sub>1 \ = \" apply (rule ext) apply (simp add: prod_1_def) - apply (auto) + apply (auto)[1] apply (simp split: option.splits decision.splits) -done - + done + lemma mt_prod_1[simp]:"\ \\<^sub>1 p = \" apply (rule ext) apply (simp add: prod_1_def) -done - + done + definition prod_2 :: "['\\'\, '\ \'\] \ ('\\'\ \ '\\'\)" (infixr "\\<^sub>2" 55) -where "p1 \\<^sub>2 p2 \ + where "p1 \\<^sub>2 p2 \ (\(x,y). (case p1 x of \allow d1\ \(case p2 y of \allow d2\ \ \allow(d1,d2)\ @@ -173,54 +173,54 @@ where "p1 \\<^sub>2 p2 \ | \deny d2\ \ \deny (d1,d2)\ | \ \ \) |\ \\))" - + lemma prod_2_mt[simp]:"p \\<^sub>2 \ = \" apply (rule ext) apply (simp add: prod_2_def) - apply (auto) + apply (auto)[1] apply (simp split: option.splits decision.splits) -done - + done + lemma mt_prod_2[simp]:"\ \\<^sub>2 p = \" apply (rule ext) apply (simp add: prod_2_def) -done - + done + definition prod_1_id ::"['\\'\, '\\'\] \ ('\ \ '\\'\)" (infixr "\\<^sub>1\<^sub>I" 55) -where "p \\<^sub>1\<^sub>I q = (p \\<^sub>1 q) o (\x. (x,x))" - + where "p \\<^sub>1\<^sub>I q = (p \\<^sub>1 q) o (\x. (x,x))" + lemma prod_1_id_mt[simp]:"p \\<^sub>1\<^sub>I \ = \" apply (rule ext) apply (simp add: prod_1_id_def) -done - + done + lemma mt_prod_1_id[simp]:"\ \\<^sub>1\<^sub>I p = \" apply (rule ext) apply (simp add: prod_1_id_def prod_1_def) -done - + done + definition prod_2_id ::"['\\'\, '\\'\] \ ('\ \ '\\'\)" (infixr "\\<^sub>2\<^sub>I" 55) -where"p \\<^sub>2\<^sub>I q = (p \\<^sub>2 q) o (\x. (x,x))" - + where"p \\<^sub>2\<^sub>I q = (p \\<^sub>2 q) o (\x. (x,x))" + lemma prod_2_id_mt[simp]:"p \\<^sub>2\<^sub>I \ = \" apply (rule ext) apply (simp add: prod_2_id_def) -done - + done + lemma mt_prod_2_id[simp]:"\ \\<^sub>2\<^sub>I p = \" apply (rule ext) apply (simp add: prod_2_id_def prod_2_def) -done - + done + subsection{* Combinators for Transition Policies *} text {* For constructing transition policies, two additional combinators are required: one combines state transitions by pairing the states, the other works equivalently on general maps. *} - + definition parallel_map :: "('\ \ '\) \ ('\ \ '\) \ ('\ \ '\ \ '\ \ '\)" (infixr "\\<^sub>M" 60) -where "p1 \\<^sub>M p2 = (\ (x,y). case p1 x of \d1\ \ + where "p1 \\<^sub>M p2 = (\ (x,y). case p1 x of \d1\ \ (case p2 y of \d2\ \ \(d1,d2)\ | \ \ \) | \ \ \)" @@ -249,81 +249,93 @@ lemma comp_ran_split_charn: "(f, g) \\<^sub>\ p = ( (((p \ Allow)\\<^sub>\\<^sub>A (A\<^sub>p f)) \ ((p \ Deny) \\<^sub>\\<^sub>A (D\<^sub>p g))))" - apply (rule ext) - apply (simp add: comp_ran_split_def map_add_def o_def ran_restrict_def image_def - Allow_def Deny_def dom_restrict_def prod_orA_def - allow_pfun_def deny_pfun_def - split:option.splits decision.splits) + apply (rule ext) + apply (simp add: comp_ran_split_def map_add_def o_def ran_restrict_def image_def + Allow_def Deny_def dom_restrict_def prod_orA_def + allow_pfun_def deny_pfun_def + split:option.splits decision.splits) apply (auto) -done + done subsection {* Distributivity of the parallel combinators *} - + lemma distr_or1_a: "(F = F1 \ F2) \ (((N \\<^sub>1 F) o f) = (((N \\<^sub>1 F1) o f) \ ((N \\<^sub>1 F2) o f))) " apply (rule ext) apply (simp add: prod_1_def map_add_def - split: decision.splits option.splits) - apply (case_tac "f x") - apply (simp_all add: prod_1_def map_add_def - split: decision.splits option.splits) -done + split: decision.splits option.splits) + subgoal for x + apply (case_tac "f x") + apply (simp_all add: prod_1_def map_add_def + split: decision.splits option.splits) + done + done lemma distr_or1: "(F = F1 \ F2) \ ((g o_f ((N \\<^sub>1 F) o f)) = ((g o_f ((N \\<^sub>1 F1) o f)) \ (g o_f ((N \\<^sub>1 F2) o f)))) " apply (rule ext)+ apply (simp add: prod_1_def map_add_def policy_range_comp_def - split: decision.splits option.splits) - apply (case_tac "f x") - apply (simp_all add: prod_1_def map_add_def - split: decision.splits option.splits) -done - + split: decision.splits option.splits) + subgoal for x + apply (case_tac "f x") + apply (simp_all add: prod_1_def map_add_def + split: decision.splits option.splits) + done + done + lemma distr_or2_a: "(F = F1 \ F2) \ (((N \\<^sub>2 F) o f) = (((N \\<^sub>2 F1) o f) \ ((N \\<^sub>2 F2) o f))) " apply (rule ext) apply (simp add: prod_2_id_def prod_2_def map_add_def - split: decision.splits option.splits) - apply (case_tac "f x") - apply (simp_all add: prod_2_def map_add_def - split: decision.splits option.splits) -done - + split: decision.splits option.splits) + subgoal for x + apply (case_tac "f x") + apply (simp_all add: prod_2_def map_add_def + split: decision.splits option.splits) + done + done + lemma distr_or2: "(F = F1 \ F2) \ ((r o_f ((N \\<^sub>2 F) o f)) = ((r o_f ((N \\<^sub>2 F1) o f)) \ (r o_f ((N \\<^sub>2 F2) o f)))) " apply (rule ext) apply (simp add: prod_2_id_def prod_2_def map_add_def policy_range_comp_def - split: decision.splits option.splits) - apply (case_tac "f x") - apply (simp_all add: prod_2_def map_add_def - split: decision.splits option.splits) -done - + split: decision.splits option.splits) + subgoal for x + apply (case_tac "f x") + apply (simp_all add: prod_2_def map_add_def + split: decision.splits option.splits) + done + done + lemma distr_orA: "(F = F1 \ F2) \ ((g o_f ((N \\<^sub>\\<^sub>A F) o f)) = ((g o_f ((N \\<^sub>\\<^sub>A F1) o f)) \ (g o_f ((N \\<^sub>\\<^sub>A F2) o f)))) " apply (rule ext)+ apply (simp add: prod_orA_def map_add_def policy_range_comp_def - split: decision.splits option.splits) - apply (case_tac "f x") - apply (simp_all add: map_add_def - split: decision.splits option.splits) -done - + split: decision.splits option.splits) + subgoal for x + apply (case_tac "f x") + apply (simp_all add: map_add_def + split: decision.splits option.splits) + done + done + lemma distr_orD: "(F = F1 \ F2) \ ((g o_f ((N \\<^sub>\\<^sub>D F) o f)) = ((g o_f ((N \\<^sub>\\<^sub>D F1) o f)) \ (g o_f ((N \\<^sub>\\<^sub>D F2) o f)))) " apply (rule ext)+ apply (simp add: prod_orD_def map_add_def policy_range_comp_def - split: decision.splits option.splits) - apply (case_tac "f x") - apply (simp_all add: map_add_def - split: decision.splits option.splits) -done - + split: decision.splits option.splits) + subgoal for x + apply (case_tac "f x") + apply (simp_all add: map_add_def + split: decision.splits option.splits) + done + done + lemma coerc_assoc: "(r o_f P) o d = r o_f (P o d)" apply (simp add: policy_range_comp_def) apply (rule ext) apply (simp split: option.splits decision.splits) -done + done lemmas ParallelDefs = prod_orA_def prod_orD_def prod_1_def prod_2_def parallel_map_def parallel_st_def comp_ran_split_def diff --git a/UPF/SeqComposition.thy b/UPF/SeqComposition.thy index ac378b9..b664882 100644 --- a/UPF/SeqComposition.thy +++ b/UPF/SeqComposition.thy @@ -5,8 +5,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2008-2014 Achim D. Brucker, Germany - * 2009-2014 Université Paris-Sud, France + * 2008-2015 Achim D. Brucker, Germany + * 2009-2017 Université Paris-Sud, France + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -38,13 +39,12 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: SeqComposition.thy 10879 2014-10-26 11:35:31Z brucker $ *) section{* Sequential Composition *} theory SeqComposition -imports - ElementaryPolicies + imports + ElementaryPolicies begin text{* @@ -62,14 +62,14 @@ where "flat_orA(allow(allow y)) = allow y" |"flat_orA(allow(deny y)) = allow y" |"flat_orA(deny(allow y)) = allow y" |"flat_orA(deny(deny y)) = deny y" - + lemma flat_orA_deny[dest]:"flat_orA x = deny y \ x = deny(deny y)" apply (case_tac "x") apply (rename_tac \) apply (case_tac "\", simp_all)[1] apply (rename_tac \) apply (case_tac "\", simp_all)[1] -done + done lemma flat_orA_allow[dest]: "flat_orA x = allow y \ x = allow(allow y) \ x = allow(deny y) @@ -79,21 +79,21 @@ lemma flat_orA_allow[dest]: "flat_orA x = allow y \ x = allow(al apply (case_tac "\", simp_all)[1] apply (rename_tac \) apply (case_tac "\", simp_all)[1] -done + done fun flat_orD :: "('\ decision) decision \ ('\ decision)" where "flat_orD(allow(allow y)) = allow y" |"flat_orD(allow(deny y)) = deny y" |"flat_orD(deny(allow y)) = deny y" |"flat_orD(deny(deny y)) = deny y" - + lemma flat_orD_allow[dest]: "flat_orD x = allow y \ x = allow(allow y)" apply (case_tac "x") apply (rename_tac \) apply (case_tac "\", simp_all)[1] apply (rename_tac \) apply (case_tac "\", simp_all)[1] -done + done lemma flat_orD_deny[dest]: "flat_orD x = deny y \ x = deny(deny y) \ x = allow(deny y) @@ -103,7 +103,7 @@ lemma flat_orD_deny[dest]: "flat_orD x = deny y \ x = deny(deny apply (case_tac "\", simp_all)[1] apply (rename_tac \) apply (case_tac "\", simp_all)[1] -done + done fun flat_1 :: "('\ decision) decision \ ('\ decision)" where "flat_1(allow(allow y)) = allow y" @@ -117,7 +117,7 @@ lemma flat_1_allow[dest]: "flat_1 x = allow y \ x = allow(allow apply (case_tac "\", simp_all)[1] apply (rename_tac \) apply (case_tac "\", simp_all)[1] -done + done lemma flat_1_deny[dest]: "flat_1 x = deny y \ x = deny(deny y) \ x = deny(allow y)" apply (case_tac "x") @@ -125,7 +125,7 @@ lemma flat_1_deny[dest]: "flat_1 x = deny y \ x = deny(deny y) apply (case_tac "\", simp_all)[1] apply (rename_tac \) apply (case_tac "\", simp_all)[1] -done + done fun flat_2 :: "('\ decision) decision \ ('\ decision)" where "flat_2(allow(allow y)) = allow y" @@ -147,7 +147,7 @@ lemma flat_2_deny[dest]: "flat_2 x = deny y \ x = deny(deny y) apply (case_tac "\", simp_all)[1] apply (rename_tac \) apply (case_tac "\", simp_all)[1] -done + done subsection{* Policy Composition *} text{* @@ -164,10 +164,11 @@ where "lift f (deny s) = (case f s of lemma lift_mt [simp]: "lift \ = \" apply (rule ext) - apply (case_tac "x") - apply (simp_all) -done - + subgoal for x + apply (case_tac "x") + apply (simp_all) + done + done text{* Since policies are maps, we inherit a composition on them. However, this results in nestings diff --git a/UPF/Service.thy b/UPF/Service.thy index 6672a32..4479260 100644 --- a/UPF/Service.thy +++ b/UPF/Service.thy @@ -5,8 +5,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2010-2012 ETH Zurich, Switzerland - * 2010-2014 Achim D. Brucker, Germany - * 2010-2014 Université Paris-Sud, France + * 2010-2015 Achim D. Brucker, Germany + * 2010-2017 Université Paris-Sud, France + * 2015-2017 The Univeristy of Sheffield, UK * * All rights reserved. * @@ -38,13 +39,12 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: Service.thy 10945 2014-11-21 12:50:43Z wolff $ *) section {* Secure Service Specification *} theory Service -imports - UPF + imports + UPF begin text {* In this section, we model a simple Web service and its access control model @@ -76,13 +76,13 @@ text{* *} type_synonym lr_id = int type_synonym LR = "lr_id \ (user set)" - + text{* The security context stores all the existing LRs. *} type_synonym \ = "patient \ LR" - + text{* The user context stores the roles the users are in. *} type_synonym \ = "user \ role" - + subsection {* Modelling Health Records and the Web Service API*} subsubsection {* Health Records *} text {* The content and the status of the entries of a health record *} diff --git a/UPF/ServiceExample.thy b/UPF/ServiceExample.thy index 7ed633d..97d0c92 100644 --- a/UPF/ServiceExample.thy +++ b/UPF/ServiceExample.thy @@ -38,13 +38,12 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: ServiceExample.thy 10954 2014-11-24 12:43:29Z wolff $ *) section {* Instantiating Our Secure Service Example *} theory ServiceExample -imports - Service + imports + Service begin text {* In the following, we briefly present an instantiations of our secure service example @@ -98,7 +97,7 @@ lemma [simp]: "(case a of allow d \ \X\ | deny d2 \< lemma [cong,simp]: "((if hasLR urp1_alice 1 \0 then \allow ()\ else \deny ()\) = \) = False" -by (simp) + by (simp) lemmas MonSimps = valid_SE_def unit_SE_def bind_SE_def lemmas Psplits = option.splits unit.splits prod.splits decision.splits @@ -112,23 +111,26 @@ lemmas PolSimps = valid_SE_def unit_SE_def bind_SE_def if_splits policy2MON_def entry3_def FunPolicy_def SE_LR_FUN_Policy_def o_def image_def UPFDefs lemma "SE_LR_RBAC_Policy ((createSCR alice Clerical patient1),\0)= Some (deny ())" -by (simp add: PolSimps) - -lemma exBool[simp]: "\a::bool. a" by auto - -lemma deny_allow[simp]: " \deny ()\ \ Some ` range allow" by auto - -lemma allow_deny[simp]: " \allow ()\ \ Some ` range deny" by auto - + by (simp add: PolSimps) + +lemma exBool[simp]: "\a::bool. a" + by auto + +lemma deny_allow[simp]: " \deny ()\ \ Some ` range allow" + by auto + +lemma allow_deny[simp]: " \allow ()\ \ Some ` range deny" + by auto + text{* Policy as monad. Alice using her first urp can read the SCR of patient1. *} lemma -"(\0 \ (os \ mbind [(createSCR alice Clerical patient1)] (PolMon); + "(\0 \ (os \ mbind [(createSCR alice Clerical patient1)] (PolMon); (return (os = [(deny (Out) )]))))" -by (simp add: PolMon_def MonSimps PolSimps) - + by (simp add: PolMon_def MonSimps PolSimps) + text{* Presenting her other urp, she is not allowed to read it. *} lemma "SE_LR_RBAC_Policy ((appendEntry alice Clerical patient1 ei d),\0)= \deny ()\" -by (simp add: PolSimps) + by (simp add: PolSimps) end diff --git a/UPF/UPF.thy b/UPF/UPF.thy index 42b4834..c4b68a3 100644 --- a/UPF/UPF.thy +++ b/UPF/UPF.thy @@ -40,7 +40,6 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: UPF.thy 10879 2014-10-26 11:35:31Z brucker $ *) section {* Putting Everything Together: UPF *} theory diff --git a/UPF/UPFCore.thy b/UPF/UPFCore.thy index 499e05d..0fefd47 100644 --- a/UPF/UPFCore.thy +++ b/UPF/UPFCore.thy @@ -6,8 +6,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2008-2014 Achim D. Brucker, Germany - * 2009-2014 Université Paris-Sud, France + * 2008-2015 Achim D. Brucker, Germany + * 2009-2017 Université Paris-Sud, France + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -39,13 +40,12 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: UPFCore.thy 10951 2014-11-21 21:54:46Z wolff $ *) section{* The Core of the Unified Policy Framework (UPF) *} theory UPFCore -imports - Monads + imports + Monads begin @@ -230,11 +230,15 @@ lemma override_A_empty[simp]: "p \\<^sub>A \ = p" lemma empty_override_A[simp]: "\ \\<^sub>A p = p" apply (rule ext) apply (simp add:override_A_def) - apply (case_tac "p x") - apply (simp_all) - apply (case_tac a) - apply (simp_all) -done + subgoal for x + apply (case_tac "p x") + apply (simp_all) + subgoal for a + apply (case_tac a) + apply (simp_all) + done + done + done lemma override_A_assoc: "p1 \\<^sub>A (p2 \\<^sub>A p3) = (p1 \\<^sub>A p2) \\<^sub>A p3" @@ -260,9 +264,13 @@ lemma override_D_empty[simp]: "p \\<^sub>D \ = p" lemma empty_override_D[simp]: "\ \\<^sub>D p = p" apply (rule ext) apply (simp add:override_D_def) - apply (case_tac "p x", simp_all) - apply (case_tac a, simp_all) -done + subgoal for x + apply (case_tac "p x", simp_all) + subgoal for a + apply (case_tac a, simp_all) + done + done + done lemma override_D_assoc: "p1 \\<^sub>D (p2 \\<^sub>D p3) = (p1 \\<^sub>D p2) \\<^sub>D p3" apply (rule ext) @@ -295,7 +303,7 @@ translations lemma policy_range_comp_strict : "f o\<^sub>f \ = \" apply (rule ext) apply (simp add: policy_range_comp_def) -done + done text{* @@ -313,21 +321,25 @@ where "(P) \ p = (\x. case p x of lemma range_split_strict[simp]: "P \ \ = \" apply (rule ext) apply (simp add: range_split_def) -done + done lemma range_split_charn: - "(f,g) \ p = (\x. case p x of + "(f,g) \ p = (\x. case p x of \allow x\ \ \allow (f x)\ | \deny x\ \ \deny (g x)\ | \ \ \)" apply (simp add: range_split_def) apply (rule ext) - apply (case_tac "p x") - apply (simp_all) - apply (case_tac "a") - apply (simp_all) -done + subgoal for x + apply (case_tac "p x") + apply (simp_all) + subgoal for a + apply (case_tac "a") + apply (simp_all) + done + done + done text{* The connection between these two becomes apparent if considering the following lemma: @@ -335,25 +347,32 @@ text{* lemma range_split_vs_range_compose: "(f,f) \ p = f o\<^sub>f p" by(simp add: range_split_charn policy_range_comp_def) - + lemma range_split_id [simp]: "(id,id) \ p = p" apply (rule ext) apply (simp add: range_split_charn id_def) - apply (case_tac "p x") - apply (simp_all) - apply (case_tac "a") - apply (simp_all) -done + subgoal for x + apply (case_tac "p x") + apply (simp_all) + subgoal for a + apply (case_tac "a") + apply (simp_all) + done + done + done lemma range_split_bi_compose [simp]: "(f1,f2) \ (g1,g2) \ p = (f1 o g1,f2 o g2) \ p" apply (rule ext) apply (simp add: range_split_charn comp_def) - apply (case_tac "p x") - apply (simp_all) - apply (case_tac "a") - apply (simp_all) -done - + subgoal for x + apply (case_tac "p x") + apply (simp_all) + subgoal for a + apply (case_tac "a") + apply (simp_all) + done + done + done text{* The next three operators are rather exotic and in most cases not used.