afp-mirror
/
UPF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Removed references to system generated names.

This commit is contained in:
Achim D. Brucker 2017-01-08 22:12:57 +00:00
parent 23edf34523
commit 0108e7575b
10 changed files with 683 additions and 605 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

157
UPF/Analysis.thy
View File

@ -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 \<mapsto> 'b) \<Rightarrow>('a \<mapsto
where "strictly_more_defined p q = (dom q \<subset> dom p)"
lemma strictly_more_vs_more: "strictly_more_defined p q \<Longrightarrow> 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 \<mapsto> 'b) \<Rightarrow> ('a \<mapsto> 'b) \<Rightarrow> bool" (infixl "\<sqsubseteq>\<^sub>A" 60)
@ -82,58 +82,60 @@ where " p \<sqsubseteq>\<^sub>A q = (\<forall> x. (case q x of \<lfloor>allow y
lemma more_permissive_refl : "p \<sqsubseteq>\<^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 \<sqsubseteq>\<^sub>A p' \<Longrightarrow> p' \<sqsubseteq>\<^sub>A p'' \<Longrightarrow> p \<sqsubseteq>\<^sub>A p''"
unfolding more_permissive_def
apply(auto split : option.split decision.split)
apply(erule_tac x = x and
P = "\<lambda>x. case p'' x of \<bottom> \<Rightarrow> True
unfolding more_permissive_def
apply(auto split : option.split decision.split)
subgoal for x y
apply(erule_tac x = x and
P = "\<lambda>x. case p'' x of \<bottom> \<Rightarrow> True
| \<lfloor>allow y\<rfloor> \<Rightarrow> \<exists>z. p' x = \<lfloor>allow z\<rfloor>
| \<lfloor>deny y\<rfloor> \<Rightarrow> 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 \<mapsto> 'b) \<Rightarrow> ('a \<mapsto> 'b) \<Rightarrow> bool" (infixl "\<sqsubseteq>\<^sub>D" 60)
where " p \<sqsubseteq>\<^sub>D q = (\<forall> x. (case q x of \<lfloor>deny y\<rfloor> \<Rightarrow> (\<exists> z. (p x = \<lfloor>deny z\<rfloor>))
where " p \<sqsubseteq>\<^sub>D q = (\<forall> x. (case q x of \<lfloor>deny y\<rfloor> \<Rightarrow> (\<exists> z. (p x = \<lfloor>deny z\<rfloor>))
| \<lfloor>allow y\<rfloor> \<Rightarrow> True
| \<bottom> \<Rightarrow> True))"
lemma more_rejective_trans : "p \<sqsubseteq>\<^sub>D p' \<Longrightarrow> p' \<sqsubseteq>\<^sub>D p'' \<Longrightarrow> p \<sqsubseteq>\<^sub>D p''"
unfolding more_rejective_def
apply(auto split : option.split decision.split)
apply(erule_tac x = x and
P = "\<lambda>x. case p'' x of \<bottom> \<Rightarrow> True
unfolding more_rejective_def
apply(auto split : option.split decision.split)
subgoal for x y
apply(erule_tac x = x and
P = "\<lambda>x. case p'' x of \<bottom> \<Rightarrow> True
| \<lfloor>allow y\<rfloor> \<Rightarrow> True
| \<lfloor>deny y\<rfloor> \<Rightarrow> \<exists>z. p' x = \<lfloor>deny z\<rfloor>" 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 \<sqsubseteq>\<^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 \<sqsubseteq>\<^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 \<sqsubseteq>\<^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 \<mapsto> 'b) \<Rightarrow> ('a' \<Rightarrow> 'a) \<Rightarrow>('b' \<Rightarrow> 'b) \<Rightarrow> ('a' \<mapsto> 'b') \<Rightarrow> bool"
("_ \<sqsubseteq>\<^bsub>_\<^esub>\<^sub>,\<^bsub>_\<^esub> _" [50,50,50,50]50)
where "p \<sqsubseteq>\<^bsub>abs\<^sub>a\<^esub>\<^sub>,\<^bsub>abs\<^sub>b\<^esub> q \<equiv>
"('a \<mapsto> 'b) \<Rightarrow> ('a' \<Rightarrow> 'a) \<Rightarrow>('b' \<Rightarrow> 'b) \<Rightarrow> ('a' \<mapsto> 'b') \<Rightarrow> bool"
("_ \<sqsubseteq>\<^bsub>_\<^esub>\<^sub>,\<^bsub>_\<^esub> _" [50,50,50,50]50)
where "p \<sqsubseteq>\<^bsub>abs\<^sub>a\<^esub>\<^sub>,\<^bsub>abs\<^sub>b\<^esub> q \<equiv>
(\<forall> a. case p a of
\<bottom> \<Rightarrow> True
| \<lfloor>allow y\<rfloor> \<Rightarrow> (\<forall> a'\<in>{x. abs\<^sub>a x=a}.
@ -142,69 +144,72 @@ where "p \<sqsubseteq>\<^bsub>abs\<^sub>a\<^esub>\<^sub>,\<^bsub>abs\<^sub>b
| \<lfloor>deny y\<rfloor> \<Rightarrow> (\<forall> a'\<in>{x. abs\<^sub>a x=a}.
\<exists> b'. q a' = \<lfloor>deny b'\<rfloor>
\<and> abs\<^sub>b b' = y))"
theorem polref_refl: "p \<sqsubseteq>\<^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 \<sqsubseteq>\<^bsub>f\<^esub>\<^sub>,\<^bsub>g\<^esub> p'"
and B: "p' \<sqsubseteq>\<^bsub>f'\<^esub>\<^sub>,\<^bsub>g'\<^esub> p''"
shows "p \<sqsubseteq>\<^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 \<sqsubseteq>\<^bsub>f\<^esub>\<^sub>,\<^bsub>g\<^esub> p'"
and B: "p' \<sqsubseteq>\<^bsub>f'\<^esub>\<^sub>,\<^bsub>g'\<^esub> p''"
shows "p \<sqsubseteq>\<^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 \<mapsto> 'b) \<Rightarrow> 'a set \<Rightarrow> ('a \<mapsto> 'b) \<Rightarrow>bool" ("_ \<approx>\<^bsub>_\<^esub> _" [60,60,60]60)
where "p \<approx>\<^bsub>D\<^esub> q = (\<forall>x\<in>D. p x = q x)"
where "p \<approx>\<^bsub>D\<^esub> q = (\<forall>x\<in>D. p x = q x)"
text{* p and q have no conflicts *}
definition no_conflicts :: "('a \<mapsto> 'b) \<Rightarrow>('a \<mapsto> 'b) \<Rightarrow>bool" where
"no_conflicts p q = (dom p = dom q \<and> (\<forall>x\<in>(dom p).
"no_conflicts p q = (dom p = dom q \<and> (\<forall>x\<in>(dom p).
(case p x of \<lfloor>allow y\<rfloor> \<Rightarrow> (\<exists>z. q x = \<lfloor>allow z\<rfloor>)
| \<lfloor>deny y\<rfloor> \<Rightarrow> (\<exists>z. q x = \<lfloor>deny z\<rfloor>))))"
lemma policy_eq:
assumes p_over_qA: "p \<sqsubseteq>\<^sub>A q "
and q_over_pA: "q \<sqsubseteq>\<^sub>A p"
and p_over_qD: "q \<sqsubseteq>\<^sub>D p"
and q_over_pD: "p \<sqsubseteq>\<^sub>D q"
and dom_eq: "dom p = dom q"
shows "no_conflicts p q"
and q_over_pA: "q \<sqsubseteq>\<^sub>A p"
and p_over_qD: "q \<sqsubseteq>\<^sub>D p"
and q_over_pD: "p \<sqsubseteq>\<^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: "\<lbrakk>dom p \<inter> dom q = {}; p x = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> q x = \<bottom>"
by (auto)
lemma dom_eq: "dom p \<inter> dom q = {} \<Longrightarrow> p \<Oplus>\<^sub>A q = p \<Oplus>\<^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) \<Delta> p = (dom(p \<triangleright> Allow) \<triangleleft> (A\<^sub>f f)) \<Oplus> (dom(p \<triangleright> Deny) \<triangleleft> (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

164
UPF/ElementaryPolicies.thy
View File

@ -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 (\<lambda>x. \<lfloor>x\<rfloor>)) = (\<forall>Dx. \<lfloor>x\<rfloor>)"
by(simp add:id_def comp_def)
lemma AllD_norm2[simp]: "deny_pfun (Some o id) = (\<forall>Dx. \<lfloor>x\<rfloor>)"
by(simp add:id_def comp_def)
lemma AllA_norm[simp]: "allow_pfun (id o Some) = (\<forall>Ax. \<lfloor>x\<rfloor>)"
by(simp add:id_def comp_def)
lemma AllA_norm2[simp]: "allow_pfun (Some o id) = (\<forall>Ax. \<lfloor>x\<rfloor>)"
by(simp add:id_def comp_def)
lemma AllA_apply[simp]: "(\<forall>Ax. Some (P x)) x = \<lfloor>allow (P x)\<rfloor>"
by(simp add:allow_pfun_def)
lemma AllD_apply[simp]: "(\<forall>Dx. Some (P x)) x = \<lfloor>deny (P x)\<rfloor>"
by(simp add:deny_pfun_def)
lemma neq_Allow_Deny: "pf \<noteq> \<emptyset> \<Longrightarrow> (deny_pfun pf) \<noteq> (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 = \<bottom>")
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 = \<bottom>")
apply (auto)
done
done
subsection{* Common Instances *}
@ -138,13 +140,11 @@ definition
text{* ... and resulting properties: *}
lemma "A\<^sub>I \<Oplus> empty = A\<^sub>I"
apply simp
done
by simp
lemma "A\<^sub>f f \<Oplus> 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 \<Longrightarrow> (allow_pfun pf) \<Oplu
lemma deny_left_cancel :"dom pf = UNIV \<Longrightarrow> (deny_pfun pf) \<Oplus> 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 \<subseteq> Allow \<union> Deny"
apply (auto simp: Allow_def Deny_def ran_def full_SetCompr_eq[symmetric])
apply (case_tac "x")
apply (simp_all)
apply (rename_tac \<alpha>)
apply (erule_tac x="\<alpha>" 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 \<alpha>)
apply (erule_tac x="\<alpha>" 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 \<triangleleft> p \<equiv> (\<lambda>x. if x \<in> S then p x else
lemma dom_dom_restrict[simp] : "dom(S \<triangleleft> p) = S \<inter> dom p"
apply (auto simp: dom_restrict_def)
apply (case_tac "x \<in> S")
apply (simp_all)
apply (case_tac "x \<in> S")
apply (simp_all)
done
subgoal for x y
apply (case_tac "x \<in> S")
apply (simp_all)
done
subgoal for x y
apply (case_tac "x \<in> S")
apply (simp_all)
done
done
lemma dom_restrict_idem[simp] : "(dom p) \<triangleleft> 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 \<triangleleft> S \<triangleleft> p = T \<inter> S \<triangleleft> 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 :: "['\<alpha>\<mapsto>'\<beta>,'\<beta> decision set] \<Rightarrow> '\<alpha> \<mapsto>'\<beta>" (infixr "\<triangleright>" 55)
where "p \<triangleright> S \<equiv> (\<lambda>x. if p x \<in> (Some`S) then p x else \<bottom>)"
@ -299,38 +316,39 @@ where "p \<triangleright>2 S \<equiv> (\<lambda>x. if (the (p x)) \<in> (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 \<triangleright> S) = S \<inter> ran p"
by(auto simp: ran_restrict_def image_def ran_def)
lemma ran_restrict_idem[simp] : "p \<triangleright> (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 \<triangleright> S) \<triangleright> T = p \<triangleright> T \<inter> 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] : "(\<forall>Ax. \<lfloor>P x\<rfloor>) \<triangleright> Allow = (\<forall>Ax. \<lfloor>P x\<rfloor>)"
apply (rule ext)
apply (auto simp: Allow_def ran_restrict_def)
done
done
lemma ran_gen_D[simp] : "(\<forall>Dx. \<lfloor>P x\<rfloor>) \<triangleright> Deny = (\<forall>Dx. \<lfloor>P x\<rfloor>)"
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

244
UPF/Monads.thy
View File

@ -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 \<leftarrow> return a; k) = k"
apply (simp add: unit_SE_def bind_SE_def)
done
done
lemma bind_right_unit: "(x \<leftarrow> m; return x) = m"
apply (simp add: unit_SE_def bind_SE_def)
apply (rule ext)
apply (case_tac "m \<sigma>")
apply ( simp_all)
done
subgoal for "\<sigma>"
apply (case_tac "m \<sigma>")
apply ( simp_all)
done
done
lemma bind_assoc: "(y \<leftarrow> (x \<leftarrow> m; k); h) = (x \<leftarrow> m; (y \<leftarrow> k; h))"
apply (simp add: unit_SE_def bind_SE_def)
apply (rule ext)
apply (case_tac "m \<sigma>", simp_all)
apply (case_tac "a", simp_all)
done
subgoal for "\<sigma>"
apply (case_tac "m \<sigma>", 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 :: "'\<iota> list \<Rightarrow> ('\<iota> \<Rightarrow> ('o,'\<sigma>) MON\<^sub>S\<^sub>E) \<Rightarrow> ('o list,'\<sigma>) MON\<^sub>S\<^sub>E"
where "mbind [] iostep \<sigma> = Some([], \<sigma>)" |
"mbind (a#H) iostep \<sigma> =
where "mbind [] iostep \<sigma> = Some([], \<sigma>)" |
"mbind (a#H) iostep \<sigma> =
(case iostep a \<sigma> of
None \<Rightarrow> Some([], \<sigma>)
| Some (out, \<sigma>') \<Rightarrow> (case mbind H iostep \<sigma>' 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 \<sigma> \<noteq> None"
apply (rule_tac x=\<sigma> 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' :: "'\<iota> list \<Rightarrow> ('\<iota> \<Rightarrow> ('o,'\<sigma>) MON\<^sub>S\<^sub>E) \<Rightarrow> ('o list,'\<sigma>) MON\<^sub>S\<^sub>E"
@ -237,12 +249,17 @@ lemma mbind_try:
else (x \<leftarrow> 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 ("\<Sqinter>\<^sub>S\<^sub>E")
lemma malt_SE_mt [simp]: "\<Sqinter>\<^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]: "\<Sqinter>\<^sub>S\<^sub>E (a # S) = (a \<sqinter>\<^sub>S\<^sub>E (\<Sqinter>\<^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 :\<equiv> returning a; m) = m"
apply (rule ext)
apply (simp add: unit_SBE_def bind_SBE_def)
done
done
lemma bind_right_unit_SBE: "(x :\<equiv> 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 :\<equiv> (x :\<equiv> m; k); h) = (x :\<equiv> m; (y :\<equiv> 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="\<lambda> x. None \<noteq> case_prod (\<lambda>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\<in>(\<lambda>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="\<lambda> x. None \<noteq> case_prod (\<lambda>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\<in>(\<lambda>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\<in>(\<lambda>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\<in>(\<lambda>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 \<sigma> = None \<Longrightarrow>
(\<sigma> \<Turnstile> (s \<leftarrow> mbind (a#S) ioprog ; M s)) =
(\<sigma> \<Turnstile> (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 \<sigma> = None \<Longrightarrow> \<not>(\<sigma> \<Turnstile> ((s \<leftarrow> 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 \<sigma> = Some(f \<sigma>,\<sigma>) \<Longrightarrow> (\<sigma> \<Turnstile> M) = f \<sigma>"
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 \<sigma> = Some(b,\<sigma>') \<Longrightarrow>
(\<sigma> \<Turnstile> (s \<leftarrow> mbind (a#S) ioprog ; M s)) =
(\<sigma>' \<Turnstile> (s \<leftarrow> mbind S ioprog ; M (b#s)))"
apply (simp add: valid_SE_def unit_SE_def bind_SE_def )
apply (cases "mbind S ioprog \<sigma>'", auto)
done
done
lemma valid_success'': "ioprog a \<sigma> = Some(b,\<sigma>') \<Longrightarrow>
(\<sigma> \<Turnstile> (s \<leftarrow> mbind (a#S) ioprog ; return (P s))) =
(\<sigma>' \<Turnstile> (s \<leftarrow> mbind S ioprog ; return (P (b#s))))"
apply (simp add: valid_SE_def unit_SE_def bind_SE_def )
apply (cases "mbind S ioprog \<sigma>'")
apply (simp_all)
apply (simp_all)
apply (auto)
done
done
lemma valid_success': "A \<sigma> = Some(b,\<sigma>') \<Longrightarrow> (\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s))) = (\<sigma>' \<Turnstile> (M b))"
by(simp add: valid_SE_def unit_SE_def bind_SE_def )
@ -453,48 +475,47 @@ lemma valid_both: "(\<sigma> \<Turnstile> (s \<leftarrow> mbind (a#S) ioprog ; r
None \<Rightarrow> (\<sigma> \<Turnstile> (return (P [])))
| Some(b,\<sigma>') \<Rightarrow> (\<sigma>' \<Turnstile> (s \<leftarrow> mbind S ioprog ; return (P (b#s)))))"
apply (case_tac "ioprog a \<sigma>")
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]: "(\<sigma> \<Turnstile> (return P)) = (P)"
by(auto simp: valid_SE_def unit_SE_def)
lemma valid_propagate_2: "\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s)) \<Longrightarrow> \<exists> v \<sigma>'. the(A \<sigma>) = (v,\<sigma>') \<and> \<sigma>' \<Turnstile> (M v)"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A \<sigma>")
apply (simp_all)
apply (simp_all)
apply (drule_tac x="A \<sigma>" 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': "\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s)) \<Longrightarrow> \<exists> a. (A \<sigma>) = Some a \<and> (snd a) \<Turnstile> (M (fst a))"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A \<sigma>")
apply (simp_all)
apply (simp_all)
apply (simp_all split: prod.splits)
apply (drule_tac x="A \<sigma>" 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'': "\<sigma> \<Turnstile> ((s \<leftarrow> A ; M s)) \<Longrightarrow> \<exists> v \<sigma>'. A \<sigma> = Some(v,\<sigma>') \<and> \<sigma>' \<Turnstile> (M v)"
apply (auto simp: valid_SE_def unit_SE_def bind_SE_def)
apply (cases "A \<sigma>")
apply (simp_all)
apply (simp_all)
apply (drule_tac x="A \<sigma>" 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]: "(\<sigma>\<^sub>0 \<Turnstile> (\<lambda>\<sigma>. Some (f \<sigma>, \<sigma>))) = (f \<sigma>\<^sub>0)"
by(simp add: valid_SE_def )
@ -513,18 +534,20 @@ lemma assert_disch3 :" \<not> P \<sigma> \<Longrightarrow> \<not> (\<sigma> \<Tu
lemma assert_D : "(\<sigma> \<Turnstile> (x \<leftarrow> assert\<^sub>S\<^sub>E P; M x)) \<Longrightarrow> P \<sigma> \<and> (\<sigma> \<Turnstile> (M True))"
by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.if_split_asm)
lemma assume_D : "(\<sigma> \<Turnstile> (x \<leftarrow> assume\<^sub>S\<^sub>E P; M x)) \<Longrightarrow> \<exists> \<sigma>. (P \<sigma> \<and> \<sigma> \<Turnstile> (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 \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = (\<sigma> \<Turnstile> B\<^sub>1)"
by(auto simp: if_SE_def valid_SE_def)
lemma if_SE_D2 : "\<not> P \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = (\<sigma> \<Turnstile> B\<^sub>2)"
by(auto simp: if_SE_def valid_SE_def)
lemma if_SE_split_asm : " (\<sigma> \<Turnstile> if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = ((P \<sigma> \<and> (\<sigma> \<Turnstile> B\<^sub>1)) \<or> (\<not> P \<sigma> \<and> (\<sigma> \<Turnstile> B\<^sub>2)))"
by(cases "P \<sigma>",auto simp: if_SE_D1 if_SE_D2)
lemma if_SE_split : " (\<sigma> \<Turnstile> if\<^sub>S\<^sub>E P B\<^sub>1 B\<^sub>2) = ((P \<sigma> \<longrightarrow> (\<sigma> \<Turnstile> B\<^sub>1)) \<and> (\<not> P \<sigma> \<longrightarrow> (\<sigma> \<Turnstile> B\<^sub>2)))"
by(cases "P \<sigma>", auto simp: if_SE_D1 if_SE_D2)
lemma [code]: "(\<sigma> \<Turnstile> m) = (case (m \<sigma>) of None \<Rightarrow> False | (Some (x,y)) \<Rightarrow> x)"
apply (simp add: valid_SE_def)
apply (cases "m \<sigma> = 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 :: "'\<sigma> \<Rightarrow> ('a,'\<sigma>) MON\<^sub>S\<^sub>B\<^sub>E \<Rightarrow> bool" (infix "\<Turnstile>\<^sub>S\<^sub>B\<^sub>E" 15)
where "\<sigma> \<Turnstile>\<^sub>S\<^sub>B\<^sub>E m \<equiv> (m \<sigma> \<noteq> None)"
where "\<sigma> \<Turnstile>\<^sub>S\<^sub>B\<^sub>E m \<equiv> (m \<sigma> \<noteq> None)"
text{*
This notation considers all non-failures as valid.
*}
lemma assume_assert: "(\<sigma> \<Turnstile>\<^sub>S\<^sub>B\<^sub>E ( _ :\<equiv> assume\<^sub>S\<^sub>B\<^sub>E P ; assert\<^sub>S\<^sub>B\<^sub>E Q)) = (P \<sigma> \<longrightarrow> Q \<sigma>)"
by(simp add: valid_SBE_def assume_SBE_def assert_SBE_def bind_SBE_def)
lemma assert_intro: "Q \<sigma> \<Longrightarrow> \<sigma> \<Turnstile>\<^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

356
UPF/Normalisation.thy
View File

@ -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 \<mapsto> 'b) list \<Rightarrow> ('a \<mapsto> 'b)" where
"list2policy l = foldr (\<lambda> x y. (x \<Oplus> y)) l \<emptyset>"
text{*
Determine the position of element of a list.
*}
fun position :: "'\<alpha> \<Rightarrow> '\<alpha> list \<Rightarrow> 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 \<in> 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) \<noteq> {} \<and> (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 \<Longrightarrow> p \<noteq> [] \<Longrightarrow> 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 \<Longrightarrow> (rm_MT_rules C p) = p"
apply (induct p)
apply (simp_all)
done
apply (simp_all)
done
lemma nMTcharn: "none_MT_rules C p = (\<forall> r \<in> set p. dom (C r) \<noteq> {})"
apply (induct p)
apply (simp_all)
done
apply (simp_all)
done
lemma nMTeqSet: "set p = set s \<Longrightarrow> none_MT_rules C p = none_MT_rules C s"
apply (simp add: nMTcharn)
done
done
lemma notMTnMT: "\<lbrakk>a \<in> set p; none_MT_rules C p\<rbrakk> \<Longrightarrow> dom (C a) \<noteq> {}"
apply (simp add: nMTcharn)
done
done
lemma none_MT_rulesconc: "none_MT_rules C (a@[b]) \<Longrightarrow> none_MT_rules C a"
apply (induct a)
apply (simp_all)
done
apply (simp_all)
done
lemma nMTtail: "none_MT_rules C p \<Longrightarrow> 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 \<Longrightarrow> p \<noteq> []"
apply (auto)
done
done
lemma SR3nMT: "\<not> not_MT C p \<Longrightarrow> rm_MT_rules C p = []"
apply (induct p)
apply (auto simp: if_splits)
done
apply (auto simp: if_splits)
done
lemma NMPcharn: "\<lbrakk>a \<in> set p; dom (C a) \<noteq> {}\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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: "\<lbrakk>applied_rule_rev C x b = Some r; applied_rule_rev C x c = Some r\<rbrakk> \<Longrightarrow>
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 \<Longrightarrow>
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 \<in> 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 \<in> 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: "\<lbrakk>applied_rule_rev C x b = None; applied_rule_rev C x c = None\<rbrakk> \<Longrightarrow>
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 \<Longrightarrow>
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 \<noteq> None \<Longrightarrow>
applied_rule_rev C x (b # p) = applied_rule_rev C x (p)"
by (auto simp: mrconc)
by (auto simp: mrconc)
lemma mrNoneMT: "\<lbrakk>r \<in> set p; applied_rule_rev C x p = None\<rbrakk> \<Longrightarrow>
x \<notin> 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 \<in> 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 :: "('\<alpha> \<mapsto>'\<beta>) \<Rightarrow> (('\<gamma> \<maps
"prod_list x (y#ys) par_comb ran_adapt dom_adapt =
((ran_adapt o_f ((par_comb x y) o dom_adapt))#(prod_list x ys par_comb ran_adapt dom_adapt))"
| "prod_list x [] par_comb ran_adapt dom_adapt = []"
text{*
An instance, as usual there are four of them.
*}
definition prod_2_list :: "[('\<alpha> \<mapsto>'\<beta>), (('\<gamma> \<mapsto>'\<delta>) list)] \<Rightarrow>
(('\<beta> \<times> '\<delta>) \<Rightarrow> 'y) \<Rightarrow> ('x \<Rightarrow> ('\<alpha> \<times> '\<gamma>)) \<Rightarrow>
(('x \<mapsto> 'y) list)" (infixr "\<Otimes>\<^sub>2\<^sub>L" 55) where
"x \<Otimes>\<^sub>2\<^sub>L y = (\<lambda> d r. (x \<Otimes>\<^sub>L y) (op \<Otimes>\<^sub>2) d r)"
lemma list2listNMT: "x \<noteq> [] \<Longrightarrow> map sem x \<noteq> []"
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 \<Otimes>\<^sub>\<or>\<^sub>D) d r"
apply (rule allI)+
apply (rule distr_orD)
apply (simp)
done
done
lemma is_strict_orD: "is_strict (op \<Otimes>\<^sub>\<or>\<^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 \<Otimes>\<^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 \<Otimes>\<^sub>2) d r"
apply (simp only: is_strict_def)
apply simp
apply (simp add: policy_range_comp_def)
done
done
lemma domStart: "t \<in> dom p1 \<Longrightarrow> (p1 \<Oplus> p2) t = p1 t"
apply (simp add: map_add_dom_app_simps)
done
done
lemma notDom: "x \<in> dom A \<Longrightarrow> \<not> 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 \<Otimes>\<^sub>1) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^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 \<in> dom (r o_f ((P1 \<Otimes>\<^sub>1 p) \<circ> 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 \<in> dom (r o_f ((P1 \<Otimes>\<^sub>1 p) \<circ> 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 \<Otimes>\<^sub>2) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^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 \<in> dom (r o_f ((P1 \<Otimes>\<^sub>2 p) \<circ> 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 \<in> dom (r o_f ((P1 \<Otimes>\<^sub>2 p) \<circ> 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 \<Otimes>\<^sub>\<or>\<^sub>A) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>\<or>\<^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 \<in> dom (r o_f ((P1 \<Otimes>\<^sub>\<or>\<^sub>A p) \<circ> 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 \<in> dom (r o_f ((P1 \<Otimes>\<^sub>\<or>\<^sub>A p) \<circ> 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 \<Otimes>\<^sub>\<or>\<^sub>D) P1 (list2policy P2)) o d)) x =
((list2policy ((P1 \<Otimes>\<^sub>L P2) (op \<Otimes>\<^sub>\<or>\<^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 \<in> dom (r o_f ((P1 \<Otimes>\<^sub>\<or>\<^sub>D p) \<circ> 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 \<in> dom (r o_f ((P1 \<Otimes>\<^sub>\<or>\<^sub>D p) \<circ> 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 \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>1 B) o (\<lambda> 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 \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>2 B) o (\<lambda> 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 \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>\<or>\<^sub>A B) o (\<lambda> 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 \<Longrightarrow> dom ((\<lambda>(x, y). x) o_f (A \<Otimes>\<^sub>\<or>\<^sub>D B) o (\<lambda> 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

194
UPF/ParallelComposition.thy
View File

@ -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 ::"['\<alpha>\<mapsto>'\<beta>, '\<gamma> \<mapsto>'\<delta>] \<Rightarrow> ('\<alpha>\<times>'\<gamma> \<mapsto> '\<beta>\<times>'\<delta>)" (infixr "\<Otimes>\<^sub>\<or>\<^sub>A" 55)
where "p1 \<Otimes>\<^sub>\<or>\<^sub>A p2 =
where "p1 \<Otimes>\<^sub>\<or>\<^sub>A p2 =
(\<lambda>(x,y). (case p1 x of
\<lfloor>allow d1\<rfloor> \<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
@ -80,25 +80,25 @@ where "p1 \<Otimes>\<^sub>\<or>\<^sub>A p2 =
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny (d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<bottom> \<Rightarrow> \<bottom>))"
lemma prod_orA_mt[simp]:"p \<Otimes>\<^sub>\<or>\<^sub>A \<emptyset> = \<emptyset>"
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]:"\<emptyset> \<Otimes>\<^sub>\<or>\<^sub>A p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_orA_def)
done
done
lemma prod_orA_quasi_commute: "p2 \<Otimes>\<^sub>\<or>\<^sub>A p1 = (((\<lambda>(x,y). (y,x)) o_f (p1 \<Otimes>\<^sub>\<or>\<^sub>A p2))) o (\<lambda>(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 ::"['\<alpha> \<mapsto> '\<beta>, '\<gamma> \<mapsto> '\<delta>] \<Rightarrow> ('\<alpha> \<times> '\<gamma> \<mapsto> '\<beta> \<times> '\<delta> )" (infixr "\<Otimes>\<^sub>\<or>\<^sub>D" 55)
where "p1 \<Otimes>\<^sub>\<or>\<^sub>D p2 =
@ -116,28 +116,28 @@ where "p1 \<Otimes>\<^sub>\<or>\<^sub>D p2 =
lemma prod_orD_mt[simp]:"p \<Otimes>\<^sub>\<or>\<^sub>D \<emptyset> = \<emptyset>"
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]:"\<emptyset> \<Otimes>\<^sub>\<or>\<^sub>D p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_orD_def)
done
done
lemma prod_orD_quasi_commute: "p2 \<Otimes>\<^sub>\<or>\<^sub>D p1 = (((\<lambda>(x,y). (y,x)) o_f (p1 \<Otimes>\<^sub>\<or>\<^sub>D p2))) o (\<lambda>(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 :: "['\<alpha>\<mapsto>'\<beta>, '\<gamma> \<mapsto>'\<delta>] \<Rightarrow> ('\<alpha>\<times>'\<gamma> \<mapsto> '\<beta>\<times>'\<delta>)" (infixr "\<Otimes>\<^sub>1" 55)
where "p1 \<Otimes>\<^sub>1 p2 \<equiv>
where "p1 \<Otimes>\<^sub>1 p2 \<equiv>
(\<lambda>(x,y). (case p1 x of
\<lfloor>allow d1\<rfloor>\<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
@ -148,21 +148,21 @@ where "p1 \<Otimes>\<^sub>1 p2 \<equiv>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny(d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
|\<bottom> \<Rightarrow> \<bottom>))"
lemma prod_1_mt[simp]:"p \<Otimes>\<^sub>1 \<emptyset> = \<emptyset>"
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]:"\<emptyset> \<Otimes>\<^sub>1 p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_1_def)
done
done
definition prod_2 :: "['\<alpha>\<mapsto>'\<beta>, '\<gamma> \<mapsto>'\<delta>] \<Rightarrow> ('\<alpha>\<times>'\<gamma> \<mapsto> '\<beta>\<times>'\<delta>)" (infixr "\<Otimes>\<^sub>2" 55)
where "p1 \<Otimes>\<^sub>2 p2 \<equiv>
where "p1 \<Otimes>\<^sub>2 p2 \<equiv>
(\<lambda>(x,y). (case p1 x of
\<lfloor>allow d1\<rfloor> \<Rightarrow>(case p2 y of
\<lfloor>allow d2\<rfloor> \<Rightarrow> \<lfloor>allow(d1,d2)\<rfloor>
@ -173,54 +173,54 @@ where "p1 \<Otimes>\<^sub>2 p2 \<equiv>
| \<lfloor>deny d2\<rfloor> \<Rightarrow> \<lfloor>deny (d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
|\<bottom> \<Rightarrow>\<bottom>))"
lemma prod_2_mt[simp]:"p \<Otimes>\<^sub>2 \<emptyset> = \<emptyset>"
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]:"\<emptyset> \<Otimes>\<^sub>2 p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_2_def)
done
done
definition prod_1_id ::"['\<alpha>\<mapsto>'\<beta>, '\<alpha>\<mapsto>'\<gamma>] \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>\<times>'\<gamma>)" (infixr "\<Otimes>\<^sub>1\<^sub>I" 55)
where "p \<Otimes>\<^sub>1\<^sub>I q = (p \<Otimes>\<^sub>1 q) o (\<lambda>x. (x,x))"
where "p \<Otimes>\<^sub>1\<^sub>I q = (p \<Otimes>\<^sub>1 q) o (\<lambda>x. (x,x))"
lemma prod_1_id_mt[simp]:"p \<Otimes>\<^sub>1\<^sub>I \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: prod_1_id_def)
done
done
lemma mt_prod_1_id[simp]:"\<emptyset> \<Otimes>\<^sub>1\<^sub>I p = \<emptyset>"
apply (rule ext)
apply (simp add: prod_1_id_def prod_1_def)
done
done
definition prod_2_id ::"['\<alpha>\<mapsto>'\<beta>, '\<alpha>\<mapsto>'\<gamma>] \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>\<times>'\<gamma>)" (infixr "\<Otimes>\<^sub>2\<^sub>I" 55)
where"p \<Otimes>\<^sub>2\<^sub>I q = (p \<Otimes>\<^sub>2 q) o (\<lambda>x. (x,x))"
where"p \<Otimes>\<^sub>2\<^sub>I q = (p \<Otimes>\<^sub>2 q) o (\<lambda>x. (x,x))"
lemma prod_2_id_mt[simp]:"p \<Otimes>\<^sub>2\<^sub>I \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: prod_2_id_def)
done
done
lemma mt_prod_2_id[simp]:"\<emptyset> \<Otimes>\<^sub>2\<^sub>I p = \<emptyset>"
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 :: "('\<alpha> \<rightharpoonup> '\<beta>) \<Rightarrow> ('\<delta> \<rightharpoonup> '\<gamma>) \<Rightarrow>
('\<alpha> \<times> '\<delta> \<rightharpoonup> '\<beta> \<times> '\<gamma>)" (infixr "\<Otimes>\<^sub>M" 60)
where "p1 \<Otimes>\<^sub>M p2 = (\<lambda> (x,y). case p1 x of \<lfloor>d1\<rfloor> \<Rightarrow>
where "p1 \<Otimes>\<^sub>M p2 = (\<lambda> (x,y). case p1 x of \<lfloor>d1\<rfloor> \<Rightarrow>
(case p2 y of \<lfloor>d2\<rfloor> \<Rightarrow> \<lfloor>(d1,d2)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)
| \<bottom> \<Rightarrow> \<bottom>)"
@ -249,81 +249,93 @@ lemma comp_ran_split_charn:
"(f, g) \<Otimes>\<^sub>\<nabla> p = (
(((p \<triangleright> Allow)\<Otimes>\<^sub>\<or>\<^sub>A (A\<^sub>p f)) \<Oplus>
((p \<triangleright> Deny) \<Otimes>\<^sub>\<or>\<^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 \<Oplus> F2) \<Longrightarrow> (((N \<Otimes>\<^sub>1 F) o f) =
(((N \<Otimes>\<^sub>1 F1) o f) \<Oplus> ((N \<Otimes>\<^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 \<Oplus> F2) \<Longrightarrow> ((g o_f ((N \<Otimes>\<^sub>1 F) o f)) =
((g o_f ((N \<Otimes>\<^sub>1 F1) o f)) \<Oplus> (g o_f ((N \<Otimes>\<^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 \<Oplus> F2) \<Longrightarrow> (((N \<Otimes>\<^sub>2 F) o f) =
(((N \<Otimes>\<^sub>2 F1) o f) \<Oplus> ((N \<Otimes>\<^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 \<Oplus> F2) \<Longrightarrow> ((r o_f ((N \<Otimes>\<^sub>2 F) o f)) =
((r o_f ((N \<Otimes>\<^sub>2 F1) o f)) \<Oplus> (r o_f ((N \<Otimes>\<^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 \<Oplus> F2) \<Longrightarrow> ((g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>A F) o f)) =
((g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>A F1) o f)) \<Oplus> (g o_f ((N \<Otimes>\<^sub>\<or>\<^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 \<Oplus> F2) \<Longrightarrow> ((g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>D F) o f)) =
((g o_f ((N \<Otimes>\<^sub>\<or>\<^sub>D F1) o f)) \<Oplus> (g o_f ((N \<Otimes>\<^sub>\<or>\<^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

37
UPF/SeqComposition.thy
View File

@ -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 \<Longrightarrow> x = deny(deny y)"
apply (case_tac "x")
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", simp_all)[1]
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", simp_all)[1]
done
done
lemma flat_orA_allow[dest]: "flat_orA x = allow y \<Longrightarrow> x = allow(allow y)
\<or> x = allow(deny y)
@ -79,21 +79,21 @@ lemma flat_orA_allow[dest]: "flat_orA x = allow y \<Longrightarrow> x = allow(al
apply (case_tac "\<alpha>", simp_all)[1]
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", simp_all)[1]
done
done
fun flat_orD :: "('\<alpha> decision) decision \<Rightarrow> ('\<alpha> 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 \<Longrightarrow> x = allow(allow y)"
apply (case_tac "x")
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", simp_all)[1]
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", simp_all)[1]
done
done
lemma flat_orD_deny[dest]: "flat_orD x = deny y \<Longrightarrow> x = deny(deny y)
\<or> x = allow(deny y)
@ -103,7 +103,7 @@ lemma flat_orD_deny[dest]: "flat_orD x = deny y \<Longrightarrow> x = deny(deny
apply (case_tac "\<alpha>", simp_all)[1]
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", simp_all)[1]
done
done
fun flat_1 :: "('\<alpha> decision) decision \<Rightarrow> ('\<alpha> decision)"
where "flat_1(allow(allow y)) = allow y"
@ -117,7 +117,7 @@ lemma flat_1_allow[dest]: "flat_1 x = allow y \<Longrightarrow> x = allow(allow
apply (case_tac "\<alpha>", simp_all)[1]
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", simp_all)[1]
done
done
lemma flat_1_deny[dest]: "flat_1 x = deny y \<Longrightarrow> x = deny(deny y) \<or> x = deny(allow y)"
apply (case_tac "x")
@ -125,7 +125,7 @@ lemma flat_1_deny[dest]: "flat_1 x = deny y \<Longrightarrow> x = deny(deny y)
apply (case_tac "\<alpha>", simp_all)[1]
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", simp_all)[1]
done
done
fun flat_2 :: "('\<alpha> decision) decision \<Rightarrow> ('\<alpha> decision)"
where "flat_2(allow(allow y)) = allow y"
@ -147,7 +147,7 @@ lemma flat_2_deny[dest]: "flat_2 x = deny y \<Longrightarrow> x = deny(deny y)
apply (case_tac "\<alpha>", simp_all)[1]
apply (rename_tac \<alpha>)
apply (case_tac "\<alpha>", 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 \<emptyset> = \<emptyset>"
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

16
UPF/Service.thy
View File

@ -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 \<rightharpoonup> (user set)"
text{* The security context stores all the existing LRs. *}
type_synonym \<Sigma> = "patient \<rightharpoonup> LR"
text{* The user context stores the roles the users are in. *}
type_synonym \<upsilon> = "user \<rightharpoonup> 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 *}

34
UPF/ServiceExample.thy
View File

@ -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 \<Rightarrow> \<lfloor>X\<rfloor> | deny d2 \<
lemma [cong,simp]:
"((if hasLR urp1_alice 1 \<Sigma>0 then \<lfloor>allow ()\<rfloor> else \<lfloor>deny ()\<rfloor>) = \<bottom>) = 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),\<sigma>0)= Some (deny ())"
by (simp add: PolSimps)
lemma exBool[simp]: "\<exists>a::bool. a" by auto
lemma deny_allow[simp]: " \<lfloor>deny ()\<rfloor> \<notin> Some ` range allow" by auto
lemma allow_deny[simp]: " \<lfloor>allow ()\<rfloor> \<notin> Some ` range deny" by auto
by (simp add: PolSimps)
lemma exBool[simp]: "\<exists>a::bool. a"
by auto
lemma deny_allow[simp]: " \<lfloor>deny ()\<rfloor> \<notin> Some ` range allow"
by auto
lemma allow_deny[simp]: " \<lfloor>allow ()\<rfloor> \<notin> Some ` range deny"
by auto
text{* Policy as monad. Alice using her first urp can read the SCR of patient1. *}
lemma
"(\<sigma>0 \<Turnstile> (os \<leftarrow> mbind [(createSCR alice Clerical patient1)] (PolMon);
"(\<sigma>0 \<Turnstile> (os \<leftarrow> 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),\<sigma>0)= \<lfloor>deny ()\<rfloor>"
by (simp add: PolSimps)
by (simp add: PolSimps)
end

1
UPF/UPF.thy
View File

@ -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

85
UPF/UPFCore.thy
View File

@ -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 \<Oplus>\<^sub>A \<emptyset> = p"
lemma empty_override_A[simp]: "\<emptyset> \<Oplus>\<^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 \<Oplus>\<^sub>A (p2 \<Oplus>\<^sub>A p3) = (p1 \<Oplus>\<^sub>A p2) \<Oplus>\<^sub>A p3"
@ -260,9 +264,13 @@ lemma override_D_empty[simp]: "p \<Oplus>\<^sub>D \<emptyset> = p"
lemma empty_override_D[simp]: "\<emptyset> \<Oplus>\<^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 \<Oplus>\<^sub>D (p2 \<Oplus>\<^sub>D p3) = (p1 \<Oplus>\<^sub>D p2) \<Oplus>\<^sub>D p3"
apply (rule ext)
@ -295,7 +303,7 @@ translations
lemma policy_range_comp_strict : "f o\<^sub>f \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: policy_range_comp_def)
done
done
text{*
@ -313,21 +321,25 @@ where "(P) \<nabla> p = (\<lambda>x. case p x of
lemma range_split_strict[simp]: "P \<nabla> \<emptyset> = \<emptyset>"
apply (rule ext)
apply (simp add: range_split_def)
done
done
lemma range_split_charn:
"(f,g) \<nabla> p = (\<lambda>x. case p x of
"(f,g) \<nabla> p = (\<lambda>x. case p x of
\<lfloor>allow x\<rfloor> \<Rightarrow> \<lfloor>allow (f x)\<rfloor>
| \<lfloor>deny x\<rfloor> \<Rightarrow> \<lfloor>deny (g x)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
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) \<nabla> p = f o\<^sub>f p"
by(simp add: range_split_charn policy_range_comp_def)
lemma range_split_id [simp]: "(id,id) \<nabla> 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) \<nabla> (g1,g2) \<nabla> p = (f1 o g1,f2 o g2) \<nabla> 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.