--- a/Admin/isatest/annomaly.ML Sat Aug 29 10:50:04 2009 +0200
+++ b/Admin/isatest/annomaly.ML Sat Aug 29 12:01:25 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/doc-src/rail.ML Sat Aug 29 10:50:04 2009 +0200
+++ b/doc-src/rail.ML Sat Aug 29 12:01:25 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 10:50:04 2009 +0200
+++ b/src/FOL/fologic.ML Sat Aug 29 12:01:25 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 10:50:04 2009 +0200
+++ b/src/FOL/intprover.ML Sat Aug 29 12:01:25 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 10:50:04 2009 +0200
+++ b/src/FOLP/hypsubst.ML Sat Aug 29 12:01:25 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 10:50:04 2009 +0200
+++ b/src/FOLP/simp.ML Sat Aug 29 12:01:25 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/abstract/Ring2.thy Sat Aug 29 10:50:04 2009 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sat Aug 29 12:01:25 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