[STATEMENT]
lemma Example2:
notes Example2'n_proc_simp[proc_simp]
shows
 "\<Gamma>'' n, \<Theta>'' n
 |\<tturnstile>\<^bsub>/F\<^esub>\<lbrace>True\<rbrace>
   COBEGIN SCHEME [0\<le>i<n]
     \<lbrace>True\<rbrace>
       CALLX (\<lambda>s. s\<lparr>ex2_n:=(ex2_n s)(i:=i)\<rparr>) \<lbrace>\<acute>ex2_n i = i\<rbrace> (''f'', i) 0
       (\<lambda>s t. t\<lparr>ex2_n:= (ex2_n t)(i:=(ex2_n s) i)\<rparr>) (\<lambda>x y. Skip)
       \<lbrace>\<acute>ex2_a (\<acute>ex2_n i)='''' \<and> \<acute>ex2_n i = i\<rbrace> \<lbrace>\<acute>ex2_a i=''''\<rbrace> \<lbrace>False\<rbrace>  \<lbrace>False\<rbrace>
     \<lbrace>\<acute>ex2_a i=''''\<rbrace>, \<lbrace>False\<rbrace>
   COEND
  \<lbrace>\<forall>i < n. \<acute>ex2_a i = ''''\<rbrace>, \<lbrace>False\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>'' n, \<Theta>'' n |\<tturnstile>\<^bsub>/F\<^esub> \<lbrace>True\<rbrace>
COBEGIN
  SCHEME [0 \<le> i < n]
\<lbrace>True\<rbrace>
CALLX (\<lambda>s. s\<lparr>ex2_n := (ex2_n s)(i := i)\<rparr>)
\<lbrace>\<acute>ex2_n i = i\<rbrace> (''f'', i) 0
(\<lambda>s t. t\<lparr>ex2_n := (ex2_n t)(i := ex2_n s i)\<rparr>) (\<lambda>x y. Skip)
\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = [] \<and> \<acute>ex2_n i = i\<rbrace> \<lbrace>\<acute>ex2_a i = []\<rbrace>
\<lbrace>False\<rbrace> \<lbrace>False\<rbrace>
\<lbrace>\<acute>ex2_a i = []\<rbrace>, \<lbrace>False\<rbrace>
COEND
\<lbrace>\<forall>i<n. \<acute>ex2_a i = []\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
unfolding Example2'n_def ann_call_def call_def block_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>'' n, \<Theta>'' n |\<tturnstile>\<^bsub>/F\<^esub> \<lbrace>True\<rbrace>
COBEGIN
  SCHEME [0 \<le> i < n]
AnnCom (AnnRec \<lbrace>True\<rbrace> (AnnComp (AnnComp (AnnComp (AnnExpr \<lbrace>True\<rbrace>) (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)) (AnnComp (AnnExpr \<lbrace>False\<rbrace>) (AnnExpr \<lbrace>False\<rbrace>))) (AnnRec \<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = [] \<and> \<acute>ex2_n i = i\<rbrace> (AnnComp (AnnExpr \<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = [] \<and> \<acute>ex2_n i = i\<rbrace>) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>))))) (DynCom (\<lambda>s. Seq (Catch (Seq (Basic (\<lambda>s. s\<lparr>ex2_n := (ex2_n s)(i := i)\<rparr>)) (Call (''f'', i))) (Seq (Basic (\<lambda>t. t\<lparr>ex2_n := (ex2_n t)(i := ex2_n s i)\<rparr>)) Throw)) (DynCom (\<lambda>t. Seq (Basic (\<lambda>t. t\<lparr>ex2_n := (ex2_n t)(i := ex2_n s i)\<rparr>)) Skip))))
\<lbrace>\<acute>ex2_a i = []\<rbrace>, \<lbrace>False\<rbrace>
COEND
\<lbrace>\<forall>i<n. \<acute>ex2_a i = []\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
apply oghoare
[PROOF STATE]
proof (prove)
goal (113 subgoals):
 1. \<lbrace>True\<rbrace> \<subseteq> pre (AnnPar (map (\<lambda>i. (AnnRec \<lbrace>True\<rbrace> (AnnComp (AnnComp (AnnComp (AnnExpr \<lbrace>True\<rbrace>) (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)) (AnnComp (AnnExpr \<lbrace>False\<rbrace>) (AnnExpr \<lbrace>False\<rbrace>))) (AnnRec \<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = [] \<and> \<acute>ex2_n i = i\<rbrace> (AnnComp (AnnExpr \<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = [] \<and> \<acute>ex2_n i = i\<rbrace>) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>)))), \<lbrace>\<acute>ex2_a i = []\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n]))
 2. \<And>i. 0 \<le> i \<and> i < n \<Longrightarrow> \<lbrace>True\<rbrace> \<subseteq> pre (AnnComp (AnnComp (AnnComp (AnnExpr \<lbrace>True\<rbrace>) (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)) (AnnComp (AnnExpr \<lbrace>False\<rbrace>) (AnnExpr \<lbrace>False\<rbrace>))) (AnnRec (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>) (AnnComp (AnnExpr (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>)) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>))))
 3. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace> \<subseteq> pre (AnnComp (AnnExpr (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>)) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>))
 4. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<acute>ex2_n i = i\<rbrace> \<subseteq> pre (AnnExpr \<lbrace>\<acute>ex2_n i = i\<rbrace>)
 5. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<acute>ex2_n i = i\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_a_update (\<lambda>_. \<acute>ex2_a(\<acute>ex2_n i := []))) \<in> pre (AnnRec (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>) (AnnComp (AnnExpr (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>)) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>)))\<rbrace>
 6. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>False\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_n_update (\<lambda>_. \<acute>ex2_n(i := ex2_n s i))) \<in> pre (AnnExpr \<lbrace>False\<rbrace>)\<rbrace>
 7. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_n_update (\<lambda>_. \<acute>ex2_n(i := i))) \<in> pre (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)\<rbrace>
 8. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>False\<rbrace> \<subseteq> \<lbrace>False\<rbrace>
 9. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> i < n
 10. \<And>x i. \<lbrakk>x \<in> snd (snd (map (\<lambda>i. (AnnRec \<lbrace>True\<rbrace> (AnnComp (AnnComp (AnnComp (AnnExpr \<lbrace>True\<rbrace>) (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)) (AnnComp (AnnExpr \<lbrace>False\<rbrace>) (AnnExpr \<lbrace>False\<rbrace>))) (AnnRec (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>) (AnnComp (AnnExpr (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>)) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>)))), \<lbrace>\<acute>ex2_a i = []\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n - 0\<rbrakk> \<Longrightarrow> False
A total of 113 subgoals...
[PROOF STEP]
(* 113 subgoals *)
[PROOF STATE]
proof (prove)
goal (113 subgoals):
 1. \<lbrace>True\<rbrace> \<subseteq> pre (AnnPar (map (\<lambda>i. (AnnRec \<lbrace>True\<rbrace> (AnnComp (AnnComp (AnnComp (AnnExpr \<lbrace>True\<rbrace>) (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)) (AnnComp (AnnExpr \<lbrace>False\<rbrace>) (AnnExpr \<lbrace>False\<rbrace>))) (AnnRec \<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = [] \<and> \<acute>ex2_n i = i\<rbrace> (AnnComp (AnnExpr \<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = [] \<and> \<acute>ex2_n i = i\<rbrace>) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>)))), \<lbrace>\<acute>ex2_a i = []\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n]))
 2. \<And>i. 0 \<le> i \<and> i < n \<Longrightarrow> \<lbrace>True\<rbrace> \<subseteq> pre (AnnComp (AnnComp (AnnComp (AnnExpr \<lbrace>True\<rbrace>) (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)) (AnnComp (AnnExpr \<lbrace>False\<rbrace>) (AnnExpr \<lbrace>False\<rbrace>))) (AnnRec (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>) (AnnComp (AnnExpr (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>)) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>))))
 3. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace> \<subseteq> pre (AnnComp (AnnExpr (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>)) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>))
 4. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<acute>ex2_n i = i\<rbrace> \<subseteq> pre (AnnExpr \<lbrace>\<acute>ex2_n i = i\<rbrace>)
 5. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<acute>ex2_n i = i\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_a_update (\<lambda>_. \<acute>ex2_a(\<acute>ex2_n i := []))) \<in> pre (AnnRec (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>) (AnnComp (AnnExpr (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>)) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>)))\<rbrace>
 6. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>False\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_n_update (\<lambda>_. \<acute>ex2_n(i := ex2_n s i))) \<in> pre (AnnExpr \<lbrace>False\<rbrace>)\<rbrace>
 7. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_n_update (\<lambda>_. \<acute>ex2_n(i := i))) \<in> pre (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)\<rbrace>
 8. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>False\<rbrace> \<subseteq> \<lbrace>False\<rbrace>
 9. \<And>i s. \<lbrakk>0 \<le> i \<and> i < n; s \<in> \<lbrace>True\<rbrace>\<rbrakk> \<Longrightarrow> i < n
 10. \<And>x i. \<lbrakk>x \<in> snd (snd (map (\<lambda>i. (AnnRec \<lbrace>True\<rbrace> (AnnComp (AnnComp (AnnComp (AnnExpr \<lbrace>True\<rbrace>) (AnnCall \<lbrace>\<acute>ex2_n i = i\<rbrace> 0)) (AnnComp (AnnExpr \<lbrace>False\<rbrace>) (AnnExpr \<lbrace>False\<rbrace>))) (AnnRec (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>) (AnnComp (AnnExpr (\<lbrace>\<acute>ex2_a (\<acute>ex2_n i) = []\<rbrace> \<inter> \<lbrace>\<acute>ex2_n i = i\<rbrace>)) (AnnExpr \<lbrace>\<acute>ex2_a i = []\<rbrace>)))), \<lbrace>\<acute>ex2_a i = []\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n - 0\<rbrakk> \<Longrightarrow> False
A total of 113 subgoals...
[PROOF STEP]
apply (clarsimp ; fail)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Example2_list:
 "\<Gamma>, \<Theta> |\<tturnstile>\<^bsub>/F\<^esub>\<lbrace>n < length \<acute>ex2_A\<rbrace>
   COBEGIN
     SCHEME [0\<le>i<n] \<lbrace>n < length \<acute>ex2_A\<rbrace> \<acute>ex2_A:=\<acute>ex2_A[i:=0] \<lbrace>\<acute>ex2_A!i=0\<rbrace>,\<lbrace>False\<rbrace>
   COEND
    \<lbrace>\<forall>i < n. \<acute>ex2_A!i = 0\<rbrace>, X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>, \<Theta> |\<tturnstile>\<^bsub>/F\<^esub> \<lbrace>n < length \<acute>ex2_A\<rbrace>
COBEGIN
  SCHEME [0 \<le> i < n]
\<lbrace>n < length \<acute>ex2_A\<rbrace>
\<acute>ex2_A := \<acute>ex2_A[i := 0]
\<lbrace>\<acute>ex2_A ! i = 0\<rbrace>, \<lbrace>False\<rbrace>
COEND
\<lbrace>\<forall>i<n. \<acute>ex2_A ! i = 0\<rbrace>, X
[PROOF STEP]
apply oghoare
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> pre (AnnPar (map (\<lambda>i. (AnnExpr \<lbrace>n < length \<acute>ex2_A\<rbrace>, \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n]))
 2. \<And>i. 0 \<le> i \<and> i < n \<Longrightarrow> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_A_update (\<lambda>_. \<acute>ex2_A[i := 0])) \<in> \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>\<rbrace>
 3. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>\<acute>ex2_A ! i = 0\<rbrace> \<inter> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_A_update (\<lambda>_. \<acute>ex2_A[j := 0])) \<in> \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>\<rbrace>
 4. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<inter> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_A_update (\<lambda>_. \<acute>ex2_A[j := 0])) \<in> \<lbrace>n < length \<acute>ex2_A\<rbrace>\<rbrace>
 5. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>False\<rbrace> \<inter> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_A_update (\<lambda>_. \<acute>ex2_A[j := 0])) \<in> \<lbrace>False\<rbrace>\<rbrace>
 6. \<And>x i. \<lbrakk>x \<in> snd (snd (map (\<lambda>i. (AnnExpr \<lbrace>n < length \<acute>ex2_A\<rbrace>, \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n - 0\<rbrakk> \<Longrightarrow> x \<in> X
 7. \<And>x i. \<lbrakk>\<forall>i<n - 0. x \<in> fst (snd (map (\<lambda>i. (AnnExpr \<lbrace>n < length \<acute>ex2_A\<rbrace>, \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n\<rbrakk> \<Longrightarrow> ex2_A x ! i = 0
[PROOF STEP]
(*7 subgoals*)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> pre (AnnPar (map (\<lambda>i. (AnnExpr \<lbrace>n < length \<acute>ex2_A\<rbrace>, \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n]))
 2. \<And>i. 0 \<le> i \<and> i < n \<Longrightarrow> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_A_update (\<lambda>_. \<acute>ex2_A[i := 0])) \<in> \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>\<rbrace>
 3. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>\<acute>ex2_A ! i = 0\<rbrace> \<inter> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_A_update (\<lambda>_. \<acute>ex2_A[j := 0])) \<in> \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>\<rbrace>
 4. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<inter> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_A_update (\<lambda>_. \<acute>ex2_A[j := 0])) \<in> \<lbrace>n < length \<acute>ex2_A\<rbrace>\<rbrace>
 5. \<And>i j. 0 \<le> i \<and> i < n \<and> 0 \<le> j \<and> j < n \<and> i \<noteq> j \<Longrightarrow> \<lbrace>False\<rbrace> \<inter> \<lbrace>n < length \<acute>ex2_A\<rbrace> \<subseteq> \<lbrace>\<acute>(ex2_A_update (\<lambda>_. \<acute>ex2_A[j := 0])) \<in> \<lbrace>False\<rbrace>\<rbrace>
 6. \<And>x i. \<lbrakk>x \<in> snd (snd (map (\<lambda>i. (AnnExpr \<lbrace>n < length \<acute>ex2_A\<rbrace>, \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n - 0\<rbrakk> \<Longrightarrow> x \<in> X
 7. \<And>x i. \<lbrakk>\<forall>i<n - 0. x \<in> fst (snd (map (\<lambda>i. (AnnExpr \<lbrace>n < length \<acute>ex2_A\<rbrace>, \<lbrace>\<acute>ex2_A ! i = 0\<rbrace>, \<lbrace>False\<rbrace>)) [0..<n] ! i)); i < n\<rbrakk> \<Longrightarrow> ex2_A x ! i = 0
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma exceptions_example:
  "\<Gamma>, \<Theta> |\<turnstile>\<^bsub>/F\<^esub>
   TRY
   \<lbrace>True \<rbrace> \<acute>y := 0;;
   \<lbrace> \<acute>y = 0 \<rbrace> THROW
   CATCH
     \<lbrace>\<acute>y = 0\<rbrace> \<acute>x := \<acute>y + 1
   END
   \<lbrace> \<acute>x = 1 \<and> \<acute>y = 0\<rbrace>, \<lbrace>False\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>, \<Theta> |\<turnstile>\<^bsub>/F\<^esub> TRY \<lbrace>True\<rbrace>
\<acute>y := 0;;
\<lbrace>\<acute>y = 0\<rbrace> THROW
CATCH \<lbrace>\<acute>y = 0\<rbrace>
\<acute>x := \<acute>y + 1 END
\<lbrace>\<acute>x = 1 \<and> \<acute>y = 0\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
by oghoare simp_all


[STATEMENT]
lemma guard_example:
  "\<Gamma>, \<Theta> |\<turnstile>\<^bsub>/{42,66}\<^esub>
  \<lbrace>True\<rbrace> (42, \<lbrace>\<acute>x=0\<rbrace>),
   (66, \<lbrace>\<acute>y=0\<rbrace>) \<longmapsto> \<lbrace>\<acute>x = 0\<rbrace>
   \<acute>y := 0;;
   \<lbrace>True\<rbrace> \<acute>x := 0
  \<lbrace> \<acute>x = 0\<rbrace>, \<lbrace>False\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>, \<Theta> |\<turnstile>\<^bsub>/{42::'c, 66::'c}\<^esub> \<lbrace>True\<rbrace>
(42::'c, \<lbrace>\<acute>x = 0\<rbrace>), (66::'c, \<lbrace>\<acute>y = 0\<rbrace>) \<longmapsto> \<lbrace>\<acute>x = 0\<rbrace>
\<acute>y := 0;;
\<lbrace>True\<rbrace>
\<acute>x := 0
\<lbrace>\<acute>x = 0\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
apply oghoare
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrace>True\<rbrace> \<inter> snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<inter> snd (66::'c, \<lbrace>\<acute>y = 0\<rbrace>) \<subseteq> pre (AnnExpr \<lbrace>\<acute>x = 0\<rbrace>)
 2. \<lbrace>True\<rbrace> \<inter> snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<subseteq> pre (AnnRec (\<lbrace>True\<rbrace> \<inter> snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>)) (AnnExpr \<lbrace>\<acute>x = 0\<rbrace>))
 3. \<lbrace>True\<rbrace> \<inter> snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<inter> - snd (66::'c, \<lbrace>\<acute>y = 0\<rbrace>) \<noteq> {} \<longrightarrow> fst (66::'c, \<lbrace>\<acute>y = 0\<rbrace>) \<in> {42::'c, 66::'c}
 4. \<lbrace>True\<rbrace> \<inter> - snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<noteq> {} \<longrightarrow> fst (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<in> {42::'c, 66::'c}
 5. \<lbrace>\<acute>x = 0\<rbrace> \<subseteq> \<lbrace>\<acute>(y_update (\<lambda>_. 0)) \<in> pre (AnnExpr \<lbrace>True\<rbrace>)\<rbrace>
 6. \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(x_update (\<lambda>_. 0)) \<in> \<lbrace>\<acute>x = 0\<rbrace>\<rbrace>
[PROOF STEP]
(*6 subgoals*)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrace>True\<rbrace> \<inter> snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<inter> snd (66::'c, \<lbrace>\<acute>y = 0\<rbrace>) \<subseteq> pre (AnnExpr \<lbrace>\<acute>x = 0\<rbrace>)
 2. \<lbrace>True\<rbrace> \<inter> snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<subseteq> pre (AnnRec (\<lbrace>True\<rbrace> \<inter> snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>)) (AnnExpr \<lbrace>\<acute>x = 0\<rbrace>))
 3. \<lbrace>True\<rbrace> \<inter> snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<inter> - snd (66::'c, \<lbrace>\<acute>y = 0\<rbrace>) \<noteq> {} \<longrightarrow> fst (66::'c, \<lbrace>\<acute>y = 0\<rbrace>) \<in> {42::'c, 66::'c}
 4. \<lbrace>True\<rbrace> \<inter> - snd (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<noteq> {} \<longrightarrow> fst (42::'c, \<lbrace>\<acute>x = 0\<rbrace>) \<in> {42::'c, 66::'c}
 5. \<lbrace>\<acute>x = 0\<rbrace> \<subseteq> \<lbrace>\<acute>(y_update (\<lambda>_. 0)) \<in> pre (AnnExpr \<lbrace>True\<rbrace>)\<rbrace>
 6. \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(x_update (\<lambda>_. 0)) \<in> \<lbrace>\<acute>x = 0\<rbrace>\<rbrace>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma peterson_thread_1:
 "\<Gamma>, \<Theta> |\<turnstile>\<^bsub>/F\<^esub> \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>  WHILE True INV \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>
  DO
  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace> \<langle>\<acute>in1:=True,, \<acute>pr1:=1 \<rangle>;;
  \<lbrace>\<acute>pr1=1 \<and> \<acute>in1\<rbrace>  \<langle>\<acute>hold:=1,, \<acute>pr1:=2 \<rangle>;;
  \<lbrace>\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)\<rbrace>
  AWAIT (\<not>\<acute>in2 \<or> \<not>(\<acute>hold=1)) THEN
     \<acute>pr1:=3
  END;;
  \<lbrace>\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> \<acute>hold=2 \<and> \<acute>pr2=2)\<rbrace>
   \<langle>\<acute>in1:=False,,\<acute>pr1:=0\<rangle>
  OD \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>,\<lbrace>False\<rbrace>
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>, \<Theta> |\<turnstile>\<^bsub>/F\<^esub> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
WHILE True INV \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
DO \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
\<langle>\<acute>in1 := True;;
\<acute>pr1 := 1\<rangle>;;
\<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace>
\<langle>\<acute>hold := 1;;
\<acute>pr1 := 2\<rangle>;;
\<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace>
AWAIT \<not> \<acute>in2 \<or> \<acute>hold \<noteq> 1 THEN \<acute>pr1 := 3 END;;
\<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace>
\<langle>\<acute>in1 := False;;
\<acute>pr1 := 0\<rangle>
OD
\<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
apply oghoare
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> \<inter> \<lbrace>\<not> \<acute>in2 \<or> \<acute>hold \<noteq> 1\<rbrace> \<subseteq> \<lbrace>\<acute>(pr1_update (\<lambda>_. 3)) \<in> pre (AnnRec \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>
 2. \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in1_update (\<lambda>_. False)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 0)) \<in> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>\<rbrace>\<rbrace>
 3. \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<inter> - \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
 4. \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> pre (AnnComp (AnnComp (AnnComp (AnnRec \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) (AnnRec \<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))) (AnnRec \<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnExpr FAKE_ANN))) (AnnRec \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))))
 5. \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in1_update (\<lambda>_. True)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 1)) \<in> pre (AnnRec \<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>\<rbrace>
 6. \<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(hold_update (\<lambda>_. 1)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 2)) \<in> pre (AnnRec \<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnExpr FAKE_ANN))\<rbrace>\<rbrace>
 7. \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<subseteq> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
[PROOF STEP]
(*7 subgoals*)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> \<inter> \<lbrace>\<not> \<acute>in2 \<or> \<acute>hold \<noteq> 1\<rbrace> \<subseteq> \<lbrace>\<acute>(pr1_update (\<lambda>_. 3)) \<in> pre (AnnRec \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>
 2. \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in1_update (\<lambda>_. False)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 0)) \<in> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>\<rbrace>\<rbrace>
 3. \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<inter> - \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
 4. \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> pre (AnnComp (AnnComp (AnnComp (AnnRec \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) (AnnRec \<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))) (AnnRec \<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnExpr FAKE_ANN))) (AnnRec \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))))
 5. \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in1_update (\<lambda>_. True)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 1)) \<in> pre (AnnRec \<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>\<rbrace>
 6. \<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(hold_update (\<lambda>_. 1)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 2)) \<in> pre (AnnRec \<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnExpr FAKE_ANN))\<rbrace>\<rbrace>
 7. \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<subseteq> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
[PROOF STEP]
apply (((auto)[1]) ; fail)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma peterson_thread_2:
 "\<Gamma>, \<Theta> |\<turnstile>\<^bsub>/F\<^esub>  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
  WHILE True INV \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
  DO
  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace> \<langle>\<acute>in2:=True,, \<acute>pr2:=1 \<rangle>;;
  \<lbrace>\<acute>pr2=1 \<and> \<acute>in2\<rbrace> \<langle> \<acute>hold:=2,, \<acute>pr2:=2 \<rangle> ;;
  \<lbrace>\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
  AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3 END;;
  \<lbrace>\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
    \<langle>\<acute>in2:=False,, \<acute>pr2:=0\<rangle>
  OD \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>,\<lbrace>False\<rbrace>
 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>, \<Theta> |\<turnstile>\<^bsub>/F\<^esub> \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
WHILE True INV \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
DO \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
\<langle>\<acute>in2 := True;;
\<acute>pr2 := 1\<rangle>;;
\<lbrace>\<acute>pr2 = 1 \<and> \<acute>in2\<rbrace>
\<langle>\<acute>hold := 2;;
\<acute>pr2 := 2\<rangle>;;
\<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace>
AWAIT \<not> \<acute>in1 \<or> \<acute>hold \<noteq> 2 THEN \<acute>pr2 := 3 END;;
\<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace>
\<langle>\<acute>in2 := False;;
\<acute>pr2 := 0\<rangle>
OD
\<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
apply oghoare
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> \<inter> \<lbrace>\<not> \<acute>in1 \<or> \<acute>hold \<noteq> 2\<rbrace> \<subseteq> \<lbrace>\<acute>(pr2_update (\<lambda>_. 3)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>
 2. \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in2_update (\<lambda>_. False)) \<in> \<lbrace>\<acute>(pr2_update (\<lambda>_. 0)) \<in> \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>\<rbrace>\<rbrace>
 3. \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> \<inter> - \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
 4. \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> pre (AnnComp (AnnComp (AnnComp (AnnRec \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) (AnnRec \<lbrace>\<acute>pr2 = 1 \<and> \<acute>in2\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))) (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN))) (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))))
 5. \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in2_update (\<lambda>_. True)) \<in> \<lbrace>\<acute>(pr2_update (\<lambda>_. 1)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 1 \<and> \<acute>in2\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>\<rbrace>
 6. \<lbrace>\<acute>pr2 = 1 \<and> \<acute>in2\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(hold_update (\<lambda>_. 2)) \<in> \<lbrace>\<acute>(pr2_update (\<lambda>_. 2)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN))\<rbrace>\<rbrace>
 7. \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> \<subseteq> \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
[PROOF STEP]
(*7 subgoals*)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> \<inter> \<lbrace>\<not> \<acute>in1 \<or> \<acute>hold \<noteq> 2\<rbrace> \<subseteq> \<lbrace>\<acute>(pr2_update (\<lambda>_. 3)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>
 2. \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in2_update (\<lambda>_. False)) \<in> \<lbrace>\<acute>(pr2_update (\<lambda>_. 0)) \<in> \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>\<rbrace>\<rbrace>
 3. \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> \<inter> - \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
 4. \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> pre (AnnComp (AnnComp (AnnComp (AnnRec \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) (AnnRec \<lbrace>\<acute>pr2 = 1 \<and> \<acute>in2\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))) (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN))) (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))))
 5. \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in2_update (\<lambda>_. True)) \<in> \<lbrace>\<acute>(pr2_update (\<lambda>_. 1)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 1 \<and> \<acute>in2\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>\<rbrace>
 6. \<lbrace>\<acute>pr2 = 1 \<and> \<acute>in2\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(hold_update (\<lambda>_. 2)) \<in> \<lbrace>\<acute>(pr2_update (\<lambda>_. 2)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN))\<rbrace>\<rbrace>
 7. \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace> \<subseteq> \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
[PROOF STEP]
by auto


[STATEMENT]
lemma Petersons_mutex_1:
  "\<Gamma>, \<Theta> |\<tturnstile>\<^bsub>/F\<^esub> \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2 \<rbrace>
  COBEGIN
  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<rbrace>  WHILE True INV \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>
  DO
  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace> \<langle> \<acute>in1:=True,, \<acute>pr1:=1 \<rangle>;;
  \<lbrace>\<acute>pr1=1 \<and> \<acute>in1\<rbrace>  \<langle> \<acute>hold:=1,,  \<acute>pr1:=2 \<rangle>;;
  \<lbrace>\<acute>pr1=2 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> (\<acute>hold=2 \<and> \<acute>pr2=2))\<rbrace>
  AWAIT (\<not>\<acute>in2 \<or> \<not>(\<acute>hold=1)) THEN \<acute>pr1:=3  END;;
  \<lbrace>\<acute>pr1=3 \<and> \<acute>in1 \<and> (\<acute>hold=1 \<or> (\<acute>hold=2 \<and> \<acute>pr2=2))\<rbrace>
   \<langle> \<acute>in1:=False,, \<acute>pr1:=0\<rangle>
  OD \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1\<rbrace>,\<lbrace>False\<rbrace>
  \<parallel>
  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
  WHILE True INV \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>
  DO
  \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace> \<langle> \<acute>in2:=True,, \<acute>pr2:=1 \<rangle>;;
  \<lbrace>\<acute>pr2=1 \<and> \<acute>in2\<rbrace> \<langle> \<acute>hold:=2,, \<acute>pr2:=2 \<rangle> ;;
  \<lbrace>\<acute>pr2=2 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
  AWAIT (\<not>\<acute>in1 \<or> \<not>(\<acute>hold=2)) THEN \<acute>pr2:=3 END;;
  \<lbrace>\<acute>pr2=3 \<and> \<acute>in2 \<and> (\<acute>hold=2 \<or> (\<acute>hold=1 \<and> \<acute>pr1=2))\<rbrace>
    \<langle> \<acute>in2:=False,, \<acute>pr2:=0\<rangle>
  OD \<lbrace>\<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>,\<lbrace>False\<rbrace>
  COEND
  \<lbrace>\<acute>pr1=0 \<and> \<not>\<acute>in1 \<and> \<acute>pr2=0 \<and> \<not>\<acute>in2\<rbrace>,\<lbrace>False\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>, \<Theta> |\<tturnstile>\<^bsub>/F\<^esub> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1 \<and> \<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
COBEGIN
  \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
WHILE True INV \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
DO \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>
\<langle>\<acute>in1 := True;;
\<acute>pr1 := 1\<rangle>;;
\<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace>
\<langle>\<acute>hold := 1;;
\<acute>pr1 := 2\<rangle>;;
\<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace>
AWAIT \<not> \<acute>in2 \<or> \<acute>hold \<noteq> 1 THEN \<acute>pr1 := 3 END;;
\<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace>
\<langle>\<acute>in1 := False;;
\<acute>pr1 := 0\<rangle>
OD
\<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace>, \<lbrace>False\<rbrace>
\<parallel>
  \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
WHILE True INV \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
DO \<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>
\<langle>\<acute>in2 := True;;
\<acute>pr2 := 1\<rangle>;;
\<lbrace>\<acute>pr2 = 1 \<and> \<acute>in2\<rbrace>
\<langle>\<acute>hold := 2;;
\<acute>pr2 := 2\<rangle>;;
\<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace>
AWAIT \<not> \<acute>in1 \<or> \<acute>hold \<noteq> 2 THEN \<acute>pr2 := 3 END;;
\<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace>
\<langle>\<acute>in2 := False;;
\<acute>pr2 := 0\<rangle>
OD
\<lbrace>\<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>, \<lbrace>False\<rbrace>
COEND
\<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1 \<and> \<acute>pr2 = 0 \<and> \<not> \<acute>in2\<rbrace>, \<lbrace>False\<rbrace>
[PROOF STEP]
apply oghoare
\<comment> \<open>81 verification conditions.\<close>
[PROOF STATE]
proof (prove)
goal (81 subgoals):
 1. pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) \<inter> \<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> \<inter> \<lbrace>\<not> \<acute>in2 \<or> \<acute>hold \<noteq> 1\<rbrace> \<subseteq> \<lbrace>\<acute>(pr1_update (\<lambda>_. 3)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>
 2. pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) \<inter> \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in1_update (\<lambda>_. False)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 0)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>\<rbrace>
 3. pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) \<inter> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in1_update (\<lambda>_. True)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 1)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>\<rbrace>
 4. pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) \<inter> \<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(hold_update (\<lambda>_. 1)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 2)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>\<rbrace>
 5. pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN)) \<inter> \<lbrace>\<acute>pr1 = 2 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> \<inter> \<lbrace>\<not> \<acute>in2 \<or> \<acute>hold \<noteq> 1\<rbrace> \<subseteq> \<lbrace>\<acute>(pr1_update (\<lambda>_. 3)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN))\<rbrace>
 6. pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN)) \<inter> \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in1_update (\<lambda>_. False)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 0)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN))\<rbrace>\<rbrace>
 7. pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN)) \<inter> \<lbrace>\<acute>pr1 = 0 \<and> \<not> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in1_update (\<lambda>_. True)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 1)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN))\<rbrace>\<rbrace>
 8. pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN)) \<inter> \<lbrace>\<acute>pr1 = 1 \<and> \<acute>in1\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(hold_update (\<lambda>_. 1)) \<in> \<lbrace>\<acute>(pr1_update (\<lambda>_. 2)) \<in> pre (AnnRec \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> (AnnExpr FAKE_ANN))\<rbrace>\<rbrace>
 9. pre (AnnRec \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) \<inter> \<lbrace>\<acute>pr2 = 2 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> \<inter> \<lbrace>\<not> \<acute>in1 \<or> \<acute>hold \<noteq> 2\<rbrace> \<subseteq> \<lbrace>\<acute>(pr2_update (\<lambda>_. 3)) \<in> pre (AnnRec \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>
 10. pre (AnnRec \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN))) \<inter> \<lbrace>\<acute>pr2 = 3 \<and> \<acute>in2 \<and> (\<acute>hold = 2 \<or> \<acute>hold = 1 \<and> \<acute>pr1 = 2)\<rbrace> \<inter> \<lbrace>True\<rbrace> \<subseteq> \<lbrace>\<acute>(in2_update (\<lambda>_. False)) \<in> \<lbrace>\<acute>(pr2_update (\<lambda>_. 0)) \<in> pre (AnnRec \<lbrace>\<acute>pr1 = 3 \<and> \<acute>in1 \<and> (\<acute>hold = 1 \<or> \<acute>hold = 2 \<and> \<acute>pr2 = 2)\<rbrace> (AnnComp (AnnExpr FAKE_ANN) (AnnExpr FAKE_ANN)))\<rbrace>\<rbrace>
A total of 81 subgoals...
[PROOF STEP]
by auto


[STATEMENT]
lemma s0_obs_id [simp]: "obs s0 = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs s0 = id
[PROOF STEP]
by (simp add: s0_def)


[STATEMENT]
lemma s0_secrecy_init [iff]: "init s0 \<subseteq> s0_secrecy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init s0 \<subseteq> s0_secrecy
[PROOF STEP]
by (simp add: s0_defs)


[STATEMENT]
lemma s0_secrecy_trans [simp, intro]: "{s0_secrecy} trans s0 {> s0_secrecy}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s0_secrecy} TS.trans s0 {> s0_secrecy}
[PROOF STEP]
apply (auto simp add: s0_all_defs PO_hoare_defs intro!: s0_secrecyI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb xc. \<lbrakk>xa \<in> s0_secrecy; xb \<in> synth (analz (ik xa)); xc \<notin> synth (analz (ik xa)); xb \<in> secret xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma s0_secrecy [iff]:"reach s0 \<subseteq> s0_secrecy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach s0 \<subseteq> s0_secrecy
[PROOF STEP]
by (rule inv_rule_basic, auto)


[STATEMENT]
lemma s0_obs_secrecy [iff]:"oreach s0 \<subseteq> s0_secrecy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oreach s0 \<subseteq> s0_secrecy
[PROOF STEP]
by (rule external_from_internal_invariant) (auto del: subsetI)


[STATEMENT]
lemma pmf_mix: "a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x
[PROOF STEP]
by (simp add: mix_pmf_def pmf_bind)


[STATEMENT]
lemma pmf_mix_deeper: "a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf a p q) x = a * pmf p x + pmf q x - a * pmf q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf a p q) x = a * pmf p x + pmf q x - a * pmf q x
[PROOF STEP]
by (simp add: left_diff_distrib' pmf_mix)


[STATEMENT]
lemma bernoulli_pmf_0 [simp]: "bernoulli_pmf 0 = return_pmf False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf 0 = return_pmf False
[PROOF STEP]
by (intro pmf_eqI) (auto simp: bernoulli_pmf.rep_eq)


[STATEMENT]
lemma bernoulli_pmf_1 [simp]: "bernoulli_pmf 1 = return_pmf True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf 1 = return_pmf True
[PROOF STEP]
by (intro pmf_eqI) (auto simp: bernoulli_pmf.rep_eq)


[STATEMENT]
lemma pmf_mix_0 [simp]: "mix_pmf 0 p q = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf 0 p q = q
[PROOF STEP]
by (simp add: mix_pmf_def bind_return_pmf)


[STATEMENT]
lemma pmf_mix_1 [simp]: "mix_pmf 1 p q = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf 1 p q = p
[PROOF STEP]
by (simp add: mix_pmf_def bind_return_pmf)


[STATEMENT]
lemma set_pmf_mix: "a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf a p q) = set_pmf p \<union> set_pmf q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf a p q) = set_pmf p \<union> set_pmf q
[PROOF STEP]
by (auto simp add: mix_pmf_def split: if_splits)


[STATEMENT]
lemma set_pmf_mix_eq: "a \<in> {0..1} \<Longrightarrow> mix_pmf a p p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {0..1} \<Longrightarrow> mix_pmf a p p = p
[PROOF STEP]
by (simp add: mix_pmf_def)


[STATEMENT]
lemma pmf_equiv_intro[intro]:
  assumes "\<And>e. e \<in> set_pmf p \<Longrightarrow> pmf p e = pmf q e"
  assumes "\<And>e. e \<in> set_pmf q \<Longrightarrow> pmf q e = pmf p e"
  shows "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
by (metis assms(2) less_irrefl pmf_neq_exists_less pmf_not_neg set_pmf_iff)


[STATEMENT]
lemma pmf_equiv_intro1[intro]:
  assumes "\<And>e. e \<in> set_pmf p \<Longrightarrow> pmf p e = pmf q e"
  shows "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
by (standard, auto simp: assms, metis assms set_pmf_iff assms
      linorder_not_le order_refl pmf_neq_exists_less pmf_not_neg set_pmf_iff)


[STATEMENT]
lemma pmf_inverse_switch_eqals:
  assumes "a \<in> {0..1}"
  shows "mix_pmf a p q = mix_pmf (1-a) q p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf a p q = mix_pmf (1 - a) q p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mix_pmf a p q = mix_pmf (1 - a) q p
[PROOF STEP]
have fst: "\<forall>x \<in> set_pmf p. pmf (mix_pmf a p q) x = pmf (mix_pmf (1-a) q p) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set_pmf p. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf p \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf p \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
assume "x \<in> set_pmf p"
[PROOF STATE]
proof (state)
this:
x \<in> set_pmf p

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf p \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
have "pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x
[PROOF STEP]
using pmf_mix[of a p q x] assms
[PROOF STATE]
proof (prove)
using this:
a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x
a \<in> {0..1}

goal (1 subgoal):
 1. pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf p \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf p \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
have "... = a * pmf p x +  pmf q x - a * pmf q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * pmf p x + (1 - a) * pmf q x = a * pmf p x + pmf q x - a * pmf q x
[PROOF STEP]
by (simp add: left_diff_distrib)
[PROOF STATE]
proof (state)
this:
a * pmf p x + (1 - a) * pmf q x = a * pmf p x + pmf q x - a * pmf q x

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf p \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
from pmf_mix[of "1-a" q p x] assms
[PROOF STATE]
proof (chain)
picking this:
1 - a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x
a \<in> {0..1}
[PROOF STEP]
have "pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x"
[PROOF STATE]
proof (prove)
using this:
1 - a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x
a \<in> {0..1}

goal (1 subgoal):
 1. pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf p \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x
[PROOF STEP]
show "pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x"
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x

goal (1 subgoal):
 1. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x
pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x

goal (1 subgoal):
 1. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_pmf p. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x

goal (1 subgoal):
 1. mix_pmf a p q = mix_pmf (1 - a) q p
[PROOF STEP]
have "\<forall>x \<in> set_pmf q. pmf (mix_pmf a p q) x =  pmf (mix_pmf (1-a) q p) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set_pmf q. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf q \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf q \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
assume "x \<in> set_pmf q"
[PROOF STATE]
proof (state)
this:
x \<in> set_pmf q

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf q \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
have "pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x
[PROOF STEP]
using pmf_mix[of a p q x] assms
[PROOF STATE]
proof (prove)
using this:
a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x
a \<in> {0..1}

goal (1 subgoal):
 1. pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf q \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf q \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
have "... = a * pmf p x +  pmf q x - a * pmf q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * pmf p x + (1 - a) * pmf q x = a * pmf p x + pmf q x - a * pmf q x
[PROOF STEP]
by (simp add: left_diff_distrib)
[PROOF STATE]
proof (state)
this:
a * pmf p x + (1 - a) * pmf q x = a * pmf p x + pmf q x - a * pmf q x

goal (1 subgoal):
 1. \<And>x. x \<in> set_pmf q \<Longrightarrow> pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
from pmf_mix[of "1-a" q p x] assms
[PROOF STATE]
proof (chain)
picking this:
1 - a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x
a \<in> {0..1}
[PROOF STEP]
show "pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x"
[PROOF STATE]
proof (prove)
using this:
1 - a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x
a \<in> {0..1}

goal (1 subgoal):
 1. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
1 - a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf (1 - a) q p) x = (1 - a) * pmf q x + (1 - (1 - a)) * pmf p x
a \<in> {0..1}
pmf (mix_pmf a p q) x = a * pmf p x + (1 - a) * pmf q x

goal (1 subgoal):
 1. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_pmf q. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x

goal (1 subgoal):
 1. mix_pmf a p q = mix_pmf (1 - a) q p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set_pmf q. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
have "\<forall>x \<in> set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) x =  pmf (mix_pmf (1-a) q p) x"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set_pmf q. pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x

goal (1 subgoal):
 1. \<forall>x\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x
[PROOF STEP]
by (metis (no_types) fst add_0_left assms mult_eq_0_iff pmf_mix set_pmf_iff)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x

goal (1 subgoal):
 1. mix_pmf a p q = mix_pmf (1 - a) q p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) x = pmf (mix_pmf (1 - a) q p) x

goal (1 subgoal):
 1. mix_pmf a p q = mix_pmf (1 - a) q p
[PROOF STEP]
by (simp add: pmf_equiv_intro1)
[PROOF STATE]
proof (state)
this:
mix_pmf a p q = mix_pmf (1 - a) q p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mix_pmf_comp_left_div:
  assumes "\<alpha> \<in> {0..(1::real)}"
    and "\<beta> \<in> {0..(1::real)}"
  assumes "\<alpha> > \<beta>"
  shows "pmf (mix_pmf (\<beta>/\<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
let ?l = "(mix_pmf (\<beta>/\<alpha>) (mix_pmf \<alpha> p q) q)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
have fst: "pmf ?l e = (\<beta>/\<alpha>) * pmf (mix_pmf \<alpha> p q) e + (1-\<beta>/\<alpha>) * pmf q e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
by (meson assms(1) assms(2) assms(3) atLeastAtMost_iff less_divide_eq_1
        less_eq_real_def not_less pmf_mix zero_le_divide_iff)
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
have "pmf (mix_pmf \<alpha> p q) e = \<alpha> * pmf p e + (1 - \<alpha>) * pmf q e"
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf \<alpha> p q) e = \<alpha> * pmf p e + (1 - \<alpha>) * pmf q e
[PROOF STEP]
using pmf_mix[of "\<alpha>" p q] assms(2) assms(3) assms(1)
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e
\<alpha> \<in> {0..1} \<Longrightarrow> pmf (mix_pmf \<alpha> p q) ?x = \<alpha> * pmf p ?x + (1 - \<alpha>) * pmf q ?x
\<beta> \<in> {0..1}
\<beta> < \<alpha>
\<alpha> \<in> {0..1}

goal (1 subgoal):
 1. pmf (mix_pmf \<alpha> p q) e = \<alpha> * pmf p e + (1 - \<alpha>) * pmf q e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf \<alpha> p q) e = \<alpha> * pmf p e + (1 - \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
have "pmf ?l e = (\<beta>/\<alpha>) * (\<alpha> * pmf p e + (1 - \<alpha>) * pmf q e) + (1-\<beta>/\<alpha>) * pmf q e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * (\<alpha> * pmf p e + (1 - \<alpha>) * pmf q e) + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
using fst assms(1) pmf_mix
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e
\<alpha> \<in> {0..1}
?a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf ?a ?p ?q) ?x = ?a * pmf ?p ?x + (1 - ?a) * pmf ?q ?x

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * (\<alpha> * pmf p e + (1 - \<alpha>) * pmf q e) + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * (\<alpha> * pmf p e + (1 - \<alpha>) * pmf q e) + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * (\<alpha> * pmf p e + (1 - \<alpha>) * pmf q e) + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
have "pmf ?l e = ((\<beta>/\<alpha>) *\<alpha> * pmf p e + (\<beta>/\<alpha>) *(1 - \<alpha>) * pmf q e) + (1-\<beta>/\<alpha>) * pmf q e"
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * (\<alpha> * pmf p e + (1 - \<alpha>) * pmf q e) + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * \<alpha> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
using fst assms(1)
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * (\<alpha> * pmf p e + (1 - \<alpha>) * pmf q e) + (1 - \<beta> / \<alpha>) * pmf q e
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e
\<alpha> \<in> {0..1}

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * \<alpha> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
by (metis  mult.assoc  ring_class.ring_distribs(1))
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * \<alpha> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * \<alpha> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
have *: "pmf ?l e = (\<beta> * pmf p e + (\<beta>/\<alpha>) *(1 - \<alpha>) * pmf q e) + (1-\<beta>/\<alpha>) * pmf q e"
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * \<alpha> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
using fst assms(1) assms(2) assms(3)
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * \<alpha> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e
\<alpha> \<in> {0..1}
\<beta> \<in> {0..1}
\<beta> < \<alpha>

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
have "pmf ?l e = (\<beta> * pmf p e + ((\<beta>/\<alpha>) - (\<beta>/\<alpha>)*\<alpha>) * pmf q e) + (1-\<beta>/\<alpha>) * pmf q e"
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta> / \<alpha> * \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
using fst assms(1) assms(2) assms(3)
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * (1 - \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e
\<alpha> \<in> {0..1}
\<beta> \<in> {0..1}
\<beta> < \<alpha>

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta> / \<alpha> * \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
by (simp add: * diff_divide_distrib right_diff_distrib')
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta> / \<alpha> * \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta> / \<alpha> * \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
have "pmf ?l e = (\<beta> * pmf p e + ((\<beta>/\<alpha>) - \<beta>) * pmf q e) + (1-\<beta>/\<alpha>) * pmf q e"
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta> / \<alpha> * \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
using fst assms(1) assms(2) assms(3)
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta> / \<alpha> * \<alpha>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> / \<alpha> * pmf (mix_pmf \<alpha> p q) e + (1 - \<beta> / \<alpha>) * pmf q e
\<alpha> \<in> {0..1}
\<beta> \<in> {0..1}
\<beta> < \<alpha>

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e
[PROOF STEP]
have "pmf ?l e = (\<beta> * pmf p e + (\<beta>/\<alpha>) * pmf q e - \<beta> * pmf q e) + 1* pmf q e-\<beta>/\<alpha>* pmf q e"
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + (\<beta> / \<alpha> - \<beta>) * pmf q e + (1 - \<beta> / \<alpha>) * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * pmf q e - \<beta> * pmf q e + 1 * pmf q e - \<beta> / \<alpha> * pmf q e
[PROOF STEP]
by (simp add: left_diff_distrib)
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * pmf q e - \<beta> * pmf q e + 1 * pmf q e - \<beta> / \<alpha> * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + \<beta> / \<alpha> * pmf q e - \<beta> * pmf q e + 1 * pmf q e - \<beta> / \<alpha> * pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mix_pmf_comp_with_dif_equiv:
  assumes "\<alpha> \<in> {0..(1::real)}"
    and "\<beta> \<in> {0..(1::real)}"
  assumes "\<alpha> > \<beta>"
  shows "mix_pmf (\<beta>/\<alpha>) (mix_pmf \<alpha> p q) q = mix_pmf \<beta> p q" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q = mix_pmf \<beta> p q
[PROOF STEP]
proof (rule pmf_equiv_intro1[symmetric])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf (mix_pmf \<beta> p q) \<Longrightarrow> pmf (mix_pmf \<beta> p q) e = pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf (mix_pmf \<beta> p q) \<Longrightarrow> pmf (mix_pmf \<beta> p q) e = pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e
[PROOF STEP]
assume a: "e \<in> set_pmf ?r"
[PROOF STATE]
proof (state)
this:
e \<in> set_pmf (mix_pmf \<beta> p q)

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf (mix_pmf \<beta> p q) \<Longrightarrow> pmf (mix_pmf \<beta> p q) e = pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e
[PROOF STEP]
have "e \<in> set_pmf ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> set_pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q)
[PROOF STEP]
using a pmf_mix_deeper
[PROOF STATE]
proof (prove)
using this:
e \<in> set_pmf (mix_pmf \<beta> p q)
?a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf ?a ?p ?q) ?x = ?a * pmf ?p ?x + pmf ?q ?x - ?a * pmf ?q ?x

goal (1 subgoal):
 1. e \<in> set_pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q)
[PROOF STEP]
by (metis assms(1) assms(2) assms(3) mix_pmf_comp_left_div pmf_eq_0_set_pmf)
[PROOF STATE]
proof (state)
this:
e \<in> set_pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q)

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf (mix_pmf \<beta> p q) \<Longrightarrow> pmf (mix_pmf \<beta> p q) e = pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<in> set_pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q)
[PROOF STEP]
have "pmf ?l e = \<beta> * pmf p e - \<beta> * pmf q e + pmf q e"
[PROOF STATE]
proof (prove)
using this:
e \<in> set_pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q)

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e - \<beta> * pmf q e + pmf q e
[PROOF STEP]
using pmf_mix_deeper[of "\<beta>/\<alpha>" p q e] mix_pmf_comp_left_div[of \<alpha> \<beta> p q e] assms
[PROOF STATE]
proof (prove)
using this:
e \<in> set_pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q)
\<beta> / \<alpha> \<in> {0..1} \<Longrightarrow> pmf (mix_pmf (\<beta> / \<alpha>) p q) e = \<beta> / \<alpha> * pmf p e + pmf q e - \<beta> / \<alpha> * pmf q e
\<lbrakk>\<alpha> \<in> {0..1}; \<beta> \<in> {0..1}; \<beta> < \<alpha>\<rbrakk> \<Longrightarrow> pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e + pmf q e - \<beta> * pmf q e
\<alpha> \<in> {0..1}
\<beta> \<in> {0..1}
\<beta> < \<alpha>

goal (1 subgoal):
 1. pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e - \<beta> * pmf q e + pmf q e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e - \<beta> * pmf q e + pmf q e

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf (mix_pmf \<beta> p q) \<Longrightarrow> pmf (mix_pmf \<beta> p q) e = pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e - \<beta> * pmf q e + pmf q e
[PROOF STEP]
show "pmf (mix_pmf \<beta> p q) e = pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e"
[PROOF STATE]
proof (prove)
using this:
pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e = \<beta> * pmf p e - \<beta> * pmf q e + pmf q e

goal (1 subgoal):
 1. pmf (mix_pmf \<beta> p q) e = pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e
[PROOF STEP]
by (metis (full_types) assms(1) assms(2) assms(3) mix_pmf_comp_left_div pmf_mix_deeper)
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf \<beta> p q) e = pmf (mix_pmf (\<beta> / \<alpha>) (mix_pmf \<alpha> p q) q) e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_mix_pmf_prob_distrib:
  assumes "a \<in> {0..1}"
    and "b \<in> {0..1}"
  shows "mix_pmf a (mix_pmf b p q) q = mix_pmf (a*b) p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
define \<gamma> where g: "\<gamma> = (a * b)"
[PROOF STATE]
proof (state)
this:
\<gamma> = a * b

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
define l where l: "l = (mix_pmf b p q)"
[PROOF STATE]
proof (state)
this:
l = mix_pmf b p q

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
define r where r: "r =  mix_pmf (a*b) p q"
[PROOF STATE]
proof (state)
this:
r = mix_pmf (a * b) p q

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
have y: "\<gamma> \<in> {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> \<in> {0..1}
[PROOF STEP]
using assms(2) mult_le_one assms g
[PROOF STATE]
proof (prove)
using this:
b \<in> {0..1}
\<lbrakk>?a \<le> (1::?'a); (0::?'a) \<le> ?b; ?b \<le> (1::?'a)\<rbrakk> \<Longrightarrow> ?a * ?b \<le> (1::?'a)
a \<in> {0..1}
b \<in> {0..1}
\<gamma> = a * b

goal (1 subgoal):
 1. \<gamma> \<in> {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<gamma> \<in> {0..1}

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
have alt_: "\<forall>e \<in> set_pmf l. pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>set_pmf l. pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
have "pmf r e = \<gamma> * pmf p e + (1-\<gamma>) * pmf q e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf r e = \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e
[PROOF STEP]
using \<open>\<gamma> \<in> {0..1}\<close> g pmf_mix r
[PROOF STATE]
proof (prove)
using this:
\<gamma> \<in> {0..1}
\<gamma> = a * b
?a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf ?a ?p ?q) ?x = ?a * pmf ?p ?x + (1 - ?a) * pmf ?q ?x
r = mix_pmf (a * b) p q

goal (1 subgoal):
 1. pmf r e = \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
pmf r e = \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pmf r e = \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
have "... = \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e = \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
\<gamma> * pmf p e + (1 - \<gamma>) * pmf q e = \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<gamma> * pmf p e + (1 - \<gamma>) * pmf q e = \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
have "... = pmf (mix_pmf \<gamma> p q) e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e = pmf (mix_pmf \<gamma> p q) e
[PROOF STEP]
using calculation g r
[PROOF STATE]
proof (prove)
using this:
pmf r e = \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e
\<gamma> * pmf p e + (1 - \<gamma>) * pmf q e = \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e
\<gamma> = a * b
r = mix_pmf (a * b) p q

goal (1 subgoal):
 1. \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e = pmf (mix_pmf \<gamma> p q) e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e = pmf (mix_pmf \<gamma> p q) e

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e = pmf (mix_pmf \<gamma> p q) e

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
have "... = \<gamma>  * pmf p e + pmf q e - \<gamma> * pmf q e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (mix_pmf \<gamma> p q) e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
using calculation
[PROOF STATE]
proof (prove)
using this:
pmf r e = \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e
\<gamma> * pmf p e + (1 - \<gamma>) * pmf q e = \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e
\<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e = pmf (mix_pmf \<gamma> p q) e

goal (1 subgoal):
 1. pmf (mix_pmf \<gamma> p q) e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (mix_pmf \<gamma> p q) e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e

goal (1 subgoal):
 1. \<And>e. e \<in> set_pmf l \<Longrightarrow> pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pmf r e = \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e
\<gamma> * pmf p e + (1 - \<gamma>) * pmf q e = \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e
\<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e = pmf (mix_pmf \<gamma> p q) e
pmf (mix_pmf \<gamma> p q) e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
show "pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e"
[PROOF STATE]
proof (prove)
using this:
pmf r e = \<gamma> * pmf p e + (1 - \<gamma>) * pmf q e
\<gamma> * pmf p e + (1 - \<gamma>) * pmf q e = \<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e
\<gamma> * pmf p e + 1 * pmf q e - \<gamma> * pmf q e = pmf (mix_pmf \<gamma> p q) e
pmf (mix_pmf \<gamma> p q) e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e

goal (1 subgoal):
 1. pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>set_pmf l. pmf r e = \<gamma> * pmf p e + pmf q e - \<gamma> * pmf q e

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
have "\<forall>e \<in> set_pmf r. pmf l e = b * pmf p e + pmf q e - b * pmf q e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>set_pmf r. pmf l e = b * pmf p e + pmf q e - b * pmf q e
[PROOF STEP]
using allI pmf_mix_deeper assms(2) l
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x
?a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf ?a ?p ?q) ?x = ?a * pmf ?p ?x + pmf ?q ?x - ?a * pmf ?q ?x
b \<in> {0..1}
l = mix_pmf b p q

goal (1 subgoal):
 1. \<forall>e\<in>set_pmf r. pmf l e = b * pmf p e + pmf q e - b * pmf q e
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>set_pmf r. pmf l e = b * pmf p e + pmf q e - b * pmf q e

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
have "mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q \<noteq> mix_pmf (a * b) p q \<Longrightarrow> False
[PROOF STEP]
assume neg:"\<not>mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q"
[PROOF STATE]
proof (state)
this:
mix_pmf a (mix_pmf b p q) q \<noteq> mix_pmf (a * b) p q

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q \<noteq> mix_pmf (a * b) p q \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mix_pmf a (mix_pmf b p q) q \<noteq> mix_pmf (a * b) p q
[PROOF STEP]
have b: "b \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
mix_pmf a (mix_pmf b p q) q \<noteq> mix_pmf (a * b) p q

goal (1 subgoal):
 1. b \<noteq> 0
[PROOF STEP]
by (metis (no_types) assms(1) mult_cancel_right2 pmf_mix_0 set_pmf_mix_eq)
[PROOF STATE]
proof (state)
this:
b \<noteq> 0

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q \<noteq> mix_pmf (a * b) p q \<Longrightarrow> False
[PROOF STEP]
have f3: "b - (a * b) > 0 \<longrightarrow> mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < b - a * b \<longrightarrow> mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
by (metis assms(2) diff_le_0_iff_le g mix_pmf_comp_with_dif_equiv mult_eq_0_iff
          nonzero_mult_div_cancel_right not_le order_refl y)
[PROOF STATE]
proof (state)
this:
0 < b - a * b \<longrightarrow> mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q \<noteq> mix_pmf (a * b) p q \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
0 < b - a * b \<longrightarrow> mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q

goal (1 subgoal):
 1. False
[PROOF STEP]
using b neg assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
0 < b - a * b \<longrightarrow> mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
b \<noteq> 0
mix_pmf a (mix_pmf b p q) q \<noteq> mix_pmf (a * b) p q
a \<in> {0..1}
b \<in> {0..1}

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q

goal (1 subgoal):
 1. mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mix_pmf a (mix_pmf b p q) q = mix_pmf (a * b) p q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mix_pmf_subset_of_original:
  assumes "a \<in> {0..1}"
  shows "(set_pmf (mix_pmf a p q)) \<subseteq> set_pmf p \<union> set_pmf q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
have "a \<in> {0<..<1} \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
by (simp add: set_pmf_mix)
[PROOF STATE]
proof (state)
this:
a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q

goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q

goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
have "a = 1 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = 1 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = 1 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q

goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a = 1 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q

goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
have "a = 0 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = 0 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = 0 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q

goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
a = 1 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
a = 0 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
a = 1 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
a = 0 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q

goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
using assms less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
a = 1 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
a = 0 \<Longrightarrow> set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
a \<in> {0..1}
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_pmf (mix_pmf a p q) \<subseteq> set_pmf p \<union> set_pmf q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mix_pmf_preserves_finite_support:
  assumes "a \<in> {0..1}"
  assumes "finite (set_pmf p)"
    and "finite (set_pmf q)"
  shows "finite (set_pmf (mix_pmf a p q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf (mix_pmf a p q))
[PROOF STEP]
by (meson assms(1) assms(2) assms(3) finite_Un finite_subset mix_pmf_subset_of_original)


[STATEMENT]
lemma ex_certain_iff_singleton_support:
  shows "(\<exists>x. pmf p x = 1) \<longleftrightarrow> card (set_pmf p) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. pmf p x = 1) = (card (set_pmf p) = 1)
[PROOF STEP]
proof (rule iffI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x. pmf p x = 1 \<Longrightarrow> card (set_pmf p) = 1
 2. card (set_pmf p) = 1 \<Longrightarrow> \<exists>x. pmf p x = 1
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<exists>x. pmf p x = 1

goal (2 subgoals):
 1. \<exists>x. pmf p x = 1 \<Longrightarrow> card (set_pmf p) = 1
 2. card (set_pmf p) = 1 \<Longrightarrow> \<exists>x. pmf p x = 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set_pmf p) = 1
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
assume neg: "\<not> card (set_pmf p) = 1"
[PROOF STATE]
proof (state)
this:
card (set_pmf p) \<noteq> 1

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (set_pmf p) \<noteq> 1
[PROOF STEP]
have "card (set_pmf p) \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
card (set_pmf p) \<noteq> 1

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (set_pmf p) \<noteq> 1

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
have "finite (set_pmf p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf p)
[PROOF STEP]
by (metis "1" empty_iff finite.emptyI finite_insert insert_iff
          not_le pmf_le_1 pmf_neq_exists_less pmf_nonneg set_pmf_iff set_return_pmf)
[PROOF STATE]
proof (state)
this:
finite (set_pmf p)

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (set_pmf p)
[PROOF STEP]
have sumeq_1: "(\<Sum>i \<in> set_pmf p. pmf p i) = 1"
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf p)

goal (1 subgoal):
 1. sum (pmf p) (set_pmf p) = 1
[PROOF STEP]
using sum_pmf_eq_1[of "set_pmf p" p]
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf p)
\<lbrakk>finite (set_pmf p); set_pmf p \<subseteq> set_pmf p\<rbrakk> \<Longrightarrow> sum (pmf p) (set_pmf p) = 1

goal (1 subgoal):
 1. sum (pmf p) (set_pmf p) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (pmf p) (set_pmf p) = 1

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
have set_pmf_nemtpy: "set_pmf p \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf p \<noteq> {}
[PROOF STEP]
by (simp add: set_pmf_not_empty)
[PROOF STATE]
proof (state)
this:
set_pmf p \<noteq> {}

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set_pmf p \<noteq> {}
[PROOF STEP]
have g1: "card (set_pmf p) > 1"
[PROOF STATE]
proof (prove)
using this:
set_pmf p \<noteq> {}

goal (1 subgoal):
 1. 1 < card (set_pmf p)
[PROOF STEP]
by (metis card_0_eq less_one nat_neq_iff neg sum.infinite sumeq_1 zero_neq_one)
[PROOF STATE]
proof (state)
this:
1 < card (set_pmf p)

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
have "card (set_pmf p) > 1 \<longrightarrow> (\<Sum>i \<in> set_pmf p. pmf p i) > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < card (set_pmf p) \<longrightarrow> 1 < sum (pmf p) (set_pmf p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < card (set_pmf p) \<Longrightarrow> 1 < sum (pmf p) (set_pmf p)
[PROOF STEP]
assume "card (set_pmf p) > 1"
[PROOF STATE]
proof (state)
this:
1 < card (set_pmf p)

goal (1 subgoal):
 1. 1 < card (set_pmf p) \<Longrightarrow> 1 < sum (pmf p) (set_pmf p)
[PROOF STEP]
have "\<exists>x y. pmf p x = 1 \<and> y \<noteq> x \<and> y \<in> set_pmf p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x y. pmf p x = 1 \<and> y \<noteq> x \<and> y \<in> set_pmf p
[PROOF STEP]
using  set_pmf_nemtpy is_singletonI' is_singleton_altdef
[PROOF STATE]
proof (prove)
using this:
set_pmf p \<noteq> {}
\<lbrakk>?A \<noteq> {}; \<And>x y. \<lbrakk>x \<in> ?A; y \<in> ?A\<rbrakk> \<Longrightarrow> x = y\<rbrakk> \<Longrightarrow> is_singleton ?A
is_singleton ?A = (card ?A = 1)

goal (1 subgoal):
 1. \<exists>x y. pmf p x = 1 \<and> y \<noteq> x \<and> y \<in> set_pmf p
[PROOF STEP]
by (metis "1" neg)
[PROOF STATE]
proof (state)
this:
\<exists>x y. pmf p x = 1 \<and> y \<noteq> x \<and> y \<in> set_pmf p

goal (1 subgoal):
 1. 1 < card (set_pmf p) \<Longrightarrow> 1 < sum (pmf p) (set_pmf p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x y. pmf p x = 1 \<and> y \<noteq> x \<and> y \<in> set_pmf p
[PROOF STEP]
show "(\<Sum>i \<in> set_pmf p. pmf p i) > 1"
[PROOF STATE]
proof (prove)
using this:
\<exists>x y. pmf p x = 1 \<and> y \<noteq> x \<and> y \<in> set_pmf p

goal (1 subgoal):
 1. 1 < sum (pmf p) (set_pmf p)
[PROOF STEP]
by (metis AE_measure_pmf_iff UNIV_I empty_iff insert_iff
            measure_pmf.prob_eq_1 pmf.rep_eq sets_measure_pmf)
[PROOF STATE]
proof (state)
this:
1 < sum (pmf p) (set_pmf p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 < card (set_pmf p) \<longrightarrow> 1 < sum (pmf p) (set_pmf p)

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < card (set_pmf p) \<longrightarrow> 1 < sum (pmf p) (set_pmf p)
[PROOF STEP]
have "card (set_pmf p) < 1"
[PROOF STATE]
proof (prove)
using this:
1 < card (set_pmf p) \<longrightarrow> 1 < sum (pmf p) (set_pmf p)

goal (1 subgoal):
 1. card (set_pmf p) < 1
[PROOF STEP]
using sumeq_1 neg
[PROOF STATE]
proof (prove)
using this:
1 < card (set_pmf p) \<longrightarrow> 1 < sum (pmf p) (set_pmf p)
sum (pmf p) (set_pmf p) = 1
card (set_pmf p) \<noteq> 1

goal (1 subgoal):
 1. card (set_pmf p) < 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
card (set_pmf p) < 1

goal (1 subgoal):
 1. card (set_pmf p) \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (set_pmf p) < 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
card (set_pmf p) < 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using g1
[PROOF STATE]
proof (prove)
using this:
card (set_pmf p) < 1
1 < card (set_pmf p)

goal (1 subgoal):
 1. False
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (set_pmf p) = 1

goal (1 subgoal):
 1. card (set_pmf p) = 1 \<Longrightarrow> \<exists>x. pmf p x = 1
[PROOF STEP]
qed (metis card_1_singletonE less_numeral_extra(1) pmf.rep_eq subset_eq
    sum_pmf_eq_1[of "set_pmf p" p]  card_gt_0_iff[of "set_pmf p"]
    measure_measure_pmf_finite[of "set_pmf p"])