# HG changeset patch # User bulwahn # Date 1267174140 -3600 # Node ID 598ee3a4c1aae70cb2f48364b91506b5240b80b6 # Parent 5038f36b5ea17dd19766910e2f863cab3d7daaab# Parent 2fcd08c624958bb0546aba7f155477c76bf9fc2a merged diff -r 5038f36b5ea1 -r 598ee3a4c1aa NEWS --- a/NEWS Thu Feb 25 15:36:38 2010 +0100 +++ b/NEWS Fri Feb 26 09:49:00 2010 +0100 @@ -38,6 +38,8 @@ and ML_command "set Syntax.trace_ast" help to diagnose syntax problems. +* Type constructors admit general mixfix syntax, not just infix. + *** Pure *** @@ -172,6 +174,13 @@ *** ML *** +* Antiquotations for type constructors: + + @{type_name NAME} -- logical type (as before) + @{type_abbrev NAME} -- type abbreviation + @{nonterminal NAME} -- type of concrete syntactic category + @{type_syntax NAME} -- syntax representation of any of the above + * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw syntax constant (cf. 'syntax' command). diff -r 5038f36b5ea1 -r 598ee3a4c1aa doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 26 09:49:00 2010 +0100 @@ -13,14 +13,14 @@ \end{matharray} \begin{rail} - 'typedecl' typespec infix? + 'typedecl' typespec mixfix? ; 'typedef' altname? abstype '=' repset ; altname: '(' (name | 'open' | 'open' name) ')' ; - abstype: typespec infix? + abstype: typespec mixfix? ; repset: term ('morphisms' name name)? ; @@ -367,7 +367,7 @@ 'rep\_datatype' ('(' (name +) ')')? (term +) ; - dtspec: parname? typespec infix? '=' (cons + '|') + dtspec: parname? typespec mixfix? '=' (cons + '|') ; cons: name ( type * ) mixfix? \end{rail} @@ -893,6 +893,9 @@ \item[iterations] sets how many sets of assignments are generated for each particular size. + \item[no\_assms] specifies whether assumptions in + structured proofs should be ignored. + \end{description} These option can be given within square brackets. diff -r 5038f36b5ea1 -r 598ee3a4c1aa doc-src/IsarRef/Thy/Inner_Syntax.thy --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Feb 26 09:49:00 2010 +0100 @@ -244,11 +244,9 @@ section {* Mixfix annotations *} text {* Mixfix annotations specify concrete \emph{inner syntax} of - Isabelle types and terms. Some commands such as @{command - "typedecl"} admit infixes only, while @{command "definition"} etc.\ - support the full range of general mixfixes and binders. Fixed - parameters in toplevel theorem statements, locale specifications - also admit mixfix annotations. + Isabelle types and terms. Locally fixed parameters in toplevel + theorem statements, locale specifications etc.\ also admit mixfix + annotations. \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} \begin{rail} diff -r 5038f36b5ea1 -r 598ee3a4c1aa doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Fri Feb 26 09:49:00 2010 +0100 @@ -959,9 +959,9 @@ \end{matharray} \begin{rail} - 'types' (typespec '=' type infix? +) + 'types' (typespec '=' type mixfix? +) ; - 'typedecl' typespec infix? + 'typedecl' typespec mixfix? ; 'arities' (nameref '::' arity +) ; diff -r 5038f36b5ea1 -r 598ee3a4c1aa doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 25 15:36:38 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 26 09:49:00 2010 +0100 @@ -33,14 +33,14 @@ \end{matharray} \begin{rail} - 'typedecl' typespec infix? + 'typedecl' typespec mixfix? ; 'typedef' altname? abstype '=' repset ; altname: '(' (name | 'open' | 'open' name) ')' ; - abstype: typespec infix? + abstype: typespec mixfix? ; repset: term ('morphisms' name name)? ; @@ -372,7 +372,7 @@ 'rep\_datatype' ('(' (name +) ')')? (term +) ; - dtspec: parname? typespec infix? '=' (cons + '|') + dtspec: parname? typespec mixfix? '=' (cons + '|') ; cons: name ( type * ) mixfix? \end{rail} @@ -906,6 +906,9 @@ \item[iterations] sets how many sets of assignments are generated for each particular size. + \item[no\_assms] specifies whether assumptions in + structured proofs should be ignored. + \end{description} These option can be given within square brackets. diff -r 5038f36b5ea1 -r 598ee3a4c1aa doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Feb 25 15:36:38 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Feb 26 09:49:00 2010 +0100 @@ -266,10 +266,9 @@ % \begin{isamarkuptext}% Mixfix annotations specify concrete \emph{inner syntax} of - Isabelle types and terms. Some commands such as \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} admit infixes only, while \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}} etc.\ - support the full range of general mixfixes and binders. Fixed - parameters in toplevel theorem statements, locale specifications - also admit mixfix annotations. + Isabelle types and terms. Locally fixed parameters in toplevel + theorem statements, locale specifications etc.\ also admit mixfix + annotations. \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} \begin{rail} diff -r 5038f36b5ea1 -r 598ee3a4c1aa doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Feb 25 15:36:38 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Feb 26 09:49:00 2010 +0100 @@ -996,9 +996,9 @@ \end{matharray} \begin{rail} - 'types' (typespec '=' type infix? +) + 'types' (typespec '=' type mixfix? +) ; - 'typedecl' typespec infix? + 'typedecl' typespec mixfix? ; 'arities' (nameref '::' arity +) ; diff -r 5038f36b5ea1 -r 598ee3a4c1aa doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Thu Feb 25 15:36:38 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Fri Feb 26 09:49:00 2010 +0100 @@ -1910,7 +1910,7 @@ (\S\ref{output-format}).} \optrue{assms}{no\_assms} -Specifies whether the relevant assumptions in structured proof should be +Specifies whether the relevant assumptions in structured proofs should be considered. The option is implicitly enabled for automatic runs. \nopagebreak @@ -2743,8 +2743,6 @@ \item[$\bullet$] Although this has never been observed, arbitrary theorem morphisms could possibly confuse Nitpick, resulting in spurious counterexamples. -\item[$\bullet$] Local definitions are not supported and result in an error. - %\item[$\bullet$] All constants and types whose names start with %\textit{Nitpick}{.} are reserved for internal use. \end{enum} diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Algebra/Congruence.thy --- a/src/HOL/Algebra/Congruence.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Algebra/Congruence.thy Fri Feb 26 09:49:00 2010 +0100 @@ -35,15 +35,17 @@ eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\ _") "is_closed A == (A \ carrier S \ closure_of A = A)" -syntax +abbreviation not_eq :: "_ \ 'a \ 'a \ bool" (infixl ".\\" 50) - not_elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50) - set_not_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.\}\" 50) + where "x .\\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)" -translations - "x .\\ y" == "~(x .=\ y)" - "x .\\ A" == "~(x .\\ A)" - "A {.\}\ B" == "~(A {.=}\ B)" +abbreviation + not_elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50) + where "x .\\<^bsub>S\<^esub> A == ~(x .\\<^bsub>S\<^esub> A)" + +abbreviation + set_not_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.\}\" 50) + where "A {.\}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)" locale equivalence = fixes S (structure) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Feb 26 09:49:00 2010 +0100 @@ -64,10 +64,8 @@ subsection {* Euclidean domains *} (* -axclass - euclidean < "domain" - - euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). +class euclidean = "domain" + + assumes euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). a = b * q + r & e_size r < e_size b)" Nothing has been proved about Euclidean domains, yet. diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Bali/Basis.thy Fri Feb 26 09:49:00 2010 +0100 @@ -222,12 +222,12 @@ section "quantifiers for option type" syntax - Oall :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10) - Oex :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10) + "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10) + "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10) syntax (symbols) - Oall :: "[pttrn, 'a option, bool] => bool" ("(3\_\_:/ _)" [0,0,10] 10) - Oex :: "[pttrn, 'a option, bool] => bool" ("(3\_\_:/ _)" [0,0,10] 10) + "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3\_\_:/ _)" [0,0,10] 10) + "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3\_\_:/ _)" [0,0,10] 10) translations "! x:A: P" == "! x:CONST Option.set A. P" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Bali/Table.thy --- a/src/HOL/Bali/Table.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Bali/Table.thy Fri Feb 26 09:49:00 2010 +0100 @@ -37,11 +37,9 @@ section "map of / table of" -syntax - table_of :: "('a \ 'b) list \ ('a, 'b) table" --{* concrete table *} - abbreviation - "table_of \ map_of" + table_of :: "('a \ 'b) list \ ('a, 'b) table" --{* concrete table *} + where "table_of \ map_of" translations (type)"'a \ 'b" <= (type)"'a \ 'b Datatype.option" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Feb 26 09:49:00 2010 +0100 @@ -30,7 +30,8 @@ VC_Take of int list * (bool * string list) option | VC_Only of string list | VC_Without of string list | - VC_Examine of string list + VC_Examine of string list | + VC_Single of string fun get_vc thy vc_name = (case Boogie_VCs.lookup thy vc_name of @@ -42,11 +43,37 @@ | _ => error ("There is no verification condition " ^ quote vc_name ^ "."))) +local + fun split_goal t = + (case Boogie_Tactics.split t of + [tp] => tp + | _ => error "Multiple goals.") + + fun single_prep t = + let + val (us, u) = split_goal t + val assms = [((@{binding vc_trace}, []), map (rpair []) us)] + in + pair [u] o snd o ProofContext.add_assms_i Assumption.assume_export assms + end + + fun single_prove goal ctxt thm = + Goal.prove ctxt [] [] goal (fn {context, ...} => HEADGOAL ( + Boogie_Tactics.split_tac + THEN' Boogie_Tactics.drop_assert_at_tac + THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context)) +in fun boogie_vc (vc_name, vc_opts) lthy = let val thy = ProofContext.theory_of lthy val vc = get_vc thy vc_name + fun extract vc l = + (case Boogie_VCs.extract vc l of + SOME vc' => vc' + | NONE => error ("There is no assertion to be proved with label " ^ + quote l ^ ".")) + val vcs = (case vc_opts of VC_Complete => [vc] @@ -55,18 +82,29 @@ | VC_Take (ps, SOME (false, ls)) => [Boogie_VCs.paths_without ps ls vc] | VC_Only ls => [Boogie_VCs.only ls vc] | VC_Without ls => [Boogie_VCs.without ls vc] - | VC_Examine ls => map_filter (Boogie_VCs.extract vc) ls) + | VC_Examine ls => map (extract vc) ls + | VC_Single l => [extract vc l]) val ts = map Boogie_VCs.prop_of_vc vcs + val (prepare, finish) = + (case vc_opts of + VC_Single _ => (single_prep (hd ts), single_prove (hd ts)) + | _ => (pair ts, K I)) + val discharge = fold (Boogie_VCs.discharge o pair vc_name) fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms)) | after_qed _ = I in lthy |> fold Variable.auto_fixes ts - |> Proof.theorem_i NONE after_qed [map (rpair []) ts] + |> (fn lthy1 => lthy1 + |> prepare + |-> (fn us => fn lthy2 => lthy2 + |> Proof.theorem_i NONE (fn thmss => fn ctxt => + let val export = map (finish lthy1) o ProofContext.export ctxt lthy2 + in after_qed (map export thmss) ctxt end) [map (rpair []) us])) end - +end fun write_list head = map Pretty.str o sort (dict_ord string_ord o pairself explode) #> @@ -239,7 +277,8 @@ val vc_name = OuterParse.name -val vc_labels = Scan.repeat1 OuterParse.name +val vc_label = OuterParse.name +val vc_labels = Scan.repeat1 vc_label val vc_paths = OuterParse.nat -- (Args.$$$ "-" |-- OuterParse.nat) >> (op upto) || @@ -247,13 +286,14 @@ val vc_opts = scan_arg - (scan_val "examine" vc_labels >> VC_Examine || + (scan_val "assertion" vc_label >> VC_Single || + scan_val "examine" vc_labels >> VC_Examine || scan_val "take" ((OuterParse.list vc_paths >> flat) -- Scan.option ( scan_val "without" vc_labels >> pair false || scan_val "and_also" vc_labels >> pair true) >> VC_Take) || scan_val "only" vc_labels >> VC_Only || scan_val "without" vc_labels >> VC_Without) || - Scan.succeed VC_Complete + Scan.succeed VC_Complete val _ = OuterSyntax.command "boogie_vc" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Fri Feb 26 09:49:00 2010 +0100 @@ -49,6 +49,26 @@ if line = 0 orelse col = 0 then no_label_name else label_prefix ^ string_of_int line ^ "_" ^ string_of_int col +local + val quote_mixfix = + Symbol.explode #> map + (fn "_" => "'_" + | "(" => "'(" + | ")" => "')" + | "/" => "'/" + | s => s) #> + implode +in +fun mk_syntax name i = + let + val syn = quote_mixfix name + val args = concat (separate ",/ " (replicate i "_")) + in + if i = 0 then Mixfix (syn, [], 1000) + else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000) + end +end + datatype attribute_value = StringValue of string | TermValue of term @@ -78,8 +98,8 @@ | NONE => let val args = Name.variant_list [] (replicate arity "'") - val (T, thy') = - ObjectLogic.typedecl (Binding.name isa_name, args, NoSyn) thy + val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args, + mk_syntax name arity) thy val type_name = fst (Term.dest_Type T) in (((name, type_name), log_new name type_name), thy') end) end @@ -93,24 +113,6 @@ local - val quote_mixfix = - Symbol.explode #> map - (fn "_" => "'_" - | "(" => "'(" - | ")" => "')" - | "/" => "'/" - | s => s) #> - implode - - fun mk_syntax name i = - let - val syn = quote_mixfix name - val args = concat (separate ",/ " (replicate i "_")) - in - if i = 0 then Mixfix (syn, [], 1000) - else Mixfix (syn ^ "()'(/" ^ args ^ "')", replicate i 0, 1000) - end - fun maybe_builtin T = let fun const name = SOME (Const (name, T)) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Boogie/Tools/boogie_tactics.ML --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Feb 26 09:49:00 2010 +0100 @@ -9,6 +9,9 @@ val unfold_labels_tac: Proof.context -> int -> tactic val boogie_tac: Proof.context -> thm list -> int -> tactic val boogie_all_tac: Proof.context -> thm list -> tactic + val split: term -> (term list * term) list + val split_tac: int -> tactic + val drop_assert_at_tac: int -> tactic val setup: theory -> theory end @@ -47,25 +50,38 @@ local - fun prep_tac facts = - Method.insert_tac facts - THEN' REPEAT_ALL_NEW - (Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}] - ORELSE' Tactic.etac @{thm conjE}) + fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u + | explode_conj t = [t] - val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv - (Conv.rewr_conv assert_at_def))) + fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u) + | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u) + | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)] + | splt (_, @{term True}) = [] + | splt tp = [tp] +in +fun split t = + splt ([], HOLogic.dest_Trueprop t) + |> map (fn (us, u) => (map HOLogic.mk_Trueprop us, HOLogic.mk_Trueprop u)) +end +val split_tac = REPEAT_ALL_NEW ( + Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}] + ORELSE' Tactic.etac @{thm conjE}) + +val drop_assert_at_tac = CONVERSION (Conv.concl_conv ~1 (Conv.try_conv ( + Conv.arg_conv (Conv.rewr_conv assert_at_def)))) + +local fun case_name_of t = (case HOLogic.dest_Trueprop (Logic.strip_imp_concl t) of @{term assert_at} $ Free (n, _) $ _ => n | _ => raise TERM ("case_name_of", [t])) fun boogie_cases ctxt = METHOD_CASES (fn facts => - ALLGOALS (prep_tac facts) #> + ALLGOALS (Method.insert_tac facts THEN' split_tac) #> Seq.maps (fn st => st - |> ALLGOALS (CONVERSION drop_assert_at) + |> ALLGOALS drop_assert_at_tac |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #> Seq.maps (fn (names, st) => CASES diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Fri Feb 26 09:49:00 2010 +0100 @@ -1541,7 +1541,7 @@ hence "real ?num \ 0" by auto have e_nat: "int (nat e) = e" using `0 \ e` by auto have num_eq: "real ?num = real (- floor_fl x)" using `0 < nat (- m)` - unfolding Float_floor real_of_float_minus real_of_float_simp real_of_nat_mult pow2_int[of "nat e", unfolded e_nat] realpow_real_of_nat[symmetric] by auto + unfolding Float_floor real_of_float_minus real_of_float_simp real_of_nat_mult pow2_int[of "nat e", unfolded e_nat] real_of_nat_power by auto have "0 < - floor_fl x" using `0 < ?num`[unfolded real_of_nat_less_iff[symmetric]] unfolding less_float_def num_eq[symmetric] real_of_float_0 real_of_nat_zero . hence "real (floor_fl x) < 0" unfolding less_float_def by auto diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Groups.thy --- a/src/HOL/Groups.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Groups.thy Fri Feb 26 09:49:00 2010 +0100 @@ -1250,7 +1250,7 @@ val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]; val dest_eqI = - fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of; + fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of; ); *} diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/HOL.thy Fri Feb 26 09:49:00 2010 +0100 @@ -846,9 +846,12 @@ setup {* let (*prevent substitution on bool*) - fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso - Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false) - (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm; + fun hyp_subst_tac' i thm = + if i <= Thm.nprems_of thm andalso + Term.exists_Const + (fn (@{const_name "op ="}, Type (_, [T, _])) => T <> @{typ bool} | _ => false) + (nth (Thm.prems_of thm) (i - 1)) + then Hypsubst.hyp_subst_tac i thm else no_tac thm; in Hypsubst.hypsubst_setup #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) @@ -1721,8 +1724,8 @@ fun eq_codegen thy defs dep thyname b t gr = (case strip_comb t of - (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE - | (Const ("op =", _), [t, u]) => + (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE + | (Const (@{const_name "op ="}, _), [t, u]) => let val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr; val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr'; @@ -1731,7 +1734,7 @@ SOME (Codegen.parens (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''') end - | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen + | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen thy defs dep thyname b (Codegen.eta_expand t ts 2) gr) | _ => NONE); @@ -2050,7 +2053,7 @@ (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) local - fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t + fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t | wrong_prem (Bound _) = true | wrong_prem _ = false; val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Feb 26 09:49:00 2010 +0100 @@ -256,8 +256,8 @@ (* Special syntax for guarded statements and guarded array updates: *) syntax - guarded_com :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) - array_update :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) + "_guarded_com" :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) + "_array_update" :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) translations "P \ c" == "IF P THEN c ELSE CONST Abort FI" "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Import/HOL/prob_extra.imp --- a/src/HOL/Import/HOL/prob_extra.imp Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Import/HOL/prob_extra.imp Fri Feb 26 09:49:00 2010 +0100 @@ -22,7 +22,7 @@ "REAL_SUP_MAX" > "HOL4Prob.prob_extra.REAL_SUP_MAX" "REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X" "REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE" - "REAL_POW" > "RealPow.realpow_real_of_nat" + "REAL_POW" > "RealDef.power_real_of_nat" "REAL_LE_INV_LE" > "Rings.le_imp_inverse_le" "REAL_LE_EQ" > "Set.basic_trans_rules_26" "REAL_INVINV_ALL" > "Rings.inverse_inverse_eq" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Import/HOL/real.imp Fri Feb 26 09:49:00 2010 +0100 @@ -105,7 +105,7 @@ "REAL_POASQ" > "HOL4Real.real.REAL_POASQ" "REAL_OVER1" > "Rings.divide_1" "REAL_OF_NUM_SUC" > "RealDef.real_of_nat_Suc" - "REAL_OF_NUM_POW" > "RealPow.realpow_real_of_nat" + "REAL_OF_NUM_POW" > "RealDef.power_real_of_nat" "REAL_OF_NUM_MUL" > "RealDef.real_of_nat_mult" "REAL_OF_NUM_LE" > "RealDef.real_of_nat_le_iff" "REAL_OF_NUM_EQ" > "RealDef.real_of_nat_inject" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/IsaMakefile Fri Feb 26 09:49:00 2010 +0100 @@ -955,11 +955,12 @@ ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \ ex/Codegenerator_Test.thy ex/Coherent.thy \ ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \ - ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ - ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ - ex/Hilbert_Classical.thy ex/Induction_Schema.thy \ - ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ - ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ + ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \ + ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \ + ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \ + ex/Induction_Schema.thy ex/InductiveInvariant.thy \ + ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ + ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \ ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \ ex/Predicate_Compile_ex.thy ex/Predicate_Compile_Quickcheck.thy \ diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Fri Feb 26 09:49:00 2010 +0100 @@ -60,9 +60,8 @@ ("(3|- _/ (2_)/ _)" [100, 55, 100] 50) "|- P c Q == ALL s s'. Sem c s s' --> s : P --> s' : Q" -syntax (xsymbols) - Valid :: "'a bexp => 'a com => 'a bexp => bool" - ("(3\ _/ (2_)/ _)" [100, 55, 100] 50) +notation (xsymbols) + Valid ("(3\ _/ (2_)/ _)" [100, 55, 100] 50) lemma ValidI [intro?]: "(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Library/Float.thy Fri Feb 26 09:49:00 2010 +0100 @@ -789,12 +789,12 @@ hence "real x / real y < 1" using `0 < y` and `0 \ x` by auto from real_of_int_div4[of "?X" y] - have "real (?X div y) \ (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power[symmetric] real_number_of . + have "real (?X div y) \ (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of . also have "\ < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto) finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto hence "?X div y + 1 \ 2^?l" by auto hence "real (?X div y + 1) * inverse (2^?l) \ 2^?l * inverse (2^?l)" - unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of + unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of by (rule mult_right_mono, auto) hence "real (?X div y + 1) * inverse (2^?l) \ 1" by auto thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False] @@ -863,12 +863,12 @@ qed from real_of_int_div4[of "?X" y] - have "real (?X div y) \ (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power[symmetric] real_number_of . + have "real (?X div y) \ (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of . also have "\ < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto) finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)" - unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of + unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of by (rule mult_strict_right_mono, auto) hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False] @@ -1188,7 +1188,7 @@ show "?thesis" proof (cases "0 < ?d") case True - hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto + hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp show ?thesis proof (cases "m mod ?p = 0") case True @@ -1224,7 +1224,7 @@ show "?thesis" proof (cases "0 < ?d") case True - hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto + hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp have "m div ?p * ?p \ m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le]) also have "\ \ m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. finally have "real (Float (m div ?p) (e + ?d)) \ real (Float m e)" unfolding real_of_float_simp add_commute[of e] @@ -1263,7 +1263,7 @@ case True have "real (m div 2^(nat ?l)) * pow2 ?l \ real m" proof - - have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power[symmetric] real_number_of unfolding pow2_int[symmetric] + have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_number_of unfolding pow2_int[symmetric] using `?l > 0` by auto also have "\ \ real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto also have "\ = real m" unfolding zmod_zdiv_equality[symmetric] .. @@ -1329,7 +1329,7 @@ hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto also have "\ \ real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 . - also have "\ = real m * inverse (2 ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def .. + also have "\ = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def .. also have "\ = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] .. finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\ 0 \ e`] . next @@ -1357,7 +1357,7 @@ case False hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] .. - also have "\ = real m / real ((2::int) ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def .. + also have "\ = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def .. also have "\ \ 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] . also have "\ = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\ 0 \ e`] . diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Library/Multiset.thy Fri Feb 26 09:49:00 2010 +0100 @@ -1502,13 +1502,13 @@ by (cases M) auto syntax - comprehension1_mset :: "'a \ 'b \ 'b multiset \ 'a multiset" + "_comprehension1_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" ("({#_/. _ :# _#})") translations "{#e. x:#M#}" == "CONST image_mset (%x. e) M" syntax - comprehension2_mset :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" + "_comprehension2_mset" :: "'a \ 'b \ 'b multiset \ bool \ 'a multiset" ("({#_/ | _ :# _./ _#})") translations "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Fri Feb 26 09:49:00 2010 +0100 @@ -167,7 +167,7 @@ begin lemma size0: "0 < n" -by (cut_tac size1, simp) +using size1 by simp lemmas definitions = zero_def one_def add_def mult_def minus_def diff_def @@ -384,23 +384,18 @@ "_NumeralType1" :: type ("1") translations - "_NumeralType1" == (type) "num1" - "_NumeralType0" == (type) "num0" + (type) "1" == (type) "num1" + (type) "0" == (type) "num0" parse_translation {* let -(* FIXME @{type_syntax} *) -val num1_const = Syntax.const "Numeral_Type.num1"; -val num0_const = Syntax.const "Numeral_Type.num0"; -val B0_const = Syntax.const "Numeral_Type.bit0"; -val B1_const = Syntax.const "Numeral_Type.bit1"; - fun mk_bintype n = let - fun mk_bit n = if n = 0 then B0_const else B1_const; + fun mk_bit 0 = Syntax.const @{type_syntax bit0} + | mk_bit 1 = Syntax.const @{type_syntax bit1}; fun bin_of n = - if n = 1 then num1_const - else if n = 0 then num0_const + if n = 1 then Syntax.const @{type_syntax num1} + else if n = 0 then Syntax.const @{type_syntax num0} else if n = ~1 then raise TERM ("negative type numeral", []) else let val (q, r) = Integer.div_mod n 2; @@ -419,25 +414,22 @@ fun int_of [] = 0 | int_of (b :: bs) = b + 2 * int_of bs; -(* FIXME @{type_syntax} *) -fun bin_of (Const ("num0", _)) = [] - | bin_of (Const ("num1", _)) = [1] - | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs - | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs - | bin_of t = raise TERM("bin_of", [t]); +fun bin_of (Const (@{type_syntax num0}, _)) = [] + | bin_of (Const (@{type_syntax num1}, _)) = [1] + | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs + | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs + | bin_of t = raise TERM ("bin_of", [t]); fun bit_tr' b [t] = - let - val rev_digs = b :: bin_of t handle TERM _ => raise Match - val i = int_of rev_digs; - val num = string_of_int (abs i); - in - Syntax.const "_NumeralType" $ Syntax.free num - end + let + val rev_digs = b :: bin_of t handle TERM _ => raise Match + val i = int_of rev_digs; + val num = string_of_int (abs i); + in + Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num + end | bit_tr' b _ = raise Match; - -(* FIXME @{type_syntax} *) -in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end; +in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end; *} subsection {* Examples *} diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Fri Feb 26 09:49:00 2010 +0100 @@ -66,9 +66,8 @@ | Some x \ frs = []" -syntax (xsymbols) - correct_state :: "[jvm_prog,prog_type,jvm_state] \ bool" - ("_,_ \JVM _ \" [51,51] 50) +notation (xsymbols) + correct_state ("_,_ \JVM _ \" [51,51] 50) lemma sup_ty_opt_OK: diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/MicroJava/BV/JVMType.thy --- a/src/HOL/MicroJava/BV/JVMType.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/MicroJava/BV/JVMType.thy Fri Feb 26 09:49:00 2010 +0100 @@ -59,15 +59,11 @@ "sup_state_opt G == Opt.le (sup_state G)" -syntax (xsymbols) - sup_ty_opt :: "['code prog,ty err,ty err] \ bool" - ("_ \ _ <=o _" [71,71] 70) - sup_loc :: "['code prog,locvars_type,locvars_type] \ bool" - ("_ \ _ <=l _" [71,71] 70) - sup_state :: "['code prog,state_type,state_type] \ bool" - ("_ \ _ <=s _" [71,71] 70) - sup_state_opt :: "['code prog,state_type option,state_type option] \ bool" - ("_ \ _ <=' _" [71,71] 70) +notation (xsymbols) + sup_ty_opt ("_ \ _ <=o _" [71,71] 70) and + sup_loc ("_ \ _ <=l _" [71,71] 70) and + sup_state ("_ \ _ <=s _" [71,71] 70) and + sup_state_opt ("_ \ _ <=' _" [71,71] 70) lemma JVM_states_unfold: diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/MicroJava/Comp/TranslCompTp.thy --- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Fri Feb 26 09:49:00 2010 +0100 @@ -19,9 +19,8 @@ comb_nil :: "'a \ 'b list \ 'a" "comb_nil a == ([], a)" -syntax (xsymbols) - "comb" :: "['a \ 'b list \ 'c, 'c \ 'b list \ 'd, 'a] \ 'b list \ 'd" - (infixr "\" 55) +notation (xsymbols) + comb (infixr "\" 55) lemma comb_nil_left [simp]: "comb_nil \ f = f" by (simp add: comb_def comb_nil_def split_beta) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/MicroJava/DFA/Semilat.thy --- a/src/HOL/MicroJava/DFA/Semilat.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/MicroJava/DFA/Semilat.thy Fri Feb 26 09:49:00 2010 +0100 @@ -32,16 +32,19 @@ "lesssub" ("(_ /\\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and "plussub" ("(_ /\\<^bsub>_\<^esub> _)" [65, 0, 66] 65) (*<*) -syntax - (* allow \ instead of \..\ *) - "_lesub" :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) - "_lesssub" :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) - "_plussub" :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("(_ /\\<^sub>_ _)" [65, 1000, 66] 65) +(* allow \ instead of \..\ *) + +abbreviation (input) + lesub1 :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) + where "x \\<^sub>r y == x \\<^bsub>r\<^esub> y" -translations - "x \\<^sub>r y" => "x \\<^bsub>r\<^esub> y" - "x \\<^sub>r y" => "x \\<^bsub>r\<^esub> y" - "x \\<^sub>f y" => "x \\<^bsub>f\<^esub> y" +abbreviation (input) + lesssub1 :: "'a \ 'a ord \ 'a \ bool" ("(_ /\\<^sub>_ _)" [50, 1000, 51] 50) + where "x \\<^sub>r y == x \\<^bsub>r\<^esub> y" + +abbreviation (input) + plussub1 :: "'a \ ('a \ 'b \ 'c) \ 'b \ 'c" ("(_ /\\<^sub>_ _)" [65, 1000, 66] 65) + where "x \\<^sub>f y == x \\<^bsub>f\<^esub> y" (*>*) defs diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/MicroJava/J/Conform.thy Fri Feb 26 09:49:00 2010 +0100 @@ -38,24 +38,13 @@ xconf (heap (store s)) (abrupt s)" -syntax (xsymbols) - hext :: "aheap => aheap => bool" - ("_ \| _" [51,51] 50) - - conf :: "'c prog => aheap => val => ty => bool" - ("_,_ \ _ ::\ _" [51,51,51,51] 50) - - lconf :: "'c prog => aheap => ('a \ val) => ('a \ ty) => bool" - ("_,_ \ _ [::\] _" [51,51,51,51] 50) - - oconf :: "'c prog => aheap => obj => bool" - ("_,_ \ _ \" [51,51,51] 50) - - hconf :: "'c prog => aheap => bool" - ("_ \h _ \" [51,51] 50) - - conforms :: "state => java_mb env' => bool" - ("_ ::\ _" [51,51] 50) +notation (xsymbols) + hext ("_ \| _" [51,51] 50) and + conf ("_,_ \ _ ::\ _" [51,51,51,51] 50) and + lconf ("_,_ \ _ [::\] _" [51,51,51,51] 50) and + oconf ("_,_ \ _ \" [51,51,51] 50) and + hconf ("_ \h _ \" [51,51] 50) and + conforms ("_ ::\ _" [51,51] 50) section "hext" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/MicroJava/JVM/JVMDefensive.thy --- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Fri Feb 26 09:49:00 2010 +0100 @@ -123,19 +123,15 @@ | Normal s' \ if check G s' then Normal (exec (G, s')) else TypeError" -consts - "exec_all_d" :: "jvm_prog \ jvm_state type_error \ jvm_state type_error \ bool" +constdefs + exec_all_d :: "jvm_prog \ jvm_state type_error \ jvm_state type_error \ bool" ("_ |- _ -jvmd-> _" [61,61,61]60) + "G |- s -jvmd-> t \ + (s,t) \ ({(s,t). exec_d G s = TypeError \ t = TypeError} \ + {(s,t). \t'. exec_d G s = Normal (Some t') \ t = Normal t'})\<^sup>*" -syntax (xsymbols) - "exec_all_d" :: "jvm_prog \ jvm_state type_error \ jvm_state type_error \ bool" - ("_ \ _ -jvmd\ _" [61,61,61]60) - -defs - exec_all_d_def: - "G \ s -jvmd\ t \ - (s,t) \ ({(s,t). exec_d G s = TypeError \ t = TypeError} \ - {(s,t). \t'. exec_d G s = Normal (Some t') \ t = Normal t'})\<^sup>*" +notation (xsymbols) + exec_all_d ("_ \ _ -jvmd\ _" [61,61,61]60) declare split_paired_All [simp del] diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/MicroJava/JVM/JVMExec.thy --- a/src/HOL/MicroJava/JVM/JVMExec.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Fri Feb 26 09:49:00 2010 +0100 @@ -32,9 +32,8 @@ "G |- s -jvm-> t == (s,t) \ {(s,t). exec(G,s) = Some t}^*" -syntax (xsymbols) - exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" - ("_ \ _ -jvm\ _" [61,61,61]60) +notation (xsymbols) + exec_all ("_ \ _ -jvm\ _" [61,61,61]60) text {* The start configuration of the JVM: in the start heap, we call a diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/NanoJava/Equivalence.thy Fri Feb 26 09:49:00 2010 +0100 @@ -33,14 +33,14 @@ cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60) "A ||=e t \ \n. ||=n: A --> |=n:e t" -syntax (xsymbols) - valid :: "[assn,stmt, assn] => bool" ( "\ {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) - evalid :: "[assn,expr,vassn] => bool" ("\\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) - nvalid :: "[nat, triple ] => bool" ("\_: _" [61,61] 60) - envalid :: "[nat,etriple ] => bool" ("\_:\<^sub>e _" [61,61] 60) - nvalids :: "[nat, triple set] => bool" ("|\_: _" [61,61] 60) - cnvalids :: "[triple set,triple set] => bool" ("_ |\/ _" [61,61] 60) -cenvalid :: "[triple set,etriple ] => bool" ("_ |\\<^sub>e/ _"[61,61] 60) +notation (xsymbols) + valid ("\ {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and + evalid ("\\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and + nvalid ("\_: _" [61,61] 60) and + envalid ("\_:\<^sub>e _" [61,61] 60) and + nvalids ("|\_: _" [61,61] 60) and + cnvalids ("_ |\/ _" [61,61] 60) and + cenvalid ("_ |\\<^sub>e/ _"[61,61] 60) lemma nvalid_def2: "\n: (P,c,Q) \ \s t. s -c-n\ t \ P s \ Q t" @@ -164,10 +164,10 @@ "MGT c Z \ (\s. Z = s, c, \ t. \n. Z -c- n\ t)" MGTe :: "expr => state => etriple" "MGTe e Z \ (\s. Z = s, e, \v t. \n. Z -e\v-n\ t)" -syntax (xsymbols) - MGTe :: "expr => state => etriple" ("MGT\<^sub>e") -syntax (HTML output) - MGTe :: "expr => state => etriple" ("MGT\<^sub>e") +notation (xsymbols) + MGTe ("MGT\<^sub>e") +notation (HTML output) + MGTe ("MGT\<^sub>e") lemma MGF_implies_complete: "\Z. {} |\ { MGT c Z} \ \ {P} c {Q} \ {} \ {P} c {Q}" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/NanoJava/State.thy --- a/src/HOL/NanoJava/State.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/NanoJava/State.thy Fri Feb 26 09:49:00 2010 +0100 @@ -84,9 +84,9 @@ lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000) "lupd x v s \ s (| locals := ((locals s)(x\v ))|)" -syntax (xsymbols) - hupd :: "loc => obj => state => state" ("hupd'(_\_')" [10,10] 1000) - lupd :: "vname => val => state => state" ("lupd'(_\_')" [10,10] 1000) +notation (xsymbols) + hupd ("hupd'(_\_')" [10,10] 1000) and + lupd ("lupd'(_\_')" [10,10] 1000) constdefs diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 26 09:49:00 2010 +0100 @@ -14,8 +14,9 @@ ML {* exception FAIL -val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1 -val def_table = Nitpick_HOL.const_def_table @{context} defs +val subst = [] +val defs = Nitpick_HOL.all_axioms_of @{theory} subst |> #1 +val def_table = Nitpick_HOL.const_def_table @{context} subst defs val hol_ctxt : Nitpick_HOL.hol_context = {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Feb 26 09:49:00 2010 +0100 @@ -1381,25 +1381,16 @@ text {* A type class without axioms: *} -axclass classA +class classA lemma "P (x\'a\classA)" nitpick [expect = genuine] oops -text {* The axiom of this type class does not contain any type variables: *} - -axclass classB -classB_ax: "P \ \ P" - -lemma "P (x\'a\classB)" -nitpick [expect = genuine] -oops - text {* An axiom with a type variable (denoting types which have at least two elements): *} -axclass classC < type -classC_ax: "\x y. x \ y" +class classC = + assumes classC_ax: "\x y. x \ y" lemma "P (x\'a\classC)" nitpick [expect = genuine] @@ -1411,11 +1402,9 @@ text {* A type class for which a constant is defined: *} -consts -classD_const :: "'a \ 'a" - -axclass classD < type -classD_ax: "classD_const (classD_const x) = classD_const x" +class classD = + fixes classD_const :: "'a \ 'a" + assumes classD_ax: "classD_const (classD_const x) = classD_const x" lemma "P (x\'a\classD)" nitpick [expect = genuine] @@ -1423,16 +1412,12 @@ text {* A type class with multiple superclasses: *} -axclass classE < classC, classD +class classE = classC + classD lemma "P (x\'a\classE)" nitpick [expect = genuine] oops -lemma "P (x\'a\{classB, classE})" -nitpick [expect = genuine] -oops - text {* OFCLASS: *} lemma "OFCLASS('a\type, type_class)" @@ -1445,12 +1430,6 @@ apply intro_classes done -lemma "OFCLASS('a, classB_class)" -nitpick [expect = none] -apply intro_classes -apply simp -done - lemma "OFCLASS('a\type, classC_class)" nitpick [expect = genuine] oops diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Nominal/Nominal.thy Fri Feb 26 09:49:00 2010 +0100 @@ -3403,13 +3403,13 @@ where ABS_in: "(abs_fun a x)\ABS_set" -typedef (ABS) ('x,'a) ABS = "ABS_set::('x\('a noption)) set" +typedef (ABS) ('x,'a) ABS ("\_\_" [1000,1000] 1000) = + "ABS_set::('x\('a noption)) set" proof fix x::"'a" and a::"'x" show "(abs_fun a x)\ ABS_set" by (rule ABS_in) qed -syntax ABS :: "type \ type \ type" ("\_\_" [1000,1000] 1000) section {* lemmas for deciding permutation equations *} (*===================================================*) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Feb 26 09:49:00 2010 +0100 @@ -2079,7 +2079,7 @@ local structure P = OuterParse and K = OuterKeyword in val datatype_decl = - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix -- + Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix -- (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix)); fun mk_datatype args = diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Feb 26 09:49:00 2010 +0100 @@ -182,7 +182,7 @@ (Scan.succeed false); fun setup_generate_fresh x = - (Args.goal_spec -- Args.tyname >> + (Args.goal_spec -- Args.type_name true >> (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x; fun setup_fresh_fun_simp x = diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Orderings.thy Fri Feb 26 09:49:00 2010 +0100 @@ -657,13 +657,14 @@ fun matches_bound v t = (case t of - Const ("_bound", _) $ Free (v', _) => v = v' + Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v' | _ => false); fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false); fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P; fun tr' q = (q, - fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] => + fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _), + Const (c, _) $ (Const (d, _) $ t $ u) $ P] => (case AList.lookup (op =) trans (q, c, d) of NONE => raise Match | SOME (l, g) => diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Probability/Borel.thy --- a/src/HOL/Probability/Borel.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Probability/Borel.thy Fri Feb 26 09:49:00 2010 +0100 @@ -82,7 +82,7 @@ fix w n assume le: "f w \ g w - inverse(real(Suc n))" hence "0 < inverse(real(Suc n))" - by (metis inverse_real_of_nat_gt_zero) + by simp thus "f w < g w" using le by arith qed diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Product_Type.thy Fri Feb 26 09:49:00 2010 +0100 @@ -448,44 +448,44 @@ *} ML {* - local - val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"] - fun Pair_pat k 0 (Bound m) = (m = k) - | Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso - m = k+i andalso Pair_pat k (i-1) t - | Pair_pat _ _ _ = false; - fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t - | no_args k i (t $ u) = no_args k i t andalso no_args k i u - | no_args k i (Bound m) = m < k orelse m > k+i - | no_args _ _ _ = true; - fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE - | split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t - | split_pat tp i _ = NONE; + val cond_split_eta_ss = HOL_basic_ss addsimps @{thms cond_split_eta}; + fun Pair_pat k 0 (Bound m) = (m = k) + | Pair_pat k i (Const (@{const_name Pair}, _) $ Bound m $ t) = + i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t + | Pair_pat _ _ _ = false; + fun no_args k i (Abs (_, _, t)) = no_args (k + 1) i t + | no_args k i (t $ u) = no_args k i t andalso no_args k i u + | no_args k i (Bound m) = m < k orelse m > k + i + | no_args _ _ _ = true; + fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE + | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t + | split_pat tp i _ = NONE; fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] [] - (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))) + (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) (K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1))); - fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t - | beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse - (beta_term_pat k i t andalso beta_term_pat k i u) - | beta_term_pat k i t = no_args k i t; - fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg - | eta_term_pat _ _ _ = false; + fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t + | beta_term_pat k i (t $ u) = + Pair_pat k i (t $ u) orelse (beta_term_pat k i t andalso beta_term_pat k i u) + | beta_term_pat k i t = no_args k i t; + fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg + | eta_term_pat _ _ _ = false; fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) - | subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg - else (subst arg k i t $ subst arg k i u) - | subst arg k i t = t; - fun beta_proc ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) = + | subst arg k i (t $ u) = + if Pair_pat k i (t $ u) then incr_boundvars k arg + else (subst arg k i t $ subst arg k i u) + | subst arg k i t = t; + fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) = (case split_pat beta_term_pat 1 t of - SOME (i,f) => SOME (metaeq ss s (subst arg 0 i f)) + SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f)) | NONE => NONE) - | beta_proc _ _ = NONE; - fun eta_proc ss (s as Const ("split", _) $ Abs (_, _, t)) = + | beta_proc _ _ = NONE; + fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) = (case split_pat eta_term_pat 1 t of - SOME (_,ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end)) + SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end)) | NONE => NONE) - | eta_proc _ _ = NONE; + | eta_proc _ _ = NONE; in val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc); val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc); @@ -565,11 +565,11 @@ ML {* local (* filtering with exists_p_split is an essential optimization *) - fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true + fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u | exists_p_split (Abs (_, _, t)) = exists_p_split t | exists_p_split _ = false; - val ss = HOL_basic_ss addsimps [thm "split_conv"]; + val ss = HOL_basic_ss addsimps @{thms split_conv}; in val split_conv_tac = SUBGOAL (fn (t, i) => if exists_p_split t then safe_full_simp_tac ss i else no_tac); @@ -634,10 +634,11 @@ lemma internal_split_conv: "internal_split c (a, b) = c a b" by (simp only: internal_split_def split_conv) +use "Tools/split_rule.ML" +setup Split_Rule.setup + hide const internal_split -use "Tools/split_rule.ML" -setup SplitRule.setup lemmas prod_caseI = prod.cases [THEN iffD2, standard] @@ -1049,7 +1050,6 @@ "Pair" ("(_,/ _)") setup {* - let fun strip_abs_split 0 t = ([], t) @@ -1058,16 +1058,18 @@ val s' = Codegen.new_name t s; val v = Free (s', T) in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end - | strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of + | strip_abs_split i (u as Const (@{const_name split}, _) $ t) = + (case strip_abs_split (i+1) t of (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u) | _ => ([], u)) | strip_abs_split i t = strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0)); -fun let_codegen thy defs dep thyname brack t gr = (case strip_comb t of - (t1 as Const ("Let", _), t2 :: t3 :: ts) => +fun let_codegen thy defs dep thyname brack t gr = + (case strip_comb t of + (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) => let - fun dest_let (l as Const ("Let", _) $ t $ u) = + fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) = (case strip_abs_split 1 u of ([p], u') => apfst (cons (p, t)) (dest_let u') | _ => ([], l)) @@ -1098,7 +1100,7 @@ | _ => NONE); fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of - (t1 as Const ("split", _), t2 :: ts) => + (t1 as Const (@{const_name split}, _), t2 :: ts) => let val ([p], u) = strip_abs_split 1 (t1 $ t2); val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Rational.thy --- a/src/HOL/Rational.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Rational.thy Fri Feb 26 09:49:00 2010 +0100 @@ -6,6 +6,7 @@ theory Rational imports GCD Archimedean_Field +uses ("Tools/float_syntax.ML") begin subsection {* Rational numbers as quotient *} @@ -1212,4 +1213,15 @@ plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat +subsection{* Float syntax *} + +syntax "_Float" :: "float_const \ 'a" ("_") + +use "Tools/float_syntax.ML" +setup Float_Syntax.setup + +text{* Test: *} +lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)" +by simp + end diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/RealDef.thy Fri Feb 26 09:49:00 2010 +0100 @@ -584,6 +584,11 @@ lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y" by (simp add: real_of_int_def) +lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n" +by (simp add: real_of_int_def of_int_power) + +lemmas power_real_of_int = real_of_int_power [symmetric] + lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))" apply (subst real_eq_of_int)+ apply (rule of_int_setsum) @@ -731,6 +736,11 @@ lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" by (simp add: real_of_nat_def of_nat_mult) +lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n" +by (simp add: real_of_nat_def of_nat_power) + +lemmas power_real_of_nat = real_of_nat_power [symmetric] + lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = (SUM x:A. real(f x))" apply (subst real_eq_of_nat)+ diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/RealPow.thy --- a/src/HOL/RealPow.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/RealPow.thy Fri Feb 26 09:49:00 2010 +0100 @@ -7,12 +7,13 @@ theory RealPow imports RealDef -uses ("Tools/float_syntax.ML") begin +(* FIXME: declare this in Rings.thy or not at all *) declare abs_mult_self [simp] -lemma two_realpow_ge_one [simp]: "(1::real) \ 2 ^ n" +(* used by Import/HOL/real.imp *) +lemma two_realpow_ge_one: "(1::real) \ 2 ^ n" by simp lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" @@ -31,18 +32,9 @@ apply (simp split add: nat_diff_split) done -lemma realpow_two_mult_inverse [simp]: - "r \ 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)" -by (simp add: real_mult_assoc [symmetric]) - -lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)" -by simp - lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" -apply (unfold real_diff_def) -apply (simp add: algebra_simps) -done +by (simp add: algebra_simps) lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" @@ -50,36 +42,6 @@ apply auto done -lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)" -apply (induct "n") -apply (auto simp add: real_of_nat_one real_of_nat_mult) -done - -lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)" -apply (induct "n") -apply (auto simp add: zero_less_mult_iff) -done - -(* used by AFP Integration theory *) -lemma realpow_increasing: - "[|(0::real) \ x; 0 \ y; x ^ Suc n \ y ^ Suc n|] ==> x \ y" - by (rule power_le_imp_le_base) - - -subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*} - -lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)" -apply (induct "n") -apply (simp_all add: nat_mult_distrib) -done -declare real_of_int_power [symmetric, simp] - -lemma power_real_number_of: - "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)" -by (simp only: real_number_of [symmetric] real_of_int_power) - -declare power_real_number_of [of _ "number_of w", standard, simp] - subsection{* Squares of Reals *} @@ -93,9 +55,6 @@ lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" by simp -lemma real_mult_self_sum_ge_zero: "(0::real) \ x*x + y*y" -by (rule sum_squares_ge_zero) - lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" by (simp add: real_add_eq_0_iff [symmetric]) @@ -172,24 +131,7 @@ apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) done -lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))" -by simp - -lemma inverse_real_of_nat_ge_zero [simp]: "0 \ inverse (real (Suc n))" -by simp - lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))" by (case_tac "n", auto) -subsection{* Float syntax *} - -syntax "_Float" :: "float_const \ 'a" ("_") - -use "Tools/float_syntax.ML" -setup Float_Syntax.setup - -text{* Test: *} -lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)" -by simp - end diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/TLA/Action.thy Fri Feb 26 09:49:00 2010 +0100 @@ -33,7 +33,7 @@ syntax (* Syntax for writing action expressions in arbitrary contexts *) - "ACT" :: "lift => 'a" ("(ACT _)") + "_ACT" :: "lift => 'a" ("(ACT _)") "_before" :: "lift => lift" ("($_)" [100] 99) "_after" :: "lift => lift" ("(_$)" [100] 99) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/TLA/Intensional.thy Fri Feb 26 09:49:00 2010 +0100 @@ -51,7 +51,7 @@ "_holdsAt" :: "['a, lift] => bool" ("(_ |= _)" [100,10] 10) (* Syntax for lifted expressions outside the scope of |- or |= *) - "LIFT" :: "lift => 'a" ("LIFT _") + "_LIFT" :: "lift => 'a" ("LIFT _") (* generic syntax for lifted constants and functions *) "_const" :: "'a => lift" ("(#_)" [1000] 999) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/TLA/Stfun.thy --- a/src/HOL/TLA/Stfun.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/TLA/Stfun.thy Fri Feb 26 09:49:00 2010 +0100 @@ -35,7 +35,7 @@ stvars :: "'a stfun => bool" syntax - "PRED" :: "lift => 'a" ("PRED _") + "_PRED" :: "lift => 'a" ("PRED _") "_stvars" :: "lift => bool" ("basevars _") translations diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Feb 26 09:49:00 2010 +0100 @@ -75,7 +75,7 @@ val leafTs' = get_nonrec_types descr' sorts; val branchTs = get_branching_types descr' sorts; val branchT = if null branchTs then HOLogic.unitT - else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs; + else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) branchTs; val arities = remove (op =) 0 (get_arities descr'); val unneeded_vars = subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars); @@ -83,7 +83,7 @@ val recTs = get_rec_types descr' sorts; val (newTs, oldTs) = chop (length (hd descr)) recTs; val sumT = if null leafTs then HOLogic.unitT - else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs; + else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) leafTs; val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); val UnivT = HOLogic.mk_setT Univ_elT; val UnivT' = Univ_elT --> HOLogic.boolT; @@ -104,9 +104,9 @@ val Type (_, [T1, T2]) = T in if i <= n2 then - Const (@{const_name "Sum_Type.Inl"}, T1 --> T) $ (mk_inj' T1 n2 i) + Const (@{const_name Inl}, T1 --> T) $ (mk_inj' T1 n2 i) else - Const (@{const_name "Sum_Type.Inr"}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2)) + Const (@{const_name Inr}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2)) end in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs) end; @@ -731,7 +731,7 @@ in (names, specs) end; val parse_datatype_decl = - (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix -- + (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix))); val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Feb 26 09:49:00 2010 +0100 @@ -53,7 +53,7 @@ fun prove_casedist_thm (i, (T, t)) = let val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) => - Abs ("z", T', Const ("True", T''))) induct_Ps; + Abs ("z", T', Const (@{const_name True}, T''))) induct_Ps; val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $ Var (("P", 0), HOLogic.boolT)) val insts = take i dummyPs @ (P::(drop (i + 1) dummyPs)); @@ -200,7 +200,7 @@ val rec_unique_thms = let val rec_unique_ts = map (fn (((set_t, T1), T2), i) => - Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $ + Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $ absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2))) (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs)); val cert = cterm_of thy1 @@ -236,7 +236,7 @@ (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, - Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', + Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) ||> Sign.parent_path @@ -416,7 +416,7 @@ fun prove_case_cong ((t, nchotomy), case_rewrites) = let val (Const ("==>", _) $ tm $ _) = t; - val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm; + val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ Ma)) = tm; val cert = cterm_of thy; val nchotomy' = nchotomy RS spec; val [v] = Term.add_vars (concl_of nchotomy') []; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Feb 26 09:49:00 2010 +0100 @@ -120,8 +120,8 @@ fun split_conj_thm th = ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th]; -val mk_conj = foldr1 (HOLogic.mk_binop "op &"); -val mk_disj = foldr1 (HOLogic.mk_binop "op |"); +val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"}); +val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"}); fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0)); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Feb 26 09:49:00 2010 +0100 @@ -76,7 +76,7 @@ fun mk_fun_constrain tT t = Syntax.const @{syntax_const "_constrain"} $ t $ - (Syntax.free "fun" $ tT $ Syntax.free "dummy"); (* FIXME @{type_syntax} (!?) *) + (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy}); (*--------------------------------------------------------------------------- diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Feb 26 09:49:00 2010 +0100 @@ -236,7 +236,7 @@ (** document antiquotation **) -val _ = ThyOutput.antiquotation "datatype" Args.tyname +val _ = ThyOutput.antiquotation "datatype" (Args.type_name true) (fn {source = src, context = ctxt, ...} => fn dtco => let val thy = ProofContext.theory_of ctxt; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Feb 26 09:49:00 2010 +0100 @@ -70,7 +70,7 @@ val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts); in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')), - foldr1 (HOLogic.mk_binop "op &") + foldr1 (HOLogic.mk_binop @{const_name "op &"}) (map HOLogic.mk_eq (frees ~~ frees'))))) end; in @@ -149,7 +149,7 @@ val prems = maps (fn ((i, (_, _, constrs)), T) => map (make_ind_prem i T) constrs) (descr' ~~ recTs); val tnames = make_tnames recTs; - val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") + val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"}) (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T)) (descr' ~~ recTs ~~ tnames))) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Feb 26 09:49:00 2010 +0100 @@ -16,10 +16,11 @@ open Datatype_Aux; -fun subsets i j = if i <= j then - let val is = subsets (i+1) j - in map (fn ks => i::ks) is @ is end - else [[]]; +fun subsets i j = + if i <= j then + let val is = subsets (i+1) j + in map (fn ks => i::ks) is @ is end + else [[]]; fun forall_intr_prf (t, prf) = let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) @@ -102,7 +103,7 @@ if i mem is then SOME (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T)) else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames)); - val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") + val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"}) (map (fn ((((i, _), T), U), tname) => make_pred i U T (mk_proj i is r) (Free (tname, T))) (descr ~~ recTs ~~ rec_result_Ts ~~ tnames))); @@ -129,8 +130,8 @@ val ivs = rev (Term.add_vars (Logic.varify (Datatype_Prop.make_ind [descr] sorts)) []); val rvs = rev (Thm.fold_terms Term.add_vars thm' []); - val ivs1 = map Var (filter_out (fn (_, T) => - tname_of (body_type T) mem ["set", "bool"]) ivs); + val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *) + tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs); val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs; val prf = diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Fri Feb 26 09:49:00 2010 +0100 @@ -2,6 +2,9 @@ * Added and implemented "binary_ints" and "bits" options * Added "std" option and implemented support for nonstandard models + * Added support for quotient types + * Added support for local definitions + * Optimized "Multiset.multiset" * Fixed soundness bugs related to "destroy_constrs" optimization and record getters * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Fri Feb 26 09:49:00 2010 +0100 @@ -158,7 +158,7 @@ datatype outcome = NotInstalled | - Normal of (int * raw_bound list) list * int list | + Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Interrupted of int list option | Error of string * int list @@ -304,7 +304,7 @@ datatype outcome = NotInstalled | - Normal of (int * raw_bound list) list * int list | + Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Interrupted of int list option | Error of string * int list @@ -938,13 +938,13 @@ $$ "{" |-- scan_list scan_assignment --| $$ "}" (* string -> raw_bound list *) -fun parse_instance inst = - Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise SYNTAX ("Kodkod.parse_instance", - "ill-formed Kodkodi output")) - scan_instance)) - (strip_blanks (explode inst)) - |> fst +val parse_instance = + fst o Scan.finite Symbol.stopper + (Scan.error (!! (fn _ => + raise SYNTAX ("Kodkod.parse_instance", + "ill-formed Kodkodi output")) + scan_instance)) + o strip_blanks o explode val problem_marker = "*** PROBLEM " val outcome_marker = "---OUTCOME---\n" @@ -1029,7 +1029,7 @@ val reindex = fst o nth indexed_problems in if null indexed_problems then - Normal ([], triv_js) + Normal ([], triv_js, "") else let val (serial_str, temp_dir) = @@ -1089,6 +1089,8 @@ if null ps then if code = 2 then TimedOut js + else if code = 0 then + Normal ([], js, first_error) else if first_error |> Substring.full |> Substring.position "NoClassDefFoundError" |> snd |> Substring.isEmpty |> not then @@ -1098,12 +1100,10 @@ |> perhaps (try (unprefix "Error: ")), js) else if io_error then Error ("I/O error", js) - else if code <> 0 then + else Error ("Unknown error", js) - else - Normal ([], js) else - Normal (ps, js) + Normal (ps, js, first_error) end in remove_temporary_files (); outcome end handle Exn.Interrupt => diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Nitpick/minipick.ML --- a/src/HOL/Tools/Nitpick/minipick.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Nitpick/minipick.ML Fri Feb 26 09:49:00 2010 +0100 @@ -321,7 +321,7 @@ in case solve_any_problem overlord NONE max_threads max_solutions problems of NotInstalled => "unknown" - | Normal ([], _) => "none" + | Normal ([], _, _) => "none" | Normal _ => "genuine" | TimedOut _ => "unknown" | Interrupted _ => "unknown" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 26 09:49:00 2010 +0100 @@ -58,8 +58,8 @@ val register_codatatype : typ -> string -> styp list -> theory -> theory val unregister_codatatype : typ -> theory -> theory val pick_nits_in_term : - Proof.state -> params -> bool -> int -> int -> int -> term list -> term - -> string * Proof.state + Proof.state -> params -> bool -> int -> int -> int -> (term * term) list + -> term list -> term -> string * Proof.state val pick_nits_in_subgoal : Proof.state -> params -> bool -> int -> int -> string * Proof.state end; @@ -187,10 +187,10 @@ (* (unit -> string) -> Pretty.T *) fun plazy f = Pretty.blk (0, pstrs (f ())) -(* Time.time -> Proof.state -> params -> bool -> int -> int -> int -> term - -> string * Proof.state *) +(* Time.time -> Proof.state -> params -> bool -> int -> int -> int + -> (term * term) list -> term list -> term -> string * Proof.state *) fun pick_them_nits_in_term deadline state (params : params) auto i n step - orig_assm_ts orig_t = + subst orig_assm_ts orig_t = let val timer = Timer.startRealTimer () val thy = Proof.theory_of state @@ -237,6 +237,7 @@ if passed_deadline deadline then raise TimeLimit.TimeOut else raise Interrupt + val orig_assm_ts = if assms orelse auto then orig_assm_ts else [] val _ = if step = 0 then print_m (fn () => "Nitpicking formula...") @@ -249,10 +250,7 @@ "goal")) [Logic.list_implies (orig_assm_ts, orig_t)])) val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) else orig_t - val assms_t = if assms orelse auto then - Logic.mk_conjunction_list (neg_t :: orig_assm_ts) - else - neg_t + val assms_t = Logic.mk_conjunction_list (neg_t :: orig_assm_ts) val (assms_t, evals) = assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms |> pairf hd tl @@ -265,12 +263,12 @@ *) val max_bisim_depth = fold Integer.max bisim_depths ~1 val case_names = case_const_names thy stds - val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy - val def_table = const_def_table ctxt defs + val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst + val def_table = const_def_table ctxt subst defs val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) - val simp_table = Unsynchronized.ref (const_simp_table ctxt) - val psimp_table = const_psimp_table ctxt - val intro_table = inductive_intro_table ctxt def_table + val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) + val psimp_table = const_psimp_table ctxt subst + val intro_table = inductive_intro_table ctxt subst def_table val ground_thm_table = ground_theorem_table thy val ersatz_table = ersatz_table thy val (hol_ctxt as {wf_cache, ...}) = @@ -412,7 +410,7 @@ if sat_solver <> "smart" then if need_incremental andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true) - sat_solver) then + sat_solver) then (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ \be used instead of " ^ quote sat_solver ^ ".")); "SAT4J") @@ -581,6 +579,9 @@ fun update_checked_problems problems = List.app (Unsynchronized.change checked_problems o Option.map o cons o nth problems) + (* string -> unit *) + fun show_kodkod_warning "" = () + | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") (* bool -> KK.raw_bound list -> problem_extension -> bool option *) fun print_and_check_model genuine bounds @@ -701,15 +702,16 @@ KK.NotInstalled => (print_m install_kodkodi_message; (max_potential, max_genuine, donno + 1)) - | KK.Normal ([], unsat_js) => - (update_checked_problems problems unsat_js; + | KK.Normal ([], unsat_js, s) => + (update_checked_problems problems unsat_js; show_kodkod_warning s; (max_potential, max_genuine, donno)) - | KK.Normal (sat_ps, unsat_js) => + | KK.Normal (sat_ps, unsat_js, s) => let val (lib_ps, con_ps) = List.partition (#unsound o snd o nth problems o fst) sat_ps in update_checked_problems problems (unsat_js @ map fst lib_ps); + show_kodkod_warning s; if null con_ps then let val num_genuine = take max_potential lib_ps @@ -937,10 +939,10 @@ else error "Nitpick was interrupted." -(* Proof.state -> params -> bool -> int -> int -> int -> term - -> string * Proof.state *) +(* Proof.state -> params -> bool -> int -> int -> int -> (term * term) list + -> term list -> term -> string * Proof.state *) fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n - step orig_assm_ts orig_t = + step subst orig_assm_ts orig_t = if getenv "KODKODI" = "" then (if auto then () else warning (Pretty.string_of (plazy install_kodkodi_message)); @@ -950,13 +952,27 @@ val deadline = Option.map (curry Time.+ (Time.now ())) timeout val outcome as (outcome_code, _) = time_limit (if debug then NONE else timeout) - (pick_them_nits_in_term deadline state params auto i n step + (pick_them_nits_in_term deadline state params auto i n step subst orig_assm_ts) orig_t in if expect = "" orelse outcome_code = expect then outcome else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") end +(* string list -> term -> bool *) +fun is_fixed_equation fixes + (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = + member (op =) fixes s + | is_fixed_equation _ _ = false +(* Proof.context -> term list * term -> (term * term) list * term list * term *) +fun extract_fixed_frees ctxt (assms, t) = + let + val fixes = Variable.fixes_of ctxt |> map snd + val (subst, other_assms) = + List.partition (is_fixed_equation fixes) assms + |>> map Logic.dest_equals + in (subst, other_assms, subst_atomic subst t) end + (* Proof.state -> params -> bool -> int -> int -> string * Proof.state *) fun pick_nits_in_subgoal state params auto i step = let @@ -967,12 +983,11 @@ 0 => (priority "No subgoal!"; ("none", state)) | n => let + val (t, frees) = Logic.goal_params t i + val t = subst_bounds (frees, t) val assms = map term_of (Assumption.all_assms_of ctxt) - val (t, frees) = Logic.goal_params t i - in - pick_nits_in_term state params auto i n step assms - (subst_bounds (frees, t)) - end + val (subst, assms, t) = extract_fixed_frees ctxt (assms, t) + in pick_nits_in_term state params auto i n step subst assms t end end end; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 26 09:49:00 2010 +0100 @@ -155,7 +155,8 @@ val is_finite_type : hol_context -> typ -> bool val special_bounds : term list -> (indexname * typ) list val is_funky_typedef : theory -> typ -> bool - val all_axioms_of : theory -> term list * term list * term list + val all_axioms_of : + theory -> (term * term) list -> term list * term list * term list val arity_of_built_in_const : theory -> (typ option * bool) list -> bool -> styp -> int option val is_built_in_const : @@ -163,11 +164,13 @@ val term_under_def : term -> term val case_const_names : theory -> (typ option * bool) list -> (string * int) list - val const_def_table : Proof.context -> term list -> const_table + val const_def_table : + Proof.context -> (term * term) list -> term list -> const_table val const_nondef_table : term list -> const_table - val const_simp_table : Proof.context -> const_table - val const_psimp_table : Proof.context -> const_table - val inductive_intro_table : Proof.context -> const_table -> const_table + val const_simp_table : Proof.context -> (term * term) list -> const_table + val const_psimp_table : Proof.context -> (term * term) list -> const_table + val inductive_intro_table : + Proof.context -> (term * term) list -> const_table -> const_table val ground_theorem_table : theory -> term list Inttab.table val ersatz_table : theory -> (string * string) list val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit @@ -619,12 +622,19 @@ fun is_univ_typedef thy (Type (s, _)) = (case typedef_info thy s of SOME {set_def, prop_of_Rep, ...} => - (case set_def of - SOME thm => - try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm - | NONE => - try (fst o dest_Const o snd o HOLogic.dest_mem - o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top} + let + val t_opt = + case set_def of + SOME thm => try (snd o Logic.dest_equals o prop_of) thm + | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) + prop_of_Rep + in + case t_opt of + SOME (Const (@{const_name top}, _)) => true + | SOME (Const (@{const_name Collect}, _) + $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true + | _ => false + end | NONE => false) | is_univ_typedef _ _ = false (* theory -> (typ option * bool) list -> typ -> bool *) @@ -1166,11 +1176,12 @@ | do_eq _ = false in do_eq end -(* theory -> term list * term list * term list *) -fun all_axioms_of thy = +(* theory -> (term * term) list -> term list * term list * term list *) +fun all_axioms_of thy subst = let (* theory list -> term list *) - val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of) + val axioms_of_thys = + maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of)) val specs = Defs.all_specifications_of (Theory.defs_of thy) val def_names = specs |> maps snd |> map_filter #def |> OrdList.make fast_string_ord @@ -1317,12 +1328,13 @@ fun pair_for_prop t = case term_under_def t of Const (s, _) => (s, t) - | Free _ => raise NOT_SUPPORTED "local definitions" | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) -(* (Proof.context -> term list) -> Proof.context -> const_table *) -fun table_for get ctxt = - get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make +(* (Proof.context -> term list) -> Proof.context -> (term * term) list + -> const_table *) +fun table_for get ctxt subst = + ctxt |> get |> map (pair_for_prop o subst_atomic subst) + |> AList.group (op =) |> Symtab.make (* theory -> (typ option * bool) list -> (string * int) list *) fun case_const_names thy stds = @@ -1335,23 +1347,23 @@ (Datatype.get_all thy) [] @ map (apsnd length o snd) (#codatatypes (Data.get thy)) -(* Proof.context -> term list -> const_table *) -fun const_def_table ctxt ts = - table_for (map prop_of o Nitpick_Defs.get) ctxt +(* Proof.context -> (term * term) list -> term list -> const_table *) +fun const_def_table ctxt subst ts = + table_for (map prop_of o Nitpick_Defs.get) ctxt subst |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) (map pair_for_prop ts) (* term list -> const_table *) fun const_nondef_table ts = fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] |> AList.group (op =) |> Symtab.make -(* Proof.context -> const_table *) +(* Proof.context -> (term * term) list -> const_table *) val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) -(* Proof.context -> const_table -> const_table *) -fun inductive_intro_table ctxt def_table = +(* Proof.context -> (term * term) list -> const_table -> const_table *) +fun inductive_intro_table ctxt subst def_table = table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) def_table o prop_of) - o Nitpick_Intros.get) ctxt + o Nitpick_Intros.get) ctxt subst (* theory -> term list Inttab.table *) fun ground_theorem_table thy = fold ((fn @{const Trueprop} $ t1 => diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Feb 26 09:49:00 2010 +0100 @@ -325,7 +325,7 @@ fun run_all_tests () = case Kodkod.solve_any_problem false NONE 0 1 (map (problem_for_nut @{context}) tests) of - Kodkod.Normal ([], _) => () + Kodkod.Normal ([], _, _) => () | _ => error "Tests failed" end; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Feb 26 09:49:00 2010 +0100 @@ -296,7 +296,7 @@ val quotspec_parser = OuterParse.and_list1 ((OuterParse.type_args -- OuterParse.binding) -- - OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- + OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- (OuterParse.$$$ "/" |-- OuterParse.term)) val _ = OuterKeyword.keyword "/" diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/TFL/post.ML Fri Feb 26 09:49:00 2010 +0100 @@ -125,7 +125,7 @@ (*lcp: curry the predicate of the induction rule*) fun curry_rule rl = - SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; + Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; (*lcp: put a theorem into Isabelle form, using meta-level connectives*) val meta_outer = diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/inductive.ML Fri Feb 26 09:49:00 2010 +0100 @@ -183,7 +183,7 @@ in case concl_of thm of Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq) - | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm + | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) => dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm)) @@ -300,7 +300,7 @@ else err_in_prem ctxt err_name rule prem "Non-atomic premise"; in (case concl of - Const ("Trueprop", _) $ t => + Const (@{const_name Trueprop}, _) $ t => if head_of t mem cs then (check_ind (err_in_rule ctxt err_name rule') t; List.app check_prem (prems ~~ aprems)) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Feb 26 09:49:00 2010 +0100 @@ -52,12 +52,13 @@ fun thyname_of s = (case optmod of NONE => Codegen.thyname_of_const thy s | SOME s => s); in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of - SOME (Const ("op =", _), [t, _]) => (case head_of t of - Const (s, _) => - CodegenData.put {intros = intros, graph = graph, - eqns = eqns |> Symtab.map_default (s, []) - (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy - | _ => (warn thm; thy)) + SOME (Const (@{const_name "op ="}, _), [t, _]) => + (case head_of t of + Const (s, _) => + CodegenData.put {intros = intros, graph = graph, + eqns = eqns |> Symtab.map_default (s, []) + (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy + | _ => (warn thm; thy)) | SOME (Const (s, _), _) => let val cs = fold Term.add_const_names (Thm.prems_of thm) []; @@ -187,7 +188,7 @@ end)) (AList.lookup op = modes name) in (case strip_comb t of - (Const ("op =", Type (_, [T, _])), _) => + (Const (@{const_name "op ="}, Type (_, [T, _])), _) => [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @ (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else []) | (Const (name, _), args) => the_default default (mk_modes name args) @@ -578,17 +579,20 @@ fun get_nparms s = if s mem names then SOME nparms else Option.map #3 (get_clauses thy s); - fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true) - | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq, false) + fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) = + Prem ([t], Envir.beta_eta_contract u, true) + | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) = + Prem ([t, u], eq, false) | dest_prem (_ $ t) = (case strip_comb t of - (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t - | (c as Const (s, _), ts) => (case get_nparms s of - NONE => Sidecond t - | SOME k => - let val (ts1, ts2) = chop k ts - in Prem (ts2, list_comb (c, ts1), false) end) - | _ => Sidecond t); + (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t + | (c as Const (s, _), ts) => + (case get_nparms s of + NONE => Sidecond t + | SOME k => + let val (ts1, ts2) = chop k ts + in Prem (ts2, list_comb (c, ts1), false) end) + | _ => Sidecond t); fun add_clause intr (clauses, arities) = let @@ -601,7 +605,7 @@ (AList.update op = (name, these (AList.lookup op = clauses name) @ [(ts2, prems)]) clauses, AList.update op = (name, (map (fn U => (case strip_type U of - (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs) + (Rs as _ :: _, @{typ bool}) => SOME (length Rs) | _ => NONE)) Ts, length Us)) arities) end; @@ -633,7 +637,7 @@ val (ts1, ts2) = chop k ts; val u = list_comb (Const (s, T), ts1); - fun mk_mode (Const ("dummy_pattern", _)) ((ts, mode), i) = ((ts, mode), i + 1) + fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1) | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1); val module' = if_library thyname module; @@ -716,7 +720,7 @@ end; fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of - (Const ("Collect", _), [u]) => + (Const (@{const_name Collect}, _), [u]) => let val (r, Ts, fs) = HOLogic.strip_psplits u in case strip_comb r of (Const (s, T), ts) => diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Feb 26 09:49:00 2010 +0100 @@ -21,7 +21,7 @@ [name] => name | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm)); -val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); +val all_simps = map (symmetric o mk_meta_eq) @{thms HOL.all_simps}; fun prf_of thm = let @@ -57,7 +57,7 @@ fun relevant_vars prop = List.foldr (fn (Var ((a, i), T), vs) => (case strip_type T of - (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs + (_, Type (s, _)) => if s mem [@{type_name bool}] then (a, T) :: vs else vs | _ => vs) | (_, vs) => vs) [] (OldTerm.term_vars prop); @@ -150,9 +150,10 @@ fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q - | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of - Const (s, _) => can (Inductive.the_inductive ctxt) s - | _ => true) + | is_meta (Const (@{const_name Trueprop}, _) $ t) = + (case head_of t of + Const (s, _) => can (Inductive.the_inductive ctxt) s + | _ => true) | is_meta _ = false; fun fun_of ts rts args used (prem :: prems) = @@ -174,7 +175,7 @@ (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems' end else (case strip_type T of - (Ts, Type ("*", [T1, T2])) => + (Ts, Type (@{type_name "*"}, [T1, T2])) => let val fx = Free (x, Ts ---> T1); val fr = Free (r, Ts ---> T2); @@ -211,8 +212,9 @@ let val fs = map (fn (rule, (ivs, intr)) => fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs) - in if dummy then Const ("HOL.default_class.default", - HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs + in + if dummy then Const (@{const_name default}, + HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs else fs end) (premss ~~ dummies); val frees = fold Term.add_frees fs []; @@ -439,7 +441,7 @@ val r = if null Ps then Extraction.nullt else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T), (if dummy then - [Abs ("x", HOLogic.unitT, Const ("HOL.default_class.default", body_type T))] + [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))] else []) @ map reorder2 (intrs ~~ (length prems - 1 downto 0)) @ [Bound (length prems)])); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/inductive_set.ML Fri Feb 26 09:49:00 2010 +0100 @@ -33,10 +33,10 @@ val collect_mem_simproc = Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss => - fn S as Const ("Collect", Type ("fun", [_, T])) $ t => + fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t => let val (u, _, ps) = HOLogic.strip_psplits t in case u of - (c as Const ("op :", _)) $ q $ S' => + (c as Const (@{const_name "op :"}, _)) $ q $ S' => (case try (HOLogic.strip_ptuple ps) q of NONE => NONE | SOME ts => @@ -74,18 +74,20 @@ in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs)) (p (fold (Logic.all o Var) vs t) f) end; - fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x) - | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x) + fun mkop @{const_name "op &"} T x = + SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x) + | mkop @{const_name "op |"} T x = + SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x) | mkop _ _ _ = NONE; fun mk_collect p T t = let val U = HOLogic.dest_setT T in HOLogic.Collect_const U $ HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t end; - fun decomp (Const (s, _) $ ((m as Const ("op :", + fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"}, Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) = mkop s T (m, p, S, mk_collect p T (head_of u)) - | decomp (Const (s, _) $ u $ ((m as Const ("op :", + | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"}, Type (_, [_, Type (_, [T, _])]))) $ p $ S)) = mkop s T (m, p, mk_collect p T (head_of u), S) | decomp _ = NONE; @@ -263,13 +265,13 @@ fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) = case prop_of thm of - Const ("Trueprop", _) $ (Const ("op =", Type (_, [T, _])) $ lhs $ rhs) => + Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) => (case body_type T of - Type ("bool", []) => + @{typ bool} => let val thy = Context.theory_of ctxt; fun factors_of t fs = case strip_abs_body t of - Const ("op :", _) $ u $ S => + Const (@{const_name "op :"}, _) $ u $ S => if is_Free S orelse is_Var S then let val ps = HOLogic.flat_tuple_paths u in (SOME ps, (S, ps) :: fs) end @@ -279,7 +281,7 @@ val (pfs, fs) = fold_map factors_of ts []; val ((h', ts'), fs') = (case rhs of Abs _ => (case strip_abs_body rhs of - Const ("op :", _) $ u $ S => + Const (@{const_name "op :"}, _) $ u $ S => (strip_comb S, SOME (HOLogic.flat_tuple_paths u)) | _ => error "member symbol on right-hand side expected") | _ => (strip_comb rhs, NONE)) @@ -412,7 +414,7 @@ val {set_arities, pred_arities, to_pred_simps, ...} = PredSetConvData.get (Context.Proof lthy); fun infer (Abs (_, _, t)) = infer t - | infer (Const ("op :", _) $ t $ u) = + | infer (Const (@{const_name "op :"}, _) $ t $ u) = infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u) | infer (t $ u) = infer t #> infer u | infer _ = I; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/numeral_syntax.ML --- a/src/HOL/Tools/numeral_syntax.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/numeral_syntax.ML Fri Feb 26 09:49:00 2010 +0100 @@ -69,7 +69,7 @@ in -fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) = (* FIXME @{type_syntax} *) +fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) = let val t' = if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/record.ML Fri Feb 26 09:49:00 2010 +0100 @@ -762,8 +762,7 @@ mk_ext (field_types_tr t) end; -(* FIXME @{type_syntax} *) -fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const "Product_Type.unit") ctxt t +fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t | record_type_tr _ ts = raise TERM ("record_type_tr", ts); fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/simpdata.ML Fri Feb 26 09:49:00 2010 +0100 @@ -10,11 +10,11 @@ structure Quantifier1 = Quantifier1Fun (struct (*abstract syntax*) - fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t) + fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t) | dest_eq _ = NONE; - fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t) + fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t) | dest_conj _ = NONE; - fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t) + fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t) | dest_imp _ = NONE; val conj = HOLogic.conj val imp = HOLogic.imp @@ -43,9 +43,9 @@ fun mk_eq th = case concl_of th (*expects Trueprop if not == *) - of Const ("==",_) $ _ $ _ => th - | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq th - | _ $ (Const ("Not", _) $ _) => th RS @{thm Eq_FalseI} + of Const (@{const_name "=="},_) $ _ $ _ => th + | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th + | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI} | _ => th RS @{thm Eq_TrueI} fun mk_eq_True r = @@ -57,7 +57,7 @@ fun lift_meta_eq_to_obj_eq i st = let - fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q + fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q | count_imp _ = 0; val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) in if j = 0 then @{thm meta_eq_to_obj_eq} @@ -65,7 +65,7 @@ let val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); fun mk_simp_implies Q = fold_rev (fn R => fn S => - Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Ps Q + Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps Q val aT = TFree ("'a", HOLogic.typeS); val x = Free ("x", aT); val y = Free ("y", aT) @@ -98,7 +98,7 @@ else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm]; in case concl_of thm - of Const ("Trueprop", _) $ p => (case head_of p + of Const (@{const_name Trueprop}, _) $ p => (case head_of p of Const (a, _) => (case AList.lookup (op =) pairs a of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm]) | NONE => [thm]) @@ -159,9 +159,12 @@ (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())"); val mksimps_pairs = - [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]), - ("All", [@{thm spec}]), ("True", []), ("False", []), - ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])]; + [(@{const_name "op -->"}, [@{thm mp}]), + (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]), + (@{const_name All}, [@{thm spec}]), + (@{const_name True}, []), + (@{const_name False}, []), + (@{const_name If}, [@{thm if_bool_eq_conj} RS @{thm iffD1}])]; val HOL_basic_ss = Simplifier.global_context @{theory} empty_ss diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/split_rule.ML Fri Feb 26 09:49:00 2010 +0100 @@ -4,49 +4,34 @@ Some tools for managing tupled arguments and abstractions in rules. *) -signature BASIC_SPLIT_RULE = +signature SPLIT_RULE = sig + val split_rule_var: term -> thm -> thm + val split_rule_goal: Proof.context -> string list list -> thm -> thm val split_rule: thm -> thm val complete_split_rule: thm -> thm -end; - -signature SPLIT_RULE = -sig - include BASIC_SPLIT_RULE - val split_rule_var: term -> thm -> thm - val split_rule_goal: Proof.context -> string list list -> thm -> thm val setup: theory -> theory end; -structure SplitRule: SPLIT_RULE = +structure Split_Rule: SPLIT_RULE = struct - - -(** theory context references **) - -val split_conv = thm "split_conv"; -val fst_conv = thm "fst_conv"; -val snd_conv = thm "snd_conv"; - -fun internal_split_const (Ta, Tb, Tc) = - Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc); - -val internal_split_def = thm "internal_split_def"; -val internal_split_conv = thm "internal_split_conv"; - - - (** split rules **) -val eval_internal_split = hol_simplify [internal_split_def] o hol_simplify [internal_split_conv]; +fun internal_split_const (Ta, Tb, Tc) = + Const (@{const_name Product_Type.internal_split}, + [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc); + +val eval_internal_split = + hol_simplify [@{thm internal_split_def}] o hol_simplify [@{thm internal_split_conv}]; + val remove_internal_split = eval_internal_split o split_all; (*In ap_split S T u, term u expects separate arguments for the factors of S, with result type T. The call creates a new term expecting one argument of type S.*) -fun ap_split (Type ("*", [T1, T2])) T3 u = +fun ap_split (Type (@{type_name "*"}, [T1, T2])) T3 u = internal_split_const (T1, T2, T3) $ Abs ("v", T1, ap_split T2 T3 @@ -127,7 +112,7 @@ THEN' hyp_subst_tac THEN' K prune_params_tac; -val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv]; +val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}]; fun split_rule_goal ctxt xss rl = let @@ -159,5 +144,3 @@ end; -structure BasicSplitRule: BASIC_SPLIT_RULE = SplitRule; -open BasicSplitRule; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/string_syntax.ML Fri Feb 26 09:49:00 2010 +0100 @@ -71,7 +71,7 @@ [] => Syntax.Appl [Syntax.Constant Syntax.constrainC, - Syntax.Constant @{const_syntax Nil}, Syntax.Constant "string"] (* FIXME @{type_syntax} *) + Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}] | cs => mk_string cs) | string_ast_tr asts = raise AST ("string_tr", asts); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Tools/typedef.ML Fri Feb 26 09:49:00 2010 +0100 @@ -255,7 +255,7 @@ (Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)) >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) => Toplevel.print o Toplevel.theory_to_proof diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/Typerep.thy Fri Feb 26 09:49:00 2010 +0100 @@ -25,15 +25,16 @@ fun typerep_tr (*"_TYPEREP"*) [ty] = Syntax.const @{const_syntax typerep} $ (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $ - (Syntax.const "itself" $ ty)) (* FIXME @{type_syntax} *) + (Syntax.const @{type_syntax itself} $ ty)) | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts); in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end *} typed_print_translation {* let - fun typerep_tr' show_sorts (*"typerep"*) (* FIXME @{type_syntax} *) - (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) = + fun typerep_tr' show_sorts (*"typerep"*) + (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _])) + (Const (@{const_syntax TYPE}, _) :: ts) = Term.list_comb (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts) | typerep_tr' _ T ts = raise Match; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/UNITY/SubstAx.thy Fri Feb 26 09:49:00 2010 +0100 @@ -17,8 +17,8 @@ LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) "A LeadsTo B == {F. F \ (reachable F \ A) leadsTo B}" -syntax (xsymbols) - "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \w " 60) +notation (xsymbols) + LeadsTo (infixl " \w " 60) text{*Resembles the previous definition of LeadsTo*} diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/UNITY/WFair.thy Fri Feb 26 09:49:00 2010 +0100 @@ -69,8 +69,8 @@ --{*predicate transformer: the largest set that leads to @{term B}*} "wlt F B == Union {A. F \ A leadsTo B}" -syntax (xsymbols) - "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\" 60) +notation (xsymbols) + leadsTo (infixl "\" 60) subsection{*transient*} diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/ex/Gauge_Integration.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Gauge_Integration.thy Fri Feb 26 09:49:00 2010 +0100 @@ -0,0 +1,573 @@ +(* Author: Jacques D. Fleuriot, University of Edinburgh + Conversion to Isar and new proofs by Lawrence C Paulson, 2004 + + Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy . +*) + +header{*Theory of Integration on real intervals*} + +theory Gauge_Integration +imports Complex_Main +begin + +text {* + +\textbf{Attention}: This theory defines the Integration on real +intervals. This is just a example theory for historical / expository interests. +A better replacement is found in the Multivariate Analysis library. This defines +the gauge integral on real vector spaces and in the Real Integral theory +is a specialization to the integral on arbitrary real intervals. The +Multivariate Analysis package also provides a better support for analysis on +integrals. + +*} + +text{*We follow John Harrison in formalizing the Gauge integral.*} + +subsection {* Gauges *} + +definition + gauge :: "[real set, real => real] => bool" where + [code del]:"gauge E g = (\x\E. 0 < g(x))" + + +subsection {* Gauge-fine divisions *} + +inductive + fine :: "[real \ real, real \ real, (real \ real \ real) list] \ bool" +for + \ :: "real \ real" +where + fine_Nil: + "fine \ (a, a) []" +| fine_Cons: + "\fine \ (b, c) D; a < b; a \ x; x \ b; b - a < \ x\ + \ fine \ (a, c) ((a, x, b) # D)" + +lemmas fine_induct [induct set: fine] = + fine.induct [of "\" "(a,b)" "D" "split P", unfolded split_conv, standard] + +lemma fine_single: + "\a < b; a \ x; x \ b; b - a < \ x\ \ fine \ (a, b) [(a, x, b)]" +by (rule fine_Cons [OF fine_Nil]) + +lemma fine_append: + "\fine \ (a, b) D; fine \ (b, c) D'\ \ fine \ (a, c) (D @ D')" +by (induct set: fine, simp, simp add: fine_Cons) + +lemma fine_imp_le: "fine \ (a, b) D \ a \ b" +by (induct set: fine, simp_all) + +lemma nonempty_fine_imp_less: "\fine \ (a, b) D; D \ []\ \ a < b" +apply (induct set: fine, simp) +apply (drule fine_imp_le, simp) +done + +lemma empty_fine_imp_eq: "\fine \ (a, b) D; D = []\ \ a = b" +by (induct set: fine, simp_all) + +lemma fine_eq: "fine \ (a, b) D \ a = b \ D = []" +apply (cases "D = []") +apply (drule (1) empty_fine_imp_eq, simp) +apply (drule (1) nonempty_fine_imp_less, simp) +done + +lemma mem_fine: + "\fine \ (a, b) D; (u, x, v) \ set D\ \ u < v \ u \ x \ x \ v" +by (induct set: fine, simp, force) + +lemma mem_fine2: "\fine \ (a, b) D; (u, z, v) \ set D\ \ a \ u \ v \ b" +apply (induct arbitrary: z u v set: fine, auto) +apply (simp add: fine_imp_le) +apply (erule order_trans [OF less_imp_le], simp) +done + +lemma mem_fine3: "\fine \ (a, b) D; (u, z, v) \ set D\ \ v - u < \ z" +by (induct arbitrary: z u v set: fine) auto + +lemma BOLZANO: + fixes P :: "real \ real \ bool" + assumes 1: "a \ b" + assumes 2: "\a b c. \P a b; P b c; a \ b; b \ c\ \ P a c" + assumes 3: "\x. \d>0. \a b. a \ x & x \ b & (b-a) < d \ P a b" + shows "P a b" +apply (subgoal_tac "split P (a,b)", simp) +apply (rule lemma_BOLZANO [OF _ _ 1]) +apply (clarify, erule (3) 2) +apply (clarify, rule 3) +done + +text{*We can always find a division that is fine wrt any gauge*} + +lemma fine_exists: + assumes "a \ b" and "gauge {a..b} \" shows "\D. fine \ (a, b) D" +proof - + { + fix u v :: real assume "u \ v" + have "a \ u \ v \ b \ \D. fine \ (u, v) D" + apply (induct u v rule: BOLZANO, rule `u \ v`) + apply (simp, fast intro: fine_append) + apply (case_tac "a \ x \ x \ b") + apply (rule_tac x="\ x" in exI) + apply (rule conjI) + apply (simp add: `gauge {a..b} \` [unfolded gauge_def]) + apply (clarify, rename_tac u v) + apply (case_tac "u = v") + apply (fast intro: fine_Nil) + apply (subgoal_tac "u < v", fast intro: fine_single, simp) + apply (rule_tac x="1" in exI, clarsimp) + done + } + with `a \ b` show ?thesis by auto +qed + +lemma fine_covers_all: + assumes "fine \ (a, c) D" and "a < x" and "x \ c" + shows "\ N < length D. \ d t e. D ! N = (d,t,e) \ d < x \ x \ e" + using assms +proof (induct set: fine) + case (2 b c D a t) + thus ?case + proof (cases "b < x") + case True + with 2 obtain N where *: "N < length D" + and **: "\ d t e. D ! N = (d,t,e) \ d < x \ x \ e" by auto + hence "Suc N < length ((a,t,b)#D) \ + (\ d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \ d < x \ x \ e)" by auto + thus ?thesis by auto + next + case False with 2 + have "0 < length ((a,t,b)#D) \ + (\ d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \ d < x \ x \ e)" by auto + thus ?thesis by auto + qed +qed auto + +lemma fine_append_split: + assumes "fine \ (a,b) D" and "D2 \ []" and "D = D1 @ D2" + shows "fine \ (a,fst (hd D2)) D1" (is "?fine1") + and "fine \ (fst (hd D2), b) D2" (is "?fine2") +proof - + from assms + have "?fine1 \ ?fine2" + proof (induct arbitrary: D1 D2) + case (2 b c D a' x D1 D2) + note induct = this + + thus ?case + proof (cases D1) + case Nil + hence "fst (hd D2) = a'" using 2 by auto + with fine_Cons[OF `fine \ (b,c) D` induct(3,4,5)] Nil induct + show ?thesis by (auto intro: fine_Nil) + next + case (Cons d1 D1') + with induct(2)[OF `D2 \ []`, of D1'] induct(8) + have "fine \ (b, fst (hd D2)) D1'" and "fine \ (fst (hd D2), c) D2" and + "d1 = (a', x, b)" by auto + with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons + show ?thesis by auto + qed + qed auto + thus ?fine1 and ?fine2 by auto +qed + +lemma fine_\_expand: + assumes "fine \ (a,b) D" + and "\ x. \ a \ x ; x \ b \ \ \ x \ \' x" + shows "fine \' (a,b) D" +using assms proof induct + case 1 show ?case by (rule fine_Nil) +next + case (2 b c D a x) + show ?case + proof (rule fine_Cons) + show "fine \' (b,c) D" using 2 by auto + from fine_imp_le[OF 2(1)] 2(6) `x \ b` + show "b - a < \' x" + using 2(7)[OF `a \ x`] by auto + qed (auto simp add: 2) +qed + +lemma fine_single_boundaries: + assumes "fine \ (a,b) D" and "D = [(d, t, e)]" + shows "a = d \ b = e" +using assms proof induct + case (2 b c D a x) + hence "D = []" and "a = d" and "b = e" by auto + moreover + from `fine \ (b,c) D` `D = []` have "b = c" + by (rule empty_fine_imp_eq) + ultimately show ?case by simp +qed auto + +lemma fine_listsum_eq_diff: + fixes f :: "real \ real" + shows "fine \ (a, b) D \ (\(u, x, v)\D. f v - f u) = f b - f a" +by (induct set: fine) simp_all + +text{*Lemmas about combining gauges*} + +lemma gauge_min: + "[| gauge(E) g1; gauge(E) g2 |] + ==> gauge(E) (%x. min (g1(x)) (g2(x)))" +by (simp add: gauge_def) + +lemma fine_min: + "fine (%x. min (g1(x)) (g2(x))) (a,b) D + ==> fine(g1) (a,b) D & fine(g2) (a,b) D" +apply (erule fine.induct) +apply (simp add: fine_Nil) +apply (simp add: fine_Cons) +done + +subsection {* Riemann sum *} + +definition + rsum :: "[(real \ real \ real) list, real \ real] \ real" where + "rsum D f = (\(u, x, v)\D. f x * (v - u))" + +lemma rsum_Nil [simp]: "rsum [] f = 0" +unfolding rsum_def by simp + +lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f" +unfolding rsum_def by simp + +lemma rsum_zero [simp]: "rsum D (\x. 0) = 0" +by (induct D, auto) + +lemma rsum_left_distrib: "rsum D f * c = rsum D (\x. f x * c)" +by (induct D, auto simp add: algebra_simps) + +lemma rsum_right_distrib: "c * rsum D f = rsum D (\x. c * f x)" +by (induct D, auto simp add: algebra_simps) + +lemma rsum_add: "rsum D (\x. f x + g x) = rsum D f + rsum D g" +by (induct D, auto simp add: algebra_simps) + +lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f" +unfolding rsum_def map_append listsum_append .. + + +subsection {* Gauge integrability (definite) *} + +definition + Integral :: "[(real*real),real=>real,real] => bool" where + [code del]: "Integral = (%(a,b) f k. \e > 0. + (\\. gauge {a .. b} \ & + (\D. fine \ (a,b) D --> + \rsum D f - k\ < e)))" + +lemma Integral_def2: + "Integral = (%(a,b) f k. \e>0. (\\. gauge {a..b} \ & + (\D. fine \ (a,b) D --> + \rsum D f - k\ \ e)))" +unfolding Integral_def +apply (safe intro!: ext) +apply (fast intro: less_imp_le) +apply (drule_tac x="e/2" in spec) +apply force +done + +text{*The integral is unique if it exists*} + +lemma Integral_unique: + "[| a \ b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2" +apply (simp add: Integral_def) +apply (drule_tac x = "\k1 - k2\ /2" in spec)+ +apply auto +apply (drule gauge_min, assumption) +apply (drule_tac \ = "%x. min (\ x) (\' x)" + in fine_exists, assumption, auto) +apply (drule fine_min) +apply (drule spec)+ +apply auto +apply (subgoal_tac "\(rsum D f - k2) - (rsum D f - k1)\ < \k1 - k2\") +apply arith +apply (drule add_strict_mono, assumption) +apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] + mult_less_cancel_right) +done + +lemma Integral_zero [simp]: "Integral(a,a) f 0" +apply (auto simp add: Integral_def) +apply (rule_tac x = "%x. 1" in exI) +apply (auto dest: fine_eq simp add: gauge_def rsum_def) +done + +lemma fine_rsum_const: "fine \ (a,b) D \ rsum D (\x. c) = (c * (b - a))" +unfolding rsum_def +by (induct set: fine, auto simp add: algebra_simps) + +lemma Integral_eq_diff_bounds: "a \ b ==> Integral(a,b) (%x. 1) (b - a)" +apply (cases "a = b", simp) +apply (simp add: Integral_def, clarify) +apply (rule_tac x = "%x. b - a" in exI) +apply (rule conjI, simp add: gauge_def) +apply (clarify) +apply (subst fine_rsum_const, assumption, simp) +done + +lemma Integral_mult_const: "a \ b ==> Integral(a,b) (%x. c) (c*(b - a))" +apply (cases "a = b", simp) +apply (simp add: Integral_def, clarify) +apply (rule_tac x = "%x. b - a" in exI) +apply (rule conjI, simp add: gauge_def) +apply (clarify) +apply (subst fine_rsum_const, assumption, simp) +done + +lemma Integral_mult: + "[| a \ b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)" +apply (auto simp add: order_le_less + dest: Integral_unique [OF order_refl Integral_zero]) +apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc) +apply (case_tac "c = 0", force) +apply (drule_tac x = "e/abs c" in spec) +apply (simp add: divide_pos_pos) +apply clarify +apply (rule_tac x="\" in exI, clarify) +apply (drule_tac x="D" in spec, clarify) +apply (simp add: pos_less_divide_eq abs_mult [symmetric] + algebra_simps rsum_right_distrib) +done + +lemma Integral_add: + assumes "Integral (a, b) f x1" + assumes "Integral (b, c) f x2" + assumes "a \ b" and "b \ c" + shows "Integral (a, c) f (x1 + x2)" +proof (cases "a < b \ b < c", simp only: Integral_def split_conv, rule allI, rule impI) + fix \ :: real assume "0 < \" + hence "0 < \ / 2" by auto + + assume "a < b \ b < c" + hence "a < b" and "b < c" by auto + + from `Integral (a, b) f x1`[simplified Integral_def split_conv, + rule_format, OF `0 < \/2`] + obtain \1 where \1_gauge: "gauge {a..b} \1" + and I1: "\ D. fine \1 (a,b) D \ \ rsum D f - x1 \ < (\ / 2)" by auto + + from `Integral (b, c) f x2`[simplified Integral_def split_conv, + rule_format, OF `0 < \/2`] + obtain \2 where \2_gauge: "gauge {b..c} \2" + and I2: "\ D. fine \2 (b,c) D \ \ rsum D f - x2 \ < (\ / 2)" by auto + + def \ \ "\ x. if x < b then min (\1 x) (b - x) + else if x = b then min (\1 b) (\2 b) + else min (\2 x) (x - b)" + + have "gauge {a..c} \" + using \1_gauge \2_gauge unfolding \_def gauge_def by auto + moreover { + fix D :: "(real \ real \ real) list" + assume fine: "fine \ (a,c) D" + from fine_covers_all[OF this `a < b` `b \ c`] + obtain N where "N < length D" + and *: "\ d t e. D ! N = (d, t, e) \ d < b \ b \ e" + by auto + obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto) + with * have "d < b" and "b \ e" by auto + have in_D: "(d, t, e) \ set D" + using D_eq[symmetric] using `N < length D` by auto + + from mem_fine[OF fine in_D] + have "d < e" and "d \ t" and "t \ e" by auto + + have "t = b" + proof (rule ccontr) + assume "t \ b" + with mem_fine3[OF fine in_D] `b \ e` `d \ t` `t \ e` `d < b` \_def + show False by (cases "t < b") auto + qed + + let ?D1 = "take N D" + let ?D2 = "drop N D" + def D1 \ "take N D @ [(d, t, b)]" + def D2 \ "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D" + + have "D \ []" using `N < length D` by auto + from hd_drop_conv_nth[OF this `N < length D`] + have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto + with fine_append_split[OF _ _ append_take_drop_id[symmetric]] + have fine1: "fine \ (a,d) ?D1" and fine2: "fine \ (d,c) ?D2" + using `N < length D` fine by auto + + have "fine \1 (a,b) D1" unfolding D1_def + proof (rule fine_append) + show "fine \1 (a, d) ?D1" + proof (rule fine1[THEN fine_\_expand]) + fix x assume "a \ x" "x \ d" + hence "x \ b" using `d < b` `x \ d` by auto + thus "\ x \ \1 x" unfolding \_def by auto + qed + + have "b - d < \1 t" + using mem_fine3[OF fine in_D] \_def `b \ e` `t = b` by auto + from `d < b` `d \ t` `t = b` this + show "fine \1 (d, b) [(d, t, b)]" using fine_single by auto + qed + note rsum1 = I1[OF this] + + have drop_split: "drop N D = [D ! N] @ drop (Suc N) D" + using nth_drop'[OF `N < length D`] by simp + + have fine2: "fine \2 (e,c) (drop (Suc N) D)" + proof (cases "drop (Suc N) D = []") + case True + note * = fine2[simplified drop_split True D_eq append_Nil2] + have "e = c" using fine_single_boundaries[OF * refl] by auto + thus ?thesis unfolding True using fine_Nil by auto + next + case False + note * = fine_append_split[OF fine2 False drop_split] + from fine_single_boundaries[OF *(1)] + have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto + with *(2) have "fine \ (e,c) (drop (Suc N) D)" by auto + thus ?thesis + proof (rule fine_\_expand) + fix x assume "e \ x" and "x \ c" + thus "\ x \ \2 x" using `b \ e` unfolding \_def by auto + qed + qed + + have "fine \2 (b, c) D2" + proof (cases "e = b") + case True thus ?thesis using fine2 by (simp add: D1_def D2_def) + next + case False + have "e - b < \2 b" + using mem_fine3[OF fine in_D] \_def `d < b` `t = b` by auto + with False `t = b` `b \ e` + show ?thesis using D2_def + by (auto intro!: fine_append[OF _ fine2] fine_single + simp del: append_Cons) + qed + note rsum2 = I2[OF this] + + have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f" + using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto + also have "\ = rsum D1 f + rsum D2 f" + by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps) + finally have "\rsum D f - (x1 + x2)\ < \" + using add_strict_mono[OF rsum1 rsum2] by simp + } + ultimately show "\ \. gauge {a .. c} \ \ + (\D. fine \ (a,c) D \ \rsum D f - (x1 + x2)\ < \)" + by blast +next + case False + hence "a = b \ b = c" using `a \ b` and `b \ c` by auto + thus ?thesis + proof (rule disjE) + assume "a = b" hence "x1 = 0" + using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto + thus ?thesis using `a = b` `Integral (b, c) f x2` by auto + next + assume "b = c" hence "x2 = 0" + using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto + thus ?thesis using `b = c` `Integral (a, b) f x1` by auto + qed +qed + +text{*Fundamental theorem of calculus (Part I)*} + +text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *} + +lemma strad1: + "\\z::real. z \ x \ \z - x\ < s \ + \(f z - f x) / (z - x) - f' x\ < e/2; + 0 < s; 0 < e; a \ x; x \ b\ + \ \z. \z - x\ < s -->\f z - f x - f' x * (z - x)\ \ e/2 * \z - x\" +apply clarify +apply (case_tac "z = x", simp) +apply (drule_tac x = z in spec) +apply (rule_tac z1 = "\inverse (z - x)\" + in real_mult_le_cancel_iff2 [THEN iffD1]) + apply simp +apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric] + mult_assoc [symmetric]) +apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) + = (f z - f x) / (z - x) - f' x") + apply (simp add: abs_mult [symmetric] mult_ac diff_minus) +apply (subst mult_commute) +apply (simp add: left_distrib diff_minus) +apply (simp add: mult_assoc divide_inverse) +apply (simp add: left_distrib) +done + +lemma lemma_straddle: + assumes f': "\x. a \ x & x \ b --> DERIV f x :> f'(x)" and "0 < e" + shows "\g. gauge {a..b} g & + (\x u v. a \ u & u \ x & x \ v & v \ b & (v - u) < g(x) + --> \(f(v) - f(u)) - (f'(x) * (v - u))\ \ e * (v - u))" +proof - + have "\x\{a..b}. + (\d > 0. \u v. u \ x & x \ v & (v - u) < d --> + \(f(v) - f(u)) - (f'(x) * (v - u))\ \ e * (v - u))" + proof (clarsimp) + fix x :: real assume "a \ x" and "x \ b" + with f' have "DERIV f x :> f'(x)" by simp + then have "\r>0. \s>0. \z. z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < r" + by (simp add: DERIV_iff2 LIM_eq) + with `0 < e` obtain s + where "\z. z \ x \ \z - x\ < s \ \(f z - f x) / (z - x) - f' x\ < e/2" and "0 < s" + by (drule_tac x="e/2" in spec, auto) + then have strad [rule_format]: + "\z. \z - x\ < s --> \f z - f x - f' x * (z - x)\ \ e/2 * \z - x\" + using `0 < e` `a \ x` `x \ b` by (rule strad1) + show "\d>0. \u v. u \ x \ x \ v \ v - u < d \ \f v - f u - f' x * (v - u)\ \ e * (v - u)" + proof (safe intro!: exI) + show "0 < s" by fact + next + fix u v :: real assume "u \ x" and "x \ v" and "v - u < s" + have "\f v - f u - f' x * (v - u)\ = + \(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\" + by (simp add: right_diff_distrib) + also have "\ \ \f v - f x - f' x * (v - x)\ + \f x - f u - f' x * (x - u)\" + by (rule abs_triangle_ineq) + also have "\ = \f v - f x - f' x * (v - x)\ + \f u - f x - f' x * (u - x)\" + by (simp add: right_diff_distrib) + also have "\ \ (e/2) * \v - x\ + (e/2) * \u - x\" + using `u \ x` `x \ v` `v - u < s` by (intro add_mono strad, simp_all) + also have "\ \ e * (v - u) / 2 + e * (v - u) / 2" + using `u \ x` `x \ v` `0 < e` by (intro add_mono, simp_all) + also have "\ = e * (v - u)" + by simp + finally show "\f v - f u - f' x * (v - u)\ \ e * (v - u)" . + qed + qed + thus ?thesis + by (simp add: gauge_def) (drule bchoice, auto) +qed + +lemma fundamental_theorem_of_calculus: + "\ a \ b; \x. a \ x & x \ b --> DERIV f x :> f'(x) \ + \ Integral(a,b) f' (f(b) - f(a))" + apply (drule order_le_imp_less_or_eq, auto) + apply (auto simp add: Integral_def2) + apply (drule_tac e = "e / (b - a)" in lemma_straddle) + apply (simp add: divide_pos_pos) + apply clarify + apply (rule_tac x="g" in exI, clarify) + apply (clarsimp simp add: rsum_def) + apply (frule fine_listsum_eq_diff [where f=f]) + apply (erule subst) + apply (subst listsum_subtractf [symmetric]) + apply (rule listsum_abs [THEN order_trans]) + apply (subst map_map [unfolded o_def]) + apply (subgoal_tac "e = (\(u, x, v)\D. (e / (b - a)) * (v - u))") + apply (erule ssubst) + apply (simp add: abs_minus_commute) + apply (rule listsum_mono) + apply (clarify, rename_tac u x v) + apply ((drule spec)+, erule mp) + apply (simp add: mem_fine mem_fine2 mem_fine3) + apply (frule fine_listsum_eq_diff [where f="\x. x"]) + apply (simp only: split_def) + apply (subst listsum_const_mult) + apply simp +done + +end diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/ex/HarmonicSeries.thy --- a/src/HOL/ex/HarmonicSeries.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/ex/HarmonicSeries.thy Fri Feb 26 09:49:00 2010 +0100 @@ -73,7 +73,8 @@ qed moreover from xs have "x \ 2^m" by auto ultimately have - "inverse (real x) \ inverse (real ((2::nat)^m))" by simp + "inverse (real x) \ inverse (real ((2::nat)^m))" + by (simp del: real_of_nat_power) moreover from xgt0 have "real x \ 0" by simp then have @@ -107,7 +108,7 @@ by (auto simp: tmdef dest: two_pow_sub) also have "\ = (real (2::nat))^(m - 1) / (real (2::nat))^m" - by (simp add: tmdef realpow_real_of_nat [symmetric]) + by (simp add: tmdef) also from mgt0 have "\ = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)" by auto @@ -319,4 +320,4 @@ ultimately show False by simp qed -end \ No newline at end of file +end diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/ex/Numeral.thy Fri Feb 26 09:49:00 2010 +0100 @@ -327,7 +327,7 @@ val k = int_of_num' n; val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k); in case T - of Type ("fun", [_, T']) => (* FIXME @{type_syntax} *) + of Type (@{type_syntax fun}, [_, T']) => if not (! show_types) andalso can Term.dest_Type T' then t' else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T' | T' => if T' = dummyT then t' else raise Match diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOL/ex/ROOT.ML Fri Feb 26 09:49:00 2010 +0100 @@ -67,7 +67,8 @@ "Quickcheck_Examples", "Landau", "Execute_Choice", - "Summation" + "Summation", + "Gauge_Integration" ]; HTML.with_charset "utf-8" (no_document use_thys) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOLCF/IOA/meta_theory/Pred.thy --- a/src/HOLCF/IOA/meta_theory/Pred.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOLCF/IOA/meta_theory/Pred.thy Fri Feb 26 09:49:00 2010 +0100 @@ -24,25 +24,25 @@ IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr ".-->" 25) -syntax ("" output) - "NOT" ::"'a predicate => 'a predicate" ("~ _" [40] 40) - "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "&" 35) - "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "|" 30) - "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "-->" 25) +notation (output) + NOT ("~ _" [40] 40) and + AND (infixr "&" 35) and + OR (infixr "|" 30) and + IMPLIES (infixr "-->" 25) -syntax (xsymbols output) - "NOT" ::"'a predicate => 'a predicate" ("\ _" [40] 40) - "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 35) - "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 30) - "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 25) +notation (xsymbols output) + NOT ("\ _" [40] 40) and + AND (infixr "\" 35) and + OR (infixr "\" 30) and + IMPLIES (infixr "\" 25) -syntax (xsymbols) - "satisfies" ::"'a => 'a predicate => bool" ("_ \ _" [100,9] 8) +notation (xsymbols) + satisfies ("_ \ _" [100,9] 8) -syntax (HTML output) - "NOT" ::"'a predicate => 'a predicate" ("\ _" [40] 40) - "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 35) - "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\" 30) +notation (HTML output) + NOT ("\ _" [40] 40) and + AND (infixr "\" 35) and + OR (infixr "\" 30) defs diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Fri Feb 26 09:49:00 2010 +0100 @@ -291,7 +291,7 @@ || Scan.succeed []; val domain_decl = - (type_args' -- P.binding -- P.opt_infix) -- + (type_args' -- P.binding -- P.opt_mixfix) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl); val domains_decl = diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Feb 26 09:49:00 2010 +0100 @@ -700,7 +700,7 @@ val parse_domain_iso : (string list * binding * mixfix * string * (binding * binding) option) parser = - (P.type_args -- P.binding -- P.opt_infix -- (P.$$$ "=" |-- P.typ) -- + (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))) >> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs)); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOLCF/Tools/pcpodef.ML Fri Feb 26 09:49:00 2010 +0100 @@ -340,7 +340,7 @@ Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/HOLCF/Tools/repdef.ML Fri Feb 26 09:49:00 2010 +0100 @@ -167,7 +167,7 @@ Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- + (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/Isar/args.ML Fri Feb 26 09:49:00 2010 +0100 @@ -54,7 +54,7 @@ val term: term context_parser val term_abbrev: term context_parser val prop: term context_parser - val tyname: string context_parser + val type_name: bool -> string context_parser val const: string context_parser val const_proper: string context_parser val bang_facts: thm list context_parser @@ -209,7 +209,8 @@ (* type and constant names *) -val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of) +fun type_name strict = + Scan.peek (fn ctxt => named_typ (ProofContext.read_type_name (Context.proof_of ctxt) strict)) >> (fn Type (c, _) => c | TFree (a, _) => a | _ => ""); val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Feb 26 09:49:00 2010 +0100 @@ -104,13 +104,13 @@ val _ = OuterSyntax.command "typedecl" "type declaration" K.thy_decl - (P.type_args -- P.binding -- P.opt_infix >> (fn ((args, a), mx) => + (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) => Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd))); val _ = OuterSyntax.command "types" "declare type abbreviations" K.thy_decl (Scan.repeat1 - (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) + (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix'))) >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/Isar/outer_parse.ML Fri Feb 26 09:49:00 2010 +0100 @@ -72,8 +72,6 @@ val typ: string parser val mixfix: mixfix parser val mixfix': mixfix parser - val opt_infix: mixfix parser - val opt_infix': mixfix parser val opt_mixfix: mixfix parser val opt_mixfix': mixfix parser val where_: string parser @@ -279,8 +277,6 @@ val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx); val mixfix' = annotation I (mfix || binder || infxl || infxr || infx); -val opt_infix = opt_annotation !!! (infxl || infxr || infx); -val opt_infix' = opt_annotation I (infxl || infxr || infx); val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx); val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Feb 26 09:49:00 2010 +0100 @@ -52,7 +52,7 @@ val infer_type: Proof.context -> string -> typ val inferred_param: string -> Proof.context -> typ * Proof.context val inferred_fixes: Proof.context -> (string * typ) list * Proof.context - val read_tyname: Proof.context -> string -> typ + val read_type_name: Proof.context -> bool -> string -> typ val read_const_proper: Proof.context -> string -> term val read_const: Proof.context -> string -> term val allow_dummies: Proof.context -> Proof.context @@ -414,7 +414,7 @@ in -fun read_tyname ctxt str = +fun read_type_name ctxt strict str = let val thy = theory_of ctxt; val (c, pos) = token_content str; @@ -425,8 +425,15 @@ else let val d = Sign.intern_type thy c; + val decl = Sign.the_type_decl thy d; val _ = Position.report (Markup.tycon d) pos; - in Type (d, replicate (Sign.arity_number thy d) dummyT) end + fun err () = error ("Bad type name: " ^ quote d); + val args = + (case decl of + Type.LogicalType n => n + | Type.Abbreviation (vs, _, _) => if strict then err () else length vs + | Type.Nonterminal => if strict then err () else 0); + in Type (d, replicate args dummyT) end end; fun read_const_proper ctxt = prep_const_proper ctxt o token_content; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Fri Feb 26 09:49:00 2010 +0100 @@ -103,14 +103,25 @@ "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))); -fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => - #1 (Term.dest_Type (ProofContext.read_tyname ctxt c)) - |> syn ? Long_Name.base_name - |> ML_Syntax.print_string)); +(* type constructors *) -val _ = inline "type_name" (type_ false); -val _ = inline "type_syntax" (type_ true); +fun type_const kind check = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => + let + val d = #1 (Term.dest_Type (ProofContext.read_type_name ctxt false c)); + val decl = Sign.the_type_decl (ProofContext.theory_of ctxt) d; + val s = + (case try check (d, decl) of + SOME s => s + | NONE => error ("Not a " ^ kind ^ ": " ^ quote d)); + in ML_Syntax.print_string s end); +val _ = inline "type_name" (type_const "logical type" (fn (d, Type.LogicalType _) => d)); +val _ = inline "type_abbrev" (type_const "type abbreviation" (fn (d, Type.Abbreviation _) => d)); +val _ = inline "nonterminal" (type_const "nonterminal" (fn (d, Type.Nonterminal) => d)); +val _ = inline "type_syntax" (type_const "type" (fn (d, _) => Long_Name.base_name d)); (* FIXME authentic syntax *) + + +(* constants *) fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c)) diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/Syntax/mixfix.ML Fri Feb 26 09:49:00 2010 +0100 @@ -101,20 +101,26 @@ fun syn_ext_types type_decls = let - fun mk_infix sy t p1 p2 p3 = - SynExt.Mfix ("(_ " ^ sy ^ "/ _)", - [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3); + fun mk_type n = replicate n SynExt.typeT ---> SynExt.typeT; + fun mk_infix sy n t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", mk_type n, t, [p1, p2], p3); fun mfix_of (_, _, NoSyn) = NONE - | mfix_of (t, 2, Infix (sy, p)) = SOME (mk_infix sy t (p + 1) (p + 1) p) - | mfix_of (t, 2, Infixl (sy, p)) = SOME (mk_infix sy t p (p + 1) p) - | mfix_of (t, 2, Infixr (sy, p)) = SOME (mk_infix sy t (p + 1) p p) - | mfix_of (t, _, _) = - error ("Bad mixfix declaration for type: " ^ quote t); (* FIXME printable!? *) + | mfix_of (t, n, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, mk_type n, t, ps, p)) + | mfix_of (t, n, Delimfix sy) = SOME (SynExt.Mfix (sy, mk_type n, t, [], SynExt.max_pri)) + | mfix_of (t, n, Infix (sy, p)) = SOME (mk_infix sy n t (p + 1) (p + 1) p) + | mfix_of (t, n, Infixl (sy, p)) = SOME (mk_infix sy n t p (p + 1) p) + | mfix_of (t, n, Infixr (sy, p)) = SOME (mk_infix sy n t (p + 1) p p) + | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); (* FIXME printable t (!?) *) - val mfix = map_filter mfix_of type_decls; + fun check_args (t, n, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) = + if SynExt.mfix_args sy = n then () + else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix + | check_args _ NONE = (); + + val mfix = map mfix_of type_decls; + val _ = map2 check_args type_decls mfix; val xconsts = map #1 type_decls; - in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end; + in SynExt.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end; (* syn_ext_consts *) @@ -140,7 +146,7 @@ | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p | mfix_of (c, ty, Binder (sy, p, q)) = [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)] - | mfix_of (c, _, _) = error ("Bad mixfix declaration for const: " ^ quote c); + | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); (* FIXME printable c (!?) *) fun binder (c, _, Binder _) = SOME (binder_name c, c) | binder _ = NONE; diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/Syntax/syn_ext.ML Fri Feb 26 09:49:00 2010 +0100 @@ -28,6 +28,8 @@ val cargs: string val any: string val sprop: string + datatype mfix = Mfix of string * typ * string * int list * int + val err_in_mfix: string -> mfix -> 'a val typ_to_nonterm: typ -> string datatype xsymb = Delim of string | @@ -37,7 +39,6 @@ datatype xprod = XProd of string * xsymb list * string * int val chain_pri: int val delims_of: xprod list -> string list list - datatype mfix = Mfix of string * typ * string * int list * int datatype syn_ext = SynExt of { xprods: xprod list, diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/sign.ML Fri Feb 26 09:49:00 2010 +0100 @@ -60,6 +60,7 @@ val intern_term: theory -> term -> term val extern_term: theory -> term -> term val intern_tycons: theory -> typ -> typ + val the_type_decl: theory -> string -> Type.decl val arity_number: theory -> string -> int val arity_sorts: theory -> string -> sort -> sort list val certify_class: theory -> class -> class @@ -308,6 +309,7 @@ (* certify wrt. type signature *) +val the_type_decl = Type.the_decl o tsig_of; val arity_number = Type.arity_number o tsig_of; fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Pure/type.ML --- a/src/Pure/type.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Pure/type.ML Fri Feb 26 09:49:00 2010 +0100 @@ -35,6 +35,7 @@ val get_mode: Proof.context -> mode val set_mode: mode -> Proof.context -> Proof.context val restore_mode: Proof.context -> Proof.context -> Proof.context + val the_decl: tsig -> string -> decl val cert_typ_mode: mode -> tsig -> typ -> typ val cert_typ: tsig -> typ -> typ val arity_number: tsig -> string -> int @@ -163,6 +164,11 @@ fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types; +fun the_decl tsig c = + (case lookup_type tsig c of + NONE => error (undecl_type c) + | SOME decl => decl); + (* certified types *) @@ -189,15 +195,14 @@ val Ts' = map cert Ts; fun nargs n = if length Ts <> n then err (bad_nargs c) else (); in - (case lookup_type tsig c of - SOME (LogicalType n) => (nargs n; Type (c, Ts')) - | SOME (Abbreviation (vs, U, syn)) => + (case the_decl tsig c of + LogicalType n => (nargs n; Type (c, Ts')) + | Abbreviation (vs, U, syn) => (nargs (length vs); if syn then check_logical c else (); if normalize then inst_typ (vs ~~ Ts') U else Type (c, Ts')) - | SOME Nonterminal => (nargs 0; check_logical c; T) - | NONE => err (undecl_type c)) + | Nonterminal => (nargs 0; check_logical c; T)) end | cert (TFree (x, S)) = TFree (x, cert_sort tsig S) | cert (TVar (xi as (_, i), S)) = diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Sequents/LK0.thy Fri Feb 26 09:49:00 2010 +0100 @@ -43,23 +43,23 @@ not_equal (infixl "~=" 50) where "x ~= y == ~ (x = y)" -syntax (xsymbols) - Not :: "o => o" ("\ _" [40] 40) - conj :: "[o, o] => o" (infixr "\" 35) - disj :: "[o, o] => o" (infixr "\" 30) - imp :: "[o, o] => o" (infixr "\" 25) - iff :: "[o, o] => o" (infixr "\" 25) - All_binder :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - Ex_binder :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - not_equal :: "['a, 'a] => o" (infixl "\" 50) +notation (xsymbols) + Not ("\ _" [40] 40) and + conj (infixr "\" 35) and + disj (infixr "\" 30) and + imp (infixr "\" 25) and + iff (infixr "\" 25) and + All (binder "\" 10) and + Ex (binder "\" 10) and + not_equal (infixl "\" 50) -syntax (HTML output) - Not :: "o => o" ("\ _" [40] 40) - conj :: "[o, o] => o" (infixr "\" 35) - disj :: "[o, o] => o" (infixr "\" 30) - All_binder :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - Ex_binder :: "[idts, o] => o" ("(3\_./ _)" [0, 10] 10) - not_equal :: "['a, 'a] => o" (infixl "\" 50) +notation (HTML output) + Not ("\ _" [40] 40) and + conj (infixr "\" 35) and + disj (infixr "\" 30) and + All (binder "\" 10) and + Ex (binder "\" 10) and + not_equal (infixl "\" 50) local diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Sequents/Sequents.thy Fri Feb 26 09:49:00 2010 +0100 @@ -65,7 +65,7 @@ (* parse translation for sequences *) -fun abs_seq' t = Abs ("s", Type ("seq'", []), t); (* FIXME @{type_syntax} *) +fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t); fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) = Const (@{const_syntax SeqO'}, dummyT) $ f diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Tools/Code/code_eval.ML Fri Feb 26 09:49:00 2010 +0100 @@ -144,7 +144,7 @@ val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq); val _ = ML_Context.add_antiq "code_datatype" (fn _ => - (Args.tyname --| Scan.lift (Args.$$$ "=") + (Args.type_name true --| Scan.lift (Args.$$$ "=") -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term))) >> ml_code_datatype_antiq); diff -r 5038f36b5ea1 -r 598ee3a4c1aa src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Feb 25 15:36:38 2010 +0100 +++ b/src/Tools/induct.ML Fri Feb 26 09:49:00 2010 +0100 @@ -345,7 +345,7 @@ Scan.lift (Args.$$$ k) >> K ""; fun attrib add_type add_pred del = - spec typeN Args.tyname >> add_type || + spec typeN (Args.type_name true) >> add_type || spec predN Args.const >> add_pred || spec setN Args.const >> add_pred || Scan.lift Args.del >> K del; @@ -856,7 +856,7 @@ | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); fun rule get_type get_pred = - named_rule typeN Args.tyname get_type || + named_rule typeN (Args.type_name true) get_type || named_rule predN Args.const get_pred || named_rule setN Args.const get_pred || Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;