--- a/Admin/isatest/annomaly.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/Admin/isatest/annomaly.ML Sat Aug 29 22:01:55 2009 +0200
@@ -20,7 +20,7 @@
val isabelleHome =
case OS.Process.getEnv "ISABELLE_HOME"
of NONE => OS.FileSys.getDir ()
- | SOME home => mkAbsolute home
+ | SOME home => mkAbsolute home
fun noparent [] = []
| noparent (n :: ns) =
@@ -33,12 +33,12 @@
fun rewrite defPrefix name =
let val abs = mkAbsolute name
- val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
- val exists = (OS.FileSys.access(abs, nil)
- handle OS.SysErr _ => false)
+ val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
+ val exists = (OS.FileSys.access(abs, nil)
+ handle OS.SysErr _ => false)
in if exists andalso rel <> ""
- then isabellePath (toArcs rel)
- else defPrefix @ noparent (toArcs name)
+ then isabellePath (toArcs rel)
+ else defPrefix @ noparent (toArcs name)
end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
in
@@ -49,10 +49,10 @@
(* should we have different files for different line numbers? *
val arcs = if line <= 1 then arcs
else arcs @ [ "l." ^ Int.toString line ]
- *)
- val arcs = if t = "structure Isabelle =\nstruct\nend;"
- andalso name = "ML"
- then ["empty_Isabelle", "empty" ] else arcs
+ *)
+ val arcs = if t = "structure Isabelle =\nstruct\nend;"
+ andalso name = "ML"
+ then ["empty_Isabelle", "empty" ] else arcs
val _ = AnnoMaLy.nameNextStream arcs
in smlnj_use_text tune str_of_pos name_space (line, name) p v t end;
--- a/NEWS Sat Aug 29 21:58:33 2009 +0200
+++ b/NEWS Sat Aug 29 22:01:55 2009 +0200
@@ -181,6 +181,10 @@
or even Display.pretty_thm_without_context as last resort.
INCOMPATIBILITY.
+* Discontinued Display.pretty_ctyp/cterm etc. INCOMPATIBILITY, use
+Syntax.pretty_typ/term directly, preferably with proper context
+instead of global theory.
+
*** System ***
--- a/doc-src/rail.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/doc-src/rail.ML Sat Aug 29 22:01:55 2009 +0200
@@ -99,7 +99,7 @@
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
|> (if ! ThyOutput.quotes then quote else I)
|> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else hyper o enclose "\\mbox{\\isa{" "}}")), style)
+ else hyper o enclose "\\mbox{\\isa{" "}}")), style)
else ("Bad " ^ kind ^ " " ^ name, false)
end;
end;
@@ -147,8 +147,8 @@
) >> (Identifier o enclose "\\isa{" "}" o Output.output o implode) ||
scan_link >> (decode_link ctxt) >>
(fn (txt, style) =>
- if style then Special_Identifier(txt)
- else Identifier(txt))
+ if style then Special_Identifier(txt)
+ else Identifier(txt))
end;
fun scan_anot ctxt =
@@ -169,12 +169,12 @@
val text_sq =
Scan.repeat (
Scan.one (fn s =>
- s <> "\n" andalso
- s <> "\t" andalso
- s <> "'" andalso
- s <> "\\" andalso
- Symbol.is_regular s) ||
- ($$ "\\" |-- $$ "'")
+ s <> "\n" andalso
+ s <> "\t" andalso
+ s <> "'" andalso
+ s <> "\\" andalso
+ Symbol.is_regular s) ||
+ ($$ "\\" |-- $$ "'")
) >> implode
fun quoted scan = $$ "'" |-- scan --| $$ "'";
in
@@ -305,9 +305,9 @@
parse_body2 -- ($$$ "*" |-- !!! "body4e expected" (parse_body4e)) >>
(fn (body1, body2) =>
if is_empty body2 then
- add_body(PLUS, new_empty_body, rev_body body1)
+ add_body(PLUS, new_empty_body, rev_body body1)
else
- add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
+ add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >>
(fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||
parse_body2e
@@ -365,36 +365,36 @@
fun position_body (body as Body(kind, text, annot, id, bodies), ystart) =
let fun max (x,y) = if x > y then x else y
fun set_body_position (Body(kind, text, annot, id, bodies), ystart, ynext) =
- Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
+ Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
fun pos_bodies_cat ([],_,ynext,liste) = (liste, ynext)
| pos_bodies_cat (x::xs, ystart, ynext, liste) =
- if is_kind_of CR x then
- (case set_body_position(x, ystart, ynext+1) of
- body as Body_Pos(_,_,_,_,_,_,ynext1) =>
- pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
- )
- else
- (case position_body(x, ystart) of
- body as Body_Pos(_,_,_,_,_,_,ynext1) =>
- pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
- )
+ if is_kind_of CR x then
+ (case set_body_position(x, ystart, ynext+1) of
+ body as Body_Pos(_,_,_,_,_,_,ynext1) =>
+ pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
+ )
+ else
+ (case position_body(x, ystart) of
+ body as Body_Pos(_,_,_,_,_,_,ynext1) =>
+ pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
+ )
fun pos_bodies_bar_plus ([],_,ynext,liste) = (liste, ynext)
| pos_bodies_bar_plus (x::xs, ystart, ynext, liste) =
- (case position_body(x, ystart) of
- body as Body_Pos(_,_,_,_,_,_,ynext1) =>
- pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
- )
+ (case position_body(x, ystart) of
+ body as Body_Pos(_,_,_,_,_,_,ynext1) =>
+ pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
+ )
in
(case kind of
CAT => (case pos_bodies_cat(bodies,ystart,ystart+1,[]) of
- (bodiesPos, ynext) =>
- Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
+ (bodiesPos, ynext) =>
+ Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
| BAR => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
- (bodiesPos, ynext) =>
- Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
+ (bodiesPos, ynext) =>
+ Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
| PLUS => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
- (bodiesPos, ynext) =>
- Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
+ (bodiesPos, ynext) =>
+ Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
| CR => set_body_position(body, ystart, ystart+3)
| EMPTY => set_body_position(body, ystart, ystart+1)
| ANNOTE => set_body_position(body, ystart, ystart+1)
@@ -406,15 +406,15 @@
fun format_body (Body_Pos(EMPTY,_,_,_,_,_,_), _) = ""
| format_body (Body_Pos(CAT,_,_,_,bodies,_,_), cent) =
let fun format_bodies([]) = ""
- | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
+ | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
in
format_bodies(bodies)
end
| format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) =
let fun format_bodies([]) = "\\rail@endbar\n"
- | format_bodies(x::xs) =
- "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
- format_body(x, "") ^ format_bodies(xs)
+ | format_bodies(x::xs) =
+ "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
+ format_body(x, "") ^ format_bodies(xs)
in
"\\rail@bar\n" ^ format_body(hd(bodies), "") ^ format_bodies(tl(bodies))
end
--- a/src/FOL/fologic.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/FOL/fologic.ML Sat Aug 29 22:01:55 2009 +0200
@@ -6,28 +6,28 @@
signature FOLOGIC =
sig
- val oT : typ
- val mk_Trueprop : term -> term
- val dest_Trueprop : term -> term
- val not : term
- val conj : term
- val disj : term
- val imp : term
- val iff : term
- val mk_conj : term * term -> term
- val mk_disj : term * term -> term
- val mk_imp : term * term -> term
- val dest_imp : term -> term*term
- val dest_conj : term -> term list
- val mk_iff : term * term -> term
- val dest_iff : term -> term*term
- val all_const : typ -> term
- val mk_all : term * term -> term
- val exists_const : typ -> term
- val mk_exists : term * term -> term
- val eq_const : typ -> term
- val mk_eq : term * term -> term
- val dest_eq : term -> term*term
+ val oT: typ
+ val mk_Trueprop: term -> term
+ val dest_Trueprop: term -> term
+ val not: term
+ val conj: term
+ val disj: term
+ val imp: term
+ val iff: term
+ val mk_conj: term * term -> term
+ val mk_disj: term * term -> term
+ val mk_imp: term * term -> term
+ val dest_imp: term -> term * term
+ val dest_conj: term -> term list
+ val mk_iff: term * term -> term
+ val dest_iff: term -> term * term
+ val all_const: typ -> term
+ val mk_all: term * term -> term
+ val exists_const: typ -> term
+ val mk_exists: term * term -> term
+ val eq_const: typ -> term
+ val mk_eq: term * term -> term
+ val dest_eq: term -> term * term
val mk_binop: string -> term * term -> term
val mk_binrel: string -> term * term -> term
val dest_bin: string -> typ -> term -> term * term
@@ -46,7 +46,8 @@
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
-(** Logical constants **)
+
+(* Logical constants *)
val not = Const ("Not", oT --> oT);
val conj = Const("op &", [oT,oT]--->oT);
@@ -80,6 +81,7 @@
fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
+
(* binary oprations and relations *)
fun mk_binop c (t, u) =
@@ -97,5 +99,4 @@
else raise TERM ("dest_bin " ^ c, [tm])
| dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
-
end;
--- a/src/FOL/intprover.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/FOL/intprover.ML Sat Aug 29 22:01:55 2009 +0200
@@ -79,8 +79,7 @@
(*One safe or unsafe step. *)
fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
-fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i,
- biresolve_tac haz_dup_brls i];
+fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_dup_brls i];
(*Dumb but fast*)
val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
--- a/src/FOLP/hypsubst.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/FOLP/hypsubst.ML Sat Aug 29 22:01:55 2009 +0200
@@ -27,7 +27,7 @@
val inspect_pair : bool -> term * term -> thm
end;
-functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
+functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
struct
local open Data in
@@ -43,13 +43,13 @@
but how could we check for this?*)
fun inspect_pair bnd (t,u) =
case (Envir.eta_contract t, Envir.eta_contract u) of
- (Bound i, _) => if loose(i,u) then raise Match
+ (Bound i, _) => if loose(i,u) then raise Match
else sym (*eliminates t*)
- | (_, Bound i) => if loose(i,t) then raise Match
+ | (_, Bound i) => if loose(i,t) then raise Match
else asm_rl (*eliminates u*)
- | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match
+ | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match
else sym (*eliminates t*)
- | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match
+ | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match
else asm_rl (*eliminates u*)
| _ => raise Match;
@@ -58,7 +58,7 @@
the rule asm_rl (resp. sym). *)
fun eq_var bnd =
let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
- | eq_var_aux k (Const("==>",_) $ A $ B) =
+ | eq_var_aux k (Const("==>",_) $ A $ B) =
((k, inspect_pair bnd (dest_eq A))
(*Exception Match comes from inspect_pair or dest_eq*)
handle Match => eq_var_aux (k+1) B)
@@ -70,13 +70,13 @@
fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
let val n = length(Logic.strip_assums_hyp Bi) - 1
val (k,symopt) = eq_var bnd Bi
- in
+ in
DETERM
(EVERY [REPEAT_DETERM_N k (etac rev_mp i),
- etac revcut_rl i,
- REPEAT_DETERM_N (n-k) (etac rev_mp i),
- etac (symopt RS subst) i,
- REPEAT_DETERM_N n (rtac imp_intr i)])
+ etac revcut_rl i,
+ REPEAT_DETERM_N (n-k) (etac rev_mp i),
+ etac (symopt RS subst) i,
+ REPEAT_DETERM_N n (rtac imp_intr i)])
end
handle THM _ => no_tac | EQ_VAR => no_tac);
--- a/src/FOLP/simp.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/FOLP/simp.ML Sat Aug 29 22:01:55 2009 +0200
@@ -52,7 +52,7 @@
val tracing : bool ref
end;
-functor SimpFun (Simp_data: SIMP_DATA) : SIMP =
+functor SimpFun (Simp_data: SIMP_DATA) : SIMP =
struct
local open Simp_data in
@@ -74,12 +74,12 @@
Similar to match_from_nat_tac, but the net does not contain numbers;
rewrite rules are not ordered.*)
fun net_tac net =
- SUBGOAL(fn (prem,i) =>
+ SUBGOAL(fn (prem,i) =>
resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i);
(*match subgoal i against possible theorems indexed by lhs in the net*)
fun lhs_net_tac net =
- SUBGOAL(fn (prem,i) =>
+ SUBGOAL(fn (prem,i) =>
biresolve_tac (Net.unify_term net
(lhs_of (Logic.strip_assums_concl prem))) i);
@@ -110,7 +110,7 @@
(*Get the norm constants from norm_thms*)
val norms =
- let fun norm thm =
+ let fun norm thm =
case lhs_of(concl_of thm) of
Const(n,_)$_ => n
| _ => error "No constant in lhs of a norm_thm"
@@ -144,7 +144,7 @@
(**** Adding "NORM" tags ****)
(*get name of the constant from conclusion of a congruence rule*)
-fun cong_const cong =
+fun cong_const cong =
case head_of (lhs_of (concl_of cong)) of
Const(c,_) => c
| _ => "" (*a placeholder distinct from const names*);
@@ -156,9 +156,9 @@
fun add_hidden_vars ccs =
let fun add_hvars tm hvars = case tm of
Abs(_,_,body) => OldTerm.add_term_vars(body,hvars)
- | _$_ => let val (f,args) = strip_comb tm
+ | _$_ => let val (f,args) = strip_comb tm
in case f of
- Const(c,T) =>
+ Const(c,T) =>
if member (op =) ccs c
then fold_rev add_hvars args hvars
else OldTerm.add_term_vars (tm, hvars)
@@ -202,13 +202,13 @@
val hvs = map (#1 o dest_Var) hvars
val refl1_tac = refl_tac 1
fun norm_step_tac st = st |>
- (case head_of(rhs_of_eq 1 st) of
- Var(ixn,_) => if ixn mem hvs then refl1_tac
- else resolve_tac normI_thms 1 ORELSE refl1_tac
- | Const _ => resolve_tac normI_thms 1 ORELSE
- resolve_tac congs 1 ORELSE refl1_tac
- | Free _ => resolve_tac congs 1 ORELSE refl1_tac
- | _ => refl1_tac)
+ (case head_of(rhs_of_eq 1 st) of
+ Var(ixn,_) => if ixn mem hvs then refl1_tac
+ else resolve_tac normI_thms 1 ORELSE refl1_tac
+ | Const _ => resolve_tac normI_thms 1 ORELSE
+ resolve_tac congs 1 ORELSE refl1_tac
+ | Free _ => resolve_tac congs 1 ORELSE refl1_tac
+ | _ => refl1_tac)
val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
val SOME(thm'',_) = Seq.pull(add_norm_tac thm')
in thm'' end;
@@ -246,9 +246,9 @@
(** Insertion of congruences and rewrites **)
(*insert a thm in a thm net*)
-fun insert_thm_warn th net =
+fun insert_thm_warn th net =
Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
- handle Net.INSERT =>
+ handle Net.INSERT =>
(writeln ("Duplicate rewrite or congruence rule:\n" ^
Display.string_of_thm_without_context th); net);
@@ -272,9 +272,9 @@
(** Deletion of congruences and rewrites **)
(*delete a thm from a thm net*)
-fun delete_thm_warn th net =
+fun delete_thm_warn th net =
Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
- handle Net.DELETE =>
+ handle Net.DELETE =>
(writeln ("No such rewrite or congruence rule:\n" ^
Display.string_of_thm_without_context th); net);
@@ -337,17 +337,17 @@
in find_if(tm,0) end;
fun IF1_TAC cong_tac i =
- let fun seq_try (ifth::ifths,ifc::ifcs) thm =
+ let fun seq_try (ifth::ifths,ifc::ifcs) thm =
(COND (if_rewritable ifc i) (DETERM(rtac ifth i))
(seq_try(ifths,ifcs))) thm
| seq_try([],_) thm = no_tac thm
and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm
and one_subt thm =
let val test = has_fewer_prems (nprems_of thm + 1)
- fun loop thm =
- COND test no_tac
+ fun loop thm =
+ COND test no_tac
((try_rew THEN DEPTH_FIRST test (refl_tac i))
- ORELSE (refl_tac i THEN loop)) thm
+ ORELSE (refl_tac i THEN loop)) thm
in (cong_tac THEN loop) thm end
in COND (may_match(case_consts,i)) try_rew no_tac end;
@@ -381,12 +381,12 @@
(*print lhs of conclusion of subgoal i*)
fun pr_goal_lhs i st =
- writeln (Syntax.string_of_term_global (Thm.theory_of_thm st)
+ writeln (Syntax.string_of_term_global (Thm.theory_of_thm st)
(lhs_of (prepare_goal i st)));
(*print conclusion of subgoal i*)
fun pr_goal_concl i st =
- writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st))
+ writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st))
(*print subgoals i to j (inclusive)*)
fun pr_goals (i,j) st =
@@ -439,7 +439,7 @@
then writeln (cat_lines
("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
else ();
- (ss,thm,anet',anet::ats,cs)
+ (ss,thm,anet',anet::ats,cs)
end;
fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
@@ -492,7 +492,7 @@
fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
let val cong_tac = net_tac cong_net
-in fn i =>
+in fn i =>
(fn thm =>
if i <= 0 orelse nprems_of thm < i then Seq.empty
else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
--- a/src/HOL/Algebra/UnivPoly.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Sat Aug 29 22:01:55 2009 +0200
@@ -817,15 +817,9 @@
text {* Degree and polynomial operations *}
lemma deg_add [simp]:
- assumes R: "p \<in> carrier P" "q \<in> carrier P"
- shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
-proof (cases "deg R p <= deg R q")
- case True show ?thesis
- by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
-next
- case False show ?thesis
- by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
-qed
+ "p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
+ deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
+by(rule deg_aboveI)(simp_all add: deg_aboveD)
lemma deg_monom_le:
"a \<in> carrier R ==> deg R (monom P a n) <= n"
--- a/src/HOL/Algebra/abstract/Ring2.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sat Aug 29 22:01:55 2009 +0200
@@ -241,7 +241,7 @@
proof (induct n)
case 0 show ?case by simp
next
- case Suc thus ?case by (simp add: add_assoc)
+ case Suc thus ?case by (simp add: add_assoc)
qed
lemma natsum_cong [cong]:
@@ -269,21 +269,21 @@
ML {*
local
- val lhss =
+ val lhss =
["t + u::'a::ring",
- "t - u::'a::ring",
- "t * u::'a::ring",
- "- t::'a::ring"];
- fun proc ss t =
+ "t - u::'a::ring",
+ "t * u::'a::ring",
+ "- t::'a::ring"];
+ fun proc ss t =
let val rew = Goal.prove (Simplifier.the_context ss) [] []
(HOLogic.mk_Trueprop
(HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
(fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
|> mk_meta_eq;
val (t', u) = Logic.dest_equals (Thm.prop_of rew);
- in if t' aconv u
+ in if t' aconv u
then NONE
- else SOME rew
+ else SOME rew
end;
in
val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
@@ -305,7 +305,7 @@
declare one_not_zero [simp]
lemma zero_not_one [simp]:
- "0 ~= (1::'a::domain)"
+ "0 ~= (1::'a::domain)"
by (rule not_sym) simp
lemma integral_iff: (* not by default a simp rule! *)
@@ -322,7 +322,7 @@
*)
(*
lemma bug: "(b::'a::ring) - (b - a) = a" by simp
- simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
+ simproc for rings cannot prove "(a::'a::ring) - (a - b) = b"
*)
lemma m_lcancel:
assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)"
@@ -330,8 +330,8 @@
assume eq: "a * b = a * c"
then have "a * (b - c) = 0" by simp
then have "a = 0 | (b - c) = 0" by (simp only: integral_iff)
- with prem have "b - c = 0" by auto
- then have "b = b - (b - c)" by simp
+ with prem have "b - c = 0" by auto
+ then have "b = b - (b - c)" by simp
also have "b - (b - c) = c" by simp
finally show "b = c" .
next
@@ -386,7 +386,7 @@
qed
-lemma unit_mult:
+lemma unit_mult:
"!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"
apply (unfold dvd_def)
apply clarify
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Sat Aug 29 22:01:55 2009 +0200
@@ -563,11 +563,7 @@
lemma deg_add [simp]:
"deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
-proof (cases "deg p <= deg q")
- case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD)
-next
- case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
-qed
+by (rule deg_aboveI) (simp add: deg_aboveD)
lemma deg_monom_ring:
"deg (monom a n::'a::ring up) <= n"
--- a/src/HOL/Complete_Lattice.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy Sat Aug 29 22:01:55 2009 +0200
@@ -76,11 +76,11 @@
lemma sup_bot [simp]:
"x \<squnion> bot = x"
- using bot_least [of x] by (simp add: le_iff_sup sup_commute)
+ using bot_least [of x] by (simp add: sup_commute)
lemma inf_top [simp]:
"x \<sqinter> top = x"
- using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
+ using top_greatest [of x] by (simp add: inf_commute)
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
--- a/src/HOL/Decision_Procs/Approximation.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sat Aug 29 22:01:55 2009 +0200
@@ -1904,7 +1904,7 @@
show "0 < real x * 2/3" using * by auto
show "real ?max + 1 \<le> real x * 2/3" using * up
by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
- auto simp add: real_of_float_max max_def)
+ auto simp add: real_of_float_max)
qed
finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
\<le> ln (real x)"
--- a/src/HOL/Decision_Procs/Ferrack.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sat Aug 29 22:01:55 2009 +0200
@@ -512,7 +512,7 @@
assumes g0: "numgcd t = 0"
shows "Inum bs t = 0"
using g0[simplified numgcd_def]
- by (induct t rule: numgcdh.induct, auto simp add: natabs0 max_def maxcoeff_pos)
+ by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
using gp
--- a/src/HOL/Finite_Set.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Finite_Set.thy Sat Aug 29 22:01:55 2009 +0200
@@ -2966,11 +2966,11 @@
lemma dual_max:
"ord.max (op \<ge>) = min"
- by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
+ by (auto simp add: ord.max_def_raw expand_fun_eq)
lemma dual_min:
"ord.min (op \<ge>) = max"
- by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
+ by (auto simp add: ord.min_def_raw expand_fun_eq)
lemma strict_below_fold1_iff:
assumes "finite A" and "A \<noteq> {}"
--- a/src/HOL/HoareParallel/Graph.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Sat Aug 29 22:01:55 2009 +0200
@@ -203,11 +203,11 @@
apply(rule_tac x = "(take m path)@patha" in exI)
apply(subgoal_tac "\<not>(length path\<le>m)")
prefer 2 apply arith
- apply(simp add: min_def)
+ apply(simp)
apply(rule conjI)
apply(subgoal_tac "\<not>(m + length patha - 1 < m)")
prefer 2 apply arith
- apply(simp add: nth_append min_def)
+ apply(simp add: nth_append)
apply(rule conjI)
apply(case_tac "m")
apply force
@@ -236,7 +236,7 @@
apply(erule_tac x = "m - 1" in allE)
apply(simp add: nth_list_update)
apply(force simp add: nth_list_update)
- apply(simp add: nth_append min_def)
+ apply(simp add: nth_append)
apply(rotate_tac -4)
apply(erule_tac x = "i - m" in allE)
apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
@@ -248,8 +248,7 @@
apply(rule_tac x = "take (Suc m) path" in exI)
apply(subgoal_tac "\<not>(length path\<le>Suc m)" )
prefer 2 apply arith
- apply(simp add: min_def)
- apply clarify
+ apply clarsimp
apply(erule_tac x = "i" in allE)
apply simp
apply clarify
--- a/src/HOL/Import/hol4rews.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Import/hol4rews.ML Sat Aug 29 22:01:55 2009 +0200
@@ -531,7 +531,7 @@
val _ = app (fn (hol,(internal,isa,opt_ty)) =>
(out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
case opt_ty of
- SOME ty => out (" :: \"" ^ (Display.string_of_ctyp (ctyp_of thy ty)) ^ "\"")
+ SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
| NONE => ())) constmaps
val _ = if null constmaps
then ()
--- a/src/HOL/Import/proof_kernel.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Sat Aug 29 22:01:55 2009 +0200
@@ -199,12 +199,12 @@
val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
handle TERM _ => ct)
in
- quote(
+ quote (
PrintMode.setmp [] (
Library.setmp show_brackets false (
Library.setmp show_all_types true (
Library.setmp Syntax.ambiguity_is_error false (
- Library.setmp show_sorts true Display.string_of_cterm))))
+ Library.setmp show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
ct)
end
@@ -226,7 +226,8 @@
| G _ = raise SMART_STRING
fun F n =
let
- val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct
+ val str =
+ Library.setmp show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
val u = Syntax.parse_term ctxt str
|> TypeInfer.constrain T |> Syntax.check_term ctxt
in
@@ -234,8 +235,9 @@
then quote str
else F (n+1)
end
- handle ERROR mesg => F (n+1)
- | SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
+ handle ERROR mesg => F (n + 1)
+ | SMART_STRING =>
+ error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
in
PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
end
@@ -243,8 +245,7 @@
val smart_string_of_thm = smart_string_of_cterm o cprop_of
-fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
-fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
+fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
fun prin t = writeln (PrintMode.setmp []
(fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
fun pth (HOLThm(ren,thm)) =
@@ -1939,16 +1940,17 @@
then
let
val p1 = quotename constname
- val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype)
+ val p2 = Syntax.string_of_typ_global thy'' ctype
val p3 = string_of_mixfix csyn
val p4 = smart_string_of_cterm crhs
in
- add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
+ add_dump ("constdefs\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ "\n " ^ p4) thy''
end
else
- (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^
- "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
- thy'')
+ add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^
+ Syntax.string_of_typ_global thy'' ctype ^
+ "\" " ^ string_of_mixfix csyn ^ "\n\ndefs\n " ^
+ quotename thmname ^ ": " ^ smart_string_of_cterm crhs) thy''
val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
SOME (_,res) => HOLThm(rens_of linfo,res)
| NONE => raise ERR "new_definition" "Bad conclusion"
@@ -2008,8 +2010,9 @@
in
((cname,cT,mk_syn thy cname)::cs,p)
end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
- val str = Library.foldl (fn (acc,(c,T,csyn)) =>
- acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
+ val str = Library.foldl (fn (acc, (c, T, csyn)) =>
+ acc ^ "\n " ^ quotename c ^ " :: \"" ^
+ Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts)
val thy' = add_dump str thy
val _ = ImportRecorder.add_consts consts
in
@@ -2137,7 +2140,7 @@
fun add_dump_constdefs thy defname constname rhs ty =
let
val n = quotename constname
- val t = Display.string_of_ctyp (ctyp_of thy ty)
+ val t = Syntax.string_of_typ_global thy ty
val syn = string_of_mixfix (mk_syn thy constname)
(*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
val eq = quote (constname ^ " == "^rhs)
@@ -2224,7 +2227,7 @@
(" apply (rule light_ex_imp_nonempty[where t="^
(proc_prop (cterm_of thy4 t))^"])\n"^
(" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
- val str_aty = Display.string_of_ctyp (ctyp_of thy aty)
+ val str_aty = Syntax.string_of_typ_global thy aty
val thy = add_dump_syntax thy rep_name
val thy = add_dump_syntax thy abs_name
val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
--- a/src/HOL/Import/shuffler.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Sat Aug 29 22:01:55 2009 +0200
@@ -57,7 +57,6 @@
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
-val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
fun mk_meta_eq th =
(case concl_of th of
@@ -304,13 +303,14 @@
val lhs = #1 (Logic.dest_equals (prop_of (final init)))
in
if not (lhs aconv origt)
- then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
- writeln (Display.string_of_cterm (cterm_of thy origt));
- writeln (Display.string_of_cterm (cterm_of thy lhs));
- writeln (Display.string_of_cterm (cterm_of thy typet));
- writeln (Display.string_of_cterm (cterm_of thy t));
- app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
- writeln "done")
+ then
+ writeln (cat_lines
+ (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
+ Syntax.string_of_term_global thy origt,
+ Syntax.string_of_term_global thy lhs,
+ Syntax.string_of_term_global thy typet,
+ Syntax.string_of_term_global thy t] @
+ map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
else ()
end
in
@@ -366,13 +366,14 @@
val lhs = #1 (Logic.dest_equals (prop_of (final init)))
in
if not (lhs aconv origt)
- then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
- writeln (Display.string_of_cterm (cterm_of thy origt));
- writeln (Display.string_of_cterm (cterm_of thy lhs));
- writeln (Display.string_of_cterm (cterm_of thy typet));
- writeln (Display.string_of_cterm (cterm_of thy t));
- app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
- writeln "done")
+ then
+ writeln (cat_lines
+ (["Something is utterly wrong: (orig, lhs, frozen type, t, tinst)",
+ Syntax.string_of_term_global thy origt,
+ Syntax.string_of_term_global thy lhs,
+ Syntax.string_of_term_global thy typet,
+ Syntax.string_of_term_global thy t] @
+ map (fn (n, T) => n ^ ": " ^ Syntax.string_of_typ_global thy T) Tinst))
else ()
end
in
@@ -407,9 +408,8 @@
end
| _ => NONE)
else NONE
- | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
- end
- handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
+ | _ => error ("Bad eta_expand argument" ^ Syntax.string_of_term_global thy t)
+ end;
fun mk_tfree s = TFree("'"^s,[])
fun mk_free s t = Free (s,t)
--- a/src/HOL/Int.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Int.thy Sat Aug 29 22:01:55 2009 +0200
@@ -266,7 +266,7 @@
proof
fix k :: int
show "abs k = sup k (- k)"
- by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric])
+ by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
qed
lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
@@ -1487,21 +1487,6 @@
add_special diff_special eq_special less_special le_special
-lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
- max (0::int) 1 = 1 & max (1::int) 0 = 1"
-by(simp add:min_def max_def)
-
-lemmas min_max_special[simp] =
- min_max_01
- max_def[of "0::int" "number_of v", standard, simp]
- min_def[of "0::int" "number_of v", standard, simp]
- max_def[of "number_of u" "0::int", standard, simp]
- min_def[of "number_of u" "0::int", standard, simp]
- max_def[of "1::int" "number_of v", standard, simp]
- min_def[of "1::int" "number_of v", standard, simp]
- max_def[of "number_of u" "1::int", standard, simp]
- min_def[of "number_of u" "1::int", standard, simp]
-
text {* Legacy theorems *}
lemmas zle_int = of_nat_le_iff [where 'a=int]
--- a/src/HOL/Lattices.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Lattices.thy Sat Aug 29 22:01:55 2009 +0200
@@ -125,10 +125,10 @@
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
by (rule antisym) (auto intro: le_infI2)
-lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
by (rule antisym) auto
-lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
by (rule antisym) auto
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
@@ -153,10 +153,10 @@
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
by (rule antisym) (auto intro: le_supI2)
-lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
by (rule antisym) auto
-lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
by (rule antisym) auto
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
@@ -199,7 +199,7 @@
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
proof-
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
- also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
+ also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1)
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
by(simp add:inf_sup_absorb inf_commute)
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
@@ -211,7 +211,7 @@
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
proof-
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
- also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
+ also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1)
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
by(simp add:sup_inf_absorb sup_commute)
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
--- a/src/HOL/Library/Multiset.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Aug 29 22:01:55 2009 +0200
@@ -331,7 +331,7 @@
lemma multiset_inter_count:
"count (A #\<inter> B) x = min (count A x) (count B x)"
-by (simp add: multiset_inter_def min_def)
+by (simp add: multiset_inter_def)
lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
by (simp add: multiset_eq_conv_count_eq multiset_inter_count
@@ -353,7 +353,7 @@
by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
-apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
+apply (simp add: multiset_eq_conv_count_eq multiset_inter_count
split: split_if_asm)
apply clarsimp
apply (erule_tac x = a in allE)
--- a/src/HOL/Library/Word.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Library/Word.thy Sat Aug 29 22:01:55 2009 +0200
@@ -1519,9 +1519,7 @@
proof -
have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le>
2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
- apply (cases "length w1 \<le> length w2")
- apply (auto simp add: max_def)
- done
+ by (auto simp:max_def)
also have "... = 2 ^ max (length w1) (length w2)"
proof -
from lw
@@ -2173,16 +2171,16 @@
apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"])
apply simp_all
apply (rule w_def)
- apply (simp add: w_defs min_def)
- apply (simp add: w_defs min_def)
+ apply (simp add: w_defs)
+ apply (simp add: w_defs)
apply (subst bv_sliceI [where ?j = k and ?i = l and ?w = w and ?w1.0 = w1 and ?w2.0 = "w2 @ w3 @ w4" and ?w3.0 = w5])
apply simp_all
apply (rule w_def)
- apply (simp add: w_defs min_def)
- apply (simp add: w_defs min_def)
+ apply (simp add: w_defs)
+ apply (simp add: w_defs)
apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4])
apply simp_all
- apply (simp_all add: w_defs min_def)
+ apply (simp_all add: w_defs)
done
qed
--- a/src/HOL/Lim.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Lim.thy Sat Aug 29 22:01:55 2009 +0200
@@ -544,8 +544,7 @@
case True thus ?thesis using `0 < s` by auto
next
case False hence "s / 2 \<ge> (x - b) / 2" by auto
- from inf_absorb2[OF this, unfolded inf_real_def]
- have "?x = (x + b) / 2" by auto
+ hence "?x = (x + b) / 2" by(simp add:field_simps)
thus ?thesis using `b < x` by auto
qed
hence "0 \<le> f ?x" using all_le `?x < x` by auto
--- a/src/HOL/Matrix/Matrix.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Matrix/Matrix.thy Sat Aug 29 22:01:55 2009 +0200
@@ -1663,7 +1663,7 @@
apply (simp add: times_matrix_def Rep_mult_matrix)
apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])
apply (simp_all)
-by (simp add: max_def ncols)
+by (simp add: ncols)
lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)"
apply (subst Rep_matrix_inject[THEN sym])
@@ -1671,7 +1671,7 @@
apply (simp add: times_matrix_def Rep_mult_matrix)
apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])
apply (simp_all)
-by (simp add: max_def nrows)
+by (simp add: nrows)
lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
apply (simp add: times_matrix_def)
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Sat Aug 29 22:01:55 2009 +0200
@@ -145,7 +145,7 @@
method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
(is "?app ST LT = ?P ST LT")
proof
- assume "?P ST LT" thus "?app ST LT" by (auto simp add: min_def list_all2_def)
+ assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_def)
next
assume app: "?app ST LT"
hence l: "length fpTs < length ST" by simp
@@ -153,7 +153,7 @@
proof -
have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
moreover from l have "length (take (length fpTs) ST) = length fpTs"
- by (simp add: min_def)
+ by simp
ultimately show ?thesis ..
qed
obtain apTs where
@@ -168,11 +168,11 @@
have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
with app
show "?P ST LT"
- apply (clarsimp simp add: list_all2_def min_def)
+ apply (clarsimp simp add: list_all2_def)
apply ((rule exI)+, (rule conjI)?)+
apply auto
done
-qed
+qed
lemma approx_loc_len [simp]:
"approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
--- a/src/HOL/MicroJava/BV/Effect.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy Sat Aug 29 22:01:55 2009 +0200
@@ -375,7 +375,7 @@
hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l")
by auto
hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs"
- by (auto simp add: min_def)
+ by (auto)
hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST"
by blast
hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []"
@@ -391,7 +391,7 @@
with Pair
have "?app s \<Longrightarrow> ?P s" by (simp only:)
moreover
- have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp simp add: min_def)
+ have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
ultimately
show ?thesis by (rule iffI)
qed
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Sat Aug 29 22:01:55 2009 +0200
@@ -293,7 +293,7 @@
shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
proof -
from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
- with suc wtl show ?thesis by (simp add: min_def)
+ with suc wtl show ?thesis by (simp)
qed
lemma (in lbv) wtl_all:
@@ -308,7 +308,7 @@
with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp
from pc have "is!pc = drop pc is ! 0" by simp
with Cons have "is!pc = i" by simp
- with take pc show ?thesis by (auto simp add: min_def split: split_if_asm)
+ with take pc show ?thesis by (auto)
qed
section "preserves-type"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat Aug 29 22:01:55 2009 +0200
@@ -959,7 +959,7 @@
apply simp
apply (simp (no_asm_simp))+
apply simp
-apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
+apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp))
(* show check_type \<dots> *)
apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
@@ -973,7 +973,7 @@
apply (simp add: check_type_def)
apply (rule states_lower, assumption)
apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append)
-apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def max_def)
+apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def)
apply (simp (no_asm_simp))+
done
@@ -988,7 +988,7 @@
apply (drule_tac x=sttp in spec, erule exE)
apply simp
apply (rule check_type_mono, assumption)
-apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split: prod.split)
+apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
done
(* ********************************************************************** *)
@@ -1058,8 +1058,7 @@
lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
\<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1070,7 +1069,6 @@
bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def ssize_sto_def max_of_list_def)
- apply (simp add: max_def)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="(length ST)" in exI)
@@ -1082,7 +1080,7 @@
\<Longrightarrow> bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)"
apply (erule exE)+
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
- apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+ apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length STo)" in exI)
@@ -1094,8 +1092,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1114,8 +1111,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1131,8 +1127,7 @@
\<Longrightarrow> bc_mt_corresp [Load i]
(\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1154,7 +1149,7 @@
\<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def max_of_list_def )
- apply (simp add: ssize_sto_def) apply (simp add: max_def)
+ apply (simp add: ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps)
apply clarify
@@ -1170,7 +1165,6 @@
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: sup_state_conv)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
- apply (simp add: max_def)
apply (intro strip)
apply (simp add: check_type_simps)
apply clarify
@@ -1182,8 +1176,7 @@
lemma bc_mt_corresp_Dup: "
bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1196,8 +1189,7 @@
lemma bc_mt_corresp_Dup_x1: "
bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1213,7 +1205,7 @@
bc_mt_corresp [IAdd] (replST 2 (PrimT Integer))
(PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
- apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+ apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
@@ -1254,7 +1246,7 @@
apply (frule widen_field, assumption+)
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
- apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+ apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps)
@@ -1305,7 +1297,7 @@
apply (simp add: max_spec_preserves_length [THEN sym])
-- "@{text check_type}"
-apply (simp add: max_ssize_def ssize_sto_def max_def)
+apply (simp add: max_ssize_def ssize_sto_def)
apply (simp add: max_of_list_def)
apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
apply simp
@@ -1316,7 +1308,7 @@
apply (simp only: comp_is_type)
apply (frule method_wf_mdecl) apply assumption apply assumption
apply (simp add: wf_mdecl_def wf_mhead_def)
-apply (simp add: max_def)
+apply (simp)
done
@@ -1473,7 +1465,7 @@
apply (case_tac "sttp1", simp)
apply (rule check_type_lower) apply assumption
apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def)
-apply (simp (no_asm_simp) add: max_of_list_def max_def)
+apply (simp (no_asm_simp) add: max_of_list_def)
(* subgoals \<exists> ... *)
apply (rule surj_pair)+
--- a/src/HOL/Nat.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Nat.thy Sat Aug 29 22:01:55 2009 +0200
@@ -1512,7 +1512,7 @@
by (simp split add: nat_diff_split)
lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
-unfolding min_def by auto
+by auto
lemma inj_on_diff_nat:
assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
--- a/src/HOL/OrderedGroup.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Sat Aug 29 22:01:55 2009 +0200
@@ -1075,16 +1075,17 @@
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def le_iff_sup sup_aci)
+by (simp add: pprt_def sup_aci)
+
lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def le_iff_inf inf_aci)
+by (simp add: nprt_def inf_aci)
lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def le_iff_sup sup_aci)
+by (simp add: pprt_def sup_aci)
lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def le_iff_inf inf_aci)
+by (simp add: nprt_def inf_aci)
lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
proof -
@@ -1118,13 +1119,13 @@
"0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
proof
assume "0 <= a + a"
- hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
+ hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
by (simp add: add_sup_inf_distribs inf_aci)
hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
hence "inf a 0 = 0" by (simp only: add_right_cancel)
- then show "0 <= a" by (simp add: le_iff_inf inf_commute)
-next
+ then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute)
+next
assume a: "0 <= a"
show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
qed
@@ -1194,22 +1195,22 @@
qed
lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
-by (simp add: le_iff_inf nprt_def inf_commute)
+unfolding le_iff_inf by (simp add: nprt_def inf_commute)
lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
-by (simp add: le_iff_sup pprt_def sup_commute)
+unfolding le_iff_sup by (simp add: pprt_def sup_commute)
lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
-by (simp add: le_iff_sup pprt_def sup_commute)
+unfolding le_iff_sup by (simp add: pprt_def sup_commute)
lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
-by (simp add: le_iff_inf nprt_def inf_commute)
+unfolding le_iff_inf by (simp add: nprt_def inf_commute)
lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
-by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
+unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
-by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
+unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
end
@@ -1274,7 +1275,7 @@
proof -
note add_le_cancel_right [of a a "- a", symmetric, simplified]
moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
- then show ?thesis by (auto simp: sup_max max_def)
+ then show ?thesis by (auto simp: sup_max)
qed
lemma abs_if_lattice:
--- a/src/HOL/SEQ.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/SEQ.thy Sat Aug 29 22:01:55 2009 +0200
@@ -582,7 +582,7 @@
ultimately
have "a (max no n) < a n" by auto
with monotone[where m=n and n="max no n"]
- show False by auto
+ show False by (auto simp:max_def split:split_if_asm)
qed
} note top_down = this
{ fix x n m fix a :: "nat \<Rightarrow> real"
--- a/src/HOL/SetInterval.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/SetInterval.thy Sat Aug 29 22:01:55 2009 +0200
@@ -181,9 +181,10 @@
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
-text {* The above four lemmas could be declared as iffs.
- If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
- seems to take forever (more than one hour). *}
+text {* The above four lemmas could be declared as iffs. Unfortunately this
+breaks many proofs. Since it only helps blast, it is better to leave well
+alone *}
+
end
subsubsection{* Emptyness, singletons, subset *}
--- a/src/HOL/Statespace/state_space.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Statespace/state_space.ML Sat Aug 29 22:01:55 2009 +0200
@@ -567,8 +567,8 @@
(case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
[] => []
| [_] => []
- | rs => ["Different types for component " ^ n ^": " ^ commas
- (map (Pretty.string_of o Display.pretty_ctyp o ctyp_of thy o snd) rs)])
+ | rs => ["Different types for component " ^ n ^": " ^
+ commas (map (Syntax.string_of_typ ctxt o snd) rs)])
val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps))
--- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP Sat Aug 29 22:01:55 2009 +0200
@@ -19,6 +19,7 @@
"QuietFlag" => "-q01",
"SubmitButton" => "RunSelectedSystems",
"ProblemSource" => "UPLOAD",
+ "ForceSystem" => "-force",
);
#----Get format and transform options if specified
--- a/src/HOL/Tools/TFL/tfl.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Sat Aug 29 22:01:55 2009 +0200
@@ -8,7 +8,7 @@
sig
val trace: bool ref
val trace_thms: string -> thm list -> unit
- val trace_cterms: string -> cterm list -> unit
+ val trace_cterm: string -> cterm -> unit
type pattern
val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
val wfrec_definition0: theory -> string -> term -> term -> theory * thm
@@ -296,7 +296,7 @@
raise TFL_ERR "no_repeat_vars"
(quote (#1 (dest_Free v)) ^
" occurs repeatedly in the pattern " ^
- quote (Display.string_of_cterm (Thry.typecheck thy pat)))
+ quote (Syntax.string_of_term_global thy pat))
else check rst
in check (FV_multiset pat)
end;
@@ -912,9 +912,10 @@
if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
else ();
-fun trace_cterms s L =
- if !trace then writeln (cat_lines (s :: map Display.string_of_cterm L))
- else ();;
+fun trace_cterm s ct =
+ if !trace then
+ writeln (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)])
+ else ();
fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
@@ -942,7 +943,7 @@
fun simplify_tc tc (r,ind) =
let val tc1 = tych tc
- val _ = trace_cterms "TC before simplification: " [tc1]
+ val _ = trace_cterm "TC before simplification: " tc1
val tc_eq = simplifier tc1
val _ = trace_thms "result: " [tc_eq]
in
--- a/src/HOL/Tools/hologic.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Sat Aug 29 22:01:55 2009 +0200
@@ -586,7 +586,7 @@
(* string *)
-val stringT = Type ("String.string", []);
+val stringT = listT charT;
val mk_string = mk_list charT o map (mk_char o ord) o explode;
val dest_string = implode o map (chr o dest_char) o dest_list;
--- a/src/HOL/Tools/metis_tools.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Sat Aug 29 22:01:55 2009 +0200
@@ -299,7 +299,7 @@
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
that new TVars are distinct and that types can be inferred from terms.*)
- fun inst_inf ctxt thpairs fsubst th =
+ fun inst_inf ctxt thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
@@ -324,11 +324,12 @@
val tms = infer_types ctxt rawtms;
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
- val _ = Output.debug (fn() => "subst_translations:")
- val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^
- Display.string_of_cterm y))
- substs'
- in cterm_instantiate substs' i_th
+ val _ = Output.debug (fn () =>
+ cat_lines ("subst_translations:" ::
+ (substs' |> map (fn (x, y) =>
+ Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
+ Syntax.string_of_term ctxt (term_of y)))));
+ in cterm_instantiate substs' i_th
handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
end;
@@ -610,14 +611,14 @@
if null unused then ()
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
case result of
- (_,ith)::_ =>
- (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
+ (_,ith)::_ =>
+ (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
[ith])
- | _ => (Output.debug (fn () => "Metis: no result");
+ | _ => (Output.debug (fn () => "Metis: no result");
[])
end
- | Metis.Resolution.Satisfiable _ =>
- (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied");
+ | Metis.Resolution.Satisfiable _ =>
+ (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied");
[])
end;
@@ -625,9 +626,9 @@
let val _ = Output.debug (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
+ if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
then (warning "Proof state contains the empty sort"; Seq.empty)
- else
+ else
(Meson.MESON ResAxioms.neg_clausify
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
THEN ResAxioms.expand_defs_tac st0) st0
--- a/src/HOL/Tools/sat_funcs.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Sat Aug 29 22:01:55 2009 +0200
@@ -51,7 +51,7 @@
val trace_sat: bool ref (* input: print trace messages *)
val solver: string ref (* input: name of SAT solver to be used *)
val counter: int ref (* output: number of resolution steps during last proof replay *)
- val rawsat_thm: cterm list -> thm
+ val rawsat_thm: Proof.context -> cterm list -> thm
val rawsat_tac: Proof.context -> int -> tactic
val sat_tac: Proof.context -> int -> tactic
val satx_tac: Proof.context -> int -> tactic
@@ -295,9 +295,7 @@
(* hyps). *)
(* ------------------------------------------------------------------------- *)
-(* Thm.cterm list -> Thm.thm *)
-
-fun rawsat_thm clauses =
+fun rawsat_thm ctxt clauses =
let
(* remove premises that equal "True" *)
val clauses' = filter (fn clause =>
@@ -310,7 +308,7 @@
((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
handle TERM ("dest_Trueprop", _) => false)
orelse (
- warning ("Ignoring non-clausal premise " ^ Display.string_of_cterm clause);
+ warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
false)) clauses'
(* remove trivial clauses -- this is necessary because zChaff removes *)
(* trivial clauses during preprocessing, and otherwise our clause *)
@@ -323,7 +321,8 @@
(* sorted in ascending order *)
val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
val _ = if !trace_sat then
- tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
+ tracing ("Sorted non-trivial clauses:\n" ^
+ cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
else ()
(* translate clauses from HOL terms to PropLogic.prop_formula *)
val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
@@ -411,7 +410,8 @@
(* ------------------------------------------------------------------------- *)
fun rawsat_tac ctxt i =
- Subgoal.FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
+ Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
+ rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)
--- a/src/HOL/UNITY/Simple/Common.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Sat Aug 29 22:01:55 2009 +0200
@@ -65,7 +65,7 @@
lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
\<in> {m} co (maxfg m)"
apply (simp add: mk_total_program_def)
-apply (simp add: constrains_def maxfg_def max_def gasc)
+apply (simp add: constrains_def maxfg_def gasc)
done
(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
@@ -73,7 +73,7 @@
(UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)
\<in> {m} co (maxfg m)"
apply (simp add: mk_total_program_def)
-apply (simp add: constrains_def maxfg_def max_def gasc)
+apply (simp add: constrains_def maxfg_def gasc)
done
--- a/src/HOL/Word/BinBoolList.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy Sat Aug 29 22:01:55 2009 +0200
@@ -918,8 +918,8 @@
apply (frule asm_rl)
apply (drule spec)
apply (erule trans)
- apply (drule_tac x = "bin_cat y n a" in spec)
- apply (simp add : bin_cat_assoc_sym min_def)
+ apply (drule_tac x = "bin_cat y n a" in spec)
+ apply (simp add : bin_cat_assoc_sym)
done
lemma bin_rcat_bl:
--- a/src/HOL/Word/BinGeneral.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy Sat Aug 29 22:01:55 2009 +0200
@@ -493,7 +493,7 @@
lemma sbintrunc_sbintrunc_l:
"n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
- by (rule bin_eqI) (auto simp: nth_sbintr min_def)
+ by (rule bin_eqI) (auto simp: nth_sbintr)
lemma bintrunc_bintrunc_ge:
"n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
@@ -501,14 +501,12 @@
lemma bintrunc_bintrunc_min [simp]:
"bintrunc m (bintrunc n w) = bintrunc (min m n) w"
- apply (unfold min_def)
apply (rule bin_eqI)
apply (auto simp: nth_bintr)
done
lemma sbintrunc_sbintrunc_min [simp]:
"sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
- apply (unfold min_def)
apply (rule bin_eqI)
apply (auto simp: nth_sbintr)
done
--- a/src/HOL/Word/WordDefinition.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy Sat Aug 29 22:01:55 2009 +0200
@@ -380,7 +380,7 @@
"n >= size w ==> bintrunc n (uint w) = uint w"
apply (unfold word_size)
apply (subst word_ubin.norm_Rep [symmetric])
- apply (simp only: bintrunc_bintrunc_min word_size min_def)
+ apply (simp only: bintrunc_bintrunc_min word_size)
apply simp
done
@@ -388,7 +388,7 @@
"wb = word_of_int bin ==> n >= size wb ==>
word_of_int (bintrunc n bin) = wb"
unfolding word_size
- by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric] min_def)
+ by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric])
lemmas bintr_uint = bintr_uint' [unfolded word_size]
lemmas wi_bintr = wi_bintr' [unfolded word_size]
--- a/src/HOL/Word/WordShift.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/HOL/Word/WordShift.thy Sat Aug 29 22:01:55 2009 +0200
@@ -319,7 +319,7 @@
lemma bl_shiftl:
"to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
- by (simp add: shiftl_bl word_rep_drop word_size min_def)
+ by (simp add: shiftl_bl word_rep_drop word_size)
lemma shiftl_zero_size:
fixes x :: "'a::len0 word"
@@ -1018,8 +1018,7 @@
word_of_int (bin_cat w (size b) (uint b))"
apply (unfold word_cat_def word_size)
apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
- word_ubin.eq_norm bintr_cat min_def)
- apply arith
+ word_ubin.eq_norm bintr_cat)
done
lemma word_cat_split_alt:
--- a/src/Pure/General/markup.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/General/markup.scala Sat Aug 29 22:01:55 2009 +0200
@@ -6,8 +6,9 @@
package isabelle
-object Markup {
+object Markup
+{
/* name */
val NAME = "name"
@@ -25,7 +26,8 @@
val FILE = "file"
val ID = "id"
- val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
+ val POSITION_PROPERTIES =
+ Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
val POSITION = "position"
val LOCATION = "location"
--- a/src/Pure/General/position.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/General/position.scala Sat Aug 29 22:01:55 2009 +0200
@@ -6,11 +6,9 @@
package isabelle
-import java.util.Properties
-
-object Position {
-
+object Position
+{
type T = List[(String, String)]
private def get_string(name: String, pos: T): Option[String] =
@@ -41,5 +39,4 @@
val end = end_offset_of(pos)
(begin, if (end.isDefined) end else begin.map(_ + 1))
}
-
}
--- a/src/Pure/General/scan.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/General/scan.scala Sat Aug 29 22:01:55 2009 +0200
@@ -11,7 +11,6 @@
object Scan
{
-
/** Lexicon -- position tree **/
object Lexicon
--- a/src/Pure/General/yxml.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/General/yxml.scala Sat Aug 29 22:01:55 2009 +0200
@@ -7,8 +7,8 @@
package isabelle
-object YXML {
-
+object YXML
+{
/* chunk markers */
private val X = '\5'
@@ -22,7 +22,8 @@
private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] {
private val end = source.length
private var state = if (end == 0) None else get_chunk(-1)
- private def get_chunk(i: Int) = {
+ private def get_chunk(i: Int) =
+ {
if (i < end) {
var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
Some((source.subSequence(i + 1, j), j))
@@ -55,8 +56,8 @@
}
- def parse_body(source: CharSequence) = {
-
+ def parse_body(source: CharSequence): List[XML.Tree] =
+ {
/* stack operations */
var stack: List[((String, XML.Attributes), List[XML.Tree])] = null
@@ -94,7 +95,7 @@
}
}
- def parse(source: CharSequence) =
+ def parse(source: CharSequence): XML.Tree =
parse_body(source) match {
case List(result) => result
case Nil => XML.Text("")
@@ -108,14 +109,15 @@
XML.Elem (Markup.BAD, Nil,
List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
- def parse_body_failsafe(source: CharSequence) = {
+ def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
+ {
try { parse_body(source) }
catch { case _: RuntimeException => List(markup_failsafe(source)) }
}
- def parse_failsafe(source: CharSequence) = {
+ def parse_failsafe(source: CharSequence): XML.Tree =
+ {
try { parse(source) }
catch { case _: RuntimeException => markup_failsafe(source) }
}
-
}
--- a/src/Pure/IsaMakefile Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/IsaMakefile Sat Aug 29 22:01:55 2009 +0200
@@ -122,10 +122,9 @@
General/symbol.scala General/xml.scala General/yxml.scala \
Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \
System/cygwin.scala System/gui_setup.scala \
- System/isabelle_process.scala System/isabelle_system.scala \
- System/platform.scala Thy/completion.scala Thy/thy_header.scala \
- Tools/isabelle_syntax.scala
-
+ System/isabelle_process.scala System/isabelle_syntax.scala \
+ System/isabelle_system.scala System/platform.scala \
+ Thy/completion.scala Thy/thy_header.scala \
JAR_DIR = $(ISABELLE_HOME)/lib/classes
PURE_JAR = $(JAR_DIR)/Pure.jar
--- a/src/Pure/Isar/isar.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/Isar/isar.scala Sat Aug 29 22:01:55 2009 +0200
@@ -14,13 +14,13 @@
/* basic editor commands */
def create_command(id: String, text: String) =
- output_sync("Isar.command " + IsabelleSyntax.encode_string(id) + " " +
- IsabelleSyntax.encode_string(text))
+ output_sync("Isar.command " + Isabelle_Syntax.encode_string(id) + " " +
+ Isabelle_Syntax.encode_string(text))
def insert_command(prev: String, id: String) =
- output_sync("Isar.insert " + IsabelleSyntax.encode_string(prev) + " " +
- IsabelleSyntax.encode_string(id))
+ output_sync("Isar.insert " + Isabelle_Syntax.encode_string(prev) + " " +
+ Isabelle_Syntax.encode_string(id))
def remove_command(id: String) =
- output_sync("Isar.remove " + IsabelleSyntax.encode_string(id))
+ output_sync("Isar.remove " + Isabelle_Syntax.encode_string(id))
}
--- a/src/Pure/Isar/isar_document.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala Sat Aug 29 22:01:55 2009 +0200
@@ -6,7 +6,9 @@
package isabelle
-object IsarDocument {
+
+object IsarDocument
+{
/* unique identifiers */
type State_ID = String
@@ -14,6 +16,7 @@
type Document_ID = String
}
+
trait IsarDocument extends Isabelle_Process
{
import IsarDocument._
@@ -22,20 +25,20 @@
/* commands */
def define_command(id: Command_ID, text: String) {
- output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
- IsabelleSyntax.encode_string(text))
+ output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
+ Isabelle_Syntax.encode_string(text))
}
/* documents */
def begin_document(id: Document_ID, path: String) {
- output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
- IsabelleSyntax.encode_string(path))
+ output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
+ Isabelle_Syntax.encode_string(path))
}
def end_document(id: Document_ID) {
- output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
+ output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
}
def edit_document(old_id: Document_ID, new_id: Document_ID,
@@ -44,21 +47,21 @@
def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
{
edit match {
- case (id, None) => IsabelleSyntax.append_string(id, result)
+ case (id, None) => Isabelle_Syntax.append_string(id, result)
case (id, Some(id2)) =>
- IsabelleSyntax.append_string(id, result)
+ Isabelle_Syntax.append_string(id, result)
result.append(" ")
- IsabelleSyntax.append_string(id2, result)
+ Isabelle_Syntax.append_string(id2, result)
}
}
val buf = new StringBuilder(40)
buf.append("Isar.edit_document ")
- IsabelleSyntax.append_string(old_id, buf)
+ Isabelle_Syntax.append_string(old_id, buf)
buf.append(" ")
- IsabelleSyntax.append_string(new_id, buf)
+ Isabelle_Syntax.append_string(new_id, buf)
buf.append(" ")
- IsabelleSyntax.append_list(append_edit, edits, buf)
+ Isabelle_Syntax.append_list(append_edit, edits, buf)
output_sync(buf.toString)
}
}
--- a/src/Pure/Isar/outer_keyword.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/Isar/outer_keyword.scala Sat Aug 29 22:01:55 2009 +0200
@@ -6,8 +6,9 @@
package isabelle
-object OuterKeyword {
+object OuterKeyword
+{
val MINOR = "minor"
val CONTROL = "control"
val DIAG = "diag"
--- a/src/Pure/System/isabelle_process.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/System/isabelle_process.scala Sat Aug 29 22:01:55 2009 +0200
@@ -204,14 +204,14 @@
def command(text: String) =
- output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
+ output_sync("Isabelle.command " + Isabelle_Syntax.encode_string(text))
def command(props: List[(String, String)], text: String) =
- output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
- IsabelleSyntax.encode_string(text))
+ output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
+ Isabelle_Syntax.encode_string(text))
def ML(text: String) =
- output_sync("ML_val " + IsabelleSyntax.encode_string(text))
+ output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
def close() = synchronized { // FIXME watchdog/timeout
output_raw("\u0000")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_syntax.scala Sat Aug 29 22:01:55 2009 +0200
@@ -0,0 +1,74 @@
+/* Title: Pure/System/isabelle_syntax.scala
+ Author: Makarius
+
+Isabelle outer syntax.
+*/
+
+package isabelle
+
+
+object Isabelle_Syntax
+{
+ /* string token */
+
+ def append_string(str: String, result: StringBuilder)
+ {
+ result.append("\"")
+ for (c <- str) {
+ if (c < 32 || c == '\\' || c == '\"') {
+ result.append("\\")
+ if (c < 10) result.append('0')
+ if (c < 100) result.append('0')
+ result.append(c.asInstanceOf[Int].toString)
+ }
+ else result.append(c)
+ }
+ result.append("\"")
+ }
+
+ def encode_string(str: String) =
+ {
+ val result = new StringBuilder(str.length + 10)
+ append_string(str, result)
+ result.toString
+ }
+
+
+ /* list */
+
+ def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
+ result: StringBuilder)
+ {
+ result.append("(")
+ val elems = body.elements
+ if (elems.hasNext) append_elem(elems.next, result)
+ while (elems.hasNext) {
+ result.append(", ")
+ append_elem(elems.next, result)
+ }
+ result.append(")")
+ }
+
+ def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
+ {
+ val result = new StringBuilder
+ append_list(append_elem, elems, result)
+ result.toString
+ }
+
+
+ /* properties */
+
+ def append_properties(props: List[(String, String)], result: StringBuilder)
+ {
+ append_list((p: (String, String), res) =>
+ { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
+ }
+
+ def encode_properties(props: List[(String, String)]) =
+ {
+ val result = new StringBuilder
+ append_properties(props, result)
+ result.toString
+ }
+}
--- a/src/Pure/System/isabelle_system.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala Sat Aug 29 22:01:55 2009 +0200
@@ -42,13 +42,11 @@
val rc = proc.waitFor
(output, rc)
}
-
}
class Isabelle_System
{
-
/** unique ids **/
private var id_count: BigInt = 0
@@ -244,6 +242,7 @@
}
+
/** system tools **/
/* external processes */
@@ -296,6 +295,7 @@
}
+
/** Isabelle resources **/
/* components */
--- a/src/Pure/Thy/thy_header.scala Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/Thy/thy_header.scala Sat Aug 29 22:01:55 2009 +0200
@@ -6,8 +6,9 @@
package isabelle
-object ThyHeader {
+object ThyHeader
+{
val HEADER = "header"
val THEORY = "theory"
val IMPORTS = "imports"
--- a/src/Pure/Tools/isabelle_syntax.scala Sat Aug 29 21:58:33 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-/* Title: Pure/Tools/isabelle_syntax.scala
- Author: Makarius
-
-Isabelle outer syntax.
-*/
-
-package isabelle
-
-
-object IsabelleSyntax {
-
- /* string token */
-
- def append_string(str: String, result: StringBuilder)
- {
- result.append("\"")
- for (c <- str) {
- if (c < 32 || c == '\\' || c == '\"') {
- result.append("\\")
- if (c < 10) result.append('0')
- if (c < 100) result.append('0')
- result.append(c.asInstanceOf[Int].toString)
- }
- else result.append(c)
- }
- result.append("\"")
- }
-
- def encode_string(str: String) =
- {
- val result = new StringBuilder(str.length + 10)
- append_string(str, result)
- result.toString
- }
-
-
- /* list */
-
- def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
- result: StringBuilder)
- {
- result.append("(")
- val elems = body.elements
- if (elems.hasNext) append_elem(elems.next, result)
- while (elems.hasNext) {
- result.append(", ")
- append_elem(elems.next, result)
- }
- result.append(")")
- }
-
- def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
- {
- val result = new StringBuilder
- append_list(append_elem, elems, result)
- result.toString
- }
-
-
- /* properties */
-
- def append_properties(props: List[(String, String)], result: StringBuilder)
- {
- append_list((p: (String, String), res) =>
- { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
- }
-
- def encode_properties(props: List[(String, String)]) =
- {
- val result = new StringBuilder
- append_properties(props, result)
- result.toString
- }
-}
--- a/src/Pure/display.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/display.ML Sat Aug 29 22:01:55 2009 +0200
@@ -27,10 +27,6 @@
val string_of_thm_without_context: thm -> string
val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
val pretty_thms: Proof.context -> thm list -> Pretty.T
- val pretty_ctyp: ctyp -> Pretty.T
- val string_of_ctyp: ctyp -> string
- val pretty_cterm: cterm -> Pretty.T
- val string_of_cterm: cterm -> string
val print_syntax: theory -> unit
val pretty_full_theory: bool -> theory -> Pretty.T list
end;
@@ -119,15 +115,6 @@
fun pretty_thms ctxt = pretty_thms_aux ctxt true;
-(* other printing commands *)
-
-fun pretty_ctyp cT = Syntax.pretty_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun string_of_ctyp cT = Syntax.string_of_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-
-fun pretty_cterm ct = Syntax.pretty_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
-fun string_of_cterm ct = Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
-
-
(** print theory **)
--- a/src/Pure/old_goals.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Pure/old_goals.ML Sat Aug 29 22:01:55 2009 +0200
@@ -362,10 +362,7 @@
(case Seq.pull (tac st0) of
SOME(st,_) => st
| _ => error ("prove_goal: tactic failed"))
- in mkresult (check, cond_timeit (!Output.timing) "" statef) end
- handle e => (print_sign_exn_unit (Thm.theory_of_cterm chorn) e;
- writeln ("The exception above was raised for\n" ^
- Display.string_of_cterm chorn); raise e);
+ in mkresult (check, cond_timeit (!Output.timing) "" statef) end;
(*Two variants: one checking the result, one not.
Neither prints runtime messages: they are for internal packages.*)
--- a/src/Tools/induct.ML Sat Aug 29 21:58:33 2009 +0200
+++ b/src/Tools/induct.ML Sat Aug 29 22:01:55 2009 +0200
@@ -288,21 +288,21 @@
(* prep_inst *)
-fun prep_inst thy align tune (tm, ts) =
+fun prep_inst ctxt align tune (tm, ts) =
let
- val cert = Thm.cterm_of thy;
+ val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
fun prep_var (x, SOME t) =
let
val cx = cert x;
val xT = #T (Thm.rep_cterm cx);
val ct = cert (tune t);
- val tT = Thm.ctyp_of_term ct;
+ val tT = #T (Thm.rep_cterm ct);
in
- if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct)
+ if Type.could_unify (tT, xT) then SOME (cx, ct)
else error (Pretty.string_of (Pretty.block
[Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
- Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
- Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
+ Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1,
+ Syntax.pretty_typ ctxt tT]))
end
| prep_var (_, NONE) = NONE;
val xs = vars_of tm;
@@ -342,12 +342,11 @@
fun cases_tac ctxt insts opt_rule facts =
let
val thy = ProofContext.theory_of ctxt;
- val cert = Thm.cterm_of thy;
fun inst_rule r =
if null insts then `RuleCases.get r
else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
- |> maps (prep_inst thy align_left I)
+ |> maps (prep_inst ctxt align_left I)
|> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
val ruleq =
@@ -411,8 +410,8 @@
(* prepare rule *)
-fun rule_instance thy inst rule =
- Drule.cterm_instantiate (prep_inst thy align_left I (Thm.prop_of rule, inst)) rule;
+fun rule_instance ctxt inst rule =
+ Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
fun internalize k th =
th |> Thm.permute_prems 0 k
@@ -589,7 +588,7 @@
(if null insts then `RuleCases.get r
else (align_left "Rule has fewer conclusions than arguments given"
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
- |> maps (prep_inst thy align_right (atomize_term thy))
+ |> maps (prep_inst ctxt align_right (atomize_term thy))
|> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
|> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
@@ -619,7 +618,7 @@
THEN' inner_atomize_tac) j))
THEN' atomize_tac) i st |> Seq.maps (fn st' =>
guess_instance ctxt (internalize more_consumes rule) i st'
- |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
+ |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
CASES (rule_cases rule' cases)
(Tactic.rtac rule' i THEN
@@ -657,7 +656,7 @@
fun inst_rule r =
if null inst then `RuleCases.get r
- else Drule.cterm_instantiate (prep_inst thy align_right I (main_prop_of r, inst)) r
+ else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
|> pair (RuleCases.get r);
fun ruleq goal =
@@ -673,7 +672,7 @@
|> Seq.maps (RuleCases.consume [] facts)
|> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
guess_instance ctxt rule i st
- |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
+ |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
(Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
--- a/src/ZF/Datatype_ZF.thy Sat Aug 29 21:58:33 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy Sat Aug 29 22:01:55 2009 +0200
@@ -14,9 +14,9 @@
(*Typechecking rules for most datatypes involving univ*)
structure Data_Arg =
struct
- val intrs =
+ val intrs =
[@{thm SigmaI}, @{thm InlI}, @{thm InrI},
- @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
+ @{thm Pair_in_univ}, @{thm Inl_in_univ}, @{thm Inr_in_univ},
@{thm zero_in_univ}, @{thm A_into_univ}, @{thm nat_into_univ}, @{thm UnCI}];
@@ -25,7 +25,7 @@
end;
-structure Data_Package =
+structure Data_Package =
Add_datatype_def_Fun
(structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
and Su=Standard_Sum
@@ -37,16 +37,16 @@
(*Typechecking rules for most codatatypes involving quniv*)
structure CoData_Arg =
struct
- val intrs =
+ val intrs =
[@{thm QSigmaI}, @{thm QInlI}, @{thm QInrI},
- @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
+ @{thm QPair_in_quniv}, @{thm QInl_in_quniv}, @{thm QInr_in_quniv},
@{thm zero_in_quniv}, @{thm A_into_quniv}, @{thm nat_into_quniv}, @{thm UnCI}];
val elims = [make_elim @{thm QInlD}, make_elim @{thm QInrD}, (*for mutual recursion*)
@{thm QSigmaE}, @{thm qsumE}]; (*allows * and + in spec*)
end;
-structure CoData_Package =
+structure CoData_Package =
Add_datatype_def_Fun
(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
and Su=Quine_Sum
@@ -69,9 +69,9 @@
val datatype_ss = @{simpset};
fun proc sg ss old =
- let val _ = if !trace then writeln ("data_free: OLD = " ^
- Display.string_of_cterm (cterm_of sg old))
- else ()
+ let val _ =
+ if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term_global sg old)
+ else ()
val (lhs,rhs) = FOLogic.dest_eq old
val (lhead, largs) = strip_comb lhs
and (rhead, rargs) = strip_comb rhs
@@ -81,15 +81,15 @@
handle Option => raise Match;
val rcon_info = the (Symtab.lookup (ConstructorsData.get sg) rname)
handle Option => raise Match;
- val new =
- if #big_rec_name lcon_info = #big_rec_name rcon_info
+ val new =
+ if #big_rec_name lcon_info = #big_rec_name rcon_info
andalso not (null (#free_iffs lcon_info)) then
if lname = rname then mk_new (largs, rargs)
else Const("False",FOLogic.oT)
else raise Match
- val _ = if !trace then
- writeln ("NEW = " ^ Display.string_of_cterm (Thm.cterm_of sg new))
- else ();
+ val _ =
+ if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
+ else ();
val goal = Logic.mk_equals (old, new)
val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
(fn _ => rtac iff_reflection 1 THEN