src/HOL/SVC_Oracle.ML
author wenzelm
Fri, 26 Oct 2001 23:58:21 +0200
changeset 11952 b10f1e8862f4
parent 11868 56db9f3a6b3e
permissions -rw-r--r--
* Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
     1
(*  Title:      HOL/SVC_Oracle.ML
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     5
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     6
Installing the oracle for SVC (Stanford Validity Checker)
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     7
7539
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
     8
The following code merely CALLS the oracle; 
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
     9
  the soundness-critical functions are at HOL/Tools/svc_funcs.ML
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    10
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    11
Based upon the work of Søren T. Heilmann
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    12
*)
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    13
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    14
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    15
(*Generalize an Isabelle formula, replacing by Vars
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    16
  all subterms not intelligible to SVC.*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    17
fun svc_abstract t =
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    18
  let
7539
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    19
    (*The oracle's result is given to the subgoal using compose_tac because
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    20
      its premises are matched against the assumptions rather than used
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    21
      to make subgoals.  Therefore , abstraction must copy the parameters
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    22
      precisely and make them available to all generated Vars.*)
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    23
    val params = Term.strip_all_vars t
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    24
    and body   = Term.strip_all_body t
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    25
    val Us = map #2 params
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    26
    val nPar = length params
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    27
    val vname = ref "V_a"
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    28
    val pairs = ref ([] : (term*term) list)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    29
    fun insert t = 
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    30
	let val T = fastype_of t
7539
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    31
            val v = Unify.combound (Var ((!vname,0), Us--->T),
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    32
				    0, nPar)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    33
	in  vname := bump_string (!vname); 
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    34
	    pairs := (t, v) :: !pairs;
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    35
	    v
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    36
	end;
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    37
    fun replace t = 
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    38
	case t of
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    39
	    Free _  => t  (*but not existing Vars, lest the names clash*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    40
	  | Bound _ => t
7539
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    41
	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    42
		      Some v => v
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    43
		    | None   => insert t)
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11707
diff changeset
    44
    (*abstraction of a numeric literal*)
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11707
diff changeset
    45
    fun lit (t as Const("0", _)) = t
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11707
diff changeset
    46
      | lit (t as Const("1", _)) = t
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11707
diff changeset
    47
      | lit (t as Const("Numeral.number_of", _) $ w) = t
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11707
diff changeset
    48
      | lit t = replace t
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    49
    (*abstraction of a real/rational expression*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    50
    fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    51
      | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    52
      | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    53
      | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    54
      | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11707
diff changeset
    55
      | rat t = lit t
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    56
    (*abstraction of an integer expression: no div, mod*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    57
    fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    58
      | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    59
      | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    60
      | int ((c as Const("uminus", _)) $ x) = c $ (int x)
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11707
diff changeset
    61
      | int t = lit t
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    62
    (*abstraction of a natural number expression: no minus*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    63
    fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    64
      | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    65
      | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11707
diff changeset
    66
      | nat t = lit t
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    67
    (*abstraction of a relation: =, <, <=*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    68
    fun rel (T, c $ x $ y) =
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    69
	    if T = HOLogic.realT then c $ (rat x) $ (rat y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    70
	    else if T = HOLogic.intT then c $ (int x) $ (int y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    71
	    else if T = HOLogic.natT then c $ (nat x) $ (nat y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    72
	    else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    73
	    else replace (c $ x $ y)   (*non-numeric comparison*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    74
    (*abstraction of a formula*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    75
    and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    76
      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    77
      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    78
      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    79
      | fm ((c as Const("True", _))) = c
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    80
      | fm ((c as Const("False", _))) = c
7539
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    81
      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    82
      | fm (t as Const("op <",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
680eca63b98e now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents: 7304
diff changeset
    83
      | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    84
      | fm t = replace t
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    85
    (*entry point, and abstraction of a meta-formula*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    86
    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    87
      | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    88
      | mt t = fm t  (*it might be a formula*)
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    89
  in (list_all (params, mt body), !pairs) end;
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    90
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    91
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    92
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    93
  abstracted.  Use via compose_tac, which performs no lifting but will
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    94
  instantiate variables.*)
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
    95
local val svc_thy = the_context () in
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
    96
7162
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    97
fun svc_tac i st = 
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
    98
  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
    99
      val (absPrem, _) = svc_abstract prem
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
   100
      val th = invoke_oracle svc_thy "svc_oracle"
7284
29105299799c now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents: 7237
diff changeset
   101
	             (#sign (rep_thm st), Svc.OracleExn absPrem)
7162
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
   102
   in 
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
   103
      compose_tac (false, th, 0) i st
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
   104
   end 
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
   105
   handle Svc.OracleExn _ => Seq.empty
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
   106
	| Subscript       => Seq.empty;
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
   107
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
   108
end;
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
   109
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
   110
7304
94c6f8f07631 if_svc_enabled;
wenzelm
parents: 7284
diff changeset
   111
(*check if user has SVC installed*)
94c6f8f07631 if_svc_enabled;
wenzelm
parents: 7284
diff changeset
   112
fun svc_enabled () = getenv "SVC_HOME" <> "";
94c6f8f07631 if_svc_enabled;
wenzelm
parents: 7284
diff changeset
   113
fun if_svc_enabled f x = if svc_enabled () then f x else ();