theory Retype_DP

lemma detype_set_sep_helper:
  "finite S \<Longrightarrow> <(\<And>* x\<in> S. x \<mapsto>o -) \<and>* R> s
   \<Longrightarrow> <(\<And>* x \<in> S. x \<mapsto>o Untyped) \<and>* R> (detype S s)" proof (induct arbitrary: R rule: finite_induct) case empty show ?case using empty by (simp add: detype_def) next case (insert a A) show ?case using insert.hyps(1-2) insert.prems apply (subst detype_insert) apply (simp add: ) apply (subst sep_conj_assoc) apply (rule detype_one_wp) apply (sep_select 2) apply (rule insert.hyps(3)) apply sep_solve done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; cdl.lift (sep_map_set_conj sep_any_map_o S \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ x:S. x \<mapsto>o Untyped) \<and>* R) (detype S s) proof (state)
goal (2 subgoals):
 1. \<And>R. cdl.lift (sep_map_set_conj sep_any_map_o {} \<and>* R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:{}. x \<mapsto>o Untyped) \<and>* R) (detype {} s)
 2. \<And>x F R. \<lbrakk>finite F; x \<notin> F; \<And>R. cdl.lift (sep_map_set_conj sep_any_map_o F \<and>* R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:F. x \<mapsto>o Untyped) \<and>* R) (detype F s); cdl.lift (sep_map_set_conj sep_any_map_o (insert x F) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ x:insert x F. x \<mapsto>o Untyped) \<and>* R) (detype (insert x F) s) proof (state)
this:
cdl.lift (sep_map_set_conj sep_any_map_o {} \<and>* R) s

goal (2 subgoals):
 1. \<And>R. cdl.lift (sep_map_set_conj sep_any_map_o {} \<and>* R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:{}. x \<mapsto>o Untyped) \<and>* R) (detype {} s)
 2. \<And>x F R. \<lbrakk>finite F; x \<notin> F; \<And>R. cdl.lift (sep_map_set_conj sep_any_map_o F \<and>* R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:F. x \<mapsto>o Untyped) \<and>* R) (detype F s); cdl.lift (sep_map_set_conj sep_any_map_o (insert x F) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ x:insert x F. x \<mapsto>o Untyped) \<and>* R) (detype (insert x F) s) proof (prove)
goal (1 subgoal):
 1. cdl.lift ((SETSEPCONJ x:{}. x \<mapsto>o Untyped) \<and>* R) (detype {} s) proof (prove)
using this:
cdl.lift (sep_map_set_conj sep_any_map_o {} \<and>* R) s

goal (1 subgoal):
 1. cdl.lift ((SETSEPCONJ x:{}. x \<mapsto>o Untyped) \<and>* R) (detype {} s) proof (state)
this:
cdl.lift ((SETSEPCONJ x:{}. x \<mapsto>o Untyped) \<and>* R) (detype {} s)

goal (1 subgoal):
 1. \<And>x F R. \<lbrakk>finite F; x \<notin> F; \<And>R. cdl.lift (sep_map_set_conj sep_any_map_o F \<and>* R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:F. x \<mapsto>o Untyped) \<and>* R) (detype F s); cdl.lift (sep_map_set_conj sep_any_map_o (insert x F) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ x:insert x F. x \<mapsto>o Untyped) \<and>* R) (detype (insert x F) s) proof (state)
goal (1 subgoal):
 1. \<And>x F R. \<lbrakk>finite F; x \<notin> F; \<And>R. cdl.lift (sep_map_set_conj sep_any_map_o F \<and>* R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:F. x \<mapsto>o Untyped) \<and>* R) (detype F s); cdl.lift (sep_map_set_conj sep_any_map_o (insert x F) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ x:insert x F. x \<mapsto>o Untyped) \<and>* R) (detype (insert x F) s) proof (state)
this:
finite A
a \<notin> A
cdl.lift (sep_map_set_conj sep_any_map_o A \<and>* ?R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:A. x \<mapsto>o Untyped) \<and>* ?R) (detype A s)
cdl.lift (sep_map_set_conj sep_any_map_o (insert a A) \<and>* R) s

goal (1 subgoal):
 1. \<And>x F R. \<lbrakk>finite F; x \<notin> F; \<And>R. cdl.lift (sep_map_set_conj sep_any_map_o F \<and>* R) s \<Longrightarrow> cdl.lift ((SETSEPCONJ x:F. x \<mapsto>o Untyped) \<and>* R) (detype F s); cdl.lift (sep_map_set_conj sep_any_map_o (insert x F) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ x:insert x F. x \<mapsto>o Untyped) \<and>* R) (detype (insert x F) s) proof (prove)
goal (1 subgoal):
 1. cdl.lift ((SETSEPCONJ x:insert a A. x \<mapsto>o Untyped) \<and>* R) (detype (insert a A) s) proof (prove)
using this:
finite A
a \<notin> A
cdl.lift (sep_map_set_conj sep_any_map_o (insert a A) \<and>* R) s

goal (1 subgoal):
 1. cdl.lift ((SETSEPCONJ x:insert a A. x \<mapsto>o Untyped) \<and>* R) (detype (insert a A) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; a \<notin> A; cdl.lift (sep_map_set_conj sep_any_map_o (insert a A) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ x:insert a A. x \<mapsto>o Untyped) \<and>* R) (detype {a} (detype A s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<notin> A; cdl.lift ((a \<mapsto>o - \<and>* sep_map_set_conj sep_any_map_o A) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((a \<mapsto>o Untyped \<and>* (SETSEPCONJ x:A. x \<mapsto>o Untyped)) \<and>* R) (detype {a} (detype A s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<notin> A; cdl.lift ((a \<mapsto>o - \<and>* sep_map_set_conj sep_any_map_o A) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift (a \<mapsto>o Untyped \<and>* (SETSEPCONJ x:A. x \<mapsto>o Untyped) \<and>* R) (detype {a} (detype A s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<notin> A; cdl.lift ((a \<mapsto>o - \<and>* sep_map_set_conj sep_any_map_o A) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift (a \<mapsto>o - \<and>* (SETSEPCONJ x:A. x \<mapsto>o Untyped) \<and>* R) (detype A s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<notin> A; cdl.lift ((a \<mapsto>o - \<and>* sep_map_set_conj sep_any_map_o A) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ x:A. x \<mapsto>o Untyped) \<and>* a \<mapsto>o - \<and>* R) (detype A s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<notin> A; cdl.lift ((a \<mapsto>o - \<and>* sep_map_set_conj sep_any_map_o A) \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift (sep_map_set_conj sep_any_map_o A \<and>* a \<mapsto>o - \<and>* R) s proof (prove)
goal:
No subgoals! proof (state)
this:
cdl.lift ((SETSEPCONJ x:insert a A. x \<mapsto>o Untyped) \<and>* R) (detype (insert a A) s)

goal:
No subgoals!