summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 14 Feb 2006 13:03:00 +0100 | |

changeset 19037 | 3be721728a6c |

parent 19036 | 73782d21e855 |

child 19038 | 62c5f7591a43 |

fixed tracing

--- a/src/Provers/blast.ML Mon Feb 13 17:02:54 2006 +0100 +++ b/src/Provers/blast.ML Tue Feb 14 13:03:00 2006 +0100 @@ -604,8 +604,24 @@ fun string_of sign d t = Sign.string_of_term sign (showTerm d t); +(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like + Ex(P) is duplicated as the assumption ~Ex(P). *) +fun negOfGoal (Const ("*Goal*", _) $ G) = negate G + | negOfGoal G = G; + +fun negOfGoal2 (G,md) = (negOfGoal G, md); + +(*Converts all Goals to Nots in the safe parts of a branch. They could + have been moved there from the literals list after substitution (equalSubst). + There can be at most one--this function could be made more efficient.*) +fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; + +(*Tactic. Convert *Goal* to negated assumption in FIRST position*) +fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN + rotate_tac ~1 i; + fun traceTerm sign t = - let val t' = norm t + let val t' = norm (negOfGoal t) val stm = string_of sign 8 t' in case topType sign t' of @@ -792,22 +808,6 @@ fun joinMd md [] = [] | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs; -(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like - Ex(P) is duplicated as the assumption ~Ex(P). *) -fun negOfGoal (Const ("*Goal*", _) $ G) = negate G - | negOfGoal G = G; - -fun negOfGoal2 (G,md) = (negOfGoal G, md); - -(*Converts all Goals to Nots in the safe parts of a branch. They could - have been moved there from the literals list after substitution (equalSubst). - There can be at most one--this function could be made more efficient.*) -fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; - -(*Tactic. Convert *Goal* to negated assumption in FIRST position*) -fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN - rotate_tac ~1 i; - (** Backtracking and Pruning **)