# HG changeset patch # User paulson # Date 937816808 -7200 # Node ID 680eca63b98e5cce7972b63193e5647cdd4f4c14 # Parent 35787339156179f1643d2a340134a832026b66c3 now uses Pattern.aeconv, not aconv, to test equality between the terms abstracted over; otherwise it is incomplete. Other changes are cosmetic diff -r 357873391561 -r 680eca63b98e src/HOL/SVC_Oracle.ML --- a/src/HOL/SVC_Oracle.ML Fri Sep 17 10:31:38 1999 +0200 +++ b/src/HOL/SVC_Oracle.ML Mon Sep 20 10:40:08 1999 +0200 @@ -5,6 +5,9 @@ Installing the oracle for SVC (Stanford Validity Checker) +The following code merely CALLS the oracle; + the soundness-critical functions are at HOL/Tools/svc_funcs.ML + Based upon the work of Søren T. Heilmann *) @@ -13,6 +16,10 @@ all subterms not intelligible to SVC.*) fun svc_abstract t = let + (*The oracle's result is given to the subgoal using compose_tac because + its premises are matched against the assumptions rather than used + to make subgoals. Therefore , abstraction must copy the parameters + precisely and make them available to all generated Vars.*) val params = Term.strip_all_vars t and body = Term.strip_all_body t val Us = map #2 params @@ -21,7 +28,7 @@ val pairs = ref ([] : (term*term) list) fun insert t = let val T = fastype_of t - val v = Unify.combound (Var ((!vname,0), Us--->T), + val v = Unify.combound (Var ((!vname,0), Us--->T), 0, nPar) in vname := bump_string (!vname); pairs := (t, v) :: !pairs; @@ -31,7 +38,7 @@ case t of Free _ => t (*but not existing Vars, lest the names clash*) | Bound _ => t - | _ => (case gen_assoc (op aconv) (!pairs, t) of + | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of Some v => v | None => insert t) (*abstraction of a real/rational expression*) @@ -72,9 +79,9 @@ | fm ((c as Const("Not", _)) $ p) = c $ (fm p) | fm ((c as Const("True", _))) = c | fm ((c as Const("False", _))) = c - | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t) - | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t) - | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t) + | fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t) + | fm (t as Const("op <", Type ("fun", [T,_])) $ _ $ _) = rel (T, t) + | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t) | fm t = replace t (*entry point, and abstraction of a meta-formula*) fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)