90 (*Transform an Term to an natural number*) |
90 (*Transform an Term to an natural number*) |
91 |
91 |
92 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0 |
92 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0 |
93 |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1 |
93 |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1 |
94 |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; |
94 |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; |
95 (*Some terms often used for pattern matching*) |
95 (*SOME terms often used for pattern matching*) |
96 |
96 |
97 val zero = mk_numeral 0; |
97 val zero = mk_numeral 0; |
98 val one = mk_numeral 1; |
98 val one = mk_numeral 1; |
99 |
99 |
100 (*Tests if a Term is representing a number*) |
100 (*Tests if a Term is representing a number*) |
448 |
448 |
449 val operations = |
449 val operations = |
450 [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), |
450 [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), |
451 ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; |
451 ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; |
452 |
452 |
453 fun applyoperation (Some f) (a,b) = f (a, b) |
453 fun applyoperation (SOME f) (a,b) = f (a, b) |
454 |applyoperation _ (_, _) = false; |
454 |applyoperation _ (_, _) = false; |
455 |
455 |
456 (*Evaluation of constant atomic formulas*) |
456 (*Evaluation of constant atomic formulas*) |
457 (*FIXME : This is an optimation but still incorrect !! *) |
457 (*FIXME : This is an optimation but still incorrect !! *) |
458 (* |
458 (* |
462 ((if dvd_op(s,t) then HOLogic.true_const |
462 ((if dvd_op(s,t) then HOLogic.true_const |
463 else HOLogic.false_const) |
463 else HOLogic.false_const) |
464 handle _ => at) |
464 handle _ => at) |
465 else |
465 else |
466 case assoc (operations,p) of |
466 case assoc (operations,p) of |
467 Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const) |
467 SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const) |
468 handle _ => at) |
468 handle _ => at) |
469 | _ => at) |
469 | _ => at) |
470 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
470 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
471 case assoc (operations,p) of |
471 case assoc (operations,p) of |
472 Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then |
472 SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then |
473 HOLogic.false_const else HOLogic.true_const) |
473 HOLogic.false_const else HOLogic.true_const) |
474 handle _ => at) |
474 handle _ => at) |
475 | _ => at) |
475 | _ => at) |
476 | _ => at; |
476 | _ => at; |
477 |
477 |
478 *) |
478 *) |
479 |
479 |
480 fun evalc_atom at = case at of |
480 fun evalc_atom at = case at of |
481 (Const (p,_) $ s $ t) => |
481 (Const (p,_) $ s $ t) => |
482 ( case assoc (operations,p) of |
482 ( case assoc (operations,p) of |
483 Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const) |
483 SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const) |
484 handle _ => at) |
484 handle _ => at) |
485 | _ => at) |
485 | _ => at) |
486 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
486 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
487 case assoc (operations,p) of |
487 case assoc (operations,p) of |
488 Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then |
488 SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then |
489 HOLogic.false_const else HOLogic.true_const) |
489 HOLogic.false_const else HOLogic.true_const) |
490 handle _ => at) |
490 handle _ => at) |
491 | _ => at) |
491 | _ => at) |
492 | _ => at; |
492 | _ => at; |
493 |
493 |
709 (* Try to find a withness for the formula *) |
709 (* Try to find a withness for the formula *) |
710 |
710 |
711 fun inf_w mi d vars x p = |
711 fun inf_w mi d vars x p = |
712 let val f = if mi then minusinf else plusinf in |
712 let val f = if mi then minusinf else plusinf in |
713 case (simpl (minusinf x p)) of |
713 case (simpl (minusinf x p)) of |
714 Const("True",_) => (Some (mk_numeral 1), HOLogic.true_const) |
714 Const("True",_) => (SOME (mk_numeral 1), HOLogic.true_const) |
715 |Const("False",_) => (None,HOLogic.false_const) |
715 |Const("False",_) => (NONE,HOLogic.false_const) |
716 |F => |
716 |F => |
717 let |
717 let |
718 fun h n = |
718 fun h n = |
719 case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of |
719 case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of |
720 Const("True",_) => (Some (mk_numeral n),HOLogic.true_const) |
720 Const("True",_) => (SOME (mk_numeral n),HOLogic.true_const) |
721 |F' => if n=1 then (None,F') |
721 |F' => if n=1 then (NONE,F') |
722 else let val (rw,rf) = h (n-1) in |
722 else let val (rw,rf) = h (n-1) in |
723 (rw,HOLogic.mk_disj(F',rf)) |
723 (rw,HOLogic.mk_disj(F',rf)) |
724 end |
724 end |
725 |
725 |
726 in (h d) |
726 in (h d) |
727 end |
727 end |
728 end; |
728 end; |
729 |
729 |
730 fun set_w d b st vars x p = let |
730 fun set_w d b st vars x p = let |
731 fun h ns = case ns of |
731 fun h ns = case ns of |
732 [] => (None,HOLogic.false_const) |
732 [] => (NONE,HOLogic.false_const) |
733 |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of |
733 |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of |
734 Const("True",_) => (Some n,HOLogic.true_const) |
734 Const("True",_) => (SOME n,HOLogic.true_const) |
735 |F' => let val (rw,rf) = h nl |
735 |F' => let val (rw,rf) = h nl |
736 in (rw,HOLogic.mk_disj(F',rf)) |
736 in (rw,HOLogic.mk_disj(F',rf)) |
737 end) |
737 end) |
738 val f = if b then linear_add else linear_sub |
738 val f = if b then linear_add else linear_sub |
739 val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[]) |
739 val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[]) |
740 in h p_elements |
740 in h p_elements |
741 end; |
741 end; |
742 |
742 |
743 fun withness d b st vars x p = case (inf_w b d vars x p) of |
743 fun withness d b st vars x p = case (inf_w b d vars x p) of |
744 (Some n,_) => (Some n,HOLogic.true_const) |
744 (SOME n,_) => (SOME n,HOLogic.true_const) |
745 |(None,Pinf) => (case (set_w d b st vars x p) of |
745 |(NONE,Pinf) => (case (set_w d b st vars x p) of |
746 (Some n,_) => (Some n,HOLogic.true_const) |
746 (SOME n,_) => (SOME n,HOLogic.true_const) |
747 |(_,Pst) => (None,HOLogic.mk_disj(Pinf,Pst))); |
747 |(_,Pst) => (NONE,HOLogic.mk_disj(Pinf,Pst))); |
748 |
748 |
749 |
749 |
750 |
750 |
751 |
751 |
752 (*Cooper main procedure*) |
752 (*Cooper main procedure*) |