170 |
170 |
171 "-------- investigate (new 2002) uniary minus --------------------------------------------------"; |
171 "-------- investigate (new 2002) uniary minus --------------------------------------------------"; |
172 "-------- investigate (new 2002) uniary minus --------------------------------------------------"; |
172 "-------- investigate (new 2002) uniary minus --------------------------------------------------"; |
173 "-------- investigate (new 2002) uniary minus --------------------------------------------------"; |
173 "-------- investigate (new 2002) uniary minus --------------------------------------------------"; |
174 val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*) |
174 val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*) |
175 TermC.atomty t; |
175 TermC.atom_trace_detail @{context} t; |
176 (* |
176 (* |
177 *** Const (HOL.Trueprop, bool => prop) |
177 *** Const (HOL.Trueprop, bool => prop) |
178 *** . Const (HOL.eq, real => real => bool) |
178 *** . Const (HOL.eq, real => real => bool) |
179 *** . . Const (Groups.minus_class.minus, real => real => real) |
179 *** . . Const (Groups.minus_class.minus, real => real => real) |
180 *** . . . Const (Groups.zero_class.zero, real) |
180 *** . . . Const (Groups.zero_class.zero, real) |
204 |
204 |
205 "======= these external values all have the same internal representation"; |
205 "======= these external values all have the same internal representation"; |
206 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*) |
206 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*) |
207 (*----------------------------------- vvvvv -------------------------------------------*) |
207 (*----------------------------------- vvvvv -------------------------------------------*) |
208 val t = TermC.parseNEW' thy "-x"; |
208 val t = TermC.parseNEW' thy "-x"; |
209 TermC.atomty t; |
209 TermC.atom_trace_detail @{context} t; |
210 (**** ------------- |
210 (**** ------------- |
211 *** Free ( -x, real)*) |
211 *** Free ( -x, real)*) |
212 case t of |
212 case t of |
213 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => () |
213 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => () |
214 | _ => error "internal representation of \"-x\" changed"; |
214 | _ => error "internal representation of \"-x\" changed"; |
215 (*----------------------------------- vvvvv -------------------------------------------*) |
215 (*----------------------------------- vvvvv -------------------------------------------*) |
216 val t = TermC.parseNEW' thy "- x"; |
216 val t = TermC.parseNEW' thy "- x"; |
217 TermC.atomty t; |
217 TermC.atom_trace_detail @{context} t; |
218 (**** ------------- |
218 (**** ------------- |
219 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*) |
219 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*) |
220 case t of |
220 case t of |
221 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => () |
221 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => () |
222 | _ => error "internal representation of \"- x\" changed"; |
222 | _ => error "internal representation of \"- x\" changed"; |
223 (*----------------------------------- vvvvvv ------------------------------------------*) |
223 (*----------------------------------- vvvvvv ------------------------------------------*) |
224 val t = TermC.parseNEW' thy "-(x)"; |
224 val t = TermC.parseNEW' thy "-(x)"; |
225 TermC.atomty t; |
225 TermC.atom_trace_detail @{context} t; |
226 (**** ------------- |
226 (**** ------------- |
227 *** Free ( -x, real)*) |
227 *** Free ( -x, real)*) |
228 case t of |
228 case t of |
229 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => () |
229 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => () |
230 | _ => error "internal representation of \"-(x)\" changed"; |
230 | _ => error "internal representation of \"-(x)\" changed"; |