--- a/Admin/CHECKLIST Thu Jun 24 18:45:31 2010 +0200
+++ b/Admin/CHECKLIST Thu Jun 24 21:03:32 2010 +0200
@@ -29,3 +29,17 @@
build
lib/html/library_index_content.template
+
+Packaging
+=========
+
+- makedist -r DISTNAME
+
+- makebin (multiplatform);
+
+- makebin -l on fast machine;
+
+- makebundle (multiplatform);
+
+- hdiutil create -srcfolder DIR DMG (Mac OS);
+
--- a/src/HOL/IsaMakefile Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/IsaMakefile Thu Jun 24 21:03:32 2010 +0200
@@ -1093,6 +1093,7 @@
$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \
Multivariate_Analysis/Brouwer_Fixpoint.thy \
+ Multivariate_Analysis/Cartesian_Euclidean_Space.thy \
Multivariate_Analysis/Convex_Euclidean_Space.thy \
Multivariate_Analysis/Derivative.thy \
Multivariate_Analysis/Determinants.thy \
--- a/src/HOL/Sledgehammer.thy Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Jun 24 21:03:32 2010 +0200
@@ -53,16 +53,6 @@
lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
by (simp add: fequal_def)
-text{*These two represent the equivalence between Boolean equality and iff.
-They can't be converted to clauses automatically, as the iff would be
-expanded...*}
-
-lemma iff_positive: "P \<or> Q \<or> P = Q"
-by blast
-
-lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
-by blast
-
text{*Theorems for translation to combinators*}
lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
--- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 24 21:03:32 2010 +0200
@@ -7,13 +7,13 @@
signature QUOTIENT_DEF =
sig
val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
- local_theory -> (term * thm) * local_theory
+ local_theory -> Quotient_Info.qconsts_info * local_theory
val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
- local_theory -> (term * thm) * local_theory
+ local_theory -> Quotient_Info.qconsts_info * local_theory
- val quotient_lift_const: typ list -> string * term -> local_theory ->
- (term * thm) * local_theory
+ val lift_raw_const: typ list -> string * term -> local_theory ->
+ Quotient_Info.qconsts_info * local_theory
end;
structure Quotient_Def: QUOTIENT_DEF =
@@ -32,12 +32,10 @@
- the new constant as term
- the rhs of the definition as term
- It returns the defined constant and its definition
- theorem; stores the data in the qconsts data slot.
+ It stores the qconst_info in the qconsts data slot.
- Restriction: At the moment the right-hand side of the
- definition must be a constant. Similarly the left-hand
- side must be a constant.
+ Restriction: At the moment the left- and right-hand
+ side of the definition must be a constant.
*)
fun error_msg bind str =
let
@@ -45,7 +43,7 @@
val pos = Position.str_of (Binding.pos_of bind)
in
error ("Head of quotient_definition " ^
- (quote str) ^ " differs from declaration " ^ name ^ pos)
+ quote str ^ " differs from declaration " ^ name ^ pos)
end
fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
@@ -69,12 +67,14 @@
val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
(* data storage *)
- fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
+ val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+
+ fun qcinfo phi = transform_qconsts phi qconst_data
fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
val lthy'' = Local_Theory.declaration true
(fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
in
- ((trm, thm), lthy'')
+ (qconst_data, lthy'')
end
fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
@@ -87,10 +87,17 @@
quotient_def (decl, (attr, (lhs, rhs))) lthy''
end
-fun quotient_lift_const qtys (b, t) ctxt =
+(* a wrapper for automatically lifting a raw constant *)
+fun lift_raw_const qtys (qconst_name, rconst) ctxt =
+let
+ val rty = fastype_of rconst
+ val qty = derive_qtyp qtys rty ctxt
+in
quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
- (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
+ (Free (qconst_name, qty), rconst))) ctxt
+end
+(* parser and command *)
val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
val quotdef_parser =
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 21:03:32 2010 +0200
@@ -26,7 +26,7 @@
val inj_repabs_trm: Proof.context -> term * term -> term
val inj_repabs_trm_chk: Proof.context -> term * term -> term
- val quotient_lift_const: typ list -> string * term -> local_theory -> term
+ val derive_qtyp: typ list -> typ -> Proof.context -> typ
val quotient_lift_all: typ list -> Proof.context -> term -> term
end;
@@ -84,7 +84,7 @@
*)
fun mk_mapfun ctxt vs rty =
let
- val vs' = map (mk_Free) vs
+ val vs' = map mk_Free vs
fun mk_mapfun_aux rty =
case rty of
@@ -103,7 +103,7 @@
let
val thy = ProofContext.theory_of ctxt
val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
- val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+ val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn
in
(#rtyp qdata, #qtyp qdata)
end
@@ -738,14 +738,12 @@
(ty_substs, filter valid_trm_subst all_trm_substs)
end
-fun quotient_lift_const qtys (b, t) ctxt =
+fun derive_qtyp qtys rty ctxt =
let
val thy = ProofContext.theory_of ctxt
- val (ty_substs, _) = get_ty_trm_substs qtys ctxt;
- val (_, ty) = dest_Const t;
- val nty = subst_tys thy ty_substs ty;
+ val (ty_substs, _) = get_ty_trm_substs qtys ctxt
in
- Free(b, nty)
+ subst_tys thy ty_substs rty
end
(*
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jun 24 21:03:32 2010 +0200
@@ -8,7 +8,7 @@
signature QUOTIENT_TYPE =
sig
val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
- -> Proof.context -> (thm * thm) * local_theory
+ -> Proof.context -> Quotient_Info.quotdata_info * local_theory
val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
-> Proof.context -> Proof.state
@@ -32,11 +32,8 @@
end
fun note (name, thm, attrs) lthy =
-let
- val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
-in
- (thm', lthy')
-end
+ Local_Theory.note ((name, attrs), [thm]) lthy |> snd
+
fun intern_attr at = Attrib.internal (K at)
@@ -64,7 +61,7 @@
|> map Free
in
lambda c (HOLogic.exists_const rty $
- lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x))))))
+ lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
end
@@ -139,7 +136,10 @@
(* main function for constructing a quotient type *)
fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
let
- val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp}
+ val part_equiv =
+ if partial
+ then equiv_thm
+ else equiv_thm RS @{thm equivp_implies_part_equivp}
(* generates the typedef *)
val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
@@ -173,15 +173,17 @@
(* name equivalence theorem *)
val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
- (* storing the quot-info *)
- fun qinfo phi = transform_quotdata phi
- {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
- val lthy4 = Local_Theory.declaration true
- (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3
+ (* storing the quotdata *)
+ val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
+
+ fun qinfo phi = transform_quotdata phi quotdata
+
+ val lthy4 = lthy3
+ |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
+ |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
+ |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
in
- lthy4
- |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
- ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
+ (quotdata, lthy4)
end
@@ -253,6 +255,7 @@
- its free type variables (first argument)
- its mixfix annotation
- the type to be quotient
+ - the partial flag (a boolean)
- the relation according to which the type is quotient
it opens a proof-state in which one has to show that the
@@ -268,7 +271,8 @@
fun mk_goal (rty, rel, partial) =
let
val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
- val const = if partial then @{const_name part_equivp} else @{const_name equivp}
+ val const =
+ if partial then @{const_name part_equivp} else @{const_name equivp}
in
HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
end
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jun 24 21:03:32 2010 +0200
@@ -679,8 +679,7 @@
(*The modes FO and FT are sticky. HO can be downgraded to FO.*)
fun set_mode FO = FO
| set_mode HO =
- if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
- else HO
+ if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jun 24 21:03:32 2010 +0200
@@ -21,7 +21,7 @@
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val is_quasi_fol_term : theory -> term -> bool
+ val is_quasi_fol_theorem : theory -> thm -> bool
val relevant_facts :
bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
@@ -88,42 +88,70 @@
Symtab.map_default (c, [ctyps])
(fn [] => [] | ctypss => insert (op =) ctyps ctypss)
-val fresh_Ex_prefix = "Sledgehammer.Ex."
+val fresh_sko_prefix = "Sledgehammer.Skox."
+
+val flip = Option.map not
-fun get_goal_consts_typs thy goals =
+(* Including equality in this list might be expected to stop rules like
+ subset_antisym from being chosen, but for some reason filtering works better
+ with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
+ because any remaining occurrences must be within comprehensions. *)
+val boring_cnf_consts =
+ [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
+ @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
+ @{const_name "op ="}]
+
+fun get_consts_typs thy pos ts =
let
- val use_natural_form = !use_natural_form
(* Free variables are included, as well as constants, to handle locales.
"skolem_id" is included to increase the complexity of theorems containing
Skolem functions. In non-CNF form, "Ex" is included but each occurrence
is considered fresh, to simulate the effect of Skolemization. *)
- fun aux (Const (x as (s, _))) =
- (if s = @{const_name Ex} andalso use_natural_form then
- (gensym fresh_Ex_prefix, [])
- else
- (const_with_typ thy x))
- |> add_const_type_to_table
- | aux (Free x) = add_const_type_to_table (const_with_typ thy x)
- | aux ((t as Const (@{const_name skolem_id}, _)) $ _) = aux t
- | aux (t $ u) = aux t #> aux u
- | aux (Abs (_, _, t)) = aux t
- | aux _ = I
- (* Including equality in this list might be expected to stop rules like
- subset_antisym from being chosen, but for some reason filtering works better
- with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
- because any remaining occurrences must be within comprehensions. *)
- val standard_consts =
- [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
- @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
- @{const_name "op ="}] @
- (if use_natural_form then
- [@{const_name All}, @{const_name Ex}, @{const_name "op &"},
- @{const_name "op -->"}]
- else
- [])
+ fun do_term t =
+ case t of
+ Const x => add_const_type_to_table (const_with_typ thy x)
+ | Free x => add_const_type_to_table (const_with_typ thy x)
+ | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
+ | t1 $ t2 => do_term t1 #> do_term t2
+ | Abs (_, _, t) => do_term t
+ | _ => I
+ fun do_quantifier sweet_pos pos body_t =
+ do_formula pos body_t
+ #> (if pos = SOME sweet_pos then I
+ else add_const_type_to_table (gensym fresh_sko_prefix, []))
+ and do_equality T t1 t2 =
+ fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
+ else do_term) [t1, t2]
+ and do_formula pos t =
+ case t of
+ Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
+ do_quantifier false pos body_t
+ | @{const "==>"} $ t1 $ t2 =>
+ do_formula (flip pos) t1 #> do_formula pos t2
+ | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
+ do_equality T t1 t2
+ | @{const Trueprop} $ t1 => do_formula pos t1
+ | @{const Not} $ t1 => do_formula (flip pos) t1
+ | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
+ do_quantifier false pos body_t
+ | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
+ do_quantifier true pos body_t
+ | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
+ | @{const "op -->"} $ t1 $ t2 =>
+ do_formula (flip pos) t1 #> do_formula pos t2
+ | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
+ do_equality T t1 t2
+ | (t0 as Const (_, @{typ bool})) $ t1 =>
+ do_term t0 #> do_formula pos t1 (* theory constant *)
+ | _ => do_term t
in
- Symtab.empty |> fold (Symtab.update o rpair []) standard_consts
- |> fold aux goals
+ Symtab.empty
+ |> (if !use_natural_form then
+ fold (do_formula pos) ts
+ else
+ fold (Symtab.update o rpair []) boring_cnf_consts
+ #> fold do_term ts)
end
(*Inserts a dummy "constant" referring to the theory name, so that relevance
@@ -217,7 +245,7 @@
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
fun consts_typs_of_term thy t =
- Symtab.fold add_expand_pairs (get_goal_consts_typs thy [t]) []
+ Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) []
fun pair_consts_typs_axiom theory_relevant thy axiom =
(axiom, axiom |> appropriate_prop_of theory_relevant
@@ -306,9 +334,11 @@
if weight >= threshold orelse
(defs_relevant andalso
defines thy (#1 clsthm) rel_const_tab) then
- (trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
- " passes: " ^ Real.toString weight);
- relevant ((ax, weight) :: newrels, rejects) axs)
+ (trace_msg (fn () =>
+ name ^ " clause " ^ Int.toString n ^
+ " passes: " ^ Real.toString weight
+ (* ^ " consts: " ^ commas (map fst consts_typs) *));
+ relevant ((ax, weight) :: newrels, rejects) axs)
else
relevant (newrels, ax :: rejects) axs
end
@@ -322,11 +352,15 @@
fun relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
thy (axioms : cnf_thm list) goals =
- if relevance_threshold > 0.0 then
+ if relevance_threshold > 1.0 then
+ []
+ else if relevance_threshold < 0.0 then
+ axioms
+ else
let
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
- val goal_const_tab = get_goal_consts_typs thy goals
+ val goal_const_tab = get_consts_typs thy (SOME true) goals
val _ =
trace_msg (fn () => "Initial constants: " ^
commas (Symtab.keys goal_const_tab))
@@ -340,8 +374,6 @@
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
relevant
end
- else
- axioms;
(***************************************************************)
(* Retrieving and filtering lemmas *)
@@ -374,6 +406,9 @@
fun subtract_cls ax_clauses =
filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
+val exists_sledgehammer_const =
+ exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
+
fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
@@ -396,7 +431,8 @@
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
- val ths = filter_out is_theorem_bad_for_atps ths0;
+ val ths = filter_out (is_theorem_bad_for_atps orf
+ exists_sledgehammer_const) ths0
in
case find_first check_thms [name1, name2, name] of
NONE => I
@@ -483,13 +519,8 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun is_quasi_fol_term thy =
- Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 []
-
-(*Ensures that no higher-order theorems "leak out"*)
-fun restrict_to_logic thy true cls =
- filter (is_quasi_fol_term thy o prop_of o fst) cls
- | restrict_to_logic _ false cls = cls
+fun is_quasi_fol_theorem thy =
+ Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
(**** Predicates to detect unwanted clauses (prolific or likely to cause
unsoundness) ****)
@@ -539,43 +570,35 @@
(has_typed_var dangerous_types t orelse
forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
-fun remove_dangerous_clauses full_types add_thms =
- filter_out (fn (cnf_th, (_, orig_th)) =>
- not (member Thm.eq_thm add_thms orig_th) andalso
- is_dangerous_term full_types (prop_of cnf_th))
-
fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
fun relevant_facts full_types respect_no_atp relevance_threshold
relevance_convergence defs_relevant max_new theory_relevant
(relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) goal_cls =
- if (only andalso null add) orelse relevance_threshold > 1.0 then
- []
- else
- let
- val thy = ProofContext.theory_of ctxt
- val has_override = not (null add) orelse not (null del)
- val is_FO = is_fol_goal thy goal_cls
- val axioms =
- checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
- (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
- else all_name_thms_pairs respect_no_atp ctxt chained_ths)
- |> cnf_rules_pairs thy
- |> not has_override ? make_unique
- |> not only ? restrict_to_logic thy is_FO
- |> (if only then
- I
- else
- remove_dangerous_clauses full_types
- (maps (ProofContext.get_fact ctxt) add))
- in
- relevance_filter ctxt relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant relevance_override
- thy axioms (map prop_of goal_cls)
- |> has_override ? make_unique
- |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
- end
+ let
+ val thy = ProofContext.theory_of ctxt
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val has_override = not (null add) orelse not (null del)
+ val is_FO = is_fol_goal thy goal_cls
+ val axioms =
+ checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
+ (map (name_thms_pair_from_ref ctxt chained_ths) add @
+ (if only then []
+ else all_name_thms_pairs respect_no_atp ctxt chained_ths))
+ |> cnf_rules_pairs thy
+ |> not has_override ? make_unique
+ |> filter (fn (cnf_thm, (_, orig_thm)) =>
+ member Thm.eq_thm add_thms orig_thm orelse
+ ((not is_FO orelse is_quasi_fol_theorem thy cnf_thm) andalso
+ not (is_dangerous_term full_types (prop_of cnf_thm))))
+ in
+ relevance_filter ctxt relevance_threshold relevance_convergence
+ defs_relevant max_new theory_relevant relevance_override
+ thy axioms (map prop_of goal_cls)
+ |> has_override ? make_unique
+ |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
+ end
(** Helper clauses **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu Jun 24 21:03:32 2010 +0200
@@ -8,6 +8,8 @@
signature SLEDGEHAMMER_FACT_PREPROCESSOR =
sig
type cnf_thm = thm * ((string * int) * thm)
+
+ val sledgehammer_prefix: string
val chained_prefix: string
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
@@ -35,13 +37,15 @@
type cnf_thm = thm * ((string * int) * thm)
+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+
(* Used to label theorems chained into the goal. *)
-val chained_prefix = "Sledgehammer.chained_"
+val chained_prefix = sledgehammer_prefix ^ "chained_"
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
-val skolem_theory_name = "Sledgehammer.Sko"
+val skolem_theory_name = sledgehammer_prefix ^ "Sko"
val skolem_prefix = "sko_"
val skolem_infix = "$"
@@ -183,25 +187,14 @@
fun vars_of_thm th =
map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
-(*Make a version of fun_cong with a given variable name*)
-local
- val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
- val cx = hd (vars_of_thm fun_cong');
- val ty = typ_of (ctyp_of_term cx);
- val thy = theory_of_thm fun_cong;
- fun mkvar a = cterm_of thy (Var((a,0),ty));
-in
-fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
-end;
+val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
-(*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n,
- serves as an upper bound on how many to remove.*)
-fun strip_lambdas 0 th = th
- | strip_lambdas n th =
- case prop_of th of
- _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
- strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
- | _ => th;
+(* Removes the lambdas from an equation of the form t = (%x. u). *)
+fun extensionalize th =
+ case prop_of th of
+ _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
+ $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+ | _ => th
fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
| is_quasi_lambda_free (t1 $ t2) =
@@ -339,9 +332,9 @@
fun to_nnf th ctxt0 =
let val th1 = th |> transform_elim |> zero_var_indexes
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
- val th3 = th2
- |> Conv.fconv_rule Object_Logic.atomize
- |> Meson.make_nnf ctxt |> strip_lambdas ~1
+ val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+ |> extensionalize
+ |> Meson.make_nnf ctxt
in (th3, ctxt) end;
(*Generate Skolem functions for a theorem supplied in nnf*)
--- a/src/HOL/Tools/inductive_codegen.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jun 24 21:03:32 2010 +0200
@@ -334,10 +334,10 @@
in
Pretty.block
([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @
- (Pretty.block ((if eqs=[] then [] else str "if " ::
+ (Pretty.block ((if null eqs then [] else str "if " ::
[Pretty.block eqs, Pretty.brk 1, str "then "]) @
(success_p ::
- (if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
+ (if null eqs then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
(if can_fail then
[Pretty.brk 1, str "| _ => DSeq.empty)"]
else [str ")"])))
--- a/src/HOL/Tools/meson.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jun 24 21:03:32 2010 +0200
@@ -521,10 +521,9 @@
nnf_ss also includes the one-point simprocs,
which are needed to avoid the various one-point theorems from generating junk clauses.*)
val nnf_simps =
- [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm Bex_def}, @{thm if_True},
- @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}];
-val nnf_extra_simps =
- @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms};
+ @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
+ if_eq_cancel cases_simp}
+val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
val nnf_ss =
HOL_basic_ss addsimps nnf_extra_simps
--- a/src/Pure/General/pretty.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Pure/General/pretty.ML Thu Jun 24 21:03:32 2010 +0200
@@ -102,10 +102,11 @@
(** printing items: compound phrases, strings, and breaks **)
-datatype T =
+abstype T =
Block of (output * output) * T list * int * int | (*markup output, body, indentation, length*)
String of output * int | (*text, length*)
- Break of bool * int; (*mandatory flag, width if not taken*)
+ Break of bool * int (*mandatory flag, width if not taken*)
+with
fun length (Block (_, _, _, len)) = len
| length (String (_, len)) = len
@@ -323,6 +324,8 @@
| from_ML (ML_Pretty.String s) = String s
| from_ML (ML_Pretty.Break b) = Break b;
+end;
+
(** abstract pretty printing context **)
--- a/src/Pure/Isar/code.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Pure/Isar/code.ML Thu Jun 24 21:03:32 2010 +0200
@@ -1132,7 +1132,7 @@
fun mk_prem z = Free (z, T_cong);
fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
- fun tac { prems, ... } = Simplifier.rewrite_goals_tac prems
+ fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]);
in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;
--- a/src/Pure/net.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Pure/net.ML Thu Jun 24 21:03:32 2010 +0200
@@ -17,6 +17,7 @@
sig
type key
val key_of_term: term -> key list
+ val encode_type: typ -> term
type 'a net
val empty: 'a net
exception INSERT
@@ -62,6 +63,11 @@
(*convert a term to a list of keys*)
fun key_of_term t = add_key_of_terms (t, []);
+(*encode_type -- for indexing purposes*)
+fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
+ | encode_type (TFree (a, _)) = Free (a, dummyT)
+ | encode_type (TVar (a, _)) = Var (a, dummyT);
+
(*Trees indexed by key lists: each arc is labelled by a key.
Each node contains a list of items, and arcs to children.
--- a/src/Pure/pure_setup.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Pure/pure_setup.ML Thu Jun 24 21:03:32 2010 +0200
@@ -18,6 +18,7 @@
(* ML toplevel pretty printing *)
+toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
toplevel_pp ["Position", "T"] "Pretty.position";
--- a/src/Tools/Code/code_target.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Tools/Code/code_target.ML Thu Jun 24 21:03:32 2010 +0200
@@ -142,9 +142,9 @@
name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
if serial1 = serial2 orelse not strict then
make_target ((serial1, serializer),
- ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
+ ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
(merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
- Symtab.join (K snd) (module_alias1, module_alias2))
+ Symtab.join (K fst) (module_alias1, module_alias2))
))
else
error ("Incompatible serializers: " ^ quote target);
--- a/src/Tools/induct.ML Thu Jun 24 18:45:31 2010 +0200
+++ b/src/Tools/induct.ML Thu Jun 24 21:03:32 2010 +0200
@@ -4,7 +4,7 @@
Proof by cases, induction, and coinduction.
*)
-signature INDUCT_DATA =
+signature INDUCT_ARGS =
sig
val cases_default: thm
val atomize: thm list
@@ -82,27 +82,17 @@
val setup: theory -> theory
end;
-functor Induct(Data: INDUCT_DATA): INDUCT =
+functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
struct
-
-(** misc utils **)
-
-(* encode_type -- for indexing purposes *)
-
-fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
- | encode_type (TFree (a, _)) = Free (a, dummyT)
- | encode_type (TVar (a, _)) = Var (a, dummyT);
-
-
-(* variables -- ordered left-to-right, preferring right *)
+(** variables -- ordered left-to-right, preferring right **)
fun vars_of tm =
rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
local
-val mk_var = encode_type o #2 o Term.dest_Var;
+val mk_var = Net.encode_type o #2 o Term.dest_Var;
fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
raise THM ("No variables in conclusion of rule", 0, [thm]);
@@ -128,14 +118,14 @@
fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
| conv1 k ctxt =
Conv.rewr_conv @{thm swap_params} then_conv
- Conv.forall_conv (conv1 (k-1) o snd) ctxt
+ Conv.forall_conv (conv1 (k - 1) o snd) ctxt
fun conv2 0 ctxt = conv1 j ctxt
- | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt
+ | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt
in conv2 i ctxt end;
fun swap_prems_conv 0 = Conv.all_conv
| swap_prems_conv i =
- Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
+ Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
Conv.rewr_conv Drule.swap_prems_eq
fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
@@ -145,46 +135,51 @@
val l = length (Logic.strip_params t);
val Hs = Logic.strip_assums_hyp t;
fun find (i, t) =
- case Data.dest_def (drop_judgment ctxt t) of
+ (case Induct_Args.dest_def (drop_judgment ctxt t) of
SOME (Bound j, _) => SOME (i, j)
| SOME (_, Bound j) => SOME (i, j)
- | _ => NONE
+ | _ => NONE);
in
- case get_first find (map_index I Hs) of
+ (case get_first find (map_index I Hs) of
NONE => NONE
| SOME (0, 0) => NONE
- | SOME (i, j) => SOME (i, l-j-1, j)
+ | SOME (i, j) => SOME (i, l - j - 1, j))
end;
-fun mk_swap_rrule ctxt ct = case find_eq ctxt (term_of ct) of
+fun mk_swap_rrule ctxt ct =
+ (case find_eq ctxt (term_of ct) of
NONE => NONE
- | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct);
+ | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
-val rearrange_eqs_simproc = Simplifier.simproc
- (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
- (fn thy => fn ss => fn t =>
- mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t))
+val rearrange_eqs_simproc =
+ Simplifier.simproc
+ (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
+ (fn thy => fn ss => fn t =>
+ mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t));
+
(* rotate k premises to the left by j, skipping over first j premises *)
fun rotate_conv 0 j 0 = Conv.all_conv
- | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k-1)
- | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i-1) j k);
+ | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1)
+ | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k);
fun rotate_tac j 0 = K all_tac
- | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv
- j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
+ | rotate_tac j k = SUBGOAL (fn (goal, i) =>
+ CONVERSION (rotate_conv
+ j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
+
(* rulify operators around definition *)
fun rulify_defs_conv ctxt ct =
- if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso
- not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct))))
+ if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) andalso
+ not (is_some (Induct_Args.dest_def (drop_judgment ctxt (term_of ct))))
then
(Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
(Conv.try_conv (rulify_defs_conv ctxt)) else_conv
- Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv
+ Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv
Conv.try_conv (rulify_defs_conv ctxt)) ct
else Conv.no_conv ct;
@@ -213,7 +208,7 @@
(* context data *)
-structure InductData = Generic_Data
+structure Data = Generic_Data
(
type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset;
val empty =
@@ -230,7 +225,7 @@
merge_ss (simpset1, simpset2));
);
-val get_local = InductData.get o Context.Proof;
+val get_local = Data.get o Context.Proof;
fun dest_rules ctxt =
let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
@@ -272,11 +267,11 @@
fun find_rules which how ctxt x =
map snd (Item_Net.retrieve (which (get_local ctxt)) (how x));
-val find_casesT = find_rules (#1 o #1) encode_type;
+val find_casesT = find_rules (#1 o #1) Net.encode_type;
val find_casesP = find_rules (#2 o #1) I;
-val find_inductT = find_rules (#1 o #2) encode_type;
+val find_inductT = find_rules (#1 o #2) Net.encode_type;
val find_inductP = find_rules (#2 o #2) I;
-val find_coinductT = find_rules (#1 o #3) encode_type;
+val find_coinductT = find_rules (#1 o #3) Net.encode_type;
val find_coinductP = find_rules (#2 o #3) I;
@@ -286,10 +281,11 @@
local
fun mk_att f g name arg =
- let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
+ let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
-fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
- fold Item_Net.remove (filter_rules rs th) rs))));
+fun del_att which =
+ Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
+ fold Item_Net.remove (filter_rules rs th) rs))));
fun map1 f (x, y, z, s) = (f x, y, z, s);
fun map2 f (x, y, z, s) = (x, f y, z, s);
@@ -320,12 +316,12 @@
val coinduct_pred = mk_att add_coinductP consumes1;
val coinduct_del = del_att map3;
-fun map_simpset f = InductData.map (map4 f);
+fun map_simpset f = Data.map (map4 f);
fun induct_simp f =
Thm.declaration_attribute (fn thm => fn context =>
- (map_simpset
- (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context));
+ map_simpset
+ (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context);
val induct_simp_add = induct_simp (op addsimps);
val induct_simp_del = induct_simp (op delsimps);
@@ -420,14 +416,15 @@
(* mark equality constraints in cases rule *)
-val equal_def' = Thm.symmetric Data.equal_def;
+val equal_def' = Thm.symmetric Induct_Args.equal_def;
fun mark_constraints n ctxt = Conv.fconv_rule
(Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
(MetaSimplifier.rewrite false [equal_def']))) ctxt));
val unmark_constraints = Conv.fconv_rule
- (MetaSimplifier.rewrite true [Data.equal_def]);
+ (MetaSimplifier.rewrite true [Induct_Args.equal_def]);
+
(* simplify *)
@@ -435,7 +432,7 @@
Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)));
fun simplify_conv ctxt ct =
- if exists_subterm (is_some o Data.dest_def) (term_of ct) then
+ if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) then
(Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct
else Conv.all_conv ct;
@@ -447,7 +444,7 @@
fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
-val trivial_tac = Data.trivial_tac;
+val trivial_tac = Induct_Args.trivial_tac;
@@ -487,7 +484,7 @@
(case opt_rule of
SOME r => Seq.single (inst_rule r)
| NONE =>
- (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
+ (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default])
|> tap (trace_rules ctxt casesN)
|> Seq.of_list |> Seq.maps (Seq.try inst_rule));
in
@@ -517,12 +514,12 @@
(* atomize *)
fun atomize_term thy =
- MetaSimplifier.rewrite_term thy Data.atomize []
+ MetaSimplifier.rewrite_term thy Induct_Args.atomize []
#> Object_Logic.drop_judgment thy;
-val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
+val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize;
-val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
+val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
val inner_atomize_tac =
Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
@@ -531,8 +528,8 @@
(* rulify *)
fun rulify_term thy =
- MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
- MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
+ MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
+ MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback [];
fun rulified_term thm =
let
@@ -542,8 +539,8 @@
in (thy, Logic.list_implies (map rulify As, rulify B)) end;
val rulify_tac =
- Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
- Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
+ Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
+ Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN'
Goal.conjunction_tac THEN_ALL_NEW
(Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);