author  boehmes 
Wed, 12 May 2010 23:53:48 +0200  
changeset 36884  88cf4896b980 
parent 36084  3176ec2244ad 
child 36891  e0d295cb8bfd 
permissions  rwrr 
33010  1 
(* Title: HOL/SMT/SMT_Base.thy 
2 
Author: Sascha Boehme, TU Muenchen 

3 
*) 

4 

5 
header {* SMTspecific definitions and basic tools *} 

6 

7 
theory SMT_Base 

35105  8 
imports Real "~~/src/HOL/Word/Word" 
33010  9 
uses 
35943
51b9155467cc
cache_io is now just a single ML file instead of a component
boehmes
parents:
35151
diff
changeset

10 
"~~/src/Tools/cache_io.ML" 
33010  11 
("Tools/smt_normalize.ML") 
12 
("Tools/smt_monomorph.ML") 

13 
("Tools/smt_translate.ML") 

14 
("Tools/smt_solver.ML") 

15 
("Tools/smtlib_interface.ML") 

16 
begin 

17 

18 
section {* Triggers for quantifier instantiation *} 

19 

20 
text {* 

21 
Some SMT solvers support triggers for quantifier instantiation. Each trigger 

22 
consists of one ore more patterns. A pattern may either be a list of positive 

23 
subterms (the first being tagged by "pat" and the consecutive subterms tagged 

24 
by "andpat"), or a list of negative subterms (the first being tagged by "nopat" 

25 
and the consecutive subterms tagged by "andpat"). 

26 
*} 

27 

28 
datatype pattern = Pattern 

29 

30 
definition pat :: "'a \<Rightarrow> pattern" 

31 
where "pat _ = Pattern" 

32 

33249  33 
definition nopat :: "'a \<Rightarrow> pattern" 
33010  34 
where "nopat _ = Pattern" 
35 

36 
definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60) 

37 
where "_ andpat _ = Pattern" 

38 

39 
definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool" 

40 
where "trigger _ P = P" 

41 

42 

36884
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36084
diff
changeset

43 

33010  44 
section {* Arithmetic *} 
45 

46 
text {* 

47 
The sign of @{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"} follows the sign of the 

48 
divisor. In contrast to that, the sign of the following operation is that of 

49 
the dividend. 

50 
*} 

51 

52 
definition rem :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "rem" 70) 

53 
where "a rem b = 

54 
(if (a \<ge> 0 \<and> b < 0) \<or> (a < 0 \<and> b \<ge> 0) then  (a mod b) else a mod b)" 

55 

56 

57 

58 
section {* Bitvectors *} 

59 

60 
text {* 

61 
The following definitions provide additional functions not found in HOLWord. 

62 
*} 

63 

64 
definition sdiv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "sdiv" 70) 

65 
where "w1 sdiv w2 = word_of_int (sint w1 div sint w2)" 

66 

67 
definition smod :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "smod" 70) 

68 
(* sign follows divisor *) 

69 
where "w1 smod w2 = word_of_int (sint w1 mod sint w2)" 

70 

71 
definition srem :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "srem" 70) 

72 
(* sign follows dividend *) 

73 
where "w1 srem w2 = word_of_int (sint w1 rem sint w2)" 

74 

75 
definition bv_shl :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

76 
where "bv_shl w1 w2 = (w1 << unat w2)" 

77 

78 
definition bv_lshr :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

79 
where "bv_lshr w1 w2 = (w1 >> unat w2)" 

80 

81 
definition bv_ashr :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

82 
where "bv_ashr w1 w2 = (w1 >>> unat w2)" 

83 

84 

36884
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36084
diff
changeset

85 

33010  86 
section {* HigherOrder Encoding *} 
87 

88 
definition "apply" where "apply f x = f x" 

89 

34960
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

90 
definition array_ext where "array_ext a b = (SOME x. a = b \<or> a x \<noteq> b x)" 
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

91 

1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

92 
lemma fun_upd_eq: "(f = f (x := y)) = (f x = y)" 
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

93 
proof 
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

94 
assume "f = f(x:=y)" 
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

95 
hence "f x = (f(x:=y)) x" by simp 
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

96 
thus "f x = y" by simp 
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

97 
qed (auto simp add: ext) 
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

98 

1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

99 
lemmas array_rules = 
1d5ee19ef940
support skolem constant for extensional arrays in Z3 proofs
boehmes
parents:
33249
diff
changeset

100 
ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_upd_eq apply_def 
33010  101 

102 

36884
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36084
diff
changeset

103 

33010  104 
section {* Firstorder logic *} 
105 

106 
text {* 

107 
Some SMT solver formats require a strict separation between formulas and terms. 

108 
The following marker symbols are used internally to separate those categories: 

109 
*} 

110 

111 
definition formula :: "bool \<Rightarrow> bool" where "formula x = x" 

112 
definition "term" where "term x = x" 

113 

114 
text {* 

115 
Predicate symbols also occurring as function symbols are turned into function 

116 
symbols by translating atomic formulas into terms: 

117 
*} 

118 

119 
abbreviation holds :: "bool \<Rightarrow> bool" where "holds \<equiv> (\<lambda>P. term P = term True)" 

120 

121 
text {* 

122 
The following constant represents equivalence, to be treated differently than 

123 
the (polymorphic) equality predicate: 

124 
*} 

125 

126 
definition iff :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "iff" 50) where 

127 
"(x iff y) = (x = y)" 

128 

129 

36884
88cf4896b980
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
boehmes
parents:
36084
diff
changeset

130 

33010  131 
section {* Setup *} 
132 

133 
use "Tools/smt_normalize.ML" 

134 
use "Tools/smt_monomorph.ML" 

135 
use "Tools/smt_translate.ML" 

136 
use "Tools/smt_solver.ML" 

137 
use "Tools/smtlib_interface.ML" 

138 

36084
3176ec2244ad
always unfold definitions of specific constants (including special binders)
boehmes
parents:
35943
diff
changeset

139 
setup {* SMT_Solver.setup *} 
33010  140 

141 
end 