1.1 --- a/src/HOL/Library/Countable.thy Mon Jul 05 15:12:20 2010 +0200
1.2 +++ b/src/HOL/Library/Countable.thy Mon Jul 05 15:12:20 2010 +0200
1.3 @@ -110,26 +110,20 @@
1.4 "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
1.5
1.6 instance proof (rule countable_classI)
1.7 - fix t t' :: typerep and ts
1.8 - have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')
1.9 - \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')"
1.10 - proof (induct rule: typerep.induct)
1.11 - case (Typerep c ts) show ?case
1.12 - proof (rule allI, rule impI)
1.13 - fix t'
1.14 - assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"
1.15 - then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"
1.16 - by (cases t') auto
1.17 - with Typerep hyp have "c = c'" and "ts = ts'" by simp_all
1.18 - with t' show "Typerep.Typerep c ts = t'" by simp
1.19 - qed
1.20 + fix t t' :: typerep and ts ts' :: "typerep list"
1.21 + assume "to_nat_typerep t = to_nat_typerep t'"
1.22 + moreover have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'"
1.23 + and "map to_nat_typerep ts = map to_nat_typerep ts' \<Longrightarrow> ts = ts'"
1.24 + proof (induct t and ts arbitrary: t' and ts' rule: typerep.inducts)
1.25 + case (Typerep c ts t')
1.26 + then obtain c' ts' where t': "t' = Typerep.Typerep c' ts'" by (cases t') auto
1.27 + with Typerep have "c = c'" and "ts = ts'" by simp_all
1.28 + with t' show "Typerep.Typerep c ts = t'" by simp
1.29 next
1.30 case Nil_typerep then show ?case by simp
1.31 next
1.32 case (Cons_typerep t ts) then show ?case by auto
1.33 qed
1.34 - then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto
1.35 - moreover assume "to_nat_typerep t = to_nat_typerep t'"
1.36 ultimately show "t = t'" by simp
1.37 qed
1.38