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

Import of current (Isabelle 2016-1) release of UPF.

This commit is contained in:
Achim D. Brucker 2016-12-26 11:43:16 +00:00
parent 243939c32e
commit 635bc0f990
3 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Monads.thy
View File

@ -512,10 +512,10 @@ lemma assert_disch3 :" \<not> P \<sigma> \<Longrightarrow> \<not> (\<sigma> \<Tu
by(auto simp: bind_SE_def assert_SE_def valid_SE_def)
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.split_if_asm)
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.split_if_asm)
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)

4
Normalisation.thy
View File

@ -228,10 +228,10 @@ proof (induct p rule: rev_induct)
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: split_if_asm)
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: split_if_asm)
by (simp add: applied_rule_rev_def split: if_split_asm)
qed
qed

2
NormalisationTestSpecification.thy
View File

@ -130,7 +130,7 @@ definition disjDomGD where "disjDomGD p = disjDom (butlast p)"
lemma distrPUTLG1: "\<lbrakk>x \<in> dom P; (list2policy PL) x = P x; PUTListGD PUT x PL\<rbrakk> \<Longrightarrow> PUT x = P x"
apply (induct PL)
apply (simp_all add: domIff PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def)
apply (auto simp: dom_def domIff split: split_if_asm)
apply (auto simp: dom_def domIff split: if_split_asm)
done
lemma distrPUTLG2: