# HG changeset patch # User huffman # Date 1292872311 28800 # Node ID 874dbac157ee50349e99ce9aa52b4d642774e342 # Parent b27e5c9f5c10ba732a68271d87f8576eb0cfe258# Parent 33e1077885958c4dbf735b0745be39d0726ba822 merged diff -r b27e5c9f5c10 -r 874dbac157ee NEWS --- 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 *** diff -r b27e5c9f5c10 -r 874dbac157ee src/CTT/CTT.thy --- 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<_,/_>)") diff -r b27e5c9f5c10 -r 874dbac157ee src/FOL/FOL.thy --- 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 diff -r b27e5c9f5c10 -r 874dbac157ee src/FOL/IFOL.thy --- 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 ("\ _" [40] 40) and - "op &" (infixr "\" 35) and - "op |" (infixr "\" 30) and + conj (infixr "\" 35) and + disj (infixr "\" 30) and All (binder "\" 10) and Ex (binder "\" 10) and Ex1 (binder "\!" 10) and - "op -->" (infixr "\" 25) and - "op <->" (infixr "\" 25) + imp (infixr "\" 25) and + iff (infixr "\" 25) notation (HTML output) Not ("\ _" [40] 40) and - "op &" (infixr "\" 35) and - "op |" (infixr "\" 30) and + conj (infixr "\" 35) and + disj (infixr "\" 30) and All (binder "\" 10) and Ex (binder "\" 10) and Ex1 (binder "\!" 10) finalconsts - False All Ex - "op =" - "op &" - "op |" - "op -->" + False All Ex eq conj disj imp axioms diff -r b27e5c9f5c10 -r 874dbac157ee src/FOL/ex/Locale_Test/Locale_Test1.thy --- 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))"; diff -r b27e5c9f5c10 -r 874dbac157ee src/FOL/ex/Nat.thy --- 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) diff -r b27e5c9f5c10 -r 874dbac157ee src/FOL/ex/ROOT.ML --- 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"; diff -r b27e5c9f5c10 -r 874dbac157ee src/FOL/fologic.ML --- 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); diff -r b27e5c9f5c10 -r 874dbac157ee src/FOL/simpdata.ML --- 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 diff -r b27e5c9f5c10 -r 874dbac157ee src/FOLP/IFOLP.thy --- 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} diff -r b27e5c9f5c10 -r 874dbac157ee src/FOLP/ex/Nat.thy --- 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) diff -r b27e5c9f5c10 -r 874dbac157ee src/FOLP/simpdata.ML --- 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}, [])]; diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/HOLCF/IOA/NTP/Multiset.thy --- 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" diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Library/Sum_Of_Squares/etc/settings --- 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" diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Mirabelle/etc/settings --- 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" diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Mutabelle/etc/settings --- 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" diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Mutabelle/lib/Tools/mutabelle --- 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 } diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Predicate.thy --- 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 \ 'b) \ 'a pred \ 'b pred" where + "map f P = P \= (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 \ (x = y)" by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) -definition map :: "('a \ 'b) \ 'a pred \ 'b pred" where - "map f P = P \= (single o f)" - primrec null :: "'a seq \ bool" where "null Empty \ True" | "null (Insert x P) \ False" diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Prolog/Test.thy --- 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" diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/ATP/atp_systems.ML --- 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, diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/ATP/etc/settings --- 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" diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/Predicate_Compile/etc/settings --- 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" \ diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version --- 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 diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/SMT/etc/settings --- 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" diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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; diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r b27e5c9f5c10 -r 874dbac157ee src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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 =) diff -r b27e5c9f5c10 -r 874dbac157ee src/LCF/LCF.thy --- 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 diff -r b27e5c9f5c10 -r 874dbac157ee src/Pure/System/isabelle_system.ML --- 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; + diff -r b27e5c9f5c10 -r 874dbac157ee src/Sequents/LK/Nat.thy --- 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) diff -r b27e5c9f5c10 -r 874dbac157ee src/Tools/Code/code_target.ML --- 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 *) diff -r b27e5c9f5c10 -r 874dbac157ee src/Tools/WWW_Find/etc/settings --- 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" diff -r b27e5c9f5c10 -r 874dbac157ee src/Tools/cache_io.ML --- 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 *) diff -r b27e5c9f5c10 -r 874dbac157ee src/ZF/Tools/datatype_package.ML --- 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 diff -r b27e5c9f5c10 -r 874dbac157ee src/ZF/Tools/induct_tacs.ML --- 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); diff -r b27e5c9f5c10 -r 874dbac157ee src/ZF/Tools/numeral_syntax.ML --- 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; diff -r b27e5c9f5c10 -r 874dbac157ee src/ZF/Tools/primrec_package.ML --- 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)) diff -r b27e5c9f5c10 -r 874dbac157ee src/ZF/ZF.thy --- 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*} diff -r b27e5c9f5c10 -r 874dbac157ee src/ZF/arith_data.ML --- 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]; diff -r b27e5c9f5c10 -r 874dbac157ee src/ZF/ind_syntax.ML --- 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; diff -r b27e5c9f5c10 -r 874dbac157ee src/ZF/simpdata.ML --- 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 =