From f6ae1d216e840a5d4c702b0dfa6bbaada52b3a12 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Fri, 1 Dec 2017 23:07:25 +0000 Subject: [PATCH] Import of current (Isabelle 2017) release of UPF. --- UPF/ElementaryPolicies.thy | 9 +++------ UPF/Monads.thy | 6 +++--- UPF/SeqComposition.thy | 8 ++++---- UPF/UPFCore.thy | 26 ++++++++------------------ 4 files changed, 18 insertions(+), 31 deletions(-) diff --git a/UPF/ElementaryPolicies.thy b/UPF/ElementaryPolicies.thy index 4b8eae2..ad05574 100644 --- a/UPF/ElementaryPolicies.thy +++ b/UPF/ElementaryPolicies.thy @@ -70,17 +70,17 @@ definition \y\ \ \allow (y)\ |\ \ \)" -syntax (xsymbols) +syntax "_allow_pfun" :: "('\ \'\) \ ('\ \ '\)" ("A\<^sub>p") translations "A\<^sub>p f" \ "AllA f" -syntax (xsymbols) +syntax "_deny_pfun" :: "('\ \'\) \ ('\ \ '\)" ("D\<^sub>p") translations "D\<^sub>p f" \ "AllD f" -notation (xsymbols) +notation "deny_pfun" (binder "\D" 10) and "allow_pfun" (binder "\A" 10) @@ -196,9 +196,6 @@ lemma sub_ran : "ran p \ Allow \ Deny" subgoal for x a apply (case_tac "x") apply (simp_all) - apply (rename_tac \) - apply (erule_tac x="\" in allE) - apply (simp) done done diff --git a/UPF/Monads.thy b/UPF/Monads.thy index 893c118..94ca85a 100644 --- a/UPF/Monads.thy +++ b/UPF/Monads.thy @@ -77,7 +77,7 @@ where "bind_SE f g = (\\. case f \ of None \') \ g out \')" notation bind_SE ("bind\<^sub>S\<^sub>E") -syntax (xsymbols) +syntax "_bind_SE" :: "[pttrn,('o,'\)MON\<^sub>S\<^sub>E,('o','\)MON\<^sub>S\<^sub>E] \ ('o','\)MON\<^sub>S\<^sub>E" ("(2 _ \ _; _)" [5,8,8]8) translations @@ -298,7 +298,7 @@ definition unit_SB :: "'o \ ('o, '\)MON\<^sub>S\<^sub>B" (" where "unit_SB e = (\\. {(e,\)})" notation unit_SB ("unit\<^sub>S\<^sub>B") -syntax (xsymbols) "_bind_SB" :: "[pttrn,('o,'\)MON\<^sub>S\<^sub>B,('o','\)MON\<^sub>S\<^sub>B] \ ('o','\)MON\<^sub>S\<^sub>B" +syntax "_bind_SB" :: "[pttrn,('o,'\)MON\<^sub>S\<^sub>B,('o','\)MON\<^sub>S\<^sub>B] \ ('o','\)MON\<^sub>S\<^sub>B" ("(2 _ := _; _)" [5,8,8]8) translations "x := f; g" \ "CONST bind_SB f (% x . g)" @@ -333,7 +333,7 @@ where "bind_SBE f g = (\\. case f \ of None \ S' then None else Some(\ (the ` S'))))" -syntax (xsymbols) "_bind_SBE" :: "[pttrn,('o,'\)MON\<^sub>S\<^sub>B\<^sub>E,('o','\)MON\<^sub>S\<^sub>B\<^sub>E] \ ('o','\)MON\<^sub>S\<^sub>B\<^sub>E" +syntax "_bind_SBE" :: "[pttrn,('o,'\)MON\<^sub>S\<^sub>B\<^sub>E,('o','\)MON\<^sub>S\<^sub>B\<^sub>E] \ ('o','\)MON\<^sub>S\<^sub>B\<^sub>E" ("(2 _ :\ _; _)" [5,8,8]8) translations "x :\ f; g" \ "CONST bind_SBE f (% x . g)" diff --git a/UPF/SeqComposition.thy b/UPF/SeqComposition.thy index b664882..55f5a5b 100644 --- a/UPF/SeqComposition.thy +++ b/UPF/SeqComposition.thy @@ -178,7 +178,7 @@ definition comp_orA :: "['\\'\, '\\'\] \ '\\'\" (infixl "o'_orA" 55) where "p2 o_orA p1 \ (map_option flat_orA) o (lift p2 \\<^sub>m p1)" -notation (xsymbols) +notation comp_orA (infixl "\\<^sub>\\<^sub>A" 55) lemma comp_orA_mt[simp]:"p \\<^sub>\\<^sub>A \ = \" @@ -191,7 +191,7 @@ definition comp_orD :: "['\\'\, '\\'\] \ '\\'\" (infixl "o'_orD" 55) where "p2 o_orD p1 \ (map_option flat_orD) o (lift p2 \\<^sub>m p1)" -notation (xsymbols) +notation comp_orD (infixl "\\<^sub>orD" 55) lemma comp_orD_mt[simp]:"p o_orD \ = \" @@ -204,7 +204,7 @@ definition comp_1 :: "['\\'\, '\\'\] \ '\\'\" (infixl "o'_1" 55) where "p2 o_1 p1 \ (map_option flat_1) o (lift p2 \\<^sub>m p1)" -notation (xsymbols) +notation comp_1 (infixl "\\<^sub>1" 55) lemma comp_1_mt[simp]:"p \\<^sub>1 \ = \" @@ -217,7 +217,7 @@ definition comp_2 :: "['\\'\, '\\'\] \ '\\'\" (infixl "o'_2" 55) where "p2 o_2 p1 \ (map_option flat_2) o (lift p2 \\<^sub>m p1)" -notation (xsymbols) +notation comp_2 (infixl "\\<^sub>2" 55) lemma comp_2_mt[simp]:"p \\<^sub>2 \ = \" diff --git a/UPF/UPFCore.thy b/UPF/UPFCore.thy index 0fefd47..9f4ad41 100644 --- a/UPF/UPFCore.thy +++ b/UPF/UPFCore.thy @@ -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) "'\ |-> '\" <= (type) "'\ \ '\ decision" -type_notation (xsymbols) "policy" (infixr "\" 0) +type_notation "policy" (infixr "\" 0) text{* ... allowing the notation @{typ "'\ \ '\"} 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" ("_ /\\<^sub>+/ _") + "_policylet2" :: "['a, 'a] => policylet" ("_ /\\<^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" ("_ /\\<^sub>+/ _") - "_policylet2" :: "['a, 'a] => policylet" ("_ /\\<^sub>-/ _") "_emptypolicy" :: "'a |-> 'b" ("\") translations @@ -142,7 +138,7 @@ translations "\" \ "CONST empty" text{* Here are some lemmas essentially showing syntactic equivalences: *} -lemma test: "empty(x+=a, y-= b) = \(x \\<^sub>+ a, y \\<^sub>- b)" by simp +lemma test: "empty(x\\<^sub>+a, y\\<^sub>-b) = \(x \\<^sub>+ a, y \\<^sub>- b)" by simp lemma test2: "p(x\\<^sub>+a,x\\<^sub>-b) = p(x\\<^sub>-b)" by simp @@ -181,12 +177,8 @@ text{* theory (which does it in reverse order). *} -syntax - "_policyoverride" :: "['a \ 'b, 'a \ 'b] \ 'a \ 'b" (infixl "(+p/)" 100) - -syntax (xsymbols) +syntax "_policyoverride" :: "['a \ 'b, 'a \ 'b] \ 'a \ 'b" (infixl "\" 100) - translations "p \ q" \ "q ++ p" @@ -218,9 +210,8 @@ where "m2 ++_A m1 = | \ \ m2 x) )" -syntax (xsymbols) +syntax "_policyoverride_A" :: "['a \ 'b, 'a \ 'b] \ 'a \ 'b" (infixl "\\<^sub>A" 100) - translations "p \\<^sub>A q" \ "p ++_A q" @@ -253,7 +244,7 @@ where "m1 ++_D m2 = | \ \ m1 x )" -syntax (xsymbols) +syntax "_policyoverride_D" :: "['a \ 'b, 'a \ 'b] \ 'a \ 'b" (infixl "\\<^sub>D" 100) translations "p \\<^sub>D q" \ "p ++_D q" @@ -294,9 +285,8 @@ where | \deny y\ \ \deny (f y)\ | \ \ \)" -syntax (xsymbols) +syntax "_policy_range_comp" :: "['\\'\, '\\'\] \ '\ \'\" (infixl "o\<^sub>f" 55) - translations "p o\<^sub>f q" \ "p o_f q"