equal
deleted
inserted
replaced
296 (** some logic operations **) |
296 (** some logic operations **) |
297 |
297 |
298 (* decompses a formula into params, premises and a conclusion *) |
298 (* decompses a formula into params, premises and a conclusion *) |
299 fun strip_full_horn trm = |
299 fun strip_full_horn trm = |
300 let |
300 let |
301 fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = |
301 fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
302 strip_outer_params t |>> cons (a, T) |
|
303 | strip_outer_params B = ([], B) |
302 | strip_outer_params B = ([], B) |
304 |
303 |
305 val (params, body) = strip_outer_params trm |
304 val (params, body) = strip_outer_params trm |
306 val (prems, concl) = Logic.strip_horn body |
305 val (prems, concl) = Logic.strip_horn body |
307 in |
306 in |
363 addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral |
362 addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral |
364 zero_less_Suc prod.size(1) mult_Suc_right}) |
363 zero_less_Suc prod.size(1) mult_Suc_right}) |
365 |
364 |
366 val natT = @{typ nat} |
365 val natT = @{typ nat} |
367 |
366 |
368 fun prod_size_const T1 T2 = |
367 fun size_prod_const T1 T2 = |
369 let |
368 let |
370 val T1_fun = T1 --> natT |
369 val T1_fun = T1 --> natT |
371 val T2_fun = T2 --> natT |
370 val T2_fun = T2 --> natT |
372 val prodT = HOLogic.mk_prodT (T1, T2) |
371 val prodT = HOLogic.mk_prodT (T1, T2) |
373 in |
372 in |
374 Const (@{const_name prod_size}, [T1_fun, T2_fun, prodT] ---> natT) |
373 Const (@{const_name size_prod}, [T1_fun, T2_fun, prodT] ---> natT) |
375 end |
374 end |
376 |
375 |
377 fun snd_const T1 T2 = |
376 fun snd_const T1 T2 = |
378 Const (@{const_name Product_Type.snd}, HOLogic.mk_prodT (T1, T2) --> T2) |
377 Const (@{const_name Product_Type.snd}, HOLogic.mk_prodT (T1, T2) --> T2) |
379 |
378 |
407 fun mk_size_measure T = |
406 fun mk_size_measure T = |
408 case T of |
407 case T of |
409 (Type (@{type_name Sum_Type.sum}, [T1, T2])) => |
408 (Type (@{type_name Sum_Type.sum}, [T1, T2])) => |
410 Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) |
409 Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) |
411 | (Type (@{type_name Product_Type.prod}, [T1, T2])) => |
410 | (Type (@{type_name Product_Type.prod}, [T1, T2])) => |
412 prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) |
411 size_prod_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) |
413 | _ => HOLogic.size_const T |
412 | _ => HOLogic.size_const T |
414 |
413 |
415 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
414 val measure_trm = mk_measure_trm (mk_size_measure) ctxt |
416 |
415 |
417 val tac = |
416 val tac = |