now with abstraction code previously in HOL/Tools/svc_funcs.ML
authorpaulson
Thu Aug 19 15:12:51 1999 +0200 (1999-08-19)
changeset 728429105299799c
parent 7283 5cfe2944910a
child 7285 52ea6848b908
now with abstraction code previously in HOL/Tools/svc_funcs.ML
src/HOL/SVC_Oracle.ML
     1.1 --- a/src/HOL/SVC_Oracle.ML	Thu Aug 19 15:11:12 1999 +0200
     1.2 +++ b/src/HOL/SVC_Oracle.ML	Thu Aug 19 15:12:51 1999 +0200
     1.3 @@ -8,6 +8,81 @@
     1.4  Based upon the work of Søren T. Heilmann
     1.5  *)
     1.6  
     1.7 +
     1.8 +(*Generalize an Isabelle formula, replacing by Vars
     1.9 +  all subterms not intelligible to SVC.*)
    1.10 +fun svc_abstract t =
    1.11 +  let
    1.12 +    val params = Term.strip_all_vars t
    1.13 +    and body   = Term.strip_all_body t
    1.14 +    val Us = map #2 params
    1.15 +    val nPar = length params
    1.16 +    val vname = ref "V_a"
    1.17 +    val pairs = ref ([] : (term*term) list)
    1.18 +    fun insert t = 
    1.19 +	let val T = fastype_of t
    1.20 +	    val v = Unify.combound (Var ((!vname,0), Us--->T),
    1.21 +				    0, nPar)
    1.22 +	in  vname := bump_string (!vname); 
    1.23 +	    pairs := (t, v) :: !pairs;
    1.24 +	    v
    1.25 +	end;
    1.26 +    fun replace t = 
    1.27 +	case t of
    1.28 +	    Free _  => t  (*but not existing Vars, lest the names clash*)
    1.29 +	  | Bound _ => t
    1.30 +	  | _ => (case gen_assoc (op aconv) (!pairs, t) of
    1.31 +		      Some v => v
    1.32 +		    | None   => insert t)
    1.33 +    (*abstraction of a real/rational expression*)
    1.34 +    fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.35 +      | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.36 +      | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.37 +      | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.38 +      | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
    1.39 +      | rat ((c as Const("RealDef.0r", _))) = c
    1.40 +      | rat ((c as Const("RealDef.1r", _))) = c 
    1.41 +      | rat (t as Const("Numeral.number_of", _) $ w) = t
    1.42 +      | rat t = replace t
    1.43 +    (*abstraction of an integer expression: no div, mod*)
    1.44 +    fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
    1.45 +      | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
    1.46 +      | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
    1.47 +      | int ((c as Const("uminus", _)) $ x) = c $ (int x)
    1.48 +      | int (t as Const("Numeral.number_of", _) $ w) = t
    1.49 +      | int t = replace t
    1.50 +    (*abstraction of a natural number expression: no minus*)
    1.51 +    fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
    1.52 +      | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
    1.53 +      | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
    1.54 +      | nat (t as Const("0", _)) = t
    1.55 +      | nat (t as Const("Numeral.number_of", _) $ w) = t
    1.56 +      | nat t = replace t
    1.57 +    (*abstraction of a relation: =, <, <=*)
    1.58 +    fun rel (T, c $ x $ y) =
    1.59 +	    if T = HOLogic.realT then c $ (rat x) $ (rat y)
    1.60 +	    else if T = HOLogic.intT then c $ (int x) $ (int y)
    1.61 +	    else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    1.62 +	    else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    1.63 +	    else replace (c $ x $ y)   (*non-numeric comparison*)
    1.64 +    (*abstraction of a formula*)
    1.65 +    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.66 +      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.67 +      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.68 +      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    1.69 +      | fm ((c as Const("True", _))) = c
    1.70 +      | fm ((c as Const("False", _))) = c
    1.71 +      | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
    1.72 +      | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
    1.73 +      | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
    1.74 +      | fm t = replace t
    1.75 +    (*entry point, and abstraction of a meta-formula*)
    1.76 +    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    1.77 +      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    1.78 +      | mt t = fm t  (*it might be a formula*)
    1.79 +  in (list_all (params, mt body), !pairs) end;
    1.80 +
    1.81 +
    1.82  (*Present the entire subgoal to the oracle, assumptions and all, but possibly
    1.83    abstracted.  Use via compose_tac, which performs no lifting but will
    1.84    instantiate variables.*)
    1.85 @@ -15,8 +90,9 @@
    1.86  
    1.87  fun svc_tac i st = 
    1.88    let val prem = BasisLibrary.List.nth (prems_of st, i-1)
    1.89 +      val (absPrem, _) = svc_abstract prem
    1.90        val th = invoke_oracle svc_thy "svc_oracle"
    1.91 -	             (#sign (rep_thm st), Svc.OracleExn prem)
    1.92 +	             (#sign (rep_thm st), Svc.OracleExn absPrem)
    1.93     in 
    1.94        compose_tac (false, th, 0) i st
    1.95     end