26 [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, |
26 [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, |
27 @{term "op - :: int => _"}, @{term "op - :: nat => _"}, |
27 @{term "op - :: int => _"}, @{term "op - :: nat => _"}, |
28 @{term "op * :: int => _"}, @{term "op * :: nat => _"}, |
28 @{term "op * :: int => _"}, @{term "op * :: nat => _"}, |
29 @{term "op div :: int => _"}, @{term "op div :: nat => _"}, |
29 @{term "op div :: int => _"}, @{term "op div :: nat => _"}, |
30 @{term "op mod :: int => _"}, @{term "op mod :: nat => _"}, |
30 @{term "op mod :: int => _"}, @{term "op mod :: nat => _"}, |
31 @{term "op &"}, @{term "op |"}, @{term "op -->"}, |
31 @{term "op &"}, @{term "op |"}, @{term HOL.implies}, |
32 @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"}, |
32 @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"}, |
33 @{term "op < :: int => _"}, @{term "op < :: nat => _"}, |
33 @{term "op < :: int => _"}, @{term "op < :: nat => _"}, |
34 @{term "op <= :: int => _"}, @{term "op <= :: nat => _"}, |
34 @{term "op <= :: int => _"}, @{term "op <= :: nat => _"}, |
35 @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"}, |
35 @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"}, |
36 @{term "abs :: int => _"}, |
36 @{term "abs :: int => _"}, |
567 | TYPE s => raise COOPER "bad type" |
567 | TYPE s => raise COOPER "bad type" |
568 |
568 |
569 fun add_bools t = |
569 fun add_bools t = |
570 let |
570 let |
571 val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"}, |
571 val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"}, |
572 @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"}, |
572 @{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"}, |
573 @{term "Not"}, @{term "All :: (int => _) => _"}, |
573 @{term "Not"}, @{term "All :: (int => _) => _"}, |
574 @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]; |
574 @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]; |
575 val is_op = member (op =) ops; |
575 val is_op = member (op =) ops; |
576 val skip = not (fastype_of t = HOLogic.boolT) |
576 val skip = not (fastype_of t = HOLogic.boolT) |
577 in case t of |
577 in case t of |
614 | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F |
614 | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F |
615 | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) = |
615 | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) = |
616 Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2) |
616 Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2) |
617 | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) = |
617 | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) = |
618 Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2) |
618 Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2) |
619 | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) = |
619 | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) = |
620 Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2) |
620 Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2) |
621 | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) = |
621 | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) = |
622 Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2) |
622 Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2) |
623 | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') = |
623 | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') = |
624 Proc.Not (fm_of_term ps vs t') |
624 Proc.Not (fm_of_term ps vs t') |
685 |
685 |
686 val comp_ss = HOL_ss addsimps @{thms semiring_norm}; |
686 val comp_ss = HOL_ss addsimps @{thms semiring_norm}; |
687 |
687 |
688 fun strip_objimp ct = |
688 fun strip_objimp ct = |
689 (case Thm.term_of ct of |
689 (case Thm.term_of ct of |
690 Const (@{const_name "op -->"}, _) $ _ $ _ => |
690 Const (@{const_name HOL.implies}, _) $ _ $ _ => |
691 let val (A, B) = Thm.dest_binop ct |
691 let val (A, B) = Thm.dest_binop ct |
692 in A :: strip_objimp B end |
692 in A :: strip_objimp B end |
693 | _ => [ct]); |
693 | _ => [ct]); |
694 |
694 |
695 fun strip_objall ct = |
695 fun strip_objall ct = |
710 val (qvs, p) = strip_objall (Thm.dest_arg p') |
710 val (qvs, p) = strip_objall (Thm.dest_arg p') |
711 val (ps, c) = split_last (strip_objimp p) |
711 val (ps, c) = split_last (strip_objimp p) |
712 val qs = filter P ps |
712 val qs = filter P ps |
713 val q = if P c then c else @{cterm "False"} |
713 val q = if P c then c else @{cterm "False"} |
714 val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs |
714 val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs |
715 (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q) |
715 (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q) |
716 val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p' |
716 val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p' |
717 val ntac = (case qs of [] => q aconvc @{cterm "False"} |
717 val ntac = (case qs of [] => q aconvc @{cterm "False"} |
718 | _ => false) |
718 | _ => false) |
719 in |
719 in |
720 if ntac then no_tac |
720 if ntac then no_tac |