[STATEMENT]
lemma comparator_uprod_compare: "comparator (uprod_compare compare)" for compare
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comparator (uprod_compare compare)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. invert_order (uprod_compare compare x y) = uprod_compare compare y x
 2. \<And>x y. uprod_compare compare x y = Eq \<Longrightarrow> x = y
 3. \<And>x y z. \<lbrakk>uprod_compare compare x y = Lt; uprod_compare compare y z = Lt\<rbrakk> \<Longrightarrow> uprod_compare compare x z = Lt
[PROOF STEP]
show "invert_order (uprod_compare compare x y) = uprod_compare compare y x" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invert_order (uprod_compare compare x y) = uprod_compare compare y x
[PROOF STEP]
proof(transfer, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>compare x y. comparator compare \<Longrightarrow> invert_order ((case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y) = (case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) x
[PROOF STEP]
case (1 compare x y)
[PROOF STATE]
proof (state)
this:
comparator compare

goal (1 subgoal):
 1. \<And>compare x y. comparator compare \<Longrightarrow> invert_order ((case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y) = (case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
comparator compare
[PROOF STEP]
interpret comparator compare
[PROOF STATE]
proof (prove)
using this:
comparator compare

goal (1 subgoal):
 1. comparator compare
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>compare x y. comparator compare \<Longrightarrow> invert_order ((case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y) = (case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invert_order ((case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y) = (case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) x
[PROOF STEP]
by(auto split!: order.split prod.split simp add: eq Gt_lt_conv Lt_lt_conv sym dest: order.asym)
[PROOF STATE]
proof (state)
this:
invert_order ((case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y) = (case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invert_order (uprod_compare compare ?x ?y) = uprod_compare compare ?y ?x

goal (2 subgoals):
 1. \<And>x y. uprod_compare compare x y = Eq \<Longrightarrow> x = y
 2. \<And>x y z. \<lbrakk>uprod_compare compare x y = Lt; uprod_compare compare y z = Lt\<rbrakk> \<Longrightarrow> uprod_compare compare x z = Lt
[PROOF STEP]
show "x = y" if "uprod_compare compare x y = Eq" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
uprod_compare compare x y = Eq

goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof(transfer, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>compare x y. \<lbrakk>comparator compare; (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Eq\<rbrakk> \<Longrightarrow> eq_upair x y
[PROOF STEP]
case (1 compare x y)
[PROOF STATE]
proof (state)
this:
comparator compare
(case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Eq

goal (1 subgoal):
 1. \<And>compare x y. \<lbrakk>comparator compare; (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Eq\<rbrakk> \<Longrightarrow> eq_upair x y
[PROOF STEP]
from 1(1)
[PROOF STATE]
proof (chain)
picking this:
comparator compare
[PROOF STEP]
interpret comparator compare
[PROOF STATE]
proof (prove)
using this:
comparator compare

goal (1 subgoal):
 1. comparator compare
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>compare x y. \<lbrakk>comparator compare; (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Eq\<rbrakk> \<Longrightarrow> eq_upair x y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_upair x y
[PROOF STEP]
using 1(2)
[PROOF STATE]
proof (prove)
using this:
(case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Eq

goal (1 subgoal):
 1. eq_upair x y
[PROOF STEP]
by(clarsimp split: order.split_asm prod.split_asm simp add: eq)
[PROOF STATE]
proof (state)
this:
eq_upair x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
uprod_compare compare ?x ?y = Eq \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>uprod_compare compare x y = Lt; uprod_compare compare y z = Lt\<rbrakk> \<Longrightarrow> uprod_compare compare x z = Lt
[PROOF STEP]
show "uprod_compare compare x z = Lt"
    if "uprod_compare compare x y = Lt" "uprod_compare compare y z = Lt" for x y z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uprod_compare compare x z = Lt
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
uprod_compare compare x y = Lt
uprod_compare compare y z = Lt

goal (1 subgoal):
 1. uprod_compare compare x z = Lt
[PROOF STEP]
proof(transfer, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>compare x y z. \<lbrakk>comparator compare; (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Lt; (case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt\<rbrakk> \<Longrightarrow> (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt
[PROOF STEP]
case (1 compare x y z)
[PROOF STATE]
proof (state)
this:
comparator compare
(case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Lt
(case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt

goal (1 subgoal):
 1. \<And>compare x y z. \<lbrakk>comparator compare; (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Lt; (case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt\<rbrakk> \<Longrightarrow> (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt
[PROOF STEP]
from 1(1)
[PROOF STATE]
proof (chain)
picking this:
comparator compare
[PROOF STEP]
interpret comparator compare
[PROOF STATE]
proof (prove)
using this:
comparator compare

goal (1 subgoal):
 1. comparator compare
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>compare x y z. \<lbrakk>comparator compare; (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Lt; (case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt\<rbrakk> \<Longrightarrow> (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt
[PROOF STEP]
using 1(2-)
[PROOF STATE]
proof (prove)
using this:
(case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) y = Lt
(case y of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt

goal (1 subgoal):
 1. (case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt
[PROOF STEP]
by(auto split!: order.splits prod.split_asm simp add: eq Gt_lt_conv Lt_lt_conv elim: trans)
[PROOF STATE]
proof (state)
this:
(case x of (a, b) \<Rightarrow> \<lambda>(c, d). let (x, y) = case compare a b of Lt \<Rightarrow> (a, b) | _ \<Rightarrow> (b, a); (x', y') = case compare c d of Lt \<Rightarrow> (c, d) | _ \<Rightarrow> (d, c) in case compare x x' of Eq \<Rightarrow> compare y y' | Lt \<Rightarrow> Lt | Gt \<Rightarrow> Gt) z = Lt

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>uprod_compare compare ?x ?y = Lt; uprod_compare compare ?y ?z = Lt\<rbrakk> \<Longrightarrow> uprod_compare compare ?x ?z = Lt

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succs_of_clause_split: "P (succs_of_clause l x) \<longleftrightarrow> (\<forall>l1 l2. x = Upair l1 l2 \<longrightarrow> P (succs_of_clause l (Upair l1 l2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (succs_of_clause l x) = (\<forall>l1 l2. x = Upair l1 l2 \<longrightarrow> P (succs_of_clause l (Upair l1 l2)))
[PROOF STEP]
by(cases x)(auto simp only:)


[STATEMENT]
lemma commute_succs_of_clause: "comp_fun_commute (succs_of_clause l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_commute (succs_of_clause l)
[PROOF STEP]
by unfold_locales(auto split: succs_of_clause_split)


[STATEMENT]
lemma idem_succs_of_clause: "comp_fun_idem (succs_of_clause l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_idem (succs_of_clause l)
[PROOF STEP]
by unfold_locales(auto split: succs_of_clause_split)


[STATEMENT]
lemma succ_imp_graph_alt_def:
  "succ_imp_graph cnf l = Finite_Set.fold (succs_of_clause l) {} cnf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_imp_graph cnf l = Finite_Set.fold (succs_of_clause l) {} cnf
[PROOF STEP]
unfolding succ_imp_graph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_fold_cfi (succs_loop_body l) {} cnf = Finite_Set.fold (succs_of_clause l) {} cnf
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma succ_imp_graph_correct:
  "finite cnf \<Longrightarrow> succ_imp_graph cnf l = {l'. (l, l') \<in> imp_graph cnf}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite cnf \<Longrightarrow> succ_imp_graph cnf l = {l'. (l, l') \<in> imp_graph cnf}
[PROOF STEP]
by(induction rule: finite_induct)(auto split: succs_of_clause_split simp add: succ_imp_graph_alt_def)


[STATEMENT]
lemma imp_graph_code:
  "imp_graph cnf =
  (if finite cnf then {(l, l'). l' \<in> succ_imp_graph cnf l}
   else Code.abort (STR ''Infinite or invalid 2CNF formula'') (\<lambda>_. imp_graph cnf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_graph cnf = (if finite cnf then {(l, l'). l' \<in> succ_imp_graph cnf l} else Code.abort STR ''Infinite or invalid 2CNF formula'' (\<lambda>_. imp_graph cnf))
[PROOF STEP]
by(auto simp add: succ_imp_graph_correct)


[STATEMENT]
lemma UNIV_lit: "UNIV = range (\<lambda>(x, pos). Lit x pos)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = range (\<lambda>(x, pos). Lit x pos)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> range (\<lambda>x. case x of (x, xa) \<Rightarrow> Lit x xa)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> range (\<lambda>x. case x of (x, xa) \<Rightarrow> Lit x xa)
[PROOF STEP]
by(cases x; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_vars_of_cnf: "finite cnf \<Longrightarrow> finite (vars_of_cnf cnf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite cnf \<Longrightarrow> finite (vars_of_cnf cnf)
[PROOF STEP]
by(clarsimp simp add: vars_of_cnf_def)


[STATEMENT]
lemma satisfiable_code:
  "satisfiable cnf \<longleftrightarrow>
  (if finite cnf \<and> is_2sat cnf then
   let G = imp_graph cnf in \<forall>x\<in>vars_of_cnf cnf. \<not> (reachable G (Pos x) (Neg x) \<and> reachable G (Neg x) (Pos x))
   else Code.abort (STR ''Infinite or invalid 2CNF formula'') (\<lambda>_. satisfiable cnf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfiable cnf = (if finite cnf \<and> is_2sat cnf then let G = imp_graph cnf in \<forall>x\<in>vars_of_cnf cnf. \<not> (reachable G (Pos x) (Neg x) \<and> reachable G (Neg x) (Pos x)) else Code.abort STR ''Infinite or invalid 2CNF formula'' (\<lambda>_. satisfiable cnf))
[PROOF STEP]
by(simp add: reachable_def finite_2sat_iff finite_vars_of_cnf Let_def)


[STATEMENT]
lemma succ_imp_graph_outside: "succ_imp_graph cnf l = {}" if "var l \<notin> vars_of_cnf cnf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_imp_graph cnf l = {}
[PROOF STEP]
proof(cases "finite cnf")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
 2. infinite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite cnf

goal (2 subgoals):
 1. finite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
 2. infinite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
[PROOF STEP]
interpret comp_fun_idem "succs_of_clause l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_idem (succs_of_clause l)
[PROOF STEP]
by(rule idem_succs_of_clause)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
 2. infinite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_imp_graph cnf l = {}
[PROOF STEP]
using True that
[PROOF STATE]
proof (prove)
using this:
finite cnf
var l \<notin> vars_of_cnf cnf

goal (1 subgoal):
 1. succ_imp_graph cnf l = {}
[PROOF STEP]
by induction(auto simp add: succ_imp_graph_alt_def vars_of_cnf_def split: if_split_asm succs_of_clause_split)
[PROOF STATE]
proof (state)
this:
succ_imp_graph cnf l = {}

goal (1 subgoal):
 1. infinite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite cnf

goal (1 subgoal):
 1. infinite cnf \<Longrightarrow> succ_imp_graph cnf l = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite cnf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite cnf

goal (1 subgoal):
 1. succ_imp_graph cnf l = {}
[PROOF STEP]
by(simp add: succ_imp_graph_alt_def)
[PROOF STATE]
proof (state)
this:
succ_imp_graph cnf l = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_fun_idem_insert_mapping: "comp_fun_idem insert_mapping"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_idem insert_mapping
[PROOF STEP]
unfolding insert_mapping_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_idem (\<lambda>uu. case uu of (k, v) \<Rightarrow> \<lambda>m. case Mapping.lookup m k of None \<Rightarrow> Mapping.update k {v} m | Some V \<Rightarrow> Mapping.update k (insert v V) m)
[PROOF STEP]
by(unfold_locales; transfer; auto simp add: Map_To_Mapping.map_apply_def fun_eq_iff split!: option.split)


[STATEMENT]
lemma comp_fun_idem_insert_clause: "comp_fun_idem insert_clause"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_idem insert_clause
[PROOF STEP]
apply(unfold_locales)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y x. insert_clause y \<circ> insert_clause x = insert_clause x \<circ> insert_clause y
 2. \<And>x. insert_clause x \<circ> insert_clause x = insert_clause x
[PROOF STEP]
subgoal for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_clause x \<circ> insert_clause y = insert_clause y \<circ> insert_clause x
[PROOF STEP]
by(cases x; cases y; simp; metis commute_left_comp comp_fun_commute rewriteL_comp_comp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. insert_clause x \<circ> insert_clause x = insert_clause x
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_clause x \<circ> insert_clause x = insert_clause x
[PROOF STEP]
by(cases x; simp; metis (no_types, opaque_lifting) commute_left_comp comp_assoc comp_fun_idem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tabulate_graph_code [code]:
  "tabulate_graph cnf =
  (if finite cnf then set_fold_cfi insert_clause' Mapping.empty cnf
   else Code.abort (STR ''Infinite clause set'') (\<lambda>_. tabulate_graph cnf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tabulate_graph cnf = (if finite cnf then set_fold_cfi insert_clause' Mapping.empty cnf else Code.abort STR ''Infinite clause set'' (\<lambda>_. tabulate_graph cnf))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tabulate_graph cnf = (if finite cnf then set_fold_cfi insert_clause' Mapping.empty cnf else Code.abort STR ''Infinite clause set'' (\<lambda>_. tabulate_graph cnf))
[PROOF STEP]
interpret comp_fun_idem insert_clause
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_idem insert_clause
[PROOF STEP]
by(rule comp_fun_idem_insert_clause)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tabulate_graph cnf = (if finite cnf then set_fold_cfi insert_clause' Mapping.empty cnf else Code.abort STR ''Infinite clause set'' (\<lambda>_. tabulate_graph cnf))
[PROOF STEP]
have * [symmetric]: "Finite_Set.fold insert_clause Mapping.empty cnf = tabulate_graph cnf"
    if "finite cnf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Set.fold insert_clause Mapping.empty cnf = tabulate_graph cnf
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
finite cnf

goal (1 subgoal):
 1. Finite_Set.fold insert_clause Mapping.empty cnf = tabulate_graph cnf
[PROOF STEP]
proof(induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Finite_Set.fold insert_clause Mapping.empty {} = tabulate_graph {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; Finite_Set.fold insert_clause Mapping.empty F = tabulate_graph F\<rbrakk> \<Longrightarrow> Finite_Set.fold insert_clause Mapping.empty (insert x F) = tabulate_graph (insert x F)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. Finite_Set.fold insert_clause Mapping.empty {} = tabulate_graph {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; Finite_Set.fold insert_clause Mapping.empty F = tabulate_graph F\<rbrakk> \<Longrightarrow> Finite_Set.fold insert_clause Mapping.empty (insert x F) = tabulate_graph (insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Set.fold insert_clause Mapping.empty {} = tabulate_graph {}
[PROOF STEP]
by(simp)(transfer; auto simp add: fun_eq_iff Map_To_Mapping.map_empty_def vars_of_cnf_def)
[PROOF STATE]
proof (state)
this:
Finite_Set.fold insert_clause Mapping.empty {} = tabulate_graph {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; Finite_Set.fold insert_clause Mapping.empty F = tabulate_graph F\<rbrakk> \<Longrightarrow> Finite_Set.fold insert_clause Mapping.empty (insert x F) = tabulate_graph (insert x F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; Finite_Set.fold insert_clause Mapping.empty F = tabulate_graph F\<rbrakk> \<Longrightarrow> Finite_Set.fold insert_clause Mapping.empty (insert x F) = tabulate_graph (insert x F)
[PROOF STEP]
case (insert C cnf)
[PROOF STATE]
proof (state)
this:
finite cnf
C \<notin> cnf
Finite_Set.fold insert_clause Mapping.empty cnf = tabulate_graph cnf

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; Finite_Set.fold insert_clause Mapping.empty F = tabulate_graph F\<rbrakk> \<Longrightarrow> Finite_Set.fold insert_clause Mapping.empty (insert x F) = tabulate_graph (insert x F)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finite_Set.fold insert_clause Mapping.empty (insert C cnf) = tabulate_graph (insert C cnf)
[PROOF STEP]
by(cases C; simp add: insert; transfer)(auto simp add: fun_eq_iff Map_To_Mapping.map_apply_def split!: option.split)
[PROOF STATE]
proof (state)
this:
Finite_Set.fold insert_clause Mapping.empty (insert C cnf) = tabulate_graph (insert C cnf)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite cnf \<Longrightarrow> tabulate_graph cnf = Finite_Set.fold insert_clause Mapping.empty cnf

goal (1 subgoal):
 1. tabulate_graph cnf = (if finite cnf then set_fold_cfi insert_clause' Mapping.empty cnf else Code.abort STR ''Infinite clause set'' (\<lambda>_. tabulate_graph cnf))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tabulate_graph cnf = (if finite cnf then set_fold_cfi insert_clause' Mapping.empty cnf else Code.abort STR ''Infinite clause set'' (\<lambda>_. tabulate_graph cnf))
[PROOF STEP]
by(clarsimp)(transfer fixing: cnf; rule *)
[PROOF STATE]
proof (state)
this:
tabulate_graph cnf = (if finite cnf then set_fold_cfi insert_clause' Mapping.empty cnf else Code.abort STR ''Infinite clause set'' (\<lambda>_. tabulate_graph cnf))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma succ_imp_graph_impl_code [code]:
  "succ_imp_graph cnf =
  (if finite cnf then let m = tabulate_graph cnf
   in (\<lambda>l. case Mapping.lookup m l of None \<Rightarrow> {} | Some succs' \<Rightarrow> succs')
   else Code.abort (STR ''Infinite clause set'') (\<lambda>_. succ_imp_graph cnf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ_imp_graph cnf = (if finite cnf then let m = tabulate_graph cnf in (\<lambda>l. case Mapping.lookup m l of None \<Rightarrow> {} | Some succs' \<Rightarrow> succs') else Code.abort STR ''Infinite clause set'' (\<lambda>_. succ_imp_graph cnf))
[PROOF STEP]
by transfer(auto simp add: succ_imp_graph_correct fun_eq_iff Map_To_Mapping.map_apply_def dest: succ_imp_graph_outside)


[STATEMENT]
lemma retrofit_with_prems:
  fixes P Q R TAG :: "prop"
  assumes 1: "PROP P ==> PROP Q" (* Original goal state *)
  assumes 2: "PROP R ==> PROP TAG &&& PROP P" (* Result of first subgoal *)
  shows "PROP R ==> PROP Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP R \<Longrightarrow> PROP Q
[PROOF STEP]
(* New goal state with &&&*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP R \<Longrightarrow> PROP Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PROP R \<Longrightarrow> PROP Q
[PROOF STEP]
assume "PROP R"
[PROOF STATE]
proof (state)
this:
PROP R

goal (1 subgoal):
 1. PROP R \<Longrightarrow> PROP Q
[PROOF STEP]
from this[THEN 2, THEN conjunctionD2]
[PROOF STATE]
proof (chain)
picking this:
PROP P
[PROOF STEP]
have "PROP P"
[PROOF STATE]
proof (prove)
using this:
PROP P

goal (1 subgoal):
 1. PROP P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
PROP P

goal (1 subgoal):
 1. PROP R \<Longrightarrow> PROP Q
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
PROP P \<Longrightarrow> PROP Q
PROP P
[PROOF STEP]
show "PROP Q"
[PROOF STATE]
proof (prove)
using this:
PROP P \<Longrightarrow> PROP Q
PROP P

goal (1 subgoal):
 1. PROP Q
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
PROP Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma retrofit_no_prems:
  fixes P Q TAG :: "prop"
  assumes 1: "PROP P ==> PROP Q" (* Original goal state *)
  assumes 2: "PROP TAG &&& PROP P" (* Result of first subgoal *)
  shows "PROP Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP Q
[PROOF STEP]
(* New goal state *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROP Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PROP Q
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
PROP TAG &&& PROP P
[PROOF STEP]
have "PROP P"
[PROOF STATE]
proof (prove)
using this:
PROP TAG &&& PROP P

goal (1 subgoal):
 1. PROP P
[PROOF STEP]
by (rule conjunctionD2)
[PROOF STATE]
proof (state)
this:
PROP P

goal (1 subgoal):
 1. PROP Q
[PROOF STEP]
thus "PROP Q"
[PROOF STATE]
proof (prove)
using this:
PROP P

goal (1 subgoal):
 1. PROP Q
[PROOF STEP]
by (rule 1)
[PROOF STATE]
proof (state)
this:
PROP Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_is_class: "finite {C. is_class P C}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {C. is_class P C}
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {C. is_class P C}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {C. is_class P C}
[PROOF STEP]
have "{C. is_class P C} = dom (map_of P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {C. is_class P C} = dom (map_of P)
[PROOF STEP]
by (simp add: is_class_def class_def dom_def)
[PROOF STATE]
proof (state)
this:
{C. is_class P C} = dom (map_of P)

goal (1 subgoal):
 1. finite {C. is_class P C}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{C. is_class P C} = dom (map_of P)

goal (1 subgoal):
 1. finite {C. is_class P C}
[PROOF STEP]
by (simp add: finite_dom_map_of)
[PROOF STATE]
proof (state)
this:
finite {C. is_class P C}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_type_simps [simp]:
  "is_type P Void \<and> is_type P Boolean \<and> is_type P Integer \<and>
  is_type P NT \<and> is_type P (Class C) = is_class P C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_type P Void \<and> is_type P Boolean \<and> is_type P Integer \<and> is_type P NT \<and> is_type P (Class C) = is_class P C
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_type P Void \<and> is_type P Boolean \<and> is_type P Integer \<and> is_type P NT \<and> is_type P (Class C) = is_class P C
[PROOF STEP]
by(simp add:is_type_def)


[STATEMENT]
lemma is_TNil_tfilter: "is_TNil (tfilter P xs) \<longleftrightarrow> (\<forall>x \<in> tset xs. \<not> P x)" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_TNil (local.tfilter P xs) = (\<forall>x\<in>tset xs. \<not> P x)
[PROOF STEP]
proof(rule iffI ballI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_TNil (local.tfilter P xs); x \<in> tset xs\<rbrakk> \<Longrightarrow> \<not> P x
 2. \<forall>x\<in>tset xs. \<not> P x \<Longrightarrow> is_TNil (local.tfilter P xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_TNil (local.tfilter P xs); x \<in> tset xs\<rbrakk> \<Longrightarrow> \<not> P x
 2. \<forall>x\<in>tset xs. \<not> P x \<Longrightarrow> is_TNil (local.tfilter P xs)
[PROOF STEP]
assume "x \<in> tset xs" ?lhs
[PROOF STATE]
proof (state)
this:
x \<in> tset xs
is_TNil (local.tfilter P xs)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_TNil (local.tfilter P xs); x \<in> tset xs\<rbrakk> \<Longrightarrow> \<not> P x
 2. \<forall>x\<in>tset xs. \<not> P x \<Longrightarrow> is_TNil (local.tfilter P xs)
[PROOF STEP]
thus "\<not> P x"
[PROOF STATE]
proof (prove)
using this:
x \<in> tset xs
is_TNil (local.tfilter P xs)

goal (1 subgoal):
 1. \<not> P x
[PROOF STEP]
proof(induct rule: tllist_set_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>\<not> is_TNil xs; is_TNil (local.tfilter P xs)\<rbrakk> \<Longrightarrow> \<not> P (thd xs)
 2. \<And>xs y. \<lbrakk>\<not> is_TNil xs; y \<in> tset (ttl xs); is_TNil (local.tfilter P (ttl xs)) \<Longrightarrow> \<not> P y; is_TNil (local.tfilter P xs)\<rbrakk> \<Longrightarrow> \<not> P y
[PROOF STEP]
case (find xs)
[PROOF STATE]
proof (state)
this:
\<not> is_TNil xs
is_TNil (local.tfilter P xs)

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>\<not> is_TNil xs; is_TNil (local.tfilter P xs)\<rbrakk> \<Longrightarrow> \<not> P (thd xs)
 2. \<And>xs y. \<lbrakk>\<not> is_TNil xs; y \<in> tset (ttl xs); is_TNil (local.tfilter P (ttl xs)) \<Longrightarrow> \<not> P y; is_TNil (local.tfilter P xs)\<rbrakk> \<Longrightarrow> \<not> P y
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<not> is_TNil xs
is_TNil (local.tfilter P xs)

goal (1 subgoal):
 1. \<not> P (thd xs)
[PROOF STEP]
by(cases xs)(simp_all split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<not> P (thd xs)

goal (1 subgoal):
 1. \<And>xs y. \<lbrakk>\<not> is_TNil xs; y \<in> tset (ttl xs); is_TNil (local.tfilter P (ttl xs)) \<Longrightarrow> \<not> P y; is_TNil (local.tfilter P xs)\<rbrakk> \<Longrightarrow> \<not> P y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs y. \<lbrakk>\<not> is_TNil xs; y \<in> tset (ttl xs); is_TNil (local.tfilter P (ttl xs)) \<Longrightarrow> \<not> P y; is_TNil (local.tfilter P xs)\<rbrakk> \<Longrightarrow> \<not> P y
[PROOF STEP]
case (step xs x)
[PROOF STATE]
proof (state)
this:
\<not> is_TNil xs
x \<in> tset (ttl xs)
is_TNil (local.tfilter P (ttl xs)) \<Longrightarrow> \<not> P x
is_TNil (local.tfilter P xs)

goal (1 subgoal):
 1. \<And>xs y. \<lbrakk>\<not> is_TNil xs; y \<in> tset (ttl xs); is_TNil (local.tfilter P (ttl xs)) \<Longrightarrow> \<not> P y; is_TNil (local.tfilter P xs)\<rbrakk> \<Longrightarrow> \<not> P y
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<not> is_TNil xs
x \<in> tset (ttl xs)
is_TNil (local.tfilter P (ttl xs)) \<Longrightarrow> \<not> P x
is_TNil (local.tfilter P xs)

goal (1 subgoal):
 1. \<not> P x
[PROOF STEP]
by(cases xs)(simp_all split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<not> P x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> P x

goal (1 subgoal):
 1. \<forall>x\<in>tset xs. \<not> P x \<Longrightarrow> is_TNil (local.tfilter P xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>tset xs. \<not> P x \<Longrightarrow> is_TNil (local.tfilter P xs)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>tset xs. \<not> P x

goal (1 subgoal):
 1. \<forall>x\<in>tset xs. \<not> P x \<Longrightarrow> is_TNil (local.tfilter P xs)
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>tset xs. \<not> P x

goal (1 subgoal):
 1. is_TNil (local.tfilter P xs)
[PROOF STEP]
by(induct arbitrary: xs rule: tfilter.fixp_induct)(simp_all split: tllist.split)
[PROOF STATE]
proof (state)
this:
is_TNil (local.tfilter P xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mcont2mcont_tfilter[THEN tllist.mcont2mcont, simp, cont_intro]:
  shows mcont_tfilter: "mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) (tfilter b P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) (TLList_CCPO_Examples.tfilter b P)
[PROOF STEP]
apply(rule tllist.fixp_preserves_mcont1[OF tfilter.mono tfilter_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) f \<Longrightarrow> mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) (\<lambda>xs. case xs of TNil b' \<Rightarrow> TNil b' | TCons x xs' \<Rightarrow> if P x then TCons x (f xs') else f xs')
[PROOF STEP]
apply(rule mcont_lprefix_case_aux)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>f x. mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) f \<Longrightarrow> mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) (\<lambda>xs. if P x then TCons x (f xs) else f xs)
 2. \<And>f. mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) f \<Longrightarrow> class.ccpo (tSup b) (tllist_ord b) (mk_less (tllist_ord b))
 3. \<And>f x. mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) f \<Longrightarrow> tllist_ord b (TNil b) x
 4. \<And>f. mcont (tSup b) (tllist_ord b) (tSup b) (tllist_ord b) f \<Longrightarrow> cont (flat_lub b) (flat_ord b) (tSup b) (tllist_ord b) TNil
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tfilter_tfilter:
  "tfilter b P (tfilter b Q xs) = tfilter b (\<lambda>x. P x \<and> Q x) xs" (is "?lhs xs = ?rhs xs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs) = TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs
[PROOF STEP]
proof(rule tllist.leq_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. tllist_ord ?b (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs)) (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs)
 2. tllist_ord ?b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))
[PROOF STEP]
have "\<forall>xs. tllist_ord b (?lhs xs) (?rhs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. tllist_ord b (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs)) (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs)
[PROOF STEP]
by(rule tfilter.fixp_induct[where Pa="\<lambda>f. \<forall>xs. tllist_ord b (tfilter b P (f xs)) (?rhs xs)"])(auto split: tllist.split)
[PROOF STATE]
proof (state)
this:
\<forall>xs. tllist_ord b (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs)) (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs)

goal (2 subgoals):
 1. tllist_ord ?b (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs)) (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs)
 2. tllist_ord ?b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))
[PROOF STEP]
thus "tllist_ord b (?lhs xs) (?rhs xs)"
[PROOF STATE]
proof (prove)
using this:
\<forall>xs. tllist_ord b (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs)) (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs)

goal (1 subgoal):
 1. tllist_ord b (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs)) (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
tllist_ord b (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs)) (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs)

goal (1 subgoal):
 1. tllist_ord b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))
[PROOF STEP]
have "\<forall>xs. tllist_ord b (?rhs xs) (?lhs xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. tllist_ord b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))
[PROOF STEP]
by(rule tfilter.fixp_induct[where Pa="\<lambda>f. \<forall>xs. tllist_ord b (f xs) (?lhs xs)"])(auto split: tllist.split)
[PROOF STATE]
proof (state)
this:
\<forall>xs. tllist_ord b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))

goal (1 subgoal):
 1. tllist_ord b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))
[PROOF STEP]
thus "tllist_ord b (?rhs xs) (?lhs xs)"
[PROOF STATE]
proof (prove)
using this:
\<forall>xs. tllist_ord b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))

goal (1 subgoal):
 1. tllist_ord b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
tllist_ord b (TLList_CCPO_Examples.tfilter b (\<lambda>x. P x \<and> Q x) xs) (TLList_CCPO_Examples.tfilter b P (TLList_CCPO_Examples.tfilter b Q xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tset_tfilter: "tset (tfilter b P xs) = {x\<in>tset xs. P x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tset (TLList_CCPO_Examples.tfilter b P xs) = {x \<in> tset xs. P x}
[PROOF STEP]
proof(rule equalityI[OF _ subsetI])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. tset (TLList_CCPO_Examples.tfilter b P xs) \<subseteq> {x \<in> tset xs. P x}
 2. \<And>x. x \<in> {x \<in> tset xs. P x} \<Longrightarrow> x \<in> tset (TLList_CCPO_Examples.tfilter b P xs)
[PROOF STEP]
show "tset (tfilter b P xs) \<subseteq> {x \<in> tset xs. P x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tset (TLList_CCPO_Examples.tfilter b P xs) \<subseteq> {x \<in> tset xs. P x}
[PROOF STEP]
by(induct arbitrary: xs rule: tfilter.fixp_induct)(auto split: tllist.split)
[PROOF STATE]
proof (state)
this:
tset (TLList_CCPO_Examples.tfilter b P xs) \<subseteq> {x \<in> tset xs. P x}

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> tset xs. P x} \<Longrightarrow> x \<in> tset (TLList_CCPO_Examples.tfilter b P xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> tset xs. P x} \<Longrightarrow> x \<in> tset (TLList_CCPO_Examples.tfilter b P xs)
[PROOF STEP]
assume "x \<in> {x \<in> tset xs. P x}"
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> tset xs. P x}

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> tset xs. P x} \<Longrightarrow> x \<in> tset (TLList_CCPO_Examples.tfilter b P xs)
[PROOF STEP]
hence "x \<in> tset xs" "P x"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> tset xs. P x}

goal (1 subgoal):
 1. x \<in> tset xs &&& P x
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
x \<in> tset xs
P x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> tset xs. P x} \<Longrightarrow> x \<in> tset (TLList_CCPO_Examples.tfilter b P xs)
[PROOF STEP]
thus "x \<in> tset (tfilter b P xs)"
[PROOF STATE]
proof (prove)
using this:
x \<in> tset xs
P x

goal (1 subgoal):
 1. x \<in> tset (TLList_CCPO_Examples.tfilter b P xs)
[PROOF STEP]
by(induct rule: tset_induct) simp_all
[PROOF STATE]
proof (state)
this:
x \<in> tset (TLList_CCPO_Examples.tfilter b P xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma below_C: "x \<sqsubseteq> C\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> C\<cdot>x
[PROOF STEP]
by (induct x) auto


[STATEMENT]
lemma C_Cinf[simp]: "C\<cdot>C\<^sup>\<infinity> = C\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<cdot>C\<^sup>\<infinity> = C\<^sup>\<infinity>
[PROOF STEP]
unfolding Cinf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<cdot>(fix\<cdot>C) = fix\<cdot>C
[PROOF STEP]
by (rule fix_eq[symmetric])


[STATEMENT]
lemma C_below_C[simp]: "(C\<^bsup>i\<^esup> \<sqsubseteq> C\<^bsup>j\<^esup>) \<longleftrightarrow> i \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C\<^bsup>i\<^esup> \<sqsubseteq> C\<^bsup>j\<^esup>) = (i \<le> j)
[PROOF STEP]
apply (induction i arbitrary: j)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. (C\<^bsup>0\<^esup> \<sqsubseteq> C\<^bsup>j\<^esup>) = (0 \<le> j)
 2. \<And>i j. (\<And>j. (C\<^bsup>i\<^esup> \<sqsubseteq> C\<^bsup>j\<^esup>) = (i \<le> j)) \<Longrightarrow> (C\<^bsup>Suc i\<^esup> \<sqsubseteq> C\<^bsup>j\<^esup>) = (Suc i \<le> j)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. (\<And>j. (C\<^bsup>i\<^esup> \<sqsubseteq> C\<^bsup>j\<^esup>) = (i \<le> j)) \<Longrightarrow> (C\<^bsup>Suc i\<^esup> \<sqsubseteq> C\<^bsup>j\<^esup>) = (Suc i \<le> j)
[PROOF STEP]
apply (case_tac j, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma below_Cinf[simp]: "r \<sqsubseteq> C\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<sqsubseteq> C\<^sup>\<infinity>
[PROOF STEP]
apply (induct r)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. adm (\<lambda>a. a \<sqsubseteq> C\<^sup>\<infinity>)
 2. \<bottom> \<sqsubseteq> C\<^sup>\<infinity>
 3. \<And>r. r \<sqsubseteq> C\<^sup>\<infinity> \<Longrightarrow> C\<cdot>r \<sqsubseteq> C\<^sup>\<infinity>
[PROOF STEP]
apply simp_all[2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r \<sqsubseteq> C\<^sup>\<infinity> \<Longrightarrow> C\<cdot>r \<sqsubseteq> C\<^sup>\<infinity>
[PROOF STEP]
apply (metis (full_types) C_Cinf monofun_cfun_arg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma C_eq_Cinf[simp]: "C\<^bsup>i\<^esup> \<noteq> C\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^bsup>i\<^esup> \<noteq> C\<^sup>\<infinity>
[PROOF STEP]
by (metis C_below_C Suc_n_not_le_n below_Cinf)


[STATEMENT]
lemma Cinf_eq_C[simp]: "C\<^sup>\<infinity> = C \<cdot> r \<longleftrightarrow> C\<^sup>\<infinity> = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C\<^sup>\<infinity> = C\<cdot>r) = (C\<^sup>\<infinity> = r)
[PROOF STEP]
by (metis C.injects C_Cinf)


[STATEMENT]
lemma C_eq_C[simp]: "(C\<^bsup>i\<^esup> = C\<^bsup>j\<^esup>) \<longleftrightarrow> i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C\<^bsup>i\<^esup> = C\<^bsup>j\<^esup>) = (i = j)
[PROOF STEP]
by (metis C_below_C le_antisym le_refl)


[STATEMENT]
lemma case_of_C_below: "(case r of C\<cdot>y \<Rightarrow> x) \<sqsubseteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case r of C\<cdot>y \<Rightarrow> x) \<sqsubseteq> x
[PROOF STEP]
by (cases r) auto


[STATEMENT]
lemma C_case_below: "C_case \<cdot> f \<sqsubseteq> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C_case\<cdot>f \<sqsubseteq> f
[PROOF STEP]
by (metis cfun_belowI C.case_rews(2) below_C monofun_cfun_arg)


[STATEMENT]
lemma C_case_bot[simp]: "C_case \<cdot> \<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C_case\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
apply (subst eq_bottom_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C_case\<cdot>\<bottom> \<sqsubseteq> \<bottom>
[PROOF STEP]
apply (rule C_case_below)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma C_case_cong:
  assumes "\<And> r'. r = C\<cdot>r' \<Longrightarrow> f\<cdot>r' = g\<cdot>r'"
  shows "C_case\<cdot>f\<cdot>r = C_case\<cdot>g\<cdot>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C_case\<cdot>f\<cdot>r = C_case\<cdot>g\<cdot>r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r = C\<cdot>?r' \<Longrightarrow> f\<cdot>?r' = g\<cdot>?r'

goal (1 subgoal):
 1. C_case\<cdot>f\<cdot>r = C_case\<cdot>g\<cdot>r
[PROOF STEP]
by (cases r) auto


[STATEMENT]
lemma C_cases:
  obtains n where "r = C\<^bsup>n\<^esup>" | "r = C\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "\<exists> n. C_take m \<cdot> r = C\<^bsup>n\<^esup> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. C_take m\<cdot>r = C\<^bsup>n\<^esup>
[PROOF STEP]
proof (rule C.finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. \<bottom> = C\<^bsup>n\<^esup>
 2. \<And>Ca. \<exists>n. Ca = C\<^bsup>n\<^esup> \<Longrightarrow> \<exists>n. C\<cdot>Ca = C\<^bsup>n\<^esup>
[PROOF STEP]
have "\<bottom> = C\<^bsup>0\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> = C\<^bsup>0\<^esup>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bottom> = C\<^bsup>0\<^esup>

goal (2 subgoals):
 1. \<exists>n. \<bottom> = C\<^bsup>n\<^esup>
 2. \<And>Ca. \<exists>n. Ca = C\<^bsup>n\<^esup> \<Longrightarrow> \<exists>n. C\<cdot>Ca = C\<^bsup>n\<^esup>
[PROOF STEP]
thus "\<exists>n. \<bottom> = C\<^bsup>n\<^esup>"
[PROOF STATE]
proof (prove)
using this:
\<bottom> = C\<^bsup>0\<^esup>

goal (1 subgoal):
 1. \<exists>n. \<bottom> = C\<^bsup>n\<^esup>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>n. \<bottom> = C\<^bsup>n\<^esup>

goal (1 subgoal):
 1. \<And>Ca. \<exists>n. Ca = C\<^bsup>n\<^esup> \<Longrightarrow> \<exists>n. C\<cdot>Ca = C\<^bsup>n\<^esup>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ca. \<exists>n. Ca = C\<^bsup>n\<^esup> \<Longrightarrow> \<exists>n. C\<cdot>Ca = C\<^bsup>n\<^esup>
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ca. \<exists>n. Ca = C\<^bsup>n\<^esup> \<Longrightarrow> \<exists>n. C\<cdot>Ca = C\<^bsup>n\<^esup>
[PROOF STEP]
show "\<exists>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> \<exists>n. C\<cdot>r = C\<^bsup>n\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> \<exists>n. C\<cdot>r = C\<^bsup>n\<^esup>
[PROOF STEP]
by (auto simp del: iterate_Suc simp add: iterate_Suc[symmetric])
[PROOF STATE]
proof (state)
this:
\<exists>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> \<exists>n. C\<cdot>r = C\<^bsup>n\<^esup>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n. C_take m\<cdot>r = C\<^bsup>n\<^esup>

goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>n. C_take ?m2\<cdot>r = C\<^bsup>n\<^esup>

goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. C_take ?m2\<cdot>r = C\<^bsup>n\<^esup>
[PROOF STEP]
obtain f where take: "\<And> m. C_take m \<cdot> r = C\<^bsup>f m\<^esup>"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. C_take ?m2\<cdot>r = C\<^bsup>n\<^esup>

goal (1 subgoal):
 1. (\<And>f. (\<And>m. C_take m\<cdot>r = C\<^bsup>f m\<^esup>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
C_take ?m\<cdot>r = C\<^bsup>f ?m\<^esup>

goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "chain (\<lambda> m. C\<^bsup>f m\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain (\<lambda>m. C\<^bsup>f m\<^esup>)
[PROOF STEP]
using ch2ch_Rep_cfunL[OF C.chain_take, where x=r, unfolded take]
[PROOF STATE]
proof (prove)
using this:
chain (\<lambda>i. C\<^bsup>f i\<^esup>)

goal (1 subgoal):
 1. chain (\<lambda>m. C\<^bsup>f m\<^esup>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
chain (\<lambda>m. C\<^bsup>f m\<^esup>)

goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "mono f"
[PROOF STATE]
proof (prove)
using this:
chain (\<lambda>m. C\<^bsup>f m\<^esup>)

goal (1 subgoal):
 1. mono f
[PROOF STEP]
by (auto simp add: mono_iff_le_Suc chain_def elim!:chainE)
[PROOF STATE]
proof (state)
this:
mono f

goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have r: "r = (\<Squnion> m. C\<^bsup>f m\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = (\<Squnion>m. C\<^bsup>f m\<^esup>)
[PROOF STEP]
by (metis (lifting) take C.reach lub_eq)
[PROOF STATE]
proof (state)
this:
r = (\<Squnion>m. C\<^bsup>f m\<^esup>)

goal (1 subgoal):
 1. \<lbrakk>\<And>n. r = C\<^bsup>n\<^esup> \<Longrightarrow> thesis; r = C\<^sup>\<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from \<open>mono f\<close>
[PROOF STATE]
proof (chain)
picking this:
mono f
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
mono f

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof(rule nat_mono_characterization)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. (\<And>m. n \<le> m \<Longrightarrow> f n = f m) \<Longrightarrow> thesis
 2. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. (\<And>m. n \<le> m \<Longrightarrow> f n = f m) \<Longrightarrow> thesis
 2. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
assume n: "\<And> m. n \<le> m ==> f n = f m"
[PROOF STATE]
proof (state)
this:
n \<le> ?m \<Longrightarrow> f n = f ?m

goal (2 subgoals):
 1. \<And>n. (\<And>m. n \<le> m \<Longrightarrow> f n = f m) \<Longrightarrow> thesis
 2. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
have "max_in_chain n (\<lambda> m. C\<^bsup>f m\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_in_chain n (\<lambda>m. C\<^bsup>f m\<^esup>)
[PROOF STEP]
apply (rule max_in_chainI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. n \<le> j \<Longrightarrow> C\<^bsup>f n\<^esup> = C\<^bsup>f j\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. n \<le> j \<Longrightarrow> f n = f j
[PROOF STEP]
apply (erule n)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
max_in_chain n (\<lambda>m. C\<^bsup>f m\<^esup>)

goal (2 subgoals):
 1. \<And>n. (\<And>m. n \<le> m \<Longrightarrow> f n = f m) \<Longrightarrow> thesis
 2. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
hence "(\<Squnion> m. C\<^bsup>f m\<^esup>) = C\<^bsup>f n\<^esup>"
[PROOF STATE]
proof (prove)
using this:
max_in_chain n (\<lambda>m. C\<^bsup>f m\<^esup>)

goal (1 subgoal):
 1. (\<Squnion>m. C\<^bsup>f m\<^esup>) = C\<^bsup>f n\<^esup>
[PROOF STEP]
unfolding  maxinch_is_thelub[OF \<open>chain _\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>i. C\<^bsup>f i\<^esup>) = C\<^bsup>f n\<^esup>

goal (1 subgoal):
 1. (\<Squnion>m. C\<^bsup>f m\<^esup>) = C\<^bsup>f n\<^esup>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Squnion>m. C\<^bsup>f m\<^esup>) = C\<^bsup>f n\<^esup>

goal (2 subgoals):
 1. \<And>n. (\<And>m. n \<le> m \<Longrightarrow> f n = f m) \<Longrightarrow> thesis
 2. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>m. C\<^bsup>f m\<^esup>) = C\<^bsup>f n\<^esup>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>m. C\<^bsup>f m\<^esup>) = C\<^bsup>f n\<^esup>
r = C\<^bsup>?n\<^esup> \<Longrightarrow> thesis
r = C\<^sup>\<infinity> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding r
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>m. C\<^bsup>f m\<^esup>) = C\<^bsup>f n\<^esup>
(\<Squnion>m. C\<^bsup>f m\<^esup>) = C\<^bsup>?n\<^esup> \<Longrightarrow> thesis
(\<Squnion>m. C\<^bsup>f m\<^esup>) = C\<^sup>\<infinity> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
assume "\<And>m. \<exists>n. m \<le> f n"
[PROOF STATE]
proof (state)
this:
\<exists>n. ?m \<le> f n

goal (1 subgoal):
 1. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
hence "\<And> n. C\<^bsup>n\<^esup> \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ?m \<le> f n

goal (1 subgoal):
 1. \<And>n. C\<^bsup>n\<^esup> \<sqsubseteq> r
[PROOF STEP]
unfolding r
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ?m \<le> f n

goal (1 subgoal):
 1. \<And>n. C\<^bsup>n\<^esup> \<sqsubseteq> (\<Squnion>m. C\<^bsup>f m\<^esup>)
[PROOF STEP]
by (fastforce intro: below_lub[OF \<open>chain _\<close>])
[PROOF STATE]
proof (state)
this:
C\<^bsup>?n\<^esup> \<sqsubseteq> r

goal (1 subgoal):
 1. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
hence "(\<Squnion> n. C\<^bsup>n\<^esup>) \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
using this:
C\<^bsup>?n\<^esup> \<sqsubseteq> r

goal (1 subgoal):
 1. (\<Squnion>n. C\<^bsup>n\<^esup>) \<sqsubseteq> r
[PROOF STEP]
by (rule lub_below[OF chain_iterate])
[PROOF STATE]
proof (state)
this:
(\<Squnion>n. C\<^bsup>n\<^esup>) \<sqsubseteq> r

goal (1 subgoal):
 1. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
hence "C\<^sup>\<infinity> \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>n. C\<^bsup>n\<^esup>) \<sqsubseteq> r

goal (1 subgoal):
 1. C\<^sup>\<infinity> \<sqsubseteq> r
[PROOF STEP]
unfolding Cinf_def fix_def2
[PROOF STATE]
proof (prove)
using this:
(\<Squnion>n. C\<^bsup>n\<^esup>) \<sqsubseteq> r

goal (1 subgoal):
 1. (\<Squnion>i. C\<^bsup>i\<^esup>) \<sqsubseteq> r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
C\<^sup>\<infinity> \<sqsubseteq> r

goal (1 subgoal):
 1. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
hence "C\<^sup>\<infinity> = r"
[PROOF STATE]
proof (prove)
using this:
C\<^sup>\<infinity> \<sqsubseteq> r

goal (1 subgoal):
 1. C\<^sup>\<infinity> = r
[PROOF STEP]
using below_Cinf
[PROOF STATE]
proof (prove)
using this:
C\<^sup>\<infinity> \<sqsubseteq> r
?r \<sqsubseteq> C\<^sup>\<infinity>

goal (1 subgoal):
 1. C\<^sup>\<infinity> = r
[PROOF STEP]
by (metis below_antisym)
[PROOF STATE]
proof (state)
this:
C\<^sup>\<infinity> = r

goal (1 subgoal):
 1. (\<And>m. \<exists>n. m \<le> f n) \<Longrightarrow> thesis
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
C\<^sup>\<infinity> = r

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
C\<^sup>\<infinity> = r
r = C\<^bsup>?n\<^esup> \<Longrightarrow> thesis
r = C\<^sup>\<infinity> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma C_case_Cinf[simp]: "C_case \<cdot> f \<cdot> C\<^sup>\<infinity> = f \<cdot> C\<^sup>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C_case\<cdot>f\<cdot>C\<^sup>\<infinity> = f\<cdot>C\<^sup>\<infinity>
[PROOF STEP]
unfolding Cinf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C_case\<cdot>f\<cdot>(fix\<cdot>C) = f\<cdot>(fix\<cdot>C)
[PROOF STEP]
by (subst fix_eq) simp


[STATEMENT]
lemma length_filter_less2:
    assumes "x \<in> set xs" "\<not>P x" "Q x" "\<And>x. P x \<Longrightarrow> Q x"
    shows "length (filter P xs) < length (filter Q xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter P xs) < length (filter Q xs)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (filter P xs) < length (filter Q xs)
[PROOF STEP]
have "\<And>x. (Q x \<and> P x) = P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (Q x \<and> P x) = P x
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
P ?x1 \<Longrightarrow> Q ?x1

goal (1 subgoal):
 1. \<And>x. (Q x \<and> P x) = P x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Q ?x1 \<and> P ?x1) = P ?x1

goal (1 subgoal):
 1. length (filter P xs) < length (filter Q xs)
[PROOF STEP]
hence "filter P xs = filter P (filter Q xs)"
[PROOF STATE]
proof (prove)
using this:
(Q ?x1 \<and> P ?x1) = P ?x1

goal (1 subgoal):
 1. filter P xs = filter P (filter Q xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter P xs = filter P (filter Q xs)

goal (1 subgoal):
 1. length (filter P xs) < length (filter Q xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter P xs = filter P (filter Q xs)

goal (1 subgoal):
 1. length (filter P xs) < length (filter Q xs)
[PROOF STEP]
have "length (...) < length (filter Q xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter P (filter Q xs)) < length (filter Q xs)
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs
\<not> P x
Q x

goal (1 subgoal):
 1. length (filter P (filter Q xs)) < length (filter Q xs)
[PROOF STEP]
by - (rule length_filter_less, auto)
[PROOF STATE]
proof (state)
this:
length (filter P (filter Q xs)) < length (filter Q xs)

goal (1 subgoal):
 1. length (filter P xs) < length (filter Q xs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (filter P xs) < length (filter Q xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (filter P xs) < length (filter Q xs)

goal (1 subgoal):
 1. length (filter P xs) < length (filter Q xs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length (filter P xs) < length (filter Q xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_filter_le2:
    assumes "\<And>x. P x \<Longrightarrow> Q x"
    shows "length (filter P xs) \<le> length (filter Q xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter P xs) \<le> length (filter Q xs)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (filter P xs) \<le> length (filter Q xs)
[PROOF STEP]
have "\<And>x. (Q x \<and> P x) = P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (Q x \<and> P x) = P x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P ?x1 \<Longrightarrow> Q ?x1

goal (1 subgoal):
 1. \<And>x. (Q x \<and> P x) = P x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Q ?x1 \<and> P ?x1) = P ?x1

goal (1 subgoal):
 1. length (filter P xs) \<le> length (filter Q xs)
[PROOF STEP]
hence "filter P xs = filter P (filter Q xs)"
[PROOF STATE]
proof (prove)
using this:
(Q ?x1 \<and> P ?x1) = P ?x1

goal (1 subgoal):
 1. filter P xs = filter P (filter Q xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter P xs = filter P (filter Q xs)

goal (1 subgoal):
 1. length (filter P xs) \<le> length (filter Q xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter P xs = filter P (filter Q xs)

goal (1 subgoal):
 1. length (filter P xs) \<le> length (filter Q xs)
[PROOF STEP]
have "length (...) \<le> length (filter Q xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter P (filter Q xs)) \<le> length (filter Q xs)
[PROOF STEP]
by - (rule length_filter_le)
[PROOF STATE]
proof (state)
this:
length (filter P (filter Q xs)) \<le> length (filter Q xs)

goal (1 subgoal):
 1. length (filter P xs) \<le> length (filter Q xs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length (filter P xs) \<le> length (filter Q xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (filter P xs) \<le> length (filter Q xs)

goal (1 subgoal):
 1. length (filter P xs) \<le> length (filter Q xs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length (filter P xs) \<le> length (filter Q xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phis_measure_update_le: "phis_measure g v (Mapping.update k a p) \<le> phis_measure g v p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phis_measure g v (Mapping.update k a p) \<le> phis_measure g v p
[PROOF STEP]
apply (rule length_filter_le2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Mapping.lookup (Mapping.update k a p) (x, v) = None \<Longrightarrow> Mapping.lookup p (x, v) = None
[PROOF STEP]
apply (case_tac "k = (x, v)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Mapping.lookup (Mapping.update k a p) (x, v) = None; k = (x, v)\<rbrakk> \<Longrightarrow> Mapping.lookup p (x, v) = None
 2. \<And>x. \<lbrakk>Mapping.lookup (Mapping.update k a p) (x, v) = None; k \<noteq> (x, v)\<rbrakk> \<Longrightarrow> Mapping.lookup p (x, v) = None
[PROOF STEP]
apply (auto simp: lookup_update lookup_update_neq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma phis_measure_update_le': "phis_measure g v p \<le> phis_measure g v (Mapping.update k [] phis) \<Longrightarrow>
       phis_measure g v (Mapping.update k a p) \<le> phis_measure g v phis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phis_measure g v p \<le> phis_measure g v (Mapping.update k [] phis) \<Longrightarrow> phis_measure g v (Mapping.update k a p) \<le> phis_measure g v phis
[PROOF STEP]
apply (rule le_trans, rule phis_measure_update_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phis_measure g v p \<le> phis_measure g v (Mapping.update k [] phis) \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
apply (rule le_trans, assumption, rule phis_measure_update_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma readArgs_phis_le:
    "readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)) \<Longrightarrow> (val,p) = readVariableRecursive g v n phis \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis"
    "readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, ms)) \<Longrightarrow> (p,u) = readArgs g v n phis ms \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); (val, p) = readVariableRecursive g v n phis\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis) &&& (\<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, ms)); (p, u) = readArgs g v n phis ms\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis)
[PROOF STEP]
proof (induction arbitrary: val p and p u rule: readVariableRecursive_readArgs.pinduct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>g v n phis val p. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); \<And>x21 x22 val p. \<lbrakk>v \<notin> defs g n; predecessors g n = x21 # x22; x22 = []; (val, p) = readVariableRecursive g v x21 phis\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis; \<And>x21 x22 x21a x22a x p u. \<lbrakk>v \<notin> defs g n; predecessors g n = x21 # x22; x22 = x21a # x22a; Mapping.lookup phis (n, v) = None; x = Mapping.update (n, v) [] phis; (p, u) = readArgs g v n x (x21 # x21a # x22a)\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v x; (val, p) = readVariableRecursive g v n phis\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
 2. \<And>g v n phis p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, [])); (p, u) = readArgs g v n phis []\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
 3. \<And>g v n phis m ms p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, m # ms)); \<And>p u. (p, u) = readArgs g v n phis ms \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis; \<And>x xa y val p. \<lbrakk>x = readArgs g v n phis ms; (xa, y) = x; (val, p) = readVariableRecursive g v m xa\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v xa; (p, u) = readArgs g v n phis (m # ms)\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
case (1 g v n phis)
[PROOF STATE]
proof (state)
this:
readVariableRecursive_readArgs_dom (Inl (g, v, n, phis))
\<lbrakk>v \<notin> defs g n; predecessors g n = ?x21.2 # ?x22.2; ?x22.2 = []; (?val2, ?p2) = readVariableRecursive g v ?x21.2 phis\<rbrakk> \<Longrightarrow> phis_measure g v ?p2 \<le> phis_measure g v phis
\<lbrakk>v \<notin> defs g n; predecessors g n = ?x21.2 # ?x22.2; ?x22.2 = ?x21a2 # ?x22a2; Mapping.lookup phis (n, v) = None; ?x2 = Mapping.update (n, v) [] phis; (?p2, ?u2) = readArgs g v n ?x2 (?x21.2 # ?x21a2 # ?x22a2)\<rbrakk> \<Longrightarrow> phis_measure g v ?p2 \<le> phis_measure g v ?x2
(val, p) = readVariableRecursive g v n phis

goal (3 subgoals):
 1. \<And>g v n phis val p. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); \<And>x21 x22 val p. \<lbrakk>v \<notin> defs g n; predecessors g n = x21 # x22; x22 = []; (val, p) = readVariableRecursive g v x21 phis\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis; \<And>x21 x22 x21a x22a x p u. \<lbrakk>v \<notin> defs g n; predecessors g n = x21 # x22; x22 = x21a # x22a; Mapping.lookup phis (n, v) = None; x = Mapping.update (n, v) [] phis; (p, u) = readArgs g v n x (x21 # x21a # x22a)\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v x; (val, p) = readVariableRecursive g v n phis\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
 2. \<And>g v n phis p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, [])); (p, u) = readArgs g v n phis []\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
 3. \<And>g v n phis m ms p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, m # ms)); \<And>p u. (p, u) = readArgs g v n phis ms \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis; \<And>x xa y val p. \<lbrakk>x = readArgs g v n phis ms; (xa, y) = x; (val, p) = readVariableRecursive g v m xa\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v xa; (p, u) = readArgs g v n phis (m # ms)\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
using "1.IH"(1,2) "1.prems"
[PROOF STATE]
proof (prove)
using this:
readVariableRecursive_readArgs_dom (Inl (g, v, n, phis))
\<lbrakk>v \<notin> defs g n; predecessors g n = ?x21.2 # ?x22.2; ?x22.2 = []; (?val2, ?p2) = readVariableRecursive g v ?x21.2 phis\<rbrakk> \<Longrightarrow> phis_measure g v ?p2 \<le> phis_measure g v phis
(val, p) = readVariableRecursive g v n phis

goal (1 subgoal):
 1. phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
apply (auto simp: readVariableRecursive.psimps Let_def phis_measure_update_le split: if_split_asm list.splits option.splits prod.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> phis_measure g v (Mapping.update (n, v) x2 x1) \<le> phis_measure g v phis
[PROOF STEP]
apply (subgoal_tac "phis_measure g v x1 \<le> phis_measure g v (Mapping.update (n,v) [] phis)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1; phis_measure g v x1 \<le> phis_measure g v (Mapping.update (n, v) [] phis)\<rbrakk> \<Longrightarrow> phis_measure g v (Mapping.update (n, v) x2 x1) \<le> phis_measure g v phis
 2. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> phis_measure g v x1 \<le> phis_measure g v (Mapping.update (n, v) [] phis)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> phis_measure g v x1 \<le> phis_measure g v (Mapping.update (n, v) [] phis)
 2. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1; phis_measure g v x1 \<le> phis_measure g v (Mapping.update (n, v) [] phis)\<rbrakk> \<Longrightarrow> phis_measure g v (Mapping.update (n, v) x2 x1) \<le> phis_measure g v phis
[PROOF STEP]
apply (rule "1.IH"(3))
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> v \<notin> defs g n
 2. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> predecessors g n = ?x21.70 x21 x21a x22a x1 x2 # ?x22.70 x21 x21a x22a x1 x2
 3. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> ?x22.70 x21 x21a x22a x1 x2 = ?x21a70 x21 x21a x22a x1 x2 # ?x22a70 x21 x21a x22a x1 x2
 4. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> Mapping.lookup phis (n, v) = None
 5. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> Mapping.update (n, v) [] phis = Mapping.update (n, v) [] phis
 6. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1\<rbrakk> \<Longrightarrow> (x1, ?u70 x21 x21a x22a x1 x2) = readArgs g v n (Mapping.update (n, v) [] phis) (?x21.70 x21 x21a x22a x1 x2 # ?x21a70 x21 x21a x22a x1 x2 # ?x22a70 x21 x21a x22a x1 x2)
 7. \<And>x21 x21a x22a x1 x2. \<lbrakk>readVariableRecursive_readArgs_dom (Inl (g, v, n, phis)); v \<notin> defs g n; predecessors g n = x21 # x21a # x22a; Mapping.lookup phis (n, v) = None; readArgs g v n (Mapping.update (n, v) [] phis) (x21 # x21a # x22a) = (x1, x2); val = (v, n, PhiDef); p = Mapping.update (n, v) x2 x1; phis_measure g v x1 \<le> phis_measure g v (Mapping.update (n, v) [] phis)\<rbrakk> \<Longrightarrow> phis_measure g v (Mapping.update (n, v) x2 x1) \<le> phis_measure g v phis
[PROOF STEP]
apply (auto simp: phis_measure_update_le')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
phis_measure g v p \<le> phis_measure g v phis

goal (2 subgoals):
 1. \<And>g v n phis p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, [])); (p, u) = readArgs g v n phis []\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
 2. \<And>g v n phis m ms p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, m # ms)); \<And>p u. (p, u) = readArgs g v n phis ms \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis; \<And>x xa y val p. \<lbrakk>x = readArgs g v n phis ms; (xa, y) = x; (val, p) = readVariableRecursive g v m xa\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v xa; (p, u) = readArgs g v n phis (m # ms)\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>g v n phis p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, [])); (p, u) = readArgs g v n phis []\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
 2. \<And>g v n phis m ms p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, m # ms)); \<And>p u. (p, u) = readArgs g v n phis ms \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis; \<And>x xa y val p. \<lbrakk>x = readArgs g v n phis ms; (xa, y) = x; (val, p) = readVariableRecursive g v m xa\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v xa; (p, u) = readArgs g v n phis (m # ms)\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
case (3 g v n m ms phis)
[PROOF STATE]
proof (state)
this:
readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis))
(?p2, ?u2) = readArgs g v n m phis \<Longrightarrow> phis_measure g v ?p2 \<le> phis_measure g v m
\<lbrakk>?x2 = readArgs g v n m phis; (?xa2, ?y2) = ?x2; (?val2, ?p2) = readVariableRecursive g v ms ?xa2\<rbrakk> \<Longrightarrow> phis_measure g v ?p2 \<le> phis_measure g v ?xa2
(p, u) = readArgs g v n m (ms # phis)

goal (2 subgoals):
 1. \<And>g v n phis p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, [])); (p, u) = readArgs g v n phis []\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
 2. \<And>g v n phis m ms p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, m # ms)); \<And>p u. (p, u) = readArgs g v n phis ms \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis; \<And>x xa y val p. \<lbrakk>x = readArgs g v n phis ms; (xa, y) = x; (val, p) = readVariableRecursive g v m xa\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v xa; (p, u) = readArgs g v n phis (m # ms)\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
from "3.IH"(1) "3.prems"
[PROOF STATE]
proof (chain)
picking this:
readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis))
(p, u) = readArgs g v n m (ms # phis)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis))
(p, u) = readArgs g v n m (ms # phis)

goal (1 subgoal):
 1. phis_measure g v p \<le> phis_measure g v m
[PROOF STEP]
apply (auto simp: readArgs.psimps split: prod.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v m
[PROOF STEP]
apply (rule le_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> ?j22 x1 x2 a aa b
 2. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> ?j22 x1 x2 a aa b \<le> phis_measure g v m
[PROOF STEP]
apply (rule "3.IH"(3))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> ?x27 x1 x2 a aa b = readArgs g v n m phis
 2. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> (?xa27 x1 x2 a aa b, ?y27 x1 x2 a aa b) = ?x27 x1 x2 a aa b
 3. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> (?val27 x1 x2 a aa b, p) = readVariableRecursive g v ms (?xa27 x1 x2 a aa b)
 4. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> phis_measure g v (?xa27 x1 x2 a aa b) \<le> phis_measure g v m
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> phis_measure g v x1 \<le> phis_measure g v m
[PROOF STEP]
apply (rule "3.IH"(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a aa b. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, m, ms # phis)); readArgs g v n m phis = (x1, x2); readVariableRecursive g v ms x1 = ((a, aa, b), p); u = (a, aa, b) # x2\<rbrakk> \<Longrightarrow> (x1, ?u40 x1 x2 a aa b) = readArgs g v n m phis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
phis_measure g v p \<le> phis_measure g v m

goal (1 subgoal):
 1. \<And>g v n phis p u. \<lbrakk>readVariableRecursive_readArgs_dom (Inr (g, v, n, phis, [])); (p, u) = readArgs g v n phis []\<rbrakk> \<Longrightarrow> phis_measure g v p \<le> phis_measure g v phis
[PROOF STEP]
qed (auto simp: readArgs.psimps split: prod.splits)


[STATEMENT]
lemma fst_readVariableRecursive:
    assumes "n \<in> set (\<alpha>n g)"
    shows "fst (readVariableRecursive g v n phis) = lookupDef g n v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (readVariableRecursive g v n phis) = lookupDef g n v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<in> set (\<alpha>n g)

goal (1 subgoal):
 1. fst (readVariableRecursive g v n phis) = lookupDef g n v
[PROOF STEP]
apply (induction rule: lookupDef_induct[where v=v])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>n \<in> set (\<alpha>n g); v \<in> defs g n; lookupDef g n v = (v, n, SimpleDef)\<rbrakk> \<Longrightarrow> fst (readVariableRecursive g v n phis) = lookupDef g n v
 2. \<And>n. \<lbrakk>n \<in> set (\<alpha>n g); v \<notin> defs g n; length (predecessors g n) \<noteq> 1; lookupDef g n v = (v, n, PhiDef)\<rbrakk> \<Longrightarrow> fst (readVariableRecursive g v n phis) = lookupDef g n v
 3. \<And>n m. \<lbrakk>v \<notin> defs g n; predecessors g n = [m]; m \<in> set (\<alpha>n g); lookupDef g n v = lookupDef g m v; fst (readVariableRecursive g v m phis) = lookupDef g m v\<rbrakk> \<Longrightarrow> fst (readVariableRecursive g v n phis) = lookupDef g n v
[PROOF STEP]
apply (simp add: readVariableRecursive.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n \<in> set (\<alpha>n g); v \<notin> defs g n; length (predecessors g n) \<noteq> 1; lookupDef g n v = (v, n, PhiDef)\<rbrakk> \<Longrightarrow> fst (readVariableRecursive g v n phis) = lookupDef g n v
 2. \<And>n m. \<lbrakk>v \<notin> defs g n; predecessors g n = [m]; m \<in> set (\<alpha>n g); lookupDef g n v = lookupDef g m v; fst (readVariableRecursive g v m phis) = lookupDef g m v\<rbrakk> \<Longrightarrow> fst (readVariableRecursive g v n phis) = lookupDef g n v
[PROOF STEP]
apply (simp add: readVariableRecursive.simps; auto simp: split_def Let_def split: list.split option.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>v \<notin> defs g n; predecessors g n = [m]; m \<in> set (\<alpha>n g); lookupDef g n v = lookupDef g m v; fst (readVariableRecursive g v m phis) = lookupDef g m v\<rbrakk> \<Longrightarrow> fst (readVariableRecursive g v n phis) = lookupDef g n v
[PROOF STEP]
apply (auto simp add: readVariableRecursive.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma phis'_aux_keys_super: "Mapping.keys (phis'_aux g v ns phis) \<supseteq> Mapping.keys phis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mapping.keys phis \<subseteq> Mapping.keys (phis'_aux g v ns phis)
[PROOF STEP]
by (auto simp: keys_dom_lookup phis'_aux_def)


[STATEMENT]
lemma phiDefNodes_aux_in_unvisited:
    shows "phiDefNodes_aux g v un n \<subseteq> set un"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phiDefNodes_aux g v un n \<subseteq> set un
[PROOF STEP]
proof (induction un arbitrary: n rule:removeAll_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n. (\<And>x n. x \<in> set xs \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> set (removeAll x xs)) \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> set xs
[PROOF STEP]
case (1 un)
[PROOF STATE]
proof (state)
this:
?x2 \<in> set un \<Longrightarrow> phiDefNodes_aux g v (removeAll ?x2 un) ?n2 \<subseteq> set (removeAll ?x2 un)

goal (1 subgoal):
 1. \<And>xs n. (\<And>x n. x \<in> set xs \<Longrightarrow> phiDefNodes_aux g v (removeAll x xs) n \<subseteq> set (removeAll x xs)) \<Longrightarrow> phiDefNodes_aux g v xs n \<subseteq> set xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phiDefNodes_aux g v un n \<subseteq> set un
[PROOF STEP]
apply (simp only: phiDefNodes_aux.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if n \<notin> set un \<or> v \<in> defs g n then {} else fold (\<union>) (map (phiDefNodes_aux g v (removeAll n un)) (predecessors g n)) (if length (predecessors g n) \<noteq> 1 then {n} else {})) \<subseteq> set un
[PROOF STEP]
apply (auto elim!: fold_union_elem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>length (predecessors g n) = Suc 0; x \<in> phiDefNodes_aux g v (removeAll n un) xa; n \<in> set un; v \<notin> defs g n; xa \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> x \<in> set un
 2. \<And>x xa. \<lbrakk>length (predecessors g n) \<noteq> Suc 0; x \<in> phiDefNodes_aux g v (removeAll n un) xa; n \<in> set un; v \<notin> defs g n; xa \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> x \<in> set un
[PROOF STEP]
apply (rename_tac m n')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n'. \<lbrakk>length (predecessors g n) = Suc 0; m \<in> phiDefNodes_aux g v (removeAll n un) n'; n \<in> set un; v \<notin> defs g n; n' \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> m \<in> set un
 2. \<And>x xa. \<lbrakk>length (predecessors g n) \<noteq> Suc 0; x \<in> phiDefNodes_aux g v (removeAll n un) xa; n \<in> set un; v \<notin> defs g n; xa \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> x \<in> set un
[PROOF STEP]
apply (drule_tac x2=n and n2=n' in 1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n'. \<lbrakk>length (predecessors g n) = Suc 0; m \<in> phiDefNodes_aux g v (removeAll n un) n'; v \<notin> defs g n; n' \<in> set (predecessors g n); phiDefNodes_aux g v (removeAll n un) n' \<subseteq> set (removeAll n un)\<rbrakk> \<Longrightarrow> m \<in> set un
 2. \<And>x xa. \<lbrakk>length (predecessors g n) \<noteq> Suc 0; x \<in> phiDefNodes_aux g v (removeAll n un) xa; n \<in> set un; v \<notin> defs g n; xa \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> x \<in> set un
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>length (predecessors g n) \<noteq> Suc 0; x \<in> phiDefNodes_aux g v (removeAll n un) xa; n \<in> set un; v \<notin> defs g n; xa \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> x \<in> set un
[PROOF STEP]
apply (rename_tac m n')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n'. \<lbrakk>length (predecessors g n) \<noteq> Suc 0; m \<in> phiDefNodes_aux g v (removeAll n un) n'; n \<in> set un; v \<notin> defs g n; n' \<in> set (predecessors g n)\<rbrakk> \<Longrightarrow> m \<in> set un
[PROOF STEP]
apply (drule_tac x2=n and n2=n' in 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n'. \<lbrakk>length (predecessors g n) \<noteq> Suc 0; m \<in> phiDefNodes_aux g v (removeAll n un) n'; v \<notin> defs g n; n' \<in> set (predecessors g n); phiDefNodes_aux g v (removeAll n un) n' \<subseteq> set (removeAll n un)\<rbrakk> \<Longrightarrow> m \<in> set un
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
phiDefNodes_aux g v un n \<subseteq> set un

goal:
No subgoals!
[PROOF STEP]
qed