--- a/NEWS Fri Feb 26 10:48:21 2010 +0100
+++ b/NEWS Fri Feb 26 10:57:35 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 ***
@@ -175,6 +177,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).
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 26 10:57:35 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.
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Fri Feb 26 10:57:35 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}
--- a/doc-src/IsarRef/Thy/Spec.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Fri Feb 26 10:57:35 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 +)
;
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 26 10:48:21 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 26 10:57:35 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.
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Feb 26 10:48:21 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Fri Feb 26 10:57:35 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}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Fri Feb 26 10:48:21 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Feb 26 10:57:35 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 +)
;
--- a/doc-src/Nitpick/nitpick.tex Fri Feb 26 10:48:21 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Fri Feb 26 10:57:35 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}
--- a/src/HOL/Algebra/Congruence.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Algebra/Congruence.thy Fri Feb 26 10:57:35 2010 +0100
@@ -35,15 +35,17 @@
eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
"is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
-syntax
+abbreviation
not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
- not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
- set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
+ where "x .\<noteq>\<^bsub>S\<^esub> y == ~(x .=\<^bsub>S\<^esub> y)"
-translations
- "x .\<noteq>\<index> y" == "~(x .=\<index> y)"
- "x .\<notin>\<index> A" == "~(x .\<in>\<index> A)"
- "A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)"
+abbreviation
+ not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
+ where "x .\<notin>\<^bsub>S\<^esub> A == ~(x .\<in>\<^bsub>S\<^esub> A)"
+
+abbreviation
+ set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
+ where "A {.\<noteq>}\<^bsub>S\<^esub> B == ~(A {.=}\<^bsub>S\<^esub> B)"
locale equivalence =
fixes S (structure)
--- a/src/HOL/Bali/Basis.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Bali/Basis.thy Fri Feb 26 10:57:35 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\<forall>_\<in>_:/ _)" [0,0,10] 10)
- Oex :: "[pttrn, 'a option, bool] => bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
+ "_Oall" :: "[pttrn, 'a option, bool] => bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10)
+ "_Oex" :: "[pttrn, 'a option, bool] => bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
translations
"! x:A: P" == "! x:CONST Option.set A. P"
--- a/src/HOL/Bali/Table.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Bali/Table.thy Fri Feb 26 10:57:35 2010 +0100
@@ -37,11 +37,9 @@
section "map of / table of"
-syntax
- table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
-
abbreviation
- "table_of \<equiv> map_of"
+ table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *}
+ where "table_of \<equiv> map_of"
translations
(type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Feb 26 10:57:35 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"
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Fri Feb 26 10:57:35 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))
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Fri Feb 26 10:57:35 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
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Feb 26 10:57:35 2010 +0100
@@ -1541,7 +1541,7 @@
hence "real ?num \<noteq> 0" by auto
have e_nat: "int (nat e) = e" using `0 \<le> 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
--- a/src/HOL/Groups.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Groups.thy Fri Feb 26 10:57:35 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;
);
*}
--- a/src/HOL/HOL.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/HOL.thy Fri Feb 26 10:57:35 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);
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Fri Feb 26 10:57:35 2010 +0100
@@ -256,8 +256,8 @@
(* Special syntax for guarded statements and guarded array updates: *)
syntax
- guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
- array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
+ "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
+ "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70, 65] 61)
translations
"P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
"a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
--- a/src/HOL/Import/HOL/prob_extra.imp Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Import/HOL/prob_extra.imp Fri Feb 26 10:57:35 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"
--- a/src/HOL/Import/HOL/real.imp Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Import/HOL/real.imp Fri Feb 26 10:57:35 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"
--- a/src/HOL/Isar_Examples/Hoare.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Fri Feb 26 10:57:35 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\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+notation (xsymbols)
+ Valid ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
lemma ValidI [intro?]:
"(!!s s'. Sem c s s' ==> s : P ==> s' : Q) ==> |- P c Q"
--- a/src/HOL/Library/Float.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Library/Float.thy Fri Feb 26 10:57:35 2010 +0100
@@ -789,12 +789,12 @@
hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto
from real_of_int_div4[of "?X" y]
- have "real (?X div y) \<le> (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) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
also have "\<dots> < 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 \<le> 2^?l" by auto
hence "real (?X div y + 1) * inverse (2^?l) \<le> 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) \<le> 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) \<le> (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) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
also have "\<dots> < 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 \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
finally have "real (Float (m div ?p) (e + ?d)) \<le> 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 \<le> 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 "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto
also have "\<dots> = 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 "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
- also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
+ also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
also have "\<dots> = 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 `\<not> 0 \<le> 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 "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
+ also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
also have "\<dots> = 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 `\<not> 0 \<le> e`] .
--- a/src/HOL/Library/Multiset.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Feb 26 10:57:35 2010 +0100
@@ -1502,13 +1502,13 @@
by (cases M) auto
syntax
- comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+ "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
("({#_/. _ :# _#})")
translations
"{#e. x:#M#}" == "CONST image_mset (%x. e) M"
syntax
- comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
("({#_/ | _ :# _./ _#})")
translations
"{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
--- a/src/HOL/Library/Numeral_Type.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Fri Feb 26 10:57:35 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 *}
--- a/src/HOL/MicroJava/BV/Correct.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Fri Feb 26 10:57:35 2010 +0100
@@ -66,9 +66,8 @@
| Some x \<Rightarrow> frs = []"
-syntax (xsymbols)
- correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
- ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
+notation (xsymbols)
+ correct_state ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50)
lemma sup_ty_opt_OK:
--- a/src/HOL/MicroJava/BV/JVMType.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Fri Feb 26 10:57:35 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] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=o _" [71,71] 70)
- sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=l _" [71,71] 70)
- sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=s _" [71,71] 70)
- sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=' _" [71,71] 70)
+notation (xsymbols)
+ sup_ty_opt ("_ \<turnstile> _ <=o _" [71,71] 70) and
+ sup_loc ("_ \<turnstile> _ <=l _" [71,71] 70) and
+ sup_state ("_ \<turnstile> _ <=s _" [71,71] 70) and
+ sup_state_opt ("_ \<turnstile> _ <=' _" [71,71] 70)
lemma JVM_states_unfold:
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy Fri Feb 26 10:57:35 2010 +0100
@@ -19,9 +19,8 @@
comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a"
"comb_nil a == ([], a)"
-syntax (xsymbols)
- "comb" :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"
- (infixr "\<box>" 55)
+notation (xsymbols)
+ comb (infixr "\<box>" 55)
lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
by (simp add: comb_def comb_nil_def split_beta)
--- a/src/HOL/MicroJava/DFA/Semilat.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Fri Feb 26 10:57:35 2010 +0100
@@ -32,16 +32,19 @@
"lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
"plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
(*<*)
-syntax
- (* allow \<sub> instead of \<bsub>..\<esub> *)
- "_lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
- "_lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
- "_plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+(* allow \<sub> instead of \<bsub>..\<esub> *)
+
+abbreviation (input)
+ lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
+ where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
-translations
- "x \<sqsubseteq>\<^sub>r y" => "x \<sqsubseteq>\<^bsub>r\<^esub> y"
- "x \<sqsubset>\<^sub>r y" => "x \<sqsubset>\<^bsub>r\<^esub> y"
- "x \<squnion>\<^sub>f y" => "x \<squnion>\<^bsub>f\<^esub> y"
+abbreviation (input)
+ lesssub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
+ where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y"
+
+abbreviation (input)
+ plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+ where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
(*>*)
defs
--- a/src/HOL/MicroJava/J/Conform.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Feb 26 10:57:35 2010 +0100
@@ -38,24 +38,13 @@
xconf (heap (store s)) (abrupt s)"
-syntax (xsymbols)
- hext :: "aheap => aheap => bool"
- ("_ \<le>| _" [51,51] 50)
-
- conf :: "'c prog => aheap => val => ty => bool"
- ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
-
- lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
- ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
-
- oconf :: "'c prog => aheap => obj => bool"
- ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
-
- hconf :: "'c prog => aheap => bool"
- ("_ \<turnstile>h _ \<surd>" [51,51] 50)
-
- conforms :: "state => java_mb env' => bool"
- ("_ ::\<preceq> _" [51,51] 50)
+notation (xsymbols)
+ hext ("_ \<le>| _" [51,51] 50) and
+ conf ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and
+ lconf ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and
+ oconf ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and
+ hconf ("_ \<turnstile>h _ \<surd>" [51,51] 50) and
+ conforms ("_ ::\<preceq> _" [51,51] 50)
section "hext"
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Fri Feb 26 10:57:35 2010 +0100
@@ -123,19 +123,15 @@
| Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
-consts
- "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
+constdefs
+ exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
("_ |- _ -jvmd-> _" [61,61,61]60)
+ "G |- s -jvmd-> t \<equiv>
+ (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
+ {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
-syntax (xsymbols)
- "exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
- ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
-
-defs
- exec_all_d_def:
- "G \<turnstile> s -jvmd\<rightarrow> t \<equiv>
- (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
- {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
+notation (xsymbols)
+ exec_all_d ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
declare split_paired_All [simp del]
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Fri Feb 26 10:57:35 2010 +0100
@@ -32,9 +32,8 @@
"G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
-syntax (xsymbols)
- exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
- ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
+notation (xsymbols)
+ exec_all ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
text {*
The start configuration of the JVM: in the start heap, we call a
--- a/src/HOL/NanoJava/Equivalence.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Fri Feb 26 10:57:35 2010 +0100
@@ -33,14 +33,14 @@
cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60)
"A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
-syntax (xsymbols)
- valid :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- evalid :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
- nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60)
- envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60)
- nvalids :: "[nat, triple set] => bool" ("|\<Turnstile>_: _" [61,61] 60)
- cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
-cenvalid :: "[triple set,etriple ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
+notation (xsymbols)
+ valid ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
+ evalid ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
+ nvalid ("\<Turnstile>_: _" [61,61] 60) and
+ envalid ("\<Turnstile>_:\<^sub>e _" [61,61] 60) and
+ nvalids ("|\<Turnstile>_: _" [61,61] 60) and
+ cnvalids ("_ |\<Turnstile>/ _" [61,61] 60) and
+ cenvalid ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
@@ -164,10 +164,10 @@
"MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n\<rightarrow> t)"
MGTe :: "expr => state => etriple"
"MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> 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:
"\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
--- a/src/HOL/NanoJava/State.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/NanoJava/State.thy Fri Feb 26 10:57:35 2010 +0100
@@ -84,9 +84,9 @@
lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000)
"lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)"
-syntax (xsymbols)
- hupd :: "loc => obj => state => state" ("hupd'(_\<mapsto>_')" [10,10] 1000)
- lupd :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
+notation (xsymbols)
+ hupd ("hupd'(_\<mapsto>_')" [10,10] 1000) and
+ lupd ("lupd'(_\<mapsto>_')" [10,10] 1000)
constdefs
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 26 10:57:35 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,
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Feb 26 10:57:35 2010 +0100
@@ -1381,25 +1381,16 @@
text {* A type class without axioms: *}
-axclass classA
+class classA
lemma "P (x\<Colon>'a\<Colon>classA)"
nitpick [expect = genuine]
oops
-text {* The axiom of this type class does not contain any type variables: *}
-
-axclass classB
-classB_ax: "P \<or> \<not> P"
-
-lemma "P (x\<Colon>'a\<Colon>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: "\<exists>x y. x \<noteq> y"
+class classC =
+ assumes classC_ax: "\<exists>x y. x \<noteq> y"
lemma "P (x\<Colon>'a\<Colon>classC)"
nitpick [expect = genuine]
@@ -1411,11 +1402,9 @@
text {* A type class for which a constant is defined: *}
-consts
-classD_const :: "'a \<Rightarrow> 'a"
-
-axclass classD < type
-classD_ax: "classD_const (classD_const x) = classD_const x"
+class classD =
+ fixes classD_const :: "'a \<Rightarrow> 'a"
+ assumes classD_ax: "classD_const (classD_const x) = classD_const x"
lemma "P (x\<Colon>'a\<Colon>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\<Colon>'a\<Colon>classE)"
nitpick [expect = genuine]
oops
-lemma "P (x\<Colon>'a\<Colon>{classB, classE})"
-nitpick [expect = genuine]
-oops
-
text {* OFCLASS: *}
lemma "OFCLASS('a\<Colon>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\<Colon>type, classC_class)"
nitpick [expect = genuine]
oops
--- a/src/HOL/Nominal/Nominal.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Nominal/Nominal.thy Fri Feb 26 10:57:35 2010 +0100
@@ -3403,13 +3403,13 @@
where
ABS_in: "(abs_fun a x)\<in>ABS_set"
-typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a noption)) set"
+typedef (ABS) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+ "ABS_set::('x\<Rightarrow>('a noption)) set"
proof
fix x::"'a" and a::"'x"
show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
qed
-syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
section {* lemmas for deciding permutation equations *}
(*===================================================*)
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Feb 26 10:57:35 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 =
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Feb 26 10:57:35 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 =
--- a/src/HOL/Orderings.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Orderings.thy Fri Feb 26 10:57:35 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) =>
--- a/src/HOL/Probability/Borel.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Probability/Borel.thy Fri Feb 26 10:57:35 2010 +0100
@@ -82,7 +82,7 @@
fix w n
assume le: "f w \<le> 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
--- a/src/HOL/Product_Type.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Product_Type.thy Fri Feb 26 10:57:35 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;
--- a/src/HOL/Rat.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Rat.thy Fri Feb 26 10:57:35 2010 +0100
@@ -6,6 +6,7 @@
theory Rat
imports GCD Archimedean_Field
+uses ("Tools/float_syntax.ML")
begin
subsection {* Rational numbers as quotient *}
@@ -1195,4 +1196,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 \<Rightarrow> '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
--- a/src/HOL/RealDef.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/RealDef.thy Fri Feb 26 10:57:35 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)+
--- a/src/HOL/RealPow.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/RealPow.thy Fri Feb 26 10:57:35 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) \<le> 2 ^ n"
+(* used by Import/HOL/real.imp *)
+lemma two_realpow_ge_one: "(1::real) \<le> 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 \<noteq> 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) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> 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) \<le> 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 \<le> 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 \<Rightarrow> '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
--- a/src/HOL/TLA/Action.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/TLA/Action.thy Fri Feb 26 10:57:35 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)
--- a/src/HOL/TLA/Intensional.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/TLA/Intensional.thy Fri Feb 26 10:57:35 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)
--- a/src/HOL/TLA/Stfun.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/TLA/Stfun.thy Fri Feb 26 10:57:35 2010 +0100
@@ -35,7 +35,7 @@
stvars :: "'a stfun => bool"
syntax
- "PRED" :: "lift => 'a" ("PRED _")
+ "_PRED" :: "lift => 'a" ("PRED _")
"_stvars" :: "lift => bool" ("basevars _")
translations
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Feb 26 10:57:35 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;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Feb 26 10:57:35 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') [];
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Feb 26 10:57:35 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));
--- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Feb 26 10:57:35 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});
(*---------------------------------------------------------------------------
--- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Feb 26 10:57:35 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;
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Feb 26 10:57:35 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)))
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Feb 26 10:57:35 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 =
--- a/src/HOL/Tools/Nitpick/HISTORY Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Fri Feb 26 10:57:35 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
--- a/src/HOL/Tools/Nitpick/kodkod.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Fri Feb 26 10:57:35 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 =>
--- a/src/HOL/Tools/Nitpick/minipick.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Fri Feb 26 10:57:35 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"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 26 10:57:35 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;
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 26 10:57:35 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 =>
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Feb 26 10:57:35 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;
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Feb 26 10:57:35 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 "/"
--- a/src/HOL/Tools/TFL/post.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML Fri Feb 26 10:57:35 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 =
--- a/src/HOL/Tools/inductive.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Feb 26 10:57:35 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))
--- a/src/HOL/Tools/inductive_codegen.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Feb 26 10:57:35 2010 +0100
@@ -51,12 +51,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) [];
@@ -186,7 +187,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)
@@ -577,17 +578,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
@@ -600,7 +604,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;
@@ -632,7 +636,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;
@@ -715,7 +719,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) =>
--- a/src/HOL/Tools/inductive_realizer.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Feb 26 10:57:35 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)]));
--- a/src/HOL/Tools/inductive_set.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML Fri Feb 26 10:57:35 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;
--- a/src/HOL/Tools/numeral_syntax.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Fri Feb 26 10:57:35 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
--- a/src/HOL/Tools/record.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/record.ML Fri Feb 26 10:57:35 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
--- a/src/HOL/Tools/simpdata.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/simpdata.ML Fri Feb 26 10:57:35 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
--- a/src/HOL/Tools/split_rule.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/split_rule.ML Fri Feb 26 10:57:35 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;
--- a/src/HOL/Tools/string_syntax.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Fri Feb 26 10:57:35 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);
--- a/src/HOL/Tools/typedef.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Fri Feb 26 10:57:35 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
--- a/src/HOL/Typerep.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/Typerep.thy Fri Feb 26 10:57:35 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;
--- a/src/HOL/UNITY/SubstAx.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Fri Feb 26 10:57:35 2010 +0100
@@ -17,8 +17,8 @@
LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60)
"A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
-syntax (xsymbols)
- "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
+notation (xsymbols)
+ LeadsTo (infixl " \<longmapsto>w " 60)
text{*Resembles the previous definition of LeadsTo*}
--- a/src/HOL/UNITY/WFair.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/UNITY/WFair.thy Fri Feb 26 10:57:35 2010 +0100
@@ -69,8 +69,8 @@
--{*predicate transformer: the largest set that leads to @{term B}*}
"wlt F B == Union {A. F \<in> A leadsTo B}"
-syntax (xsymbols)
- "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
+notation (xsymbols)
+ leadsTo (infixl "\<longmapsto>" 60)
subsection{*transient*}
--- a/src/HOL/ex/HarmonicSeries.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy Fri Feb 26 10:57:35 2010 +0100
@@ -73,7 +73,8 @@
qed
moreover from xs have "x \<le> 2^m" by auto
ultimately have
- "inverse (real x) \<ge> inverse (real ((2::nat)^m))" by simp
+ "inverse (real x) \<ge> inverse (real ((2::nat)^m))"
+ by (simp del: real_of_nat_power)
moreover
from xgt0 have "real x \<noteq> 0" by simp
then have
@@ -107,7 +108,7 @@
by (auto simp: tmdef dest: two_pow_sub)
also have
"\<dots> = (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
"\<dots> = (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
--- a/src/HOL/ex/Numeral.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOL/ex/Numeral.thy Fri Feb 26 10:57:35 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
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Fri Feb 26 10:57:35 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" ("\<not> _" [40] 40)
- "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
- "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 30)
- "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<longrightarrow>" 25)
+notation (xsymbols output)
+ NOT ("\<not> _" [40] 40) and
+ AND (infixr "\<and>" 35) and
+ OR (infixr "\<or>" 30) and
+ IMPLIES (infixr "\<longrightarrow>" 25)
-syntax (xsymbols)
- "satisfies" ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8)
+notation (xsymbols)
+ satisfies ("_ \<Turnstile> _" [100,9] 8)
-syntax (HTML output)
- "NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
- "AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
- "OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 30)
+notation (HTML output)
+ NOT ("\<not> _" [40] 40) and
+ AND (infixr "\<and>" 35) and
+ OR (infixr "\<or>" 30)
defs
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Fri Feb 26 10:57:35 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 =
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Feb 26 10:57:35 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));
--- a/src/HOLCF/Tools/pcpodef.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML Fri Feb 26 10:57:35 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)) =
--- a/src/HOLCF/Tools/repdef.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML Fri Feb 26 10:57:35 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)) =
--- a/src/Pure/Isar/args.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/Isar/args.ML Fri Feb 26 10:57:35 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)
--- a/src/Pure/Isar/isar_syn.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Feb 26 10:57:35 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))));
--- a/src/Pure/Isar/outer_parse.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/Isar/outer_parse.ML Fri Feb 26 10:57:35 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);
--- a/src/Pure/Isar/proof_context.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Feb 26 10:57:35 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;
--- a/src/Pure/ML/ml_antiquote.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Fri Feb 26 10:57:35 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))
--- a/src/Pure/Syntax/mixfix.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/Syntax/mixfix.ML Fri Feb 26 10:57:35 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;
--- a/src/Pure/Syntax/syn_ext.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Fri Feb 26 10:57:35 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,
--- a/src/Pure/sign.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/sign.ML Fri Feb 26 10:57:35 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);
--- a/src/Pure/type.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Pure/type.ML Fri Feb 26 10:57:35 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)) =
--- a/src/Sequents/LK0.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Sequents/LK0.thy Fri Feb 26 10:57:35 2010 +0100
@@ -43,23 +43,23 @@
not_equal (infixl "~=" 50) where
"x ~= y == ~ (x = y)"
-syntax (xsymbols)
- Not :: "o => o" ("\<not> _" [40] 40)
- conj :: "[o, o] => o" (infixr "\<and>" 35)
- disj :: "[o, o] => o" (infixr "\<or>" 30)
- imp :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
- iff :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25)
- All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
- Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+notation (xsymbols)
+ Not ("\<not> _" [40] 40) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ imp (infixr "\<longrightarrow>" 25) and
+ iff (infixr "\<longleftrightarrow>" 25) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ not_equal (infixl "\<noteq>" 50)
-syntax (HTML output)
- Not :: "o => o" ("\<not> _" [40] 40)
- conj :: "[o, o] => o" (infixr "\<and>" 35)
- disj :: "[o, o] => o" (infixr "\<or>" 30)
- All_binder :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10)
- Ex_binder :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10)
- not_equal :: "['a, 'a] => o" (infixl "\<noteq>" 50)
+notation (HTML output)
+ Not ("\<not> _" [40] 40) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
+ All (binder "\<forall>" 10) and
+ Ex (binder "\<exists>" 10) and
+ not_equal (infixl "\<noteq>" 50)
local
--- a/src/Sequents/Sequents.thy Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Sequents/Sequents.thy Fri Feb 26 10:57:35 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
--- a/src/Tools/Code/code_eval.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Tools/Code/code_eval.ML Fri Feb 26 10:57:35 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);
--- a/src/Tools/induct.ML Fri Feb 26 10:48:21 2010 +0100
+++ b/src/Tools/induct.ML Fri Feb 26 10:57:35 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;