src/HOL/Library/Countable.thy
changeset 37715 44b27ea94a16
parent 37678 0040bafffdef
child 39198 f967a16dfcdd
equal deleted 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
   131   then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto
       
   132   moreover assume "to_nat_typerep t = to_nat_typerep t'"
       
   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