260 |
260 |
261 |
261 |
262 (*evaluate identity |
262 (*evaluate identity |
263 > reflI; |
263 > reflI; |
264 val it = "(?t = ?t) = True" |
264 val it = "(?t = ?t) = True" |
265 > val t = str2term "x = 0"; |
265 > val t = TermC.parse_test @{context} "x = 0"; |
266 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
266 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
267 |
267 |
268 > val t = str2term "1 = 0"; |
268 > val t = TermC.parse_test @{context} "1 = 0"; |
269 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
269 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
270 ----------- thus needs Rule.Eval ! |
270 ----------- thus needs Rule.Eval ! |
271 > val t = str2term "0 = 0"; |
271 > val t = TermC.parse_test @{context} "0 = 0"; |
272 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
272 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; |
273 > UnparseC.term t'; |
273 > UnparseC.term t'; |
274 val it = \<^const_name>\<open>True\<close> |
274 val it = \<^const_name>\<open>True\<close> |
275 |
275 |
276 val t = str2term "Not (x = 0)"; |
276 val t = TermC.parse_test @{context} "Not (x = 0)"; |
277 atomt t; UnparseC.term t; |
277 atomt t; UnparseC.term t; |
278 *** ------------- |
278 *** ------------- |
279 *** Const ( Not) |
279 *** Const ( Not) |
280 *** . Const ( op =) |
280 *** . Const ( op =) |
281 *** . . Free ( x, ) |
281 *** . . Free ( x, ) |
296 ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")") |
296 ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")") |
297 ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"), |
297 ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"), |
298 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
298 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) |
299 | eval_ident _ _ _ _ = NONE; |
299 | eval_ident _ _ _ _ = NONE; |
300 (* TODO |
300 (* TODO |
301 > val t = str2term "x =!= 0"; |
301 > val t = TermC.parse_test @{context} "x =!= 0"; |
302 > val SOME (str, t') = eval_ident "ident_" "b" t thy; |
302 > val SOME (str, t') = eval_ident "ident_" "b" t thy; |
303 > UnparseC.term t'; |
303 > UnparseC.term t'; |
304 val str = "ident_(x)_(0)" : string |
304 val str = "ident_(x)_(0)" : string |
305 val it = "(x =!= 0) = False" : string |
305 val it = "(x =!= 0) = False" : string |
306 > val t = str2term "1 =!= 0"; |
306 > val t = TermC.parse_test @{context} "1 =!= 0"; |
307 > val SOME (str, t') = eval_ident "ident_" "b" t thy; |
307 > val SOME (str, t') = eval_ident "ident_" "b" t thy; |
308 > UnparseC.term t'; |
308 > UnparseC.term t'; |
309 val str = "ident_(1)_(0)" : string |
309 val str = "ident_(1)_(0)" : string |
310 val it = "(1 =!= 0) = False" : string |
310 val it = "(1 =!= 0) = False" : string |
311 > val t = str2term "0 =!= 0"; |
311 > val t = TermC.parse_test @{context} "0 =!= 0"; |
312 > val SOME (str, t') = eval_ident "ident_" "b" t thy; |
312 > val SOME (str, t') = eval_ident "ident_" "b" t thy; |
313 > UnparseC.term t'; |
313 > UnparseC.term t'; |
314 val str = "ident_(0)_(0)" : string |
314 val str = "ident_(0)_(0)" : string |
315 val it = "(0 =!= 0) = True" : string |
315 val it = "(0 =!= 0) = True" : string |
316 *) |
316 *) |