equal
deleted
inserted
replaced
14 "~~/src/Tools/rat.ML" |
14 "~~/src/Tools/rat.ML" |
15 "~~/src/Provers/Arith/cancel_sums.ML" |
15 "~~/src/Provers/Arith/cancel_sums.ML" |
16 ("arith_data.ML") |
16 ("arith_data.ML") |
17 "~~/src/Provers/Arith/fast_lin_arith.ML" |
17 "~~/src/Provers/Arith/fast_lin_arith.ML" |
18 ("Tools/lin_arith.ML") |
18 ("Tools/lin_arith.ML") |
|
19 ("Tools/function_package/size.ML") |
19 begin |
20 begin |
20 |
21 |
21 subsection {* Type @{text ind} *} |
22 subsection {* Type @{text ind} *} |
22 |
23 |
23 typedecl ind |
24 typedecl ind |
109 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False" |
110 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False" |
110 by auto |
111 by auto |
111 |
112 |
112 text {* size of a datatype value *} |
113 text {* size of a datatype value *} |
113 |
114 |
|
115 use "Tools/function_package/size.ML" |
|
116 |
114 class size = type + |
117 class size = type + |
115 fixes size :: "'a \<Rightarrow> nat" |
118 fixes size :: "'a \<Rightarrow> nat" |
|
119 |
|
120 setup Size.setup |
116 |
121 |
117 rep_datatype nat |
122 rep_datatype nat |
118 distinct Suc_not_Zero Zero_not_Suc |
123 distinct Suc_not_Zero Zero_not_Suc |
119 inject Suc_Suc_eq |
124 inject Suc_Suc_eq |
120 induction nat_induct |
125 induction nat_induct |
1465 "inf \<equiv> min" |
1470 "inf \<equiv> min" |
1466 "sup \<equiv> max" |
1471 "sup \<equiv> max" |
1467 by intro_classes (auto simp add: inf_nat_def sup_nat_def) |
1472 by intro_classes (auto simp add: inf_nat_def sup_nat_def) |
1468 |
1473 |
1469 |
1474 |
1470 subsection {* Size function *} |
1475 subsection {* Size function declarations *} |
1471 |
1476 |
1472 lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n" |
1477 lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n" |
1473 by (induct n) simp_all |
1478 by (induct n) simp_all |
|
1479 |
|
1480 lemma size_bool [code func]: |
|
1481 "size (b\<Colon>bool) = 0" by (cases b) auto |
|
1482 |
|
1483 declare "*.size" [noatp] |
|
1484 |
1474 |
1485 |
1475 subsection {* legacy bindings *} |
1486 subsection {* legacy bindings *} |
1476 |
1487 |
1477 ML |
1488 ML |
1478 {* |
1489 {* |