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

Import of current (Isabelle 2017) release of UPF.

This commit is contained in:
Achim D. Brucker 2017-12-01 23:07:25 +00:00
parent 0108e7575b
commit f6ae1d216e
4 changed files with 18 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
UPF/ElementaryPolicies.thy
View File

@ -70,17 +70,17 @@ definition
\<lfloor>y\<rfloor> \<Rightarrow> \<lfloor>allow (y)\<rfloor>
|\<bottom> \<Rightarrow> \<bottom>)"
syntax (xsymbols)
syntax
"_allow_pfun" :: "('\<alpha> \<rightharpoonup>'\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("A\<^sub>p")
translations
"A\<^sub>p f" \<rightleftharpoons> "AllA f"
syntax (xsymbols)
syntax
"_deny_pfun" :: "('\<alpha> \<rightharpoonup>'\<beta>) \<Rightarrow> ('\<alpha> \<mapsto> '\<beta>)" ("D\<^sub>p")
translations
"D\<^sub>p f" \<rightleftharpoons> "AllD f"
notation (xsymbols)
notation
"deny_pfun" (binder "\<forall>D" 10) and
"allow_pfun" (binder "\<forall>A" 10)
@ -196,9 +196,6 @@ lemma sub_ran : "ran p \<subseteq> Allow \<union> Deny"
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

6
UPF/Monads.thy
View File

@ -77,7 +77,7 @@ where "bind_SE f g = (\<lambda>\<sigma>. case f \<sigma> of None \<Rightarro
| Some (out, \<sigma>') \<Rightarrow> g out \<sigma>')"
notation bind_SE ("bind\<^sub>S\<^sub>E")
syntax (xsymbols)
syntax
"_bind_SE" :: "[pttrn,('o,'\<sigma>)MON\<^sub>S\<^sub>E,('o','\<sigma>)MON\<^sub>S\<^sub>E] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>E"
("(2 _ \<leftarrow> _; _)" [5,8,8]8)
translations
@ -298,7 +298,7 @@ definition unit_SB :: "'o \<Rightarrow> ('o, '\<sigma>)MON\<^sub>S\<^sub>B" ("
where "unit_SB e = (\<lambda>\<sigma>. {(e,\<sigma>)})"
notation unit_SB ("unit\<^sub>S\<^sub>B")
syntax (xsymbols) "_bind_SB" :: "[pttrn,('o,'\<sigma>)MON\<^sub>S\<^sub>B,('o','\<sigma>)MON\<^sub>S\<^sub>B] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>B"
syntax "_bind_SB" :: "[pttrn,('o,'\<sigma>)MON\<^sub>S\<^sub>B,('o','\<sigma>)MON\<^sub>S\<^sub>B] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>B"
("(2 _ := _; _)" [5,8,8]8)
translations
"x := f; g" \<rightleftharpoons> "CONST bind_SB f (% x . g)"
@ -333,7 +333,7 @@ where "bind_SBE f g = (\<lambda>\<sigma>. case f \<sigma> of None \<Rightarr
in if None \<in> S' then None
else Some(\<Union> (the ` S'))))"
syntax (xsymbols) "_bind_SBE" :: "[pttrn,('o,'\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E,('o','\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E"
syntax "_bind_SBE" :: "[pttrn,('o,'\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E,('o','\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E] \<Rightarrow> ('o','\<sigma>)MON\<^sub>S\<^sub>B\<^sub>E"
("(2 _ :\<equiv> _; _)" [5,8,8]8)
translations
"x :\<equiv> f; g" \<rightleftharpoons> "CONST bind_SBE f (% x . g)"

8
UPF/SeqComposition.thy
View File

@ -178,7 +178,7 @@ definition
comp_orA :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>" (infixl "o'_orA" 55) where
"p2 o_orA p1 \<equiv> (map_option flat_orA) o (lift p2 \<circ>\<^sub>m p1)"
notation (xsymbols)
notation
comp_orA (infixl "\<circ>\<^sub>\<or>\<^sub>A" 55)
lemma comp_orA_mt[simp]:"p \<circ>\<^sub>\<or>\<^sub>A \<emptyset> = \<emptyset>"
@ -191,7 +191,7 @@ definition
comp_orD :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>" (infixl "o'_orD" 55) where
"p2 o_orD p1 \<equiv> (map_option flat_orD) o (lift p2 \<circ>\<^sub>m p1)"
notation (xsymbols)
notation
comp_orD (infixl "\<circ>\<^sub>orD" 55)
lemma comp_orD_mt[simp]:"p o_orD \<emptyset> = \<emptyset>"
@ -204,7 +204,7 @@ definition
comp_1 :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>" (infixl "o'_1" 55) where
"p2 o_1 p1 \<equiv> (map_option flat_1) o (lift p2 \<circ>\<^sub>m p1)"
notation (xsymbols)
notation
comp_1 (infixl "\<circ>\<^sub>1" 55)
lemma comp_1_mt[simp]:"p \<circ>\<^sub>1 \<emptyset> = \<emptyset>"
@ -217,7 +217,7 @@ definition
comp_2 :: "['\<beta>\<mapsto>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha>\<mapsto>'\<gamma>" (infixl "o'_2" 55) where
"p2 o_2 p1 \<equiv> (map_option flat_2) o (lift p2 \<circ>\<^sub>m p1)"
notation (xsymbols)
notation
comp_2 (infixl "\<circ>\<^sub>2" 55)
lemma comp_2_mt[simp]:"p \<circ>\<^sub>2 \<emptyset> = \<emptyset>"

26
UPF/UPFCore.thy
View File

@ -84,7 +84,7 @@ text{*In the following, we introduce a number of shortcuts and alternative notat
The type of policies is represented as: *}
translations (type) "'\<alpha> |-> '\<beta>" <= (type) "'\<alpha> \<rightharpoonup> '\<beta> decision"
type_notation (xsymbols) "policy" (infixr "\<mapsto>" 0)
type_notation "policy" (infixr "\<mapsto>" 0)
text{* ... allowing the notation @{typ "'\<alpha> \<mapsto> '\<beta>"} for the policy type and the
alternative notations for @{term None} and @{term Some} of the \HOL library
@ -123,16 +123,12 @@ text{*
nonterminal policylets and policylet
syntax
"_policylet1" :: "['a, 'a] => policylet" ("_ /+=/ _")
"_policylet2" :: "['a, 'a] => policylet" ("_ /-=/ _")
"_policylet1" :: "['a, 'a] => policylet" ("_ /\<mapsto>\<^sub>+/ _")
"_policylet2" :: "['a, 'a] => policylet" ("_ /\<mapsto>\<^sub>-/ _")
"" :: "policylet => policylets" ("_")
"_Maplets" :: "[policylet, policylets] => policylets" ("_,/ _")
"_Maplets" :: "[policylet, policylets] => policylets" ("_,/ _")
"_MapUpd" :: "['a |-> 'b, policylets] => 'a |-> 'b" ("_/'(_')" [900,0]900)
syntax (xsymbols)
"_policylet1" :: "['a, 'a] => policylet" ("_ /\<mapsto>\<^sub>+/ _")
"_policylet2" :: "['a, 'a] => policylet" ("_ /\<mapsto>\<^sub>-/ _")
"_emptypolicy" :: "'a |-> 'b" ("\<emptyset>")
translations
@ -142,7 +138,7 @@ translations
"\<emptyset>" \<rightleftharpoons> "CONST empty"
text{* Here are some lemmas essentially showing syntactic equivalences: *}
lemma test: "empty(x+=a, y-= b) = \<emptyset>(x \<mapsto>\<^sub>+ a, y \<mapsto>\<^sub>- b)" by simp
lemma test: "empty(x\<mapsto>\<^sub>+a, y\<mapsto>\<^sub>-b) = \<emptyset>(x \<mapsto>\<^sub>+ a, y \<mapsto>\<^sub>- b)" by simp
lemma test2: "p(x\<mapsto>\<^sub>+a,x\<mapsto>\<^sub>-b) = p(x\<mapsto>\<^sub>-b)" by simp
@ -181,12 +177,8 @@ text{*
theory (which does it in reverse order).
*}
syntax
"_policyoverride" :: "['a \<mapsto> 'b, 'a \<mapsto> 'b] \<Rightarrow> 'a \<mapsto> 'b" (infixl "(+p/)" 100)
syntax (xsymbols)
syntax
"_policyoverride" :: "['a \<mapsto> 'b, 'a \<mapsto> 'b] \<Rightarrow> 'a \<mapsto> 'b" (infixl "\<Oplus>" 100)
translations
"p \<Oplus> q" \<rightleftharpoons> "q ++ p"
@ -218,9 +210,8 @@ where "m2 ++_A m1 =
| \<bottom> \<Rightarrow> m2 x)
)"
syntax (xsymbols)
syntax
"_policyoverride_A" :: "['a \<mapsto> 'b, 'a \<mapsto> 'b] \<Rightarrow> 'a \<mapsto> 'b" (infixl "\<Oplus>\<^sub>A" 100)
translations
"p \<Oplus>\<^sub>A q" \<rightleftharpoons> "p ++_A q"
@ -253,7 +244,7 @@ where "m1 ++_D m2 =
| \<bottom> \<Rightarrow> m1 x
)"
syntax (xsymbols)
syntax
"_policyoverride_D" :: "['a \<mapsto> 'b, 'a \<mapsto> 'b] \<Rightarrow> 'a \<mapsto> 'b" (infixl "\<Oplus>\<^sub>D" 100)
translations
"p \<Oplus>\<^sub>D q" \<rightleftharpoons> "p ++_D q"
@ -294,9 +285,8 @@ where
| \<lfloor>deny y\<rfloor> \<Rightarrow> \<lfloor>deny (f y)\<rfloor>
| \<bottom> \<Rightarrow> \<bottom>)"
syntax (xsymbols)
syntax
"_policy_range_comp" :: "['\<beta>\<Rightarrow>'\<gamma>, '\<alpha>\<mapsto>'\<beta>] \<Rightarrow> '\<alpha> \<mapsto>'\<gamma>" (infixl "o\<^sub>f" 55)
translations
"p o\<^sub>f q" \<rightleftharpoons> "p o_f q"