theory Retype_C

lemma htd_update_list_dom_better [rule_format]:
  "(\<forall>p d. dom_s (htd_update_list p xs d) =
          (dom_s d) \<union> dom_tll p xs)" apply(induct_tac xs) apply simp apply clarsimp apply(auto split: if_split_asm) apply(erule notE) apply(clarsimp simp: dom_s_def) apply(case_tac y) apply clarsimp+ apply(clarsimp simp: dom_s_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>p d. dom_s (htd_update_list p xs d) = dom_s d \<union> dom_tll p xs proof (prove)
goal (2 subgoals):
 1. \<forall>p d. dom_s (htd_update_list p [] d) = dom_s d \<union> dom_tll p []
 2. \<And>x1 x2. \<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2 \<Longrightarrow> \<forall>p d. dom_s (htd_update_list p (x1 # x2) d) = dom_s d \<union> dom_tll p (x1 # x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2 \<Longrightarrow> \<forall>p d. dom_s (htd_update_list p (x1 # x2) d) = dom_s d \<union> dom_tll p (x1 # x2) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 p d. \<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2 \<Longrightarrow> insert (p, SIndexVal) (dom_s d - {uu_. \<exists>y. uu_ = (p, y)} \<union> {(p, SIndexTyp n) |n. (\<exists>a b. x1 n = Some (a, b)) \<or> (\<exists>a b. snd (d p) n = Some (a, b))} \<union> dom_tll (p + 1) x2) = insert (p, SIndexVal) (dom_s d \<union> (dom_tll (p + 1) x2 \<union> {(p, SIndexTyp n) |n. \<exists>a b. x1 n = Some (a, b)})) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 p d n aa ba. \<lbrakk>\<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2; (p, SIndexTyp n) \<notin> dom_s d; (p, SIndexTyp n) \<notin> dom_tll (p + 1) x2; snd (d p) n = Some (aa, ba); x1 n = None\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2 p d y. \<lbrakk>\<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2; (p, y) \<notin> dom_tll (p + 1) x2; \<forall>n. y = SIndexTyp n \<longrightarrow> x1 n = None \<and> snd (d p) n = None; (p, y) \<in> dom_s d\<rbrakk> \<Longrightarrow> y = SIndexVal proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 p d n aa ba. \<lbrakk>\<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2; (p, SIndexTyp n) \<notin> dom_tll (p + 1) x2; snd (d p) n = Some (aa, ba); x1 n = None\<rbrakk> \<Longrightarrow> (p, SIndexTyp n) \<in> dom_s d
 2. \<And>x1 x2 p d y. \<lbrakk>\<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2; (p, y) \<notin> dom_tll (p + 1) x2; \<forall>n. y = SIndexTyp n \<longrightarrow> x1 n = None \<and> snd (d p) n = None; (p, y) \<in> dom_s d\<rbrakk> \<Longrightarrow> y = SIndexVal proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 p d y. \<lbrakk>\<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2; (p, y) \<notin> dom_tll (p + 1) x2; \<forall>n. y = SIndexTyp n \<longrightarrow> x1 n = None \<and> snd (d p) n = None; (p, y) \<in> dom_s d\<rbrakk> \<Longrightarrow> y = SIndexVal proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 p d y. \<lbrakk>\<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2; (p, y) \<notin> dom_tll (p + 1) x2; \<forall>n. y = SIndexTyp n \<longrightarrow> x1 n = None \<and> snd (d p) n = None; (p, y) \<in> dom_s d; y = SIndexVal\<rbrakk> \<Longrightarrow> y = SIndexVal
 2. \<And>x1 x2 p d y x2a. \<lbrakk>\<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2; (p, y) \<notin> dom_tll (p + 1) x2; \<forall>n. y = SIndexTyp n \<longrightarrow> x1 n = None \<and> snd (d p) n = None; (p, y) \<in> dom_s d; y = SIndexTyp x2a\<rbrakk> \<Longrightarrow> y = SIndexVal proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 p d x2a. \<lbrakk>\<forall>p d. dom_s (htd_update_list p x2 d) = dom_s d \<union> dom_tll p x2; (p, SIndexTyp x2a) \<notin> dom_tll (p + 1) x2; (p, SIndexTyp x2a) \<in> dom_s d; x1 x2a = None; snd (d p) x2a = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!