no longer declare .psimps rules as [simp].
This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.
(* Title: HOL/ex/SVC_Oracle.thy
ID: $Id$
Author: Lawrence C Paulson
Copyright 1999 University of Cambridge
Based upon the work of Søren T. Heilmann.
*)
header {* Installing an oracle for SVC (Stanford Validity Checker) *}
theory SVC_Oracle
imports Main
uses "svc_funcs.ML"
begin
consts
iff_keep :: "[bool, bool] => bool"
iff_unfold :: "[bool, bool] => bool"
hide_const iff_keep iff_unfold
oracle svc_oracle = Svc.oracle
ML {*
(*
Installing the oracle for SVC (Stanford Validity Checker)
The following code merely CALLS the oracle;
the soundness-critical functions are at svc_funcs.ML
Based upon the work of Søren T. Heilmann
*)
(*Generalize an Isabelle formula, replacing by Vars
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
val nPar = length params
val vname = Unsynchronized.ref "V_a"
val pairs = Unsynchronized.ref ([] : (term*term) list)
fun insert t =
let val T = fastype_of t
val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
in vname := Symbol.bump_string (!vname);
pairs := (t, v) :: !pairs;
v
end;
fun replace t =
case t of
Free _ => t (*but not existing Vars, lest the names clash*)
| Bound _ => t
| _ => (case AList.lookup Pattern.aeconv (!pairs) t of
SOME v => v
| NONE => insert t)
(*abstraction of a numeric literal*)
fun lit t = if can HOLogic.dest_number t then t else replace t;
(*abstraction of a real/rational expression*)
fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
| rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x)
| rat t = lit t
(*abstraction of an integer expression: no div, mod*)
fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
| int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
| int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y)
| int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x)
| int t = lit t
(*abstraction of a natural number expression: no minus*)
fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
| nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
| nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
| nat t = lit t
(*abstraction of a relation: =, <, <=*)
fun rel (T, c $ x $ y) =
if T = HOLogic.realT then c $ (rat x) $ (rat y)
else if T = HOLogic.intT then c $ (int x) $ (int y)
else if T = HOLogic.natT then c $ (nat x) $ (nat y)
else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
else replace (c $ x $ y) (*non-numeric comparison*)
(*abstraction of a formula*)
and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
| fm ((c as Const(@{const_name True}, _))) = c
| fm ((c as Const(@{const_name False}, _))) = c
| fm (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
| mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
| mt t = fm t (*it might be a formula*)
in (list_all (params, mt body), !pairs) end;
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
abstracted. Use via compose_tac, which performs no lifting but will
instantiate variables.*)
val svc_tac = CSUBGOAL (fn (ct, i) =>
let
val thy = Thm.theory_of_cterm ct;
val (abs_goal, _) = svc_abstract (Thm.term_of ct);
val th = svc_oracle (Thm.cterm_of thy abs_goal);
in compose_tac (false, th, 0) i end
handle TERM _ => no_tac);
*}
end