[STATEMENT]
lemma max_getIJ_coreProperties:
  assumes "card V \<ge> 2"
  assumes "(I, J) = max_getIJ Q_pos Q_neg V"
  shows "card I \<ge> 1 \<and> card J \<ge> 1 \<and> V = I \<union> J \<and> I \<inter> J = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
have "finite V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite V
[PROOF STEP]
using assms(1) card.infinite
[PROOF STATE]
proof (prove)
using this:
2 \<le> card V
infinite ?A \<Longrightarrow> card ?A = 0

goal (1 subgoal):
 1. finite V
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite V

goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
define l where "l = sorted_list_of_set V"
[PROOF STATE]
proof (state)
this:
l = sorted_list_of_set V

goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = sorted_list_of_set V
[PROOF STEP]
have "length l \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
l = sorted_list_of_set V

goal (1 subgoal):
 1. 1 \<le> length l
[PROOF STEP]
by (metis Suc_1 Suc_le_lessD \<open>finite V\<close> assms(1) distinct_card
        distinct_sorted_list_of_set less_imp_le set_sorted_list_of_set)
[PROOF STATE]
proof (state)
this:
1 \<le> length l

goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
proof (cases "Set.is_empty Q_neg")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
 2. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Set.is_empty Q_neg

goal (2 subgoals):
 1. Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
 2. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
define x where "x = arg_max_list (score Q_pos) l"
[PROOF STATE]
proof (state)
this:
x = arg_max_list (score Q_pos) l

goal (2 subgoals):
 1. Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
 2. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = arg_max_list (score Q_pos) l
[PROOF STEP]
have "x \<in> (set l)"
[PROOF STATE]
proof (prove)
using this:
x = arg_max_list (score Q_pos) l

goal (1 subgoal):
 1. x \<in> set l
[PROOF STEP]
using \<open>1 \<le> length l\<close> arg_max_list_element
[PROOF STATE]
proof (prove)
using this:
x = arg_max_list (score Q_pos) l
1 \<le> length l
1 \<le> length ?l \<Longrightarrow> arg_max_list ?f ?l \<in> set ?l

goal (1 subgoal):
 1. x \<in> set l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> set l

goal (2 subgoals):
 1. Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
 2. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set l
[PROOF STEP]
have "x \<in> V"
[PROOF STATE]
proof (prove)
using this:
x \<in> set l

goal (1 subgoal):
 1. x \<in> V
[PROOF STEP]
by (simp add: \<open>finite V\<close> l_def)
[PROOF STATE]
proof (state)
this:
x \<in> V

goal (2 subgoals):
 1. Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
 2. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> V

goal (2 subgoals):
 1. Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
 2. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
have "(I, J) = ({x}, V - {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I, J) = ({x}, V - {x})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (I, J) = ({x}, V - {x})
[PROOF STEP]
have "(I, J) =  (let l = sorted_list_of_set V in
    let x = arg_max_list (score Q_pos) l in
    ({x}, V - {x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I, J) = (let l = sorted_list_of_set V; x = arg_max_list (score Q_pos) l in ({x}, V - {x}))
[PROOF STEP]
by (simp add: True assms(2))
[PROOF STATE]
proof (state)
this:
(I, J) = (let l = sorted_list_of_set V; x = arg_max_list (score Q_pos) l in ({x}, V - {x}))

goal (1 subgoal):
 1. (I, J) = ({x}, V - {x})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(I, J) = (let l = sorted_list_of_set V; x = arg_max_list (score Q_pos) l in ({x}, V - {x}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(I, J) = (let l = sorted_list_of_set V; x = arg_max_list (score Q_pos) l in ({x}, V - {x}))

goal (1 subgoal):
 1. (I, J) = ({x}, V - {x})
[PROOF STEP]
by (metis l_def x_def)
[PROOF STATE]
proof (state)
this:
(I, J) = ({x}, V - {x})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(I, J) = ({x}, V - {x})

goal (2 subgoals):
 1. Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
 2. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(I, J) = ({x}, V - {x})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(I, J) = ({x}, V - {x})

goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
using Pair_inject \<open>finite V\<close> assms(1) calculation
[PROOF STATE]
proof (prove)
using this:
(I, J) = ({x}, V - {x})
\<lbrakk>(?a, ?b) = (?a', ?b'); \<lbrakk>?a = ?a'; ?b = ?b'\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R
finite V
2 \<le> card V
x \<in> V

goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}

goal (1 subgoal):
 1. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Set.is_empty Q_neg

goal (1 subgoal):
 1. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
define x where "x = arg_max_list (score Q_neg) l"
[PROOF STATE]
proof (state)
this:
x = arg_max_list (score Q_neg) l

goal (1 subgoal):
 1. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = arg_max_list (score Q_neg) l
[PROOF STEP]
have "x \<in> (set l)"
[PROOF STATE]
proof (prove)
using this:
x = arg_max_list (score Q_neg) l

goal (1 subgoal):
 1. x \<in> set l
[PROOF STEP]
using \<open>1 \<le> length l\<close> arg_max_list_element
[PROOF STATE]
proof (prove)
using this:
x = arg_max_list (score Q_neg) l
1 \<le> length l
1 \<le> length ?l \<Longrightarrow> arg_max_list ?f ?l \<in> set ?l

goal (1 subgoal):
 1. x \<in> set l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> set l

goal (1 subgoal):
 1. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set l
[PROOF STEP]
have "x \<in> V"
[PROOF STATE]
proof (prove)
using this:
x \<in> set l

goal (1 subgoal):
 1. x \<in> V
[PROOF STEP]
by (simp add: \<open>finite V\<close> l_def)
[PROOF STATE]
proof (state)
this:
x \<in> V

goal (1 subgoal):
 1. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> V

goal (1 subgoal):
 1. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
have "(I, J) = (V - {x}, {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I, J) = (V - {x}, {x})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (I, J) = (V - {x}, {x})
[PROOF STEP]
have "(I, J) = (let l = sorted_list_of_set V in
  let x = arg_max_list (score Q_neg) l in (V - {x}, {x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (I, J) = (let l = sorted_list_of_set V; x = arg_max_list (score Q_neg) l in (V - {x}, {x}))
[PROOF STEP]
by (simp add: False assms(2))
[PROOF STATE]
proof (state)
this:
(I, J) = (let l = sorted_list_of_set V; x = arg_max_list (score Q_neg) l in (V - {x}, {x}))

goal (1 subgoal):
 1. (I, J) = (V - {x}, {x})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(I, J) = (let l = sorted_list_of_set V; x = arg_max_list (score Q_neg) l in (V - {x}, {x}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(I, J) = (let l = sorted_list_of_set V; x = arg_max_list (score Q_neg) l in (V - {x}, {x}))

goal (1 subgoal):
 1. (I, J) = (V - {x}, {x})
[PROOF STEP]
by (metis l_def x_def)
[PROOF STATE]
proof (state)
this:
(I, J) = (V - {x}, {x})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(I, J) = (V - {x}, {x})

goal (1 subgoal):
 1. \<not> Set.is_empty Q_neg \<Longrightarrow> 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(I, J) = (V - {x}, {x})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(I, J) = (V - {x}, {x})

goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
using Pair_inject \<open>finite V\<close> assms(1) calculation
[PROOF STATE]
proof (prove)
using this:
(I, J) = (V - {x}, {x})
\<lbrakk>(?a, ?b) = (?a', ?b'); \<lbrakk>?a = ?a'; ?b = ?b'\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R
finite V
2 \<le> card V
x \<in> V

goal (1 subgoal):
 1. 1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 \<le> card I \<and> 1 \<le> card J \<and> V = I \<union> J \<and> I \<inter> J = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_monom_x_x [simp]: "var_monom x * var_monom x \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var_monom x * var_monom x \<noteq> 1
[PROOF STEP]
by (unfold eq_monom_sum_var, auto simp: sum_var_monom_mult sum_var_monom_var)


[STATEMENT]
lemma monom_list_x_x[simp]: "monom_list (var_monom x * var_monom x) = [(x,2)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_list (var_monom x * var_monom x) = [(x, 2)]
[PROOF STEP]
by (transfer, auto simp: monom_mult_list.simps)


[STATEMENT]
lemma assumes b: "b + a > 0" and a: "(a :: int) \<ge> 0"
  shows "check_poly_strict_mono_discrete (>) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
note [simp] = poly_add.simps poly_mult.simps monom_mult_poly.simps zero_poly_def one_poly_def
    extract_def check_poly_strict_mono_discrete_def poly_subst.simps monom_subst_def poly_power.simps
    check_poly_gt_def poly_split_def check_poly_ge.simps
[PROOF STATE]
proof (state)
this:
poly_add [] ?q = ?q
poly_add ((?m, ?c) # ?p) ?q = (case List.extract (\<lambda>mc. fst mc = ?m) ?q of None \<Rightarrow> (?m, ?c) # poly_add ?p ?q | Some (q1, (x, d), q2) \<Rightarrow> if ?c + d = (0::?'a) then poly_add ?p (q1 @ q2) else (?m, ?c + d) # poly_add ?p (q1 @ q2))
poly_mult [] ?q = []
poly_mult (?mc # ?p) ?q = poly_add (monom_mult_poly ?mc ?q) (poly_mult ?p ?q)
monom_mult_poly ?uu [] = []
monom_mult_poly (?m, ?c) ((?m', ?d) # ?p) = (if ?c * ?d = (0::?'a) then monom_mult_poly (?m, ?c) ?p else (?m * ?m', ?c * ?d) # monom_mult_poly (?m, ?c) ?p)
zero_poly \<equiv> []
one_poly \<equiv> [(1, 1::?'a)]
List.extract ?P ?xs = (case dropWhile (Not \<circ> ?P) ?xs of [] \<Rightarrow> None | y # ys \<Rightarrow> Some (takeWhile (Not \<circ> ?P) ?xs, y, ys))
check_poly_strict_mono_discrete ?gt ?p ?v \<equiv> check_poly_gt ?gt (poly_subst (\<lambda>w. poly_of (if w = ?v then PSum [PNum (1::?'a), PVar ?v] else PVar w)) ?p) ?p
poly_subst ?\<sigma> [] = zero_poly
poly_subst ?\<sigma> ((?m, ?c) # ?p) = poly_add (poly_mult [(1, ?c)] (monom_subst ?\<sigma> ?m)) (poly_subst ?\<sigma> ?p)
monom_subst ?\<sigma> ?m = monom_list_subst ?\<sigma> (monom_list ?m)
poly_power ?uu 0 = one_poly
poly_power ?p (Suc ?n) = poly_mult ?p (poly_power ?p ?n)
check_poly_gt ?gt ?p ?q \<equiv> let (a1, p1) = poly_split 1 ?p; (b1, q1) = poly_split 1 ?q in ?gt a1 b1 \<and> check_poly_ge p1 q1
poly_split ?m ?p \<equiv> case List.extract (\<lambda>(n, uu_). ?m = n) ?p of None \<Rightarrow> (0::?'a, ?p) | Some (p1, (x, c), p2) \<Rightarrow> (c, p1 @ p2)
check_poly_ge [] ?q = list_all (\<lambda>(uu_, d). d \<le> (0::?'a)) ?q
check_poly_ge ((?m, ?c) # ?p) ?q = (case List.extract (\<lambda>nd. fst nd = ?m) ?q of None \<Rightarrow> (0::?'a) \<le> ?c \<and> check_poly_ge ?p ?q | Some (q1, (x, d), q2) \<Rightarrow> d \<le> ?c \<and> check_poly_ge ?p (q1 @ q2))

goal (1 subgoal):
 1. check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
proof (cases "a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
 2. a \<noteq> 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = 0

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
 2. a \<noteq> 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
0 < b + a
a = 0
[PROOF STEP]
have b: "b > 0 \<and> b \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < b + a
a = 0

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

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
 2. a \<noteq> 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
using b True
[PROOF STATE]
proof (prove)
using this:
0 < b \<and> b \<noteq> 0
a = 0

goal (1 subgoal):
 1. check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> 0

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
have [simp]: "2 = Suc (Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 = Suc (Suc 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 = Suc (Suc 0)

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
using False a b
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
0 \<le> a
0 < b + a

goal (1 subgoal):
 1. check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
check_poly_strict_mono_discrete (\<lambda>x y. y < x) (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma assumes b: "b + a \<ge> 0" and a: "(a :: int) \<ge> 0"
  shows "check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
note [simp] = poly_add.simps poly_mult.simps monom_mult_poly.simps zero_poly_def one_poly_def
    extract_def check_poly_weak_mono_discrete_def poly_subst.simps monom_subst_def poly_power.simps
    check_poly_gt_def poly_split_def check_poly_ge.simps
[PROOF STATE]
proof (state)
this:
poly_add [] ?q = ?q
poly_add ((?m, ?c) # ?p) ?q = (case List.extract (\<lambda>mc. fst mc = ?m) ?q of None \<Rightarrow> (?m, ?c) # poly_add ?p ?q | Some (q1, (x, d), q2) \<Rightarrow> if ?c + d = (0::?'a) then poly_add ?p (q1 @ q2) else (?m, ?c + d) # poly_add ?p (q1 @ q2))
poly_mult [] ?q = []
poly_mult (?mc # ?p) ?q = poly_add (monom_mult_poly ?mc ?q) (poly_mult ?p ?q)
monom_mult_poly ?uu [] = []
monom_mult_poly (?m, ?c) ((?m', ?d) # ?p) = (if ?c * ?d = (0::?'a) then monom_mult_poly (?m, ?c) ?p else (?m * ?m', ?c * ?d) # monom_mult_poly (?m, ?c) ?p)
zero_poly \<equiv> []
one_poly \<equiv> [(1, 1::?'a)]
List.extract ?P ?xs = (case dropWhile (Not \<circ> ?P) ?xs of [] \<Rightarrow> None | y # ys \<Rightarrow> Some (takeWhile (Not \<circ> ?P) ?xs, y, ys))
check_poly_weak_mono_discrete ?p ?v \<equiv> check_poly_ge (poly_subst (\<lambda>w. poly_of (if w = ?v then PSum [PNum (1::?'a), PVar ?v] else PVar w)) ?p) ?p
poly_subst ?\<sigma> [] = zero_poly
poly_subst ?\<sigma> ((?m, ?c) # ?p) = poly_add (poly_mult [(1, ?c)] (monom_subst ?\<sigma> ?m)) (poly_subst ?\<sigma> ?p)
monom_subst ?\<sigma> ?m = monom_list_subst ?\<sigma> (monom_list ?m)
poly_power ?uu 0 = one_poly
poly_power ?p (Suc ?n) = poly_mult ?p (poly_power ?p ?n)
check_poly_gt ?gt ?p ?q \<equiv> let (a1, p1) = poly_split 1 ?p; (b1, q1) = poly_split 1 ?q in ?gt a1 b1 \<and> check_poly_ge p1 q1
poly_split ?m ?p \<equiv> case List.extract (\<lambda>(n, uu_). ?m = n) ?p of None \<Rightarrow> (0::?'a, ?p) | Some (p1, (x, c), p2) \<Rightarrow> (c, p1 @ p2)
check_poly_ge [] ?q = list_all (\<lambda>(uu_, d). d \<le> (0::?'a)) ?q
check_poly_ge ((?m, ?c) # ?p) ?q = (case List.extract (\<lambda>nd. fst nd = ?m) ?q of None \<Rightarrow> (0::?'a) \<le> ?c \<and> check_poly_ge ?p ?q | Some (q1, (x, d), q2) \<Rightarrow> d \<le> ?c \<and> check_poly_ge ?p (q1 @ q2))

goal (1 subgoal):
 1. check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
proof (cases "a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
 2. a \<noteq> 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = 0

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
 2. a \<noteq> 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
0 \<le> b + a
a = 0
[PROOF STEP]
have b: "0 \<le> b"
[PROOF STATE]
proof (prove)
using this:
0 \<le> b + a
a = 0

goal (1 subgoal):
 1. 0 \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> b

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
 2. a \<noteq> 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
using b True
[PROOF STATE]
proof (prove)
using this:
0 \<le> b
a = 0

goal (1 subgoal):
 1. check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> 0

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
have [simp]: "2 = Suc (Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 = Suc (Suc 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 = Suc (Suc 0)

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
using False a b
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
0 \<le> a
0 \<le> b + a

goal (1 subgoal):
 1. check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
check_poly_weak_mono_discrete (poly_of (PSum [PNum c, PMult [PNum b, PVar x], PMult [PNum a, PVar x, PVar x]])) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongE:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   \<sigma> :: "(name list \<times> 'a list) list"

  assumes "P \<doteq>\<^sub>c Q"
  "wellFormedSubst \<sigma>"

  shows "\<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. \<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]
[PROOF STEP]
by(auto simp add: weakCongruence_def)


[STATEMENT]
lemma weakCongI[case_names cWeakPsiCong]:
  fixes P   :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes "\<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]"

  shows "P \<doteq>\<^sub>c Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<doteq>\<^sub>c Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellFormedSubst ?\<sigma> \<Longrightarrow> ?\<Psi> \<rhd> P[<?\<sigma>>] \<doteq> Q[<?\<sigma>>]

goal (1 subgoal):
 1. P \<doteq>\<^sub>c Q
[PROOF STEP]
by(auto simp add: weakCongruence_def)


[STATEMENT]
lemma weakCongClosed:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   p :: "name prm"

  assumes "P \<doteq>\<^sub>c Q"

  shows "(p \<bullet> P) \<doteq>\<^sub>c (p \<bullet> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> P \<doteq>\<^sub>c p \<bullet> Q
[PROOF STEP]
proof(induct rule: weakCongI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>] \<doteq> p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
case(cWeakPsiCong \<Psi> \<sigma>)
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>] \<doteq> p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
note \<open>P \<doteq>\<^sub>c Q\<close>
[PROOF STATE]
proof (state)
this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>] \<doteq> p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>] \<doteq> p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
from \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellFormedSubst \<sigma>
[PROOF STEP]
have "wellFormedSubst (rev p \<bullet> \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. wellFormedSubst (rev p \<bullet> \<sigma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wellFormedSubst (rev p \<bullet> \<sigma>)

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>] \<doteq> p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<doteq>\<^sub>c Q
wellFormedSubst (rev p \<bullet> \<sigma>)
[PROOF STEP]
have "((rev p) \<bullet> \<Psi>) \<rhd> P[<(rev p \<bullet> \<sigma>)>] \<doteq>  Q[<(rev p \<bullet> \<sigma>)>]"
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q
wellFormedSubst (rev p \<bullet> \<sigma>)

goal (1 subgoal):
 1. rev p \<bullet> \<Psi> \<rhd> P[<rev p \<bullet> \<sigma>>] \<doteq> Q[<rev p \<bullet> \<sigma>>]
[PROOF STEP]
by(rule weakCongE)
[PROOF STATE]
proof (state)
this:
rev p \<bullet> \<Psi> \<rhd> P[<rev p \<bullet> \<sigma>>] \<doteq> Q[<rev p \<bullet> \<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>] \<doteq> p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
rev p \<bullet> \<Psi> \<rhd> P[<rev p \<bullet> \<sigma>>] \<doteq> Q[<rev p \<bullet> \<sigma>>]

goal (1 subgoal):
 1. \<Psi> \<rhd> p \<bullet> P[<\<sigma>>] \<doteq> p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
by(drule_tac p=p in weakPsiCongClosed) (simp add: eqvts)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> p \<bullet> P[<\<sigma>>] \<doteq> p \<bullet> Q[<\<sigma>>]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongReflexive:
  fixes \<Psi>  :: 'b
  and   P  :: "('a, 'b, 'c) psi"

  shows "P \<doteq>\<^sub>c P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<doteq>\<^sub>c P
[PROOF STEP]
by(auto intro: weakCongI weakPsiCongReflexive)


[STATEMENT]
lemma weakCongSym:
  fixes \<Psi>  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   Q  :: "('a, 'b, 'c) psi"

  assumes "P \<doteq>\<^sub>c Q"

  shows "Q \<doteq>\<^sub>c P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<doteq>\<^sub>c P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. Q \<doteq>\<^sub>c P
[PROOF STEP]
by(auto simp add: weakCongruence_def weakPsiCongSym)


[STATEMENT]
lemma weakCongTransitive:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<doteq> Q"
  and     "\<Psi> \<rhd> Q \<doteq> R"

  shows "\<Psi> \<rhd> P \<doteq> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<doteq> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<doteq> Q
\<Psi> \<rhd> Q \<doteq> R

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<doteq> R
[PROOF STEP]
by(auto intro: weakCongI weakPsiCongTransitive dest: weakCongE)


[STATEMENT]
lemma weakCongWeakBisim:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "P \<doteq>\<^sub>c Q"

  shows "\<Psi> \<rhd> P \<approx> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<approx> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<approx> Q
[PROOF STEP]
apply(drule_tac \<sigma>="[]" in weakCongE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wellFormedSubst []
 2. ?\<Psi>1 \<rhd> P[<[]>] \<doteq> Q[<[]>] \<Longrightarrow> \<Psi> \<rhd> P \<approx> Q
[PROOF STEP]
by(auto dest: weakPsiCongE)


[STATEMENT]
lemma weakCongWeakPsiCong:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "P \<doteq>\<^sub>c Q"

  shows "\<Psi> \<rhd> P \<doteq> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<doteq> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<doteq> Q
[PROOF STEP]
by(drule_tac weakCongE[where \<Psi>=\<Psi> and \<sigma>="[]"]) auto


[STATEMENT]
lemma strongBisimWeakCong:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "P \<sim>\<^sub>s Q"

  shows "P \<doteq>\<^sub>c Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<doteq>\<^sub>c Q
[PROOF STEP]
proof(induct rule: weakCongI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]
[PROOF STEP]
case(cWeakPsiCong \<Psi> \<sigma>)
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]
[PROOF STEP]
from assms \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<sim>\<^sub>s Q
wellFormedSubst \<sigma>
[PROOF STEP]
have "P[<\<sigma>>] \<sim> Q[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
P \<sim>\<^sub>s Q
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. P[<\<sigma>>] \<sim> Q[<\<sigma>>]
[PROOF STEP]
by(rule closeSubstE)
[PROOF STATE]
proof (state)
this:
P[<\<sigma>>] \<sim> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]
[PROOF STEP]
hence "\<Psi> \<rhd> P[<\<sigma>>] \<sim> Q[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
P[<\<sigma>>] \<sim> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<Psi> \<rhd> P[<\<sigma>>] \<sim> Q[<\<sigma>>]
[PROOF STEP]
by(metis bisimE(3) statEqBisim Identity Commutativity)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P[<\<sigma>>] \<sim> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P[<\<sigma>>] \<sim> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]
[PROOF STEP]
by(rule strongBisimWeakPsiCong)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P[<\<sigma>>] \<doteq> Q[<\<sigma>>]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma structCongWeakCong:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "P \<equiv>\<^sub>s Q"

  shows "P \<doteq>\<^sub>c Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<doteq>\<^sub>c Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<equiv>\<^sub>s Q

goal (1 subgoal):
 1. P \<doteq>\<^sub>c Q
[PROOF STEP]
by(metis strongBisimWeakCong structCongBisimSubst)


[STATEMENT]
lemma weakCongUnfold:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   \<sigma> :: "(name list \<times> 'a list) list"

  assumes "P \<doteq>\<^sub>c Q"
  and     "wellFormedSubst \<sigma>"

  shows "P[<\<sigma>>] \<doteq>\<^sub>c Q[<\<sigma>>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P[<\<sigma>>] \<doteq>\<^sub>c Q[<\<sigma>>]
[PROOF STEP]
proof(induct rule: weakCongI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>][<\<sigma>'>] \<doteq> Q[<\<sigma>>][<\<sigma>'>]
[PROOF STEP]
case(cWeakPsiCong \<Psi> \<sigma>')
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>'

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>][<\<sigma>'>] \<doteq> Q[<\<sigma>>][<\<sigma>'>]
[PROOF STEP]
with \<open>wellFormedSubst \<sigma>\<close> \<open>wellFormedSubst \<sigma>'\<close>
[PROOF STATE]
proof (chain)
picking this:
wellFormedSubst \<sigma>
wellFormedSubst \<sigma>'
wellFormedSubst \<sigma>'
[PROOF STEP]
have "wellFormedSubst(\<sigma>@\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
wellFormedSubst \<sigma>
wellFormedSubst \<sigma>'
wellFormedSubst \<sigma>'

goal (1 subgoal):
 1. wellFormedSubst (\<sigma> @ \<sigma>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wellFormedSubst (\<sigma> @ \<sigma>')

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>][<\<sigma>'>] \<doteq> Q[<\<sigma>>][<\<sigma>'>]
[PROOF STEP]
with \<open>P \<doteq>\<^sub>c Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<doteq>\<^sub>c Q
wellFormedSubst (\<sigma> @ \<sigma>')
[PROOF STEP]
have "\<Psi> \<rhd> P[<(\<sigma>@\<sigma>')>] \<doteq> Q[<(\<sigma>@\<sigma>')>]"
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q
wellFormedSubst (\<sigma> @ \<sigma>')

goal (1 subgoal):
 1. \<Psi> \<rhd> P[<(\<sigma> @ \<sigma>')>] \<doteq> Q[<(\<sigma> @ \<sigma>')>]
[PROOF STEP]
by(rule weakCongE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P[<(\<sigma> @ \<sigma>')>] \<doteq> Q[<(\<sigma> @ \<sigma>')>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> \<Psi> \<rhd> P[<\<sigma>>][<\<sigma>'>] \<doteq> Q[<\<sigma>>][<\<sigma>'>]
[PROOF STEP]
thus "\<Psi> \<rhd> P[<\<sigma>>][<\<sigma>'>] \<doteq> Q[<\<sigma>>][<\<sigma>'>]"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P[<(\<sigma> @ \<sigma>')>] \<doteq> Q[<(\<sigma> @ \<sigma>')>]

goal (1 subgoal):
 1. \<Psi> \<rhd> P[<\<sigma>>][<\<sigma>'>] \<doteq> Q[<\<sigma>>][<\<sigma>'>]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P[<\<sigma>>][<\<sigma>'>] \<doteq> Q[<\<sigma>>][<\<sigma>'>]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongOutputPres:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   M :: 'a
  and   N :: 'a

  assumes "P \<doteq>\<^sub>c Q"

  shows "M\<langle>N\<rangle>.P \<doteq>\<^sub>c M\<langle>N\<rangle>.Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M\<langle>N\<rangle>.P \<doteq>\<^sub>c M\<langle>N\<rangle>.Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. M\<langle>N\<rangle>.P \<doteq>\<^sub>c M\<langle>N\<rangle>.Q
[PROOF STEP]
by(fastforce intro: weakCongI weakCongE weakPsiCongOutputPres)


[STATEMENT]
lemma weakCongInputPres:
  fixes \<Psi>    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes "P \<doteq>\<^sub>c Q"
  and     "distinct xvec"

  shows "M\<lparr>\<lambda>*xvec N\<rparr>.P \<doteq>\<^sub>c M\<lparr>\<lambda>*xvec N\<rparr>.Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M\<lparr>\<lambda>*xvec N\<rparr>.P \<doteq>\<^sub>c M\<lparr>\<lambda>*xvec N\<rparr>.Q
[PROOF STEP]
proof(induct rule: weakCongI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
case(cWeakPsiCong \<Psi> \<sigma>)
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
obtain p where "(p \<bullet> xvec) \<sharp>* \<sigma>"
             and "(p \<bullet> xvec) \<sharp>* P" and "(p \<bullet> xvec) \<sharp>* Q" and "(p \<bullet> xvec) \<sharp>* \<Psi>" and "(p \<bullet> xvec) \<sharp>* N"
             and S: "set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>(p \<bullet> xvec) \<sharp>* \<sigma>; (p \<bullet> xvec) \<sharp>* P; (p \<bullet> xvec) \<sharp>* Q; (p \<bullet> xvec) \<sharp>* \<Psi>; (p \<bullet> xvec) \<sharp>* N; set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac c="(\<sigma>, P, Q, \<Psi>, N)" in name_list_avoiding) auto
[PROOF STATE]
proof (state)
this:
(p \<bullet> xvec) \<sharp>* \<sigma>
(p \<bullet> xvec) \<sharp>* P
(p \<bullet> xvec) \<sharp>* Q
(p \<bullet> xvec) \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* N
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
from \<open>P \<doteq>\<^sub>c Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<doteq>\<^sub>c Q
[PROOF STEP]
have "(p \<bullet> P) \<doteq>\<^sub>c (p \<bullet> Q)"
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. p \<bullet> P \<doteq>\<^sub>c p \<bullet> Q
[PROOF STEP]
by(rule weakCongClosed)
[PROOF STATE]
proof (state)
this:
p \<bullet> P \<doteq>\<^sub>c p \<bullet> Q

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
p \<bullet> P \<doteq>\<^sub>c p \<bullet> Q

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
fix Tvec :: "'a list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
from \<open>(p \<bullet> P) \<doteq>\<^sub>c (p \<bullet> Q)\<close> \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> P \<doteq>\<^sub>c p \<bullet> Q
wellFormedSubst \<sigma>
[PROOF STEP]
have "(p \<bullet> P)[<\<sigma>>] \<doteq>\<^sub>c (p \<bullet> Q)[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> P \<doteq>\<^sub>c p \<bullet> Q
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. p \<bullet> P[<\<sigma>>] \<doteq>\<^sub>c p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
by(rule weakCongUnfold)
[PROOF STATE]
proof (state)
this:
p \<bullet> P[<\<sigma>>] \<doteq>\<^sub>c p \<bullet> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<bullet> P[<\<sigma>>] \<doteq>\<^sub>c p \<bullet> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
assume "length xvec = length Tvec" and "distinct xvec"
[PROOF STATE]
proof (state)
this:
length xvec = length Tvec
distinct xvec

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> P[<\<sigma>>] \<doteq>\<^sub>c p \<bullet> Q[<\<sigma>>]
length xvec = length Tvec
distinct xvec
[PROOF STEP]
have "\<Psi> \<rhd> ((p \<bullet> P)[<\<sigma>>])[(p \<bullet> xvec)::=Tvec] \<doteq> ((p \<bullet> Q)[<\<sigma>>])[(p \<bullet> xvec)::=Tvec]"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> P[<\<sigma>>] \<doteq>\<^sub>c p \<bullet> Q[<\<sigma>>]
length xvec = length Tvec
distinct xvec

goal (1 subgoal):
 1. \<Psi> \<rhd> p \<bullet> P[<\<sigma>>][(p \<bullet> xvec)::=Tvec] \<doteq> p \<bullet> Q[<\<sigma>>][(p \<bullet> xvec)::=Tvec]
[PROOF STEP]
by(drule_tac weakCongE[where \<sigma>="[((p \<bullet> xvec), Tvec)]"]) auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> p \<bullet> P[<\<sigma>>][(p \<bullet> xvec)::=Tvec] \<doteq> p \<bullet> Q[<\<sigma>>][(p \<bullet> xvec)::=Tvec]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
hence "\<Psi> \<rhd> ((p \<bullet> P)[<\<sigma>>])[(p \<bullet> xvec)::=Tvec] \<approx> ((p \<bullet> Q)[<\<sigma>>])[(p \<bullet> xvec)::=Tvec]"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> p \<bullet> P[<\<sigma>>][(p \<bullet> xvec)::=Tvec] \<doteq> p \<bullet> Q[<\<sigma>>][(p \<bullet> xvec)::=Tvec]

goal (1 subgoal):
 1. \<Psi> \<rhd> p \<bullet> P[<\<sigma>>][(p \<bullet> xvec)::=Tvec] \<approx> p \<bullet> Q[<\<sigma>>][(p \<bullet> xvec)::=Tvec]
[PROOF STEP]
by(rule weakPsiCongE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> p \<bullet> P[<\<sigma>>][(p \<bullet> xvec)::=Tvec] \<approx> p \<bullet> Q[<\<sigma>>][(p \<bullet> xvec)::=Tvec]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>length xvec = length ?Tvec2; distinct xvec\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>][(p \<bullet> xvec)::=?Tvec2] \<approx> p \<bullet> Q[<\<sigma>>][(p \<bullet> xvec)::=?Tvec2]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
with \<open>(p \<bullet> xvec) \<sharp>* \<sigma>\<close> \<open>distinct xvec\<close>
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> xvec) \<sharp>* \<sigma>
distinct xvec
\<lbrakk>length xvec = length ?Tvec2; distinct xvec\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>][(p \<bullet> xvec)::=?Tvec2] \<approx> p \<bullet> Q[<\<sigma>>][(p \<bullet> xvec)::=?Tvec2]
[PROOF STEP]
have "\<Psi> \<rhd> (M\<lparr>\<lambda>*(p \<bullet> xvec) (p \<bullet> N)\<rparr>.(p \<bullet> P))[<\<sigma>>] \<doteq> (M\<lparr>\<lambda>*(p \<bullet> xvec) (p \<bullet> N)\<rparr>.(p \<bullet> Q))[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> xvec) \<sharp>* \<sigma>
distinct xvec
\<lbrakk>length xvec = length ?Tvec2; distinct xvec\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> p \<bullet> P[<\<sigma>>][(p \<bullet> xvec)::=?Tvec2] \<approx> p \<bullet> Q[<\<sigma>>][(p \<bullet> xvec)::=?Tvec2]

goal (1 subgoal):
 1. \<Psi> \<rhd> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q[<\<sigma>>]
[PROOF STEP]
by(force intro: weakPsiCongInputPres)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
from \<open>(p \<bullet> xvec) \<sharp>* N\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> S
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* P
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
[PROOF STEP]
have "M\<lparr>\<lambda>*(p \<bullet> xvec) (p \<bullet> N)\<rparr>.(p \<bullet> P) = M\<lparr>\<lambda>*xvec N\<rparr>.P"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* P
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)

goal (1 subgoal):
 1. M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P = M\<lparr>\<lambda>*xvec N\<rparr>.P
[PROOF STEP]
apply(simp add: psi.inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p \<bullet> xvec) \<sharp>* N; (p \<bullet> xvec) \<sharp>* P; set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)\<rbrakk> \<Longrightarrow> inputChain (p \<bullet> xvec) (p \<bullet> N) (p \<bullet> P) = inputChain xvec N P
[PROOF STEP]
by(rule inputChainAlpha[symmetric]) auto
[PROOF STATE]
proof (state)
this:
M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P = M\<lparr>\<lambda>*xvec N\<rparr>.P

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P = M\<lparr>\<lambda>*xvec N\<rparr>.P

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
from \<open>(p \<bullet> xvec) \<sharp>* N\<close> \<open>(p \<bullet> xvec) \<sharp>* Q\<close> S
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* Q
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
[PROOF STEP]
have "M\<lparr>\<lambda>*(p \<bullet> xvec) (p \<bullet> N)\<rparr>.(p \<bullet> Q) = M\<lparr>\<lambda>*xvec N\<rparr>.Q"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* Q
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)

goal (1 subgoal):
 1. M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q = M\<lparr>\<lambda>*xvec N\<rparr>.Q
[PROOF STEP]
apply(simp add: psi.inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p \<bullet> xvec) \<sharp>* N; (p \<bullet> xvec) \<sharp>* Q; set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)\<rbrakk> \<Longrightarrow> inputChain (p \<bullet> xvec) (p \<bullet> N) (p \<bullet> Q) = inputChain xvec N Q
[PROOF STEP]
by(rule inputChainAlpha[symmetric]) auto
[PROOF STATE]
proof (state)
this:
M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q = M\<lparr>\<lambda>*xvec N\<rparr>.Q

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q[<\<sigma>>]
M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P = M\<lparr>\<lambda>*xvec N\<rparr>.P
M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q = M\<lparr>\<lambda>*xvec N\<rparr>.Q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q[<\<sigma>>]
M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> P = M\<lparr>\<lambda>*xvec N\<rparr>.P
M\<lparr>\<lambda>*p \<bullet> xvec p \<bullet> N\<rparr>.p \<bullet> Q = M\<lparr>\<lambda>*xvec N\<rparr>.Q

goal (1 subgoal):
 1. \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P[<\<sigma>>] \<doteq> M\<lparr>\<lambda>*xvec N\<rparr>.Q[<\<sigma>>]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongCasePresAux:
  fixes \<Psi>   :: 'b
  and   CsP :: "('c \<times> ('a, 'b, 'c) psi) list"
  and   CsQ :: "('c \<times> ('a, 'b, 'c) psi) list"

  assumes C1: "\<And>\<phi> P. (\<phi>, P) mem CsP \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem CsQ \<and> guarded Q \<and> P \<doteq>\<^sub>c Q"
  and     C2: "\<And>\<phi> Q. (\<phi>, Q) mem CsQ \<Longrightarrow> \<exists>P. (\<phi>, P) mem CsP \<and> guarded P \<and> P \<doteq>\<^sub>c Q"

  shows "Cases CsP \<doteq>\<^sub>c Cases CsQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
fix \<Psi> :: 'b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
fix \<sigma> :: "(name list \<times> 'a list) list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
assume "wellFormedSubst \<sigma>"
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
have "\<Psi> \<rhd> Cases(caseListSeqSubst CsP \<sigma>) \<doteq> Cases(caseListSeqSubst CsQ \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> Cases caseListSeqSubst CsP \<sigma> \<doteq> Cases caseListSeqSubst CsQ \<sigma>
[PROOF STEP]
proof(rule weakPsiCongCasePres)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
 2. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
fix \<phi> P
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
 2. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
assume "(\<phi>, P) mem (caseListSeqSubst CsP \<sigma>)"
[PROOF STATE]
proof (state)
this:
(\<phi>, P) mem caseListSeqSubst CsP \<sigma>

goal (2 subgoals):
 1. \<And>\<phi> P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
 2. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<phi>, P) mem caseListSeqSubst CsP \<sigma>
[PROOF STEP]
obtain \<phi>' P' where "(\<phi>', P') mem CsP" and "\<phi> = substCond.seqSubst \<phi>' \<sigma>" and PeqP': "P = (P'[<\<sigma>>])"
[PROOF STATE]
proof (prove)
using this:
(\<phi>, P) mem caseListSeqSubst CsP \<sigma>

goal (1 subgoal):
 1. (\<And>\<phi>' P'. \<lbrakk>(\<phi>', P') mem CsP; \<phi> = substCond.seqSubst \<phi>' \<sigma>; P = P'[<\<sigma>>]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(induct CsP) force+
[PROOF STATE]
proof (state)
this:
(\<phi>', P') mem CsP
\<phi> = substCond.seqSubst \<phi>' \<sigma>
P = P'[<\<sigma>>]

goal (2 subgoals):
 1. \<And>\<phi> P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
 2. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
from \<open>(\<phi>', P') mem CsP\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<phi>', P') mem CsP
[PROOF STEP]
obtain Q' where "(\<phi>', Q') mem CsQ" and "guarded Q'" and "P' \<doteq>\<^sub>c Q'"
[PROOF STATE]
proof (prove)
using this:
(\<phi>', P') mem CsP

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>(\<phi>', Q') mem CsQ; guarded Q'; P' \<doteq>\<^sub>c Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: C1)
[PROOF STATE]
proof (state)
this:
(\<phi>', Q') mem CsQ
guarded Q'
P' \<doteq>\<^sub>c Q'

goal (2 subgoals):
 1. \<And>\<phi> P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
 2. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
from \<open>(\<phi>', Q') mem CsQ\<close> \<open>\<phi> = substCond.seqSubst \<phi>' \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<phi>', Q') mem CsQ
\<phi> = substCond.seqSubst \<phi>' \<sigma>
[PROOF STEP]
obtain Q where "(\<phi>, Q) mem (caseListSeqSubst CsQ \<sigma>)" and "Q = Q'[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
(\<phi>', Q') mem CsQ
\<phi> = substCond.seqSubst \<phi>' \<sigma>

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>(\<phi>, Q) mem caseListSeqSubst CsQ \<sigma>; Q = Q'[<\<sigma>>]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(induct CsQ) auto
[PROOF STATE]
proof (state)
this:
(\<phi>, Q) mem caseListSeqSubst CsQ \<sigma>
Q = Q'[<\<sigma>>]

goal (2 subgoals):
 1. \<And>\<phi> P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<Longrightarrow> \<exists>Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
 2. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
with PeqP' \<open>guarded Q'\<close> \<open>P' \<doteq>\<^sub>c Q'\<close> \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
P = P'[<\<sigma>>]
guarded Q'
P' \<doteq>\<^sub>c Q'
wellFormedSubst \<sigma>
(\<phi>, Q) mem caseListSeqSubst CsQ \<sigma>
Q = Q'[<\<sigma>>]
[PROOF STEP]
show "\<exists>Q. (\<phi>, Q) mem (caseListSeqSubst CsQ \<sigma>) \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)"
[PROOF STATE]
proof (prove)
using this:
P = P'[<\<sigma>>]
guarded Q'
P' \<doteq>\<^sub>c Q'
wellFormedSubst \<sigma>
(\<phi>, Q) mem caseListSeqSubst CsQ \<sigma>
Q = Q'[<\<sigma>>]

goal (1 subgoal):
 1. \<exists>Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
by(blast dest: weakCongE guardedSeqSubst)
[PROOF STATE]
proof (state)
this:
\<exists>Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<and> guarded Q \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)

goal (1 subgoal):
 1. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
fix \<phi> Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
assume "(\<phi>, Q) mem (caseListSeqSubst CsQ \<sigma>)"
[PROOF STATE]
proof (state)
this:
(\<phi>, Q) mem caseListSeqSubst CsQ \<sigma>

goal (1 subgoal):
 1. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<phi>, Q) mem caseListSeqSubst CsQ \<sigma>
[PROOF STEP]
obtain \<phi>' Q' where "(\<phi>', Q') mem CsQ" and "\<phi> = substCond.seqSubst \<phi>' \<sigma>" and QeqQ': "Q = Q'[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
(\<phi>, Q) mem caseListSeqSubst CsQ \<sigma>

goal (1 subgoal):
 1. (\<And>\<phi>' Q'. \<lbrakk>(\<phi>', Q') mem CsQ; \<phi> = substCond.seqSubst \<phi>' \<sigma>; Q = Q'[<\<sigma>>]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(induct CsQ) force+
[PROOF STATE]
proof (state)
this:
(\<phi>', Q') mem CsQ
\<phi> = substCond.seqSubst \<phi>' \<sigma>
Q = Q'[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
from \<open>(\<phi>', Q') mem CsQ\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<phi>', Q') mem CsQ
[PROOF STEP]
obtain P' where "(\<phi>', P') mem CsP" and "guarded P'" and "P' \<doteq>\<^sub>c Q'"
[PROOF STATE]
proof (prove)
using this:
(\<phi>', Q') mem CsQ

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>(\<phi>', P') mem CsP; guarded P'; P' \<doteq>\<^sub>c Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: C2)
[PROOF STATE]
proof (state)
this:
(\<phi>', P') mem CsP
guarded P'
P' \<doteq>\<^sub>c Q'

goal (1 subgoal):
 1. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
from \<open>(\<phi>', P') mem CsP\<close> \<open>\<phi> = substCond.seqSubst \<phi>' \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<phi>', P') mem CsP
\<phi> = substCond.seqSubst \<phi>' \<sigma>
[PROOF STEP]
obtain P where "(\<phi>, P) mem (caseListSeqSubst CsP \<sigma>)" and "P = P'[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
(\<phi>', P') mem CsP
\<phi> = substCond.seqSubst \<phi>' \<sigma>

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>(\<phi>, P) mem caseListSeqSubst CsP \<sigma>; P = P'[<\<sigma>>]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(induct CsP) auto
[PROOF STATE]
proof (state)
this:
(\<phi>, P) mem caseListSeqSubst CsP \<sigma>
P = P'[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<phi> Q. (\<phi>, Q) mem caseListSeqSubst CsQ \<sigma> \<Longrightarrow> \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
with QeqQ' \<open>guarded P'\<close> \<open>P' \<doteq>\<^sub>c Q'\<close> \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
Q = Q'[<\<sigma>>]
guarded P'
P' \<doteq>\<^sub>c Q'
wellFormedSubst \<sigma>
(\<phi>, P) mem caseListSeqSubst CsP \<sigma>
P = P'[<\<sigma>>]
[PROOF STEP]
show "\<exists>P. (\<phi>, P) mem (caseListSeqSubst CsP \<sigma>) \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)"
[PROOF STATE]
proof (prove)
using this:
Q = Q'[<\<sigma>>]
guarded P'
P' \<doteq>\<^sub>c Q'
wellFormedSubst \<sigma>
(\<phi>, P) mem caseListSeqSubst CsP \<sigma>
P = P'[<\<sigma>>]

goal (1 subgoal):
 1. \<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)
[PROOF STEP]
by(blast dest: weakCongE guardedSeqSubst)
[PROOF STATE]
proof (state)
this:
\<exists>P. (\<phi>, P) mem caseListSeqSubst CsP \<sigma> \<and> guarded P \<and> (\<forall>\<Psi>. \<Psi> \<rhd> P \<doteq> Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Cases caseListSeqSubst CsP \<sigma> \<doteq> Cases caseListSeqSubst CsQ \<sigma>

goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
wellFormedSubst ?\<sigma>2 \<Longrightarrow> ?\<Psi>'2 \<rhd> Cases caseListSeqSubst CsP ?\<sigma>2 \<doteq> Cases caseListSeqSubst CsQ ?\<sigma>2

goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
wellFormedSubst ?\<sigma>2 \<Longrightarrow> ?\<Psi>'2 \<rhd> Cases caseListSeqSubst CsP ?\<sigma>2 \<doteq> Cases caseListSeqSubst CsQ ?\<sigma>2

goal (1 subgoal):
 1. Cases CsP \<doteq>\<^sub>c Cases CsQ
[PROOF STEP]
by(rule_tac weakCongI) auto
[PROOF STATE]
proof (state)
this:
Cases CsP \<doteq>\<^sub>c Cases CsQ

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongParPres:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"

  assumes "P \<doteq>\<^sub>c Q"

  shows "P \<parallel> R \<doteq>\<^sub>c Q \<parallel> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> R \<doteq>\<^sub>c Q \<parallel> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. P \<parallel> R \<doteq>\<^sub>c Q \<parallel> R
[PROOF STEP]
by(fastforce intro: weakCongI weakCongE weakPsiCongParPres)


[STATEMENT]
lemma weakCongResPres:
  fixes P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   x :: name

  assumes "P \<doteq>\<^sub>c Q"

  shows "\<lparr>\<nu>x\<rparr>P \<doteq>\<^sub>c \<lparr>\<nu>x\<rparr>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>\<nu>x\<rparr>P \<doteq>\<^sub>c \<lparr>\<nu>x\<rparr>Q
[PROOF STEP]
proof(induct rule: weakCongI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P[<\<sigma>>] \<doteq> \<lparr>\<nu>x\<rparr>Q[<\<sigma>>]
[PROOF STEP]
case(cWeakPsiCong \<Psi> \<sigma>)
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P[<\<sigma>>] \<doteq> \<lparr>\<nu>x\<rparr>Q[<\<sigma>>]
[PROOF STEP]
obtain y::name where "y \<sharp> (\<Psi>::'b)" and "y \<sharp> P" and "y \<sharp> Q" and "y \<sharp> \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<sharp> \<Psi>; y \<sharp> P; y \<sharp> Q; y \<sharp> \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(generate_fresh "name") (auto simp add: fresh_prod)
[PROOF STATE]
proof (state)
this:
y \<sharp> \<Psi>
y \<sharp> P
y \<sharp> Q
y \<sharp> \<sigma>

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P[<\<sigma>>] \<doteq> \<lparr>\<nu>x\<rparr>Q[<\<sigma>>]
[PROOF STEP]
from \<open>P \<doteq>\<^sub>c Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<doteq>\<^sub>c Q
[PROOF STEP]
have "([(x, y)] \<bullet> P) \<doteq>\<^sub>c ([(x, y)] \<bullet> Q)"
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q

goal (1 subgoal):
 1. [(x, y)] \<bullet> P \<doteq>\<^sub>c [(x, y)] \<bullet> Q
[PROOF STEP]
by(rule weakCongClosed)
[PROOF STATE]
proof (state)
this:
[(x, y)] \<bullet> P \<doteq>\<^sub>c [(x, y)] \<bullet> Q

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P[<\<sigma>>] \<doteq> \<lparr>\<nu>x\<rparr>Q[<\<sigma>>]
[PROOF STEP]
hence "\<Psi> \<rhd> ([(x, y)] \<bullet> P)[<\<sigma>>] \<doteq> ([(x, y)] \<bullet> Q)[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<bullet> P \<doteq>\<^sub>c [(x, y)] \<bullet> Q

goal (1 subgoal):
 1. \<Psi> \<rhd> [(x, y)] \<bullet> P[<\<sigma>>] \<doteq> [(x, y)] \<bullet> Q[<\<sigma>>]
[PROOF STEP]
using \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (prove)
using this:
[(x, y)] \<bullet> P \<doteq>\<^sub>c [(x, y)] \<bullet> Q
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. \<Psi> \<rhd> [(x, y)] \<bullet> P[<\<sigma>>] \<doteq> [(x, y)] \<bullet> Q[<\<sigma>>]
[PROOF STEP]
by(rule weakCongE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> [(x, y)] \<bullet> P[<\<sigma>>] \<doteq> [(x, y)] \<bullet> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P[<\<sigma>>] \<doteq> \<lparr>\<nu>x\<rparr>Q[<\<sigma>>]
[PROOF STEP]
hence "\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>(([(x, y)] \<bullet> P)[<\<sigma>>]) \<doteq> \<lparr>\<nu>y\<rparr>(([(x, y)] \<bullet> Q)[<\<sigma>>])"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> [(x, y)] \<bullet> P[<\<sigma>>] \<doteq> [(x, y)] \<bullet> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> P[<\<sigma>>] \<doteq> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> Q[<\<sigma>>]
[PROOF STEP]
using \<open>y \<sharp> \<Psi>\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> [(x, y)] \<bullet> P[<\<sigma>>] \<doteq> [(x, y)] \<bullet> Q[<\<sigma>>]
y \<sharp> \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> P[<\<sigma>>] \<doteq> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> Q[<\<sigma>>]
[PROOF STEP]
by(rule weakPsiCongResPres)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> P[<\<sigma>>] \<doteq> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<And>\<Psi> \<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P[<\<sigma>>] \<doteq> \<lparr>\<nu>x\<rparr>Q[<\<sigma>>]
[PROOF STEP]
with \<open>y \<sharp> P\<close> \<open>y \<sharp> Q\<close>  \<open>y \<sharp> \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> P
y \<sharp> Q
y \<sharp> \<sigma>
\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> P[<\<sigma>>] \<doteq> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> Q[<\<sigma>>]
[PROOF STEP]
show "\<Psi> \<rhd> (\<lparr>\<nu>x\<rparr>P)[<\<sigma>>] \<doteq> (\<lparr>\<nu>x\<rparr>Q)[<\<sigma>>]"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> P
y \<sharp> Q
y \<sharp> \<sigma>
\<Psi> \<rhd> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> P[<\<sigma>>] \<doteq> \<lparr>\<nu>y\<rparr>[(x, y)] \<bullet> Q[<\<sigma>>]

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P[<\<sigma>>] \<doteq> \<lparr>\<nu>x\<rparr>Q[<\<sigma>>]
[PROOF STEP]
by(simp add: alphaRes)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P[<\<sigma>>] \<doteq> \<lparr>\<nu>x\<rparr>Q[<\<sigma>>]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongBangPres:
  fixes P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "P \<doteq>\<^sub>c Q"
  and     "guarded P"
  and     "guarded Q"

  shows "!P \<doteq>\<^sub>c !Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<doteq>\<^sub>c !Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<doteq>\<^sub>c Q
guarded P
guarded Q

goal (1 subgoal):
 1. !P \<doteq>\<^sub>c !Q
[PROOF STEP]
by(fastforce intro: weakCongI weakCongE weakPsiCongBangPres  guardedSeqSubst)


[STATEMENT]
lemma is_Less_iff: "is_Less f = (\<exists>r rs. f = Less r rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Less f = (\<exists>r rs. f = Less r rs)
[PROOF STEP]
by(induct f) auto


[STATEMENT]
lemma is_Eq_iff: "(\<forall>i j. a \<noteq> Less i j) = (\<exists>i j. a = Eq i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i j. a \<noteq> Less i j) = (\<exists>i j. a = Eq i j)
[PROOF STEP]
by(cases a) auto


[STATEMENT]
lemma set_lbounds:
 "set(lbounds as) = {(r/c, (-1/c) *\<^sub>s cs)|r c cs. Less r (c#cs) \<in> set as \<and> c>0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (lbounds as) = {(r / c, (- 1 / c) *\<^sub>s cs) |r c cs. Less r (c # cs) \<in> set as \<and> 0 < c}
[PROOF STEP]
by(force simp: lbounds_def split:list.splits atom.splits if_splits)


[STATEMENT]
lemma set_ubounds:
 "set(ubounds as) = {(r/c, (-1/c) *\<^sub>s cs)|r c cs. Less r (c#cs) \<in> set as \<and> c<0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (ubounds as) = {(r / c, (- 1 / c) *\<^sub>s cs) |r c cs. Less r (c # cs) \<in> set as \<and> c < 0}
[PROOF STEP]
by(force simp: ubounds_def split:list.splits atom.splits if_splits)


[STATEMENT]
lemma set_ebounds:
  "set(ebounds as) = {(r/c, (-1/c) *\<^sub>s cs)|r c cs. Eq r (c#cs) \<in> set as \<and> c\<noteq>0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (ebounds as) = {(r / c, (- 1 / c) *\<^sub>s cs) |r c cs. Eq r (c # cs) \<in> set as \<and> c \<noteq> 0}
[PROOF STEP]
by(force simp: ebounds_def split:list.splits atom.splits if_splits)


[STATEMENT]
lemma I_asubst:
 "I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
[PROOF STEP]
proof(cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x11 x12. a = Less x11 x12 \<Longrightarrow> I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
 2. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
[PROOF STEP]
case (Less r cs)
[PROOF STATE]
proof (state)
this:
a = Less r cs

goal (2 subgoals):
 1. \<And>x11 x12. a = Less x11 x12 \<Longrightarrow> I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
 2. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Less r cs

goal (1 subgoal):
 1. I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
[PROOF STEP]
by(cases t, cases cs,
    simp_all add:eval_def distrib_left iprod_left_add_distrib)
    arith
[PROOF STATE]
proof (state)
this:
I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)

goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
[PROOF STEP]
case (Eq r cs)
[PROOF STATE]
proof (state)
this:
a = Eq r cs

goal (1 subgoal):
 1. \<And>x21 x22. a = Eq x21 x22 \<Longrightarrow> I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Eq r cs

goal (1 subgoal):
 1. I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)
[PROOF STEP]
by(cases t, cases cs, simp_all add:eval_def distrib_left iprod_left_add_distrib)
      arith
[PROOF STATE]
proof (state)
this:
I\<^sub>R (asubst t a) xs = I\<^sub>R a (eval t xs # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma I_subst:
  "qfree \<phi> \<Longrightarrow> R.I (subst \<phi> t) xs = R.I \<phi> (eval t xs # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qfree \<phi> \<Longrightarrow> R.I (subst \<phi> t) xs = R.I \<phi> (eval t xs # xs)
[PROOF STEP]
by(induct \<phi>)(simp_all add:I_asubst)


[STATEMENT]
lemma I_subst_pretty:
  "qfree \<phi> \<Longrightarrow> R.I (subst \<phi> (r,cs)) xs = R.I \<phi> ((r + \<langle>cs,xs\<rangle>) # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qfree \<phi> \<Longrightarrow> R.I (subst \<phi> (r, cs)) xs = R.I \<phi> ((r + \<langle>cs,xs\<rangle>) # xs)
[PROOF STEP]
by(simp add:I_subst eval_def)


[STATEMENT]
lemma qfree_min_inf: "qfree \<phi> \<Longrightarrow> qfree(inf\<^sub>- \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qfree \<phi> \<Longrightarrow> qfree (inf\<^sub>- \<phi>)
[PROOF STEP]
by(induct \<phi> rule:min_inf.induct) simp_all


[STATEMENT]
lemma qfree_plus_inf: "qfree \<phi> \<Longrightarrow> qfree(inf\<^sub>+ \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qfree \<phi> \<Longrightarrow> qfree (inf\<^sub>+ \<phi>)
[PROOF STEP]
by(induct \<phi> rule:plus_inf.induct) simp_all