equal
deleted
inserted
replaced
52 by pat_completeness auto |
52 by pat_completeness auto |
53 |
53 |
54 termination by (relation "measure (\<lambda>x. size x)") |
54 termination by (relation "measure (\<lambda>x. size x)") |
55 (simp, simp only: in_measure rtype_size) |
55 (simp, simp only: in_measure rtype_size) |
56 |
56 |
57 instance proof (rule countable_classI) |
57 instance |
58 fix t t' :: rtype |
58 proof (rule countable_classI) |
|
59 fix t t' :: rtype and ts |
59 have "(\<forall>t'. to_nat_rtype t = to_nat_rtype t' \<longrightarrow> t = t') |
60 have "(\<forall>t'. to_nat_rtype t = to_nat_rtype t' \<longrightarrow> t = t') |
60 \<and> (\<forall>ts'. map to_nat_rtype ts = map to_nat_rtype ts' \<longrightarrow> ts = ts')" |
61 \<and> (\<forall>ts'. map to_nat_rtype ts = map to_nat_rtype ts' \<longrightarrow> ts = ts')" |
61 proof (induct rule: rtype.induct) |
62 proof (induct rule: rtype.induct) |
62 case (RType c ts) show ?case |
63 case (RType c ts) show ?case |
63 proof (rule allI, rule impI) |
64 proof (rule allI, rule impI) |