[STATEMENT]
lemma assumes "\<And> G \<phi>. IsProperInX (\<lambda>x . \<lparr>G,\<^bold>\<iota>y . \<phi> y x\<rparr>)"
  shows Fx_equiv_xH: "[\<^bold>\<forall> H . \<^bold>\<exists> F . \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<forall>H. \<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
proof (rule "\<^bold>\<forall>I")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
fix H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
let ?G = "(\<^bold>\<lambda>x . \<^bold>\<forall> p . p \<^bold>\<rightarrow> p)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
obtain \<phi> where \<phi>_def: "\<phi> = (\<lambda> y x . (y\<^sup>P) \<^bold>= x \<^bold>& \<lbrace>x,H\<rbrace>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<phi>. \<phi> = (\<lambda>y x. y\<^sup>P \<^bold>= x \<^bold>& \<lbrace>x,H\<rbrace>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> = (\<lambda>y x. y\<^sup>P \<^bold>= x \<^bold>& \<lbrace>x,H\<rbrace>)

goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
have "[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>?G,\<^bold>\<iota>y . \<phi> y (x\<^sup>P)\<rparr>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v]
[PROOF STEP]
using relations_1[OF assms]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>?G1,\<^bold>\<iota>y. ?\<phi>1 y (x\<^sup>P)\<rparr>) in ?v]

goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v]

goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
hence 1: "[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y . \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v] \<Longrightarrow> [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]
[PROOF STEP]
apply (PLM_subst_method
          "\<lambda> x . \<lparr>?G,\<^bold>\<iota>y . \<phi> y (x\<^sup>P)\<rparr>" "\<lambda> x . (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v] \<Longrightarrow> \<forall>x v. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P)) in v]
 2. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v] \<Longrightarrow> [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v]
[PROOF STEP]
using exe_impl_exists
[PROOF STATE]
proof (prove)
using this:
[\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. ?\<phi> y ?x\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>?\<phi> y ?x) in ?v]

goal (2 subgoals):
 1. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v] \<Longrightarrow> \<forall>x v. [\<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P)) in v]
 2. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v] \<Longrightarrow> [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>\<^bold>\<lambda>x. \<^bold>\<forall>p. p \<^bold>\<rightarrow> p,\<^bold>\<iota>y. \<phi> y (x\<^sup>P)\<rparr>) in v]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]

goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]
[PROOF STEP]
obtain F where F_def: "[\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y . \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]

goal (1 subgoal):
 1. (\<And>F. [\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]

goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]

goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
have 2: "\<And> v x . [(\<^bold>\<exists>!y . \<^bold>\<A>\<phi> y (x\<^sup>P)) \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace> in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v x. [(\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P)) \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace> in v]
[PROOF STEP]
proof (rule "\<^bold>\<equiv>I"; rule CP)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v x. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v] \<Longrightarrow> [\<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
fix x v
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v x. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v] \<Longrightarrow> [\<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
assume "[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]"
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]

goal (2 subgoals):
 1. \<And>v x. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v] \<Longrightarrow> [\<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
hence "[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
unfolding exists_unique_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (2 subgoals):
 1. \<And>v x. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v] \<Longrightarrow> [\<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
obtain \<alpha> where "[\<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. (\<And>\<alpha>. [\<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (2 subgoals):
 1. \<And>v x. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v] \<Longrightarrow> [\<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
hence "[\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
unfolding \<phi>_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
using "\<^bold>&E"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>(\<beta>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal (2 subgoals):
 1. \<And>v x. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v] \<Longrightarrow> [\<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
hence "[\<^bold>\<A>(\<lbrace>x\<^sup>P,H\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]
[PROOF STEP]
using Act_Basic_2[equiv_lr] "\<^bold>&E"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<alpha>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[\<^bold>\<A>(?\<phi>1 \<^bold>& ?\<psi>1) in ?v] \<Longrightarrow> [\<^bold>\<A>?\<phi>1 \<^bold>& \<^bold>\<A>?\<psi>1 in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]

goal (2 subgoals):
 1. \<And>v x. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v] \<Longrightarrow> [\<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
thus "[\<lbrace>x\<^sup>P,H\<rbrace> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]

goal (1 subgoal):
 1. [\<lbrace>x\<^sup>P,H\<rbrace> in v]
[PROOF STEP]
using en_eq_10[equiv_lr]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]
[\<^bold>\<A>\<lbrace>?x1,?F1\<rbrace> in ?v] \<Longrightarrow> [\<lbrace>?x1,?F1\<rbrace> in ?v]

goal (1 subgoal):
 1. [\<lbrace>x\<^sup>P,H\<rbrace> in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<lbrace>x\<^sup>P,H\<rbrace> in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
fix x v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
assume "[\<lbrace>x\<^sup>P,H\<rbrace> in v]"
[PROOF STATE]
proof (state)
this:
[\<lbrace>x\<^sup>P,H\<rbrace> in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
hence 1: "[\<^bold>\<A>(\<lbrace>x\<^sup>P,H\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<lbrace>x\<^sup>P,H\<rbrace> in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]
[PROOF STEP]
using en_eq_10[equiv_rl]
[PROOF STATE]
proof (prove)
using this:
[\<lbrace>x\<^sup>P,H\<rbrace> in v]
[\<lbrace>?x1,?F1\<rbrace> in ?v] \<Longrightarrow> [\<^bold>\<A>\<lbrace>?x1,?F1\<rbrace> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
have "[x \<^bold>= x in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x \<^bold>= x in v]
[PROOF STEP]
using id_eq_1[where 'a=\<nu>]
[PROOF STATE]
proof (prove)
using this:
[?x \<^bold>= ?x in ?v]

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

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
hence "[\<^bold>\<A>(x \<^bold>= x) in v]"
[PROOF STATE]
proof (prove)
using this:
[x \<^bold>= x in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x) in v]
[PROOF STEP]
using id_act_3[equiv_lr]
[PROOF STATE]
proof (prove)
using this:
[x \<^bold>= x in v]
[?\<alpha>1 \<^bold>= ?\<beta>1 in ?v] \<Longrightarrow> [\<^bold>\<A>(?\<alpha>1 \<^bold>= ?\<beta>1) in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x \<^bold>= x) in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(x \<^bold>= x) in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
hence "[\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x \<^bold>= x) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
unfolding identity_\<nu>_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
using 1 Act_Basic_2[equiv_rl] "\<^bold>&I"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P) in v]
[\<^bold>\<A>\<lbrace>x\<^sup>P,H\<rbrace> in v]
[\<^bold>\<A>?\<phi>1 \<^bold>& \<^bold>\<A>?\<psi>1 in ?v] \<Longrightarrow> [\<^bold>\<A>(?\<phi>1 \<^bold>& ?\<psi>1) in ?v]
\<lbrakk>[?\<phi> in ?v]; [?\<psi> in ?v]\<rbrakk> \<Longrightarrow> [?\<phi> \<^bold>& ?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
hence "[\<^bold>\<A>\<phi> x (x\<^sup>P) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<phi> x (x\<^sup>P) in v]
[PROOF STEP]
unfolding \<phi>_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(x\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> x (x\<^sup>P) in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> x (x\<^sup>P) in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
have "[\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]
[PROOF STEP]
proof (rule "\<^bold>\<forall>I"; rule CP)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<beta>. [\<^bold>\<A>\<phi> \<beta> (x\<^sup>P) in v] \<Longrightarrow> [\<beta> \<^bold>= x in v]
[PROOF STEP]
fix \<beta>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<beta>. [\<^bold>\<A>\<phi> \<beta> (x\<^sup>P) in v] \<Longrightarrow> [\<beta> \<^bold>= x in v]
[PROOF STEP]
assume "[\<^bold>\<A>\<phi> \<beta> (x\<^sup>P) in v]"
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> \<beta> (x\<^sup>P) in v]

goal (1 subgoal):
 1. \<And>\<beta>. [\<^bold>\<A>\<phi> \<beta> (x\<^sup>P) in v] \<Longrightarrow> [\<beta> \<^bold>= x in v]
[PROOF STEP]
hence "[\<^bold>\<A>(\<beta> \<^bold>= x) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> \<beta> (x\<^sup>P) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<beta> \<^bold>= x) in v]
[PROOF STEP]
unfolding \<phi>_def identity_\<nu>_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<beta>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<beta>\<^sup>P \<^bold>= x\<^sup>P) in v]
[PROOF STEP]
using Act_Basic_2[equiv_lr] "\<^bold>&E"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<beta>\<^sup>P \<^bold>= x\<^sup>P \<^bold>& \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[\<^bold>\<A>(?\<phi>1 \<^bold>& ?\<psi>1) in ?v] \<Longrightarrow> [\<^bold>\<A>?\<phi>1 \<^bold>& \<^bold>\<A>?\<psi>1 in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]
[?\<phi> \<^bold>& ?\<psi> in ?v] \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>(\<beta>\<^sup>P \<^bold>= x\<^sup>P) in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>(\<beta> \<^bold>= x) in v]

goal (1 subgoal):
 1. \<And>\<beta>. [\<^bold>\<A>\<phi> \<beta> (x\<^sup>P) in v] \<Longrightarrow> [\<beta> \<^bold>= x in v]
[PROOF STEP]
thus "[\<beta> \<^bold>= x in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<beta> \<^bold>= x) in v]

goal (1 subgoal):
 1. [\<beta> \<^bold>= x in v]
[PROOF STEP]
using id_act_3[equiv_rl]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>(\<beta> \<^bold>= x) in v]
[\<^bold>\<A>(?\<alpha>1 \<^bold>= ?\<beta>1) in ?v] \<Longrightarrow> [?\<alpha>1 \<^bold>= ?\<beta>1 in ?v]

goal (1 subgoal):
 1. [\<beta> \<^bold>= x in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<beta> \<^bold>= x in v]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<A>\<phi> x (x\<^sup>P) in v]
[\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]
[PROOF STEP]
have "[\<^bold>\<A>\<phi> x (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> x (x\<^sup>P) in v]
[\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<phi> x (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]
[PROOF STEP]
using "\<^bold>&I"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> x (x\<^sup>P) in v]
[\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x in v]
\<lbrakk>[?\<phi> in ?v]; [?\<psi> in ?v]\<rbrakk> \<Longrightarrow> [?\<phi> \<^bold>& ?\<psi> in ?v]

goal (1 subgoal):
 1. [\<^bold>\<A>\<phi> x (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
[\<^bold>\<A>\<phi> x (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
hence "[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<A>\<phi> x (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= x) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
by (rule existential)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. \<And>v x. [\<lbrace>x\<^sup>P,H\<rbrace> in v] \<Longrightarrow> [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
thus "[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]
[PROOF STEP]
unfolding exists_unique_def
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>\<alpha>. \<^bold>\<A>\<phi> \<alpha> (x\<^sup>P) \<^bold>& (\<^bold>\<forall>\<beta>. \<^bold>\<A>\<phi> \<beta> (x\<^sup>P) \<^bold>\<rightarrow> \<beta> \<^bold>= \<alpha>) in v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P) in v]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (?x\<^sup>P)) \<^bold>\<equiv> \<lbrace>?x\<^sup>P,H\<rbrace> in ?v]

goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
have "[\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
apply (PLM_subst_goal_method
          "\<lambda>\<phi> . \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<phi> x)"
          "\<lambda> x . (\<^bold>\<exists>!y . \<^bold>\<A>\<phi> y (x\<^sup>P))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x v. [(\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P)) \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. [\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]
[PROOF STEP]
using 2 F_def
[PROOF STATE]
proof (prove)
using this:
[(\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (?x\<^sup>P)) \<^bold>\<equiv> \<lbrace>?x\<^sup>P,H\<rbrace> in ?v]
[\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]

goal (2 subgoals):
 1. \<forall>x v. [(\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P)) \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace> in v]
 2. [\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> (\<^bold>\<exists>!y. \<^bold>\<A>\<phi> y (x\<^sup>P))) in v]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal (1 subgoal):
 1. \<And>H. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
thus "[\<^bold>\<exists> F . \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]
[PROOF STEP]
by (rule existential)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>F. \<^bold>\<box>(\<^bold>\<forall>x. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lbrace>x\<^sup>P,H\<rbrace>) in v]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma original_paradox:
    assumes is_propositional: "(\<And>G \<phi>. IsProperInX (\<lambda>x. \<lparr>G,\<^bold>\<iota>y. \<phi> y x\<rparr>))"
    shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
have "[\<^bold>\<exists>x y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<exists>x y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[PROOF STEP]
using aclassical2
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>x y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in ?v]

goal (1 subgoal):
 1. [\<^bold>\<exists>x y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>x y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>x y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[PROOF STEP]
obtain x where
      "[\<^bold>\<exists> y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>x y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. (\<And>x. [\<^bold>\<exists>y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[PROOF STEP]
obtain y where xy_def:
      "[\<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>y. \<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. (\<And>y. [\<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<lparr>A!,x\<^sup>P\<rparr> \<^bold>& \<lparr>A!,y\<^sup>P\<rparr> \<^bold>& x \<^bold>\<noteq> y \<^bold>& (\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
have "[\<^bold>\<exists> F . \<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[PROOF STEP]
using diffprop[OF assms, OF xy_def[conj1,conj1,conj1],
                     OF xy_def[conj1,conj1,conj2],
                     OF xy_def[conj1,conj2]]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>F. \<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. [\<^bold>\<exists>F. \<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[\<^bold>\<exists>F. \<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<exists>F. \<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[PROOF STEP]
obtain F where "[\<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<exists>F. \<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. (\<And>F. [\<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Instantiate)
[PROOF STATE]
proof (state)
this:
[\<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[\<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
have "[\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr> in v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr> in v]
[PROOF STEP]
using xy_def[conj2]
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<forall>F. \<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. [\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr> in v]
[PROOF STEP]
by (rule "\<^bold>\<forall>E")
[PROOF STATE]
proof (state)
this:
[\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[\<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr> in v]
[PROOF STEP]
have "\<And>\<phi>.[\<phi> in v]"
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr> in v]

goal (1 subgoal):
 1. \<And>\<phi>. [\<phi> in v]
[PROOF STEP]
using PLM.raa_cor_2
[PROOF STATE]
proof (prove)
using this:
[\<^bold>\<not>(\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr>) in v]
[\<lparr>F,x\<^sup>P\<rparr> \<^bold>\<equiv> \<lparr>F,y\<^sup>P\<rparr> in v]
\<lbrakk>[\<^bold>\<not>?\<phi> in ?v]; [\<^bold>\<not>?\<psi> in ?v] \<Longrightarrow> [?\<phi> in ?v]; [\<^bold>\<not>?\<phi> in ?v]\<rbrakk> \<Longrightarrow> [?\<psi> in ?v]

goal (1 subgoal):
 1. \<And>\<phi>. [\<phi> in v]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[?\<phi> in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
[?\<phi> in v]

goal (1 subgoal):
 1. False
[PROOF STEP]
using Semantics.T4
[PROOF STATE]
proof (prove)
using this:
[?\<phi> in v]
[\<^bold>\<not>?\<psi> in ?w] = (\<not> [?\<psi> in ?w])

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ND_sound_complete_countable:
  fixes \<Gamma> :: "'a :: countable formula set"
  shows "\<Gamma> \<turnstile> F \<longleftrightarrow> \<Gamma> \<TTurnstile> F" (is "?n \<longleftrightarrow> ?s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma> \<turnstile> F) = \<Gamma> \<TTurnstile> F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma> \<turnstile> F \<Longrightarrow> \<Gamma> \<TTurnstile> F
 2. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
assume ?n
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> F

goal (2 subgoals):
 1. \<Gamma> \<turnstile> F \<Longrightarrow> \<Gamma> \<TTurnstile> F
 2. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
thus ?s
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> F

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F
[PROOF STEP]
by (fact ND_sound)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<TTurnstile> F

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
assume s: ?s
[PROOF STATE]
proof (state)
this:
\<Gamma> \<TTurnstile> F

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
with compact_entailment
[PROOF STATE]
proof (chain)
picking this:
?\<Gamma> \<TTurnstile> ?F \<Longrightarrow> \<exists>\<Gamma>'. finite \<Gamma>' \<and> \<Gamma>' \<subseteq> ?\<Gamma> \<and> \<Gamma>' \<TTurnstile> ?F
\<Gamma> \<TTurnstile> F
[PROOF STEP]
obtain \<Gamma>' where 0: "finite \<Gamma>'" "\<Gamma>' \<TTurnstile> F" "\<Gamma>' \<subseteq> \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
?\<Gamma> \<TTurnstile> ?F \<Longrightarrow> \<exists>\<Gamma>'. finite \<Gamma>' \<and> \<Gamma>' \<subseteq> ?\<Gamma> \<and> \<Gamma>' \<TTurnstile> ?F
\<Gamma> \<TTurnstile> F

goal (1 subgoal):
 1. (\<And>\<Gamma>'. \<lbrakk>finite \<Gamma>'; \<Gamma>' \<TTurnstile> F; \<Gamma>' \<subseteq> \<Gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding entailment_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<A>. (\<forall>G\<in>?\<Gamma>. \<A> \<Turnstile> G) \<longrightarrow> \<A> \<Turnstile> ?F \<Longrightarrow> \<exists>\<Gamma>'. finite \<Gamma>' \<and> \<Gamma>' \<subseteq> ?\<Gamma> \<and> (\<forall>\<A>. (\<forall>G\<in>\<Gamma>'. \<A> \<Turnstile> G) \<longrightarrow> \<A> \<Turnstile> ?F)
\<forall>\<A>. (\<forall>G\<in>\<Gamma>. \<A> \<Turnstile> G) \<longrightarrow> \<A> \<Turnstile> F

goal (1 subgoal):
 1. (\<And>\<Gamma>'. \<lbrakk>finite \<Gamma>'; \<forall>\<A>. (\<forall>G\<in>\<Gamma>'. \<A> \<Turnstile> G) \<longrightarrow> \<A> \<Turnstile> F; \<Gamma>' \<subseteq> \<Gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite \<Gamma>'
\<Gamma>' \<TTurnstile> F
\<Gamma>' \<subseteq> \<Gamma>

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite \<Gamma>'
\<Gamma>' \<TTurnstile> F
\<Gamma>' \<subseteq> \<Gamma>
[PROOF STEP]
obtain \<Gamma>'' where \<Gamma>'': "\<Gamma>' = set_mset \<Gamma>''"
[PROOF STATE]
proof (prove)
using this:
finite \<Gamma>'
\<Gamma>' \<TTurnstile> F
\<Gamma>' \<subseteq> \<Gamma>

goal (1 subgoal):
 1. (\<And>\<Gamma>''. \<Gamma>' = set_mset \<Gamma>'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_set_mset_mset_set
[PROOF STATE]
proof (prove)
using this:
finite \<Gamma>'
\<Gamma>' \<TTurnstile> F
\<Gamma>' \<subseteq> \<Gamma>
finite ?A \<Longrightarrow> set_mset (mset_set ?A) = ?A

goal (1 subgoal):
 1. (\<And>\<Gamma>''. \<Gamma>' = set_mset \<Gamma>'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Gamma>' = set_mset \<Gamma>''

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
have su: "set_mset \<Gamma>'' \<subseteq> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset \<Gamma>'' \<subseteq> \<Gamma>
[PROOF STEP]
using 0  \<Gamma>''
[PROOF STATE]
proof (prove)
using this:
finite \<Gamma>'
\<Gamma>' \<TTurnstile> F
\<Gamma>' \<subseteq> \<Gamma>
\<Gamma>' = set_mset \<Gamma>''

goal (1 subgoal):
 1. set_mset \<Gamma>'' \<subseteq> \<Gamma>
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
set_mset \<Gamma>'' \<subseteq> \<Gamma>

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
from 0
[PROOF STATE]
proof (chain)
picking this:
finite \<Gamma>'
\<Gamma>' \<TTurnstile> F
\<Gamma>' \<subseteq> \<Gamma>
[PROOF STEP]
have "\<Turnstile> \<Gamma>'' \<Rightarrow> {#F#}"
[PROOF STATE]
proof (prove)
using this:
finite \<Gamma>'
\<Gamma>' \<TTurnstile> F
\<Gamma>' \<subseteq> \<Gamma>

goal (1 subgoal):
 1. \<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
unfolding sequent_semantics_def entailment_def \<Gamma>''
[PROOF STATE]
proof (prove)
using this:
finite (set_mset \<Gamma>'')
\<forall>\<A>. (\<forall>G\<in>#\<Gamma>''. \<A> \<Turnstile> G) \<longrightarrow> \<A> \<Turnstile> F
set_mset \<Gamma>'' \<subseteq> \<Gamma>

goal (1 subgoal):
 1. \<forall>A. (\<forall>\<gamma>\<in>#\<Gamma>''. A \<Turnstile> \<gamma>) \<longrightarrow> (\<exists>\<delta>\<in>#F, {#}. A \<Turnstile> \<delta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
with SC_sound_complete
[PROOF STATE]
proof (chain)
picking this:
?\<Gamma> \<Rightarrow> ?\<Delta> = \<Turnstile> ?\<Gamma> \<Rightarrow> ?\<Delta>
\<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
have "\<Gamma>'' \<Rightarrow> {#F#}"
[PROOF STATE]
proof (prove)
using this:
?\<Gamma> \<Rightarrow> ?\<Delta> = \<Turnstile> ?\<Gamma> \<Rightarrow> ?\<Delta>
\<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}

goal (1 subgoal):
 1. \<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Gamma>'' \<Rightarrow> F, {#}

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
with SCND
[PROOF STATE]
proof (chain)
picking this:
?\<Gamma> \<Rightarrow> ?\<Delta> \<Longrightarrow> set_mset ?\<Gamma> \<union> \<^bold>\<not> ` set_mset ?\<Delta> \<turnstile> \<bottom>
\<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
have "set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset {#F#} \<turnstile> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
?\<Gamma> \<Rightarrow> ?\<Delta> \<Longrightarrow> set_mset ?\<Gamma> \<union> \<^bold>\<not> ` set_mset ?\<Delta> \<turnstile> \<bottom>
\<Gamma>'' \<Rightarrow> F, {#}

goal (1 subgoal):
 1. set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
thus ?n
[PROOF STATE]
proof (prove)
using this:
set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<turnstile> F
[PROOF STEP]
using ND.CC Weaken[OF _ su[THEN insert_mono]]
[PROOF STATE]
proof (prove)
using this:
set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>
\<^bold>\<not> ?F \<triangleright> ?\<Gamma> \<turnstile> \<bottom> \<Longrightarrow> ?\<Gamma> \<turnstile> ?F
?a1 \<triangleright> set_mset \<Gamma>'' \<turnstile> ?F \<Longrightarrow> ?a1 \<triangleright> \<Gamma> \<turnstile> ?F

goal (1 subgoal):
 1. \<Gamma> \<turnstile> F
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ND_sound_complete_finite:
  assumes "finite \<Gamma>"
  shows "\<Gamma> \<turnstile> F \<longleftrightarrow> \<Gamma> \<TTurnstile> F" (is "?n \<longleftrightarrow> ?s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma> \<turnstile> F) = \<Gamma> \<TTurnstile> F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma> \<turnstile> F \<Longrightarrow> \<Gamma> \<TTurnstile> F
 2. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
assume ?n
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> F

goal (2 subgoals):
 1. \<Gamma> \<turnstile> F \<Longrightarrow> \<Gamma> \<TTurnstile> F
 2. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
thus ?s
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> F

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F
[PROOF STEP]
by (fact ND_sound)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<TTurnstile> F

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
assume s: ?s
[PROOF STATE]
proof (state)
this:
\<Gamma> \<TTurnstile> F

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<TTurnstile> F
[PROOF STEP]
obtain \<Gamma>'' where \<Gamma>'': "\<Gamma> = set_mset \<Gamma>''"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<TTurnstile> F

goal (1 subgoal):
 1. (\<And>\<Gamma>''. \<Gamma> = set_mset \<Gamma>'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_set_mset_mset_set assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<TTurnstile> F
finite ?A \<Longrightarrow> set_mset (mset_set ?A) = ?A
finite \<Gamma>

goal (1 subgoal):
 1. (\<And>\<Gamma>''. \<Gamma> = set_mset \<Gamma>'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Gamma> = set_mset \<Gamma>''

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
have su: "set_mset \<Gamma>'' \<subseteq> \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset \<Gamma>'' \<subseteq> \<Gamma>
[PROOF STEP]
using \<Gamma>''
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = set_mset \<Gamma>''

goal (1 subgoal):
 1. set_mset \<Gamma>'' \<subseteq> \<Gamma>
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
set_mset \<Gamma>'' \<subseteq> \<Gamma>

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
have "\<Turnstile> \<Gamma>'' \<Rightarrow> {#F#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<TTurnstile> F

goal (1 subgoal):
 1. \<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
unfolding sequent_semantics_def entailment_def \<Gamma>''
[PROOF STATE]
proof (prove)
using this:
\<forall>\<A>. (\<forall>G\<in>#\<Gamma>''. \<A> \<Turnstile> G) \<longrightarrow> \<A> \<Turnstile> F

goal (1 subgoal):
 1. \<forall>A. (\<forall>\<gamma>\<in>#\<Gamma>''. A \<Turnstile> \<gamma>) \<longrightarrow> (\<exists>\<delta>\<in>#F, {#}. A \<Turnstile> \<delta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
with SC_sound_complete
[PROOF STATE]
proof (chain)
picking this:
?\<Gamma> \<Rightarrow> ?\<Delta> = \<Turnstile> ?\<Gamma> \<Rightarrow> ?\<Delta>
\<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
have "\<Gamma>'' \<Rightarrow> {#F#}"
[PROOF STATE]
proof (prove)
using this:
?\<Gamma> \<Rightarrow> ?\<Delta> = \<Turnstile> ?\<Gamma> \<Rightarrow> ?\<Delta>
\<Turnstile> \<Gamma>'' \<Rightarrow> F, {#}

goal (1 subgoal):
 1. \<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Gamma>'' \<Rightarrow> F, {#}

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
with SCND
[PROOF STATE]
proof (chain)
picking this:
?\<Gamma> \<Rightarrow> ?\<Delta> \<Longrightarrow> set_mset ?\<Gamma> \<union> \<^bold>\<not> ` set_mset ?\<Delta> \<turnstile> \<bottom>
\<Gamma>'' \<Rightarrow> F, {#}
[PROOF STEP]
have "set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset {#F#} \<turnstile> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
?\<Gamma> \<Rightarrow> ?\<Delta> \<Longrightarrow> set_mset ?\<Gamma> \<union> \<^bold>\<not> ` set_mset ?\<Delta> \<turnstile> \<bottom>
\<Gamma>'' \<Rightarrow> F, {#}

goal (1 subgoal):
 1. set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<TTurnstile> F \<Longrightarrow> \<Gamma> \<turnstile> F
[PROOF STEP]
thus ?n
[PROOF STATE]
proof (prove)
using this:
set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<turnstile> F
[PROOF STEP]
using ND.CC Weaken[OF _ su[THEN insert_mono]]
[PROOF STATE]
proof (prove)
using this:
set_mset \<Gamma>'' \<union> \<^bold>\<not> ` set_mset (F, {#}) \<turnstile> \<bottom>
\<^bold>\<not> ?F \<triangleright> ?\<Gamma> \<turnstile> \<bottom> \<Longrightarrow> ?\<Gamma> \<turnstile> ?F
?a1 \<triangleright> set_mset \<Gamma>'' \<turnstile> ?F \<Longrightarrow> ?a1 \<triangleright> \<Gamma> \<turnstile> ?F

goal (1 subgoal):
 1. \<Gamma> \<turnstile> F
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isSng_correct_exists1 :
    "invar s \<Longrightarrow> (isSng s \<longleftrightarrow> (\<exists>!e. (e \<in> \<alpha> s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar s \<Longrightarrow> isSng s = (\<exists>!e. e \<in> \<alpha> s)
[PROOF STEP]
by (auto simp add: isSng_correct)


[STATEMENT]
lemma isSng_correct_card :
    "invar s \<Longrightarrow> (isSng s \<longleftrightarrow> (card (\<alpha> s) = 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar s \<Longrightarrow> isSng s = (card (\<alpha> s) = 1)
[PROOF STEP]
by (auto simp add: isSng_correct card_Suc_eq)


[STATEMENT]
lemma iteratei_correct: "invar S \<Longrightarrow> set_iterator (iteratei S) (\<alpha> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator (iteratei S) (\<alpha> S)
[PROOF STEP]
unfolding iteratei_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator (it_to_it (list_it S)) (\<alpha> S)
[PROOF STEP]
apply (rule it_to_it_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator (list_it S) (\<alpha> S)
[PROOF STEP]
by (rule list_it_correct)


[STATEMENT]
lemma pi_iteratei[icf_proper_iteratorI]:
    "proper_it (iteratei S) (iteratei S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (iteratei S) (iteratei S)
[PROOF STEP]
unfolding iteratei_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (it_to_it (list_it S)) (it_to_it (list_it S))
[PROOF STEP]
by (intro icf_proper_iteratorI)


[STATEMENT]
lemma iteratei_rule_P:
    "\<lbrakk>
      invar S;
      I (\<alpha> S) \<sigma>0;
      !!x it \<sigma>. \<lbrakk> c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>);
      !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>;
      !!\<sigma> it. \<lbrakk> it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (iteratei S c f \<sigma>0)
[PROOF STEP]
apply (rule set_iterator_rule_P [OF iteratei_correct, of S I \<sigma>0 c f P])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> invar S
 2. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> I (\<alpha> S) \<sigma>0
 3. \<And>Sa \<sigma> x. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>; c \<sigma>; x \<in> Sa; I Sa \<sigma>; Sa \<subseteq> \<alpha> S\<rbrakk> \<Longrightarrow> I (Sa - {x}) (f x \<sigma>)
 4. \<And>\<sigma>. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>; I {} \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 5. \<And>\<sigma> Sa. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>; Sa \<subseteq> \<alpha> S; Sa \<noteq> {}; \<not> c \<sigma>; I Sa \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iteratei_rule_insert_P:
    "\<lbrakk>
      invar S;
      I {} \<sigma>0;
      !!x it \<sigma>. \<lbrakk> c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (insert x it) (f x \<sigma>);
      !!\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>;
      !!\<sigma> it. \<lbrakk> it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (iteratei S c f \<sigma>0)
[PROOF STEP]
apply (rule
      set_iterator_rule_insert_P[OF iteratei_correct, of S I \<sigma>0 c f P])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> invar S
 2. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> I {} \<sigma>0
 3. \<And>Sa \<sigma> x. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>; c \<sigma>; x \<in> \<alpha> S - Sa; I Sa \<sigma>; Sa \<subseteq> \<alpha> S\<rbrakk> \<Longrightarrow> I (set_ins x Sa) (f x \<sigma>)
 4. \<And>\<sigma>. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>; I (\<alpha> S) \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
 5. \<And>\<sigma> Sa. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>; \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>; Sa \<subseteq> \<alpha> S; Sa \<noteq> \<alpha> S; \<not> c \<sigma>; I Sa \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_rule_P:
    "\<lbrakk>
      invar S;
      I (\<alpha> S) \<sigma>0;
      !!x it \<sigma>. \<lbrakk> x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>);
      !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S (\<lambda>_. True) f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (iterate S f \<sigma>0)
[PROOF STEP]
apply (rule set_iterator_no_cond_rule_P [OF iteratei_correct, of S I \<sigma>0 f P])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> invar S
 2. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> I (\<alpha> S) \<sigma>0
 3. \<And>Sa \<sigma> x. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; x \<in> Sa; I Sa \<sigma>; Sa \<subseteq> \<alpha> S\<rbrakk> \<Longrightarrow> I (Sa - {x}) (f x \<sigma>)
 4. \<And>\<sigma>. \<lbrakk>invar S; I (\<alpha> S) \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>; I {} \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterate_rule_insert_P:
    "\<lbrakk>
      invar S;
      I {} \<sigma>0;
      !!x it \<sigma>. \<lbrakk> x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (insert x it) (f x \<sigma>);
      !!\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S (\<lambda>_. True) f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (iterate S f \<sigma>0)
[PROOF STEP]
apply (rule set_iterator_no_cond_rule_insert_P [OF iteratei_correct,
      of S I \<sigma>0 f P])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> invar S
 2. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> I {} \<sigma>0
 3. \<And>Sa \<sigma> x. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>; x \<in> \<alpha> S - Sa; I Sa \<sigma>; Sa \<subseteq> \<alpha> S\<rbrakk> \<Longrightarrow> I (set_ins x Sa) (f x \<sigma>)
 4. \<And>\<sigma>. \<lbrakk>invar S; I {} \<sigma>0; \<And>x it \<sigma>. \<lbrakk>x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma>\<rbrakk> \<Longrightarrow> I (set_ins x it) (f x \<sigma>); \<And>\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>; I (\<alpha> S) \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma image_filter_correct_aux2:
    "invar1 s \<Longrightarrow>
    \<alpha>2 (image_filter (\<lambda>x. if P x then (Some (f x)) else None) s)
    = f ` {x\<in>\<alpha>1 s. P x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar1 s \<Longrightarrow> \<alpha>2 (image_filter (\<lambda>x. if P x then Some (f x) else None) s) = f ` {x \<in> \<alpha>1 s. P x}
[PROOF STEP]
by (auto simp add: image_filter_correct_aux)


[STATEMENT]
lemma disjoint_witness_None: "\<lbrakk>invar1 s1; invar2 s2\<rbrakk>
    \<Longrightarrow> disjoint_witness s1 s2 = None \<longleftrightarrow> \<alpha>1 s1 \<inter> \<alpha>2 s2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar1 s1; invar2 s2\<rbrakk> \<Longrightarrow> (disjoint_witness s1 s2 = None) = (\<alpha>1 s1 \<inter> \<alpha>2 s2 = {})
[PROOF STEP]
by (case_tac "disjoint_witness s1 s2")
       (auto dest: disjoint_witness_correct)


[STATEMENT]
lemma disjoint_witnessI: "\<lbrakk>
    invar1 s1;
    invar2 s2;
    \<alpha>1 s1 \<inter> \<alpha>2 s2 \<noteq> {};
    !!a. \<lbrakk>disjoint_witness s1 s2 = Some a\<rbrakk> \<Longrightarrow> P
                            \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar1 s1; invar2 s2; \<alpha>1 s1 \<inter> \<alpha>2 s2 \<noteq> {}; \<And>a. disjoint_witness s1 s2 = Some a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (case_tac "disjoint_witness s1 s2")
       (auto dest: disjoint_witness_correct)


[STATEMENT]
lemma sel_someD:
    "\<lbrakk> invar s; sel s f = Some r; !!x. \<lbrakk>x\<in>\<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (cases "\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P; \<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>invar s; sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P; \<not> (\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r)\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x ra. \<lbrakk>invar s; sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P; x \<in> \<alpha> s; f x = Some ra\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>invar s; sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P; \<not> (\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r)\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (erule_tac f=f and x=x in selE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x ra. \<lbrakk>sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P; x \<in> \<alpha> s; f x = Some ra\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<And>x ra. \<lbrakk>sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P; x \<in> \<alpha> s; f x = Some ra\<rbrakk> \<Longrightarrow> f x = Some (?r3 x ra)
 3. \<And>x ra xa raa. \<lbrakk>sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P; x \<in> \<alpha> s; f x = Some ra; sel s f = Some raa; xa \<in> \<alpha> s; f xa = Some raa\<rbrakk> \<Longrightarrow> P
 4. \<lbrakk>invar s; sel s f = Some r; \<And>x. \<lbrakk>x \<in> \<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P; \<not> (\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r)\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; sel s f = Some r; \<forall>x\<in>\<alpha> s. f x = None\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (drule (1) selI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sel s f = Some r; \<forall>x\<in>\<alpha> s. f x = None; sel s f = None\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sel_noneD:
    "\<lbrakk> invar s; sel s f = None; x\<in>\<alpha> s \<rbrakk> \<Longrightarrow> f x = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; sel s f = None; x \<in> \<alpha> s\<rbrakk> \<Longrightarrow> f x = None
[PROOF STEP]
apply (cases "\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; sel s f = None; x \<in> \<alpha> s; \<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r\<rbrakk> \<Longrightarrow> f x = None
 2. \<lbrakk>invar s; sel s f = None; x \<in> \<alpha> s; \<not> (\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r)\<rbrakk> \<Longrightarrow> f x = None
[PROOF STEP]
apply (safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa r. \<lbrakk>invar s; sel s f = None; x \<in> \<alpha> s; xa \<in> \<alpha> s; f xa = Some r\<rbrakk> \<Longrightarrow> f x = None
 2. \<lbrakk>invar s; sel s f = None; x \<in> \<alpha> s; \<not> (\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r)\<rbrakk> \<Longrightarrow> f x = None
[PROOF STEP]
apply (erule_tac f=f and x=xa in selE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa r. \<lbrakk>sel s f = None; x \<in> \<alpha> s; xa \<in> \<alpha> s; f xa = Some r\<rbrakk> \<Longrightarrow> xa \<in> \<alpha> s
 2. \<And>xa r. \<lbrakk>sel s f = None; x \<in> \<alpha> s; xa \<in> \<alpha> s; f xa = Some r\<rbrakk> \<Longrightarrow> f xa = Some (?r3 xa r)
 3. \<And>xa r xaa ra. \<lbrakk>sel s f = None; x \<in> \<alpha> s; xa \<in> \<alpha> s; f xa = Some r; sel s f = Some ra; xaa \<in> \<alpha> s; f xaa = Some ra\<rbrakk> \<Longrightarrow> f x = None
 4. \<lbrakk>invar s; sel s f = None; x \<in> \<alpha> s; \<not> (\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r)\<rbrakk> \<Longrightarrow> f x = None
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sel'_someD:
    "\<lbrakk> invar s; sel' s P = Some x \<rbrakk> \<Longrightarrow> x\<in>\<alpha> s \<and> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; sel' s P = Some x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s \<and> P x
[PROOF STEP]
apply (cases "\<exists>x\<in>\<alpha> s. P x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; sel' s P = Some x; \<exists>x\<in>\<alpha> s. P x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s \<and> P x
 2. \<lbrakk>invar s; sel' s P = Some x; \<not> (\<exists>x\<in>\<alpha> s. P x)\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s \<and> P x
[PROOF STEP]
apply (safe)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>invar s; sel' s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<And>xa. \<lbrakk>invar s; sel' s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; sel' s P = Some x; \<not> (\<exists>x\<in>\<alpha> s. P x)\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 4. \<lbrakk>invar s; sel' s P = Some x; \<not> (\<exists>x\<in>\<alpha> s. P x)\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply (erule_tac P=P and x=xa in sel'E)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>xa. \<lbrakk>sel' s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> xa \<in> \<alpha> s
 2. \<And>xa. \<lbrakk>sel' s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> P xa
 3. \<And>xa xaa. \<lbrakk>sel' s P = Some x; xa \<in> \<alpha> s; P xa; sel' s P = Some xaa; xaa \<in> \<alpha> s; P xaa\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 4. \<And>xa. \<lbrakk>invar s; sel' s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> P x
 5. \<lbrakk>invar s; sel' s P = Some x; \<not> (\<exists>x\<in>\<alpha> s. P x)\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 6. \<lbrakk>invar s; sel' s P = Some x; \<not> (\<exists>x\<in>\<alpha> s. P x)\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>invar s; sel' s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 3. \<lbrakk>invar s; sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply (erule_tac P=P and x=xa in sel'E)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>xa. \<lbrakk>sel' s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> xa \<in> \<alpha> s
 2. \<And>xa. \<lbrakk>sel' s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> P xa
 3. \<And>xa xaa. \<lbrakk>sel' s P = Some x; xa \<in> \<alpha> s; P xa; sel' s P = Some xaa; xaa \<in> \<alpha> s; P xaa\<rbrakk> \<Longrightarrow> P x
 4. \<lbrakk>invar s; sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 5. \<lbrakk>invar s; sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply (drule (1) sel'I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x; sel' s P = None\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply (drule (1) sel'I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sel' s P = Some x; \<forall>x\<in>\<alpha> s. \<not> P x; sel' s P = None\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sel'_noneD:
    "\<lbrakk> invar s; sel' s P = None; x\<in>\<alpha> s \<rbrakk> \<Longrightarrow> \<not>P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; sel' s P = None; x \<in> \<alpha> s\<rbrakk> \<Longrightarrow> \<not> P x
[PROOF STEP]
apply (cases "\<exists>x\<in>\<alpha> s. P x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; sel' s P = None; x \<in> \<alpha> s; \<exists>x\<in>\<alpha> s. P x\<rbrakk> \<Longrightarrow> \<not> P x
 2. \<lbrakk>invar s; sel' s P = None; x \<in> \<alpha> s; \<not> (\<exists>x\<in>\<alpha> s. P x)\<rbrakk> \<Longrightarrow> \<not> P x
[PROOF STEP]
apply (safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>invar s; sel' s P = None; x \<in> \<alpha> s; xa \<in> \<alpha> s; P xa; P x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>invar s; sel' s P = None; x \<in> \<alpha> s; \<not> (\<exists>x\<in>\<alpha> s. P x); P x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule_tac P=P and x=xa in sel'E)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>sel' s P = None; x \<in> \<alpha> s; xa \<in> \<alpha> s; P xa; P x\<rbrakk> \<Longrightarrow> xa \<in> \<alpha> s
 2. \<And>xa. \<lbrakk>sel' s P = None; x \<in> \<alpha> s; xa \<in> \<alpha> s; P xa; P x\<rbrakk> \<Longrightarrow> P xa
 3. \<And>xa xaa. \<lbrakk>sel' s P = None; x \<in> \<alpha> s; xa \<in> \<alpha> s; P xa; P x; sel' s P = Some xaa; xaa \<in> \<alpha> s; P xaa\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>invar s; sel' s P = None; x \<in> \<alpha> s; \<not> (\<exists>x\<in>\<alpha> s. P x); P x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iterateoi_correct:
    "invar S \<Longrightarrow> set_iterator_linord (iterateoi S) (\<alpha> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator_linord (iterateoi S) (\<alpha> S)
[PROOF STEP]
unfolding iterateoi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator_linord (it_to_it (list_ordered_it S)) (\<alpha> S)
[PROOF STEP]
apply (rule it_to_it_linord_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator_linord (list_ordered_it S) (\<alpha> S)
[PROOF STEP]
by (rule list_ordered_it_correct)


[STATEMENT]
lemma pi_iterateoi[icf_proper_iteratorI]:
    "proper_it (iterateoi S) (iterateoi S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (iterateoi S) (iterateoi S)
[PROOF STEP]
unfolding iterateoi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (it_to_it (list_ordered_it S)) (it_to_it (list_ordered_it S))
[PROOF STEP]
by (intro icf_proper_iteratorI)


[STATEMENT]
lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
    assumes MINV: "invar s"
    assumes I0: "I (\<alpha> s) \<sigma>0"
    assumes IP: "!!k it \<sigma>. \<lbrakk>
      c \<sigma>;
      k \<in> it;
      \<forall>j\<in>it. k\<le>j;
      \<forall>j\<in>\<alpha> s - it. j\<le>k;
      it \<subseteq> \<alpha> s;
      I it \<sigma>
    \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
    assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
    assumes II: "!!\<sigma> it. \<lbrakk>
      it \<subseteq> \<alpha> s;
      it \<noteq> {};
      \<not> c \<sigma>;
      I it \<sigma>;
      \<forall>k\<in>it. \<forall>j\<in>\<alpha> s - it. j\<le>k
    \<rbrakk> \<Longrightarrow> P \<sigma>"
    shows "P (iterateoi s c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iterateoi s c f \<sigma>0)
[PROOF STEP]
using set_iterator_linord_rule_P [OF iterateoi_correct,
    OF MINV, of I \<sigma>0 c f P, OF I0 _ IF] IP II
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> \<alpha> s; \<And>x'. x' \<in> \<alpha> s - S \<Longrightarrow> x' \<le> x; \<And>x'. x' \<in> S \<Longrightarrow> x \<le> x'\<rbrakk> \<Longrightarrow> I (S - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> I {} \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> \<alpha> s; S \<noteq> {}; \<And>x x'. \<lbrakk>x \<in> S; x' \<in> \<alpha> s - S\<rbrakk> \<Longrightarrow> x' \<le> x; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (iterateoi s c f \<sigma>0)
\<lbrakk>c ?\<sigma>2; ?k2 \<in> ?it2; \<forall>j\<in>?it2. ?k2 \<le> j; \<forall>j\<in>\<alpha> s - ?it2. j \<le> ?k2; ?it2 \<subseteq> \<alpha> s; I ?it2 ?\<sigma>2\<rbrakk> \<Longrightarrow> I (?it2 - {?k2}) (f ?k2 ?\<sigma>2)
\<lbrakk>?it2 \<subseteq> \<alpha> s; ?it2 \<noteq> {}; \<not> c ?\<sigma>2; I ?it2 ?\<sigma>2; \<forall>k\<in>?it2. \<forall>j\<in>\<alpha> s - ?it2. j \<le> k\<rbrakk> \<Longrightarrow> P ?\<sigma>2

goal (1 subgoal):
 1. P (iterateoi s c f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
    assumes MINV: "invar s"
    assumes I0: "I ((\<alpha> s)) \<sigma>0"
    assumes IP: "!!k it \<sigma>. \<lbrakk> k \<in> it; \<forall>j\<in>it. k\<le>j;
        \<forall>j\<in>(\<alpha> s) - it. j\<le>k; it \<subseteq> (\<alpha> s); I it \<sigma> \<rbrakk>
      \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
    assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
  shows "P (iterateo s f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (iterateo s f \<sigma>0)
[PROOF STEP]
apply (rule iterateoi_rule_P [where I = I])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. invar s
 2. I (\<alpha> s) \<sigma>0
 3. \<And>k it \<sigma>. \<lbrakk>True; k \<in> it; \<forall>j\<in>it. k \<le> j; \<forall>j\<in>\<alpha> s - it. j \<le> k; it \<subseteq> \<alpha> s; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)
 4. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 5. \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> s; it \<noteq> {}; \<not> True; I it \<sigma>; \<forall>k\<in>it. \<forall>j\<in>\<alpha> s - it. j \<le> k\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply (simp_all add: assms)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rev_iterateoi_correct:
    "invar S \<Longrightarrow> set_iterator_rev_linord (rev_iterateoi S) (\<alpha> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator_rev_linord (reverse_iterateoi S) (\<alpha> S)
[PROOF STEP]
unfolding rev_iterateoi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator_rev_linord (it_to_it (list_rev_it S)) (\<alpha> S)
[PROOF STEP]
apply (rule it_to_it_rev_linord_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar S \<Longrightarrow> set_iterator_rev_linord (list_rev_it S) (\<alpha> S)
[PROOF STEP]
by (rule list_rev_it_correct)


[STATEMENT]
lemma pi_rev_iterateoi[icf_proper_iteratorI]:
    "proper_it (rev_iterateoi S) (rev_iterateoi S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (reverse_iterateoi S) (reverse_iterateoi S)
[PROOF STEP]
unfolding rev_iterateoi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (it_to_it (list_rev_it S)) (it_to_it (list_rev_it S))
[PROOF STEP]
by (intro icf_proper_iteratorI)


[STATEMENT]
lemma rev_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
    assumes MINV: "invar s"
    assumes I0: "I ((\<alpha> s)) \<sigma>0"
    assumes IP: "!!k it \<sigma>. \<lbrakk>
      c \<sigma>;
      k \<in> it;
      \<forall>j\<in>it. k\<ge>j;
      \<forall>j\<in>(\<alpha> s) - it. j\<ge>k;
      it \<subseteq> (\<alpha> s);
      I it \<sigma>
    \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
    assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
    assumes II: "!!\<sigma> it. \<lbrakk>
      it \<subseteq> (\<alpha> s);
      it \<noteq> {};
      \<not> c \<sigma>;
      I it \<sigma>;
      \<forall>k\<in>it. \<forall>j\<in>(\<alpha> s) - it. j\<ge>k
    \<rbrakk> \<Longrightarrow> P \<sigma>"
  shows "P (rev_iterateoi s c f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (reverse_iterateoi s c f \<sigma>0)
[PROOF STEP]
using set_iterator_rev_linord_rule_P [OF rev_iterateoi_correct,
    OF MINV, of I \<sigma>0 c f P, OF I0 _ IF] IP II
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>S \<sigma> x. \<lbrakk>c \<sigma>; x \<in> S; I S \<sigma>; S \<subseteq> \<alpha> s; \<And>x'. x' \<in> \<alpha> s - S \<Longrightarrow> x \<le> x'; \<And>x'. x' \<in> S \<Longrightarrow> x' \<le> x\<rbrakk> \<Longrightarrow> I (S - {x}) (f x \<sigma>); \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> I {} \<sigma>; \<And>\<sigma> S. \<lbrakk>S \<subseteq> \<alpha> s; S \<noteq> {}; \<And>x x'. \<lbrakk>x \<in> S; x' \<in> \<alpha> s - S\<rbrakk> \<Longrightarrow> x \<le> x'; \<not> c \<sigma>; I S \<sigma>\<rbrakk> \<Longrightarrow> P \<sigma>\<rbrakk> \<Longrightarrow> P (reverse_iterateoi s c f \<sigma>0)
\<lbrakk>c ?\<sigma>4; ?k4 \<in> ?it4; \<forall>j\<in>?it4. j \<le> ?k4; \<forall>j\<in>\<alpha> s - ?it4. ?k4 \<le> j; ?it4 \<subseteq> \<alpha> s; I ?it4 ?\<sigma>4\<rbrakk> \<Longrightarrow> I (?it4 - {?k4}) (f ?k4 ?\<sigma>4)
\<lbrakk>?it4 \<subseteq> \<alpha> s; ?it4 \<noteq> {}; \<not> c ?\<sigma>4; I ?it4 ?\<sigma>4; \<forall>k\<in>?it4. \<forall>j\<in>\<alpha> s - ?it4. k \<le> j\<rbrakk> \<Longrightarrow> P ?\<sigma>4

goal (1 subgoal):
 1. P (reverse_iterateoi s c f \<sigma>0)
[PROOF STEP]
by simp


[STATEMENT]
lemma reverse_iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
    assumes MINV: "invar s"
    assumes I0: "I ((\<alpha> s)) \<sigma>0"
    assumes IP: "!!k it \<sigma>. \<lbrakk>
      k \<in> it;
      \<forall>j\<in>it. k\<ge>j;
      \<forall>j\<in> (\<alpha> s) - it. j\<ge>k;
      it \<subseteq> (\<alpha> s);
      I it \<sigma>
    \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
    assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
  shows "P (rev_iterateo s f \<sigma>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (reverse_iterateo s f \<sigma>0)
[PROOF STEP]
apply (rule rev_iterateoi_rule_P [where I = I])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. invar s
 2. I (\<alpha> s) \<sigma>0
 3. \<And>k it \<sigma>. \<lbrakk>True; k \<in> it; \<forall>j\<in>it. j \<le> k; \<forall>j\<in>\<alpha> s - it. k \<le> j; it \<subseteq> \<alpha> s; I it \<sigma>\<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)
 4. \<And>\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
 5. \<And>\<sigma> it. \<lbrakk>it \<subseteq> \<alpha> s; it \<noteq> {}; \<not> True; I it \<sigma>; \<forall>k\<in>it. \<forall>j\<in>\<alpha> s - it. k \<le> j\<rbrakk> \<Longrightarrow> P \<sigma>
[PROOF STEP]
apply (simp_all add: assms)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma minE:
     assumes A: "invar s" "x\<in>\<alpha> s" "P x"
     obtains x' where
     "min s P = Some x'" "x'\<in>\<alpha> s" "P x'" "\<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>min s P = Some x'; x' \<in> \<alpha> s; P x'; \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<le> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>min s P = Some x'; x' \<in> \<alpha> s; P x'; \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<le> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from min_correct(1)[of s x P, OF A]
[PROOF STATE]
proof (chain)
picking this:
min s P \<in> Some ` {x \<in> \<alpha> s. P x}
[PROOF STEP]
have
       MIS: "min s P \<in> Some ` {x \<in> \<alpha> s. P x}"
[PROOF STATE]
proof (prove)
using this:
min s P \<in> Some ` {x \<in> \<alpha> s. P x}

goal (1 subgoal):
 1. min s P \<in> Some ` {x \<in> \<alpha> s. P x}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
min s P \<in> Some ` {x \<in> \<alpha> s. P x}

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>min s P = Some x'; x' \<in> \<alpha> s; P x'; \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<le> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
min s P \<in> Some ` {x \<in> \<alpha> s. P x}
[PROOF STEP]
obtain x' where KV: "min s P = Some x'" "x'\<in>\<alpha> s" "P x'"
[PROOF STATE]
proof (prove)
using this:
min s P \<in> Some ` {x \<in> \<alpha> s. P x}

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>min s P = Some x'; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min s P = Some x'
x' \<in> \<alpha> s
P x'

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>min s P = Some x'; x' \<in> \<alpha> s; P x'; \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<le> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (rule that[OF KV])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<le> x
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> \<alpha> s; P x\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (drule (1) min_correct(2)[OF \<open>invar s\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>P x; the (min s P) \<le> x\<rbrakk> \<Longrightarrow> x' \<le> x
[PROOF STEP]
apply (simp add: KV(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_Some:
     "\<lbrakk> invar s; min s P = Some x \<rbrakk> \<Longrightarrow> x\<in>\<alpha> s"
     "\<lbrakk> invar s; min s P = Some x \<rbrakk> \<Longrightarrow> P x"
     "\<lbrakk> invar s; min s P = Some x; x'\<in>\<alpha> s; P x'\<rbrakk> \<Longrightarrow> x\<le>x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s) &&& (\<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x) &&& (\<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x')
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (cases "{x \<in> \<alpha> s. P x} = {}")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invar s; min s P = Some x; {x \<in> \<alpha> s. P x} = {}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; min s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 3. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 4. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (drule (1) min_correct(3))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>min s P = Some x; {x \<in> \<alpha> s. P x} = {}; min s P = None\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; min s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 3. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 4. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invar s; min s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invar s; min s P = Some x; \<exists>x. x \<in> \<alpha> s \<and> P x\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>invar s; min s P = Some x; xa \<in> \<alpha> s \<and> P xa\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>invar s; min s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (drule (2) min_correct(1)[of s _ P])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>min s P = Some x; xa \<in> \<alpha> s; P xa; min s P \<in> Some ` {x \<in> \<alpha> s. P x}\<rbrakk> \<Longrightarrow> x \<in> \<alpha> s
 2. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply auto [1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; min s P = Some x\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (cases "{x \<in> \<alpha> s. P x} = {}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invar s; min s P = Some x; {x \<in> \<alpha> s. P x} = {}\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; min s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (drule (1) min_correct(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>min s P = Some x; {x \<in> \<alpha> s. P x} = {}; min s P = None\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; min s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> P x
 3. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; min s P = Some x; {x \<in> \<alpha> s. P x} \<noteq> {}\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invar s; min s P = Some x; \<exists>x. x \<in> \<alpha> s \<and> P x\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>invar s; min s P = Some x; xa \<in> \<alpha> s \<and> P xa\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>invar s; min s P = Some x; xa \<in> \<alpha> s; P xa\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (drule (2) min_correct(1)[of s _ P])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>min s P = Some x; xa \<in> \<alpha> s; P xa; min s P \<in> Some ` {x \<in> \<alpha> s. P x}\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply auto [1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invar s; min s P = Some x; x' \<in> \<alpha> s; P x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply (drule (2) min_correct(2)[where P=P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>min s P = Some x; x' \<in> \<alpha> s; P x'; the (min s P) \<le> x'\<rbrakk> \<Longrightarrow> x \<le> x'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done