equal
deleted
inserted
replaced
19 ZERO::"my_int" |
19 ZERO::"my_int" |
20 where |
20 where |
21 "ZERO \<equiv> (0::nat, 0::nat)" |
21 "ZERO \<equiv> (0::nat, 0::nat)" |
22 |
22 |
23 ML {* print_qconstinfo @{context} *} |
23 ML {* print_qconstinfo @{context} *} |
24 |
|
25 |
24 |
26 term ZERO |
25 term ZERO |
27 thm ZERO_def |
26 thm ZERO_def |
28 |
27 |
29 ML {* prop_of @{thm ZERO_def} *} |
28 ML {* prop_of @{thm ZERO_def} *} |
141 fun lift_thm_my_int lthy t = |
140 fun lift_thm_my_int lthy t = |
142 lift_thm lthy qty ty_name rsp_thms defs t |
141 lift_thm lthy qty ty_name rsp_thms defs t |
143 *} |
142 *} |
144 |
143 |
145 print_quotients |
144 print_quotients |
|
145 ML {* quotdata_lookup @{context} "IntEx.my_int" *} |
|
146 ML {* quotdata_lookup @{context} "my_int" *} |
146 |
147 |
147 ML {* |
148 ML {* |
148 val test = lift_thm_my_int @{context} @{thm plus_sym_pre} |
149 val test = lift_thm_my_int @{context} @{thm plus_sym_pre} |
149 *} |
150 *} |
150 |
151 |
151 ML {* my_lift (prop_of test) @{thm plus_sym_pre} @{context} *} |
|
152 |
152 |
153 ML {* |
153 ML {* |
154 ObjectLogic.atomize_term @{theory} (prop_of test) |
154 val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test)) |
155 |> Syntax.string_of_term @{context} |
155 val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre})) |
156 |> writeln |
156 *} |
157 *} |
157 |
158 |
158 |
159 lemma plus_assoc_pre: |
159 lemma plus_assoc_pre: |
160 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
160 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
161 apply (cases i) |
161 apply (cases i) |
162 apply (cases j) |
162 apply (cases j) |