35 |
35 |
36 (* number *) |
36 (* number *) |
37 |
37 |
38 local |
38 local |
39 |
39 |
40 val zero = @{cpat "0"}; |
40 val cterm_of = Thm.cterm_of @{context}; |
41 val zeroT = Thm.ctyp_of_cterm zero; |
41 fun tvar S = (("'a", 0), S); |
42 |
42 |
43 val one = @{cpat "1"}; |
43 val zero_tvar = tvar @{sort zero}; |
44 val oneT = Thm.ctyp_of_cterm one; |
44 val zero = cterm_of (Const (@{const_name zero_class.zero}, TVar zero_tvar)); |
45 |
45 |
46 val numeral = @{cpat "numeral"}; |
46 val one_tvar = tvar @{sort one}; |
47 val numeralT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm numeral)); |
47 val one = cterm_of (Const (@{const_name one_class.one}, TVar one_tvar)); |
48 |
48 |
49 val uminus = @{cpat "uminus"}; |
49 val numeral_tvar = tvar @{sort numeral}; |
50 val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus)); |
50 val numeral = cterm_of (Const (@{const_name numeral}, @{typ num} --> TVar numeral_tvar)); |
51 |
51 |
52 fun instT T V = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of V), T)], []); |
52 val uminus_tvar = tvar @{sort uminus}; |
|
53 val uminus = cterm_of (Const (@{const_name uminus}, TVar uminus_tvar --> TVar uminus_tvar)); |
|
54 |
|
55 fun instT T v = Thm.instantiate_cterm ([(v, T)], []); |
53 |
56 |
54 in |
57 in |
55 |
58 |
56 fun mk_cnumber T 0 = instT T zeroT zero |
59 fun mk_cnumber T 0 = instT T zero_tvar zero |
57 | mk_cnumber T 1 = instT T oneT one |
60 | mk_cnumber T 1 = instT T one_tvar one |
58 | mk_cnumber T i = |
61 | mk_cnumber T i = |
59 if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i) |
62 if i > 0 then |
60 else Thm.apply (instT T uminusT uminus) (Thm.apply (instT T numeralT numeral) (mk_cnumeral (~i))); |
63 Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral i) |
|
64 else |
|
65 Thm.apply (instT T uminus_tvar uminus) |
|
66 (Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral (~ i))); |
61 |
67 |
62 end; |
68 end; |
63 |
69 |
64 fun mk_num_syntax n = |
70 fun mk_num_syntax n = |
65 if n > 0 then |
71 if n > 0 then |