theory Retype_C

lemma typ_le_uinfo_array_tag_n_m:
  "0 < n \<Longrightarrow> td \<le> uinfo_array_tag_n_m TYPE('a :: c_type) n m
    = (td \<le> typ_uinfo_t TYPE('a) \<or> td = uinfo_array_tag_n_m TYPE('a) n m)" proof - have ind: "\<And>xs cs. \<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (cs i)) xs) n'
    \<subseteq> (fst ` (\<Union>i. td_set (typ_uinfo_t TYPE('a)) i)) \<times> UNIV" apply (induct_tac xs) apply clarsimp apply clarsimp apply (fastforce intro: image_eqI[rotated]) done assume "0 < n" thus ?thesis apply (simp add: uinfo_array_tag_n_m_def typ_tag_le_def upt_conv_Cons) apply (auto dest!: ind[rule_format, THEN subsetD], (blast dest: td_set_offset)+) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (td \<le> uinfo_array_tag_n_m TYPE('a) n m) = (td \<le> typ_uinfo_t TYPE('a) \<or> td = uinfo_array_tag_n_m TYPE('a) n m) proof (state)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (td \<le> uinfo_array_tag_n_m TYPE('a) n m) = (td \<le> typ_uinfo_t TYPE('a) \<or> td = uinfo_array_tag_n_m TYPE('a) n m) proof (prove)
goal (1 subgoal):
 1. \<And>xs cs. \<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (cs i)) xs) n' \<subseteq> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) \<times> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>xs cs. \<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (cs i)) []) n' \<subseteq> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) \<times> UNIV
 2. \<And>xs cs x1 x2. \<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (cs i)) x2) n' \<subseteq> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) \<times> UNIV \<Longrightarrow> \<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (cs i)) (x1 # x2)) n' \<subseteq> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) \<times> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>xs cs x1 x2. \<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (cs i)) x2) n' \<subseteq> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) \<times> UNIV \<Longrightarrow> \<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (cs i)) (x1 # x2)) n' \<subseteq> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) \<times> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>cs x2 n' a b. \<lbrakk>\<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (cs i)) x2) n' \<subseteq> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) \<times> UNIV; (a, b) \<in> td_set (typ_uinfo_t TYPE('a)) n'\<rbrakk> \<Longrightarrow> a \<in> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>n'. td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (?cs2 i)) ?xs2) n' \<subseteq> fst ` \<Union> (range (td_set (typ_uinfo_t TYPE('a)))) \<times> UNIV

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (td \<le> uinfo_array_tag_n_m TYPE('a) n m) = (td \<le> typ_uinfo_t TYPE('a) \<or> td = uinfo_array_tag_n_m TYPE('a) n m) proof (state)
this:
0 < n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (td \<le> uinfo_array_tag_n_m TYPE('a) n m) = (td \<le> typ_uinfo_t TYPE('a) \<or> td = uinfo_array_tag_n_m TYPE('a) n m) proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (td \<le> uinfo_array_tag_n_m TYPE('a) n m) = (td \<le> typ_uinfo_t TYPE('a) \<or> td = uinfo_array_tag_n_m TYPE('a) n m) proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (\<exists>na. td = TypDesc (TypAggregate (DTPair (typ_uinfo_t TYPE('a)) [] # map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (replicate i CHR ''1'')) [Suc 0..<n])) (typ_name (typ_uinfo_t TYPE('a)) @ CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string m) \<and> na = 0 \<or> (td, na) \<in> td_set (typ_uinfo_t TYPE('a)) 0 \<or> (td, na) \<in> td_set_list (map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (replicate i CHR ''1'')) [Suc 0..<n]) (size_td (typ_info_t TYPE('a)))) = ((\<exists>n. (td, n) \<in> td_set (typ_uinfo_t TYPE('a)) 0) \<or> td = TypDesc (TypAggregate (DTPair (typ_uinfo_t TYPE('a)) [] # map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (replicate i CHR ''1'')) [Suc 0..<n])) (typ_name (typ_uinfo_t TYPE('a)) @ CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string m)) proof (prove)
goal:
No subgoals! proof (state)
this:
(td \<le> uinfo_array_tag_n_m TYPE('a) n m) = (td \<le> typ_uinfo_t TYPE('a) \<or> td = uinfo_array_tag_n_m TYPE('a) n m)

goal:
No subgoals!