# HG changeset patch # User wenzelm # Date 1251540085 -7200 # Node ID 696d64ed85dad93f07934b37bd8c8d497a5535ed # Parent a89f876731c5bdf03ad86f8729c50bc477ad392f eliminated hard tabs; diff -r a89f876731c5 -r 696d64ed85da Admin/isatest/annomaly.ML --- 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; diff -r a89f876731c5 -r 696d64ed85da doc-src/rail.ML --- 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 diff -r a89f876731c5 -r 696d64ed85da src/FOL/fologic.ML --- 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; diff -r a89f876731c5 -r 696d64ed85da src/FOL/intprover.ML --- 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)); diff -r a89f876731c5 -r 696d64ed85da src/FOLP/hypsubst.ML --- 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); diff -r a89f876731c5 -r 696d64ed85da src/FOLP/simp.ML --- 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))) diff -r a89f876731c5 -r 696d64ed85da src/HOL/Algebra/abstract/Ring2.thy --- 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