--- a/src/HOL/Bali/DeclConcepts.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Mon Jun 14 15:10:50 2010 +0200
@@ -244,30 +244,30 @@
lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
by (cases m) (simp add: mhead_def member_is_static_simp)
-constdefs --{* some mnemotic selectors for various pairs *}
-
- "decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname"
- "decliface \<equiv> fst" --{* get the interface component *}
+-- {* some mnemotic selectors for various pairs *}
+
+definition decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
+ "decliface = fst" --{* get the interface component *}
- "mbr":: "(qtname \<times> memberdecl) \<Rightarrow> memberdecl"
- "mbr \<equiv> snd" --{* get the memberdecl component *}
+definition mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
+ "mbr = snd" --{* get the memberdecl component *}
- "mthd":: "('b \<times> 'a) \<Rightarrow> 'a"
- --{* also used for mdecl, mhead *}
- "mthd \<equiv> snd" --{* get the method component *}
+definition mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
+ "mthd = snd" --{* get the method component *}
+ --{* also used for mdecl, mhead *}
- "fld":: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme"
- --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
- "fld \<equiv> snd" --{* get the field component *}
+definition fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
+ "fld = snd" --{* get the field component *}
+ --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
+-- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
-constdefs --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
- fname:: "(vname \<times> 'a) \<Rightarrow> vname" --{* also used for fdecl *}
- "fname \<equiv> fst"
-
- declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
- "declclassf \<equiv> snd"
+definition fname:: "vname \<times> 'a \<Rightarrow> vname" where
+ "fname = fst"
+ --{* also used for fdecl *}
+definition declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" where
+ "declclassf = snd"
lemma decliface_simp[simp]: "decliface (I,m) = I"
@@ -318,12 +318,13 @@
lemma declclassf_simp[simp]:"declclassf (n,c) = c"
by (simp add: declclassf_def)
-constdefs --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
- "fldname" :: "(vname \<times> qtname) \<Rightarrow> vname"
- "fldname \<equiv> fst"
+ --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
- "fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname"
- "fldclass \<equiv> snd"
+definition fldname :: "vname \<times> qtname \<Rightarrow> vname" where
+ "fldname = fst"
+
+definition fldclass :: "vname \<times> qtname \<Rightarrow> qtname" where
+ "fldclass = snd"
lemma fldname_simp[simp]: "fldname (n,c) = n"
by (simp add: fldname_def)
@@ -337,8 +338,8 @@
text {* Convert a qualified method declaration (qualified with its declaring
class) to a qualified member declaration: @{text methdMembr} *}
-definition methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)" where
- "methdMembr m \<equiv> (fst m,mdecl (snd m))"
+definition methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" where
+ "methdMembr m = (fst m, mdecl (snd m))"
lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
by (simp add: methdMembr_def)
--- a/src/HOL/Bali/WellType.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Bali/WellType.thy Mon Jun 14 15:10:50 2010 +0200
@@ -103,22 +103,23 @@
"mheads G S (ClassT C) = cmheads G S C"
"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
-constdefs
+definition
--{* applicable methods, cf. 15.11.2.1 *}
- appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
- "appl_methds G S rt \<equiv> \<lambda> sig.
+ appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+ "appl_methds G S rt = (\<lambda> sig.
{(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and>
- G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
+ G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
+definition
--{* more specific methods, cf. 15.11.2.2 *}
- more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
- "more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
+ more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
+ "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
+definition
--{* maximally specific methods, cf. 15.11.2.2 *}
- max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
-
- "max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
+ max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+ "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
(\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
--- a/src/HOL/Import/proof_kernel.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon Jun 14 15:10:50 2010 +0200
@@ -1946,7 +1946,7 @@
val p3 = string_of_mixfix csyn
val p4 = smart_string_of_cterm crhs
in
- add_dump ("constdefs\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ "\n " ^ p4) thy''
+ add_dump ("definition\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n " ^ p4) thy''
end
else
add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^
@@ -2139,18 +2139,6 @@
end
handle e => (message "exception in new_type_definition"; print_exn e)
-fun add_dump_constdefs thy defname constname rhs ty =
- let
- val n = quotename constname
- val t = Syntax.string_of_typ_global thy ty
- val syn = string_of_mixfix (mk_syn thy constname)
- (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
- val eq = quote (constname ^ " == "^rhs)
- val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
- in
- add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy
- end
-
fun add_dump_syntax thy name =
let
val n = quotename name
--- a/src/HOL/List.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/List.thy Mon Jun 14 15:10:50 2010 +0200
@@ -4188,8 +4188,8 @@
primrec -- {*The lexicographic ordering for lists of the specified length*}
lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
- "lexn r 0 = {}"
- | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
+ [code del]: "lexn r 0 = {}"
+ | [code del]: "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
{(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
definition
--- a/src/HOL/MicroJava/BV/BVSpec.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Mon Jun 14 15:10:50 2010 +0200
@@ -15,48 +15,53 @@
to type \emph{checking}.
*}
-constdefs
+definition
-- "The program counter will always be inside the method:"
- check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
- "check_bounded ins et \<equiv>
+ check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool" where
+ "check_bounded ins et \<longleftrightarrow>
(\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
(\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
+definition
-- "The method type only contains declared classes:"
- check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool"
- "check_types G mxs mxr phi \<equiv> set phi \<subseteq> states G mxs mxr"
+ check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool" where
+ "check_types G mxs mxr phi \<longleftrightarrow> set phi \<subseteq> states G mxs mxr"
+definition
-- "An instruction is welltyped if it is applicable and its effect"
-- "is compatible with the type at all successor instructions:"
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
- exception_table,p_count] \<Rightarrow> bool"
- "wt_instr i G rT phi mxs max_pc et pc \<equiv>
+ exception_table,p_count] \<Rightarrow> bool" where
+ "wt_instr i G rT phi mxs max_pc et pc \<longleftrightarrow>
app i G mxs rT pc et (phi!pc) \<and>
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
+definition
-- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
- wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
- "wt_start G C pTs mxl phi ==
+ wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool" where
+ "wt_start G C pTs mxl phi \<longleftrightarrow>
G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
+definition
-- "A method is welltyped if the body is not empty, if execution does not"
-- "leave the body, if the method type covers all instructions and mentions"
-- "declared classes only, if the method calling convention is respected, and"
-- "if all instructions are welltyped."
wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
- exception_table,method_type] \<Rightarrow> bool"
- "wt_method G C pTs rT mxs mxl ins et phi \<equiv>
- let max_pc = length ins in
+ exception_table,method_type] \<Rightarrow> bool" where
+ "wt_method G C pTs rT mxs mxl ins et phi \<longleftrightarrow>
+ (let max_pc = length ins in
0 < max_pc \<and>
length phi = length ins \<and>
check_bounded ins et \<and>
check_types G mxs (1+length pTs+mxl) (map OK phi) \<and>
wt_start G C pTs mxl phi \<and>
- (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc)"
+ (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc))"
+definition
-- "A program is welltyped if it is wellformed and all methods are welltyped"
- wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
- "wt_jvm_prog G phi ==
+ wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool" where
+ "wt_jvm_prog G phi \<longleftrightarrow>
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Mon Jun 14 15:10:50 2010 +0200
@@ -117,10 +117,10 @@
| Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
-constdefs
+definition
exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
- ("_ |- _ -jvmd-> _" [61,61,61]60)
- "G |- s -jvmd-> t \<equiv>
+ ("_ |- _ -jvmd-> _" [61,61,61]60) where
+ "G |- s -jvmd-> t \<longleftrightarrow>
(s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
{(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
--- a/src/HOL/Nitpick.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Nitpick.thy Mon Jun 14 15:10:50 2010 +0200
@@ -214,6 +214,10 @@
definition inverse_frac :: "'a \<Rightarrow> 'a" where
"inverse_frac q \<equiv> frac (denom q) (num q)"
+definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+[nitpick_simp]:
+"less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0"
+
definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
[nitpick_simp]:
"less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0"
@@ -245,7 +249,7 @@
wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
- less_eq_frac of_frac
+ less_frac less_eq_frac of_frac
hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
word
hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
@@ -254,6 +258,6 @@
list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
- inverse_frac_def less_eq_frac_def of_frac_def
+ inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
end
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Jun 14 15:10:50 2010 +0200
@@ -95,20 +95,20 @@
nitpick [expect = genuine]
oops
-lemma "Pair a b \<equiv> Abs_Prod (Pair_Rep a b)"
+lemma "Pair a b = Abs_prod (Pair_Rep a b)"
nitpick [card = 1\<midarrow>2, expect = none]
by (rule Pair_def)
-lemma "Pair a b \<equiv> Abs_Prod (Pair_Rep b a)"
+lemma "Pair a b = Abs_prod (Pair_Rep b a)"
nitpick [card = 1\<midarrow>2, expect = none]
nitpick [dont_box, expect = genuine]
oops
-lemma "fst (Abs_Prod (Pair_Rep a b)) = a"
+lemma "fst (Abs_prod (Pair_Rep a b)) = a"
nitpick [card = 2, expect = none]
-by (simp add: Pair_def [THEN symmetric])
+by (simp add: Pair_def [THEN sym])
-lemma "fst (Abs_Prod (Pair_Rep a b)) = b"
+lemma "fst (Abs_prod (Pair_Rep a b)) = b"
nitpick [card = 1\<midarrow>2, expect = none]
nitpick [dont_box, expect = genuine]
oops
@@ -117,19 +117,19 @@
nitpick [expect = none]
apply (rule ccontr)
apply simp
-apply (drule subst [where P = "\<lambda>r. Abs_Prod r = Abs_Prod (Pair_Rep a b)"])
+apply (drule subst [where P = "\<lambda>r. Abs_prod r = Abs_prod (Pair_Rep a b)"])
apply (rule refl)
-by (simp add: Pair_def [THEN symmetric])
+by (simp add: Pair_def [THEN sym])
-lemma "Abs_Prod (Rep_Prod a) = a"
+lemma "Abs_prod (Rep_prod a) = a"
nitpick [card = 2, expect = none]
-by (rule Rep_Prod_inverse)
+by (rule Rep_prod_inverse)
-lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inl_Rep a)"
+lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inl_Rep a)"
nitpick [card = 1, expect = none]
-by (simp only: Inl_def o_def)
+by (simp add: Inl_def o_def)
-lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inr_Rep a)"
+lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inr_Rep a)"
nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]
oops
@@ -137,20 +137,20 @@
nitpick [expect = none]
by (rule Inl_Rep_not_Inr_Rep)
-lemma "Abs_Sum (Rep_Sum a) = a"
+lemma "Abs_sum (Rep_sum a) = a"
nitpick [card = 1, expect = none]
nitpick [card = 2, expect = none]
-by (rule Rep_Sum_inverse)
+by (rule Rep_sum_inverse)
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
nitpick [expect = none]
by (rule Zero_nat_def_raw)
-lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
+lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
nitpick [expect = none]
by (rule Suc_def)
-lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
+lemma "Suc n = Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
nitpick [expect = genuine]
oops
--- a/src/HOL/Rat.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Rat.thy Mon Jun 14 15:10:50 2010 +0200
@@ -1182,15 +1182,16 @@
(@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
(@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
(@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
+ (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}),
(@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
(@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
(@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})]
*}
lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
- number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
- plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
- zero_rat_inst.zero_rat
+ number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat
+ ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
+ uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
subsection{* Float syntax *}
--- a/src/HOL/RealDef.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/RealDef.thy Mon Jun 14 15:10:50 2010 +0200
@@ -1806,12 +1806,13 @@
(@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
(@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
(@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
+ (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_eq_frac}),
(@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
*}
lemmas [nitpick_def] = inverse_real_inst.inverse_real
number_real_inst.number_of_real one_real_inst.one_real
- ord_real_inst.less_eq_real plus_real_inst.plus_real
+ ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real
times_real_inst.times_real uminus_real_inst.uminus_real
zero_real_inst.zero_real
--- a/src/HOL/Sledgehammer.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Jun 14 15:10:50 2010 +0200
@@ -25,6 +25,9 @@
("Tools/Sledgehammer/metis_tactics.ML")
begin
+definition skolem_id :: "'a \<Rightarrow> 'a" where
+[no_atp]: "skolem_id = (\<lambda>x. x)"
+
definition COMBI :: "'a \<Rightarrow> 'a" where
[no_atp]: "COMBI P \<equiv> P"
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Mon Jun 14 15:10:50 2010 +0200
@@ -80,7 +80,7 @@
fun kodkod_formula_from_term ctxt card frees =
let
- fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r =
+ fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
let
val jss = atom_schema_of SRep card T1 |> map (rpair 0)
|> all_combinations
@@ -115,7 +115,7 @@
@{const Not} $ t1 => Not (to_F Ts t1)
| @{const False} => False
| @{const True} => True
- | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+ | Const (@{const_name All}, _) $ Abs (_, T, t') =>
All (decls_for SRep card Ts T, to_F (T :: Ts) t')
| (t0 as Const (@{const_name All}, _)) $ t1 =>
to_F Ts (t0 $ eta_expand Ts t1 1)
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Jun 14 15:10:50 2010 +0200
@@ -298,7 +298,6 @@
val peephole_optim = true
val nat_card = 4
val int_card = 9
- val bits = 8
val j0 = 0
val constrs = kodkod_constrs peephole_optim nat_card int_card j0
val (free_rels, pool, table) =
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 14 15:10:50 2010 +0200
@@ -18,6 +18,7 @@
structure Metis_Tactics : METIS_TACTICS =
struct
+open Sledgehammer_Util
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
open Sledgehammer_HOL_Clause
@@ -84,7 +85,7 @@
val args = map hol_term_to_fol_FO tms
in Metis.Term.Fn (c, tyargs @ args) end
| (CombVar ((v, _), _), []) => Metis.Term.Var v
- | _ => error "hol_term_to_fol_FO";
+ | _ => raise Fail "hol_term_to_fol_FO";
fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
| hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
@@ -118,7 +119,7 @@
metis_lit pol "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
-fun literals_of_hol_thm thy mode t =
+fun literals_of_hol_term thy mode t =
let val (lits, types_sorts) = literals_of_term thy t
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
@@ -134,21 +135,24 @@
fun metis_of_tfree tf =
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
-fun hol_thm_to_fol is_conjecture ctxt mode th =
- let val thy = ProofContext.theory_of ctxt
- val (mlits, types_sorts) =
- (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
+fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (skolem_somes, (mlits, types_sorts)) =
+ th |> prop_of |> conceal_skolem_somes j skolem_somes
+ ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
in
if is_conjecture then
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
- type_literals_for_types types_sorts)
+ type_literals_for_types types_sorts, skolem_somes)
else
let val tylits = filter_out (default_sort ctxt) types_sorts
|> type_literals_for_types
val mtylits = if Config.get ctxt type_lits
then map (metis_of_type_literals false) tylits else []
in
- (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
+ (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
+ skolem_somes)
end
end;
@@ -194,7 +198,7 @@
fun apply_list rator nargs rands =
let val trands = terms_of rands
in if length trands = nargs then Term (list_comb(rator, trands))
- else error
+ else raise Fail
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
" expected " ^ Int.toString nargs ^
" received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
@@ -229,12 +233,22 @@
| NONE =>
case strip_prefix tfree_prefix x of
SOME tf => mk_tfree ctxt tf
- | NONE => error ("fol_type_to_isa: " ^ x));
+ | NONE => raise Fail ("fol_type_to_isa: " ^ x));
+
+fun reveal_skolem_somes skolem_somes =
+ map_aterms (fn t as Const (s, T) =>
+ if String.isPrefix skolem_theory_name s then
+ AList.lookup (op =) skolem_somes s
+ |> the |> map_types Type_Infer.paramify_vars
+ else
+ t
+ | t => t)
(*Maps metis terms to isabelle terms*)
-fun fol_term_to_hol_RAW ctxt fol_tm =
+fun hol_term_from_fol_PT ctxt fol_tm =
let val thy = ProofContext.theory_of ctxt
- val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
+ val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
+ Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
(case strip_prefix tvar_prefix v of
SOME w => Type (make_tvar w)
@@ -250,7 +264,7 @@
Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
| _ => case tm_to_tt rator of
Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
- | _ => error "tm_to_tt: HO application"
+ | _ => raise Fail "tm_to_tt: HO application"
end
| tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
and applic_to_tt ("=",ts) =
@@ -265,12 +279,13 @@
val tys = types_of (List.take(tts,ntypes))
in if length tys = ntypes then
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
- else error ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
- " but gets " ^ Int.toString (length tys) ^
- " type arguments\n" ^
- cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
- " the terms are \n" ^
- cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
+ else
+ raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
+ " but gets " ^ Int.toString (length tys) ^
+ " type arguments\n" ^
+ cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
+ " the terms are \n" ^
+ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
case strip_prefix tconst_prefix a of
@@ -284,12 +299,17 @@
SOME b =>
let val opr = Term.Free(b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
- | NONE => error ("unexpected metis function: " ^ a)
- in case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected" end;
+ | NONE => raise Fail ("unexpected metis function: " ^ a)
+ in
+ case tm_to_tt fol_tm of
+ Term t => t
+ | _ => raise Fail "fol_tm_to_tt: Term expected"
+ end
(*Maps fully-typed metis terms to isabelle terms*)
-fun fol_term_to_hol_FT ctxt fol_tm =
- let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
+fun hol_term_from_fol_FT ctxt fol_tm =
+ let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
+ Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
(case strip_prefix schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
@@ -302,7 +322,7 @@
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix fixed_var_prefix x of
SOME v => Free (v, fol_type_to_isa ctxt ty)
- | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
+ | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
cvt tm1 $ cvt tm2
| cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
@@ -316,21 +336,21 @@
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix fixed_var_prefix x of
SOME v => Free (v, dummyT)
- | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
- fol_term_to_hol_RAW ctxt t))
- | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t);
- fol_term_to_hol_RAW ctxt t)
- in cvt fol_tm end;
+ | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
+ hol_term_from_fol_PT ctxt t))
+ | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
+ hol_term_from_fol_PT ctxt t)
+ in fol_tm |> cvt end
-fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
- | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
- | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
+fun hol_term_from_fol FT = hol_term_from_fol_FT
+ | hol_term_from_fol _ = hol_term_from_fol_PT
-fun fol_terms_to_hol ctxt mode fol_tms =
- let val ts = map (fol_term_to_hol ctxt mode) fol_tms
+fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
+ let val thy = ProofContext.theory_of ctxt
+ val ts = map (hol_term_from_fol mode ctxt) fol_tms
val _ = trace_msg (fn () => " calling type inference:")
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
- val ts' = infer_types ctxt ts;
+ val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
val _ = app (fn t => trace_msg
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
@@ -354,7 +374,8 @@
fun lookth thpairs (fth : Metis.Thm.thm) =
the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
- handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
+ handle Option =>
+ raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
fun is_TrueI th = Thm.eq_thm(TrueI,th);
@@ -371,22 +392,23 @@
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
(* INFERENCE RULE: ASSUME *)
-fun assume_inf ctxt mode atm =
+fun assume_inf ctxt mode skolem_somes atm =
inst_excluded_middle
(ProofContext.theory_of ctxt)
- (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
+ (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm))
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
that new TVars are distinct and that types can be inferred from terms.*)
-fun inst_inf ctxt mode thpairs fsubst th =
+fun inst_inf ctxt mode skolem_somes thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
+ (* We call "reveal_skolem_somes" and "infer_types" below. *)
+ val t = hol_term_from_fol mode ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option =>
(trace_msg (fn() => "List.find failed for the variable " ^ x ^
@@ -401,7 +423,8 @@
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
- val tms = infer_types ctxt rawtms;
+ val tms = rawtms |> map (reveal_skolem_somes skolem_somes)
+ |> infer_types ctxt
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = trace_msg (fn () =>
@@ -409,10 +432,11 @@
(substs' |> map (fn (x, y) =>
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
Syntax.string_of_term ctxt (term_of y)))));
- in cterm_instantiate substs' i_th end
+ in cterm_instantiate substs' i_th end
handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
| ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
- "\n(Perhaps you want to try \"metisFT\".)")
+ "\n(Perhaps you want to try \"metisFT\" if you \
+ \haven't done so already.)")
(* INFERENCE RULE: RESOLVE *)
@@ -428,7 +452,7 @@
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
end;
-fun resolve_inf ctxt mode thpairs atm th1 th2 =
+fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
let
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
@@ -438,15 +462,16 @@
else if is_TrueI i_th2 then i_th1
else
let
- val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
+ val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes)
+ (Metis.Term.Fn atm)
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
val prems_th2 = prems_of i_th2
val index_th1 = get_index (mk_not i_atm) prems_th1
- handle Empty => error "Failed to find literal in th1"
+ handle Empty => raise Fail "Failed to find literal in th1"
val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1)
val index_th2 = get_index i_atm prems_th2
- handle Empty => error "Failed to find literal in th2"
+ handle Empty => raise Fail "Failed to find literal in th2"
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end
end;
@@ -455,9 +480,9 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inf ctxt mode t =
+fun refl_inf ctxt mode skolem_somes t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (fol_terms_to_hol ctxt mode) t
+ val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) t
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
@@ -467,10 +492,10 @@
| get_ty_arg_size _ _ = 0;
(* INFERENCE RULE: EQUALITY *)
-fun equality_inf ctxt mode (pos, atm) fp fr =
+fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr =
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis.Term.Fn atm
- val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
+ val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolem_somes [m_tm, fr]
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -491,6 +516,10 @@
fun path_finder_HO tm [] = (tm, Term.Bound 0)
| path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
| path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
+ | path_finder_HO tm ps =
+ raise Fail ("equality_inf, path_finder_HO: path = " ^
+ space_implode " " (map Int.toString ps) ^
+ " isa-term: " ^ Syntax.string_of_term ctxt tm)
fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
| path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
path_finder_FT tm ps t1
@@ -498,10 +527,11 @@
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
| path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
- | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
- space_implode " " (map Int.toString ps) ^
- " isa-term: " ^ Syntax.string_of_term ctxt tm ^
- " fol-term: " ^ Metis.Term.toString t)
+ | path_finder_FT tm ps t =
+ raise Fail ("equality_inf, path_finder_FT: path = " ^
+ space_implode " " (map Int.toString ps) ^
+ " isa-term: " ^ Syntax.string_of_term ctxt tm ^
+ " fol-term: " ^ Metis.Term.toString t)
fun path_finder FO tm ps _ = path_finder_FO tm ps
| path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
(*equality: not curried, as other predicates are*)
@@ -539,24 +569,28 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
- | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
- | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
- factor (inst_inf ctxt mode thpairs f_subst f_th1)
- | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
- factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
- | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
- | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
- equality_inf ctxt mode f_lit f_p f_r;
+fun step ctxt mode skolem_somes thpairs p =
+ case p of
+ (fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
+ | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolem_somes f_atm
+ | (_, Metis.Proof.Subst (f_subst, f_th1)) =>
+ factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1)
+ | (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
+ factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2)
+ | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm
+ | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
+ equality_inf ctxt mode skolem_somes f_lit f_p f_r
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
-fun translate _ _ thpairs [] = thpairs
- | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
+(* FIXME: use "fold" instead *)
+fun translate _ _ _ thpairs [] = thpairs
+ | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
let val _ = trace_msg (fn () => "=============================================")
val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
- val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
+ val th = Meson.flexflex_first_order (step ctxt mode skolem_somes
+ thpairs (fol_th, inf))
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg (fn () => "=============================================")
val n_metis_lits =
@@ -564,7 +598,7 @@
in
if nprems_of th = n_metis_lits then ()
else error "Metis: proof reconstruction has gone wrong";
- translate mode ctxt ((fol_th, th) :: thpairs) infpairs
+ translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
end;
(*Determining which axiom clauses are actually used*)
@@ -592,7 +626,8 @@
type logic_map =
{axioms: (Metis.Thm.thm * thm) list,
- tfrees: type_literal list};
+ tfrees: type_literal list,
+ skolem_somes: (string * term) list}
fun const_in_metis c (pred, tm_list) =
let
@@ -610,14 +645,15 @@
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
- | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
- add_type_thm cls {axioms = (mth, ith) :: axioms,
- tfrees = tfrees}
+ | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} =
+ add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
+ skolem_somes = skolem_somes}
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees} : logic_map =
- {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
- tfrees = tfrees};
+fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map =
+ {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
+ axioms,
+ tfrees = tfrees, skolem_somes = skolem_somes}
fun string_of_mode FO = "FO"
| string_of_mode HO = "HO"
@@ -628,18 +664,27 @@
let val thy = ProofContext.theory_of ctxt
(*The modes FO and FT are sticky. HO can be downgraded to FO.*)
fun set_mode FO = FO
- | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
+ | set_mode HO =
+ if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
+ else HO
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture ith {axioms, tfrees} : logic_map =
- let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
+ fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map =
+ let
+ val (mth, tfree_lits, skolem_somes) =
+ hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes
+ ith
in
{axioms = (mth, Meson.make_meta_clause ith) :: axioms,
- tfrees = union (op =) tfree_lits tfrees}
+ tfrees = union (op =) tfree_lits tfrees,
+ skolem_somes = skolem_somes}
end;
- val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt}
- val lmap = fold (add_thm false) ths (add_tfrees lmap0)
+ val lmap as {skolem_somes, ...} =
+ {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
+ |> fold (add_thm true) cls
+ |> add_tfrees
+ |> fold (add_thm false) ths
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
(*Now check for the existence of certain combinators*)
@@ -649,11 +694,10 @@
val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
- val lmap' = if mode=FO then lmap
- else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
- in
- (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
- end;
+ val lmap =
+ lmap |> mode <> FO
+ ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
+ in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
fun refute cls =
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
@@ -664,7 +708,7 @@
exception METIS of string;
-(* Main function to start metis prove and reconstruction *)
+(* Main function to start metis proof and reconstruction *)
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs =
@@ -674,7 +718,7 @@
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
- val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
+ val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
@@ -694,7 +738,7 @@
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
val proof = Metis.Proof.proof mth
- val result = translate mode ctxt' axioms proof
+ val result = translate ctxt' mode skolem_somes axioms proof
and used = map_filter (used_axioms axioms) proof
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 14 15:10:50 2010 +0200
@@ -21,6 +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 relevant_facts :
bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> thm list
@@ -116,6 +117,8 @@
add_const_typ_table (const_with_typ thy (c,typ), tab)
| add_term_consts_typs_rm thy (Free(c, typ), tab) =
add_const_typ_table (const_with_typ thy (c,typ), tab)
+ | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _, tab) =
+ tab
| add_term_consts_typs_rm thy (t $ u, tab) =
add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
| add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
@@ -368,38 +371,35 @@
fun valid_facts facts =
(facts, []) |-> Facts.fold_static (fn (name, ths0) =>
- let
- fun check_thms a =
- (case try (ProofContext.get_thms ctxt) a of
- NONE => false
- | SOME ths1 => Thm.eq_thms (ths0, ths1));
+ if Facts.is_concealed facts name orelse
+ (respect_no_atp andalso is_package_def name) orelse
+ member (op =) multi_base_blacklist (Long_Name.base_name name) then
+ I
+ else
+ let
+ fun check_thms a =
+ (case try (ProofContext.get_thms ctxt) a of
+ NONE => false
+ | SOME ths1 => Thm.eq_thms (ths0, ths1));
- val name1 = Facts.extern facts name;
- val name2 = Name_Space.extern full_space name;
- val ths = filter_out is_theorem_bad_for_atps ths0;
- in
- if Facts.is_concealed facts name orelse
- (respect_no_atp andalso is_package_def name) then
- I
- else case find_first check_thms [name1, name2, name] of
- NONE => I
- | SOME name' =>
- cons (name' |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix, ths)
- end);
+ val name1 = Facts.extern facts name;
+ val name2 = Name_Space.extern full_space name;
+ val ths = filter_out is_theorem_bad_for_atps ths0;
+ in
+ case find_first check_thms [name1, name2, name] of
+ NONE => I
+ | SOME name' =>
+ cons (name' |> forall (member Thm.eq_thm chained_ths) ths
+ ? prefix chained_prefix, ths)
+ end)
in valid_facts global_facts @ valid_facts local_facts end;
fun multi_name a th (n, pairs) =
(n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
-fun add_single_names (a, []) pairs = pairs
- | add_single_names (a, [th]) pairs = (a, th) :: pairs
- | add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs));
-
-(*Ignore blacklisted basenames*)
-fun add_multi_names (a, ths) pairs =
- if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs
- else add_single_names (a, ths) pairs;
+fun add_names (a, []) pairs = pairs
+ | add_names (a, [th]) pairs = (a, th) :: pairs
+ | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs))
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
@@ -408,8 +408,7 @@
fun name_thm_pairs respect_no_atp ctxt name_thms_pairs =
let
val (mults, singles) = List.partition is_multi name_thms_pairs
- val ps = [] |> fold add_single_names singles
- |> fold add_multi_names mults
+ val ps = [] |> fold add_names singles |> fold add_names mults
in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
fun is_named ("", th) =
@@ -472,8 +471,12 @@
(* 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 (Meson.is_fol_term thy o prop_of o fst) cls
+fun restrict_to_logic thy true cls =
+ filter (is_quasi_fol_term thy o prop_of o fst) cls
| restrict_to_logic thy false cls = cls;
(**** Predicates to detect unwanted clauses (prolific or likely to cause
@@ -531,7 +534,7 @@
fun remove_dangerous_clauses full_types add_thms =
filter_out (is_dangerous_theorem full_types add_thms o fst)
-fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
+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
@@ -542,17 +545,17 @@
else
let
val thy = ProofContext.theory_of ctxt
- val add_thms = cnf_for_facts ctxt add
val has_override = not (null add) orelse not (null del)
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_fol_goal thy goal_cls
val axioms =
- checked_name_thm_pairs respect_no_atp ctxt
+ 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
- |> restrict_to_logic thy is_FO
- |> not only ? remove_dangerous_clauses full_types add_thms
+ |> not only ? restrict_to_logic thy is_FO
+ |> (if only then I
+ else remove_dangerous_clauses full_types (cnf_for_facts ctxt add))
in
relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
@@ -564,7 +567,7 @@
create additional clauses based on the information from extra_cls *)
fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy =
let
- val is_FO = is_first_order thy goal_cls
+ val is_FO = is_fol_goal thy goal_cls
val ccls = subtract_cls extra_cls goal_cls
val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
@@ -576,7 +579,7 @@
val conjectures = make_conjecture_clauses dfg thy ccls
val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
- val helper_clauses = get_helper_clauses dfg thy is_FO (conjectures, extra_cls, [])
+ val helper_clauses = get_helper_clauses dfg thy is_FO conjectures extra_cls
val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
val classrel_clauses = make_classrel_clauses thy subs supers'
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 14 15:10:50 2010 +0200
@@ -10,8 +10,10 @@
val chained_prefix: string
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
+ val skolem_theory_name: string
val skolem_prefix: string
val skolem_infix: string
+ val is_skolem_const_name: string -> bool
val cnf_axiom: theory -> thm -> thm list
val multi_base_blacklist: string list
val is_theorem_bad_for_atps: thm -> bool
@@ -39,6 +41,7 @@
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
+val skolem_theory_name = "Sledgehammer.Sko"
val skolem_prefix = "sko_"
val skolem_infix = "$"
@@ -75,10 +78,16 @@
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);
-fun skolem_name thm_name nref var_name =
- skolem_prefix ^ thm_name ^ "_" ^ Int.toString (Unsynchronized.inc nref) ^
+fun skolem_name thm_name j var_name =
+ skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^
skolem_infix ^ (if var_name = "" then "g" else flatten_name var_name)
+(* Hack: Could return false positives (e.g., a user happens to declare a
+ constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+ Long_Name.base_name
+ #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
fun rhs_extra_types lhsT rhs =
let val lhs_vars = Term.add_tfreesT lhsT []
fun add_new_TFrees (TFree v) =
@@ -87,64 +96,76 @@
val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
+fun skolem_type_and_args bound_T body =
+ let
+ val args1 = OldTerm.term_frees body
+ val Ts1 = map type_of args1
+ val Ts2 = rhs_extra_types (Ts1 ---> bound_T) body
+ val args2 = map (fn T => Free (gensym "vsk", T)) Ts2
+ in (Ts2 ---> Ts1 ---> bound_T, args2 @ args1) end
+
(* Traverse a theorem, declaring Skolem function definitions. String "s" is the
suggested prefix for the Skolem constants. *)
fun declare_skolem_funs s th thy =
let
- val nref = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) (axs, thy) =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val cname = skolem_name s nref s'
- val args0 = OldTerm.term_frees xtp (*get the formal parameter list*)
- val Ts = map type_of args0
- val extraTs = rhs_extra_types (Ts ---> T) xtp
- val argsx = map (fn T => Free (gensym "vsk", T)) extraTs
- val args = argsx @ args0
- val cT = extraTs ---> Ts ---> T
- val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
- (*Forms a lambda-abstraction over the formal parameters*)
- val (c, thy) =
- Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
- val cdef = cname ^ "_def"
- val ((_, ax), thy) =
- Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
- val ax' = Drule.export_without_context ax
- in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
+ val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p)))
+ (axs, thy) =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val id = skolem_name s (Unsynchronized.inc skolem_count) s'
+ val (cT, args) = skolem_type_and_args T body
+ val rhs = list_abs_free (map dest_Free args,
+ HOLogic.choice_const T $ body)
+ (*Forms a lambda-abstraction over the formal parameters*)
+ val (c, thy) =
+ Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
+ val cdef = id ^ "_def"
+ val ((_, ax), thy) =
+ Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy
+ val ax' = Drule.export_without_context ax
+ in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy) end
| dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
- in dec_sko (subst_bound (Free (fname, T), p)) thx end
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
+ in dec_sko (subst_bound (Free (fname, T), p)) thx end
| dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
| dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
| dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
| dec_sko t thx = thx
in dec_sko (prop_of th) ([], thy) end
+fun mk_skolem_id t =
+ let val T = fastype_of t in Const (@{const_name skolem_id}, T --> T) $ t end
+
(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skolem_funs s th =
- let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *)
- fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (s', T, p))) defs =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
- val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
- val Ts = map type_of args
- val cT = Ts ---> T
- val id = skolem_name s sko_count s'
- val c = Free (id, cT)
- val rhs = list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ xtp)
- (*Forms a lambda-abstraction over the formal parameters*)
- val def = Logic.mk_equals (c, rhs)
- in dec_sko (subst_bound (list_comb(c,args), p)) (def :: defs) end
- | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
- in dec_sko (subst_bound (Free(fname,T), p)) defs end
- | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
- | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
- | dec_sko t defs = defs (*Do nothing otherwise*)
+fun assume_skolem_funs inline s th =
+ let
+ val skolem_count = Unsynchronized.ref 0 (* FIXME ??? *)
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
+ val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
+ val Ts = map type_of args
+ val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
+ val id = skolem_name s (Unsynchronized.inc skolem_count) s'
+ val c = Free (id, cT)
+ val rhs = list_abs_free (map dest_Free args,
+ HOLogic.choice_const T $ body)
+ |> inline ? mk_skolem_id
+ (*Forms a lambda-abstraction over the formal parameters*)
+ val def = Logic.mk_equals (c, rhs)
+ val comb = list_comb (if inline then rhs else c, args)
+ in dec_sko (subst_bound (comb, p)) (def :: defs) end
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
+ in dec_sko (subst_bound (Free(fname,T), p)) defs end
+ | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+ | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
+ | dec_sko t defs = defs (*Do nothing otherwise*)
in dec_sko (prop_of th) [] end;
@@ -273,19 +294,28 @@
(*Given the definition of a Skolem function, return a theorem to replace
an existential formula by a use of that function.
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_of_def def =
- let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
- val (ch, frees) = c_variant_abs_multi (rhs, [])
- val (chilbert,cabs) = Thm.dest_comb ch
+fun skolem_theorem_of_def inline def =
+ let
+ val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
+ val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
+ val (ch, frees) = c_variant_abs_multi (rhs', [])
+ val (chilbert, cabs) = ch |> Thm.dest_comb
val thy = Thm.theory_of_cterm chilbert
val t = Thm.term_of chilbert
- val T = case t of
- Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T
- | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
+ val T =
+ case t of
+ Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
+ | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
val cex = Thm.cterm_of thy (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
- and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
- fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS @{thm someI_ex}) 1
+ and conc =
+ Drule.list_comb (if inline then rhs else c, frees)
+ |> Drule.beta_conv cabs |> c_mkTrueprop
+ fun tacf [prem] =
+ (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
+ else rewrite_goals_tac [def])
+ THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
+ RS @{thm someI_ex}) 1
in Goal.prove_internal [ex_tm] conc tacf
|> forall_intr_list frees
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
@@ -303,9 +333,9 @@
in (th3, ctxt) end;
(*Generate Skolem functions for a theorem supplied in nnf*)
-fun assume_skolem_of_def s th =
- map (skolem_of_def o Thm.assume o cterm_of (theory_of_thm th))
- (assume_skolem_funs s th)
+fun skolem_theorems_of_assume inline s th =
+ map (skolem_theorem_of_def inline o Thm.assume o cterm_of (theory_of_thm th))
+ (assume_skolem_funs inline s th)
(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
@@ -364,7 +394,7 @@
else gensym "unknown_thm_";
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolem_thm (s, th) =
+fun skolemize_theorem s th =
if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
is_theorem_bad_for_atps th then
[]
@@ -372,7 +402,8 @@
let
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
- val defs = assume_skolem_of_def s nnfth
+ val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
+ val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in
cnfs |> map introduce_combinators
@@ -402,7 +433,7 @@
fun cnf_axiom thy th0 =
let val th = Thm.transfer thy th0 in
case lookup_cache thy th of
- NONE => map Thm.close_derivation (skolem_thm (fake_name th, th))
+ NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
| SOME cls => cls
end;
@@ -438,7 +469,8 @@
fun skolem_cnfs (th, ctxt0, ctxt, nnfth, defs) =
let
- val (cnfs, ctxt) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt;
+ val (cnfs, ctxt) =
+ Meson.make_cnf (map (skolem_theorem_of_def false) defs) nnfth ctxt
val cnfs' = cnfs
|> map introduce_combinators
|> Variable.export ctxt ctxt0
@@ -455,14 +487,18 @@
if Facts.is_concealed facts name orelse already_seen thy name then I
else cons (name, ths));
val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
- if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
- else fold_index (fn (i, th) =>
- if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
- I
- else
- cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
+ if member (op =) multi_base_blacklist (Long_Name.base_name name) then
+ I
+ else
+ fold_index (fn (i, th) =>
+ if is_theorem_bad_for_atps th orelse
+ is_some (lookup_cache thy th) then
+ I
+ else
+ cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)
in
- if null new_facts then NONE
+ if null new_facts then
+ NONE
else
let
val (defs, thy') = thy
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 14 15:10:50 2010 +0200
@@ -29,14 +29,16 @@
val type_of_combterm : combterm -> fol_type
val strip_combterm_comb : combterm -> combterm * combterm list
val literals_of_term : theory -> term -> literal list * typ list
+ val conceal_skolem_somes :
+ int -> (string * term) list -> term -> (string * term) list * term
exception TRIVIAL
val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
val make_axiom_clauses : bool -> theory ->
(thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
val type_wrapper_name : string
- val get_helper_clauses : bool -> theory -> bool ->
- hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
- hol_clause list
+ val get_helper_clauses :
+ bool -> theory -> bool -> hol_clause list
+ -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
val write_tptp_file : bool -> bool -> bool -> Path.T ->
hol_clause list * hol_clause list * hol_clause list * hol_clause list *
classrel_clause list * arity_clause list -> name_pool option * int
@@ -115,28 +117,31 @@
TyVar (make_schematic_type_var x, string_of_indexname x);
-fun const_type_of dfg thy (c,t) =
- let val (tp,ts) = type_of dfg t
- in (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
-
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
-fun combterm_of dfg thy (Const(c,t)) =
- let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
- val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
+fun combterm_of dfg thy (Const (c, T)) =
+ let
+ val (tp, ts) = type_of dfg T
+ val tvar_list =
+ (if String.isPrefix skolem_theory_name c then
+ [] |> Term.add_tvarsT T |> map TVar
+ else
+ (c, T) |> Sign.const_typargs thy)
+ |> map (simp_type_of dfg)
+ val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
in (c',ts) end
- | combterm_of dfg _ (Free(v,t)) =
- let val (tp,ts) = type_of dfg t
+ | combterm_of dfg _ (Free(v, T)) =
+ let val (tp,ts) = type_of dfg T
val v' = CombConst (`make_fixed_var v, tp, [])
in (v',ts) end
- | combterm_of dfg _ (Var(v,t)) =
- let val (tp,ts) = type_of dfg t
+ | combterm_of dfg _ (Var(v, T)) =
+ let val (tp,ts) = type_of dfg T
val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
in (v',ts) end
| combterm_of dfg thy (P $ Q) =
let val (P',tsP) = combterm_of dfg thy P
val (Q',tsQ) = combterm_of dfg thy Q
in (CombApp(P',Q'), union (op =) tsP tsQ) end
- | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
+ | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t);
fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
| predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
@@ -153,36 +158,78 @@
fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
val literals_of_term = literals_of_term_dfg false;
+fun skolem_name i j num_T_args =
+ skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
+ skolem_infix ^ "g"
+
+fun conceal_skolem_somes i skolem_somes t =
+ if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
+ let
+ fun aux skolem_somes
+ (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
+ let
+ val (skolem_somes, s) =
+ if i = ~1 then
+ (skolem_somes, @{const_name undefined})
+ else case AList.find (op aconv) skolem_somes t of
+ s :: _ => (skolem_somes, s)
+ | _ =>
+ let
+ val s = skolem_theory_name ^ "." ^
+ skolem_name i (length skolem_somes)
+ (length (Term.add_tvarsT T []))
+ in ((s, t) :: skolem_somes, s) end
+ in (skolem_somes, Const (s, T)) end
+ | aux skolem_somes (t1 $ t2) =
+ let
+ val (skolem_somes, t1) = aux skolem_somes t1
+ val (skolem_somes, t2) = aux skolem_somes t2
+ in (skolem_somes, t1 $ t2) end
+ | aux skolem_somes (Abs (s, T, t')) =
+ let val (skolem_somes, t') = aux skolem_somes t' in
+ (skolem_somes, Abs (s, T, t'))
+ end
+ | aux skolem_somes t = (skolem_somes, t)
+ in aux skolem_somes t end
+ else
+ (skolem_somes, t)
+
(* Trivial problem, which resolution cannot handle (empty clause) *)
exception TRIVIAL;
(* making axiom and conjecture clauses *)
-fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
- let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
- in
- if forall isFalse lits then
- raise TRIVIAL
- else
- HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
- kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
- end;
-
-
-fun add_axiom_clause dfg thy (th, (name, id)) =
- let val cls = make_clause dfg thy (id, name, Axiom, th) in
- not (isTaut cls) ? cons (name, cls)
+fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes =
+ let
+ val (skolem_somes, t) =
+ th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
+ val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t
+ in
+ if forall isFalse lits then
+ raise TRIVIAL
+ else
+ (skolem_somes,
+ HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+ kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
end
+fun add_axiom_clause dfg thy (th, (name, id)) (skolem_somes, clss) =
+ let
+ val (skolem_somes, cls) =
+ make_clause dfg thy (id, name, Axiom, th) skolem_somes
+ in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
+
fun make_axiom_clauses dfg thy clauses =
- fold (add_axiom_clause dfg thy) clauses []
+ ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd
-fun make_conjecture_clauses_aux _ _ _ [] = []
- | make_conjecture_clauses_aux dfg thy n (th::ths) =
- make_clause dfg thy (n,"conjecture", Conjecture, th) ::
- make_conjecture_clauses_aux dfg thy (n+1) ths;
-
-fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
-
+fun make_conjecture_clauses dfg thy =
+ let
+ fun aux _ _ [] = []
+ | aux n skolem_somes (th :: ths) =
+ let
+ val (skolem_somes, cls) =
+ make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes
+ in cls :: aux (n + 1) skolem_somes ths end
+ in aux 0 [] end
(**********************************************************************)
(* convert clause into ATP specific formats: *)
@@ -415,19 +462,16 @@
fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
-fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) =
- member (op =) user_lemmas axiom_name ? fold count_literal literals
-
fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint)
-fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
+fun get_helper_clauses dfg thy isFO conjectures axcls =
if isFO then
[]
else
let
- val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
- val ct = init_counters |> fold count_clause conjectures
- |> fold (count_user_clause user_lemmas) axclauses
+ val axclauses = map snd (make_axiom_clauses dfg thy axcls)
+ val ct = init_counters
+ |> fold (fold count_clause) [conjectures, axclauses]
fun needed c = the (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
@@ -439,9 +483,7 @@
else []
val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
@{thm equal_imp_fequal}]
- in
- map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
- end;
+ in map snd (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end
(*Find the minimal arity of each function mentioned in the term. Also, note which uses
are not at top level, to see if hBOOL is needed.*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 14 15:10:50 2010 +0200
@@ -345,8 +345,8 @@
>> merge_relevance_overrides))
(add_to_relevance_override [])
val parse_sledgehammer_command =
- (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
- -- Scan.option Parse.nat) #>> sledgehammer_trans
+ (Scan.optional Parse.short_ident runN -- parse_params
+ -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
val parse_sledgehammer_params_command =
parse_params #>> sledgehammer_params_trans
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 14 15:10:50 2010 +0200
@@ -41,12 +41,6 @@
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-(* Hack: Could return false positives (e.g., a user happens to declare a
- constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
- Long_Name.base_name
- #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
val index_in_shape : int -> int list list -> int =
find_index o exists o curry (op =)
fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
@@ -263,9 +257,16 @@
fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
-(*The number of type arguments of a constant, zero if it's monomorphic*)
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+ (instances of) Skolem pseudoconstants, this information is encoded in the
+ constant name. *)
fun num_type_args thy s =
- length (Sign.const_typargs thy (s, Sign.the_const_type thy s))
+ if String.isPrefix skolem_theory_name s then
+ s |> unprefix skolem_theory_name
+ |> space_explode skolem_infix |> hd
+ |> space_explode "_" |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
fun fix_atp_variable_name s =
let
@@ -323,9 +324,12 @@
else
(* Extra args from "hAPP" come after any arguments
given directly to the constant. *)
- Sign.const_instance thy (c,
- map (type_from_node tfrees)
- (drop num_term_args us)))
+ if String.isPrefix skolem_theory_name c then
+ map fastype_of ts ---> HOLogic.typeT
+ else
+ Sign.const_instance thy (c,
+ map (type_from_node tfrees)
+ (drop num_term_args us)))
in list_comb (t, ts) end
| NONE => (* a free or schematic variable *)
let
@@ -580,16 +584,29 @@
| extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
| extract_num _ = NONE
in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
-
-fun apply_command _ 1 = "by "
- | apply_command 1 _ = "apply "
- | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
-fun metis_command i n [] = apply_command i n ^ "metis"
- | metis_command i n ss =
- apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")"
-fun metis_line i n xs =
+
+val indent_size = 2
+val no_label = ("", ~1)
+
+val raw_prefix = "X"
+val assum_prefix = "A"
+val fact_prefix = "F"
+
+fun string_for_label (s, num) = s ^ string_of_int num
+
+fun metis_using [] = ""
+ | metis_using ls =
+ "using " ^ space_implode " " (map string_for_label ls) ^ " "
+fun metis_apply _ 1 = "by "
+ | metis_apply 1 _ = "apply "
+ | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
+fun metis_itself [] = "metis"
+ | metis_itself ss = "(metis " ^ space_implode " " ss ^ ")"
+fun metis_command i n (ls, ss) =
+ metis_using ls ^ metis_apply i n ^ metis_itself ss
+fun metis_line i n ss =
"Try this command: " ^
- Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n"
+ Markup.markup Markup.sendback (metis_command i n ([], ss)) ^ ".\n"
fun minimize_line _ [] = ""
| minimize_line minimize_command facts =
case minimize_command facts of
@@ -639,15 +656,6 @@
fun smart_case_split [] facts = ByMetis facts
| smart_case_split proofs facts = CaseSplit (proofs, facts)
-val indent_size = 2
-val no_label = ("", ~1)
-
-val raw_prefix = "X"
-val assum_prefix = "A"
-val fact_prefix = "F"
-
-fun string_for_label (s, num) = s ^ string_of_int num
-
fun add_fact_from_dep thm_names num =
if is_axiom_clause_number thm_names num then
apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
@@ -948,7 +956,7 @@
let
val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
val ss = ss |> map unprefix_chained |> sort_distinct string_ord
- in metis_command 1 1 (map string_for_label ls @ ss) end
+ in metis_command 1 1 (ls, ss) end
and do_step ind (Fix xs) =
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
| do_step ind (Let (t1, t2)) =
--- a/src/HOL/Tools/meson.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/meson.ML Mon Jun 14 15:10:50 2010 +0200
@@ -9,7 +9,6 @@
sig
val trace: bool Unsynchronized.ref
val term_pair_of: indexname * (typ * 'a) -> term * 'a
- val first_order_resolve: thm -> thm -> thm
val flexflex_first_order: thm -> thm
val size_of_subgoals: thm -> int
val too_many_clauses: Proof.context option -> term -> bool
@@ -98,11 +97,13 @@
let val thy = theory_of_thm thA
val tmA = concl_of thA
val Const("==>",_) $ tmB $ _ = prop_of thB
- val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
+ val tenv =
+ Pattern.first_order_match thy (tmB, tmA)
+ (Vartab.empty, Vartab.empty) |> snd
val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
in thA RS (cterm_instantiate ct_pairs thB) end) () of
SOME th => th
- | NONE => raise THM ("first_order_resolve", 0, [thA, thB]));
+ | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
fun flexflex_first_order th =
case (tpairs_of th) of
@@ -315,15 +316,17 @@
val has_meta_conn =
exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
-fun apply_skolem_ths (th, rls) =
- let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
- | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls)
- in tryall rls end;
+fun apply_skolem_theorem (th, rls) =
+ let
+ fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
+ | tryall (rl :: rls) =
+ first_order_resolve th rl handle THM _ => tryall rls
+ in tryall rls end
-(*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
- Strips universal quantifiers and breaks up conjunctions.
- Eliminates existential quantifiers using skoths: Skolemization theorems.*)
-fun cnf skoths ctxt (th,ths) =
+(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
+ Strips universal quantifiers and breaks up conjunctions.
+ Eliminates existential quantifiers using Skolemization theorems. *)
+fun cnf skolem_ths ctxt (th, ths) =
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
@@ -337,7 +340,7 @@
in ctxtr := ctxt'; cnf_aux (th', ths) end
| Const ("Ex", _) =>
(*existential quantifier: Insert Skolem functions*)
- cnf_aux (apply_skolem_ths (th,skoths), ths)
+ cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
| Const ("op |", _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
@@ -353,7 +356,7 @@
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
-fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
+fun make_cnf skolem_ths th ctxt = cnf skolem_ths ctxt (th, []);
(*Generalization, removal of redundant equalities, removal of tautologies.*)
fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
--- a/src/HOL/Tools/refute.ML Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Tools/refute.ML Mon Jun 14 15:10:50 2010 +0200
@@ -517,7 +517,7 @@
end
(* ------------------------------------------------------------------------- *)
-(* get_def: looks up the definition of a constant, as created by "constdefs" *)
+(* get_def: looks up the definition of a constant *)
(* ------------------------------------------------------------------------- *)
(* theory -> string * Term.typ -> (string * Term.term) option *)
@@ -711,7 +711,7 @@
(* Note: currently we use "inverse" functions to the definitional *)
(* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *)
- (* "typedef", "constdefs". A more general approach could consider *)
+ (* "typedef", "definition". A more general approach could consider *)
(* *every* axiom of the theory and collect it if it has a constant/ *)
(* type/typeclass in common with the term 't'. *)
--- a/src/HOL/Wellfounded.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/Wellfounded.thy Mon Jun 14 15:10:50 2010 +0200
@@ -683,10 +683,8 @@
text{* Lexicographic combinations *}
definition
- lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
- (infixr "<*lex*>" 80)
-where
- "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
+ lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
+ [code del]: "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
apply (unfold wf_def lex_prod_def)
--- a/src/HOL/ex/Codegenerator_Candidates.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Mon Jun 14 15:10:50 2010 +0200
@@ -26,8 +26,6 @@
While_Combinator
begin
-declare lexn.simps [code del]
-
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
empty: "sublist [] xs"
| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
--- a/src/ZF/ZF.thy Mon Jun 14 15:10:36 2010 +0200
+++ b/src/ZF/ZF.thy Mon Jun 14 15:10:50 2010 +0200
@@ -199,10 +199,7 @@
finalconsts
0 Pow Inf Union PrimReplace mem
-defs
-(*don't try to use constdefs: the declaration order is tightly constrained*)
-
- (* Bounded Quantifiers *)
+defs (* Bounded Quantifiers *)
Ball_def: "Ball(A, P) == \<forall>x. x\<in>A --> P(x)"
Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)"