author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 7539  680eca63b98e 
child 11707  6c45813c2db1 
permissions  rwrr 
7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

1 
(* Title: HOL/SVC_Oracle.ML 
7144  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson 

4 
Copyright 1999 University of Cambridge 

5 

6 
Installing the oracle for SVC (Stanford Validity Checker) 

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 soundnesscritical 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  11 
Based upon the work of Søren T. Heilmann 
12 
*) 

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) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

44 
(*abstraction of a real/rational expression*) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

45 
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

46 
 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

47 
 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

48 
 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

49 
 rat ((c as Const("uminus", _)) $ x) = c $ (rat x) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

50 
 rat ((c as Const("RealDef.0r", _))) = c 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

51 
 rat ((c as Const("RealDef.1r", _))) = c 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

52 
 rat (t as Const("Numeral.number_of", _) $ w) = t 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

53 
 rat t = replace t 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

54 
(*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

55 
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

56 
 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

57 
 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("uminus", _)) $ x) = c $ (int x) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

59 
 int (t as Const("Numeral.number_of", _) $ w) = t 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

60 
 int t = replace t 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

61 
(*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

62 
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

63 
 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("Suc", _)) $ x) = c $ (nat x) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

65 
 nat (t as Const("0", _)) = t 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

66 
 nat (t as Const("Numeral.number_of", _) $ w) = t 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

67 
 nat t = replace t 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

68 
(*abstraction of a relation: =, <, <=*) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

69 
fun rel (T, c $ x $ y) = 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

70 
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

71 
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

72 
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

73 
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

74 
else replace (c $ x $ y) (*nonnumeric comparison*) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

75 
(*abstraction of a formula*) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

76 
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

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("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

79 
 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

80 
 fm ((c as Const("True", _))) = c 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

81 
 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

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) 
680eca63b98e
now uses Pattern.aeconv, not aconv, to test equality between the terms
paulson
parents:
7304
diff
changeset

84 
 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

85 
 fm t = replace t 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

86 
(*entry point, and abstraction of a metaformula*) 
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

87 
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

88 
 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

89 
 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

90 
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

91 

29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

92 

7144  93 
(*Present the entire subgoal to the oracle, assumptions and all, but possibly 
94 
abstracted. Use via compose_tac, which performs no lifting but will 

95 
instantiate variables.*) 

7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

96 
local val svc_thy = the_context () in 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

97 

7162  98 
fun svc_tac i st = 
7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

99 
let val prem = BasisLibrary.List.nth (prems_of st, i1) 
7284
29105299799c
now with abstraction code previously in HOL/Tools/svc_funcs.ML
paulson
parents:
7237
diff
changeset

100 
val (absPrem, _) = svc_abstract prem 
7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

101 
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

102 
(#sign (rep_thm st), Svc.OracleExn absPrem) 
7162  103 
in 
104 
compose_tac (false, th, 0) i st 

105 
end 

106 
handle Svc.OracleExn _ => Seq.empty 

107 
 Subscript => Seq.empty; 

7144  108 

7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

109 
end; 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

110 

7144  111 

7304  112 
(*check if user has SVC installed*) 
113 
fun svc_enabled () = getenv "SVC_HOME" <> ""; 

114 
fun if_svc_enabled f x = if svc_enabled () then f x else (); 