[STATEMENT]
lemma trss_stack_comp_s:
  "((s,c),e,(s',c'))\<in>trss fg \<Longrightarrow> ((s@r,c),e,(s'@r,c'))\<in>trss fg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((s, c), e, s', c') \<in> trss fg \<Longrightarrow> ((s @ r, c), e, s' @ r, c') \<in> trss fg
[PROOF STEP]
by (auto elim!: trss.cases intro: trss.intros)


[STATEMENT]
lemma primerec_getpren[elim]: "\<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < n; n \<le> m\<rbrakk> \<Longrightarrow> primerec (get_fstn_args m n ! i) m
[PROOF STEP]
apply(induct n, auto simp: get_fstn_args.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>i < n \<Longrightarrow> primerec (get_fstn_args m n ! i) m; i < Suc n; Suc n \<le> m\<rbrakk> \<Longrightarrow> primerec ((get_fstn_args m n @ [recf.id m n]) ! i) m
[PROOF STEP]
apply(cases "i = n", auto simp: nth_append intro: prime_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Minr_lemma: "
  \<lbrakk>primerec rf (Suc (length xs))\<rbrakk>
     \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) =
            Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
let ?rt = "(recf.id (Suc (length xs)) ((length xs)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
let ?rf = "(Cn (Suc (Suc (length xs)))
    rec_not [Cn (Suc (Suc (length xs))) rf
    (get_fstn_args (Suc (Suc (length xs))) (length xs) @
                [recf.id (Suc (Suc (length xs)))
    (Suc ((length xs)))])])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
let ?rq = "(rec_all ?rt ?rf)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
assume h: "primerec rf (Suc (length xs))"
[PROOF STATE]
proof (state)
this:
primerec rf (Suc (length xs))

goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
have h1: "primerec ?rq (Suc (length xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))
[PROOF STEP]
apply(rule_tac primerec_all_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. primerec (recf.id (Suc (length xs)) (length xs)) (Suc (length xs))
 2. primerec (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])]) (Suc (Suc (length xs)))
 3. 0 < Suc (length xs)
[PROOF STEP]
apply(auto simp: h nth_append)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))

goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))

goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
have "arity rf = Suc (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arity rf = Suc (length xs)
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
primerec rf (Suc (length xs))

goal (1 subgoal):
 1. arity rf = Suc (length xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arity rf = Suc (length xs)

goal (1 subgoal):
 1. primerec rf (Suc (length xs)) \<Longrightarrow> rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))
arity rf = Suc (length xs)
[PROOF STEP]
show "rec_exec (rec_Minr rf) (xs @ [w]) =
    Minr (\<lambda> args. (0 < rec_exec rf args)) xs w"
[PROOF STATE]
proof (prove)
using this:
primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs))
arity rf = Suc (length xs)

goal (1 subgoal):
 1. rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
apply(simp add: arity.simps Let_def sigma_lemma all_lemma)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs)); arity rf = Suc (length xs)\<rbrakk> \<Longrightarrow> UF.Sigma (rec_exec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])]))) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w
[PROOF STEP]
apply(rule_tac  sigma_minr_lemma)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>primerec (rec_all (recf.id (Suc (length xs)) (length xs)) (Cn (Suc (Suc (length xs))) rec_not [Cn (Suc (Suc (length xs))) rf (get_fstn_args (Suc (Suc (length xs))) (length xs) @ [recf.id (Suc (Suc (length xs))) (Suc (length xs))])])) (Suc (length xs)); arity rf = Suc (length xs)\<rbrakk> \<Longrightarrow> primerec rf (Suc (length xs))
[PROOF STEP]
apply(simp add: h)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rec_exec (rec_Minr rf) (xs @ [w]) = Minr (\<lambda>args. 0 < rec_exec rf args) xs w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_ext_none [simp]:
  "cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (document_ptr.Ext (Inr (Inr document_ext_ptr))) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast (document_ptr.Ext (Inr (Inr document_ext_ptr))) = None
[PROOF STEP]
by(simp add: cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)


[STATEMENT]
lemma sum_list_map_cons:
  "sum_list (map weight (y # ys)) = weight y + sum_list (map weight ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map weight (y # ys)) = weight y + sum_list (map weight ys)
[PROOF STEP]
by auto


[STATEMENT]
theorem (in group) unit_group_unique:
  assumes "card (carrier G) = 1"
  shows "\<exists> h. h \<in> iso G unit_group"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
card (carrier G) = 1
[PROOF STEP]
obtain x where "carrier G = {x}"
[PROOF STATE]
proof (prove)
using this:
card (carrier G) = 1

goal (1 subgoal):
 1. (\<And>x. carrier G = {x} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: card_eq_SucD)
[PROOF STATE]
proof (state)
this:
carrier G = {x}

goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
hence "(\<lambda> x. ()) \<in> iso G unit_group"
[PROOF STATE]
proof (prove)
using this:
carrier G = {x}

goal (1 subgoal):
 1. (\<lambda>x. ()) \<in> Group.iso G unit_group
[PROOF STEP]
by -(rule group_isoI, auto simp add:unit_group_is_group is_group, simp add:unit_group_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. ()) \<in> Group.iso G unit_group

goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. ()) \<in> Group.iso G unit_group

goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>h. h \<in> Group.iso G unit_group

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minGraphProps7': "minGraphProps g \<Longrightarrow>
  f \<in> \<F> g \<Longrightarrow> v \<in> \<V> f \<Longrightarrow>  f \<in> set (faceListAt g ! v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f\<rbrakk> \<Longrightarrow> f \<in> set (faceListAt g ! v)
[PROOF STEP]
apply (frule minGraphProps7)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f\<rbrakk> \<Longrightarrow> ?f \<in> \<F> g
 2. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f\<rbrakk> \<Longrightarrow> ?v \<in> \<V> ?f
 3. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f; ?f \<in> set (facesAt g ?v)\<rbrakk> \<Longrightarrow> f \<in> set (faceListAt g ! v)
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f; f \<in> set (facesAt g v)\<rbrakk> \<Longrightarrow> f \<in> set (faceListAt g ! v)
[PROOF STEP]
by (simp add: facesAt_def split: if_split_asm)


[STATEMENT]
lemma replacefacesAt2_5: "x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F!k) \<or> x \<in> set newfs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
proof (induct ns arbitrary: F)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>F. x \<in> set (replacefacesAt2 [] oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
 2. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
x \<in> set (replacefacesAt2 [] oldf newfs F ! k)

goal (2 subgoals):
 1. \<And>F. x \<in> set (replacefacesAt2 [] oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
 2. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (replacefacesAt2 [] oldf newfs F ! k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> set (replacefacesAt2 [] oldf newfs F ! k)

goal (1 subgoal):
 1. x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> set (F ! k) \<or> x \<in> set newfs

goal (1 subgoal):
 1. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
case (Cons n ns)
[PROOF STATE]
proof (state)
this:
x \<in> set (replacefacesAt2 ns oldf newfs ?F ! k) \<Longrightarrow> x \<in> set (?F ! k) \<or> x \<in> set newfs
x \<in> set (replacefacesAt2 (n # ns) oldf newfs F ! k)

goal (1 subgoal):
 1. \<And>a ns F. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; x \<in> set (replacefacesAt2 (a # ns) oldf newfs F ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (replacefacesAt2 ns oldf newfs ?F ! k) \<Longrightarrow> x \<in> set (?F ! k) \<or> x \<in> set newfs
x \<in> set (replacefacesAt2 (n # ns) oldf newfs F ! k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> set (replacefacesAt2 ns oldf newfs ?F ! k) \<Longrightarrow> x \<in> set (?F ! k) \<or> x \<in> set newfs
x \<in> set (replacefacesAt2 (n # ns) oldf newfs F ! k)

goal (1 subgoal):
 1. x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply(simp add: split: if_split_asm )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k)\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply (frule Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs; n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply (thin_tac "\<And>F. x \<in> set (replacefacesAt2 ns oldf newfs F ! k) \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply (case_tac "x \<in> set newfs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs; x \<in> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
 2. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs; x \<notin> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k) \<or> x \<in> set newfs; x \<notin> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k) \<or> x \<in> set newfs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
apply (case_tac "k = n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k = n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
 2. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k \<noteq> n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! n); x \<in> set (replace oldf newfs (F ! n)); x \<notin> set newfs; k = n\<rbrakk> \<Longrightarrow> x \<in> set (F ! n)
 2. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k \<noteq> n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
apply (frule replace5)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! n); x \<in> set (replace oldf newfs (F ! n)); x \<notin> set newfs; k = n; x \<in> set (F ! n) \<or> x \<in> set newfs\<rbrakk> \<Longrightarrow> x \<in> set (F ! n)
 2. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k \<noteq> n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < |F|; x \<in> set (replacefacesAt2 ns oldf newfs (F[n := replace oldf newfs (F ! n)]) ! k); x \<in> set (F[n := replace oldf newfs (F ! n)] ! k); x \<notin> set newfs; k \<noteq> n\<rbrakk> \<Longrightarrow> x \<in> set (F ! k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> set (F ! k) \<or> x \<in> set newfs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma NMPDA[rule_format]: "DenyAll \<in> set p \<longrightarrow> not_MT C  p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DenyAll \<in> set p \<longrightarrow> not_MT C p
[PROOF STEP]
by (induct p, simp_all add: DAnMT)


[STATEMENT]
lemma tconcat_TCons [simp]: "tconcat b (TCons a tr) = lappendt a (tconcat b tr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tconcat b (TCons a tr) = lappendt a (tconcat b tr)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma cross_ratio_not_zero:
  assumes "z \<noteq> u" and "v \<noteq> w"
  shows "cross_ratio z u v w \<noteq> 0\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio z u v w \<noteq> 0\<^sub>h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> u
v \<noteq> w

goal (1 subgoal):
 1. cross_ratio z u v w \<noteq> 0\<^sub>h
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
fix z u v w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
assume nz: "z \<noteq> vec_zero" "u \<noteq> vec_zero" "v \<noteq> vec_zero" "w \<noteq> vec_zero"
[PROOF STATE]
proof (state)
this:
z \<noteq> vec_zero
u \<noteq> vec_zero
v \<noteq> vec_zero
w \<noteq> vec_zero

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
obtain z1 z2 u1 u2 v1 v2 w1 w2 where *: "z = (z1, z2)" "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z1 z2 u1 u2 v1 v2 w1 w2. \<lbrakk>z = (z1, z2); u = (u1, u2); v = (v1, v2); w = (w1, w2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z, cases u, cases v, cases w, auto)
[PROOF STATE]
proof (state)
this:
z = (z1, z2)
u = (u1, u2)
v = (v1, v2)
w = (w1, w2)

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
obtain x1 x2 where **: "cross_ratio_cvec z u v w = (x1, x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2. cross_ratio_cvec z u v w = (x1, x2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "cross_ratio_cvec z u v w", auto)
[PROOF STATE]
proof (state)
this:
cross_ratio_cvec z u v w = (x1, x2)

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
assume "\<not> z \<approx>\<^sub>v u" "\<not> v \<approx>\<^sub>v w"
[PROOF STATE]
proof (state)
this:
\<not> z \<approx>\<^sub>v u
\<not> v \<approx>\<^sub>v w

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
hence "z1*u2 \<noteq> z2*u1" "v1*w2 \<noteq> v2*w1"
[PROOF STATE]
proof (prove)
using this:
\<not> z \<approx>\<^sub>v u
\<not> v \<approx>\<^sub>v w

goal (1 subgoal):
 1. z1 * u2 \<noteq> z2 * u1 &&& v1 * w2 \<noteq> v2 * w1
[PROOF STEP]
using * nz complex_cvec_eq_mix
[PROOF STATE]
proof (prove)
using this:
\<not> z \<approx>\<^sub>v u
\<not> v \<approx>\<^sub>v w
z = (z1, z2)
u = (u1, u2)
v = (v1, v2)
w = (w1, w2)
z \<noteq> vec_zero
u \<noteq> vec_zero
v \<noteq> vec_zero
w \<noteq> vec_zero
\<lbrakk>(?z1.0, ?z2.0) \<noteq> vec_zero; (?w1.0, ?w2.0) \<noteq> vec_zero\<rbrakk> \<Longrightarrow> ((?z1.0, ?z2.0) \<approx>\<^sub>v (?w1.0, ?w2.0)) = (?z1.0 * ?w2.0 = ?z2.0 * ?w1.0)

goal (1 subgoal):
 1. z1 * u2 \<noteq> z2 * u1 &&& v1 * w2 \<noteq> v2 * w1
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
z1 * u2 \<noteq> z2 * u1
v1 * w2 \<noteq> v2 * w1

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
hence "x1 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
z1 * u2 \<noteq> z2 * u1
v1 * w2 \<noteq> v2 * w1

goal (1 subgoal):
 1. x1 \<noteq> 0
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
z1 * u2 \<noteq> z2 * u1
v1 * w2 \<noteq> v2 * w1
z = (z1, z2)
u = (u1, u2)
v = (v1, v2)
w = (w1, w2)
cross_ratio_cvec z u v w = (x1, x2)

goal (1 subgoal):
 1. x1 \<noteq> 0
[PROOF STEP]
by (auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
x1 \<noteq> 0

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
thus "\<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> 0

goal (1 subgoal):
 1. \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
using zero_cvec_z1_zero_iff * **
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> 0
(?z1.0, ?z2.0) \<noteq> vec_zero \<Longrightarrow> ((?z1.0, ?z2.0) \<approx>\<^sub>v 0\<^sub>v) = (?z1.0 = 0)
z = (z1, z2)
u = (u1, u2)
v = (v1, v2)
w = (w1, w2)
cross_ratio_cvec z u v w = (x1, x2)

goal (1 subgoal):
 1. \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree_le_max_perm_degree: "degree (det A) \<le> max_perm_degree A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Square_Matrix.det A) \<le> max_perm_degree A
[PROOF STEP]
unfolding det_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. to_fun A i (p i))) \<le> max_perm_degree A
[PROOF STEP]
by (rule order_trans[OF degree_sum_le_Max])
     (auto intro!: degree_prod_le_max_perm_degree Max_le_iff[THEN iffD2] permutes_id simp: sign_permut)


[STATEMENT]
lemma KS_SK_id:
  "KS\<cdot>(SK\<cdot>xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. KS\<cdot>(SK\<cdot>xs) = xs
[PROOF STEP]
by (induct xs) (simp_all add: KS_def failK_def)


[STATEMENT]
lemma row_zero[simp]:
  "i < nr \<Longrightarrow> row (0\<^sub>m nr nc) i = 0\<^sub>v nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < nr \<Longrightarrow> row (0\<^sub>m nr nc) i = 0\<^sub>v nc
[PROOF STEP]
by (intro eq_vecI, auto)


[STATEMENT]
lemma carrier_vec_induct [consumes 1, case_names 0 Suc, induct set:carrier_vec]:
  assumes v: "v \<in> carrier_vec n"
    and 1: "P 0 vNil" and 2: "\<And>n a v. v \<in> carrier_vec n \<Longrightarrow> P n v \<Longrightarrow> P (Suc n) (vCons a v)"
  shows "P n v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P n v
[PROOF STEP]
proof (insert v, induct n arbitrary: v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. v \<in> carrier_vec 0 \<Longrightarrow> P 0 v
 2. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec 0

goal (2 subgoals):
 1. \<And>v. v \<in> carrier_vec 0 \<Longrightarrow> P 0 v
 2. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec 0
[PROOF STEP]
have "v = vec 0 ((!) [])"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec 0

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

goal (2 subgoals):
 1. \<And>v. v \<in> carrier_vec 0 \<Longrightarrow> P 0 v
 2. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
P 0 vNil
v = vNil
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P 0 vNil
v = vNil

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

goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
?v \<in> carrier_vec n \<Longrightarrow> P n ?v
v \<in> carrier_vec (Suc n)

goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. v \<in> carrier_vec n \<Longrightarrow> P n v; v \<in> carrier_vec (Suc n)\<rbrakk> \<Longrightarrow> P (Suc n) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?v \<in> carrier_vec n \<Longrightarrow> P n ?v
v \<in> carrier_vec (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?v \<in> carrier_vec n \<Longrightarrow> P n ?v
v \<in> carrier_vec (Suc n)

goal (1 subgoal):
 1. P (Suc n) v
[PROOF STEP]
by (cases v, auto dest!: carrier_vecD intro:2)
[PROOF STATE]
proof (state)
this:
P (Suc n) v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma m3_inv1_lkeysec_for_analz [simp]:
  "\<lbrakk> s \<in> m3_inv1_lkeysec \<rbrakk> \<Longrightarrow> Key (shrK C) \<in> analz (IK s) \<longleftrightarrow> C \<in> bad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> m3_inv1_lkeysec \<Longrightarrow> (Key (shrK C) \<in> analz (IK s)) = (C \<in> bad)
[PROOF STEP]
by auto


[STATEMENT]
lemma IF2wit: "x \<in> IF2set IF2wit \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> IF2set IF2wit \<Longrightarrow> False
[PROOF STEP]
unfolding IF2wit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> IF2set (ctor2 wit_F2) \<Longrightarrow> False
[PROOF STEP]
by (elim UnE F2.wit[elim_format] UN_E FalseE |
      rule refl |  hypsubst | assumption | unfold IF2set_simps)+


[STATEMENT]
lemma refl_joinable_iff: "(\<forall>x. \<exists>y. (x, y) \<in> R) = refl (joinable R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. \<exists>y. (x, y) \<in> R) = refl (joinable R)
[PROOF STEP]
by (auto intro!: refl_onI dest: refl_onD simp add: joinable_simp)


[STATEMENT]
lemma lemma_3_5_ii_1 [simp]: "d1 a a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d1 a a = (1::'a)
[PROOF STEP]
apply (subst lemma_3_5_i_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = a
[PROOF STEP]
by simp


[STATEMENT]
lemma cong_sym: "R \<in> congruences \<Longrightarrow> R a b \<Longrightarrow> R b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R \<in> congruences; R a b\<rbrakk> \<Longrightarrow> R b a
[PROOF STEP]
by (simp add: congruences_def equivp_symp)


[STATEMENT]
lemma numer_cf5_pos: "-7.293 \<le> x \<Longrightarrow> numer_cf5 x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (7293 / 10 ^ 3) \<le> x \<Longrightarrow> 0 < numer_cf5 x
[PROOF STEP]
unfolding numer_cf5_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (7293 / 10 ^ 3) \<le> x \<Longrightarrow> 0 < x ^ 5 + 30 * x ^ 4 + 420 * x ^ 3 + 3360 * x\<^sup>2 + 15120 * x + 30240
[PROOF STEP]
by sturm


[STATEMENT]
lemma Aenc_synth_eq2 [simp]:
     "X \<notin> synth H \<Longrightarrow> (Aenc X K \<in> synth H) = (Aenc X K \<in> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<notin> synth H \<Longrightarrow> (Aenc X K \<in> synth H) = (Aenc X K \<in> H)
[PROOF STEP]
by blast


[STATEMENT]
lemma in_var_pr_var [simp]:
  "in_var (pr_var x) = in_var x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_var (pr_var x) = in_var x
[PROOF STEP]
by (simp add: pr_var_def)


[STATEMENT]
lemma E_inf_r:
  "step.E_inf s (r f) =
    lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
have "step.E_inf s (r f) =
    lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
unfolding rF_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step.E_inf s (lfp (\<lambda>F \<omega>. if fst (shd \<omega>) = Skip then f (snd (shd \<omega>)) else F (stl \<omega>))) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
proof (rule step.E_inf_lfp[THEN fun_cong])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<lambda>(b, a). if fst b = Skip then f (snd b) else a) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)
 2. \<And>s. sup_continuous (HOL.If (fst s = Skip) (f (snd s)))
 3. \<And>F cfg. F \<in> borel_measurable step.St \<Longrightarrow> \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
 4. \<And>s. finite (step s)
[PROOF STEP]
let ?F = "\<lambda>t x. (if fst t = Skip then f (snd t) else x)"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<lambda>(b, a). if fst b = Skip then f (snd b) else a) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)
 2. \<And>s. sup_continuous (HOL.If (fst s = Skip) (f (snd s)))
 3. \<And>F cfg. F \<in> borel_measurable step.St \<Longrightarrow> \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
 4. \<And>s. finite (step s)
[PROOF STEP]
show "(\<lambda>(s, x). ?F s x) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(s, x). if fst s = Skip then f (snd s) else x) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)
[PROOF STEP]
apply (simp add: measurable_split_conv split_beta')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if fst (fst x) = Skip then f (snd (fst x)) else snd x) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)
[PROOF STEP]
apply (intro borel_measurable_max borel_measurable_const measurable_If predE
         measurable_compose[OF measurable_snd] measurable_compose[OF measurable_fst])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>a. f (snd a)) \<in> borel_measurable (count_space UNIV)
 2. (\<lambda>a. a) \<in> borel_measurable borel
 3. Measurable.pred (count_space UNIV) (\<lambda>a. fst a = Skip)
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>(s, x). if fst s = Skip then f (snd s) else x) \<in> borel_measurable (count_space UNIV \<Otimes>\<^sub>M borel)

goal (3 subgoals):
 1. \<And>s. sup_continuous (HOL.If (fst s = Skip) (f (snd s)))
 2. \<And>F cfg. F \<in> borel_measurable step.St \<Longrightarrow> \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
 3. \<And>s. finite (step s)
[PROOF STEP]
show "\<And>s. sup_continuous (?F s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. sup_continuous (HOL.If (fst s = Skip) (f (snd s)))
[PROOF STEP]
by (auto simp: sup_continuous_def SUP_sup_distrib[symmetric] split: prod.split pgcl.split)
[PROOF STATE]
proof (state)
this:
sup_continuous (HOL.If (fst ?s2 = Skip) (f (snd ?s2)))

goal (2 subgoals):
 1. \<And>F cfg. F \<in> borel_measurable step.St \<Longrightarrow> \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
 2. \<And>s. finite (step s)
[PROOF STEP]
show "\<And>F cfg. (\<integral>\<^sup>+\<omega>. ?F (state cfg) (F \<omega>) \<partial>step.T cfg) =
      ?F (state cfg) (nn_integral (step.T cfg) F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>F cfg. \<integral>\<^sup>+ \<omega>. (if fst (state cfg) = Skip then f (snd (state cfg)) else F \<omega>) \<partial>step.T cfg = (if fst (state cfg) = Skip then f (snd (state cfg)) else integral\<^sup>N (step.T cfg) F)
[PROOF STEP]
by (auto simp: split: pgcl.split prod.split)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ \<omega>. (if fst (state ?cfg3) = Skip then f (snd (state ?cfg3)) else ?F3 \<omega>) \<partial>step.T ?cfg3 = (if fst (state ?cfg3) = Skip then f (snd (state ?cfg3)) else integral\<^sup>N (step.T ?cfg3) ?F3)

goal (1 subgoal):
 1. \<And>s. finite (step s)
[PROOF STEP]
qed (rule step_finite)
[PROOF STATE]
proof (state)
this:
step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s

goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s

goal (1 subgoal):
 1. step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
step.E_inf s (r f) = lfp (\<lambda>F s. \<Sqinter>D\<in>step s. \<integral>\<^sup>+ t. (if fst t = Skip then f (snd t) else F t) \<partial>measure_pmf D) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_less_sum_gt_zero: "(w < s) \<Longrightarrow> (0 < s + (-w::real))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w < s \<Longrightarrow> 0 < s + - w
[PROOF STEP]
by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of s])


[STATEMENT]
lemma real_of_preal_trichotomy:
  "\<exists>m. (x::real) = real_of_preal m \<or> x = 0 \<or> x = -(real_of_preal m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa y. x = Abs_Real (Dedekind_Real.realrel `` {(xa, y)}) \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
case (Abs_Real u v)
[PROOF STATE]
proof (state)
this:
x = Abs_Real (Dedekind_Real.realrel `` {(u, v)})

goal (1 subgoal):
 1. \<And>xa y. x = Abs_Real (Dedekind_Real.realrel `` {(xa, y)}) \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
proof (cases u v rule: linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. u < v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 3. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
u < v

goal (3 subgoals):
 1. u < v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 3. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u < v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u < v

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
using less_add_left
[PROOF STATE]
proof (prove)
using this:
u < v
?r < ?s \<Longrightarrow> ?r + (?s - ?r) = ?s

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
apply (simp add: Abs_Real real_of_preal_def real_minus real_zero_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u < v; \<And>r s. r < s \<Longrightarrow> r + (s - r) = s\<rbrakk> \<Longrightarrow> \<exists>m. u + 1 = m + 1 + v \<or> u + 1 = 1 + v \<or> u + (m + 1) = 1 + v
[PROOF STEP]
by (metis preal_add_assoc preal_add_commute)
[PROOF STATE]
proof (state)
this:
\<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m

goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
case equal
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
 2. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u = v

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
using Abs_Real real_zero_iff
[PROOF STATE]
proof (prove)
using this:
u = v
x = Abs_Real (Dedekind_Real.realrel `` {(u, v)})
Abs_Real (Dedekind_Real.realrel `` {(?x, ?x)}) = 0

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m

goal (1 subgoal):
 1. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
case greater
[PROOF STATE]
proof (state)
this:
v < u

goal (1 subgoal):
 1. v < u \<Longrightarrow> \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v < u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v < u

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
using less_add_left
[PROOF STATE]
proof (prove)
using this:
v < u
?r < ?s \<Longrightarrow> ?r + (?s - ?r) = ?s

goal (1 subgoal):
 1. \<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m
[PROOF STEP]
apply (simp add: Abs_Real real_of_preal_def real_minus real_zero_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v < u; \<And>r s. r < s \<Longrightarrow> r + (s - r) = s\<rbrakk> \<Longrightarrow> \<exists>m. u + 1 = m + 1 + v \<or> u + 1 = 1 + v \<or> u + (m + 1) = 1 + v
[PROOF STEP]
by (metis preal_add_assoc preal_add_commute)
[PROOF STATE]
proof (state)
this:
\<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m. x = real_of_preal m \<or> x = 0 \<or> x = - real_of_preal m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ifT_cong:
  assumes "b = c" "c \<Longrightarrow> x = u" "\<not>c \<Longrightarrow> y = v"
  shows "Heap_Monad_Ext.if\<^sub>T \<langle>b\<rangle> x y = Heap_Monad_Ext.if\<^sub>T \<langle>c\<rangle> u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Heap_Monad_Ext.if\<^sub>T \<langle>b\<rangle> x y = Heap_Monad_Ext.if\<^sub>T \<langle>c\<rangle> u v
[PROOF STEP]
unfolding Heap_Monad_Ext.if\<^sub>T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>b\<rangle> \<bind> (\<lambda>b. if b then x else y) = \<langle>c\<rangle> \<bind> (\<lambda>b. if b then u else v)
[PROOF STEP]
unfolding return_bind
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if b then x else y) = (if c then u else v)
[PROOF STEP]
using if_cong[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c \<Longrightarrow> c; \<not> c \<Longrightarrow> \<not> c\<rbrakk> \<Longrightarrow> (if b then x else y) = (if c then u else v)

goal (1 subgoal):
 1. (if b then x else y) = (if c then u else v)
[PROOF STEP]
.


[STATEMENT]
lemma of_comp_add:
  fixes a b :: "'a :: monoid_add"
  shows "of_comp (a + b) = of_comp a + of_comp b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_comp (a + b) = of_comp a + of_comp b
[PROOF STEP]
by simp


[STATEMENT]
lemma smallomega_1_conv_filterlim: "f \<in> \<omega>[F](\<lambda>_. 1) \<longleftrightarrow> filterlim f at_infinity F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<in> \<omega>[F](\<lambda>_. 1::'b)) = filterlim f at_infinity F
[PROOF STEP]
by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)


[STATEMENT]
lemma EVAL'_I:
  "(\<And>I. finite (adom I) \<Longrightarrow> eval Qinf I = {} \<Longrightarrow> eval_on (fv Q) Qfin I = eval Q I) \<Longrightarrow>
   (\<And>I. finite (adom I) \<Longrightarrow> eval Qinf I \<noteq> {} \<Longrightarrow> infinite (eval Q I)) \<Longrightarrow> EVAL' Q Qfin Qinf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>I. \<lbrakk>finite (adom I); eval Qinf I = {}\<rbrakk> \<Longrightarrow> eval_on (fv Q) Qfin I = eval Q I; \<And>I. \<lbrakk>finite (adom I); eval Qinf I \<noteq> {}\<rbrakk> \<Longrightarrow> infinite (eval Q I)\<rbrakk> \<Longrightarrow> EVAL' Q Qfin Qinf
[PROOF STEP]
unfolding EVAL'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>I. \<lbrakk>finite (adom I); eval Qinf I = {}\<rbrakk> \<Longrightarrow> eval_on (fv Q) Qfin I = eval Q I; \<And>I. \<lbrakk>finite (adom I); eval Qinf I \<noteq> {}\<rbrakk> \<Longrightarrow> infinite (eval Q I)\<rbrakk> \<Longrightarrow> \<forall>I. finite (adom I) \<longrightarrow> (if eval Qinf I = {} then eval_on (fv Q) Qfin I = eval Q I else infinite (eval Q I))
[PROOF STEP]
by auto


[STATEMENT]
lemma c_types_agree_top1: "c_types_agree (TopType []) ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_types_agree (TopType []) ts
[PROOF STEP]
using ct_suffix_ts_conv_suffix to_ct_list_def
[PROOF STATE]
proof (prove)
using this:
ct_suffix (to_ct_list ?ts) (to_ct_list ?ts') = suffix ?ts ?ts'
to_ct_list ?ts = map TSome ?ts

goal (1 subgoal):
 1. c_types_agree (TopType []) ts
[PROOF STEP]
by (simp add: ct_suffix_nil)


[STATEMENT]
lemma PO_m3_step3_refines_m2_step3:
  "{R23}
     (m2_step3 Ra A B Na Nb), (m3_step3 Ra A B Na Nb)
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23} m2_step3 Ra A B Na Nb, m3_step3 Ra A B Na Nb {> R23}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)


[STATEMENT]
lemma directly_subsumes: "directly_subsumes drinks2 drinks 1 1 vend_fail vend_nothing"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. directly_subsumes drinks2 drinks 1 1 vend_fail vend_nothing
[PROOF STEP]
apply (rule direct_subsumption[of _ _ _ _ "\<lambda>c2. c2 $ 2 = Some (Num 0)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t c1 c2. \<lbrakk>obtains 1 c1 drinks2 0 <> t; obtains 1 c2 drinks 0 <> t\<rbrakk> \<Longrightarrow> c2 $ 2 = Some (Num 0)
 2. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> subsumes vend_fail c vend_nothing
[PROOF STEP]
apply (simp add: obtains_1_c2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> subsumes vend_fail c vend_nothing
[PROOF STEP]
apply (rule subsumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> Label vend_nothing = Label vend_fail \<and> Arity vend_nothing = Arity vend_fail
 2. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> can_take_transition vend_fail i c
 3. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> evaluate_outputs vend_nothing i c = evaluate_outputs vend_fail i c
 4. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>p1 p2 i. posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_fail) i c = Some p2 \<longrightarrow> posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_nothing) i c = Some p1 \<longrightarrow> (\<forall>P r'. p1 $ r' = None \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))
[PROOF STEP]
apply (simp add: vend_fail_def vend_nothing_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> can_take_transition vend_fail i c
 2. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> evaluate_outputs vend_nothing i c = evaluate_outputs vend_fail i c
 3. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>p1 p2 i. posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_fail) i c = Some p2 \<longrightarrow> posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_nothing) i c = Some p1 \<longrightarrow> (\<forall>P r'. p1 $ r' = None \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))
[PROOF STEP]
apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>i. can_take_transition vend_nothing i c \<longrightarrow> evaluate_outputs vend_nothing i c = evaluate_outputs vend_fail i c
 2. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>p1 p2 i. posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_fail) i c = Some p2 \<longrightarrow> posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_nothing) i c = Some p1 \<longrightarrow> (\<forall>P r'. p1 $ r' = None \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))
[PROOF STEP]
apply (simp add: vend_fail_def vend_nothing_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. c $ 2 = Some (Num 0) \<Longrightarrow> \<forall>p1 p2 i. posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_fail) i c = Some p2 \<longrightarrow> posterior_separate (Arity vend_nothing) (Guards vend_nothing) (Updates vend_nothing) i c = Some p1 \<longrightarrow> (\<forall>P r'. p1 $ r' = None \<or> (P (p2 $ r') \<longrightarrow> P (p1 $ r')))
[PROOF STEP]
by (simp add: posterior_separate_def vend_fail_def vend_nothing_def)


[STATEMENT]
lemma eventually_nonzero_ln_const'_at_top [eventually_nonzero_simps]:
  "b > 0 \<Longrightarrow> eventually_nonzero at_top (\<lambda>x. ln (x * b :: real))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < b \<Longrightarrow> eventually_nonzero at_top (\<lambda>x. ln (x * b))
[PROOF STEP]
using eventually_nonzero_ln_const_at_top[of b]
[PROOF STATE]
proof (prove)
using this:
0 < b \<Longrightarrow> eventually_nonzero at_top (\<lambda>x. ln (b * x))

goal (1 subgoal):
 1. 0 < b \<Longrightarrow> eventually_nonzero at_top (\<lambda>x. ln (x * b))
[PROOF STEP]
by (simp add: mult.commute)


[STATEMENT]
lemma tauCases:
  fixes P  :: pi
  and   \<alpha>  :: freeRes
  and   P' :: pi

  assumes "\<tau>.(P) \<longmapsto>\<alpha> \<prec> P'"
  and     "Prop (\<tau>) P"

  shows "Prop \<alpha> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>.P \<longmapsto> \<alpha> \<prec> P'
Prop (\<tau>) P

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
by(cases rule: tauCases') (auto simp add: pi.inject residual.inject)


[STATEMENT]
lemma iT_Plus_neg_Max: "
  \<lbrakk> finite I; I \<oplus>- k \<noteq> {} \<rbrakk> \<Longrightarrow> Max (I \<oplus>- k) = Max I - k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; I \<oplus>- k \<noteq> {}\<rbrakk> \<Longrightarrow> Max (I \<oplus>- k) = Max I - k
[PROOF STEP]
apply (simp add: iT_Plus_neg_image_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; I \<down>\<ge> k \<noteq> {}\<rbrakk> \<Longrightarrow> (MAX n\<in>I \<down>\<ge> k. n - k) = Max I - k
[PROOF STEP]
apply (simp add: Max_mono2 monoI cut_ge_finite cut_ge_Max_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iMOD_div: "
  \<lbrakk> 0 < k; m mod k = 0 \<rbrakk> \<Longrightarrow>
  [r, mod m] \<oslash> k = [r div k, mod (m div k) ]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; m mod k = 0\<rbrakk> \<Longrightarrow> [ r, mod m ] \<oslash> k = [ r div k, mod m div k ]
[PROOF STEP]
apply (case_tac "m = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < k; m mod k = 0; m = 0\<rbrakk> \<Longrightarrow> [ r, mod m ] \<oslash> k = [ r div k, mod m div k ]
 2. \<lbrakk>0 < k; m mod k = 0; m \<noteq> 0\<rbrakk> \<Longrightarrow> [ r, mod m ] \<oslash> k = [ r div k, mod m div k ]
[PROOF STEP]
apply (simp add: iMOD_0 iIN_0 iT_Div_singleton)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; m mod k = 0; m \<noteq> 0\<rbrakk> \<Longrightarrow> [ r, mod m ] \<oslash> k = [ r div k, mod m div k ]
[PROOF STEP]
apply (clarsimp elim!: dvdE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ka. \<lbrakk>0 < k; 0 < ka; m = k * ka\<rbrakk> \<Longrightarrow> [ r, mod k * ka ] \<oslash> k = [ r div k, mod ka ]
[PROOF STEP]
apply (rename_tac q)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; m = k * q\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (cut_tac r="r div k" and k=k and m=q in iMOD_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r div k, mod q ] \<otimes> k = [ r div k * k, mod q * k ]\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (drule arg_cong[where f="\<lambda>x. x \<oplus> (r mod k)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r div k, mod q ] \<otimes> k \<oplus> r mod k = [ r div k * k, mod q * k ] \<oplus> r mod k\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (drule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r div k * k, mod q * k ] \<oplus> r mod k = [ r div k, mod q ] \<otimes> k \<oplus> r mod k\<rbrakk> \<Longrightarrow> [ r, mod k * q ] \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (simp add: iMOD_add mult.commute[of k])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (cut_tac I="[r div k, mod q] \<otimes> k" and m=k and n="r mod k" in iT_Plus_Div_distrib_mod_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k\<rbrakk> \<Longrightarrow> \<forall>x\<in>[ r div k, mod q ] \<otimes> k. x mod k + r mod k mod k < k
 2. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q x. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; x \<in> [ r div k, mod q ] \<otimes> k\<rbrakk> \<Longrightarrow> x mod k + r mod k mod k < k
 2. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (simp only: iMOD_mult iMOD_iff, elim conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q x. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k * k, mod q * k ] \<oplus> r mod k; x mod (q * k) = r div k * k mod (q * k); r div k * k \<le> x\<rbrakk> \<Longrightarrow> x mod k + r mod k mod k < k
 2. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (drule mod_factor_imp_mod_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q x. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k * k, mod q * k ] \<oplus> r mod k; r div k * k \<le> x; x mod k = 0\<rbrakk> \<Longrightarrow> x mod k + r mod k mod k < k
 2. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k \<oplus> r mod k div k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (simp add: iT_Plus_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>0 < k; 0 < q; [ r, mod q * k ] = [ r div k, mod q ] \<otimes> k \<oplus> r mod k; [ r div k, mod q ] \<otimes> k \<oplus> r mod k \<oslash> k = [ r div k, mod q ] \<otimes> k \<oslash> k\<rbrakk> \<Longrightarrow> [ r div k, mod q ] \<otimes> k \<oslash> k = [ r div k, mod q ]
[PROOF STEP]
apply (simp add: iT_Mult_Div[OF _ mod_self] iT_Mult_1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iT_Div_cut_ge2: "
  0 < k \<Longrightarrow> (I \<oslash> k) \<down>\<ge> (t div k) = I \<down>\<ge> (t - t mod k) \<oslash> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> (I \<oslash> k) \<down>\<ge> (t div k) = I \<down>\<ge> (t - t mod k) \<oslash> k
[PROOF STEP]
by (frule iT_Div_cut_ge[of k I "t div k"], simp add: div_mult_cancel)


[STATEMENT]
lemma i_set_i_set0_mem_conv: "(I \<in> i_set) = (I \<in> i_set0 \<and> I \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<in> i_set) = (I \<in> i_set0 \<and> I \<noteq> {})
[PROOF STEP]
apply (insert i_set_imp_not_empty[of I])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I \<in> i_set \<Longrightarrow> I \<noteq> {}) \<Longrightarrow> (I \<in> i_set) = (I \<in> i_set0 \<and> I \<noteq> {})
[PROOF STEP]
apply (fastforce simp: i_set0_i_set_mem_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_set_cont_min_eq: "i_set_cont = i_set_cont_min"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_set_cont = i_set_cont_min
[PROOF STEP]
apply (rule set_eqI, rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> i_set_cont \<Longrightarrow> x \<in> i_set_cont_min
 2. \<And>x. x \<in> i_set_cont_min \<Longrightarrow> x \<in> i_set_cont
[PROOF STEP]
apply (rename_tac x, rule_tac a=x in i_set_cont.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. x \<in> i_set_cont \<Longrightarrow> x \<in> i_set_cont
 2. \<And>x n. \<lbrakk>x \<in> i_set_cont; x = [n\<dots>]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont_min
 3. \<And>x n. \<lbrakk>x \<in> i_set_cont; x = [\<dots>n]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont_min
 4. \<And>x n d. \<lbrakk>x \<in> i_set_cont; x = [n\<dots>,d]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont_min
 5. \<And>x. x \<in> i_set_cont_min \<Longrightarrow> x \<in> i_set_cont
[PROOF STEP]
apply (fastforce simp: iIN_0_iTILL_conv[symmetric])+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> i_set_cont_min \<Longrightarrow> x \<in> i_set_cont
[PROOF STEP]
apply (rename_tac x, rule_tac a=x in i_set_cont_min.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> i_set_cont_min \<Longrightarrow> x \<in> i_set_cont_min
 2. \<And>x n. \<lbrakk>x \<in> i_set_cont_min; x = [n\<dots>]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont
 3. \<And>x n d. \<lbrakk>x \<in> i_set_cont_min; x = [n\<dots>,d]\<rbrakk> \<Longrightarrow> x \<in> i_set_cont
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cblinfun_blinfun_transfer_tendsto[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) tendsto tendsto"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)
[PROOF STEP]
note cblinfun_blinfun_transfer[transfer_rule]
[PROOF STATE]
proof (state)
this:
blinfun_cblinfun_eq 0 0
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (+) (+)
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (-) (-)
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) uminus uminus
(real_complex_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (*\<^sub>R) (*\<^sub>C)
(eq_onp bounded_clinear ===> blinfun_cblinfun_eq) Blinfun CBlinfun
(blinfun_cblinfun_eq ===> (=)) norm norm
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> (=)) dist dist
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) sgn sgn
(((=) ===> blinfun_cblinfun_eq) ===> (=)) Cauchy Cauchy

goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)
[PROOF STEP]
unfolding tendsto_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<lambda>f l F. \<forall>e>0. \<forall>\<^sub>F x in F. dist (f x) l < e) (\<lambda>f l F. \<forall>e>0. \<forall>\<^sub>F x in F. dist (f x) l < e)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
(((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adj_0[simp]: \<open>0* = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0* = 0
[PROOF STEP]
by (metis add_cancel_right_left adj_plus)


[STATEMENT]
lemma unitaryD2[simp]: "unitary U \<Longrightarrow> U o\<^sub>C\<^sub>L U* = id_cblinfun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary U \<Longrightarrow> U o\<^sub>C\<^sub>L U* = id_cblinfun
[PROOF STEP]
unfolding unitary_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U* o\<^sub>C\<^sub>L U = id_cblinfun \<and> U o\<^sub>C\<^sub>L U* = id_cblinfun \<Longrightarrow> U o\<^sub>C\<^sub>L U* = id_cblinfun
[PROOF STEP]
by simp


[STATEMENT]
lemma cblinfun_extension_apply:
  assumes "cblinfun_extension_exists S f"
    and "v \<in> S"
  shows "(cblinfun_extension S f) *\<^sub>V v = f v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_extension S f *\<^sub>V v = f v
[PROOF STEP]
by (smt assms cblinfun_extension_def cblinfun_extension_exists_def tfl_some)


[STATEMENT]
lemma inter_imp_subset: "A \<inter> B = A \<Longrightarrow> A \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> B = A \<Longrightarrow> A \<subseteq> B
[PROOF STEP]
by blast


[STATEMENT]
lemma make_observable_transitions_mono: "ts |\<subseteq>| (make_observable_transitions base_trans nexts dones ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
proof (induction rule: make_observable_transitions.induct[of "\<lambda> base_trans nexts dones ts . ts |\<subseteq>| (make_observable_transitions base_trans nexts dones ts)"])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
case (1 base_trans nexts dones ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); ?xa = dones |\<union>| nexts; ?xb = ts |\<union>| ?x; ?xc = t_target |`| ?x |-| ?xa; ?xc \<noteq> {||}\<rbrakk> \<Longrightarrow> ?xb |\<subseteq>| make_observable_transitions base_trans ?xc ?xa ?xb

goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
define qtrans where qtrans_def: "qtrans = ffUnion (fimage (\<lambda> q . (let qts = ffilter (\<lambda>t . t_source t |\<in>| q) base_trans;
                                           ios = fimage (\<lambda> t . (t_input t, t_output t)) qts
                                       in fimage (\<lambda>(x,y) . (q,x,y, t_target |`| ((ffilter (\<lambda>t . (t_input t, t_output t) = (x,y)) qts)))) ios)) nexts)"
[PROOF STATE]
proof (state)
this:
qtrans = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts)

goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
have qtrans_prop: "\<And> t . t |\<in>| qtrans \<longleftrightarrow> t_source t |\<in>| nexts \<and> t_target t \<noteq> {||} \<and> fset (t_target t) = t_target ` {t' | t' . t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source t \<and> t_input t' = t_input t \<and> t_output t' = t_output t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. (t |\<in>| qtrans) = (t_source t |\<in>| nexts \<and> t_target t \<noteq> {||} \<and> fset (t_target t) = t_target ` {t' |t'. t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source t \<and> t_input t' = t_input t \<and> t_output t' = t_output t})
[PROOF STEP]
using make_observable_transitions_qtrans_helper[OF qtrans_def]
[PROOF STATE]
proof (prove)
using this:
(?t |\<in>| qtrans) = (t_source ?t |\<in>| nexts \<and> t_target ?t \<noteq> {||} \<and> fset (t_target ?t) = t_target ` {t'. t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source ?t \<and> t_input t' = t_input ?t \<and> t_output t' = t_output ?t})

goal (1 subgoal):
 1. \<And>t. (t |\<in>| qtrans) = (t_source t |\<in>| nexts \<and> t_target t \<noteq> {||} \<and> fset (t_target t) = t_target ` {t' |t'. t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source t \<and> t_input t' = t_input t \<and> t_output t' = t_output t})
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(?t |\<in>| qtrans) = (t_source ?t |\<in>| nexts \<and> t_target ?t \<noteq> {||} \<and> fset (t_target ?t) = t_target ` {t' |t'. t' |\<in>| base_trans \<and> t_source t' |\<in>| t_source ?t \<and> t_input t' = t_input ?t \<and> t_output t' = t_output ?t})

goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
let ?dones' = "dones |\<union>| nexts"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
let ?ts'    = "ts |\<union>| qtrans"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
let ?nexts' = "(fimage t_target qtrans) |-| ?dones'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
have res_cases: "make_observable_transitions base_trans nexts dones ts = (if ?nexts' = {||}
            then ?ts'
            else make_observable_transitions base_trans ?nexts' ?dones' ?ts')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. make_observable_transitions base_trans nexts dones ts = (if t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} then ts |\<union>| qtrans else make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans))
[PROOF STEP]
unfolding make_observable_transitions.simps[of base_trans nexts dones ts] qtrans_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if t_target |`| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) |-| (dones |\<union>| nexts) = {||} then ts |\<union>| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) else make_observable_transitions base_trans (t_target |`| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts))) = (if t_target |`| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) |-| (dones |\<union>| nexts) = {||} then ts |\<union>| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) else make_observable_transitions base_trans (t_target |`| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts) |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| ffUnion ((\<lambda>q. (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) (ffilter (\<lambda>t. t_source t |\<in>| q) base_trans))) |`| (\<lambda>t. (t_input t, t_output t)) |`| ffilter (\<lambda>t. t_source t |\<in>| q) base_trans) |`| nexts)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
make_observable_transitions base_trans nexts dones ts = (if t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} then ts |\<union>| qtrans else make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans))

goal (1 subgoal):
 1. \<And>base_trans nexts dones ts. (\<And>x xa xb xc. \<lbrakk>x = ffUnion ((\<lambda>q. let qts = ffilter (\<lambda>t. t_source t |\<in>| q) base_trans in Let ((\<lambda>t. (t_input t, t_output t)) |`| qts) ((|`|) (\<lambda>(x, y). (q, x, y, t_target |`| ffilter (\<lambda>t. (t_input t, t_output t) = (x, y)) qts)))) |`| nexts); xa = dones |\<union>| nexts; xb = ts |\<union>| x; xc = t_target |`| x |-| xa; xc \<noteq> {||}\<rbrakk> \<Longrightarrow> xb |\<subseteq>| make_observable_transitions base_trans xc xa xb) \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
proof (cases "?nexts' = {||}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
 2. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
t_target |`| qtrans |-| (dones |\<union>| nexts) = {||}

goal (2 subgoals):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
 2. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t_target |`| qtrans |-| (dones |\<union>| nexts) = {||}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t_target |`| qtrans |-| (dones |\<union>| nexts) = {||}

goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
using res_cases
[PROOF STATE]
proof (prove)
using this:
t_target |`| qtrans |-| (dones |\<union>| nexts) = {||}
make_observable_transitions base_trans nexts dones ts = (if t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} then ts |\<union>| qtrans else make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans))

goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||}

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||}
[PROOF STEP]
have "make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
[PROOF STATE]
proof (prove)
using this:
t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||}

goal (1 subgoal):
 1. make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
using res_cases
[PROOF STATE]
proof (prove)
using this:
t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||}
make_observable_transitions base_trans nexts dones ts = (if t_target |`| qtrans |-| (dones |\<union>| nexts) = {||} then ts |\<union>| qtrans else make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans))

goal (1 subgoal):
 1. make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
have "ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans ?nexts' ?dones' ?ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
using "1"[OF qtrans_def _ _ _ False, of ?dones' ?ts']
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>dones |\<union>| nexts = dones |\<union>| nexts; ts |\<union>| qtrans = ts |\<union>| qtrans; t_target |`| qtrans |-| (dones |\<union>| nexts) = t_target |`| qtrans |-| (dones |\<union>| nexts)\<rbrakk> \<Longrightarrow> ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. t_target |`| qtrans |-| (dones |\<union>| nexts) \<noteq> {||} \<Longrightarrow> ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
make_observable_transitions base_trans nexts dones ts = make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)
ts |\<union>| qtrans |\<subseteq>| make_observable_transitions base_trans (t_target |`| qtrans |-| (dones |\<union>| nexts)) (dones |\<union>| nexts) (ts |\<union>| qtrans)

goal (1 subgoal):
 1. ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ts |\<subseteq>| make_observable_transitions base_trans nexts dones ts

goal:
No subgoals!
[PROOF STEP]
qed