src/HOL/Library/Countable.thy
 changeset 37715 44b27ea94a16 parent 37678 0040bafffdef child 39198 f967a16dfcdd
equal inserted replaced
37714:2eb2b048057b 37715:44b27ea94a16
`   108 `
`   108 `
`   109 fun to_nat_typerep :: "typerep \<Rightarrow> nat" where`
`   109 fun to_nat_typerep :: "typerep \<Rightarrow> nat" where`
`   110   "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"`
`   110   "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"`
`   111 `
`   111 `
`   112 instance proof (rule countable_classI)`
`   112 instance proof (rule countable_classI)`
`   113   fix t t' :: typerep and ts`
`   113   fix t t' :: typerep and ts ts' :: "typerep list"`
`   114   have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')`
`   114   assume "to_nat_typerep t = to_nat_typerep t'"`
`   115     \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')"`
`   115   moreover have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'"`
`   116   proof (induct rule: typerep.induct)`
`   116     and "map to_nat_typerep ts = map to_nat_typerep ts' \<Longrightarrow> ts = ts'"`
`   117     case (Typerep c ts) show ?case`
`   117   proof (induct t and ts arbitrary: t' and ts' rule: typerep.inducts)`
`   118     proof (rule allI, rule impI)`
`   118     case (Typerep c ts t')`
`   119       fix t'`
`   119     then obtain c' ts' where t': "t' = Typerep.Typerep c' ts'" by (cases t') auto`
`   120       assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"`
`   120     with Typerep have "c = c'" and "ts = ts'" by simp_all`
`   121       then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"`
`   121     with t' show "Typerep.Typerep c ts = t'" by simp`
`   122         by (cases t') auto`
`       `
`   123       with Typerep hyp have "c = c'" and "ts = ts'" by simp_all`
`       `
`   124       with t' show "Typerep.Typerep c ts = t'" by simp`
`       `
`   125     qed`
`       `
`   126   next`
`   122   next`
`   127     case Nil_typerep then show ?case by simp`
`   123     case Nil_typerep then show ?case by simp`
`   128   next`
`   124   next`
`   129     case (Cons_typerep t ts) then show ?case by auto`
`   125     case (Cons_typerep t ts) then show ?case by auto`
`   130   qed`
`   126   qed`
`   133   ultimately show "t = t'" by simp`
`   127   ultimately show "t = t'" by simp`
`   134 qed`
`   128 qed`
`   135 `
`   129 `
`   136 end`
`   130 end`
`   137 `
`   131 `