basicSizeScript.sml

1Theory basicSize[bare]
2Ancestors
3  pair sum option numeral
4Libs
5  HolKernel Parse boolLib pairLib Prim_rec
6
7val bool_size_def = new_definition
8  ("bool_size_def", ``bool_size (b:bool) = 0``);
9
10val min_pair_size_def = new_definition
11  ("min_pair_size_def", ``min_pair_size f g (x, y) = f x + g y``);
12
13val pair_size_def = new_definition
14  ("pair_size_def", ``pair_size f g (x, y) = 1 + (f x + g y)``);
15
16val one_size_def = new_definition
17  ("one_size_def", ``one_size (x:one) = 0``);
18
19val itself_size_def = new_definition
20  ("itself_size_def", ``itself_size (x : 'a itself) = 0``);
21
22val sum_size_def =
23 new_recursive_definition
24   {def = ``(sum_size (f:'a->num) g (INL x) = f x) /\
25            (sum_size f (g:'b->num) (INR y) = g y)``,
26    name="sum_size_def",
27    rec_axiom = sumTheory.sum_Axiom};
28
29val full_sum_size_def = new_definition
30  ("full_sum_size_def", ``full_sum_size f g sum = 1 + (sum_size f g sum)``);
31Theorem full_sum_size_thm:
32   (full_sum_size f g (INL x) = 1 + (f x)) /\
33    (full_sum_size f g (INR y) = 1 + (g y))
34Proof
35  REWRITE_TAC [full_sum_size_def, sum_size_def]
36QED
37
38val option_size_def =
39 new_recursive_definition
40   {def = ``(option_size f NONE = 0) /\
41            (option_size f (SOME x) = 1 + (f x))``,
42    name="option_size_def",
43    rec_axiom = optionTheory.option_Axiom};
44