theory Trace_More_RG

lemma rg_set_preserved:
  assumes x: "\<And>x. \<lbrace>fn' x\<rbrace>,\<lbrace>R\<rbrace> m -,\<lbrace>\<lambda>rv. fn x\<rbrace>"
  shows      "\<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>,\<lbrace>R\<rbrace> m -,\<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace>" apply (induct xs) apply (simp add: rg_TrueI validI_prefix_closed[OF x]) apply simp apply (rule rg_vcg_conj_lift) apply (rule x) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s0 s. set [] \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set [] \<subseteq> {x. fn x s0 s}\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. set (a # xs) \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set (a # xs) \<subseteq> {x. fn x s0 s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. set (a # xs) \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set (a # xs) \<subseteq> {x. fn x s0 s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. fn' a s0 s \<and> set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. fn a s0 s \<and> set xs \<subseteq> {x. fn x s0 s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> \<Longrightarrow> \<lbrace>fn' a\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv. fn a\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. set xs \<subseteq> {x. fn' x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>rv s0 s. set xs \<subseteq> {x. fn x s0 s}\<rbrace> proof (prove)
goal:
No subgoals!