[STATEMENT]
lemma alist_remove_min:
  assumes "is_binqueue l xs"
  and "distinct (vals xs)"
  and "distinct (prios xs)"
  and "normalized xs"
  and "xs \<noteq> []"
  shows "set (dfs alist (delete_min xs)) =
  set (PQ.alist_of (PQ.remove_min (pqueue xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
[PROOF STEP]
obtain t where ot: "find_min xs = Some t"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []

goal (1 subgoal):
 1. (\<And>t. find_min xs = Some t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using normalized_find_min_exists
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
\<lbrakk>normalized ?xs; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>t. find_min ?xs = Some t

goal (1 subgoal):
 1. (\<And>t. find_min xs = Some t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
find_min xs = Some t

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
find_min xs = Some t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
find_min xs = Some t

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
proof (cases t)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
case (Node a v ys)
[PROOF STATE]
proof (state)
this:
t = Node a v ys

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
[PROOF STEP]
have "\<not> PQ.is_empty (pqueue xs)"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []

goal (1 subgoal):
 1. \<not> PQ.is_empty (pqueue xs)
[PROOF STEP]
by (simp add: empty_empty)
[PROOF STATE]
proof (state)
this:
\<not> PQ.is_empty (pqueue xs)

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
hence "set (PQ.alist_of (PQ.remove_min (pqueue xs))) =
      set (PQ.alist_of (pqueue xs)) - {(PQ.min (pqueue xs),
        the (PQ.priority (pqueue xs) (PQ.min (pqueue xs))))}"
[PROOF STATE]
proof (prove)
using this:
\<not> PQ.is_empty (pqueue xs)

goal (1 subgoal):
 1. set (pq.alist_of (remove_min (pqueue xs))) = set (pq.alist_of (pqueue xs)) - {(PQ.min (pqueue xs), the (PQ.priority (pqueue xs) (PQ.min (pqueue xs))))}
[PROOF STEP]
by (simp add: set_alist_of_remove_min[of "pqueue xs"] del: alist_of_remove_min)
[PROOF STATE]
proof (state)
this:
set (pq.alist_of (remove_min (pqueue xs))) = set (pq.alist_of (pqueue xs)) - {(PQ.min (pqueue xs), the (PQ.priority (pqueue xs) (PQ.min (pqueue xs))))}

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (pq.alist_of (remove_min (pqueue xs))) = set (pq.alist_of (pqueue xs)) - {(PQ.min (pqueue xs), the (PQ.priority (pqueue xs) (PQ.min (pqueue xs))))}

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
from assms ot Node
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
find_min xs = Some t
t = Node a v ys
[PROOF STEP]
have "set (dfs alist (delete_min xs)) = set (dfs alist xs) - {(v, a)}"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
find_min xs = Some t
t = Node a v ys

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
using alist_delete_min[of xs]
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
find_min xs = Some t
t = Node a v ys
\<lbrakk>distinct (vals xs); distinct (prios xs); find_min xs = Some (Node ?a ?v ?ts)\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (elements xs) - {(?v, ?a)}

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (elements (delete_min xs)) = set (elements xs) - {(v, a)}

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (elements (delete_min xs)) = set (elements xs) - {(v, a)}

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
from Node ot
[PROOF STATE]
proof (chain)
picking this:
t = Node a v ys
find_min xs = Some t
[PROOF STEP]
have "priority (the (find_min xs)) = a"
[PROOF STATE]
proof (prove)
using this:
t = Node a v ys
find_min xs = Some t

goal (1 subgoal):
 1. priority (the (find_min xs)) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
priority (the (find_min xs)) = a

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
priority (the (find_min xs)) = a
[PROOF STEP]
have "a = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
priority (the (find_min xs)) = a

goal (1 subgoal):
 1. a = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))
[PROOF STEP]
by (simp add: find_min_p_min)
[PROOF STATE]
proof (state)
this:
a = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
from Node ot
[PROOF STATE]
proof (chain)
picking this:
t = Node a v ys
find_min xs = Some t
[PROOF STEP]
have "val (the (find_min xs)) = v"
[PROOF STATE]
proof (prove)
using this:
t = Node a v ys
find_min xs = Some t

goal (1 subgoal):
 1. val (the (find_min xs)) = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
val (the (find_min xs)) = v

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
val (the (find_min xs)) = v
[PROOF STEP]
have "v = PQ.min (pqueue xs)"
[PROOF STATE]
proof (prove)
using this:
is_binqueue l xs
distinct (vals xs)
distinct (prios xs)
normalized xs
xs \<noteq> []
val (the (find_min xs)) = v

goal (1 subgoal):
 1. v = PQ.min (pqueue xs)
[PROOF STEP]
by (simp add: find_min_v_min)
[PROOF STATE]
proof (state)
this:
v = PQ.min (pqueue xs)

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v = PQ.min (pqueue xs)

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
note \<open>distinct (vals xs)\<close>
[PROOF STATE]
proof (state)
this:
distinct (vals xs)

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>is_binqueue l xs; distinct (vals xs); distinct (prios xs); normalized xs; xs \<noteq> []; find_min xs = Some t; t = Node x1 x2 x3\<rbrakk> \<Longrightarrow> set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (pq.alist_of (remove_min (pqueue xs))) = set (pq.alist_of (pqueue xs)) - {(PQ.min (pqueue xs), the (PQ.priority (pqueue xs) (PQ.min (pqueue xs))))}
set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
a = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))
v = PQ.min (pqueue xs)
distinct (vals xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (pq.alist_of (remove_min (pqueue xs))) = set (pq.alist_of (pqueue xs)) - {(PQ.min (pqueue xs), the (PQ.priority (pqueue xs) (PQ.min (pqueue xs))))}
set (elements (delete_min xs)) = set (elements xs) - {(v, a)}
a = the (PQ.priority (pqueue xs) (PQ.min (pqueue xs)))
v = PQ.min (pqueue xs)
distinct (vals xs)

goal (1 subgoal):
 1. set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))
[PROOF STEP]
by (simp add: alist_pqueue)
[PROOF STATE]
proof (state)
this:
set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (elements (delete_min xs)) = set (pq.alist_of (remove_min (pqueue xs)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma homs_pass1': "no_Emptys hs \<Longrightarrow> homs(pass\<^sub>1' hs) = pass\<^sub>1 (homs hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys hs \<Longrightarrow> homs (pass\<^sub>1' hs) = Pairing_Heap_Tree.pass\<^sub>1 (homs hs)
[PROOF STEP]
apply(induction hs rule: Pairing_Heap_List1.pass\<^sub>1.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>h1 h2 hs. \<lbrakk>no_Emptys hs \<Longrightarrow> homs (pass\<^sub>1' hs) = Pairing_Heap_Tree.pass\<^sub>1 (homs hs); no_Emptys (h1 # h2 # hs)\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' (h1 # h2 # hs)) = Pairing_Heap_Tree.pass\<^sub>1 (homs (h1 # h2 # hs))
 2. no_Emptys [] \<Longrightarrow> homs (pass\<^sub>1' []) = Pairing_Heap_Tree.pass\<^sub>1 (homs [])
 3. \<And>v. no_Emptys [v] \<Longrightarrow> homs (pass\<^sub>1' [v]) = Pairing_Heap_Tree.pass\<^sub>1 (homs [v])
[PROOF STEP]
subgoal for h1 h2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_Emptys hs_ \<Longrightarrow> homs (pass\<^sub>1' hs_) = Pairing_Heap_Tree.pass\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_)\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' (h1 # h2 # hs_)) = Pairing_Heap_Tree.pass\<^sub>1 (homs (h1 # h2 # hs_))
[PROOF STEP]
apply(case_tac h1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_Emptys hs_ \<Longrightarrow> homs (pass\<^sub>1' hs_) = Pairing_Heap_Tree.pass\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = heap.Empty\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' (h1 # h2 # hs_)) = Pairing_Heap_Tree.pass\<^sub>1 (homs (h1 # h2 # hs_))
 2. \<And>x21 x22. \<lbrakk>no_Emptys hs_ \<Longrightarrow> homs (pass\<^sub>1' hs_) = Pairing_Heap_Tree.pass\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = Hp x21 x22\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' (h1 # h2 # hs_)) = Pairing_Heap_Tree.pass\<^sub>1 (homs (h1 # h2 # hs_))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>no_Emptys hs_ \<Longrightarrow> homs (pass\<^sub>1' hs_) = Pairing_Heap_Tree.pass\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = Hp x21 x22\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' (h1 # h2 # hs_)) = Pairing_Heap_Tree.pass\<^sub>1 (homs (h1 # h2 # hs_))
[PROOF STEP]
apply(case_tac h2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22. \<lbrakk>no_Emptys hs_ \<Longrightarrow> homs (pass\<^sub>1' hs_) = Pairing_Heap_Tree.pass\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = Hp x21 x22; h2 = heap.Empty\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' (h1 # h2 # hs_)) = Pairing_Heap_Tree.pass\<^sub>1 (homs (h1 # h2 # hs_))
 2. \<And>x21 x22 x21a x22a. \<lbrakk>no_Emptys hs_ \<Longrightarrow> homs (pass\<^sub>1' hs_) = Pairing_Heap_Tree.pass\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = Hp x21 x22; h2 = Hp x21a x22a\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' (h1 # h2 # hs_)) = Pairing_Heap_Tree.pass\<^sub>1 (homs (h1 # h2 # hs_))
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. no_Emptys [] \<Longrightarrow> homs (pass\<^sub>1' []) = Pairing_Heap_Tree.pass\<^sub>1 (homs [])
 2. \<And>v. no_Emptys [v] \<Longrightarrow> homs (pass\<^sub>1' [v]) = Pairing_Heap_Tree.pass\<^sub>1 (homs [v])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. no_Emptys [v] \<Longrightarrow> homs (pass\<^sub>1' [v]) = Pairing_Heap_Tree.pass\<^sub>1 (homs [v])
[PROOF STEP]
subgoal for h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys [h] \<Longrightarrow> homs (pass\<^sub>1' [h]) = Pairing_Heap_Tree.pass\<^sub>1 (homs [h])
[PROOF STEP]
apply(case_tac h)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_Emptys [h]; h = heap.Empty\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' [h]) = Pairing_Heap_Tree.pass\<^sub>1 (homs [h])
 2. \<And>x21 x22. \<lbrakk>no_Emptys [h]; h = Hp x21 x22\<rbrakk> \<Longrightarrow> homs (pass\<^sub>1' [h]) = Pairing_Heap_Tree.pass\<^sub>1 (homs [h])
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hom_merge': "\<lbrakk> no_Emptys lhs; Pairing_Heap_List1_Analysis.is_root h\<rbrakk>
       \<Longrightarrow> hom (merge' (Hp x lhs) h) = link \<langle>homs lhs, x, hom h\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_Emptys lhs; is_root' h\<rbrakk> \<Longrightarrow> hom (merge' (Hp x lhs) h) = link \<langle>homs lhs, x, hom h\<rangle>
[PROOF STEP]
by(cases h) auto


[STATEMENT]
lemma hom_pass2': "no_Emptys hs \<Longrightarrow> hom(pass\<^sub>2' hs) = pass\<^sub>2 (homs hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys hs \<Longrightarrow> hom (pass\<^sub>2' hs) = Pairing_Heap_Tree.pass\<^sub>2 (homs hs)
[PROOF STEP]
by(induction hs rule: homs.induct) (auto simp: hom_merge' is_root_pass2)


[STATEMENT]
lemma del_min': "is_root' h \<Longrightarrow> hom(del_min' h) = del_min (hom h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_root' h \<Longrightarrow> hom (del_min' h) = Pairing_Heap_Tree.del_min (hom h)
[PROOF STEP]
by(cases h)
  (auto simp: homs_pass1' hom_pass2' no_Emptys_pass1 is_root_pass2)


[STATEMENT]
lemma insert': "is_root' h \<Longrightarrow> hom(insert' x h) = insert x (hom h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_root' h \<Longrightarrow> hom (insert' x h) = Pairing_Heap_Tree.insert x (hom h)
[PROOF STEP]
by(cases h)(auto)


[STATEMENT]
lemma merge':
  "\<lbrakk> is_root' h1; is_root' h2 \<rbrakk> \<Longrightarrow> hom(merge' h1 h2) = merge (hom h1) (hom h2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_root' h1; is_root' h2\<rbrakk> \<Longrightarrow> hom (merge' h1 h2) = Pairing_Heap_Tree.merge (hom h1) (hom h2)
[PROOF STEP]
apply(cases h1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_root' h1; is_root' h2; h1 = heap.Empty\<rbrakk> \<Longrightarrow> hom (merge' h1 h2) = Pairing_Heap_Tree.merge (hom h1) (hom h2)
 2. \<And>x21 x22. \<lbrakk>is_root' h1; is_root' h2; h1 = Hp x21 x22\<rbrakk> \<Longrightarrow> hom (merge' h1 h2) = Pairing_Heap_Tree.merge (hom h1) (hom h2)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>is_root' h1; is_root' h2; h1 = Hp x21 x22\<rbrakk> \<Longrightarrow> hom (merge' h1 h2) = Pairing_Heap_Tree.merge (hom h1) (hom h2)
[PROOF STEP]
apply(cases h2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22. \<lbrakk>is_root' h1; is_root' h2; h1 = Hp x21 x22; h2 = heap.Empty\<rbrakk> \<Longrightarrow> hom (merge' h1 h2) = Pairing_Heap_Tree.merge (hom h1) (hom h2)
 2. \<And>x21 x22 x21a x22a. \<lbrakk>is_root' h1; is_root' h2; h1 = Hp x21 x22; h2 = Hp x21a x22a\<rbrakk> \<Longrightarrow> hom (merge' h1 h2) = Pairing_Heap_Tree.merge (hom h1) (hom h2)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma T_pass1': "no_Emptys hs \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1(homs hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys hs \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs hs)
[PROOF STEP]
apply(induction hs rule: Pairing_Heap_List1.pass\<^sub>1.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>h1 h2 hs. \<lbrakk>no_Emptys hs \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs hs); no_Emptys (h1 # h2 # hs)\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' (h1 # h2 # hs) = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs (h1 # h2 # hs))
 2. no_Emptys [] \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' [] = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs [])
 3. \<And>v. no_Emptys [v] \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' [v] = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs [v])
[PROOF STEP]
subgoal for h1 h2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_Emptys hs_ \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs_ = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_)\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' (h1 # h2 # hs_) = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs (h1 # h2 # hs_))
[PROOF STEP]
apply(case_tac h1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_Emptys hs_ \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs_ = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = heap.Empty\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' (h1 # h2 # hs_) = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs (h1 # h2 # hs_))
 2. \<And>x21 x22. \<lbrakk>no_Emptys hs_ \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs_ = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = Hp x21 x22\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' (h1 # h2 # hs_) = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs (h1 # h2 # hs_))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22. \<lbrakk>no_Emptys hs_ \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs_ = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = Hp x21 x22\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' (h1 # h2 # hs_) = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs (h1 # h2 # hs_))
[PROOF STEP]
apply(case_tac h2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22. \<lbrakk>no_Emptys hs_ \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs_ = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = Hp x21 x22; h2 = heap.Empty\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' (h1 # h2 # hs_) = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs (h1 # h2 # hs_))
 2. \<And>x21 x22 x21a x22a. \<lbrakk>no_Emptys hs_ \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' hs_ = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs hs_); no_Emptys (h1 # h2 # hs_); h1 = Hp x21 x22; h2 = Hp x21a x22a\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' (h1 # h2 # hs_) = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs (h1 # h2 # hs_))
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. no_Emptys [] \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' [] = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs [])
 2. \<And>v. no_Emptys [v] \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' [v] = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs [v])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. no_Emptys [v] \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' [v] = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs [v])
[PROOF STEP]
subgoal for h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys [h] \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' [h] = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs [h])
[PROOF STEP]
apply(case_tac h)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_Emptys [h]; h = heap.Empty\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' [h] = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs [h])
 2. \<And>x21 x22. \<lbrakk>no_Emptys [h]; h = Hp x21 x22\<rbrakk> \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1' [h] = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>1 (homs [h])
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma T_pass2': "no_Emptys hs \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2' hs = T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2(homs hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_Emptys hs \<Longrightarrow> T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2' hs = Pairing_Heap_Tree_Analysis.T\<^sub>p\<^sub>a\<^sub>s\<^sub>s\<^sub>2 (homs hs)
[PROOF STEP]
by(induction hs rule: homs.induct) (auto simp: hom_merge' is_root_pass2)


[STATEMENT]
lemma size_hp: "is_root' h \<Longrightarrow> size_hp h = size (hom h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_root' h \<Longrightarrow> size_hp h = size (hom h)
[PROOF STEP]
proof(induction h)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_root' heap.Empty \<Longrightarrow> size_hp heap.Empty = size (hom heap.Empty)
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1 x2)\<rbrakk> \<Longrightarrow> size_hp (Hp x1 x2) = size (hom (Hp x1 x2))
[PROOF STEP]
case (Hp _ hs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set hs; is_root' ?x2a\<rbrakk> \<Longrightarrow> size_hp ?x2a = size (hom ?x2a)
is_root' (Hp x1_ hs)

goal (2 subgoals):
 1. is_root' heap.Empty \<Longrightarrow> size_hp heap.Empty = size (hom heap.Empty)
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1 x2)\<rbrakk> \<Longrightarrow> size_hp (Hp x1 x2) = size (hom (Hp x1 x2))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set hs; is_root' ?x2a\<rbrakk> \<Longrightarrow> size_hp ?x2a = size (hom ?x2a)
is_root' (Hp x1_ hs)

goal (1 subgoal):
 1. size_hp (Hp x1_ hs) = size (hom (Hp x1_ hs))
[PROOF STEP]
apply(induction hs rule: homs.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set []; is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ [])\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ []) = size (hom (Hp x1_ []))
 2. \<And>x lhs rhs. \<lbrakk>\<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set lhs; is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ lhs)\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ lhs) = size (hom (Hp x1_ lhs)); \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set rhs; is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ rhs)\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ rhs) = size (hom (Hp x1_ rhs)); \<And>x2a. \<lbrakk>x2a \<in> set (Hp x lhs # rhs); is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ (Hp x lhs # rhs))\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ (Hp x lhs # rhs)) = size (hom (Hp x1_ (Hp x lhs # rhs)))
 3. \<And>va. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set (heap.Empty # va); is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ (heap.Empty # va))\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ (heap.Empty # va)) = size (hom (Hp x1_ (heap.Empty # va)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x lhs rhs. \<lbrakk>\<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set lhs; is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ lhs)\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ lhs) = size (hom (Hp x1_ lhs)); \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set rhs; is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ rhs)\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ rhs) = size (hom (Hp x1_ rhs)); \<And>x2a. \<lbrakk>x2a \<in> set (Hp x lhs # rhs); is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ (Hp x lhs # rhs))\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ (Hp x lhs # rhs)) = size (hom (Hp x1_ (Hp x lhs # rhs)))
 2. \<And>va. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set (heap.Empty # va); is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ (heap.Empty # va))\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ (heap.Empty # va)) = size (hom (Hp x1_ (heap.Empty # va)))
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>va. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set (heap.Empty # va); is_root' x2a\<rbrakk> \<Longrightarrow> size_hp x2a = size (hom x2a); is_root' (Hp x1_ (heap.Empty # va))\<rbrakk> \<Longrightarrow> size_hp (Hp x1_ (heap.Empty # va)) = size (hom (Hp x1_ (heap.Empty # va)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
size_hp (Hp x1_ hs) = size (hom (Hp x1_ hs))

goal (1 subgoal):
 1. is_root' heap.Empty \<Longrightarrow> size_hp heap.Empty = size (hom heap.Empty)
[PROOF STEP]
qed simp


[STATEMENT]
lemma "a \<^bold>\<or> a \<^bold>\<approx> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (a \<^bold>\<or> a) w = a w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (a w \<or> a w) = a w
[PROOF STEP]
by simp


[STATEMENT]
lemma "a \<^bold>\<and> a \<^bold>\<approx> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (a \<^bold>\<and> a) w = a w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (a w \<and> a w) = a w
[PROOF STEP]
by simp


[STATEMENT]
lemma "a \<^bold>\<preceq> a \<^bold>\<or> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<^bold>\<or> b \<^bold>\<succeq> a
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>w. a w \<or> b w) \<^bold>\<succeq> a
[PROOF STEP]
by simp


[STATEMENT]
lemma "a \<^bold>\<and> b \<^bold>\<preceq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<^bold>\<succeq> a \<^bold>\<and> b
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<^bold>\<succeq> (\<lambda>w. a w \<and> b w)
[PROOF STEP]
by simp


[STATEMENT]
lemma "(a \<^bold>\<and> b) \<^bold>\<or> b \<^bold>\<approx> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (a \<^bold>\<and> b \<^bold>\<or> b) w = b w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (a w \<and> b w \<or> b w) = b w
[PROOF STEP]
by auto


[STATEMENT]
lemma "a \<^bold>\<and> (a \<^bold>\<or> b) \<^bold>\<approx> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (a \<^bold>\<and> (a \<^bold>\<or> b)) w = a w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (a w \<and> (a w \<or> b w)) = a w
[PROOF STEP]
by auto


[STATEMENT]
lemma "a \<^bold>\<preceq> c \<Longrightarrow> b \<^bold>\<preceq> c \<Longrightarrow> a \<^bold>\<or> b \<^bold>\<preceq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<^bold>\<succeq> a; c \<^bold>\<succeq> b\<rbrakk> \<Longrightarrow> c \<^bold>\<succeq> a \<^bold>\<or> b
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<^bold>\<succeq> a; c \<^bold>\<succeq> b\<rbrakk> \<Longrightarrow> c \<^bold>\<succeq> (\<lambda>w. a w \<or> b w)
[PROOF STEP]
by simp


[STATEMENT]
lemma "c \<^bold>\<preceq> a \<Longrightarrow> c \<^bold>\<preceq> b \<Longrightarrow> c \<^bold>\<preceq> a \<^bold>\<and> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<^bold>\<succeq> c; b \<^bold>\<succeq> c\<rbrakk> \<Longrightarrow> a \<^bold>\<and> b \<^bold>\<succeq> c
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<^bold>\<succeq> c; b \<^bold>\<succeq> c\<rbrakk> \<Longrightarrow> (\<lambda>w. a w \<and> b w) \<^bold>\<succeq> c
[PROOF STEP]
by simp


[STATEMENT]
lemma "a \<^bold>\<preceq> b \<equiv> (a \<^bold>\<or> b) \<^bold>\<approx> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<^bold>\<succeq> a \<equiv> \<forall>w. (a \<^bold>\<or> b) w = b w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<^bold>\<succeq> a \<equiv> \<forall>w. (a w \<or> b w) = b w
[PROOF STEP]
by smt


[STATEMENT]
lemma "b \<^bold>\<preceq> a \<equiv> (a \<^bold>\<and> b) \<^bold>\<approx> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<^bold>\<succeq> b \<equiv> \<forall>w. (a \<^bold>\<and> b) w = b w
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<^bold>\<succeq> b \<equiv> \<forall>w. (a w \<and> b w) = b w
[PROOF STEP]
by smt


[STATEMENT]
lemma "a \<^bold>\<preceq> c \<Longrightarrow> b \<^bold>\<preceq> d \<Longrightarrow> (a \<^bold>\<or> b) \<^bold>\<preceq> (c \<^bold>\<or> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<^bold>\<succeq> a; d \<^bold>\<succeq> b\<rbrakk> \<Longrightarrow> c \<^bold>\<or> d \<^bold>\<succeq> a \<^bold>\<or> b
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<^bold>\<succeq> a; d \<^bold>\<succeq> b\<rbrakk> \<Longrightarrow> (\<lambda>w. c w \<or> d w) \<^bold>\<succeq> (\<lambda>w. a w \<or> b w)
[PROOF STEP]
by simp


[STATEMENT]
lemma "a \<^bold>\<preceq> c \<Longrightarrow> b \<^bold>\<preceq> d \<Longrightarrow> (a \<^bold>\<and> b) \<^bold>\<preceq> (c \<^bold>\<and> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<^bold>\<succeq> a; d \<^bold>\<succeq> b\<rbrakk> \<Longrightarrow> c \<^bold>\<and> d \<^bold>\<succeq> a \<^bold>\<and> b
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<^bold>\<succeq> a; d \<^bold>\<succeq> b\<rbrakk> \<Longrightarrow> (\<lambda>w. c w \<and> d w) \<^bold>\<succeq> (\<lambda>w. a w \<and> b w)
[PROOF STEP]
by simp


[STATEMENT]
lemma comp_symm: "\<phi>\<^sup>c = \<psi> \<Longrightarrow> \<phi> = \<psi>\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sup>c = \<psi> \<Longrightarrow> \<phi> = \<psi>\<^sup>c
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X w. \<not> \<phi> X w) = \<psi> \<Longrightarrow> \<phi> = (\<lambda>X w. \<not> \<psi> X w)
[PROOF STEP]
by blast


[STATEMENT]
lemma comp_invol: "\<phi>\<^sup>c\<^sup>c = \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X. compl\<^sup>c (\<phi> X)) = \<phi>
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X w. \<not> \<not> \<phi> X w) = \<phi>
[PROOF STEP]
by blast


[STATEMENT]
lemma dual_symm: "(\<phi> \<equiv> \<psi>\<^sup>d) \<Longrightarrow> (\<psi> \<equiv> \<phi>\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<equiv> \<psi>\<^sup>d \<Longrightarrow> \<psi> \<equiv> \<phi>\<^sup>d
[PROOF STEP]
unfolding dual_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<equiv> \<lambda>X w. \<not> \<psi> (\<lambda>w. \<not> X w) w \<Longrightarrow> \<psi> \<equiv> \<lambda>X w. \<not> \<not> \<psi> (\<lambda>w. \<not> \<not> X w) w
[PROOF STEP]
by simp


[STATEMENT]
lemma dual_comp: "\<phi>\<^sup>d\<^sup>c = \<phi>\<^sup>c\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sup>d\<^sup>c = \<phi>\<^sup>c\<^sup>d
[PROOF STEP]
unfolding dual_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X. compl\<^sup>c (\<phi> (\<^bold>\<midarrow>X))) = (\<lambda>X. compl\<^sup>c (\<phi> (\<^bold>\<midarrow>X)))
[PROOF STEP]
by simp


[STATEMENT]
lemma "id\<^sup>d \<^bold>\<equiv> id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id\<^sup>d \<^bold>\<equiv> id
[PROOF STEP]
by (simp add: id_def dual_def equal_op_def conn)


[STATEMENT]
lemma "id\<^sup>c \<^bold>\<equiv> compl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id\<^sup>c \<^bold>\<equiv> compl
[PROOF STEP]
by (simp add: id_def dual_def equal_op_def conn)


[STATEMENT]
lemma "(A \<^bold>\<squnion> B)\<^sup>d \<^bold>\<equiv> (A\<^sup>d) \<^bold>\<sqinter> (B\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<^bold>\<squnion> B\<^sup>d \<^bold>\<equiv> A\<^sup>d \<^bold>\<sqinter> B\<^sup>d
[PROOF STEP]
by (simp add: dual_def equal_op_def conn)


[STATEMENT]
lemma "(A \<^bold>\<squnion> B)\<^sup>c \<^bold>\<equiv> (A\<^sup>c) \<^bold>\<sqinter> (B\<^sup>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X. (\<^bold>\<or>) (A X)\<^sup>c (B X)) \<^bold>\<equiv> A\<^sup>c \<^bold>\<sqinter> B\<^sup>c
[PROOF STEP]
by (simp add: equal_op_def conn)


[STATEMENT]
lemma "(A \<^bold>\<sqinter> B)\<^sup>d \<^bold>\<equiv> (A\<^sup>d) \<^bold>\<squnion> (B\<^sup>d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<^bold>\<sqinter> B\<^sup>d \<^bold>\<equiv> A\<^sup>d \<^bold>\<squnion> B\<^sup>d
[PROOF STEP]
by (simp add: dual_def equal_op_def conn)


[STATEMENT]
lemma "(A \<^bold>\<sqinter> B)\<^sup>c \<^bold>\<equiv> (A\<^sup>c) \<^bold>\<squnion> (B\<^sup>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X. (\<^bold>\<and>) (A X)\<^sup>c (B X)) \<^bold>\<equiv> A\<^sup>c \<^bold>\<squnion> B\<^sup>c
[PROOF STEP]
by (simp add: equal_op_def conn)


[STATEMENT]
lemma fp_c: "(fp \<phi>\<^sup>c) X = (X \<^bold>\<approx> \<^bold>\<midarrow>(\<phi> X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. \<phi>\<^sup>c X w = X w) = (\<forall>w. X w = \<phi>\<^sup>c X w)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. (\<not> \<phi> X w) = X w) = (\<forall>w. X w = (\<not> \<phi> X w))
[PROOF STEP]
by auto


[STATEMENT]
lemma fp_dc:"(fp \<phi>\<^sup>d\<^sup>c) X = (X \<^bold>\<approx> \<phi>(\<^bold>\<midarrow>X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. \<phi>\<^sup>d\<^sup>c X w = X w) = (\<forall>w. X w = \<phi> (\<^bold>\<midarrow>X) w)
[PROOF STEP]
unfolding dual_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. (\<not> \<not> \<phi> (\<lambda>w. \<not> X w) w) = X w) = (\<forall>w. X w = \<phi> (\<lambda>w. \<not> X w) w)
[PROOF STEP]
by auto


[STATEMENT]
lemma ofp_c: "(\<phi>\<^sup>c)\<^sup>f\<^sup>p \<^bold>\<equiv> (\<phi>\<^sup>f\<^sup>p)\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sup>c\<^sup>f\<^sup>p \<^bold>\<equiv> (\<lambda>X. (\<^bold>\<leftrightarrow>) (\<phi> X)\<^sup>c X)
[PROOF STEP]
unfolding conn equal_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X w. ((\<not> \<phi> X w) = X w) = (\<phi> X w \<noteq> X w)
[PROOF STEP]
by auto


[STATEMENT]
lemma ofp_d: "(\<phi>\<^sup>d)\<^sup>f\<^sup>p \<^bold>\<equiv> (\<phi>\<^sup>f\<^sup>p)\<^sup>d\<^sup>c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sup>d\<^sup>f\<^sup>p \<^bold>\<equiv> \<phi>\<^sup>f\<^sup>p\<^sup>d\<^sup>c
[PROOF STEP]
unfolding dual_def equal_op_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X w. ((\<not> \<phi> (\<lambda>w. \<not> X w) w) = X w) = (\<not> \<phi> (\<lambda>w. \<not> X w) w \<noteq> (\<not> X w))
[PROOF STEP]
by auto


[STATEMENT]
lemma ofp_dc:"(\<phi>\<^sup>d\<^sup>c)\<^sup>f\<^sup>p \<^bold>\<equiv> (\<phi>\<^sup>f\<^sup>p)\<^sup>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sup>d\<^sup>c\<^sup>f\<^sup>p \<^bold>\<equiv> \<phi>\<^sup>f\<^sup>p\<^sup>d
[PROOF STEP]
unfolding dual_def equal_op_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X w. ((\<not> \<not> \<phi> (\<lambda>w. \<not> X w) w) = X w) = (\<phi> (\<lambda>w. \<not> X w) w \<noteq> (\<not> X w))
[PROOF STEP]
by auto


[STATEMENT]
lemma ofp_decomp: "\<phi>\<^sup>f\<^sup>p \<^bold>\<equiv> (id \<^bold>\<sqinter> \<phi>) \<^bold>\<squnion> ((id \<^bold>\<squnion> \<phi>)\<^sup>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi>\<^sup>f\<^sup>p \<^bold>\<equiv> (\<lambda>X. (id \<^bold>\<sqinter> \<phi>) X \<^bold>\<or> (\<^bold>\<or>) (id X)\<^sup>c (\<phi> X))
[PROOF STEP]
unfolding equal_op_def id_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X w. (\<phi> X w = X w) = (X w \<and> \<phi> X w \<or> \<not> (X w \<or> \<phi> X w))
[PROOF STEP]
by auto


[STATEMENT]
lemma ofp_invol: "(\<phi>\<^sup>f\<^sup>p)\<^sup>f\<^sup>p \<^bold>\<equiv> \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X. (\<^bold>\<leftrightarrow>) (\<phi> X)\<^sup>f\<^sup>p X) \<^bold>\<equiv> \<phi>
[PROOF STEP]
unfolding conn equal_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X w. ((\<phi> X w = X w) = X w) = \<phi> X w
[PROOF STEP]
by auto


[STATEMENT]
lemma fp_rel: "((fp \<phi>) X) = (\<phi>\<^sup>f\<^sup>p X \<^bold>\<approx> \<^bold>\<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. \<phi> X w = X w) = (\<forall>w. \<phi>\<^sup>f\<^sup>p X w = \<^bold>\<top> w)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. \<phi> X w = X w) = (\<forall>w. (\<phi> X w = X w) = True)
[PROOF STEP]
by auto


[STATEMENT]
lemma fp_d_rel:  "((fp \<phi>\<^sup>d) X) = (\<phi>\<^sup>f\<^sup>p(\<^bold>\<midarrow>X) \<^bold>\<approx> \<^bold>\<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. \<phi>\<^sup>d X w = X w) = (\<forall>w. \<phi>\<^sup>f\<^sup>p (\<^bold>\<midarrow>X) w = \<^bold>\<top> w)
[PROOF STEP]
unfolding dual_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. (\<not> \<phi> (\<lambda>w. \<not> X w) w) = X w) = (\<forall>w. (\<phi> (\<lambda>w. \<not> X w) w = (\<not> X w)) = True)
[PROOF STEP]
by auto


[STATEMENT]
lemma fp_c_rel: "((fp \<phi>\<^sup>c) X) = (\<phi>\<^sup>f\<^sup>p  X  \<^bold>\<approx> \<^bold>\<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. \<phi>\<^sup>c X w = X w) = (\<forall>w. \<phi>\<^sup>f\<^sup>p X w = \<^bold>\<bottom> w)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. (\<not> \<phi> X w) = X w) = (\<forall>w. (\<phi> X w = X w) = False)
[PROOF STEP]
by auto


[STATEMENT]
lemma fp_dc_rel: "((fp \<phi>\<^sup>d\<^sup>c) X) = (\<phi>\<^sup>f\<^sup>p(\<^bold>\<midarrow>X) \<^bold>\<approx> \<^bold>\<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. \<phi>\<^sup>d\<^sup>c X w = X w) = (\<forall>w. \<phi>\<^sup>f\<^sup>p (\<^bold>\<midarrow>X) w = \<^bold>\<bottom> w)
[PROOF STEP]
unfolding dual_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. (\<not> \<not> \<phi> (\<lambda>w. \<not> X w) w) = X w) = (\<forall>w. (\<phi> (\<lambda>w. \<not> X w) w = (\<not> X w)) = False)
[PROOF STEP]
by auto


[STATEMENT]
lemma eq_ext: "a \<^bold>\<approx> b \<Longrightarrow>  a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. a w = b w \<Longrightarrow> a = b
[PROOF STEP]
using ext
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g

goal (1 subgoal):
 1. \<forall>w. a w = b w \<Longrightarrow> a = b
[PROOF STEP]
by blast


[STATEMENT]
lemma eq_ext': "a \<^bold>\<equiv> b \<Longrightarrow>  a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<^bold>\<equiv> b \<Longrightarrow> a = b
[PROOF STEP]
using ext
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g

goal (1 subgoal):
 1. a \<^bold>\<equiv> b \<Longrightarrow> a = b
[PROOF STEP]
unfolding equal_op_def
[PROOF STATE]
proof (prove)
using this:
(\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g

goal (1 subgoal):
 1. \<forall>X w. a X w = b X w \<Longrightarrow> a = b
[PROOF STEP]
by blast


[STATEMENT]
lemma join_char: "a \<^bold>\<preceq> b \<longleftrightarrow> a \<^bold>\<or> b \<^bold>\<approx> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<^bold>\<succeq> a) = (\<forall>w. (a \<^bold>\<or> b) w = b w)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<^bold>\<succeq> a) = (\<forall>w. (a w \<or> b w) = b w)
[PROOF STEP]
by blast


[STATEMENT]
lemma atomic1: "\<forall>w. \<exists>q. q w \<and> (\<forall>p. p w \<longrightarrow> q \<^bold>\<preceq> p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. \<exists>q. q w \<and> (\<forall>p. p w \<longrightarrow> p \<^bold>\<succeq> q)
[PROOF STEP]
using the_sym_eq_trivial
[PROOF STATE]
proof (prove)
using this:
(THE y. ?x = y) = ?x

goal (1 subgoal):
 1. \<forall>w. \<exists>q. q w \<and> (\<forall>p. p w \<longrightarrow> p \<^bold>\<succeq> q)
[PROOF STEP]
by (metis (full_types))


[STATEMENT]
lemma atomic2: "\<forall>w. \<exists>q. q w \<and> atom(q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. \<exists>q. q w \<and> atom q
[PROOF STEP]
using the_sym_eq_trivial
[PROOF STATE]
proof (prove)
using this:
(THE y. ?x = y) = ?x

goal (1 subgoal):
 1. \<forall>w. \<exists>q. q w \<and> atom q
[PROOF STEP]
by (metis (full_types) atom_def compl_def bottom_def)


[STATEMENT]
lemma atomic3: "\<forall>p. \<not>(p \<^bold>\<approx> \<^bold>\<bottom>) \<longrightarrow> (\<exists>q. atom(q) \<and> q \<^bold>\<preceq> p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
(*using atom_def unfolding conn by fastforce*)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
assume "\<not>(p \<^bold>\<approx> \<^bold>\<bottom>)"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>w. p w = \<^bold>\<bottom> w)

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
hence "\<exists>v. p v"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>w. p w = \<^bold>\<bottom> w)

goal (1 subgoal):
 1. \<exists>v. p v
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>w. p w = False)

goal (1 subgoal):
 1. \<exists>v. p v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>v. p v

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. p v
[PROOF STEP]
obtain w where 1:"p w"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. p v

goal (1 subgoal):
 1. (\<And>w. p w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule exE)
[PROOF STATE]
proof (state)
this:
p w

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
let ?q="\<lambda>v. v = w"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
(*using HOL primitive equality*)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
have 2: "atom ?q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom (\<lambda>v. v = w)
[PROOF STEP]
unfolding atom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>wa. (wa = w) = \<^bold>\<bottom> wa) \<and> (\<forall>p. p \<^bold>\<succeq> (\<lambda>wa. wa = w) \<or> \<^bold>\<midarrow>p \<^bold>\<succeq> (\<lambda>wa. wa = w))
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>wa. (wa = w) = False) \<and> (\<forall>p. p \<^bold>\<succeq> (\<lambda>wa. wa = w) \<or> (\<lambda>w. \<not> p w) \<^bold>\<succeq> (\<lambda>wa. wa = w))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom (\<lambda>v. v = w)

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
have "\<forall>v. ?q v \<longrightarrow> p v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<^bold>\<succeq> (\<lambda>v. v = w)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
p w

goal (1 subgoal):
 1. p \<^bold>\<succeq> (\<lambda>v. v = w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<^bold>\<succeq> (\<lambda>v. v = w)

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
hence 3: "?q \<^bold>\<preceq> p"
[PROOF STATE]
proof (prove)
using this:
p \<^bold>\<succeq> (\<lambda>v. v = w)

goal (1 subgoal):
 1. p \<^bold>\<succeq> (\<lambda>wa. wa = w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<^bold>\<succeq> (\<lambda>wa. wa = w)

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
from 2 3
[PROOF STATE]
proof (chain)
picking this:
atom (\<lambda>v. v = w)
p \<^bold>\<succeq> (\<lambda>wa. wa = w)
[PROOF STEP]
have "\<exists>q. atom(q) \<and> q \<^bold>\<preceq> p"
[PROOF STATE]
proof (prove)
using this:
atom (\<lambda>v. v = w)
p \<^bold>\<succeq> (\<lambda>wa. wa = w)

goal (1 subgoal):
 1. \<exists>q. atom q \<and> p \<^bold>\<succeq> q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>q. atom q \<and> p \<^bold>\<succeq> q

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<Longrightarrow> \<exists>q. atom q \<and> p \<^bold>\<succeq> q

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
hence "\<not>(p \<^bold>\<approx> \<^bold>\<bottom>) \<longrightarrow> (\<exists>q. atom(q) \<and> q \<^bold>\<preceq> p)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<Longrightarrow> \<exists>q. atom q \<and> p \<^bold>\<succeq> q

goal (1 subgoal):
 1. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
by (rule impI)
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>w. ?p2 w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> ?p2 \<^bold>\<succeq> q)

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>w. ?p2 w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> ?p2 \<^bold>\<succeq> q)

goal (1 subgoal):
 1. \<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)
[PROOF STEP]
by (rule allI)
[PROOF STATE]
proof (state)
this:
\<forall>p. \<not> (\<forall>w. p w = \<^bold>\<bottom> w) \<longrightarrow> (\<exists>q. atom q \<and> p \<^bold>\<succeq> q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_fun_zero [simp]:
  "inv fun_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abstract_Linear_Poly.inv fun_zero
[PROOF STEP]
by simp


[STATEMENT]
lemma inv_fun_plus [simp]:
  "\<lbrakk>inv (f1 :: nat \<Rightarrow> 'a::monoid_add); inv f2\<rbrakk> \<Longrightarrow> inv (fun_plus f1 f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Abstract_Linear_Poly.inv f1; Abstract_Linear_Poly.inv f2\<rbrakk> \<Longrightarrow> Abstract_Linear_Poly.inv (fun_plus f1 f2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Abstract_Linear_Poly.inv f1; Abstract_Linear_Poly.inv f2\<rbrakk> \<Longrightarrow> Abstract_Linear_Poly.inv (fun_plus f1 f2)
[PROOF STEP]
have *: "{v. f1 v + f2 v \<noteq> (0 :: 'a)} \<subseteq> {v. f1 v \<noteq> (0 :: 'a)} \<union> {v. f2 v \<noteq> (0 :: 'a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v. f1 v + f2 v \<noteq> (0::'a)} \<subseteq> {v. f1 v \<noteq> (0::'a)} \<union> {v. f2 v \<noteq> (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v. f1 v + f2 v \<noteq> (0::'a)} \<subseteq> {v. f1 v \<noteq> (0::'a)} \<union> {v. f2 v \<noteq> (0::'a)}

goal (1 subgoal):
 1. \<lbrakk>Abstract_Linear_Poly.inv f1; Abstract_Linear_Poly.inv f2\<rbrakk> \<Longrightarrow> Abstract_Linear_Poly.inv (fun_plus f1 f2)
[PROOF STEP]
assume "inv f1" "inv f2"
[PROOF STATE]
proof (state)
this:
Abstract_Linear_Poly.inv f1
Abstract_Linear_Poly.inv f2

goal (1 subgoal):
 1. \<lbrakk>Abstract_Linear_Poly.inv f1; Abstract_Linear_Poly.inv f2\<rbrakk> \<Longrightarrow> Abstract_Linear_Poly.inv (fun_plus f1 f2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Abstract_Linear_Poly.inv f1
Abstract_Linear_Poly.inv f2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Abstract_Linear_Poly.inv f1
Abstract_Linear_Poly.inv f2

goal (1 subgoal):
 1. Abstract_Linear_Poly.inv (fun_plus f1 f2)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Abstract_Linear_Poly.inv f1
Abstract_Linear_Poly.inv f2
{v. f1 v + f2 v \<noteq> (0::'a)} \<subseteq> {v. f1 v \<noteq> (0::'a)} \<union> {v. f2 v \<noteq> (0::'a)}

goal (1 subgoal):
 1. Abstract_Linear_Poly.inv (fun_plus f1 f2)
[PROOF STEP]
by (auto simp add: finite_subset)
[PROOF STATE]
proof (state)
this:
Abstract_Linear_Poly.inv (fun_plus f1 f2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_fun_scale [simp]:
  "inv (f :: nat \<Rightarrow> 'a::ring) \<Longrightarrow> inv (fun_scale r f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abstract_Linear_Poly.inv f \<Longrightarrow> Abstract_Linear_Poly.inv (fun_scale r f)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Abstract_Linear_Poly.inv f \<Longrightarrow> Abstract_Linear_Poly.inv (fun_scale r f)
[PROOF STEP]
have *: "{v. r * (f v) \<noteq> 0} \<subseteq> {v. f v \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v. r * f v \<noteq> (0::'a)} \<subseteq> {v. f v \<noteq> (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v. r * f v \<noteq> (0::'a)} \<subseteq> {v. f v \<noteq> (0::'a)}

goal (1 subgoal):
 1. Abstract_Linear_Poly.inv f \<Longrightarrow> Abstract_Linear_Poly.inv (fun_scale r f)
[PROOF STEP]
assume "inv f"
[PROOF STATE]
proof (state)
this:
Abstract_Linear_Poly.inv f

goal (1 subgoal):
 1. Abstract_Linear_Poly.inv f \<Longrightarrow> Abstract_Linear_Poly.inv (fun_scale r f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Abstract_Linear_Poly.inv f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Abstract_Linear_Poly.inv f

goal (1 subgoal):
 1. Abstract_Linear_Poly.inv (fun_scale r f)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Abstract_Linear_Poly.inv f
{v. r * f v \<noteq> (0::'a)} \<subseteq> {v. f v \<noteq> (0::'a)}

goal (1 subgoal):
 1. Abstract_Linear_Poly.inv (fun_scale r f)
[PROOF STEP]
by (auto simp add: finite_subset)
[PROOF STATE]
proof (state)
this:
Abstract_Linear_Poly.inv (fun_scale r f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeff_plus [simp] : "coeff (lp1 + lp2) var = coeff lp1 var + coeff lp2 var"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (lp1 + lp2) var = coeff lp1 var + coeff lp2 var
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma coeff_scaleRat [simp]: "coeff (k *R lp1) var = k * coeff lp1 var"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (k *R lp1) var = k * coeff lp1 var
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma coeff_uminus [simp]: "coeff (-lp) var = - coeff lp var"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (- lp) var = - coeff lp var
[PROOF STEP]
unfolding uminus_linear_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (- 1 *R lp) var = - coeff lp var
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma coeff_minus [simp]: "coeff (lp1 - lp2) var = coeff lp1 var - coeff lp2 var"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (lp1 - lp2) var = coeff lp1 var - coeff lp2 var
[PROOF STEP]
unfolding minus_linear_poly_def uminus_linear_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (lp1 + - 1 *R lp2) var = coeff lp1 var - coeff lp2 var
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma coeff_zero: "coeff p x \<noteq> 0 \<longleftrightarrow> x \<in> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (coeff p x \<noteq> 0) = (x \<in> vars p)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma finite_vars: "finite (vars p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars p)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma set_vars_list: "set (vars_list lp) = vars lp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (vars_list lp) = vars lp
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma valuate_zero: "(0 \<lbrace>v\<rbrace>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<lbrace> v \<rbrace> = (0::'a)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma
  valuate_diff: "(p \<lbrace>v1\<rbrace>) - (p \<lbrace>v2\<rbrace>) = (p \<lbrace> \<lambda> x. v1 x - v2 x \<rbrace>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<lbrace> v1 \<rbrace> - p \<lbrace> v2 \<rbrace> = p \<lbrace> \<lambda>x. v1 x - v2 x \<rbrace>
[PROOF STEP]
by (transfer, simp add: sum_subtractf[THEN sym], auto simp: rational_vector.scale_right_diff_distrib)


[STATEMENT]
lemma valuate_opposite_val:
  shows "p \<lbrace> \<lambda> x. - v x \<rbrace> = - (p \<lbrace> v \<rbrace>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<lbrace> \<lambda>x. - v x \<rbrace> = - p \<lbrace> v \<rbrace>
[PROOF STEP]
using valuate_diff[of p "\<lambda> x. 0" v]
[PROOF STATE]
proof (prove)
using this:
p \<lbrace> \<lambda>x. 0::'a \<rbrace> - p \<lbrace> v \<rbrace> = p \<lbrace> \<lambda>x. (0::'a) - v x \<rbrace>

goal (1 subgoal):
 1. p \<lbrace> \<lambda>x. - v x \<rbrace> = - p \<lbrace> v \<rbrace>
[PROOF STEP]
by (auto simp add: valuate_def)


[STATEMENT]
lemma valuate_nonneg:
  fixes v :: "'a::linordered_rational_vector valuation"
  assumes "\<forall> x \<in> vars p. (coeff p x > 0 \<longrightarrow> v x \<ge> 0) \<and> (coeff p x < 0 \<longrightarrow> v x \<le> 0)"
  shows "p \<lbrace> v \<rbrace> \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> p \<lbrace> v \<rbrace>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))

goal (1 subgoal):
 1. (0::'a) \<le> p \<lbrace> v \<rbrace>
[PROOF STEP]
proof (transfer, unfold fun_valuate_def, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pa va. \<lbrakk>Abstract_Linear_Poly.inv pa; \<forall>x\<in>fun_vars pa. (0 < fun_coeff pa x \<longrightarrow> (0::'a) \<le> va x) \<and> (fun_coeff pa x < 0 \<longrightarrow> va x \<le> (0::'a)); \<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))\<rbrakk> \<Longrightarrow> (0::'a) \<le> (\<Sum>x\<in>{v. pa v \<noteq> 0}. pa x *R va x)
[PROOF STEP]
case (1 p v)
[PROOF STATE]
proof (state)
this:
Abstract_Linear_Poly.inv p
\<forall>x\<in>fun_vars p. (0 < fun_coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (fun_coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))

goal (1 subgoal):
 1. \<And>pa va. \<lbrakk>Abstract_Linear_Poly.inv pa; \<forall>x\<in>fun_vars pa. (0 < fun_coeff pa x \<longrightarrow> (0::'a) \<le> va x) \<and> (fun_coeff pa x < 0 \<longrightarrow> va x \<le> (0::'a)); \<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))\<rbrakk> \<Longrightarrow> (0::'a) \<le> (\<Sum>x\<in>{v. pa v \<noteq> 0}. pa x *R va x)
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
Abstract_Linear_Poly.inv p
\<forall>x\<in>fun_vars p. (0 < fun_coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (fun_coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))
[PROOF STEP]
have fin: "finite {v. p v \<noteq> 0}"
[PROOF STATE]
proof (prove)
using this:
Abstract_Linear_Poly.inv p
\<forall>x\<in>fun_vars p. (0 < fun_coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (fun_coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))

goal (1 subgoal):
 1. finite {v. p v \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {v. p v \<noteq> 0}

goal (1 subgoal):
 1. \<And>pa va. \<lbrakk>Abstract_Linear_Poly.inv pa; \<forall>x\<in>fun_vars pa. (0 < fun_coeff pa x \<longrightarrow> (0::'a) \<le> va x) \<and> (fun_coeff pa x < 0 \<longrightarrow> va x \<le> (0::'a)); \<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))\<rbrakk> \<Longrightarrow> (0::'a) \<le> (\<Sum>x\<in>{v. pa v \<noteq> 0}. pa x *R va x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {v. p v \<noteq> 0}
[PROOF STEP]
show "0 \<le> (\<Sum>x\<in>{v. p v \<noteq> 0}. p x *R v x)"
[PROOF STATE]
proof (prove)
using this:
finite {v. p v \<noteq> 0}

goal (1 subgoal):
 1. (0::'a) \<le> (\<Sum>x\<in>{v. p v \<noteq> 0}. p x *R v x)
[PROOF STEP]
proof (induct rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (0::'a) \<le> (\<Sum>x\<in>{}. p x *R v x)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (0::'a) \<le> (\<Sum>x\<in>F. p x *R v x)\<rbrakk> \<Longrightarrow> (0::'a) \<le> (\<Sum>x\<in>insert x F. p x *R v x)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (0::'a) \<le> (\<Sum>x\<in>{}. p x *R v x)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (0::'a) \<le> (\<Sum>x\<in>F. p x *R v x)\<rbrakk> \<Longrightarrow> (0::'a) \<le> (\<Sum>x\<in>insert x F. p x *R v x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (\<Sum>x\<in>{}. p x *R v x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (\<Sum>x\<in>{}. p x *R v x)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (0::'a) \<le> (\<Sum>x\<in>F. p x *R v x)\<rbrakk> \<Longrightarrow> (0::'a) \<le> (\<Sum>x\<in>insert x F. p x *R v x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (0::'a) \<le> (\<Sum>x\<in>F. p x *R v x)\<rbrakk> \<Longrightarrow> (0::'a) \<le> (\<Sum>x\<in>insert x F. p x *R v x)
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
(0::'a) \<le> (\<Sum>x\<in>F. p x *R v x)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (0::'a) \<le> (\<Sum>x\<in>F. p x *R v x)\<rbrakk> \<Longrightarrow> (0::'a) \<le> (\<Sum>x\<in>insert x F. p x *R v x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (\<Sum>x\<in>insert x F. p x *R v x)
[PROOF STEP]
unfolding sum.insert[OF insert(1-2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> p x *R v x + (\<Sum>x\<in>F. p x *R v x)
[PROOF STEP]
proof (rule order.trans[OF _ add_mono[OF _ insert(3)]])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (0::'a) \<le> ?a1 + (0::'a)
 2. ?a1 \<le> p x *R v x
[PROOF STEP]
show "0 \<le> p x *R v x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> p x *R v x
[PROOF STEP]
using scaleRat_leq1[of 0 "v x" "p x"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) \<le> v x; 0 < p x\<rbrakk> \<Longrightarrow> p x *R (0::'a) \<le> p x *R v x

goal (1 subgoal):
 1. (0::'a) \<le> p x *R v x
[PROOF STEP]
using scaleRat_leq2[of "v x" 0 "p x"] 1(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) \<le> v x; 0 < p x\<rbrakk> \<Longrightarrow> p x *R (0::'a) \<le> p x *R v x
\<lbrakk>v x \<le> (0::'a); p x < 0\<rbrakk> \<Longrightarrow> p x *R (0::'a) \<le> p x *R v x
\<forall>x\<in>fun_vars p. (0 < fun_coeff p x \<longrightarrow> (0::'a) \<le> v x) \<and> (fun_coeff p x < 0 \<longrightarrow> v x \<le> (0::'a))

goal (1 subgoal):
 1. (0::'a) \<le> p x *R v x
[PROOF STEP]
by (cases "p x > 0"; cases "p x < 0"; auto)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> p x *R v x

goal (1 subgoal):
 1. (0::'a) \<le> (0::'a) + (0::'a)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (\<Sum>x\<in>insert x F. p x *R v x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (\<Sum>x\<in>{v. p v \<noteq> 0}. p x *R v x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valuate_nonpos:
  fixes v :: "'a::linordered_rational_vector valuation"
  assumes "\<forall> x \<in> vars p. (coeff p x > 0 \<longrightarrow> v x \<le> 0) \<and> (coeff p x < 0 \<longrightarrow> v x \<ge> 0)"
  shows "p \<lbrace> v \<rbrace> \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> \<le> (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> v x \<le> (0::'a)) \<and> (coeff p x < 0 \<longrightarrow> (0::'a) \<le> v x)

goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> \<le> (0::'a)
[PROOF STEP]
using valuate_opposite_val[of p v]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> v x \<le> (0::'a)) \<and> (coeff p x < 0 \<longrightarrow> (0::'a) \<le> v x)
p \<lbrace> \<lambda>x. - v x \<rbrace> = - p \<lbrace> v \<rbrace>

goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> \<le> (0::'a)
[PROOF STEP]
using valuate_nonneg[of p "\<lambda> x. - v x"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> v x \<le> (0::'a)) \<and> (coeff p x < 0 \<longrightarrow> (0::'a) \<le> v x)
p \<lbrace> \<lambda>x. - v x \<rbrace> = - p \<lbrace> v \<rbrace>
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> - v x) \<and> (coeff p x < 0 \<longrightarrow> - v x \<le> (0::'a)) \<Longrightarrow> (0::'a) \<le> p \<lbrace> \<lambda>x. - v x \<rbrace>

goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> \<le> (0::'a)
[PROOF STEP]
using scaleRat_leq2[of "0::'a" _ "-1"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> v x \<le> (0::'a)) \<and> (coeff p x < 0 \<longrightarrow> (0::'a) \<le> v x)
p \<lbrace> \<lambda>x. - v x \<rbrace> = - p \<lbrace> v \<rbrace>
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> - v x) \<and> (coeff p x < 0 \<longrightarrow> - v x \<le> (0::'a)) \<Longrightarrow> (0::'a) \<le> p \<lbrace> \<lambda>x. - v x \<rbrace>
\<lbrakk>(0::'a) \<le> ?b; - 1 < 0\<rbrakk> \<Longrightarrow> - 1 *R ?b \<le> - 1 *R (0::'a)

goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> \<le> (0::'a)
[PROOF STEP]
using scaleRat_leq2[of _ "0::'a" "-1"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> v x \<le> (0::'a)) \<and> (coeff p x < 0 \<longrightarrow> (0::'a) \<le> v x)
p \<lbrace> \<lambda>x. - v x \<rbrace> = - p \<lbrace> v \<rbrace>
\<forall>x\<in>vars p. (0 < coeff p x \<longrightarrow> (0::'a) \<le> - v x) \<and> (coeff p x < 0 \<longrightarrow> - v x \<le> (0::'a)) \<Longrightarrow> (0::'a) \<le> p \<lbrace> \<lambda>x. - v x \<rbrace>
\<lbrakk>(0::'a) \<le> ?b; - 1 < 0\<rbrakk> \<Longrightarrow> - 1 *R ?b \<le> - 1 *R (0::'a)
\<lbrakk>?a \<le> (0::'a); - 1 < 0\<rbrakk> \<Longrightarrow> - 1 *R (0::'a) \<le> - 1 *R ?a

goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> \<le> (0::'a)
[PROOF STEP]
by force


[STATEMENT]
lemma valuate_uminus: "(-p) \<lbrace>v\<rbrace> = - (p \<lbrace>v\<rbrace>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - p \<lbrace> v \<rbrace> = - p \<lbrace> v \<rbrace>
[PROOF STEP]
unfolding uminus_linear_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 *R p \<lbrace> v \<rbrace> = - p \<lbrace> v \<rbrace>
[PROOF STEP]
by (transfer, auto simp: sum_negf)


[STATEMENT]
lemma valuate_add_lemma:
  fixes v :: "'a \<Rightarrow> 'b::rational_vector"
  assumes "finite {v. f1 v \<noteq> 0}" "finite {v. f2 v \<noteq> 0}"
  shows
    "(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) =
   (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) +  (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
let ?A = "{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
have "?A = {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)} = {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)} = {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)} = {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}
[PROOF STEP]
have
    "finite ?A"
[PROOF STATE]
proof (prove)
using this:
{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)} = {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}

goal (1 subgoal):
 1. finite ({v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)} = {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}
finite {v. f1 v \<noteq> 0}
finite {v. f2 v \<noteq> 0}

goal (1 subgoal):
 1. finite ({v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)})
[PROOF STEP]
by (subgoal_tac "{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0} = {v. f1 v \<noteq> 0} \<union> {v. f2 v \<noteq> 0}") auto
[PROOF STATE]
proof (state)
this:
finite ({v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)})

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite ({v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)})
[PROOF STEP]
have "(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) =
    (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)}. (f1 x + f2 x) *R v x)"
[PROOF STATE]
proof (prove)
using this:
finite ({v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)})

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)}. (f1 x + f2 x) *R v x)
[PROOF STEP]
by (rule sum.mono_neutral_left) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)}. (f1 x + f2 x) *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)}. (f1 x + f2 x) *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
have "... = (\<Sum>x \<in> {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. (f1 x + f2 x) *R v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. (f1 x + f2 x) *R v x)
[PROOF STEP]
by (rule sum.cong) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. (f1 x + f2 x) *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0} \<union> {v. f1 v + f2 v = 0 \<and> (f1 v \<noteq> 0 \<or> f2 v \<noteq> 0)}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. (f1 x + f2 x) *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
have "... = (\<Sum>x \<in> {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) +
                   (\<Sum>x \<in> {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
by (simp add: scaleRat_left_distrib sum.distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
have "... = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) +  (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
fix f1 f2::"'a \<Rightarrow> rat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
assume "finite {v. f1 v \<noteq> 0}" "finite {v. f2 v \<noteq> 0}"
[PROOF STATE]
proof (state)
this:
finite {v. f1 v \<noteq> 0}
finite {v. f2 v \<noteq> 0}

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {v. f1 v \<noteq> 0}
finite {v. f2 v \<noteq> 0}
[PROOF STEP]
have "finite {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}"
[PROOF STATE]
proof (prove)
using this:
finite {v. f1 v \<noteq> 0}
finite {v. f2 v \<noteq> 0}

goal (1 subgoal):
 1. finite {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}
[PROOF STEP]
by (subgoal_tac "{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0} = {v. f1 v \<noteq> 0} \<union> {v. f2 v \<noteq> 0}") auto
[PROOF STATE]
proof (state)
this:
finite {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
have "(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) =
        (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> (f2 v \<noteq> 0 \<and> f1 v = 0)}. f1 x *R v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
have "... = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)
[PROOF STEP]
using \<open>finite {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}\<close>
[PROOF STATE]
proof (prove)
using this:
finite {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)
[PROOF STEP]
by (rule sum.mono_neutral_left[THEN sym]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x)
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)
[PROOF STEP]
have "(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) =
        (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x)
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0 \<and> f1 v = 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite {v. ?f1a2 v \<noteq> 0}; finite {v. ?f2a2 v \<noteq> 0}\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{v. ?f1a2 v \<noteq> 0 \<or> ?f2a2 v \<noteq> 0}. ?f1a2 x *R v x) = (\<Sum>x\<in>{v. ?f1a2 v \<noteq> 0}. ?f1a2 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite {v. ?f1a2 v \<noteq> 0}; finite {v. ?f2a2 v \<noteq> 0}\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{v. ?f1a2 v \<noteq> 0 \<or> ?f2a2 v \<noteq> 0}. ?f1a2 x *R v x) = (\<Sum>x\<in>{v. ?f1a2 v \<noteq> 0}. ?f1a2 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite {v. f1 v \<noteq> 0}
finite {v. f2 v \<noteq> 0}

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
using *[of f1 f2]
[PROOF STATE]
proof (prove)
using this:
finite {v. f1 v \<noteq> 0}
finite {v. f2 v \<noteq> 0}
\<lbrakk>finite {v. f1 v \<noteq> 0}; finite {v. f2 v \<noteq> 0}\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
using *[of f2 f1]
[PROOF STATE]
proof (prove)
using this:
finite {v. f1 v \<noteq> 0}
finite {v. f2 v \<noteq> 0}
\<lbrakk>finite {v. f1 v \<noteq> 0}; finite {v. f2 v \<noteq> 0}\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x)
\<lbrakk>finite {v. f2 v \<noteq> 0}; finite {v. f1 v \<noteq> 0}\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{v. f2 v \<noteq> 0 \<or> f1 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
by (subgoal_tac "{v. f2 v \<noteq> 0 \<or> f1 v \<noteq> 0} = {v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}") auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x)
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x)
(\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f1 v \<noteq> 0 \<or> f2 v \<noteq> 0}. f2 x *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f1 v + f2 v \<noteq> 0}. (f1 x + f2 x) *R v x) = (\<Sum>x\<in>{v. f1 v \<noteq> 0}. f1 x *R v x) + (\<Sum>x\<in>{v. f2 v \<noteq> 0}. f2 x *R v x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valuate_add:  "(p1 + p2) \<lbrace>v\<rbrace> = (p1 \<lbrace>v\<rbrace>) + (p2 \<lbrace>v\<rbrace>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 + p2 \<lbrace> v \<rbrace> = p1 \<lbrace> v \<rbrace> + p2 \<lbrace> v \<rbrace>
[PROOF STEP]
by (transfer, simp add: valuate_add_lemma)


[STATEMENT]
lemma valuate_minus: "(p1 - p2) \<lbrace>v\<rbrace> = (p1 \<lbrace>v\<rbrace>) - (p2 \<lbrace>v\<rbrace>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 - p2 \<lbrace> v \<rbrace> = p1 \<lbrace> v \<rbrace> - p2 \<lbrace> v \<rbrace>
[PROOF STEP]
unfolding minus_linear_poly_def valuate_add
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 \<lbrace> v \<rbrace> + - p2 \<lbrace> v \<rbrace> = p1 \<lbrace> v \<rbrace> - p2 \<lbrace> v \<rbrace>
[PROOF STEP]
by (simp add: valuate_uminus)


[STATEMENT]
lemma valuate_scaleRat:
  "(c *R lp) \<lbrace> v \<rbrace> = c *R ( lp\<lbrace>v\<rbrace> )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
proof (cases "c=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
 2. c \<noteq> 0 \<Longrightarrow> c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
 2. c \<noteq> 0 \<Longrightarrow> c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
by (auto simp add: valuate_def zero_linear_poly_def Abs_linear_poly_inverse)
[PROOF STATE]
proof (state)
this:
c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
[PROOF STEP]
have "\<And> v. Rep_linear_poly (c *R lp) v = c * (Rep_linear_poly lp v)"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. \<And>v. Rep_linear_poly (c *R lp) v = c * Rep_linear_poly lp v
[PROOF STEP]
unfolding scaleRat_linear_poly_def
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0

goal (1 subgoal):
 1. \<And>v. Rep_linear_poly (map_fun id (map_fun Rep_linear_poly Abs_linear_poly) fun_scale c lp) v = c * Rep_linear_poly lp v
[PROOF STEP]
using Abs_linear_poly_inverse[of "\<lambda>v. c * Rep_linear_poly lp v"]
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
(\<lambda>v. c * Rep_linear_poly lp v) \<in> {c. Abstract_Linear_Poly.inv c} \<Longrightarrow> Rep_linear_poly (Abs_linear_poly (\<lambda>v. c * Rep_linear_poly lp v)) = (\<lambda>v. c * Rep_linear_poly lp v)

goal (1 subgoal):
 1. \<And>v. Rep_linear_poly (map_fun id (map_fun Rep_linear_poly Abs_linear_poly) fun_scale c lp) v = c * Rep_linear_poly lp v
[PROOF STEP]
using Rep_linear_poly
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
(\<lambda>v. c * Rep_linear_poly lp v) \<in> {c. Abstract_Linear_Poly.inv c} \<Longrightarrow> Rep_linear_poly (Abs_linear_poly (\<lambda>v. c * Rep_linear_poly lp v)) = (\<lambda>v. c * Rep_linear_poly lp v)
Rep_linear_poly ?x \<in> {c. Abstract_Linear_Poly.inv c}

goal (1 subgoal):
 1. \<And>v. Rep_linear_poly (map_fun id (map_fun Rep_linear_poly Abs_linear_poly) fun_scale c lp) v = c * Rep_linear_poly lp v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Rep_linear_poly (c *R lp) ?v = c * Rep_linear_poly lp ?v

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Rep_linear_poly (c *R lp) ?v = c * Rep_linear_poly lp ?v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep_linear_poly (c *R lp) ?v = c * Rep_linear_poly lp ?v

goal (1 subgoal):
 1. c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>
[PROOF STEP]
unfolding valuate_def
[PROOF STATE]
proof (prove)
using this:
Rep_linear_poly (c *R lp) ?v = c * Rep_linear_poly lp ?v

goal (1 subgoal):
 1. map_fun Rep_linear_poly id fun_valuate (c *R lp) v = c *R map_fun Rep_linear_poly id fun_valuate lp v
[PROOF STEP]
using \<open>c \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
Rep_linear_poly (c *R lp) ?v = c * Rep_linear_poly lp ?v
c \<noteq> 0

goal (1 subgoal):
 1. map_fun Rep_linear_poly id fun_valuate (c *R lp) v = c *R map_fun Rep_linear_poly id fun_valuate lp v
[PROOF STEP]
by auto (subst rational_vector.scale_sum_right, auto)
[PROOF STATE]
proof (state)
this:
c *R lp \<lbrace> v \<rbrace> = c *R lp \<lbrace> v \<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valuate_Var: "(Var x) \<lbrace>v\<rbrace> = v x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Var x \<lbrace> v \<rbrace> = v x
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma valuate_sum: "((\<Sum>x\<in>A. f x) \<lbrace> v \<rbrace>) = (\<Sum>x\<in>A. ((f x) \<lbrace> v \<rbrace>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f A \<lbrace> v \<rbrace> = (\<Sum>x\<in>A. f x \<lbrace> v \<rbrace>)
[PROOF STEP]
by (induct A rule: infinite_finite_induct, auto simp: valuate_zero valuate_add)


[STATEMENT]
lemma distinct_vars_list:
  "distinct (vars_list p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (vars_list p)
[PROOF STEP]
by transfer (use distinct_sorted_list_of_set in auto)


[STATEMENT]
lemma zero_coeff_zero: "p = 0 \<longleftrightarrow> (\<forall> v. coeff p v = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p = 0) = (\<forall>v. coeff p v = 0)
[PROOF STEP]
by transfer auto