theory Trace_More_RG

lemma rg_shrinks_proof:
  assumes y: "\<And>s0 s. finite (S s0 s)"
  assumes x: "\<And>x. \<lbrace>\<lambda>s0 s. x \<notin> S s0 s \<and> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. x \<notin> S s0 s\<rbrace>"
  assumes z: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. x \<notin> S s0 s\<rbrace>"
  assumes w: "\<And>s0 s. P s0 s \<Longrightarrow> x \<in> S s0 s"
  shows      "\<lbrace>\<lambda>s0 s. card (S s0 s) \<le> n \<and> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. card (S s0 s) < n\<rbrace>" apply (clarsimp simp: validI_def validI_prefix_closed[OF x]) apply (erule less_le_trans[rotated]) apply (rule psubset_card_mono[OF y]) apply (rule psubsetI) apply clarsimp apply (rule ccontr) apply (drule (2) use_validI[OF _ x, OF _ conjI]) apply simp by (metis use_validI w z)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. card (S s0 s) \<le> n \<and> P s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. card (S s0 s) < n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>card (S s0 s) \<le> n; P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> card (S (last_st_tr tr s0) s') < n proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> card (S (last_st_tr tr s0) s') < card (S s0 s) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> S (last_st_tr tr s0) s' \<subset> S s0 s proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> S (last_st_tr tr s0) s' \<subseteq> S s0 s
 2. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> S (last_st_tr tr s0) s' \<noteq> S s0 s proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s' x. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s; x \<in> S (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> x \<in> S s0 s
 2. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> S (last_st_tr tr s0) s' \<noteq> S s0 s proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s' x. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s; x \<in> S (last_st_tr tr s0) s'; x \<notin> S s0 s\<rbrakk> \<Longrightarrow> False
 2. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> S (last_st_tr tr s0) s' \<noteq> S s0 s proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s' x. \<lbrakk>P s0 s; x \<in> S (last_st_tr tr s0) s'; x \<notin> S s0 s; x \<notin> S (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> S (last_st_tr tr s0) s' \<noteq> S s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> S (last_st_tr tr s0) s' \<noteq> S s0 s