# HG changeset patch
# User haftmann
# Date 1278335540 -7200
# Node ID 44b27ea94a160d7a4a22857ee2c896c8813f37f1
# Parent 2eb2b048057b9990b4666cd7ef3fa6b4e9570f8c
tuned proof
diff -r 2eb2b048057b -r 44b27ea94a16 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy Mon Jul 05 15:12:20 2010 +0200
+++ b/src/HOL/Library/Countable.thy Mon Jul 05 15:12:20 2010 +0200
@@ -110,26 +110,20 @@
"to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
instance proof (rule countable_classI)
- fix t t' :: typerep and ts
- have "(\t'. to_nat_typerep t = to_nat_typerep t' \ t = t')
- \ (\ts'. map to_nat_typerep ts = map to_nat_typerep ts' \ ts = ts')"
- proof (induct rule: typerep.induct)
- case (Typerep c ts) show ?case
- proof (rule allI, rule impI)
- fix t'
- assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"
- then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"
- by (cases t') auto
- with Typerep hyp have "c = c'" and "ts = ts'" by simp_all
- with t' show "Typerep.Typerep c ts = t'" by simp
- qed
+ fix t t' :: typerep and ts ts' :: "typerep list"
+ assume "to_nat_typerep t = to_nat_typerep t'"
+ moreover have "to_nat_typerep t = to_nat_typerep t' \ t = t'"
+ and "map to_nat_typerep ts = map to_nat_typerep ts' \ ts = ts'"
+ proof (induct t and ts arbitrary: t' and ts' rule: typerep.inducts)
+ case (Typerep c ts t')
+ then obtain c' ts' where t': "t' = Typerep.Typerep c' ts'" by (cases t') auto
+ with Typerep have "c = c'" and "ts = ts'" by simp_all
+ with t' show "Typerep.Typerep c ts = t'" by simp
next
case Nil_typerep then show ?case by simp
next
case (Cons_typerep t ts) then show ?case by auto
qed
- then have "to_nat_typerep t = to_nat_typerep t' \ t = t'" by auto
- moreover assume "to_nat_typerep t = to_nat_typerep t'"
ultimately show "t = t'" by simp
qed