wenzelm@12869: (* Title: HOL/ex/SVC_Oracle.thy wenzelm@12869: ID: $Id$ wenzelm@12869: Author: Lawrence C Paulson wenzelm@12869: Copyright 1999 University of Cambridge wenzelm@12869: wenzelm@17388: Based upon the work of Søren T. Heilmann. wenzelm@17388: *) wenzelm@12869: wenzelm@17388: header {* Installing an oracle for SVC (Stanford Validity Checker) *} wenzelm@12869: wenzelm@16836: theory SVC_Oracle wenzelm@16836: imports Main wenzelm@24470: uses "svc_funcs.ML" wenzelm@16836: begin wenzelm@12869: wenzelm@12869: consts wenzelm@12869: iff_keep :: "[bool, bool] => bool" wenzelm@12869: iff_unfold :: "[bool, bool] => bool" wenzelm@12869: wenzelm@36176: hide_const iff_keep iff_unfold wenzelm@16836: wenzelm@28290: oracle svc_oracle = Svc.oracle wenzelm@12869: wenzelm@24470: ML {* wenzelm@24470: (* wenzelm@24470: Installing the oracle for SVC (Stanford Validity Checker) wenzelm@24470: wenzelm@24470: The following code merely CALLS the oracle; wenzelm@24470: the soundness-critical functions are at svc_funcs.ML wenzelm@24470: wenzelm@24470: Based upon the work of Søren T. Heilmann wenzelm@24470: *) wenzelm@24470: wenzelm@24470: wenzelm@24470: (*Generalize an Isabelle formula, replacing by Vars wenzelm@24470: all subterms not intelligible to SVC.*) wenzelm@24470: fun svc_abstract t = wenzelm@24470: let wenzelm@24470: (*The oracle's result is given to the subgoal using compose_tac because wenzelm@24470: its premises are matched against the assumptions rather than used wenzelm@24470: to make subgoals. Therefore , abstraction must copy the parameters wenzelm@24470: precisely and make them available to all generated Vars.*) wenzelm@24470: val params = Term.strip_all_vars t wenzelm@24470: and body = Term.strip_all_body t wenzelm@24470: val Us = map #2 params wenzelm@24470: val nPar = length params wenzelm@32740: val vname = Unsynchronized.ref "V_a" wenzelm@32740: val pairs = Unsynchronized.ref ([] : (term*term) list) wenzelm@24470: fun insert t = wenzelm@24470: let val T = fastype_of t wenzelm@24470: val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar) wenzelm@24470: in vname := Symbol.bump_string (!vname); wenzelm@24470: pairs := (t, v) :: !pairs; wenzelm@24470: v wenzelm@24470: end; wenzelm@24470: fun replace t = wenzelm@24470: case t of wenzelm@24470: Free _ => t (*but not existing Vars, lest the names clash*) wenzelm@24470: | Bound _ => t wenzelm@24470: | _ => (case AList.lookup Pattern.aeconv (!pairs) t of wenzelm@24470: SOME v => v wenzelm@24470: | NONE => insert t) wenzelm@24470: (*abstraction of a numeric literal*) haftmann@25929: fun lit t = if can HOLogic.dest_number t then t else replace t; wenzelm@24470: (*abstraction of a real/rational expression*) haftmann@35267: fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) haftmann@35267: | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) haftmann@35084: | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) haftmann@35267: | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) haftmann@35267: | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x) wenzelm@24470: | rat t = lit t wenzelm@24470: (*abstraction of an integer expression: no div, mod*) haftmann@35267: fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y) haftmann@35267: | int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y) haftmann@35267: | int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y) haftmann@35267: | int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x) wenzelm@24470: | int t = lit t wenzelm@24470: (*abstraction of a natural number expression: no minus*) haftmann@35267: fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y) haftmann@35267: | nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y) wenzelm@24470: | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x) wenzelm@24470: | nat t = lit t wenzelm@24470: (*abstraction of a relation: =, <, <=*) wenzelm@24470: fun rel (T, c $ x $ y) = wenzelm@24470: if T = HOLogic.realT then c $ (rat x) $ (rat y) wenzelm@24470: else if T = HOLogic.intT then c $ (int x) $ (int y) wenzelm@24470: else if T = HOLogic.natT then c $ (nat x) $ (nat y) wenzelm@24470: else if T = HOLogic.boolT then c $ (fm x) $ (fm y) wenzelm@24470: else replace (c $ x $ y) (*non-numeric comparison*) wenzelm@24470: (*abstraction of a formula*) haftmann@38549: and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q) haftmann@38549: | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q) haftmann@38549: | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q) haftmann@38558: | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p) haftmann@38558: | fm ((c as Const(@{const_name True}, _))) = c haftmann@38558: | fm ((c as Const(@{const_name False}, _))) = c haftmann@38549: | fm (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) haftmann@35092: | fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) haftmann@35092: | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t) wenzelm@24470: | fm t = replace t wenzelm@24470: (*entry point, and abstraction of a meta-formula*) haftmann@38558: fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p) wenzelm@24470: | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q) wenzelm@24470: | mt t = fm t (*it might be a formula*) wenzelm@24470: in (list_all (params, mt body), !pairs) end; wenzelm@24470: wenzelm@24470: wenzelm@24470: (*Present the entire subgoal to the oracle, assumptions and all, but possibly wenzelm@24470: abstracted. Use via compose_tac, which performs no lifting but will wenzelm@24470: instantiate variables.*) wenzelm@24470: wenzelm@28290: val svc_tac = CSUBGOAL (fn (ct, i) => wenzelm@24470: let wenzelm@28290: val thy = Thm.theory_of_cterm ct; wenzelm@28290: val (abs_goal, _) = svc_abstract (Thm.term_of ct); wenzelm@28290: val th = svc_oracle (Thm.cterm_of thy abs_goal); wenzelm@28290: in compose_tac (false, th, 0) i end wenzelm@28290: handle TERM _ => no_tac); wenzelm@24470: *} wenzelm@20813: wenzelm@12869: end