--- a/src/HOL/Library/Code_Char.thy Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/Library/Code_Char.thy Sat Apr 09 13:10:20 2011 +0200
@@ -59,6 +59,6 @@
(Scala "!(_.toList)")
-declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]
+(*declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]*)
end
--- a/src/HOL/Quickcheck_Exhaustive.thy Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sat Apr 09 13:10:20 2011 +0200
@@ -16,18 +16,39 @@
subsection {* exhaustive generator type classes *}
class exhaustive = term_of +
-fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+ fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+
+class full_exhaustive = term_of +
+ fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+
+instantiation code_numeral :: full_exhaustive
+begin
+
+function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+ where "full_exhaustive_code_numeral' f d i =
+ (if d < i then None
+ else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
+by pat_completeness auto
+
+termination
+ by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
+
+definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
+
+instance ..
+
+end
instantiation code_numeral :: exhaustive
begin
-function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
where "exhaustive_code_numeral' f d i =
(if d < i then None
- else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))"
+ else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
by pat_completeness auto
-termination
+termination
by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
definition "exhaustive f d = exhaustive_code_numeral' f d 0"
@@ -39,7 +60,16 @@
instantiation nat :: exhaustive
begin
-definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
+definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
+
+instance ..
+
+end
+
+instantiation nat :: full_exhaustive
+begin
+
+definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
instance ..
@@ -48,8 +78,8 @@
instantiation int :: exhaustive
begin
-function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
- where "exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => exhaustive' f d (i + 1)))"
+function exhaustive' :: "(int => term list option) => int => int => term list option"
+ where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
by pat_completeness auto
termination
@@ -61,11 +91,37 @@
end
+instantiation int :: full_exhaustive
+begin
+
+function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
+ where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"
+by pat_completeness auto
+
+termination
+ by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
+
+definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
+
+instance ..
+
+end
+
instantiation prod :: (exhaustive, exhaustive) exhaustive
begin
definition
- "exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y),
+ "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
+
+instance ..
+
+end
+
+instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
+begin
+
+definition
+ "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
%u. let T1 = (Typerep.typerep (TYPE('a)));
T2 = (Typerep.typerep (TYPE('b)))
in Code_Evaluation.App (Code_Evaluation.App (
@@ -80,11 +136,29 @@
instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
begin
-fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
+where
+ "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
+ orelse (if i > 1 then
+ exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
+ f (g(a := b))) d) d) (i - 1) d else None)"
+
+definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
where
- "exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
+ "exhaustive_fun f d = exhaustive_fun' f d d"
+
+instance ..
+
+end
+
+instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
+begin
+
+fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+where
+ "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
orelse (if i > 1 then
- exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt).
+ full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
f (g(a := b),
(%_. let A = (Typerep.typerep (TYPE('a)));
B = (Typerep.typerep (TYPE('b)));
@@ -94,9 +168,9 @@
(Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
(gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
-definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
+definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
where
- "exhaustive_fun f d = exhaustive_fun' f d d"
+ "full_exhaustive_fun f d = full_exhaustive_fun' f d d"
instance ..
@@ -351,6 +425,20 @@
class bounded_forall =
fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
+subsection {* Fast exhaustive combinators *}
+
+
+class fast_exhaustive = term_of +
+ fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
+
+consts throw_Counterexample :: "term list => unit"
+consts catch_Counterexample :: "unit => term list option"
+
+code_const throw_Counterexample
+ (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
+code_const catch_Counterexample
+ (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
+
subsection {* Defining combinators for any first-order data type *}
definition catch_match :: "term list option => term list option => term list option"
--- a/src/HOL/Rat.thy Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/Rat.thy Sat Apr 09 13:10:20 2011 +0200
@@ -1136,7 +1136,17 @@
begin
definition
- "exhaustive f d = exhaustive (%(k, kt). exhaustive (%(l, lt).
+ "exhaustive f d = exhaustive (%k. exhaustive (%l. f (Fract (Code_Numeral.int_of k) (Code_Numeral.int_of l))) d) d"
+
+instance ..
+
+end
+
+instantiation rat :: full_exhaustive
+begin
+
+definition
+ "full_exhaustive f d = full_exhaustive (%(k, kt). full_exhaustive (%(l, lt).
f (valterm_fract (Code_Numeral.int_of k, %_. Code_Evaluation.term_of (Code_Numeral.int_of k)) (Code_Numeral.int_of l, %_. Code_Evaluation.term_of (Code_Numeral.int_of l)))) d) d"
instance ..
--- a/src/HOL/RealDef.thy Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/RealDef.thy Sat Apr 09 13:10:20 2011 +0200
@@ -1772,7 +1772,17 @@
begin
definition
- "exhaustive f d = exhaustive (%r. f (valterm_ratreal r)) d"
+ "exhaustive f d = exhaustive (%r. f (Ratreal r)) d"
+
+instance ..
+
+end
+
+instantiation real :: full_exhaustive
+begin
+
+definition
+ "full_exhaustive f d = full_exhaustive (%r. f (valterm_ratreal r)) d"
instance ..
--- a/src/HOL/SMT_Examples/SMT_Examples.certs Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs Sat Apr 09 13:10:20 2011 +0200
@@ -15018,3 +15018,219 @@
#36 := [asserted]: #16
[mp #36 #70]: false
unsat
+1953a39a3cc38daf2fde4846aa1d5cbc2ff95785 60 0
+#2 := false
+#8 := 0::Int
+decl ?v1!0 :: Int
+#67 := ?v1!0
+#70 := (<= ?v1!0 0::Int)
+#63 := (not #70)
+#11 := 1::Int
+#68 := (>= ?v1!0 1::Int)
+#69 := (not #68)
+#79 := (or #69 #63)
+#82 := (not #79)
+#64 := (or #63 #69)
+#71 := (not #64)
+#83 := (iff #71 #82)
+#80 := (iff #64 #79)
+#81 := [rewrite]: #80
+#84 := [monotonicity #81]: #83
+#9 := (:var 0 Int)
+#48 := (>= #9 1::Int)
+#46 := (not #48)
+#42 := (<= #9 0::Int)
+#43 := (not #42)
+#50 := (or #43 #46)
+#53 := (forall (vars (?v1 Int)) #50)
+#56 := (not #53)
+#72 := (~ #56 #71)
+#73 := [sk]: #72
+#12 := (< #9 1::Int)
+#10 := (< 0::Int #9)
+#13 := (or #10 #12)
+#14 := (forall (vars (?v0 Int) (?v1 Int)) #13)
+#15 := (not #14)
+#59 := (iff #15 #56)
+#36 := (forall (vars (?v1 Int)) #13)
+#39 := (not #36)
+#57 := (iff #39 #56)
+#54 := (iff #36 #53)
+#51 := (iff #13 #50)
+#47 := (iff #12 #46)
+#49 := [rewrite]: #47
+#44 := (iff #10 #43)
+#45 := [rewrite]: #44
+#52 := [monotonicity #45 #49]: #51
+#55 := [quant-intro #52]: #54
+#58 := [monotonicity #55]: #57
+#40 := (iff #15 #39)
+#37 := (iff #14 #36)
+#38 := [elim-unused]: #37
+#41 := [monotonicity #38]: #40
+#60 := [trans #41 #58]: #59
+#35 := [asserted]: #15
+#61 := [mp #35 #60]: #56
+#76 := [mp~ #61 #73]: #71
+#77 := [mp #76 #84]: #82
+#85 := [not-or-elim #77]: #70
+#78 := [not-or-elim #77]: #68
+#141 := [th-lemma arith farkas 1 1]: #64
+#142 := [unit-resolution #141 #78]: #63
+[unit-resolution #142 #85]: false
+unsat
+4d18c87aa576f201e48ea20e31f11fb8675b59d4 8 0
+#2 := false
+#1 := true
+#33 := (not true)
+#63 := (iff #33 false)
+#65 := [rewrite]: #63
+#62 := [asserted]: #33
+[mp #62 #65]: false
+unsat
+ad406fc43130e24f380abadc1fc8a246fab490af 145 0
+#2 := false
+decl f3 :: (-> S2 Int S1)
+#22 := 42::Int
+decl f4 :: (-> S3 Int S2)
+#20 := 3::Int
+decl f6 :: S3
+#18 := f6
+#21 := (f4 f6 3::Int)
+#23 := (f3 #21 42::Int)
+decl f1 :: S1
+#4 := f1
+#86 := (= f1 #23)
+decl f5 :: S3
+#8 := f5
+#255 := (f4 f5 3::Int)
+#246 := (f3 #255 42::Int)
+#568 := (= #246 #23)
+#207 := (= #23 #246)
+#202 := (= #21 #255)
+#558 := (= #255 #21)
+#83 := (= f5 f6)
+#92 := (not #83)
+#93 := (or #92 #86)
+#98 := (not #93)
+#24 := (= #23 f1)
+#19 := (= f6 f5)
+#25 := (implies #19 #24)
+#26 := (not #25)
+#99 := (iff #26 #98)
+#96 := (iff #25 #93)
+#89 := (implies #83 #86)
+#94 := (iff #89 #93)
+#95 := [rewrite]: #94
+#90 := (iff #25 #89)
+#87 := (iff #24 #86)
+#88 := [rewrite]: #87
+#84 := (iff #19 #83)
+#85 := [rewrite]: #84
+#91 := [monotonicity #85 #88]: #90
+#97 := [trans #91 #95]: #96
+#100 := [monotonicity #97]: #99
+#82 := [asserted]: #26
+#103 := [mp #82 #100]: #98
+#101 := [not-or-elim #103]: #83
+#564 := [monotonicity #101]: #558
+#565 := [symm #564]: #202
+#208 := [monotonicity #565]: #207
+#566 := [symm #208]: #568
+#257 := (= f1 #246)
+#11 := (:var 0 Int)
+#9 := (:var 1 Int)
+#10 := (f4 f5 #9)
+#12 := (f3 #10 #11)
+#13 := (pattern #12)
+#64 := 0::Int
+#61 := -1::Int
+#62 := (* -1::Int #11)
+#63 := (+ #9 #62)
+#65 := (<= #63 0::Int)
+#47 := (= f1 #12)
+#71 := (iff #47 #65)
+#76 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #71)
+#116 := (~ #76 #76)
+#114 := (~ #71 #71)
+#115 := [refl]: #114
+#117 := [nnf-pos #115]: #116
+#15 := (<= #9 #11)
+#14 := (= #12 f1)
+#16 := (iff #14 #15)
+#17 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #16)
+#79 := (iff #17 #76)
+#53 := (iff #15 #47)
+#58 := (forall (vars (?v0 Int) (?v1 Int)) (:pat #13) #53)
+#77 := (iff #58 #76)
+#74 := (iff #53 #71)
+#68 := (iff #65 #47)
+#72 := (iff #68 #71)
+#73 := [rewrite]: #72
+#69 := (iff #53 #68)
+#66 := (iff #15 #65)
+#67 := [rewrite]: #66
+#70 := [monotonicity #67]: #69
+#75 := [trans #70 #73]: #74
+#78 := [quant-intro #75]: #77
+#59 := (iff #17 #58)
+#56 := (iff #16 #53)
+#50 := (iff #47 #15)
+#54 := (iff #50 #53)
+#55 := [rewrite]: #54
+#51 := (iff #16 #50)
+#48 := (iff #14 #47)
+#49 := [rewrite]: #48
+#52 := [monotonicity #49]: #51
+#57 := [trans #52 #55]: #56
+#60 := [quant-intro #57]: #59
+#80 := [trans #60 #78]: #79
+#46 := [asserted]: #17
+#81 := [mp #46 #80]: #76
+#106 := [mp~ #81 #117]: #76
+#557 := (not #76)
+#220 := (or #557 #257)
+#168 := (* -1::Int 42::Int)
+#253 := (+ 3::Int #168)
+#254 := (<= #253 0::Int)
+#258 := (iff #257 #254)
+#221 := (or #557 #258)
+#223 := (iff #221 #220)
+#560 := (iff #220 #220)
+#561 := [rewrite]: #560
+#573 := (iff #258 #257)
+#1 := true
+#571 := (iff #257 true)
+#572 := (iff #571 #257)
+#232 := [rewrite]: #572
+#231 := (iff #258 #571)
+#575 := (iff #254 true)
+#576 := -39::Int
+#245 := (<= -39::Int 0::Int)
+#579 := (iff #245 true)
+#580 := [rewrite]: #579
+#577 := (iff #254 #245)
+#570 := (= #253 -39::Int)
+#186 := -42::Int
+#260 := (+ 3::Int -42::Int)
+#233 := (= #260 -39::Int)
+#363 := [rewrite]: #233
+#239 := (= #253 #260)
+#259 := (= #168 -42::Int)
+#256 := [rewrite]: #259
+#574 := [monotonicity #256]: #239
+#244 := [trans #574 #363]: #570
+#578 := [monotonicity #244]: #577
+#581 := [trans #578 #580]: #575
+#236 := [monotonicity #581]: #231
+#216 := [trans #236 #232]: #573
+#559 := [monotonicity #216]: #223
+#562 := [trans #559 #561]: #223
+#222 := [quant-inst #20 #22]: #221
+#563 := [mp #222 #562]: #220
+#567 := [unit-resolution #563 #106]: #257
+#569 := [trans #567 #566]: #86
+#102 := (not #86)
+#104 := [not-or-elim #103]: #102
+[unit-resolution #104 #569]: false
+unsat
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Sat Apr 09 13:10:20 2011 +0200
@@ -390,11 +390,12 @@
lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt
-
lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt
lemma "\<forall>x::int. SMT.trigger [[SMT.pat x]] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
+lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt
+
subsection {* Non-linear arithmetic over integers and reals *}
@@ -468,6 +469,9 @@
"f (\<forall>x. g x) \<Longrightarrow> True"
by smt+
+lemma True using let_rsp by smt
+
+lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt
lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps)
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Apr 09 13:10:20 2011 +0200
@@ -15,6 +15,7 @@
val put_counterexample_batch: (unit -> (int -> term list option) list)
-> Proof.context -> Proof.context
val put_validator_batch: (unit -> (int -> bool) list) -> Proof.context -> Proof.context
+ exception Counterexample of term list
val smart_quantifier : bool Config.T
val quickcheck_pretty : bool Config.T
val setup: theory -> theory
@@ -23,11 +24,19 @@
structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
struct
-(* dynamic options *)
+(* basics *)
+
+(** dynamic options **)
val (smart_quantifier, setup_smart_quantifier) =
Attrib.config_bool "quickcheck_smart_quantifier" (K true)
+val (fast, setup_fast) =
+ Attrib.config_bool "quickcheck_fast" (K false)
+
+val (full_support, setup_full_support) =
+ Attrib.config_bool "quickcheck_full_support" (K true)
+
val (quickcheck_pretty, setup_quickcheck_pretty) =
Attrib.config_bool "quickcheck_pretty" (K true)
@@ -51,9 +60,6 @@
end
| mk_sumcases _ f T = f T
-fun mk_undefined T = Const(@{const_name undefined}, T)
-
-
(** abstract syntax **)
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
@@ -61,7 +67,6 @@
val size = @{term "i :: code_numeral"}
val size_pred = @{term "(i :: code_numeral) - 1"}
val size_ge_zero = @{term "(i :: code_numeral) > 0"}
-fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
fun mk_none_continuation (x, y) =
let
@@ -70,26 +75,122 @@
Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
end
-(** datatypes **)
+fun mk_unit_let (x, y) =
+ Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ (absdummy (@{typ unit}, y))
+
+(* handling inductive datatypes *)
-(* constructing exhaustive generator instances on datatypes *)
+(** constructing generator instances **)
exception FUNCTION_TYPE;
+
+exception Counterexample of term list
+
val exhaustiveN = "exhaustive";
+val full_exhaustiveN = "full_exhaustive";
+val fast_exhaustiveN = "fast_exhaustive";
+val bounded_forallN = "bounded_forall";
-fun exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
+fun fast_exhaustiveT T = (T --> @{typ unit})
+ --> @{typ code_numeral} --> @{typ unit}
+
+fun exhaustiveT T = (T --> @{typ "Code_Evaluation.term list option"})
+ --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
+
+fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
+
+fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
--> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
--> @{typ "Code_Evaluation.term list option"}
-fun mk_equations descr vs tycos exhaustives (Ts, Us) =
+fun mk_equation_terms generics (descr, vs, Ts) =
+ let
+ val (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, exhaustives) = generics
+ val rhss =
+ Datatype_Aux.interpret_construction descr vs
+ { atyp = mk_call, dtyp = mk_aux_call }
+ |> (map o apfst) Type
+ |> map (fn (T, cs) => map (mk_consexpr T) cs)
+ |> map mk_rhs
+ val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts
+ in
+ map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
+ end
+
+fun gen_mk_call c T = (T, fn t => c T $ absdummy (T, t) $ size_pred)
+
+fun gen_mk_aux_call functerms fTs (k, _) (tyco, Ts) =
+ let
+ val T = Type (tyco, Ts)
+ val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
+ in
+ (T, fn t => nth functerms k $ absdummy (T, t) $ size_pred)
+ end
+
+fun gen_mk_consexpr test_function functerms simpleT (c, xs) =
+ let
+ val (Ts, fns) = split_list xs
+ val constr = Const (c, Ts ---> simpleT)
+ val bounds = map Bound (((length xs) - 1) downto 0)
+ val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
+ val start_term = test_function simpleT $ list_comb (constr, bounds)
+ in fold_rev (fn f => fn t => f t) fns start_term end
+
+fun mk_fast_equations functerms =
let
+ fun test_function T = Free ("f", T --> @{typ "unit"})
+ val mk_call = gen_mk_call (fn T =>
+ Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
+ fast_exhaustiveT T))
+ val mk_aux_call = gen_mk_aux_call functerms
+ val mk_consexpr = gen_mk_consexpr test_function functerms
+ fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"}
+ $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"}
+ in
+ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
+ end
+
+fun mk_equations functerms =
+ let
+ fun test_function T = Free ("f", T --> @{typ "term list option"})
+ val mk_call = gen_mk_call (fn T =>
+ Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
+ val mk_aux_call = gen_mk_aux_call functerms
+ val mk_consexpr = gen_mk_consexpr test_function functerms
+ fun mk_rhs exprs =
+ @{term "If :: bool => term list option => term list option => term list option"}
+ $ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
+ in
+ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
+ end
+
+fun mk_bounded_forall_equations functerms =
+ let
+ fun test_function T = Free ("P", T --> @{typ bool})
+ val mk_call = gen_mk_call (fn T =>
+ Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
+ bounded_forallT T))
+ val mk_aux_call = gen_mk_aux_call functerms
+ val mk_consexpr = gen_mk_consexpr test_function functerms
+ fun mk_rhs exprs =
+ @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
+ (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
+ in
+ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
+ end
+
+fun mk_full_equations functerms =
+ let
+ fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
fun mk_call T =
let
- val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
+ val full_exhaustive =
+ Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
+ full_exhaustiveT T)
in
- (T, (fn t => exhaustive $
+ (T, (fn t => full_exhaustive $
(HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
$ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
end
@@ -98,7 +199,7 @@
val T = Type (tyco, Ts)
val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
in
- (T, (fn t => nth exhaustives k $
+ (T, (fn t => nth functerms k $
(HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
$ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
end
@@ -119,19 +220,11 @@
fun mk_rhs exprs =
@{term "If :: bool => term list option => term list option => term list option"}
$ size_ge_zero $ (foldr1 mk_none_continuation exprs) $ @{term "None :: term list option"}
- val rhss =
- Datatype_Aux.interpret_construction descr vs
- { atyp = mk_call, dtyp = mk_aux_call }
- |> (map o apfst) Type
- |> map (fn (T, cs) => map (mk_consexpr T) cs)
- |> map mk_rhs
- val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives (Ts @ Us);
- val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
in
- eqs
+ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
end
-
-(* foundational definition with the function package *)
+
+(** foundational definition with the function package **)
val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
@@ -152,90 +245,87 @@
(HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
@{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
-(* creating the instances *)
-
-fun instantiate_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
- let
- val _ = Datatype_Aux.message config "Creating exhaustive generators...";
- val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames);
- in
- thy
- |> Class.instantiation (tycos, vs, @{sort exhaustive})
- |> Quickcheck_Common.define_functions
- (fn exhaustives => mk_equations descr vs tycos exhaustives (Ts, Us), SOME termination_tac)
- prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end handle FUNCTION_TYPE =>
+(** instantiating generator classes **)
+
+val contains_recursive_type_under_function_types =
+ exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
+ (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false))))
+
+fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
+ config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+ if not (contains_recursive_type_under_function_types descr) then
+ let
+ val _ = Datatype_Aux.message config ("Creating " ^ name ^ "...")
+ val fullnames = map (prefix (constprfx ^ "_")) (names @ auxnames)
+ in
+ thy
+ |> Class.instantiation (tycos, vs, sort)
+ |> Quickcheck_Common.define_functions
+ (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), NONE)
+ prfx argnames fullnames (map mk_T (Ts @ Us))
+ |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+ end
+ else
(Datatype_Aux.message config
- "Creation of exhaustive generators failed because the datatype contains a function type";
+ ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type");
thy)
-(* constructing bounded_forall instances on datatypes *)
+val instantiate_bounded_forall_datatype = instantiate_datatype
+ ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
+ mk_bounded_forall_equations, bounded_forallT, ["P", "i"]);
-val bounded_forallN = "bounded_forall";
+val instantiate_fast_exhaustive_datatype = instantiate_datatype
+ ("fast exhaustive generators", fast_exhaustiveN, @{sort fast_exhaustive},
+ mk_fast_equations, fast_exhaustiveT, ["f", "i"])
-fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool}
+val instantiate_exhaustive_datatype = instantiate_datatype
+ ("exhaustive generators", exhaustiveN, @{sort full_exhaustive}, mk_equations, exhaustiveT, ["f", "i"])
-fun mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us) =
+val instantiate_full_exhaustive_datatype = instantiate_datatype
+ ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
+ mk_full_equations, full_exhaustiveT, ["f", "i"])
+
+(* building and compiling generator expressions *)
+
+fun mk_fast_generator_expr ctxt (t, eval_terms) =
let
- fun mk_call T =
- let
- val bounded_forall =
- Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
- bounded_forallT T)
- in
- (T, (fn t => bounded_forall $ absdummy (T, t) $ size_pred))
- end
- fun mk_aux_call fTs (k, _) (tyco, Ts) =
- let
- val T = Type (tyco, Ts)
- val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
- in
- (T, (fn t => nth bounded_foralls k $ absdummy (T, t) $ size_pred))
- end
- fun mk_consexpr simpleT (c, xs) =
+ val thy = ProofContext.theory_of ctxt
+ val ctxt' = Variable.auto_fixes t ctxt
+ val names = Term.add_free_names t []
+ val frees = map Free (Term.add_frees t [])
+ val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+ val depth = Free (depth_name, @{typ code_numeral})
+ val return = @{term "throw_Counterexample :: term list => unit"} $
+ (HOLogic.mk_list @{typ "term"}
+ (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
+ fun mk_exhaustive_closure (free as Free (_, T)) t =
+ Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, fast_exhaustiveT T)
+ $ lambda free t $ depth
+ val none_t = @{term "()"}
+ fun mk_safe_if (cond, then_t, else_t) =
+ @{term "If :: bool => unit => unit => unit"} $ cond $ then_t $ else_t
+ fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
+ fun mk_naive_test_term t =
+ fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return))
+ fun mk_smart_test_term' concl bound_vars assms =
let
- val (Ts, fns) = split_list xs
- val constr = Const (c, Ts ---> simpleT)
- val bounds = map Bound (((length xs) - 1) downto 0)
- val start_term = Free ("P", simpleT --> @{typ bool}) $ list_comb (constr, bounds)
- in fold_rev (fn f => fn t => f t) fns start_term end
- fun mk_rhs exprs =
- @{term "If :: bool => bool => bool => bool"} $ size_ge_zero $
- (foldr1 HOLogic.mk_conj exprs) $ @{term "True"}
- val rhss =
- Datatype_Aux.interpret_construction descr vs
- { atyp = mk_call, dtyp = mk_aux_call }
- |> (map o apfst) Type
- |> map (fn (T, cs) => map (mk_consexpr T) cs)
- |> map mk_rhs
- val lhss =
- map2 (fn t => fn T => t $ Free ("P", T --> @{typ bool}) $ size) bounded_foralls (Ts @ Us)
- val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
- in
- eqs
- end
-
-(* creating the bounded_forall instances *)
-
-fun instantiate_bounded_forall_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
- let
- val _ = Datatype_Aux.message config "Creating bounded universal quantifiers...";
- val bounded_forallsN = map (prefix (bounded_forallN ^ "_")) (names @ auxnames);
- in
- thy
- |> Class.instantiation (tycos, vs, @{sort bounded_forall})
- |> Quickcheck_Common.define_functions
- (fn bounded_foralls =>
- mk_bounded_forall_equations descr vs tycos bounded_foralls (Ts, Us), NONE)
- prfx ["P", "i"] bounded_forallsN (map bounded_forallT (Ts @ Us))
- |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
- end handle FUNCTION_TYPE =>
- (Datatype_Aux.message config
- "Creation of bounded universal quantifiers failed because the datatype contains a function type";
- thy)
-
-(** building and compiling generator expressions **)
+ fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
+ val (vars, check) =
+ case assms of [] => (vars_of concl, (concl, none_t, return))
+ | assm :: assms => (vars_of assm, (assm,
+ mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
+ in
+ fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
+ end
+ fun mk_smart_test_term t =
+ let
+ val (assms, concl) = Quickcheck_Common.strip_imp t
+ in
+ mk_smart_test_term' concl [] assms
+ end
+ val mk_test_term =
+ if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
+ in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
fun mk_generator_expr ctxt (t, eval_terms) =
let
@@ -244,6 +334,48 @@
val names = Term.add_free_names t []
val frees = map Free (Term.add_frees t [])
val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+ val depth = Free (depth_name, @{typ code_numeral})
+ val return = @{term "Some :: term list => term list option"} $
+ (HOLogic.mk_list @{typ "term"}
+ (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
+ fun mk_exhaustive_closure (free as Free (_, T)) t =
+ Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
+ $ lambda free t $ depth
+ val none_t = @{term "None :: term list option"}
+ fun mk_safe_if (cond, then_t, else_t) =
+ @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
+ (@{term "If :: bool => term list option => term list option => term list option"}
+ $ cond $ then_t $ else_t) $ none_t;
+ fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
+ fun mk_naive_test_term t =
+ fold_rev mk_exhaustive_closure frees (mk_safe_if (t, none_t, return))
+ fun mk_smart_test_term' concl bound_vars assms =
+ let
+ fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
+ val (vars, check) =
+ case assms of [] => (vars_of concl, (concl, none_t, return))
+ | assm :: assms => (vars_of assm, (assm,
+ mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
+ in
+ fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
+ end
+ fun mk_smart_test_term t =
+ let
+ val (assms, concl) = Quickcheck_Common.strip_imp t
+ in
+ mk_smart_test_term' concl [] assms
+ end
+ val mk_test_term =
+ if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
+ in lambda depth (mk_test_term t) end
+
+fun mk_full_generator_expr ctxt (t, eval_terms) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ctxt' = Variable.auto_fixes t ctxt
+ val names = Term.add_free_names t []
+ val frees = map Free (Term.add_frees t [])
+ val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
val depth = Free (depth_name, @{typ code_numeral})
val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
@@ -257,7 +389,7 @@
$ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
$ lambda free (lambda term_var t))
else
- Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
+ Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
$ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
$ lambda free (lambda term_var t)) $ depth
val none_t = @{term "None :: term list option"}
@@ -288,7 +420,7 @@
if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
in lambda depth (mk_test_term t) end
-val mk_parametric_generator_expr =
+fun mk_parametric_generator_expr mk_generator_expr =
Quickcheck_Common.gen_mk_parametric_generator_expr
((mk_generator_expr, absdummy (@{typ "code_numeral"}, @{term "None :: term list option"})),
@{typ "code_numeral => term list option"})
@@ -359,7 +491,10 @@
fun compile_generator_expr ctxt ts =
let
val thy = ProofContext.theory_of ctxt
- val t' = mk_parametric_generator_expr ctxt ts;
+ val mk_generator_expr =
+ if Config.get ctxt fast then mk_fast_generator_expr
+ else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
+ val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
thy (SOME target) (fn proc => fn g =>
@@ -394,14 +529,20 @@
thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
end;
-(** setup **)
+(* setup *)
val setup =
Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
+(* #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
(((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
#> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
- (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
+ (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
+ #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+ (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))*)
#> setup_smart_quantifier
+ #> setup_full_support
+ #> setup_fast
#> setup_quickcheck_pretty
#> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Sat Apr 09 13:10:20 2011 +0200
@@ -284,7 +284,11 @@
val {facts, goal, ...} = Proof.goal st
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
- val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
+ val cprop =
+ (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) of
+ SOME ct => ct
+ | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure (
+ "goal is not a HOL term")))
in
map snd xwthms
|> map_index I
--- a/src/HOL/Tools/SMT/smt_translate.ML Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Sat Apr 09 13:10:20 2011 +0200
@@ -168,28 +168,28 @@
(** eta-expand quantifiers, let expressions and built-ins *)
local
- fun eta T t = Abs (Name.uu, T, Term.incr_boundvars 1 t $ Bound 0)
+ fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0))
- fun exp T = eta (Term.domain_type (Term.domain_type T))
+ fun exp f T = eta f (Term.domain_type (Term.domain_type T))
fun exp2 T q =
let val U = Term.domain_type T
- in Abs (Name.uu, U, q $ eta (Term.domain_type U) (Bound 0)) end
+ in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end
fun exp2' T l =
let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
- in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
+ in Abs (Name.uu, U1, eta I U2 (l $ Bound 0)) end
fun expf k i T t =
let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
in
Term.incr_boundvars (length Ts) t
- |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
+ |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1)
|> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
end
in
-fun eta_expand ctxt funcs =
+fun eta_expand ctxt is_fol funcs =
let
fun exp_func t T ts =
(case Termtab.lookup funcs t of
@@ -199,18 +199,30 @@
| NONE => Term.list_comb (t, ts))
fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
- | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
+ | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp expand T t
| expand (q as Const (@{const_name All}, T)) = exp2 T q
| expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
- | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t
+ | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t
| expand (q as Const (@{const_name Ex}, T)) = exp2 T q
| expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
- l $ expand t $ abs_expand a
+ if is_fol then expand (Term.betapply (Abs a, t))
+ else l $ expand t $ abs_expand a
| expand ((l as Const (@{const_name Let}, T)) $ t $ u) =
- l $ expand t $ exp (Term.range_type T) u
+ if is_fol then expand (u $ t)
+ else l $ expand t $ exp expand (Term.range_type T) u
| expand ((l as Const (@{const_name Let}, T)) $ t) =
- exp2 T (l $ expand t)
- | expand (l as Const (@{const_name Let}, T)) = exp2' T l
+ if is_fol then
+ let val U = Term.domain_type (Term.range_type T)
+ in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
+ else exp2 T (l $ expand t)
+ | expand (l as Const (@{const_name Let}, T)) =
+ if is_fol then
+ let val U = Term.domain_type (Term.range_type T)
+ in
+ Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U,
+ Bound 0 $ Bound 1))
+ end
+ else exp2' T l
| expand t =
(case Term.strip_comb t of
(u as Const (c as (_, T)), ts) =>
@@ -363,12 +375,6 @@
@{lemma "P = True == P" by (rule eq_reflection) simp},
@{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
- fun reduce_let (Const (@{const_name Let}, _) $ t $ u) =
- reduce_let (Term.betapply (u, t))
- | reduce_let (t $ u) = reduce_let t $ reduce_let u
- | reduce_let (Abs (n, T, t)) = Abs (n, T, reduce_let t)
- | reduce_let t = t
-
fun as_term t = @{const HOL.eq (bool)} $ t $ @{const SMT.term_true}
fun wrap_in_if t =
@@ -432,7 +438,7 @@
| NONE => as_term (in_term t)))
| _ => as_term (in_term t))
in
- map (reduce_let #> in_form) #>
+ map in_form #>
cons (SMT_Utils.prop_of term_bool) #>
pair (fol_rules, [term_bool], builtin)
end
@@ -566,7 +572,7 @@
val (ctxt2, ts3) =
ts2
- |> eta_expand ctxt1 funcs
+ |> eta_expand ctxt1 is_fol funcs
|> lift_lambdas ctxt1
||> intro_explicit_application
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat Apr 09 13:10:20 2011 +0200
@@ -564,19 +564,19 @@
(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
local
- val elim_all = @{lemma "(ALL x. P) == P" by simp}
- val elim_ex = @{lemma "(EX x. P) == P" by simp}
-
- fun elim_unused_conv ctxt =
- Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
- (Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
+ val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
+ val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
- fun elim_unused_tac ctxt =
- REPEAT_ALL_NEW (
- Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
- ORELSE' CONVERSION (elim_unused_conv ctxt))
+ fun elim_unused_tac i st = (
+ Tactic.match_tac [@{thm refl}]
+ ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+ ORELSE' (
+ Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}]
+ THEN' elim_unused_tac)) i st
in
-fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac (elim_unused_tac ctxt)
+
+val elim_unused_vars = Thm o Z3_Proof_Tools.by_tac elim_unused_tac
+
end
@@ -781,7 +781,7 @@
| (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
| (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
| (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
- | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
+ | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars ct, cxp)
| (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
| (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
| (Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Fri Apr 08 23:33:57 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Sat Apr 09 13:10:20 2011 +0200
@@ -63,15 +63,23 @@
try Thm.first_order_match (Thm.cprop_of thm, ct)
|> Option.map (fn inst => Thm.instantiate inst thm)
-fun net_instance' f net ct =
- let
- val xthms = Net.match_term net (Thm.term_of ct)
- fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms
- fun first_of' f ct =
- let val thm = Thm.trivial ct
- in get_first (f (try (fn rule => rule COMP thm))) xthms end
- in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
-val net_instance = net_instance' I
+local
+ fun instances_from_net match f net ct =
+ let
+ val lookup = if match then Net.match_term else Net.unify_term
+ val xthms = lookup net (Thm.term_of ct)
+ fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms
+ fun first_of' f ct =
+ let val thm = Thm.trivial ct
+ in get_first (f (try (fn rule => rule COMP thm))) xthms end
+ in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
+in
+
+fun net_instance' f = instances_from_net false f
+
+val net_instance = instances_from_net true I
+
+end