theory Retype_DP

lemma generate_object_ids_rv:
  "\<lbrace>K (target_type \<noteq> UntypedType) \<rbrace>
  generate_object_ids n target_type obj_range
  \<lbrace>\<lambda>r s.  r = map (\<lambda>x. {x}) (map pick r) \<and> length r = n \<and> set (map pick r) \<subseteq> obj_range
  \<and> distinct (map pick r) \<rbrace>" apply (clarsimp simp:generate_object_ids_def) apply wp apply clarsimp apply (simp add: distinct_map) apply (intro conjI) apply (clarsimp simp:Fun.comp_def) apply (rule subsetD[rotated,OF nonempty_pick_in]) apply fastforce apply fastforce apply (clarsimp simp:Fun.comp_def inj_on_def) apply (drule_tac x = xa in bspec) apply simp apply (frule_tac x = xa in bspec,simp) apply (drule_tac x = y in bspec,simp)+ apply (rule ccontr) apply clarsimp apply (drule nonempty_pick_in)+ apply clarsimp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (target_type \<noteq> UntypedType)\<rbrace> generate_object_ids n target_type obj_range \<lbrace>\<lambda>r s. r = map (\<lambda>x. {x}) (map pick r) \<and> length r = n \<and> set (map pick r) \<subseteq> obj_range \<and> distinct (map pick r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. target_type \<noteq> UntypedType\<rbrace> do s <- get;
setlist <- select {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}) \<and> n = length x};
if target_type \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) setlist else return setlist
od \<lbrace>\<lambda>r s. r = map ((\<lambda>x. {x}) \<circ> pick) r \<and> length r = n \<and> pick ` set r \<subseteq> obj_range \<and> distinct (map pick r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. target_type \<noteq> UntypedType \<Longrightarrow> \<forall>x\<in>{x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}) \<and> n = length x}. (target_type \<noteq> UntypedType \<longrightarrow> map (\<lambda>x. {pick x}) x = map ((\<lambda>x. {x}) \<circ> pick) (map (\<lambda>x. {pick x}) x) \<and> length (map (\<lambda>x. {pick x}) x) = n \<and> pick ` set (map (\<lambda>x. {pick x}) x) \<subseteq> obj_range \<and> distinct (map pick (map (\<lambda>x. {pick x}) x))) \<and> (\<not> target_type \<noteq> UntypedType \<longrightarrow> x = map ((\<lambda>x. {x}) \<circ> pick) x \<and> length x = n \<and> pick ` set x \<subseteq> obj_range \<and> distinct (map pick x)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x\<rbrakk> \<Longrightarrow> pick ` (\<lambda>x. {pick x}) ` set x \<subseteq> obj_range \<and> distinct (map (pick \<circ> (\<lambda>x. {pick x})) x) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x\<rbrakk> \<Longrightarrow> pick ` (\<lambda>x. {pick x}) ` set x \<subseteq> obj_range \<and> inj_on (pick \<circ> (\<lambda>x. {pick x})) (set x) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x\<rbrakk> \<Longrightarrow> pick ` (\<lambda>x. {pick x}) ` set x \<subseteq> obj_range
 2. \<And>s x. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x\<rbrakk> \<Longrightarrow> inj_on (pick \<circ> (\<lambda>x. {pick x})) (set x) proof (prove)
goal (2 subgoals):
 1. \<And>s x xc. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xc \<in> set x\<rbrakk> \<Longrightarrow> pick xc \<in> obj_range
 2. \<And>s x. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x\<rbrakk> \<Longrightarrow> inj_on (pick \<circ> (\<lambda>x. {pick x})) (set x) proof (prove)
goal (3 subgoals):
 1. \<And>s x xc. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xc \<in> set x\<rbrakk> \<Longrightarrow> xc \<noteq> {}
 2. \<And>s x xc. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xc \<in> set x\<rbrakk> \<Longrightarrow> xc \<subseteq> obj_range
 3. \<And>s x. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x\<rbrakk> \<Longrightarrow> inj_on (pick \<circ> (\<lambda>x. {pick x})) (set x) proof (prove)
goal (2 subgoals):
 1. \<And>s x xc. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xc \<in> set x\<rbrakk> \<Longrightarrow> xc \<subseteq> obj_range
 2. \<And>s x. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x\<rbrakk> \<Longrightarrow> inj_on (pick \<circ> (\<lambda>x. {pick x})) (set x) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x\<rbrakk> \<Longrightarrow> inj_on (pick \<circ> (\<lambda>x. {pick x})) (set x) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y\<rbrakk> \<Longrightarrow> xa = y proof (prove)
goal (2 subgoals):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y\<rbrakk> \<Longrightarrow> xa \<in> set x
 2. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y; \<forall>b\<in>set x. xa \<noteq> b \<longrightarrow> xa \<inter> b = {}\<rbrakk> \<Longrightarrow> xa = y proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y; \<forall>b\<in>set x. xa \<noteq> b \<longrightarrow> xa \<inter> b = {}\<rbrakk> \<Longrightarrow> xa = y proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; \<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y; \<forall>b\<in>set x. xa \<noteq> b \<longrightarrow> xa \<inter> b = {}; xa \<noteq> {} \<and> xa \<subseteq> obj_range \<and> xa \<subseteq> cdl_objects s -` {Some Untyped}\<rbrakk> \<Longrightarrow> xa = y proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y; xa \<noteq> {} \<and> xa \<subseteq> obj_range \<and> xa \<subseteq> cdl_objects s -` {Some Untyped}; y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; xa \<noteq> y \<longrightarrow> xa \<inter> y = {}\<rbrakk> \<Longrightarrow> xa = y proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y; xa \<noteq> {} \<and> xa \<subseteq> obj_range \<and> xa \<subseteq> cdl_objects s -` {Some Untyped}; y \<noteq> {} \<and> y \<subseteq> obj_range \<and> y \<subseteq> cdl_objects s -` {Some Untyped}; xa \<noteq> y \<longrightarrow> xa \<inter> y = {}; xa \<noteq> y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y; xa \<inter> y = {}; xa \<noteq> y; xa \<noteq> {}; y \<noteq> {}; xa \<subseteq> obj_range; xa \<subseteq> cdl_objects s -` {Some Untyped}; y \<subseteq> obj_range; y \<subseteq> cdl_objects s -` {Some Untyped}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y; xa \<inter> y = {}; xa \<noteq> y; xa \<subseteq> obj_range; xa \<subseteq> cdl_objects s -` {Some Untyped}; y \<subseteq> obj_range; y \<subseteq> cdl_objects s -` {Some Untyped}; pick xa \<in> xa; pick y \<in> y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x xa y. \<lbrakk>target_type \<noteq> UntypedType; distinct x; n = length x; xa \<in> set x; y \<in> set x; pick xa = pick y; xa \<inter> y = {}; xa \<noteq> y; xa \<subseteq> obj_range; xa \<subseteq> cdl_objects s -` {Some Untyped}; y \<subseteq> obj_range; y \<subseteq> cdl_objects s -` {Some Untyped}; pick y \<in> xa; pick y \<in> y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!