278 val SOME (id,t') = eval_fn op_ t thy; |
278 val SOME (id,t') = eval_fn op_ t thy; |
279 (*** calc: operator = pow not defined*) |
279 (*** calc: operator = pow not defined*) |
280 |
280 |
281 case (op_, t) of |
281 case (op_, t) of |
282 ("Transcendental.powr", |
282 ("Transcendental.powr", |
283 Const ("Transcendental.powr", _) $ (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _))) $ |
283 Const (\<^const_name>\<open>powr\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $ |
284 (Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) => () |
284 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => () |
285 | _ => error "3 \<up> 2 CHANGED"; |
285 | _ => error "3 \<up> 2 CHANGED"; |
286 val SOME (id, t') = eval_binop thmid op_ t thy; |
286 val SOME (id, t') = eval_binop thmid op_ t thy; |
287 (*** calc: operator = pow not defined*) |
287 (*** calc: operator = pow not defined*) |
288 |
288 |
289 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED"; |
289 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED"; |
301 "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; |
301 "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; |
302 "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; |
302 "----------- RE-BUILD fun calcul ---------------------------------------------------------------"; |
303 val (t1, t2) = (@{term 3}, @{term "2::real"}); |
303 val (t1, t2) = (@{term 3}, @{term "2::real"}); |
304 |
304 |
305 "~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2)); |
305 "~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2)); |
306 val (Const ("Num.numeral_class.numeral", _) $ n1) = t1; |
306 val (Const (\<^const_name>\<open>numeral\<close>, _) $ n1) = t1; |
307 val (Const ("Num.numeral_class.numeral", _) $ n2) = t2; |
307 val (Const (\<^const_name>\<open>numeral\<close>, _) $ n2) = t2; |
308 val (T, _) = HOLogic.dest_number t1 |
308 val (T, _) = HOLogic.dest_number t1 |
309 val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2) |
309 val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2) |
310 val result = |
310 val result = |
311 case op_ of |
311 case op_ of |
312 "Groups.plus_class.plus" => i1 + i2 |
312 "Groups.plus_class.plus" => i1 + i2 |