--- a/NEWS Mon Dec 20 10:57:01 2010 -0800
+++ b/NEWS Mon Dec 20 11:11:51 2010 -0800
@@ -603,7 +603,9 @@
*** FOL and ZF ***
-* All constant names are now qualified. INCOMPATIBILITY.
+* All constant names are now qualified internally and use proper
+identifiers, e.g. "IFOL.eq" instead of "op =". INCOMPATIBILITY.
+
*** ML ***
--- a/src/CTT/CTT.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/CTT/CTT.thy Mon Dec 20 11:11:51 2010 -0800
@@ -54,7 +54,7 @@
lambda :: "(i => i) => i" (binder "lam " 10)
app :: "[i,i]=>i" (infixl "`" 60)
(*Natural numbers*)
- "0" :: "i" ("0")
+ Zero :: "i" ("0")
(*Pairing*)
pair :: "[i,i]=>i" ("(1<_,/_>)")
--- a/src/FOL/FOL.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOL/FOL.thy Mon Dec 20 11:11:51 2010 -0800
@@ -175,7 +175,7 @@
(
val thy = @{theory}
type claset = Cla.claset
- val equality_name = @{const_name "op ="}
+ val equality_name = @{const_name eq}
val not_name = @{const_name Not}
val notE = @{thm notE}
val ccontr = @{thm ccontr}
@@ -391,4 +391,7 @@
setup Induct.setup
declare case_split [cases type: o]
+
+hide_const (open) eq
+
end
--- a/src/FOL/IFOL.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOL/IFOL.thy Mon Dec 20 11:11:51 2010 -0800
@@ -42,13 +42,13 @@
(* Connectives *)
- "op =" :: "['a, 'a] => o" (infixl "=" 50)
+ eq :: "['a, 'a] => o" (infixl "=" 50)
Not :: "o => o" ("~ _" [40] 40)
- "op &" :: "[o, o] => o" (infixr "&" 35)
- "op |" :: "[o, o] => o" (infixr "|" 30)
- "op -->" :: "[o, o] => o" (infixr "-->" 25)
- "op <->" :: "[o, o] => o" (infixr "<->" 25)
+ conj :: "[o, o] => o" (infixr "&" 35)
+ disj :: "[o, o] => o" (infixr "|" 30)
+ imp :: "[o, o] => o" (infixr "-->" 25)
+ iff :: "[o, o] => o" (infixr "<->" 25)
(* Quantifiers *)
@@ -69,28 +69,24 @@
notation (xsymbols)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
All (binder "\<forall>" 10) and
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10) and
- "op -->" (infixr "\<longrightarrow>" 25) and
- "op <->" (infixr "\<longleftrightarrow>" 25)
+ imp (infixr "\<longrightarrow>" 25) and
+ iff (infixr "\<longleftrightarrow>" 25)
notation (HTML output)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
All (binder "\<forall>" 10) and
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10)
finalconsts
- False All Ex
- "op ="
- "op &"
- "op |"
- "op -->"
+ False All Ex eq conj disj imp
axioms
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Dec 20 11:11:51 2010 -0800
@@ -156,7 +156,7 @@
end;
*}
-local_setup {* Config.put show_hyps true *}
+declare [[show_hyps]]
ML {*
check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
--- a/src/FOL/ex/Nat.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOL/ex/Nat.thy Mon Dec 20 11:11:51 2010 -0800
@@ -13,7 +13,7 @@
arities nat :: "term"
consts
- 0 :: nat ("0")
+ Zero :: nat ("0")
Suc :: "nat => nat"
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/FOL/ex/ROOT.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOL/ex/ROOT.ML Mon Dec 20 11:11:51 2010 -0800
@@ -1,8 +1,3 @@
-(* Title: FOL/ex/ROOT.ML
-
-Examples for First-Order Logic.
-*)
-
use_thys [
"First_Order_Logic",
"Natural_Numbers",
@@ -21,5 +16,4 @@
"If"
];
-(*regression test for locales -- sets several global flags!*)
no_document use_thy "Locale_Test/Locale_Test";
--- a/src/FOL/fologic.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOL/fologic.ML Mon Dec 20 11:11:51 2010 -0800
@@ -50,29 +50,29 @@
(* Logical constants *)
val not = Const (@{const_name Not}, oT --> oT);
-val conj = Const(@{const_name "op &"}, [oT,oT]--->oT);
-val disj = Const(@{const_name "op |"}, [oT,oT]--->oT);
-val imp = Const(@{const_name "op -->"}, [oT,oT]--->oT)
-val iff = Const(@{const_name "op <->"}, [oT,oT]--->oT);
+val conj = Const(@{const_name conj}, [oT,oT]--->oT);
+val disj = Const(@{const_name disj}, [oT,oT]--->oT);
+val imp = Const(@{const_name imp}, [oT,oT]--->oT)
+val iff = Const(@{const_name iff}, [oT,oT]--->oT);
fun mk_conj (t1, t2) = conj $ t1 $ t2
and mk_disj (t1, t2) = disj $ t1 $ t2
and mk_imp (t1, t2) = imp $ t1 $ t2
and mk_iff (t1, t2) = iff $ t1 $ t2;
-fun dest_imp (Const(@{const_name "op -->"},_) $ A $ B) = (A, B)
+fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
-fun dest_conj (Const (@{const_name "op &"}, _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
-fun dest_iff (Const(@{const_name "op <->"},_) $ A $ B) = (A, B)
+fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
| dest_iff t = raise TERM ("dest_iff", [t]);
-fun eq_const T = Const (@{const_name "op ="}, [T, T] ---> oT);
+fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const (@{const_name "op ="}, _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
--- a/src/FOL/simpdata.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOL/simpdata.ML Mon Dec 20 11:11:51 2010 -0800
@@ -8,15 +8,15 @@
(*Make meta-equalities. The operator below is Trueprop*)
fun mk_meta_eq th = case concl_of th of
- _ $ (Const(@{const_name "op ="},_)$_$_) => th RS @{thm eq_reflection}
- | _ $ (Const(@{const_name "op <->"},_)$_$_) => th RS @{thm iff_reflection}
+ _ $ (Const(@{const_name eq},_)$_$_) => th RS @{thm eq_reflection}
+ | _ $ (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
| _ =>
error("conclusion must be a =-equality or <->");;
fun mk_eq th = case concl_of th of
Const("==",_)$_$_ => th
- | _ $ (Const(@{const_name "op ="},_)$_$_) => mk_meta_eq th
- | _ $ (Const(@{const_name "op <->"},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name eq},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
| _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T};
@@ -32,7 +32,7 @@
error("Premises and conclusion of congruence rules must use =-equality or <->");
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]), (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name imp}, [@{thm mp}]), (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name All}, [@{thm spec}]), (@{const_name True}, []), (@{const_name False}, [])];
fun mk_atomize pairs =
@@ -55,11 +55,11 @@
structure Quantifier1 = Quantifier1Fun(
struct
(*abstract syntax*)
- fun dest_eq((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_eq((c as Const(@{const_name eq},_)) $ s $ t) = SOME(c,s,t)
| dest_eq _ = NONE;
- fun dest_conj((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_conj((c as Const(@{const_name conj},_)) $ s $ t) = SOME(c,s,t)
| dest_conj _ = NONE;
- fun dest_imp((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_imp((c as Const(@{const_name imp},_)) $ s $ t) = SOME(c,s,t)
| dest_imp _ = NONE;
val conj = FOLogic.conj
val imp = FOLogic.imp
--- a/src/FOLP/IFOLP.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOLP/IFOLP.thy Mon Dec 20 11:11:51 2010 -0800
@@ -24,14 +24,14 @@
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5)
(*** Logical Connectives -- Type Formers ***)
- "op =" :: "['a,'a] => o" (infixl "=" 50)
+ eq :: "['a,'a] => o" (infixl "=" 50)
True :: "o"
False :: "o"
Not :: "o => o" ("~ _" [40] 40)
- "op &" :: "[o,o] => o" (infixr "&" 35)
- "op |" :: "[o,o] => o" (infixr "|" 30)
- "op -->" :: "[o,o] => o" (infixr "-->" 25)
- "op <->" :: "[o,o] => o" (infixr "<->" 25)
+ conj :: "[o,o] => o" (infixr "&" 35)
+ disj :: "[o,o] => o" (infixr "|" 30)
+ imp :: "[o,o] => o" (infixr "-->" 25)
+ iff :: "[o,o] => o" (infixr "<->" 25)
(*Quantifiers*)
All :: "('a => o) => o" (binder "ALL " 10)
Ex :: "('a => o) => o" (binder "EX " 10)
@@ -51,9 +51,9 @@
inr :: "p=>p"
when :: "[p, p=>p, p=>p]=>p"
lambda :: "(p => p) => p" (binder "lam " 55)
- "op `" :: "[p,p]=>p" (infixl "`" 60)
+ App :: "[p,p]=>p" (infixl "`" 60)
alll :: "['a=>p]=>p" (binder "all " 55)
- "op ^" :: "[p,'a]=>p" (infixl "^" 55)
+ app :: "[p,'a]=>p" (infixl "^" 55)
exists :: "['a,p]=>p" ("(1[_,/_])")
xsplit :: "[p,['a,p]=>p]=>p"
ideq :: "'a=>p"
@@ -595,7 +595,7 @@
struct
(*Take apart an equality judgement; otherwise raise Match!*)
fun dest_eq (Const (@{const_name Proof}, _) $
- (Const (@{const_name "op ="}, _) $ t $ u) $ _) = (t, u);
+ (Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u);
val imp_intr = @{thm impI}
--- a/src/FOLP/ex/Nat.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOLP/ex/Nat.thy Mon Dec 20 11:11:51 2010 -0800
@@ -13,7 +13,7 @@
arities nat :: "term"
consts
- 0 :: nat ("0")
+ Zero :: nat ("0")
Suc :: "nat => nat"
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/FOLP/simpdata.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/FOLP/simpdata.ML Mon Dec 20 11:11:51 2010 -0800
@@ -17,15 +17,15 @@
(* Conversion into rewrite rules *)
fun mk_eq th = case concl_of th of
- _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
- | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
+ _ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th
+ | _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th
| _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
| _ => make_iff_T th;
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name imp}, [@{thm mp}]),
+ (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name "All"}, [@{thm spec}]),
(@{const_name True}, []),
(@{const_name False}, [])];
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy Mon Dec 20 11:11:51 2010 -0800
@@ -13,7 +13,7 @@
consts
- "{|}" :: "'a multiset" ("{|}")
+ emptym :: "'a multiset" ("{|}")
addm :: "['a multiset, 'a] => 'a multiset"
delm :: "['a multiset, 'a] => 'a multiset"
countm :: "['a multiset, 'a => bool] => nat"
--- a/src/HOL/Library/Sum_Of_Squares/etc/settings Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Library/Sum_Of_Squares/etc/settings Mon Dec 20 11:11:51 2010 -0800
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_SUM_OF_SQUARES="$COMPONENT"
--- a/src/HOL/Mirabelle/etc/settings Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Mirabelle/etc/settings Mon Dec 20 11:11:51 2010 -0800
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
MIRABELLE_HOME="$COMPONENT"
MIRABELLE_LOGIC=HOL
@@ -5,4 +7,4 @@
MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
MIRABELLE_TIMEOUT=30
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/etc/settings Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Mutabelle/etc/settings Mon Dec 20 11:11:51 2010 -0800
@@ -1,7 +1,9 @@
+# -*- shell-script -*- :mode=shellscript:
+
MUTABELLE_HOME="$COMPONENT"
DEFAULT_MUTABELLE_LOGIC=HOL
DEFAULT_MUTABELLE_IMPORT_THEORY=Complex_Main
DEFAULT_MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Mon Dec 20 11:11:51 2010 -0800
@@ -2,7 +2,7 @@
#
# Author: Lukas Bulwahn
#
-# DESCRIPTION: mutant-testing tool for counterexample generators and automated proof tools
+# DESCRIPTION: mutant-testing for counterexample generators and automated tools
PRG="$(basename "$0")"
@@ -16,7 +16,8 @@
echo " -T THEORY parent theory to use (default $DEFAULT_MUTABELLE_IMPORT_THEORY)"
echo " -O DIR output directory for test data (default $DEFAULT_MUTABELLE_OUTPUT_PATH)"
echo
- echo " THEORY is the name of the theory of which all theorems should be mutated and tested"
+ echo " THEORY is the name of the theory of which all theorems should be"
+ echo " mutated and tested."
echo
exit 1
}
--- a/src/HOL/Predicate.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Predicate.thy Mon Dec 20 11:11:51 2010 -0800
@@ -788,6 +788,17 @@
unfolding is_empty_def holds_eq
by (rule unit_pred_cases) (auto elim: botE intro: singleI)
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
+ "map f P = P \<guillemotright>= (single o f)"
+
+lemma eval_map [simp]:
+ "eval (map f P) = image f (eval P)"
+ by (auto simp add: map_def)
+
+type_lifting map
+ by (auto intro!: pred_eqI simp add: image_image)
+
+
subsubsection {* Implementation *}
datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
@@ -925,9 +936,6 @@
lemma eq_is_eq: "eq x y \<equiv> (x = y)"
by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
- "map f P = P \<guillemotright>= (single o f)"
-
primrec null :: "'a seq \<Rightarrow> bool" where
"null Empty \<longleftrightarrow> True"
| "null (Insert x P) \<longleftrightarrow> False"
--- a/src/HOL/Prolog/Test.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Prolog/Test.thy Mon Dec 20 11:11:51 2010 -0800
@@ -37,9 +37,9 @@
sue :: person
ned :: person
- "23" :: nat ("23")
- "24" :: nat ("24")
- "25" :: nat ("25")
+ nat23 :: nat ("23")
+ nat24 :: nat ("24")
+ nat25 :: nat ("25")
age :: "[person, nat] => bool"
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Dec 20 11:11:51 2010 -0800
@@ -12,7 +12,7 @@
type atp_config =
{exec: string * string,
required_execs: (string * string) list,
- arguments: bool -> Time.time -> string,
+ arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
@@ -20,6 +20,11 @@
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
+ (* for experimentation purposes -- do not use in production code *)
+ val e_generate_weights : bool Unsynchronized.ref
+ val e_weight_factor : real Unsynchronized.ref
+ val e_default_weight : real Unsynchronized.ref
+
val eN : string
val spassN : string
val vampireN : string
@@ -44,7 +49,7 @@
type atp_config =
{exec: string * string,
required_execs: (string * string) list,
- arguments: bool -> Time.time -> string,
+ arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
@@ -94,12 +99,35 @@
val tstp_proof_delims =
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
+val e_generate_weights = Unsynchronized.ref false
+val e_weight_factor = Unsynchronized.ref 60.0
+val e_default_weight = Unsynchronized.ref 0.5
+
+fun e_weights weights =
+ if !e_generate_weights then
+ "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
+ \--destructive-er-aggressive --destructive-er --presat-simplify \
+ \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
+ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
+ \-H'(4*FunWeight(SimulateSOS, " ^
+ string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^
+ ",20,1.5,1.5,1" ^
+ (weights ()
+ |> map (fn (s, w) => "," ^ s ^ ":" ^
+ string_of_int (Real.ceil (w * !e_weight_factor)))
+ |> implode) ^
+ "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
+ \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
+ \FIFOWeight(PreferProcessed))'"
+ else
+ "-xAutoDev"
+
val e_config : atp_config =
{exec = ("E_HOME", "eproof"),
required_execs = [],
- arguments = fn _ => fn timeout =>
- "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
- \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
+ arguments = fn _ => fn timeout => fn weights =>
+ "--tstp-in --tstp-out -l5 " ^ e_weights weights ^ " -tAutoDev \
+ \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
has_incomplete_mode = false,
proof_delims = [tstp_proof_delims],
known_failures =
@@ -125,7 +153,7 @@
val spass_config : atp_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
- arguments = fn complete => fn timeout =>
+ arguments = fn complete => fn timeout => fn _ =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
|> not complete ? prefix "-SOS=1 ",
@@ -152,7 +180,7 @@
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
- arguments = fn complete => fn timeout =>
+ arguments = fn complete => fn timeout => fn _ =>
(* This would work too but it's less tested: "--proof tptp " ^ *)
"--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
" --thanks \"Andrei and Krystof\" --input_file"
@@ -214,7 +242,7 @@
: atp_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
- arguments = fn _ => fn timeout =>
+ arguments = fn _ => fn timeout => fn _ =>
" -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
^ " -s " ^ the_system system_name system_versions,
has_incomplete_mode = false,
--- a/src/HOL/Tools/ATP/etc/settings Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/ATP/etc/settings Mon Dec 20 11:11:51 2010 -0800
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_ATP="$COMPONENT"
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Dec 20 11:11:51 2010 -0800
@@ -857,8 +857,9 @@
val args' = map (rename_vars_term renaming) args
val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
val _ = tracing ("Generated prolog program:\n" ^ prog)
- val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
- (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
+ val solution = TimeLimit.timeLimit timeout (fn prog =>
+ Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
+ (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
val tss = parse_solutions solution
in
--- a/src/HOL/Tools/Predicate_Compile/etc/settings Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/etc/settings Mon Dec 20 11:11:51 2010 -0800
@@ -1,5 +1,8 @@
# -*- shell-script -*- :mode=shellscript:
+# FIXME contrib_devel not official
+# FIXME $(type -p swipl) etc. does not allow spaces in file name
+
EXEC_SWIPL="$(choosefrom \
"$ISABELLE_HOME/contrib/swipl/$ISABELLE_PLATFORM/bin/swipl" \
"$ISABELLE_HOME/contrib_devel/swipl/$ISABELLE_PLATFORM/bin/swipl" \
--- a/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Mon Dec 20 11:11:51 2010 -0800
@@ -7,6 +7,9 @@
if [ "$EXEC_SWIPL" = "" ]; then
echo ""
else
+ # FIXME does not allow spaces in $EXEC_SWIPL
+ # FIXME "expr match" not portable
+ # FIXME prefer $(...) in bash
VERSION=`$EXEC_SWIPL --version`
echo `expr match "$VERSION" 'SWI-Prolog version \([0-9\.]*\)'`
fi
--- a/src/HOL/Tools/SMT/etc/settings Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/SMT/etc/settings Mon Dec 20 11:11:51 2010 -0800
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_SMT="$COMPONENT"
REMOTE_SMT="$ISABELLE_SMT/lib/scripts/remote_smt"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Dec 20 11:11:51 2010 -0800
@@ -29,6 +29,7 @@
Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
-> (translated_formula option * ((string * 'a) * thm)) list
-> string problem * string Symtab.table * int * (string * 'a) list vector
+ val atp_problem_weights : string problem -> (string * real) list
end;
structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
@@ -253,13 +254,15 @@
(** Helper facts **)
+fun fold_formula f (AQuant (_, _, phi)) = fold_formula f phi
+ | fold_formula f (AConn (_, phis)) = fold (fold_formula f) phis
+ | fold_formula f (AAtom tm) = f tm
+
fun count_term (ATerm ((s, _), tms)) =
(if is_atp_variable s then I
else Symtab.map_entry s (Integer.add 1))
#> fold count_term tms
-fun count_formula (AQuant (_, _, phi)) = count_formula phi
- | count_formula (AConn (_, phis)) = fold count_formula phis
- | count_formula (AAtom tm) = count_term tm
+val count_formula = fold_formula count_term
val init_counters =
metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)
@@ -316,14 +319,13 @@
val supers = tvar_classes_of_terms fact_ts
val tycons = type_consts_of_terms thy (goal_t :: fact_ts)
(* TFrees in the conjecture; TVars in the facts *)
- val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
+ val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
val (supers', arity_clauses) =
if type_sys = No_Types then ([], [])
else make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in
- (fact_names |> map single,
- (conjectures, facts, class_rel_clauses, arity_clauses))
+ (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
end
fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t])
@@ -473,9 +475,9 @@
fun problem_line_for_free_type j lit =
Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
-fun problem_lines_for_free_types type_sys conjectures =
+fun problem_lines_for_free_types type_sys conjs =
let
- val litss = map (free_type_literals_for_conjecture type_sys) conjectures
+ val litss = map (free_type_literals_for_conjecture type_sys) conjs
val lits = fold (union (op =)) litss []
in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
@@ -602,7 +604,7 @@
val aritiesN = "Arity declarations"
val helpersN = "Helper facts"
val conjsN = "Conjectures"
-val tfreesN = "Type variables"
+val free_typesN = "Type variables"
fun offset_of_heading_in_problem _ [] j = j
| offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
@@ -613,7 +615,7 @@
explicit_apply hyp_ts concl_t facts =
let
val thy = ProofContext.theory_of ctxt
- val (fact_names, (conjectures, facts, class_rel_clauses, arity_clauses)) =
+ val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt type_sys hyp_ts concl_t facts
(* Reordering these might or might not confuse the proof reconstruction
code or the SPASS Flotter hack. *)
@@ -622,8 +624,8 @@
(class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map problem_line_for_arity_clause arity_clauses),
(helpersN, []),
- (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjectures),
- (tfreesN, problem_lines_for_free_types type_sys conjectures)]
+ (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
+ (free_typesN, problem_lines_for_free_types type_sys conjs)]
val const_tab = const_table_for_problem explicit_apply problem
val problem =
problem |> repair_problem thy explicit_forall type_sys const_tab
@@ -643,4 +645,42 @@
fact_names |> Vector.fromList)
end
+(* FUDGE *)
+val conj_weight = 0.0
+val hyp_weight = 0.05
+val fact_min_weight = 0.1
+val fact_max_weight = 1.0
+
+fun add_term_weights weight (ATerm (s, tms)) =
+ (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
+ #> fold (add_term_weights weight) tms
+val add_formula_weights = fold_formula o add_term_weights
+fun add_problem_line_weights weight (Fof (_, _, phi)) =
+ add_formula_weights weight phi
+
+fun add_conjectures_weights [] = I
+ | add_conjectures_weights conjs =
+ let val (hyps, conj) = split_last conjs in
+ add_problem_line_weights conj_weight conj
+ #> fold (add_problem_line_weights hyp_weight) hyps
+ end
+
+fun add_facts_weights facts =
+ let
+ val num_facts = length facts
+ fun weight_of j =
+ fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
+ / Real.fromInt num_facts
+ in
+ map weight_of (0 upto num_facts - 1) ~~ facts
+ |> fold (uncurry add_problem_line_weights)
+ end
+
+(* Weights are from 0.0 (most important) to 1.0 (least important). *)
+fun atp_problem_weights problem =
+ Symtab.empty
+ |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
+ |> add_facts_weights (these (AList.lookup (op =) problem factsN))
+ |> Symtab.dest
+
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 20 11:11:51 2010 -0800
@@ -53,6 +53,8 @@
type prover = params -> minimize_command -> prover_problem -> prover_result
(* for experimentation purposes -- do not use in production code *)
+ val atp_run_twice_threshold : int Unsynchronized.ref
+ val atp_first_iter_time_frac : real Unsynchronized.ref
val smt_weights : bool Unsynchronized.ref
val smt_weight_min_facts : int Unsynchronized.ref
val smt_min_weight : int Unsynchronized.ref
@@ -318,15 +320,17 @@
| smt_weighted_fact thy num_facts (fact, j) =
(untranslated_fact fact, j) |> weight_smt_fact thy num_facts
+fun overlord_file_location_for_prover prover =
+ (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
+
+
(* generic TPTP-based ATPs *)
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
| int_opt_add _ _ = NONE
-fun overlord_file_location_for_prover prover =
- (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
-
-val atp_first_iter_time_frac = 0.67
+val atp_run_twice_threshold = Unsynchronized.ref 50
+val atp_first_iter_time_frac = Unsynchronized.ref 0.67
(* Important messages are important but not so important that users want to see
them each time. *)
@@ -358,15 +362,6 @@
error ("No such directory: " ^ quote dest_dir ^ ".")
val measure_run_time = verbose orelse Config.get ctxt measure_run_time
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
- (* write out problem file and call ATP *)
- fun command_line complete timeout probfile =
- let
- val core = File.shell_path command ^ " " ^ arguments complete timeout ^
- " " ^ File.shell_path probfile
- in
- (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
- else "exec " ^ core) ^ " 2>&1"
- end
fun split_time s =
let
val split = String.tokens (fn c => str c = "\n");
@@ -378,16 +373,35 @@
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
val as_time = Scan.read Symbol.stopper time o raw_explode
in (output, as_time t) end;
- fun run_on probfile =
+ fun run_on prob_file =
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
(home_var, _) :: _ =>
error ("The environment variable " ^ quote home_var ^ " is not set.")
| [] =>
if File.exists command then
let
+ val readable_names = debug andalso overlord
+ val (atp_problem, pool, conjecture_offset, fact_names) =
+ prepare_atp_problem ctxt readable_names explicit_forall type_sys
+ explicit_apply hyp_ts concl_t facts
+ val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
+ atp_problem
+ val _ = File.write_list prob_file ss
+ val conjecture_shape =
+ conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
+ |> map single
fun run complete timeout =
let
- val command = command_line complete timeout probfile
+ fun weights () = atp_problem_weights atp_problem
+ val core =
+ File.shell_path command ^ " " ^
+ arguments complete timeout weights ^ " " ^
+ File.shell_path prob_file
+ val command =
+ (if measure_run_time then
+ "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
+ else
+ "exec " ^ core) ^ " 2>&1"
val ((output, msecs), res_code) =
bash_output command
|>> (if overlord then
@@ -399,22 +413,14 @@
extract_tstplike_proof_and_outcome verbose complete res_code
proof_delims known_failures output
in (output, msecs, tstplike_proof, outcome) end
- val readable_names = debug andalso overlord
- val (atp_problem, pool, conjecture_offset, fact_names) =
- prepare_atp_problem ctxt readable_names explicit_forall type_sys
- explicit_apply hyp_ts concl_t facts
- val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
- atp_problem
- val _ = File.write_list probfile ss
- val conjecture_shape =
- conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
- |> map single
- val run_twice = has_incomplete_mode andalso not auto
+ val run_twice =
+ has_incomplete_mode andalso not auto andalso
+ length facts >= !atp_run_twice_threshold
val timer = Timer.startRealTimer ()
val result =
- run false
+ run (not run_twice)
(if run_twice then
- seconds (0.001 * atp_first_iter_time_frac
+ seconds (0.001 * !atp_first_iter_time_frac
* Real.fromInt (Time.toMilliseconds timeout))
else
timeout)
@@ -431,13 +437,13 @@
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
- fun cleanup probfile =
- if dest_dir = "" then try File.rm probfile else NONE
- fun export probfile (_, (output, _, _, _)) =
+ fun cleanup prob_file =
+ if dest_dir = "" then try File.rm prob_file else NONE
+ fun export prob_file (_, (output, _, _, _)) =
if dest_dir = "" then
()
else
- File.write (Path.explode (Path.implode probfile ^ "_proof")) output
+ File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
val ((pool, conjecture_shape, fact_names),
(output, msecs, tstplike_proof, outcome)) =
with_path cleanup export run_on problem_path_name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 20 11:11:51 2010 -0800
@@ -254,7 +254,8 @@
val facts = get_facts "SMT solver" true smt_relevance_fudge smts
val weight = SMT_Weighted_Fact oo weight_smt_fact thy
fun smt_head facts =
- try (SMT_Solver.smt_filter_head state (facts ()))
+ (if debug then curry (op o) SOME else try)
+ (SMT_Solver.smt_filter_head state (facts ()))
in
smts |> map (`(class_of_smt_solver ctxt))
|> AList.group (op =)
--- a/src/LCF/LCF.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/LCF/LCF.thy Mon Dec 20 11:11:51 2010 -0800
@@ -18,13 +18,13 @@
typedecl tr
typedecl void
-typedecl ('a,'b) "*" (infixl "*" 6)
-typedecl ('a,'b) "+" (infixl "+" 5)
+typedecl ('a,'b) prod (infixl "*" 6)
+typedecl ('a,'b) sum (infixl "+" 5)
arities
"fun" :: (cpo, cpo) cpo
- "*" :: (cpo, cpo) cpo
- "+" :: (cpo, cpo) cpo
+ prod :: (cpo, cpo) cpo
+ sum :: (cpo, cpo) cpo
tr :: cpo
void :: cpo
--- a/src/Pure/System/isabelle_system.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/Pure/System/isabelle_system.ML Mon Dec 20 11:11:51 2010 -0800
@@ -7,10 +7,11 @@
signature ISABELLE_SYSTEM =
sig
val isabelle_tool: string -> string -> int
- val rm_tree: Path.T -> unit
val mkdirs: Path.T -> unit
val mkdir: Path.T -> unit
val copy_dir: Path.T -> Path.T -> unit
+ val with_tmp_file: string -> (Path.T -> 'a) -> 'a
+ val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
end;
structure Isabelle_System: ISABELLE_SYSTEM =
@@ -37,8 +38,6 @@
(* directory operations *)
-fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
-
fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
fun mkdir path =
@@ -48,5 +47,33 @@
if File.eq (src, dst) then ()
else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
+
+(* unique tmp files *)
+
+local
+
+fun fresh_path name =
+ let
+ val path = File.tmp_path (Path.basic (name ^ serial_string ()));
+ val _ = File.exists path andalso
+ raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
+ in path end;
+
+fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
+
+in
+
+fun with_tmp_file name f =
+ let val path = fresh_path name
+ in Exn.release (Exn.capture f path before try File.rm path) end;
+
+fun with_tmp_dir name f =
+ let
+ val path = fresh_path name;
+ val _ = mkdirs path;
+ in Exn.release (Exn.capture f path before try rm_tree path) end;
+
end;
+end;
+
--- a/src/Sequents/LK/Nat.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/Sequents/LK/Nat.thy Mon Dec 20 11:11:51 2010 -0800
@@ -11,7 +11,7 @@
typedecl nat
arities nat :: "term"
-consts "0" :: nat ("0")
+consts Zero :: nat ("0")
Suc :: "nat=>nat"
rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/Tools/Code/code_target.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/Tools/Code/code_target.ML Mon Dec 20 11:11:51 2010 -0800
@@ -397,7 +397,7 @@
then if strict
then error (env_var ^ " not set; cannot check code for " ^ target)
else warning (env_var ^ " not set; skipped checking code for " ^ target)
- else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
+ else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
end;
end; (* local *)
--- a/src/Tools/WWW_Find/etc/settings Mon Dec 20 10:57:01 2010 -0800
+++ b/src/Tools/WWW_Find/etc/settings Mon Dec 20 11:11:51 2010 -0800
@@ -1,7 +1,8 @@
-# the path to lighttpd
+# -*- shell-script -*- :mode=shellscript:
+
LIGHTTPD="/usr/sbin/lighttpd"
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-
WWWFINDDIR="$COMPONENT"
WWWCONFIG="$WWWFINDDIR/lighttpd.conf"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$WWWFINDDIR/lib/Tools"
--- a/src/Tools/cache_io.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/Tools/cache_io.ML Mon Dec 20 11:11:51 2010 -0800
@@ -7,8 +7,6 @@
signature CACHE_IO =
sig
(*IO wrapper*)
- val with_tmp_file: string -> (Path.T -> 'a) -> 'a
- val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
type result = {
output: string list,
redirected_output: string list,
@@ -34,21 +32,6 @@
val cache_io_prefix = "cache-io-"
-fun with_tmp_file name f =
- let
- val path = File.tmp_path (Path.explode (name ^ serial_string ()))
- val x = Exn.capture f path
- val _ = try File.rm path
- in Exn.release x end
-
-fun with_tmp_dir name f =
- let
- val path = File.tmp_path (Path.explode (name ^ serial_string ()))
- val _ = Isabelle_System.mkdirs path
- val x = Exn.capture f path
- val _ = try Isabelle_System.rm_tree path
- in Exn.release x end
-
type result = {
output: string list,
redirected_output: string list,
@@ -62,8 +45,9 @@
in {output=split_lines out2, redirected_output=out1, return_code=rc} end
fun run make_cmd str =
- with_tmp_file cache_io_prefix (fn in_path =>
- with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
+ Isabelle_System.with_tmp_file cache_io_prefix (fn in_path =>
+ Isabelle_System.with_tmp_file cache_io_prefix (fn out_path =>
+ raw_run make_cmd str in_path out_path))
(* cache *)
--- a/src/ZF/Tools/datatype_package.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/ZF/Tools/datatype_package.ML Mon Dec 20 11:11:51 2010 -0800
@@ -91,7 +91,7 @@
(** Define the constructors **)
(*The empty tuple is 0*)
- fun mk_tuple [] = @{const "0"}
+ fun mk_tuple [] = @{const zero}
| mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
fun mk_inject n k u = Balanced_Tree.access
--- a/src/ZF/Tools/induct_tacs.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/ZF/Tools/induct_tacs.ML Mon Dec 20 11:11:51 2010 -0800
@@ -118,7 +118,7 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
(*analyze the LHS of a case equation to get a constructor*)
- fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
+ fun const_of (Const(@{const_name IFOL.eq}, _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
Syntax.string_of_term_global thy eqn);
--- a/src/ZF/Tools/numeral_syntax.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/ZF/Tools/numeral_syntax.ML Mon Dec 20 11:11:51 2010 -0800
@@ -19,12 +19,12 @@
(* bits *)
-fun mk_bit 0 = Syntax.const @{const_syntax "0"}
- | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
+fun mk_bit 0 = Syntax.const @{const_syntax zero}
+ | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax zero}
| mk_bit _ = raise Fail "mk_bit";
-fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
- | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax zero}, _)) = 0
+ | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax zero}, _)) = 1
| dest_bit _ = raise Match;
--- a/src/ZF/Tools/primrec_package.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/ZF/Tools/primrec_package.ML Mon Dec 20 11:11:51 2010 -0800
@@ -115,8 +115,8 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const (@{const_name 0}, Ind_Syntax.iT),
- #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
+ (Const (@{const_name zero}, Ind_Syntax.iT),
+ #2 recursor_pair, Const (@{const_name zero}, Ind_Syntax.iT)))
| SOME (rhs, cargs', eq) =>
(rhs, inst_recursor (recursor_pair, cargs'), eq)
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
--- a/src/ZF/ZF.thy Mon Dec 20 10:57:01 2010 -0800
+++ b/src/ZF/ZF.thy Mon Dec 20 11:11:51 2010 -0800
@@ -17,7 +17,7 @@
consts
- "0" :: "i" ("0") --{*the empty set*}
+ zero :: "i" ("0") --{*the empty set*}
Pow :: "i => i" --{*power sets*}
Inf :: "i" --{*infinite set*}
--- a/src/ZF/arith_data.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/ZF/arith_data.ML Mon Dec 20 11:11:51 2010 -0800
@@ -24,7 +24,7 @@
val iT = Ind_Syntax.iT;
-val zero = Const(@{const_name 0}, iT);
+val zero = Const(@{const_name zero}, iT);
val succ = Const(@{const_name succ}, iT --> iT);
fun mk_succ t = succ $ t;
val one = mk_succ zero;
@@ -44,7 +44,7 @@
(* dest_sum *)
-fun dest_sum (Const(@{const_name 0},_)) = []
+fun dest_sum (Const(@{const_name zero},_)) = []
| dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t
| dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u
| dest_sum tm = [tm];
--- a/src/ZF/ind_syntax.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/ZF/ind_syntax.ML Mon Dec 20 11:11:51 2010 -0800
@@ -29,7 +29,7 @@
fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
(*simple error-checking in the premises of an inductive definition*)
-fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) =
+fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =
error"Premises may not be conjuctive"
| chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
@@ -96,7 +96,7 @@
let val (_,args) = strip_comb rec_tm
fun is_ind arg = (type_of arg = iT)
in case filter is_ind (args @ cs) of
- [] => @{const 0}
+ [] => @{const zero}
| u_args => Balanced_Tree.make mk_Un u_args
end;
--- a/src/ZF/simpdata.ML Mon Dec 20 10:57:01 2010 -0800
+++ b/src/ZF/simpdata.ML Mon Dec 20 11:11:51 2010 -0800
@@ -32,8 +32,8 @@
val ZF_conn_pairs =
[(@{const_name Ball}, [@{thm bspec}]),
(@{const_name All}, [@{thm spec}]),
- (@{const_name "op -->"}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
+ (@{const_name imp}, [@{thm mp}]),
+ (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}])];
(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =