--- a/src/HOL/Fun.thy Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/Fun.thy Wed Oct 21 15:54:31 2009 +0200
@@ -78,6 +78,9 @@
lemma image_compose: "(f o g) ` r = f`(g`r)"
by (simp add: comp_def, blast)
+lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
+ by auto
+
lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
by (unfold comp_def, blast)
--- a/src/HOL/SMT/Tools/smt_monomorph.ML Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_monomorph.ML Wed Oct 21 15:54:31 2009 +0200
@@ -32,7 +32,7 @@
fun consts_of ts = AList.group (op =) (fold Term.add_consts ts [])
|> filter_out (ignored o fst)
-val join_consts = curry (AList.join (op =) (K (merge (op =))))
+fun join_consts cs ds = AList.join (op =) (K (merge (op =))) (cs, ds)
fun diff_consts cs ds =
let fun diff (n, Ts) =
(case AList.lookup (op =) cs n of
@@ -55,7 +55,7 @@
fun proper_match ps env =
forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps
-val eq_tab = eq_set (op =) o pairself Vartab.dest
+fun eq_tab (tab1, tab2) = eq_set (op =) (Vartab.dest tab1, Vartab.dest tab2)
fun specialize thy cs is ((r, ps), ces) (ts, ns) =
let
--- a/src/HOL/SMT/Tools/z3_model.ML Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_model.ML Wed Oct 21 15:54:31 2009 +0200
@@ -82,12 +82,12 @@
fun spaced p = p --| space
val key = spaced (lift name) #-> lift' ident
-val mapping = spaced (this "->")
+fun mapping st = spaced (this "->") st
fun in_braces p = spaced ($$ "{") |-- p --| spaced ($$ "}")
-val bool_expr =
- this "true" >> K @{term True} ||
- this "false" >> K @{term False}
+fun bool_expr st =
+ (this "true" >> K @{term True} ||
+ this "false" >> K @{term False}) st
fun number_expr T =
let
@@ -95,7 +95,7 @@
fun frac n d = Const (@{const_name divide}, T --> T --> T) $ n $ d
in num :|-- (fn n => Scan.optional ($$ "/" |-- num >> frac n) n) end
-val value = this "val!" |-- lift nat_num
+fun value st = (this "val!" |-- lift nat_num) st
fun value_expr T = value #-> lift' (get_value T)
val domT = Term.domain_type
--- a/src/HOL/SMT/Tools/z3_proof.ML Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof.ML Wed Oct 21 15:54:31 2009 +0200
@@ -192,9 +192,11 @@
val variables =
par (this "vars" |-- bsep1 (par ((lift name >> K "x") --| blank -- sort)))
-val patterns = bsep (par ((this ":pat" || this ":nopat") |-- bsep1 (lift id)))
-val quant_kind =
- this "forall" >> K T.mk_forall || this "exists" >> K T.mk_exists
+fun patterns st =
+ bsep (par ((this ":pat" || this ":nopat") |-- bsep1 (lift id))) st
+fun quant_kind st =
+ (this "forall" >> K T.mk_forall ||
+ this "exists" >> K T.mk_exists) st
fun quantifier thy = par (quant_kind --| blank --
variables --| patterns --| blank -- arg thy) >>
(fn ((q, vs), body) => fold_rev (q thy) vs body)
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML Wed Oct 21 15:54:31 2009 +0200
@@ -386,52 +386,55 @@
datatype conj_disj = CONJ | DISJ | NCON | NDIS
fun kind_of t =
- if is_conj t then CONJ
- else if is_disj t then DISJ
- else if is_neg' is_conj t then NCON
- else if is_neg' is_disj t then NDIS
- else CONJ (*allows to prove equalities with single literals on each side*)
+ if is_conj t then SOME CONJ
+ else if is_disj t then SOME DISJ
+ else if is_neg' is_conj t then SOME NCON
+ else if is_neg' is_disj t then SOME NDIS
+ else NONE
in
fun prove_conj_disj_eq ct =
let val cp = Thm.dest_binop ct
in
(case pairself (kind_of o Thm.term_of) cp of
- (CONJ, CONJ) => prove_eq true true cp
- | (CONJ, NDIS) => prove_eq true false cp
- | (DISJ, DISJ) => contrapos1 (prove_eq false false) cp
- | (DISJ, NCON) => contrapos2 (prove_eq false true) cp
- | (NCON, NCON) => contrapos1 (prove_eq true true) cp
- | (NCON, DISJ) => contrapos3 (prove_eq true false) cp
- | (NDIS, NDIS) => prove_eq false false cp
- | (NDIS, CONJ) => prove_eq false true cp)
+ (SOME CONJ, SOME CONJ) => prove_eq true true cp
+ | (SOME CONJ, SOME NDIS) => prove_eq true false cp
+ | (SOME CONJ, NONE) => prove_eq true true cp
+ | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
+ | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
+ | (SOME DISJ, NONE) => contrapos1 (prove_eq false false) cp
+ | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
+ | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
+ | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
+ | (SOME NDIS, SOME NDIS) => prove_eq false false cp
+ | (SOME NDIS, SOME CONJ) => prove_eq false true cp
+ | (SOME NDIS, NONE) => prove_eq false true cp
+ | _ => raise CTERM ("prove_conj_disj_eq", [ct]))
end
end
(** unfolding of distinct **)
local
- val distinct1 = @{lemma "distinct [] == ~False" by simp}
- val distinct2 = @{lemma "distinct [x] == ~False" by simp}
- val distinct3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
+ val set1 = @{lemma "x ~: set [] == ~False" by simp}
+ val set2 = @{lemma "x ~: set [x] == False" by simp}
+ val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
+ val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
+ val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
+
+ fun set_conv ct =
+ (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
+ (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
+
+ val dist1 = @{lemma "distinct [] == ~False" by simp}
+ val dist2 = @{lemma "distinct [x] == ~False" by simp}
+ val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
by simp}
- val set1 = @{lemma "x ~: set [] == ~False" by simp}
- val set2 = @{lemma "x ~: set [y] == x ~= y" by simp}
- val set3 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
-
fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
-
- fun unfold_conv rule1 rule2 rule3 sub_conv =
- let
- fun uconv ct =
- (Conv.rewr_conv rule1 else_conv
- Conv.rewr_conv rule2 else_conv
- (Conv.rewr_conv rule3 then_conv binop_conv sub_conv uconv)) ct
- in uconv end
-
- val set_conv = unfold_conv set1 set2 set3 Conv.all_conv
in
-val unfold_distinct_conv = unfold_conv distinct1 distinct2 distinct3 set_conv
+fun unfold_distinct_conv ct =
+ (More_Conv.rewrs_conv [dist1, dist2] else_conv
+ (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
end
--- a/src/HOL/SMT/Tools/z3_proof_terms.ML Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_terms.ML Wed Oct 21 15:54:31 2009 +0200
@@ -143,8 +143,8 @@
fun dec (i, v) = if i = 0 then NONE else SOME (i - 1, v)
in mk_preterm (Thm.capply cq (Thm.cabs cv ct), map_filter dec vs) end
in
-val mk_forall = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat All})
-val mk_exists = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat Ex})
+fun mk_forall thy = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat All}) thy
+fun mk_exists thy = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat Ex}) thy
end
--- a/src/HOL/Set.thy Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/Set.thy Wed Oct 21 15:54:31 2009 +0200
@@ -458,7 +458,7 @@
unfolding mem_def by (erule le_funE, erule le_boolE)
-- {* Rule in Modus Ponens style. *}
-lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
+lemma rev_subsetD [noatp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
-- {* The same, with reversed premises for use with @{text erule} --
cf @{text rev_mp}. *}
by (rule subsetD)
@@ -467,13 +467,13 @@
\medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
*}
-lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
+lemma subsetCE [noatp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
-- {* Classical elimination rule. *}
unfolding mem_def by (blast dest: le_funE le_boolE)
-lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+lemma subset_eq [noatp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
-lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
+lemma contra_subsetD [noatp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
by blast
lemma subset_refl [simp]: "A \<subseteq> A"
@@ -488,8 +488,11 @@
lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
by (rule subsetD)
+lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"
+ by simp
+
lemmas basic_trans_rules [trans] =
- order_trans_rules set_rev_mp set_mp
+ order_trans_rules set_rev_mp set_mp eq_mem_trans
subsubsection {* Equality *}
--- a/src/HOL/SetInterval.thy Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/SetInterval.thy Wed Oct 21 15:54:31 2009 +0200
@@ -395,6 +395,11 @@
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
by (auto simp add: atLeastAtMost_def)
+lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
+ apply (induct k)
+ apply (simp_all add: atLeastLessThanSuc)
+ done
+
subsubsection {* Image *}
lemma image_add_atLeastAtMost:
@@ -522,20 +527,20 @@
lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
by (subst UN_UN_finite_eq [symmetric]) blast
-lemma UN_finite2_subset:
- assumes sb: "!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)"
- shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
-proof (rule UN_finite_subset)
- fix n
- have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)" by (rule sb)
- also have "... \<subseteq> (\<Union>n::nat. \<Union>i\<in>{0..<n}. B i)" by blast
- also have "... = (\<Union>n. B n)" by (simp add: UN_UN_finite_eq)
- finally show "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>n. B n)" .
-qed
+lemma UN_finite2_subset:
+ "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
+ apply (rule UN_finite_subset)
+ apply (subst UN_UN_finite_eq [symmetric, of B])
+ apply blast
+ done
lemma UN_finite2_eq:
- "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
- by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE)
+ "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
+ apply (rule subset_antisym)
+ apply (rule UN_finite2_subset, blast)
+ apply (rule UN_finite2_subset [where k=k])
+ apply (force simp add: atLeastLessThan_add_Un [of 0] UN_Un)
+ done
subsubsection {* Cardinality *}
--- a/src/HOL/Tools/res_atp.ML Wed Oct 21 15:54:01 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Oct 21 15:54:31 2009 +0200
@@ -290,15 +290,6 @@
(* Retrieving and filtering lemmas *)
(***************************************************************)
-(*** white list and black list of lemmas ***)
-
-(*The rule subsetI is frequently omitted by the relevance filter.*)
-val whitelist_fo = [subsetI];
-(* ext has been a 'helper clause', always given to the atps.
- As such it was not passed to metis, but metis does not include ext (in contrast
- to the other helper_clauses *)
-val whitelist_ho = [ResHolClause.ext];
-
(*** retrieve lemmas and filter them ***)
(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
@@ -519,11 +510,8 @@
val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy isFO
|> remove_unwanted_clauses
- val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
- (* add whitelist *)
- val white_cls = ths_to_cls thy (whitelist_fo @ (if isFO then [] else whitelist_ho))
in
- white_cls @ axcls
+ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
end;
(* prepare for passing to writer,