summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 05 Jul 2010 15:12:20 +0200 | |

changeset 37715 | 44b27ea94a16 |

parent 37714 | 2eb2b048057b |

child 37716 | 24bb91462892 |

tuned proof

--- 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 "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t') - \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> 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' \<Longrightarrow> t = t'" + and "map to_nat_typerep ts = map to_nat_typerep ts' \<Longrightarrow> 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' \<Longrightarrow> t = t'" by auto - moreover assume "to_nat_typerep t = to_nat_typerep t'" ultimately show "t = t'" by simp qed