--- a/Admin/isatest/annomaly.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/Admin/isatest/annomaly.ML Tue Sep 01 14:13:34 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/Admin/isatest/isatest-makeall Tue Sep 01 14:12:18 2009 +0200
+++ b/Admin/isatest/isatest-makeall Tue Sep 01 14:13:34 2009 +0200
@@ -80,7 +80,7 @@
NICE=""
;;
- macbroy21)
+ macbroy22)
MFLAGS="-k"
NICE=""
;;
--- a/Admin/isatest/isatest-makedist Tue Sep 01 14:12:18 2009 +0200
+++ b/Admin/isatest/isatest-makedist Tue Sep 01 14:13:34 2009 +0200
@@ -94,13 +94,13 @@
$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
# give test some time to copy settings and start
sleep 15
-$SSH macbroy21 "$MAKEALL $HOME/settings/at-poly"
+$SSH macbroy22 "$MAKEALL $HOME/settings/at-poly"
sleep 15
$SSH macbroy20 "$MAKEALL $HOME/settings/at-poly-5.1-para-e"
sleep 15
#$SSH macbroy24 "$MAKEALL -l HOL proofterms $HOME/settings/at-sml-dev-p"
#sleep 15
-$SSH macbroy22 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
+$SSH macbroy21 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
sleep 15
$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
sleep 15
--- a/Admin/isatest/isatest-stats Tue Sep 01 14:12:18 2009 +0200
+++ b/Admin/isatest/isatest-stats Tue Sep 01 14:13:34 2009 +0200
@@ -6,7 +6,7 @@
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
+PLATFORMS="at-poly at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
ISABELLE_SESSIONS="\
HOL-Plain \
--- a/NEWS Tue Sep 01 14:12:18 2009 +0200
+++ b/NEWS Tue Sep 01 14:13:34 2009 +0200
@@ -18,22 +18,25 @@
*** HOL ***
-* New testing tool "Mirabelle" for automated (proof) tools. Applies several
-tools and tactics like sledgehammer, metis, or quickcheck, to every proof step
-in a theory. To be used in batch mode via "isabelle mirabelle".
-
-* New proof method "sos" (sum of squares) for nonlinear real arithmetic
-(originally due to John Harison). It requires Library/Sum_Of_Squares.
-It is not a complete decision procedure but works well in practice
-on quantifier-free real arithmetic with +, -, *, ^, =, <= and <,
-i.e. boolean combinations of equalities and inequalities between
-polynomials. It makes use of external semidefinite programming solvers.
-For more information and examples see Library/Sum_Of_Squares.
-
-* Set.UNIV and Set.empty are mere abbreviations for top and bot. INCOMPATIBILITY.
-
-* More convenient names for set intersection and union. INCOMPATIBILITY:
-
+* New testing tool "Mirabelle" for automated (proof) tools. Applies
+several tools and tactics like sledgehammer, metis, or quickcheck, to
+every proof step in a theory. To be used in batch mode via the
+"mirabelle" utility.
+
+* New proof method "sos" (sum of squares) for nonlinear real
+arithmetic (originally due to John Harison). It requires
+Library/Sum_Of_Squares. It is not a complete decision procedure but
+works well in practice on quantifier-free real arithmetic with +, -,
+*, ^, =, <= and <, i.e. boolean combinations of equalities and
+inequalities between polynomials. It makes use of external
+semidefinite programming solvers. For more information and examples
+see src/HOL/Library/Sum_Of_Squares.
+
+* Set.UNIV and Set.empty are mere abbreviations for top and bot.
+INCOMPATIBILITY.
+
+* More convenient names for set intersection and union.
+INCOMPATIBILITY:
Set.Int ~> Set.inter
Set.Un ~> Set.union
@@ -43,8 +46,6 @@
etc.
INCOMPATIBILITY.
-* New quickcheck implementation using new code generator.
-
* New class "boolean_algebra".
* Refinements to lattices classes:
@@ -81,15 +82,16 @@
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
-* Relation composition "R O S" now has a "more standard" argument order,
-i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
+* Relation composition "R O S" now has a "more standard" argument
+order, i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
-may occationally break, since the O_assoc rule was not rewritten like this.
-Fix using O_assoc[symmetric].
-The same applies to the curried version "R OO S".
-
-* GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
-infinite sets. It is shown that they form a complete lattice.
+may occationally break, since the O_assoc rule was not rewritten like
+this. Fix using O_assoc[symmetric]. The same applies to the curried
+version "R OO S".
+
+* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
+of finite and infinite sets. It is shown that they form a complete
+lattice.
* ML antiquotation @{code_datatype} inserts definition of a datatype
generated by the code generator; see Predicate.thy for an example.
@@ -97,9 +99,9 @@
* New method "linarith" invokes existing linear arithmetic decision
procedure only.
-* Implementation of quickcheck using generic code generator; default
-generators are provided for all suitable HOL types, records and
-datatypes.
+* New implementation of quickcheck uses generic code generator;
+default generators are provided for all suitable HOL types, records
+and datatypes.
* Constants Set.Pow and Set.image now with authentic syntax;
object-logic definitions Set.Pow_def and Set.image_def.
@@ -110,6 +112,9 @@
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
Suc_plus1 -> Suc_eq_plus1
+* Moved theorems:
+Wellfounded.in_inv_image -> Relation.in_inv_image
+
* New sledgehammer option "Full Types" in Proof General settings menu.
Causes full type information to be output to the ATPs. This slows
ATPs down considerably but eliminates a source of unsound "proofs"
@@ -121,17 +126,13 @@
DatatypePackage ~> Datatype
InductivePackage ~> Inductive
- etc.
-
INCOMPATIBILITY.
* NewNumberTheory: Jeremy Avigad's new version of part of
NumberTheory. If possible, use NewNumberTheory, not NumberTheory.
-* Simplified interfaces of datatype module. INCOMPATIBILITY.
-
-* Abbreviation "arbitrary" of "undefined" has disappeared; use
-"undefined" directly. INCOMPATIBILITY.
+* Discontinued abbreviation "arbitrary" of constant
+"undefined". INCOMPATIBILITY, use "undefined" directly.
* New evaluator "approximate" approximates an real valued term using
the same method as the approximation method.
@@ -155,10 +156,14 @@
* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
parallel tactical reasoning.
-* Tactical FOCUS is similar to SUBPROOF, but allows the body tactic to
-introduce new subgoals and schematic variables. FOCUS_PARAMS is
-similar, but focuses on the parameter prefix only, leaving subgoal
-premises unchanged.
+* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS
+are similar to SUBPROOF, but are slightly more flexible: only the
+specified parts of the subgoal are imported into the context, and the
+body tactic may introduce new subgoals and schematic variables.
+
+* Old tactical METAHYPS, which does not observe the proof context, has
+been renamed to Old_Goals.METAHYPS and awaits deletion. Use SUBPROOF
+or Subgoal.FOCUS etc.
* Renamed functor TableFun to Table, and GraphFun to Graph. (Since
functors have their own ML name space there is no point to mark them
@@ -179,6 +184,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 Tue Sep 01 14:12:18 2009 +0200
+++ b/doc-src/rail.ML Tue Sep 01 14:13:34 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/etc/settings Tue Sep 01 14:12:18 2009 +0200
+++ b/etc/settings Tue Sep 01 14:13:34 2009 +0200
@@ -173,7 +173,7 @@
# The pdf file viewer
if [ $(uname -s) = Darwin ]; then
- PDF_VIEWER=open
+ PDF_VIEWER="open -W -n"
else
PDF_VIEWER=xpdf
fi
--- a/src/FOL/fologic.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/FOL/fologic.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/FOL/intprover.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/FOLP/hypsubst.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/FOLP/simp.ML Tue Sep 01 14:13:34 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/Divisibility.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Tue Sep 01 14:13:34 2009 +0200
@@ -2656,25 +2656,7 @@
shows "(x \<in> carrier G \<and> x gcdof a b) =
greatest (division_rel G) x (Lower (division_rel G) {a, b})"
unfolding isgcd_def greatest_def Lower_def elem_def
-proof (simp, safe)
- fix xa
- assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> xa divides x"
- assume r2[rule_format]: "\<forall>y\<in>carrier G. y divides a \<and> y divides b \<longrightarrow> y divides x"
-
- assume "xa \<in> carrier G" "x divides a" "x divides b"
- with carr
- show "xa divides x"
- by (fast intro: r1 r2)
-next
- fix a' y
- assume r1[rule_format]:
- "\<forall>xa\<in>{l. \<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> l divides x} \<inter> carrier G.
- xa divides x"
- assume "y \<in> carrier G" "y divides a" "y divides b"
- with carr
- show "y divides x"
- by (fast intro: r1)
-qed (simp, simp)
+by auto
lemma lcmof_leastUpper:
fixes G (structure)
@@ -2682,25 +2664,7 @@
shows "(x \<in> carrier G \<and> x lcmof a b) =
least (division_rel G) x (Upper (division_rel G) {a, b})"
unfolding islcm_def least_def Upper_def elem_def
-proof (simp, safe)
- fix xa
- assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides xa"
- assume r2[rule_format]: "\<forall>y\<in>carrier G. a divides y \<and> b divides y \<longrightarrow> x divides y"
-
- assume "xa \<in> carrier G" "a divides x" "b divides x"
- with carr
- show "x divides xa"
- by (fast intro: r1 r2)
-next
- fix a' y
- assume r1[rule_format]:
- "\<forall>xa\<in>{l. \<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides l} \<inter> carrier G.
- x divides xa"
- assume "y \<in> carrier G" "a divides y" "b divides y"
- with carr
- show "x divides y"
- by (fast intro: r1)
-qed (simp, simp)
+by auto
lemma somegcd_meet:
fixes G (structure)
--- a/src/HOL/Algebra/UnivPoly.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Tue Sep 01 14:13:34 2009 +0200
@@ -592,15 +592,14 @@
proof (cases "n = k")
case True
then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
- by (simp cong: R.finsum_cong add: ivl_disj_int_singleton Pi_def)
+ by (simp cong: R.finsum_cong add: Pi_def)
also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
by (simp only: ivl_disj_un_singleton)
finally show ?thesis .
next
case False with n_le_k have n_less_k: "n < k" by arith
with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
- by (simp add: R.finsum_Un_disjoint f1 f2
- ivl_disj_int_singleton Pi_def del: Un_insert_right)
+ by (simp add: R.finsum_Un_disjoint f1 f2 Pi_def del: Un_insert_right)
also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
by (simp only: ivl_disj_un_singleton)
also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
@@ -817,15 +816,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"
@@ -945,8 +938,7 @@
also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
- by (simp cong: R.finsum_cong
- add: ivl_disj_int_singleton deg_aboveD R Pi_def)
+ by (simp cong: R.finsum_cong add: deg_aboveD R Pi_def)
finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
= coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>"
@@ -989,8 +981,7 @@
have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<k} \<union> {k}. ?s i) k"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff P p k"
- by (simp cong: R.finsum_cong
- add: ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
+ by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R RR Pi_def)
finally show ?thesis .
next
case False
@@ -998,8 +989,7 @@
coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k"
by (simp only: ivl_disj_un_singleton)
also from False have "... = coeff P p k"
- by (simp cong: R.finsum_cong
- add: ivl_disj_int_singleton coeff_finsum deg_aboveD R Pi_def)
+ by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R Pi_def)
finally show ?thesis .
qed
qed (simp_all add: R Pi_def)
--- a/src/HOL/Algebra/abstract/Ring2.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Tue Sep 01 14:13:34 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"
@@ -678,8 +674,7 @@
also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff p (deg p) * coeff q (deg q)"
- by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
- setsum_0 deg_aboveD)
+ by (simp add: setsum_Un_disjoint setsum_0 deg_aboveD)
finally have "setsum ?s {.. deg p + deg q}
= coeff p (deg p) * coeff q (deg q)" .
with nz show "setsum ?s {.. deg p + deg q} ~= 0"
@@ -723,8 +718,7 @@
have "... = coeff (setsum ?s ({..<k} Un {k})) k"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff p k"
- by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
- setsum_0 coeff_natsum deg_aboveD)
+ by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
finally show ?thesis .
next
case False
@@ -732,8 +726,7 @@
coeff (setsum ?s ({..<deg p} Un {deg p})) k"
by (simp only: ivl_disj_un_singleton)
also from False have "... = coeff p k"
- by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
- setsum_0 coeff_natsum deg_aboveD)
+ by (simp add: setsum_Un_disjoint setsum_0 coeff_natsum deg_aboveD)
finally show ?thesis .
qed
qed
--- a/src/HOL/Auth/Event.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Auth/Event.thy Tue Sep 01 14:13:34 2009 +0200
@@ -139,9 +139,11 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
+lemmas Says_imp_parts_knows_Spy =
+ Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
+
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
- parts.Body [THEN revcut_rl, standard]
+ Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard]
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
--- a/src/HOL/Auth/KerberosIV.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Tue Sep 01 14:13:34 2009 +0200
@@ -899,7 +899,6 @@
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp))
apply blast
-atp_minimize [atp=spass] Crypt_imp_invKey_keysFor invKey_K new_keys_not_used
apply (metis Crypt_imp_invKey_keysFor invKey_K new_keys_not_used)
apply (clarify)
apply (frule Says_Tgs_message_form, assumption)
@@ -1316,7 +1315,6 @@
txt{*K4*}
apply blast
txt{*Level 8: K5*}
-atp_minimize [atp=e] Tgs_not_bad authKeysI less_SucI mem_def nat_add_commute servK_notin_authKeysD spies_partsEs(1)
apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
txt{*Oops1*}
apply (blast dest!: unique_authKeys intro: less_SucI)
--- a/src/HOL/Auth/KerberosV.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Auth/KerberosV.thy Tue Sep 01 14:13:34 2009 +0200
@@ -697,9 +697,7 @@
txt{*K4*}
apply (force dest!: Crypt_imp_keysFor, clarify)
txt{*K6*}
-apply (drule Says_imp_spies [THEN parts.Inj, THEN parts.Fst])
-apply (drule Says_imp_spies [THEN parts.Inj, THEN parts.Snd])
-apply (blast dest!: unique_CryptKey)
+apply (metis Says_imp_spies Says_ticket_parts analz.Fst analz.Inj analz_conj_parts unique_CryptKey)
done
text{*Needs a unicity theorem, hence moved here*}
@@ -841,13 +839,10 @@
apply (erule kerbV.induct, analz_mono_contra)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, simp_all, blast)
-txt{*K4 splits into distinct subcases*}
-apply auto
-txt{*servK can't have been enclosed in two certificates*}
- prefer 2 apply (blast dest: unique_CryptKey)
-txt{*servK is fresh and so could not have been used, by
- @{text new_keys_not_used}*}
-apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
+txt{*K4*}
+apply (metis Auth_fresh_not_AKcryptSK Crypt_imp_invKey_keysFor Says_ticket_analz
+ analz.Fst invKey_K new_keys_not_analzd parts.Fst Says_imp_parts_knows_Spy
+ unique_CryptKey)
done
text{*Long term keys are not issued as servKeys*}
@@ -981,9 +976,7 @@
txt{*K4*}
apply (blast dest!: authK_not_AKcryptSK)
txt{*Oops1*}
-apply clarify
-apply simp
-apply (blast dest!: AKcryptSK_analz_insert)
+apply (metis AKcryptSK_analz_insert insert_Key_singleton)
done
text{* First simplification law for analz: no session keys encrypt
@@ -1039,8 +1032,8 @@
\<in> set evs; authK \<in> symKeys;
Key authK \<in> analz (spies evs); evs \<in> kerbV \<rbrakk>
\<Longrightarrow> Key servK \<in> analz (spies evs)"
-apply (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Fst])
-done
+ by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
+
text{*lemma @{text servK_notin_authKeysD} not needed in version V*}
@@ -1112,16 +1105,16 @@
apply (frule_tac [5] Says_ticket_analz)
apply (safe del: impI conjI impCE)
apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes)
-txt{*Fake*}
-apply spy_analz
-txt{*K2*}
-apply (blast intro: parts_insertI less_SucI)
-txt{*K4*}
-apply (blast dest: authTicket_authentic Confidentiality_Kas)
-txt{*Oops1*}
+ txt{*Fake*}
+ apply spy_analz
+ txt{*K2*}
+ apply (blast intro: parts_insertI less_SucI)
+ txt{*K4*}
+ apply (blast dest: authTicket_authentic Confidentiality_Kas)
+ txt{*Oops1*}
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
txt{*Oops2*}
- apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
+apply (metis Suc_le_eq linorder_linear linorder_not_le msg.simps(2) unique_servKeys)
done
@@ -1270,17 +1263,7 @@
Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; evs \<in> kerbV \<rbrakk>
\<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
-apply (frule authK_authentic)
-apply assumption+
-apply (frule servK_authentic)
-prefer 2 apply (blast dest: authK_authentic Says_Kas_message_form)
-apply assumption+
-apply clarify
-apply (blast dest: K4_imp_K2 Key_unique_SesKey intro!: Says_K6)
-(*Single command proof: much slower!
-apply (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro!: Says_K6)
-*)
-done
+ by (metis authK_authentic Oops_range_spies1 Says_K6 servK_authentic u_K4_imp_K2 unique_authKeys)
lemma A_authenticates_B_r:
"\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
@@ -1301,8 +1284,7 @@
apply (erule_tac [9] exE)
apply (frule_tac [9] K4_imp_K2)
apply assumption+
-apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs
-)
+apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs)
done
@@ -1478,7 +1460,7 @@
...expands as follows - including extra exE because of new form of lemmas*)
apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE)
apply (case_tac "Key authK \<in> analz (spies evs5)")
-apply (drule Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Fst, THEN analz_Decrypt', THEN analz.Fst], assumption, assumption, simp)
+ apply (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE)
apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst])
apply (frule servK_authentic_ter, blast, assumption+)
--- a/src/HOL/Auth/Kerberos_BAN.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Tue Sep 01 14:13:34 2009 +0200
@@ -288,15 +288,8 @@
on evs)"
apply (unfold before_def)
apply (erule rev_mp)
-apply (erule bankerberos.induct, simp_all)
-txt{*We need this simplification only for Message 2*}
-apply (simp (no_asm) add: takeWhile_tail)
-apply auto
-txt{*Two subcases of Message 2. Subcase: used before*}
-apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD]
- used_takeWhile_used)
-txt{*subcase: CT before*}
-apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
+apply (erule bankerberos.induct, simp_all add: takeWhile_tail)
+apply (metis length_rev set_rev takeWhile_void used_evs_rev)
done
@@ -492,6 +485,7 @@
txt{*BK3*}
apply (blast dest: Kab_authentic unique_session_keys)
done
+
lemma lemma_B [rule_format]:
"\<lbrakk> B \<notin> bad; evs \<in> bankerberos \<rbrakk>
\<Longrightarrow> Key K \<notin> analz (spies evs) \<longrightarrow>
@@ -585,9 +579,8 @@
txt{*BK2*}
apply (blast intro: parts_insertI less_SucI)
txt{*BK3*}
-apply (case_tac "Aa \<in> bad")
- prefer 2 apply (blast dest: Kab_authentic unique_session_keys)
-apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI)
+apply (metis Crypt_Spy_analz_bad Kab_authentic Says_imp_analz_Spy
+ Says_imp_parts_knows_Spy analz.Snd less_SucI unique_session_keys)
txt{*Oops: PROOF FAILS if unsafe intro below*}
apply (blast dest: unique_session_keys intro!: less_SucI)
done
--- a/src/HOL/Auth/NS_Shared.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Tue Sep 01 14:13:34 2009 +0200
@@ -273,11 +273,11 @@
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
txt{*NS2*}
apply blast
-txt{*NS3, Server sub-case*}
+txt{*NS3*}
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
dest: Says_imp_knows_Spy analz.Inj unique_session_keys)
-txt{*NS3, Spy sub-case; also Oops*}
-apply (blast dest: unique_session_keys)+
+txt{*Oops*}
+apply (blast dest: unique_session_keys)
done
--- a/src/HOL/Auth/Recur.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Auth/Recur.thy Tue Sep 01 14:13:34 2009 +0200
@@ -419,15 +419,10 @@
apply spy_analz
txt{*RA2*}
apply blast
-txt{*RA3 remains*}
+txt{*RA3*}
apply (simp add: parts_insert_spies)
-txt{*Now we split into two cases. A single blast could do it, but it would take
- a CPU minute.*}
-apply (safe del: impCE)
-txt{*RA3, case 1: use lemma previously proved by induction*}
-apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key])
-txt{*RA3, case 2: K is an old key*}
-apply (blast dest: resp_analz_insert dest: Key_in_parts_respond)
+apply (metis Key_in_parts_respond parts.Body parts.Fst resp_analz_insert
+ respond_Spy_not_see_session_key usedI)
txt{*RA4*}
apply blast
done
--- a/src/HOL/Bali/Example.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Bali/Example.thy Tue Sep 01 14:13:34 2009 +0200
@@ -1167,7 +1167,6 @@
apply (simp,rule assigned.select_convs)
apply (simp)
apply simp
-apply blast
apply simp
apply (simp add: intersect_ts_def)
done
--- a/src/HOL/Complete_Lattice.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Finite_Set.thy Tue Sep 01 14:13:34 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/GCD.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/GCD.thy Tue Sep 01 14:13:34 2009 +0200
@@ -1895,8 +1895,6 @@
lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
-declare successor_int_def[simp]
-
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
--- a/src/HOL/HOL.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/HOL.thy Tue Sep 01 14:13:34 2009 +0200
@@ -29,6 +29,7 @@
"~~/src/Tools/induct.ML"
("~~/src/Tools/induct_tacs.ML")
("Tools/recfun_codegen.ML")
+ "~~/src/Tools/more_conv.ML"
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
--- a/src/HOL/HoareParallel/Graph.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Import/hol4rews.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Int.thy Tue Sep 01 14:13:34 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/IsaMakefile Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 01 14:13:34 2009 +0200
@@ -108,6 +108,7 @@
$(SRC)/Tools/random_word.ML \
$(SRC)/Tools/value.ML \
$(SRC)/Tools/Code_Generator.thy \
+ $(SRC)/Tools/more_conv.ML \
HOL.thy \
Tools/hologic.ML \
Tools/recfun_codegen.ML \
--- a/src/HOL/Isar_examples/Mutilated_Checkerboard.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Isar_examples/Mutilated_Checkerboard.thy Tue Sep 01 14:13:34 2009 +0200
@@ -113,7 +113,7 @@
lemma evnodd_insert: "evnodd (insert (i, j) C) b =
(if (i + j) mod 2 = b
then insert (i, j) (evnodd C b) else evnodd C b)"
- by (simp add: evnodd_def) blast
+ by (simp add: evnodd_def)
subsection {* Dominoes *}
--- a/src/HOL/Lattices.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Lattices.thy Tue Sep 01 14:13:34 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/Abstract_Rat.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Abstract_Rat.thy Tue Sep 01 14:13:34 2009 +0200
@@ -189,14 +189,9 @@
have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
assume H: ?lhs
- {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" hence ?rhs
- using na nb H
- apply (simp add: INum_def split_def isnormNum_def)
- apply (cases "a = 0", simp_all)
- apply (cases "b = 0", simp_all)
- apply (cases "a' = 0", simp_all)
- apply (cases "a' = 0", simp_all add: of_int_eq_0_iff)
- done}
+ {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
+ hence ?rhs using na nb H
+ by (simp add: INum_def split_def isnormNum_def split: split_if_asm)}
moreover
{ assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
@@ -517,10 +512,7 @@
have n0: "isnormNum 0\<^sub>N" by simp
show ?thesis using nx ny
apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
- apply (simp add: INum_def split_def isnormNum_def fst_conv snd_conv)
- apply (cases "a=0",simp_all)
- apply (cases "a'=0",simp_all)
- done
+ by (simp add: INum_def split_def isnormNum_def fst_conv snd_conv split: split_if_asm)
}
qed
lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
--- a/src/HOL/Library/Continuity.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Continuity.thy Tue Sep 01 14:13:34 2009 +0200
@@ -156,7 +156,7 @@
apply (rule up_chainI)
apply simp
apply (drule Un_absorb1)
-apply (auto simp add: nat_not_singleton)
+apply (auto split:split_if_asm)
done
@@ -184,8 +184,7 @@
apply (rule down_chainI)
apply simp
apply (drule Int_absorb1)
-apply auto
-apply (auto simp add: nat_not_singleton)
+apply (auto split:split_if_asm)
done
--- a/src/HOL/Library/Convex_Euclidean_Space.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Tue Sep 01 14:13:34 2009 +0200
@@ -3355,9 +3355,8 @@
qed(auto intro!:path_connected_singleton) next
case False hence *:"{x::real^'n. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" unfolding not_le apply -apply(rule set_ext,rule)
unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib)
- have ***:"\<And>xa. (if xa = 0 then 0 else 1) \<noteq> 1 \<Longrightarrow> xa = 0" apply(rule ccontr) by auto
have **:"{x::real^'n. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule)
- unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto intro!: ***)
+ unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm)
have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
apply(rule continuous_at_norm[unfolded o_def]) by auto
--- a/src/HOL/Library/Euclidean_Space.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Tue Sep 01 14:13:34 2009 +0200
@@ -1055,28 +1055,6 @@
lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e"
by (metis basic_trans_rules(21) norm_triangle_ineq)
-lemma setsum_delta:
- assumes fS: "finite S"
- shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
-proof-
- let ?f = "(\<lambda>k. if k=a then b k else 0)"
- {assume a: "a \<notin> S"
- hence "\<forall> k\<in> S. ?f k = 0" by simp
- hence ?thesis using a by simp}
- moreover
- {assume a: "a \<in> S"
- let ?A = "S - {a}"
- let ?B = "{a}"
- have eq: "S = ?A \<union> ?B" using a by blast
- have dj: "?A \<inter> ?B = {}" by simp
- from fS have fAB: "finite ?A" "finite ?B" by auto
- have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
- using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
- by simp
- then have ?thesis using a by simp}
- ultimately show ?thesis by blast
-qed
-
lemma component_le_norm: "\<bar>x$i\<bar> <= norm (x::real ^ 'n::finite)"
apply (simp add: norm_vector_def)
apply (rule member_le_setL2, simp_all)
@@ -2079,13 +2057,6 @@
lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \<star> B) + (A \<star> C)"
by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)
-lemma setsum_delta':
- assumes fS: "finite S" shows
- "setsum (\<lambda>k. if a = k then b k else 0) S =
- (if a\<in> S then b a else 0)"
- using setsum_delta[OF fS, of a b, symmetric]
- by (auto intro: setsum_cong)
-
lemma matrix_mul_lid:
fixes A :: "'a::semiring_1 ^ 'm ^ 'n::finite"
shows "mat 1 ** A = A"
@@ -3926,14 +3897,6 @@
shows "finite s \<and> card s \<le> card t"
by (metis exchange_lemma[OF f i sp] hassize_def finite_subset card_mono)
-lemma finite_Atleast_Atmost[simp]: "finite {f x |x. x\<in> {(i::'a::finite_intvl_succ) .. j}}"
-proof-
- have eq: "{f x |x. x\<in> {i .. j}} = f ` {i .. j}" by auto
- show ?thesis unfolding eq
- apply (rule finite_imageI)
- apply (rule finite_intvl)
- done
-qed
lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
proof-
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Sep 01 14:13:34 2009 +0200
@@ -633,8 +633,7 @@
by (auto simp add: inverse_eq_divide power_divide)
from k have kn: "k > n"
- apply (simp add: leastP_def setge_def fps_sum_rep_nth)
- by (cases "k \<le> n", auto)
+ by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
then have "dist (?s n) a < (1/2)^n" unfolding dth
by (auto intro: power_strict_decreasing)
also have "\<dots> <= (1/2)^n0" using nn0
@@ -1244,10 +1243,9 @@
{assume n0: "n \<noteq> 0"
then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
"{0..n - 1}\<union>{n} = {0..n}"
- apply (simp_all add: expand_set_eq) by presburger+
+ by (auto simp: expand_set_eq)
have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
- "{0..n - 1}\<inter>{n} ={}" using n0
- by (simp_all add: expand_set_eq, presburger+)
+ "{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
have f: "finite {0}" "finite {1}" "finite {2 .. n}"
"finite {0 .. n - 1}" "finite {n}" by simp_all
have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}"
@@ -2503,6 +2501,29 @@
then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp
qed
+lemma fps_ginv_deriv:
+ assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0"
+ shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
+proof-
+ let ?ia = "fps_ginv b a"
+ let ?iXa = "fps_ginv X a"
+ let ?d = "fps_deriv"
+ let ?dia = "?d ?ia"
+ have iXa0: "?iXa $ 0 = 0" by (simp add: fps_ginv_def)
+ have da0: "?d a $ 0 \<noteq> 0" using a1 by simp
+ from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" by simp
+ then have "(?d ?ia oo a) * ?d a = ?d b" unfolding fps_compose_deriv[OF a0] .
+ then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" by simp
+ then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a"
+ by (simp add: fps_divide_def)
+ then have "(?d ?ia oo a) oo ?iXa = (?d b / ?d a) oo ?iXa "
+ unfolding inverse_mult_eq_1[OF da0] by simp
+ then have "?d ?ia oo (a oo ?iXa) = (?d b / ?d a) oo ?iXa"
+ unfolding fps_compose_assoc[OF iXa0 a0] .
+ then show ?thesis unfolding fps_inv_ginv[symmetric]
+ unfolding fps_inv_right[OF a0 a1] by simp
+qed
+
subsection{* Elementary series *}
subsubsection{* Exponential series *}
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Sep 01 14:13:34 2009 +0200
@@ -577,11 +577,12 @@
next
case (pCons c cs)
{assume c0: "c = 0"
- from pCons.hyps pCons.prems c0 have ?case apply auto
+ from pCons.hyps pCons.prems c0 have ?case
+ apply (auto)
apply (rule_tac x="k+1" in exI)
apply (rule_tac x="a" in exI, clarsimp)
apply (rule_tac x="q" in exI)
- by (auto simp add: power_Suc)}
+ by (auto)}
moreover
{assume c0: "c\<noteq>0"
hence ?case apply-
--- a/src/HOL/Library/Multiset.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Sep 01 14:13:34 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/Permutations.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Permutations.thy Tue Sep 01 14:13:34 2009 +0200
@@ -843,9 +843,7 @@
unfolding permutes_def by metis+
from eq have "(Fun.swap a b id o p) a = (Fun.swap a c id o q) a" by simp
hence bc: "b = c"
- apply (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong)
- apply (cases "a = b", auto)
- by (cases "b = c", auto)
+ by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm)
from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp
hence "p = q" unfolding o_assoc swap_id_idempotent
by (simp add: o_def)
--- a/src/HOL/Library/Univ_Poly.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Tue Sep 01 14:13:34 2009 +0200
@@ -820,37 +820,24 @@
done
qed
-lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp
+lemma (in semiring_0) pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0"
+by simp
lemma (in semiring_0) pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp
lemma (in semiring_0) pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)"
unfolding pnormal_def by simp
lemma (in semiring_0) pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p"
- unfolding pnormal_def
- apply (cases "pnormalize p = []", auto)
- by (cases "c = 0", auto)
+ unfolding pnormal_def by(auto split: split_if_asm)
lemma (in semiring_0) pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0"
-proof(induct p)
- case Nil thus ?case by (simp add: pnormal_def)
-next
- case (Cons a as) thus ?case
- apply (simp add: pnormal_def)
- apply (cases "pnormalize as = []", simp_all)
- apply (cases "as = []", simp_all)
- apply (cases "a=0", simp_all)
- apply (cases "a=0", simp_all)
- done
-qed
+by(induct p) (simp_all add: pnormal_def split: split_if_asm)
lemma (in semiring_0) pnormal_length: "pnormal p \<Longrightarrow> 0 < length p"
unfolding pnormal_def length_greater_0_conv by blast
lemma (in semiring_0) pnormal_last_length: "\<lbrakk>0 < length p ; last p \<noteq> 0\<rbrakk> \<Longrightarrow> pnormal p"
- apply (induct p, auto)
- apply (case_tac "p = []", auto)
- apply (simp add: pnormal_def)
- by (rule pnormal_cons, auto)
+by (induct p) (auto simp: pnormal_def split: split_if_asm)
+
lemma (in semiring_0) pnormal_id: "pnormal p \<longleftrightarrow> (0 < length p \<and> last p \<noteq> 0)"
using pnormal_last_length pnormal_length pnormal_last_nonzero by blast
@@ -918,9 +905,7 @@
qed
lemma (in semiring_0) pnormalize_eq: "last p \<noteq> 0 \<Longrightarrow> pnormalize p = p"
- apply (induct p, auto)
- apply (case_tac p, auto)+
- done
+by (induct p) (auto split: split_if_asm)
lemma (in semiring_0) last_pnormalize: "pnormalize p \<noteq> [] \<Longrightarrow> last (pnormalize p) \<noteq> 0"
by (induct p, auto)
--- a/src/HOL/Library/Word.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/Word.thy Tue Sep 01 14:13:34 2009 +0200
@@ -1008,12 +1008,7 @@
fix xs
assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
thus "norm_signed (\<zero>#xs) = \<zero>#xs"
- apply (simp add: norm_signed_Cons)
- apply safe
- apply simp_all
- apply (rule norm_unsigned_equal)
- apply assumption
- done
+ by (simp add: norm_signed_Cons norm_unsigned_equal split: split_if_asm)
next
fix xs
assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
@@ -1519,9 +1514,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 +2166,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/Library/normarith.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/normarith.ML Tue Sep 01 14:13:34 2009 +0200
@@ -15,7 +15,7 @@
structure NormArith : NORM_ARITH =
struct
- open Conv Thm Conv2;
+ open Conv Thm;
val bool_eq = op = : bool *bool -> bool
fun dest_ratconst t = case term_of t of
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
@@ -322,6 +322,7 @@
val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE
else SOME(norm_cmul_rule v t))
(v ~~ nubs)
+ fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
in inequality_canon_rule ctxt (end_itlist norm_add_rule ths)
end
val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @
@@ -332,9 +333,9 @@
in RealArith.real_linear_prover translator
(map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
zerodests,
- map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
+ map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
- map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
+ map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) gts)
end
in val real_vector_combo_prover = real_vector_combo_prover
@@ -353,6 +354,7 @@
val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
+ fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
--- a/src/HOL/Library/positivstellensatz.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Tue Sep 01 14:13:34 2009 +0200
@@ -81,82 +81,6 @@
structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t)));
structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
- (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
-structure Conv2 =
-struct
- open Conv
-fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
-fun is_comb t = case (term_of t) of _$_ => true | _ => false;
-fun is_abs t = case (term_of t) of Abs _ => true | _ => false;
-
-fun end_itlist f l =
- case l of
- [] => error "end_itlist"
- | [x] => x
- | (h::t) => f h (end_itlist f t);
-
- fun absc cv ct = case term_of ct of
- Abs (v,_, _) =>
- let val (x,t) = Thm.dest_abs (SOME v) ct
- in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t)
- end
- | _ => all_conv ct;
-
-fun cache_conv conv =
- let
- val tab = ref Termtab.empty
- fun cconv t =
- case Termtab.lookup (!tab) (term_of t) of
- SOME th => th
- | NONE => let val th = conv t
- in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
- in cconv end;
-fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
- handle CTERM _ => false;
-
-local
- fun thenqc conv1 conv2 tm =
- case try conv1 tm of
- SOME th1 => (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
- | NONE => conv2 tm
-
- fun thencqc conv1 conv2 tm =
- let val th1 = conv1 tm
- in (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
- end
- fun comb_qconv conv tm =
- let val (l,r) = Thm.dest_comb tm
- in (case try conv l of
- SOME th1 => (case try conv r of SOME th2 => Thm.combination th1 th2
- | NONE => Drule.fun_cong_rule th1 r)
- | NONE => Drule.arg_cong_rule l (conv r))
- end
- fun repeatqc conv tm = thencqc conv (repeatqc conv) tm
- fun sub_qconv conv tm = if is_abs tm then absc conv tm else comb_qconv conv tm
- fun once_depth_qconv conv tm =
- (conv else_conv (sub_qconv (once_depth_qconv conv))) tm
- fun depth_qconv conv tm =
- thenqc (sub_qconv (depth_qconv conv))
- (repeatqc conv) tm
- fun redepth_qconv conv tm =
- thenqc (sub_qconv (redepth_qconv conv))
- (thencqc conv (redepth_qconv conv)) tm
- fun top_depth_qconv conv tm =
- thenqc (repeatqc conv)
- (thencqc (sub_qconv (top_depth_qconv conv))
- (thencqc conv (top_depth_qconv conv))) tm
- fun top_sweep_qconv conv tm =
- thenqc (repeatqc conv)
- (sub_qconv (top_sweep_qconv conv)) tm
-in
-val (once_depth_conv, depth_conv, rdepth_conv, top_depth_conv, top_sweep_conv) =
- (fn c => try_conv (once_depth_qconv c),
- fn c => try_conv (depth_qconv c),
- fn c => try_conv (redepth_qconv c),
- fn c => try_conv (top_depth_qconv c),
- fn c => try_conv (top_sweep_qconv c));
-end;
-end;
(* Some useful derived rules *)
@@ -373,15 +297,6 @@
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
fun is_comb t = case (term_of t) of _$_ => true | _ => false;
-fun cache_conv conv =
- let
- val tab = ref Termtab.empty
- fun cconv t =
- case Termtab.lookup (!tab) (term_of t) of
- SOME th => th
- | NONE => let val th = conv t
- in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
- in cconv end;
fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
handle CTERM _ => false;
@@ -571,7 +486,7 @@
val nnf_norm_conv' =
nnf_conv then_conv
literals_conv [@{term "op &"}, @{term "op |"}] []
- (cache_conv
+ (More_Conv.cache_conv
(first_conv [real_lt_conv, real_le_conv,
real_eq_conv, real_not_lt_conv,
real_not_le_conv, real_not_eq_conv, all_conv]))
--- a/src/HOL/Lim.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Lim.thy Tue Sep 01 14:13:34 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/List.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/List.thy Tue Sep 01 14:13:34 2009 +0200
@@ -881,10 +881,8 @@
lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
by (induct xs) auto
-lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
-apply (induct j, simp_all)
-apply (erule ssubst, auto)
-done
+lemma set_upt [simp]: "set[i..<j] = {i..<j}"
+by (induct j) (simp_all add: atLeastLessThanSuc)
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
@@ -2394,6 +2392,30 @@
nth_Cons_number_of [simp]
+subsubsection {* @{text upto}: interval-list on @{typ int} *}
+
+(* FIXME make upto tail recursive? *)
+
+function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
+"upto i j = (if i \<le> j then i # [i+1..j] else [])"
+by auto
+termination
+by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
+
+declare upto.simps[code, simp del]
+
+lemmas upto_rec_number_of[simp] =
+ upto.simps[of "number_of m" "number_of n", standard]
+
+lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
+by(simp add: upto.simps)
+
+lemma set_upto[simp]: "set[i..j] = {i..j}"
+apply(induct i j rule:upto.induct)
+apply(simp add: upto.simps simp_from_to)
+done
+
+
subsubsection {* @{text "distinct"} and @{text remdups} *}
lemma distinct_append [simp]:
@@ -2448,6 +2470,12 @@
lemma distinct_upt[simp]: "distinct[i..<j]"
by (induct j) auto
+lemma distinct_upto[simp]: "distinct[i..j]"
+apply(induct i j rule:upto.induct)
+apply(subst upto.simps)
+apply(simp)
+done
+
lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
apply(induct xs arbitrary: i)
apply simp
@@ -3091,6 +3119,12 @@
lemma sorted_upt[simp]: "sorted[i..<j]"
by (induct j) (simp_all add:sorted_append)
+lemma sorted_upto[simp]: "sorted[i..j]"
+apply(induct i j rule:upto.induct)
+apply(subst upto.simps)
+apply(simp add:sorted_Cons)
+done
+
subsubsection {* @{text sorted_list_of_set} *}
@@ -3124,89 +3158,6 @@
end
-subsubsection {* @{text upto}: the generic interval-list *}
-
-class finite_intvl_succ = linorder +
-fixes successor :: "'a \<Rightarrow> 'a"
-assumes finite_intvl: "finite{a..b}"
-and successor_incr: "a < successor a"
-and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
-
-context finite_intvl_succ
-begin
-
-definition
- upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
-"upto i j == sorted_list_of_set {i..j}"
-
-lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
-by(simp add:upto_def finite_intvl)
-
-lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
-apply(insert successor_incr[of i])
-apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
-apply(metis ord_discrete less_le not_le)
-done
-
-lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
- sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
-apply(simp add:sorted_list_of_set_def upto_def)
-apply (rule the1_equality[OF finite_sorted_distinct_unique])
- apply (simp add:finite_intvl)
-apply(rule the1I2[OF finite_sorted_distinct_unique])
- apply (simp add:finite_intvl)
-apply (simp add: sorted_Cons insert_intvl Ball_def)
-apply (metis successor_incr leD less_imp_le order_trans)
-done
-
-lemma sorted_list_of_set_rec2: "i \<le> j \<Longrightarrow>
- sorted_list_of_set {i..successor j} =
- sorted_list_of_set {i..j} @ [successor j]"
-apply(simp add:sorted_list_of_set_def upto_def)
-apply (rule the1_equality[OF finite_sorted_distinct_unique])
- apply (simp add:finite_intvl)
-apply(rule the1I2[OF finite_sorted_distinct_unique])
- apply (simp add:finite_intvl)
-apply (simp add: sorted_append Ball_def expand_set_eq)
-apply(rule conjI)
-apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr)
-apply (metis leD linear order_trans successor_incr)
-done
-
-lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
-by(simp add: upto_def sorted_list_of_set_rec)
-
-lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
-by(simp add: upto_rec)
-
-lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
-by(simp add: upto_def sorted_list_of_set_rec2)
-
-end
-
-text{* The integers are an instance of the above class: *}
-
-instantiation int:: finite_intvl_succ
-begin
-
-definition
-successor_int_def[simp]: "successor = (%i\<Colon>int. i+1)"
-
-instance
-by intro_classes (simp_all add: successor_int_def)
-
-end
-
-text{* Now @{term"[i..j::int]"} is defined for integers. *}
-
-hide (open) const successor
-
-lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
-by(rule upto_rec2[where 'a = int, simplified successor_int_def])
-
-lemmas upto_rec_number_of_int[simp] = upto_rec[of "number_of m :: int" "number_of n", standard]
-
-
subsubsection {* @{text lists}: the list-forming operator over sets *}
inductive_set
@@ -3829,9 +3780,7 @@
"{n<..<m} = set [Suc n..<m]"
by auto
-lemma atLeastLessThan_upt [code_unfold]:
- "{n..<m} = set [n..<m]"
-by auto
+lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
lemma greaterThanAtMost_upt [code_unfold]:
"{n<..m} = set [Suc n..<Suc m]"
@@ -3880,12 +3829,123 @@
"{i<..j::int} = set [i+1..j]"
by auto
-lemma atLeastAtMost_upto [code_unfold]:
- "{i..j::int} = set [i..j]"
-by auto
+lemmas atLeastAtMost_upto [code_unfold] = set_upto[symmetric]
lemma setsum_set_upto_conv_listsum [code_unfold]:
"setsum f (set [i..j::int]) = listsum (map f [i..j])"
by (rule setsum_set_distinct_conv_listsum) simp
+
+text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
+and similiarly for @{text"\<exists>"}. *}
+
+function all_from_to_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
+"all_from_to_nat P i j =
+ (if i < j then if P i then all_from_to_nat P (i+1) j else False
+ else True)"
+by auto
+termination
+by (relation "measure(%(P,i,j). j - i)") auto
+
+declare all_from_to_nat.simps[simp del]
+
+lemma all_from_to_nat_iff_ball:
+ "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)"
+proof(induct P i j rule:all_from_to_nat.induct)
+ case (1 P i j)
+ let ?yes = "i < j & P i"
+ show ?case
+ proof (cases)
+ assume ?yes
+ hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)"
+ by(simp add: all_from_to_nat.simps)
+ also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp
+ also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R")
+ proof
+ assume L: ?L
+ show ?R
+ proof clarify
+ fix n assume n: "n : {i..<j}"
+ show "P n"
+ proof cases
+ assume "n = i" thus "P n" using L by simp
+ next
+ assume "n ~= i"
+ hence "i+1 <= n" using n by auto
+ thus "P n" using L n by simp
+ qed
+ qed
+ next
+ assume R: ?R thus ?L using `?yes` 1 by auto
+ qed
+ finally show ?thesis .
+ next
+ assume "~?yes" thus ?thesis by(auto simp add: all_from_to_nat.simps)
+ qed
+qed
+
+
+lemma list_all_iff_all_from_to_nat[code_unfold]:
+ "list_all P [i..<j] = all_from_to_nat P i j"
+by(simp add: all_from_to_nat_iff_ball list_all_iff)
+
+lemma list_ex_iff_not_all_from_to_not_nat[code_unfold]:
+ "list_ex P [i..<j] = (~all_from_to_nat (%x. ~P x) i j)"
+by(simp add: all_from_to_nat_iff_ball list_ex_iff)
+
+
+function all_from_to_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
+"all_from_to_int P i j =
+ (if i <= j then if P i then all_from_to_int P (i+1) j else False
+ else True)"
+by auto
+termination
+by (relation "measure(%(P,i,j). nat(j - i + 1))") auto
+
+declare all_from_to_int.simps[simp del]
+
+lemma all_from_to_int_iff_ball:
+ "all_from_to_int P i j = (ALL n : {i .. j}. P n)"
+proof(induct P i j rule:all_from_to_int.induct)
+ case (1 P i j)
+ let ?yes = "i <= j & P i"
+ show ?case
+ proof (cases)
+ assume ?yes
+ hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)"
+ by(simp add: all_from_to_int.simps)
+ also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp
+ also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R")
+ proof
+ assume L: ?L
+ show ?R
+ proof clarify
+ fix n assume n: "n : {i..j}"
+ show "P n"
+ proof cases
+ assume "n = i" thus "P n" using L by simp
+ next
+ assume "n ~= i"
+ hence "i+1 <= n" using n by auto
+ thus "P n" using L n by simp
+ qed
+ qed
+ next
+ assume R: ?R thus ?L using `?yes` 1 by auto
+ qed
+ finally show ?thesis .
+ next
+ assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps)
+ qed
+qed
+
+lemma list_all_iff_all_from_to_int[code_unfold]:
+ "list_all P [i..j] = all_from_to_int P i j"
+by(simp add: all_from_to_int_iff_ball list_all_iff)
+
+lemma list_ex_iff_not_all_from_to_not_int[code_unfold]:
+ "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
+by(simp add: all_from_to_int_iff_ball list_ex_iff)
+
+
end
--- a/src/HOL/Matrix/Matrix.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Matrix/Matrix.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Tue Sep 01 14:13:34 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/BV/Typing_Framework_err.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Tue Sep 01 14:13:34 2009 +0200
@@ -62,15 +62,9 @@
lemma bounded_err_stepI:
"\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n))
\<Longrightarrow> bounded (err_step n ap step) n"
-apply (unfold bounded_def)
-apply clarify
-apply (simp add: err_step_def split: err.splits)
-apply (simp add: error_def)
- apply blast
-apply (simp split: split_if_asm)
- apply (blast dest: in_map_sndD)
-apply (simp add: error_def)
-apply blast
+apply (clarsimp simp: bounded_def err_step_def split: err.splits)
+apply (simp add: error_def image_def)
+apply (blast dest: in_map_sndD)
done
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Sep 01 14:13:34 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/MicroJava/J/TypeRel.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Sep 01 14:13:34 2009 +0200
@@ -97,6 +97,14 @@
qed
qed
+text {* Code generator setup (FIXME!) *}
+
+consts_code
+ "wfrec" ("\<module>wfrec?")
+attach {*
+fun wfrec f x = f (wfrec f) x;
+*}
+
consts
method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
--- a/src/HOL/Nat.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Nat.thy Tue Sep 01 14:13:34 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)"
@@ -1588,9 +1588,6 @@
lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
using inc_induct[of 0 k P] by blast
-lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
- by auto
-
(*The others are
i - j - k = i - (j + k),
k \<le> j ==> j - k + i = j + i - k,
--- a/src/HOL/Nominal/nominal_thmdecls.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Tue Sep 01 14:13:34 2009 +0200
@@ -74,7 +74,7 @@
val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
val ([goal_term, pi''], ctxt') = Variable.import_terms false
[HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
- val _ = Display.print_cterm (cterm_of thy goal_term)
+ val _ = writeln (Syntax.string_of_term ctxt' goal_term);
in
Goal.prove ctxt' [] [] goal_term
(fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
--- a/src/HOL/OrderedGroup.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Tue Sep 01 14:13:34 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/Recdef.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Recdef.thy Tue Sep 01 14:13:34 2009 +0200
@@ -19,6 +19,65 @@
("Tools/recdef.ML")
begin
+inductive
+ wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
+ for R :: "('a * 'a) set"
+ and F :: "('a => 'b) => 'a => 'b"
+where
+ wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
+ wfrec_rel R F x (F g x)"
+
+constdefs
+ cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
+ "cut f r x == (%y. if (y,x):r then f y else undefined)"
+
+ adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
+ "adm_wf R F == ALL f g x.
+ (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
+
+ wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
+ [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+
+subsection{*Well-Founded Recursion*}
+
+text{*cut*}
+
+lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
+by (simp add: expand_fun_eq cut_def)
+
+lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
+by (simp add: cut_def)
+
+text{*Inductive characterization of wfrec combinator; for details see:
+John Harrison, "Inductive definitions: automation and application"*}
+
+lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
+apply (simp add: adm_wf_def)
+apply (erule_tac a=x in wf_induct)
+apply (rule ex1I)
+apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
+apply (fast dest!: theI')
+apply (erule wfrec_rel.cases, simp)
+apply (erule allE, erule allE, erule allE, erule mp)
+apply (fast intro: the_equality [symmetric])
+done
+
+lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
+apply (simp add: adm_wf_def)
+apply (intro strip)
+apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
+apply (rule refl)
+done
+
+lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
+apply (simp add: wfrec_def)
+apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
+apply (rule wfrec_rel.wfrecI)
+apply (intro strip)
+apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
+done
+
+
text{** This form avoids giant explosions in proofs. NOTE USE OF ==*}
lemma def_wfrec: "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"
apply auto
--- a/src/HOL/Relation.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Relation.thy Tue Sep 01 14:13:34 2009 +0200
@@ -599,6 +599,9 @@
apply blast
done
+lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
+ by (auto simp:inv_image_def)
+
subsection {* Finiteness *}
--- a/src/HOL/SEQ.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/SEQ.thy Tue Sep 01 14:13:34 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/SET-Protocol/Cardholder_Registration.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Tue Sep 01 14:13:34 2009 +0200
@@ -715,6 +715,7 @@
==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
text{*The @{text "(no_asm)"} attribute is essential, since it retains
the quantifier and allows the simprule's condition to itself be simplified.*}
lemma Nonce_compromise [rule_format (no_asm)]:
@@ -741,12 +742,11 @@
apply blast --{*3*}
apply blast --{*5*}
txt{*Message 6*}
-apply (force del: allE ballE impCE simp add: symKey_compromise)
+apply (metis symKey_compromise)
--{*cardSK compromised*}
txt{*Simplify again--necessary because the previous simplification introduces
- some logical connectives*}
-apply (force del: allE ballE impCE
- simp del: image_insert image_Un imp_disjL
+ some logical connectives*}
+apply (force simp del: image_insert image_Un imp_disjL
simp add: analz_image_keys_simps symKey_compromise)
done
--- a/src/HOL/SET-Protocol/Purchase.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/SET-Protocol/Purchase.thy Tue Sep 01 14:13:34 2009 +0200
@@ -1040,9 +1040,8 @@
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
apply simp_all
apply blast
-apply (force dest!: signed_Hash_imp_used)
-apply (clarify) --{*speeds next step*}
-apply (blast dest: unique_LID_M)
+apply (metis subsetD insert_subset parts.Fst parts_increasing signed_Hash_imp_used)
+apply (metis unique_LID_M)
apply (blast dest!: Notes_Cardholder_self_False)
done
--- a/src/HOL/Set.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Set.thy Tue Sep 01 14:13:34 2009 +0200
@@ -1268,10 +1268,26 @@
"(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
by auto
+lemma Int_insert_left_if0[simp]:
+ "a \<notin> C \<Longrightarrow> (insert a B) Int C = B \<inter> C"
+ by auto
+
+lemma Int_insert_left_if1[simp]:
+ "a \<in> C \<Longrightarrow> (insert a B) Int C = insert a (B Int C)"
+ by auto
+
lemma Int_insert_right:
"A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
by auto
+lemma Int_insert_right_if0[simp]:
+ "a \<notin> A \<Longrightarrow> A Int (insert a B) = A Int B"
+ by auto
+
+lemma Int_insert_right_if1[simp]:
+ "a \<in> A \<Longrightarrow> A Int (insert a B) = insert a (A Int B)"
+ by auto
+
lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
by blast
--- a/src/HOL/SetInterval.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/SetInterval.thy Tue Sep 01 14:13:34 2009 +0200
@@ -181,33 +181,108 @@
"(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 and singletons *}
+subsubsection{* Emptyness, singletons, subset *}
context order
begin
-lemma atLeastAtMost_empty [simp]: "n < m ==> {m..n} = {}";
-by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
+lemma atLeastatMost_empty[simp]:
+ "b < a \<Longrightarrow> {a..b} = {}"
+by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
+
+lemma atLeastatMost_empty_iff[simp]:
+ "{a..b} = {} \<longleftrightarrow> (~ a <= b)"
+by auto (blast intro: order_trans)
+
+lemma atLeastatMost_empty_iff2[simp]:
+ "{} = {a..b} \<longleftrightarrow> (~ a <= b)"
+by auto (blast intro: order_trans)
+
+lemma atLeastLessThan_empty[simp]:
+ "b <= a \<Longrightarrow> {a..<b} = {}"
+by(auto simp: atLeastLessThan_def)
-lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n} = {}"
-by (auto simp add: atLeastLessThan_def)
+lemma atLeastLessThan_empty_iff[simp]:
+ "{a..<b} = {} \<longleftrightarrow> (~ a < b)"
+by auto (blast intro: le_less_trans)
+
+lemma atLeastLessThan_empty_iff2[simp]:
+ "{} = {a..<b} \<longleftrightarrow> (~ a < b)"
+by auto (blast intro: le_less_trans)
-lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}"
+lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}"
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
+lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l"
+by auto (blast intro: less_le_trans)
+
+lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l"
+by auto (blast intro: less_le_trans)
+
lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
+lemma atLeastatMost_subset_iff[simp]:
+ "{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d"
+unfolding atLeastAtMost_def atLeast_def atMost_def
+by (blast intro: order_trans)
+
+lemma atLeastatMost_psubset_iff:
+ "{a..b} < {c..d} \<longleftrightarrow>
+ ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"
+by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
+
end
+lemma (in linorder) atLeastLessThan_subset_iff:
+ "{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d"
+apply (auto simp:subset_eq Ball_def)
+apply(frule_tac x=a in spec)
+apply(erule_tac x=d in allE)
+apply (simp add: less_imp_le)
+done
+
+subsubsection {* Intersection *}
+
+context linorder
+begin
+
+lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}"
+by auto
+
+lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}"
+by auto
+
+lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}"
+by auto
+
+lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}"
+by auto
+
+lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}"
+by auto
+
+lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}"
+by auto
+
+lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}"
+by auto
+
+lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}"
+by auto
+
+end
+
+
subsection {* Intervals of natural numbers *}
subsubsection {* The Constant @{term lessThan} *}
@@ -662,17 +737,6 @@
subsubsection {* Disjoint Intersections *}
-text {* Singletons and open intervals *}
-
-lemma ivl_disj_int_singleton:
- "{l::'a::order} Int {l<..} = {}"
- "{..<u} Int {u} = {}"
- "{l} Int {l<..<u} = {}"
- "{l<..<u} Int {u} = {}"
- "{l} Int {l<..u} = {}"
- "{l..<u} Int {u} = {}"
- by simp+
-
text {* One- and two-sided intervals *}
lemma ivl_disj_int_one:
@@ -699,7 +763,7 @@
"{l..m} Int {m<..u} = {}"
by auto
-lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
+lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two
subsubsection {* Some Differences *}
--- a/src/HOL/Statespace/state_space.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Statespace/state_space.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP Tue Sep 01 14:13:34 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/ATP_Manager/atp_manager.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Sep 01 14:13:34 2009 +0200
@@ -24,7 +24,7 @@
type prover = int -> (thm * (string * int)) list option ->
(thm * (string * int)) list option -> string -> int ->
Proof.context * (thm list * thm) ->
- bool * string * string * string vector * (thm * (string * int)) list
+ bool * (string * string list) * string * string vector * (thm * (string * int)) list
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
val get_prover: string -> theory -> prover option
@@ -305,7 +305,7 @@
type prover = int -> (thm * (string * int)) list option ->
(thm * (string * int)) list option -> string -> int ->
Proof.context * (thm list * thm) ->
- bool * string * string * string vector * (thm * (string * int)) list
+ bool * (string * string list) * string * string vector * (thm * (string * int)) list
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
@@ -345,7 +345,7 @@
let
val _ = register birthtime deadtime (Thread.self (), desc)
val result =
- let val (success, message, _, _, _) =
+ let val (success, (message, _), _, _, _) =
prover (get_timeout ()) NONE NONE name i (Proof.get_goal proof_state)
in (success, message) end
handle ResHolClause.TOO_TRIVIAL
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Sep 01 14:13:34 2009 +0200
@@ -41,6 +41,12 @@
(* basic template *)
+fun with_path cleanup after f path =
+ Exn.capture f path
+ |> tap (fn _ => cleanup path)
+ |> Exn.release
+ |> tap (after path)
+
fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
timeout axiom_clauses filtered_clauses name subgoalno goal =
let
@@ -73,26 +79,29 @@
preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
(* write out problem file and call prover *)
- val probfile = prob_pathname subgoalno
- val conj_pos = writer probfile clauses
- val (proof, rc) = system_out (
- if File.exists cmd then
- space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
- else error ("Bad executable: " ^ Path.implode cmd))
+ fun cmd_line probfile = space_implode " " ["exec", File.shell_path cmd,
+ args, File.platform_path probfile]
+ fun run_on probfile =
+ if File.exists cmd
+ then writer probfile clauses |> pair (system_out (cmd_line probfile))
+ else error ("Bad executable: " ^ Path.implode cmd)
(* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
- val _ =
- if destdir' = "" then File.rm probfile
+ fun cleanup probfile = if destdir' = "" then File.rm probfile else ()
+ fun export probfile ((proof, _), _) = if destdir' = "" then ()
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
+ val ((proof, rc), conj_pos) = with_path cleanup export run_on
+ (prob_pathname subgoalno)
+
(* check for success and print out some information on failure *)
val failure = find_failure proof
val success = rc = 0 andalso is_none failure
val message =
- if is_some failure then "External prover failed."
- else if rc <> 0 then "External prover failed: " ^ proof
- else "Try this command: " ^
- produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
+ if is_some failure then ("External prover failed.", [])
+ else if rc <> 0 then ("External prover failed: " ^ proof, [])
+ else apfst (fn s => "Try this command: " ^ s)
+ (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno))
val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
in (success, message, proof, thm_names, the_filtered_clauses) end;
--- a/src/HOL/Tools/Function/fundef_core.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML Tue Sep 01 14:13:34 2009 +0200
@@ -577,8 +577,6 @@
val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
-fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt);
-
fun mk_partial_induct_rule thy globals R complete_thm clauses =
let
val Globals {domT, x, z, a, P, D, ...} = globals
@@ -614,7 +612,7 @@
val case_hyp_conv = K (case_hyp RS eq_reflection)
local open Conv in
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
- val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
+ val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
end
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Tue Sep 01 14:13:34 2009 +0200
@@ -7,14 +7,14 @@
type action
val register : string * action -> theory -> theory
+ val logfile : string Config.T
val timeout : int Config.T
- val verbose : bool Config.T
val start_line : int Config.T
val end_line : int Config.T
- val set_logfile : string -> theory -> theory
val goal_thm_of : Proof.state -> thm
- val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
+ val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
+ Proof.state -> bool
val theorems_in_proof_term : Thm.thm -> Thm.thm list
val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
val get_setting : (string * string) list -> string * string -> string
@@ -38,7 +38,8 @@
(* Mirabelle core *)
-type action = {pre: Proof.state, post: Toplevel.state option} -> string option
+type action = Time.time -> {pre: Proof.state, post: Toplevel.state option} ->
+ string option
structure Actions = TheoryDataFun
(
@@ -53,15 +54,10 @@
val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
-val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true
-val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
-val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
+val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
+val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
-val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5
-
-fun set_logfile name =
- let val _ = File.write (Path.explode name) "" (* erase file content *)
- in Config.put_thy logfile name end
+val setup = setup1 #> setup2 #> setup3 #> setup4
local
@@ -71,17 +67,15 @@
(* FIXME: with multithreading and parallel proofs enabled, we might need to
encapsulate this inside a critical section *)
-fun verbose_msg verbose msg = if verbose then SOME msg else NONE
-
-fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x
- handle TimeLimit.TimeOut => verbose_msg verb "time out"
- | ERROR msg => verbose_msg verb ("error: " ^ msg)
+fun capture_exns f x =
+ let
+ fun f' x = f x
+ handle TimeLimit.TimeOut => SOME "time out"
+ | ERROR msg => SOME ("error: " ^ msg)
+ in (case try f' x of NONE => SOME "exception" | SOME msg => msg) end
-fun capture_exns verb f x =
- (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
-
-fun apply_action (c as (verb, _)) st (name, action) =
- Option.map (pair name) (capture_exns verb (with_time_limit c action) st)
+fun apply_action timeout st (name, action) =
+ Option.map (pair name) (capture_exns (action timeout) st)
fun in_range _ _ NONE = true
| in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
@@ -90,15 +84,11 @@
let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
in if in_range l r (Position.line_of pos) then f x else [] end
-fun pretty_print verbose pos name msgs =
+fun pretty_print pos name msgs =
let
- val file = the_default "unknown file" (Position.file_of pos)
-
val str0 = string_of_int o the_default 0
val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
-
- val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc
- val head = full_loc ^ " (" ^ name ^ "):"
+ val head = "at " ^ loc ^ " (" ^ name ^ "):"
fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
in
@@ -112,22 +102,23 @@
val thy = Proof.theory_of pre
val pos = Toplevel.pos_of tr
val name = Toplevel.name_of tr
- val verb = Config.get_thy thy verbose
- val secs = Time.fromSeconds (Config.get_thy thy timeout)
+ val timeout = Time.fromSeconds (Config.get_thy thy timeout)
val st = {pre=pre, post=post}
in
Actions.get thy
|> Symtab.dest
- |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
- |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
+ |> only_within_range thy pos (map_filter (apply_action timeout st))
+ |> (fn [] => () | msgs => log thy (pretty_print pos name msgs))
end
end
+val blacklist = ["disable_pr", "enable_pr", "done", "."]
+
fun step_hook tr pre post =
(* FIXME: might require wrapping into "interruptible" *)
if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
- not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
+ not (member (op =) blacklist (Toplevel.name_of tr))
then basic_hook tr (Toplevel.proof_of pre) (SOME post)
else () (* FIXME: add theory_hook here *)
@@ -137,10 +128,12 @@
val goal_thm_of = snd o snd o Proof.get_goal
-fun can_apply tac st =
- let val (ctxt, (facts, goal)) = Proof.get_goal st
+fun can_apply timeout tac st =
+ let
+ val (ctxt, (facts, goal)) = Proof.get_goal st
+ val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
in
- (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of
+ (case TimeLimit.timeLimit timeout (Seq.pull o full_tac) goal of
SOME (thm, _) => true
| NONE => false)
end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Tue Sep 01 14:13:34 2009 +0200
@@ -5,8 +5,8 @@
structure Mirabelle_Arith : MIRABELLE_ACTION =
struct
-fun arith_action {pre=st, ...} =
- if Mirabelle.can_apply Arith_Data.arith_tac st
+fun arith_action timeout {pre=st, ...} =
+ if Mirabelle.can_apply timeout Arith_Data.arith_tac st
then SOME "succeeded"
else NONE
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Tue Sep 01 14:13:34 2009 +0200
@@ -5,7 +5,7 @@
structure Mirabelle_Metis : MIRABELLE_ACTION =
struct
-fun metis_action {pre, post} =
+fun metis_action timeout {pre, post} =
let
val thms = Mirabelle.theorems_of_sucessful_proof post
val names = map Thm.get_name thms
@@ -14,7 +14,7 @@
fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
in
- (if Mirabelle.can_apply metis pre then "succeeded" else "failed")
+ (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
|> suffix (" (" ^ commas names ^ ")")
|> SOME
end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML Tue Sep 01 14:13:34 2009 +0200
@@ -5,11 +5,12 @@
structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
struct
-fun quickcheck_action args {pre=st, ...} =
+fun quickcheck_action limit args {pre=st, ...} =
let
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
+ val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
in
- (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of
+ (case TimeLimit.timeLimit limit quickcheck st of
NONE => SOME "no counterexample"
| SOME _ => SOME "counterexample found")
end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Tue Sep 01 14:13:34 2009 +0200
@@ -7,13 +7,14 @@
(* FIXME:
-fun refute_action args {pre=st, ...} =
+fun refute_action args timeout {pre=st, ...} =
let
val subgoal = 0
val thy = Proof.theory_of st
val thm = goal_thm_of st
- val _ = Refute.refute_subgoal thy args thm subgoal
+ val refute = Refute.refute_subgoal thy args thm
+ val _ = TimeLimit.timeLimit timeout refute subgoal
in
val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 01 14:13:34 2009 +0200
@@ -5,27 +5,77 @@
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
struct
-fun sledgehammer_action {pre=st, ...} =
+fun thms_of_name ctxt name =
+ let
+ val lex = OuterKeyword.get_lexicons
+ val get = maps (ProofContext.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source {do_recover=false}
+ |> OuterLex.source {do_recover=SOME false} lex Position.start
+ |> OuterLex.source_proper
+ |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
+fun safe init done f x =
let
- val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
+ val y = init x
+ val z = Exn.capture f y
+ val _ = done y
+ in Exn.release z end
+
+val proverK = "prover"
+val keepK = "keep"
+val metisK = "metis"
+
+fun sledgehammer_action args timeout {pre=st, ...} =
+ let
+ val prover_name =
+ AList.lookup (op =) args proverK
+ |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
+
val thy = Proof.theory_of st
val prover = the (AtpManager.get_prover prover_name thy)
- val timeout = AtpManager.get_timeout ()
+ val atp_timeout = AtpManager.get_timeout ()
- val (success, message) =
+ (* run sledgehammer *)
+ fun init NONE = !AtpWrapper.destdir
+ | init (SOME path) =
+ let
+ (* Warning: we implicitly assume single-threaded execution here! *)
+ val old = !AtpWrapper.destdir
+ val _ = AtpWrapper.destdir := path
+ in old end
+ fun done path = AtpWrapper.destdir := path
+ fun sh _ =
let
- val (success, message, _, _, _) =
- prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
- in (success, message) end
- handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
- | ERROR msg => (false, "error: " ^ msg)
+ val atp = prover atp_timeout NONE NONE prover_name 1
+ val (success, (message, thm_names), _, _, _) =
+ TimeLimit.timeLimit timeout atp (Proof.get_goal st)
+ in (success, message, SOME thm_names) end
+ handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
+ | ERROR msg => (false, "error: " ^ msg, NONE)
+ val (success, message, thm_names) = safe init done sh
+ (AList.lookup (op =) args keepK)
+
+ (* try metis *)
+ fun get_thms ctxt = maps (thms_of_name ctxt)
+ fun metis thms ctxt = MetisTools.metis_tac ctxt thms
+ fun apply_metis thms = "\nApplying metis with these theorems: " ^
+ (if Mirabelle.can_apply timeout (metis thms) st
+ then "success"
+ else "failure")
+ val msg = if not (AList.defined (op =) args metisK) then ""
+ else (apply_metis (get_thms (Proof.context_of st) (these thm_names))
+ handle ERROR m => "\nException: " ^ m)
in
if success
- then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
+ then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)
else NONE
end
-fun invoke _ = Mirabelle.register ("sledgehammer", sledgehammer_action)
+fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/doc/options.txt Tue Sep 01 14:13:34 2009 +0200
@@ -0,0 +1,6 @@
+Options for sledgehammer:
+
+ * prover=NAME: name of the external prover to call
+ * keep=PATH: path where to keep temporary files created by sledgehammer
+ * metis=X: apply metis with the theorems found by sledgehammer (X may be any
+ non-empty string)
--- a/src/HOL/Tools/Mirabelle/etc/settings Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/etc/settings Tue Sep 01 14:13:34 2009 +0200
@@ -4,6 +4,5 @@
MIRABELLE_THEORY=Main
MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
MIRABELLE_TIMEOUT=30
-MIRABELLE_VERBOSE=false
ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Tue Sep 01 14:13:34 2009 +0200
@@ -7,15 +7,17 @@
PRG="$(basename "$0")"
-function action_names() {
+function print_action_names() {
TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
- ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_\(.*\)\.ML/\1/'`
+ for NAME in $TOOLS
+ do
+ echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/ \1/'
+ done
}
function usage() {
out="$MIRABELLE_OUTPUT_PATH"
timeout="$MIRABELLE_TIMEOUT"
- action_names
echo
echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
echo
@@ -23,7 +25,6 @@
echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)"
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
echo " -O DIR output directory for test data (default $out)"
- echo " -v be verbose"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
echo
echo " Apply the given actions (i.e., automated proof tools)"
@@ -31,14 +32,11 @@
echo
echo " ACTIONS is a colon-separated list of actions, where each action is"
echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
- for NAME in $ACTION_NAMES
- do
- echo " $NAME"
- done
+ print_action_names
echo
- echo " FILES is a space-separated list of theory files, where each file is"
- echo " either NAME.thy or NAME.thy[START:END] and START and END are numbers"
- echo " indicating the range the given actions are to be applied."
+ echo " FILES is a list of theory files, where each file is either NAME.thy"
+ echo " or NAME.thy[START:END] and START and END are numbers indicating the"
+ echo " range the given actions are to be applied."
echo
exit 1
}
@@ -48,7 +46,7 @@
# options
-while getopts "L:T:O:vt:" OPT
+while getopts "L:T:O:t:?" OPT
do
case "$OPT" in
L)
@@ -60,9 +58,6 @@
O)
MIRABELLE_OUTPUT_PATH="$OPTARG"
;;
- v)
- MIRABELLE_VERBOSE=true
- ;;
t)
MIRABELLE_TIMEOUT="$OPTARG"
;;
@@ -81,13 +76,13 @@
# setup
-mkdir -p $MIRABELLE_OUTPUT_PATH
+mkdir -p "$MIRABELLE_OUTPUT_PATH"
## main
for FILE in "$@"
do
- perl -w $MIRABELLE_HOME/lib/scripts/mirabelle.pl $ACTIONS "$FILE"
+ perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
done
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Tue Sep 01 14:13:34 2009 +0200
@@ -13,7 +13,6 @@
my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
-my $verbose = $ENV{'MIRABELLE_VERBOSE'};
my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
@@ -26,10 +25,10 @@
my $thy_file = $ARGV[1];
my $start_line = "0";
my $end_line = "~1";
-if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { # FIXME
- my $thy_file = $1;
- my $start_line = $2;
- my $end_line = $3;
+if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
+ $thy_file = $1;
+ $start_line = $2;
+ $end_line = $3;
}
my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
my $new_thy_name = $thy_name . "_Mirabelle";
@@ -43,9 +42,11 @@
my $log_file = $output_path . "/" . $thy_name . ".log";
my @action_files;
+my @action_names;
foreach (split(/:/, $actions)) {
if (m/([^[]*)/) {
push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
+ push @action_names, $1;
}
}
my $tools = "";
@@ -62,9 +63,8 @@
begin
setup {*
- Mirabelle.set_logfile "$log_file" #>
+ Config.put_thy Mirabelle.logfile "$log_file" #>
Config.put_thy Mirabelle.timeout $timeout #>
- Config.put_thy Mirabelle.verbose $verbose #>
Config.put_thy Mirabelle.start_line $start_line #>
Config.put_thy Mirabelle.end_line $end_line
*}
@@ -99,7 +99,8 @@
my $thy_text = join("", @lines);
my $old_len = length($thy_text);
-$thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$setup_thy_name" /gm;
+$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
+$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g;
die "No 'imports' found" if length($thy_text) == $old_len;
open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
@@ -114,14 +115,21 @@
# run isabelle
-my $r = system "$isabelle_home/bin/isabelle-process " .
+open(LOG_FILE, ">$log_file");
+print LOG_FILE "Run of $new_thy_file with:\n";
+foreach $name (@action_names) {
+ print LOG_FILE " $name\n";
+}
+print LOG_FILE "\n\n";
+close(LOG_FILE);
+
+my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
"-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
# cleanup
unlink $root_file;
-unlink $new_thy_file;
unlink $setup_file;
exit $r;
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Sep 01 14:13:34 2009 +0200
@@ -29,30 +29,30 @@
val bT = HOLogic.boolT;
val dest_numeral = HOLogic.dest_number #> snd;
-val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
+val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
-val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
+val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
-val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
+val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
-val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
+val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
asetgt, asetge, asetdvd, asetndvd,asetP],
- [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
+ [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]] = [@{thms "aset"}, @{thms "bset"}];
-val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"},
+val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"},
@{thm "plusinfinity"}, @{thm "cppi"}];
val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
-val [zdvd_mono,simp_from_to,all_not_ex] =
+val [zdvd_mono,simp_from_to,all_not_ex] =
[@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
@@ -62,49 +62,49 @@
(* recognising cterm without moving to terms *)
-datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm
+datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm
| Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm
| Dvd of cterm*cterm | NDvd of cterm*cterm | Nox
-fun whatis x ct =
-( case (term_of ct) of
+fun whatis x ct =
+( case (term_of ct) of
Const("op &",_)$_$_ => And (Thm.dest_binop ct)
| Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
| Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
-| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
+| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
| Const (@{const_name HOL.less}, _) $ y$ z =>
- if term_of x aconv y then Lt (Thm.dest_arg ct)
+ if term_of x aconv y then Lt (Thm.dest_arg ct)
else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name HOL.less_eq}, _) $ y $ z =>
- if term_of x aconv y then Le (Thm.dest_arg ct)
+| Const (@{const_name HOL.less_eq}, _) $ y $ z =>
+ if term_of x aconv y then Le (Thm.dest_arg ct)
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
- if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
+ if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
- if term_of x aconv y then
- NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
+ if term_of x aconv y then
+ NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
| _ => Nox)
- handle CTERM _ => Nox;
+ handle CTERM _ => Nox;
-fun get_pmi_term t =
- let val (x,eq) =
+fun get_pmi_term t =
+ let val (x,eq) =
(Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
(Thm.dest_arg t)
in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
val get_pmi = get_pmi_term o cprop_of;
-val p_v' = @{cpat "?P' :: int => bool"};
+val p_v' = @{cpat "?P' :: int => bool"};
val q_v' = @{cpat "?Q' :: int => bool"};
val p_v = @{cpat "?P:: int => bool"};
val q_v = @{cpat "?Q:: int => bool"};
-fun myfwd (th1, th2, th3) p q
- [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
- let
+fun myfwd (th1, th2, th3) p q
+ [(th_1,th_2,th_3), (th_1',th_2',th_3')] =
+ let
val (mp', mq') = (get_pmi th_1, get_pmi th_1')
- val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
+ val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
[th_1, th_1']
val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
@@ -123,15 +123,15 @@
val [addC, mulC, subC, negC] = map term_of [cadd, cmulC, cminus, cneg]
val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
-val is_numeral = can dest_numeral;
+val is_numeral = can dest_numeral;
-fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
+fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
-val [minus1,plus1] =
+val [minus1,plus1] =
map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
-fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
+fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
asetgt, asetge,asetdvd,asetndvd,asetP,
infDdvd, infDndvd, asetconj,
asetdisj, infDconj, infDdisj] cp =
@@ -144,11 +144,11 @@
| Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse))
| Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue))
| Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue))
-| Dvd (d,s) =>
+| Dvd (d,s) =>
([],let val dd = dvd d
- in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)
+ in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)
| NDvd(d,s) => ([],let val dd = dvd d
- in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
+ in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
| _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP));
fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt,
@@ -165,110 +165,112 @@
| Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse))
| Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse))
| Dvd (d,s) => ([],let val dd = dvd d
- in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)
+ in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)
| NDvd (d,s) => ([],let val dd = dvd d
- in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
+ in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
| _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))
(* Canonical linear form for terms, formulae etc.. *)
-fun provelin ctxt t = Goal.prove ctxt [] [] t
+fun provelin ctxt t = Goal.prove ctxt [] [] t
(fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
-fun linear_cmul 0 tm = zero
- | linear_cmul n tm = case tm of
+fun linear_cmul 0 tm = zero
+ | linear_cmul n tm = case tm of
Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
| Const (@{const_name HOL.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
| Const (@{const_name HOL.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
| (m as Const (@{const_name HOL.uminus}, _)) $ a => m $ linear_cmul n a
| _ => numeral1 (fn m => n * m) tm;
-fun earlier [] x y = false
- | earlier (h::t) x y =
- if h aconv y then false else if h aconv x then true else earlier t x y;
+fun earlier [] x y = false
+ | earlier (h::t) x y =
+ if h aconv y then false else if h aconv x then true else earlier t x y;
-fun linear_add vars tm1 tm2 = case (tm1, tm2) of
+fun linear_add vars tm1 tm2 = case (tm1, tm2) of
(Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1,
Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
- if x1 = x2 then
+ if x1 = x2 then
let val c = numeral2 (curry op +) c1 c2
in if c = zero then linear_add vars r1 r2
else addC$(mulC$c$x1)$(linear_add vars r1 r2)
- end
+ end
else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
| (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, _) =>
addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
- | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
+ | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
| (_, _) => numeral2 (curry op +) tm1 tm2;
-
-fun linear_neg tm = linear_cmul ~1 tm;
-fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
+
+fun linear_neg tm = linear_cmul ~1 tm;
+fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
-fun lint vars tm = if is_numeral tm then tm else case tm of
+fun lint vars tm = if is_numeral tm then tm else case tm of
Const (@{const_name HOL.uminus}, _) $ t => linear_neg (lint vars t)
| Const (@{const_name HOL.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
| Const (@{const_name HOL.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
| Const (@{const_name HOL.times}, _) $ s $ t =>
- let val s' = lint vars s
- val t' = lint vars t
- in if is_numeral s' then (linear_cmul (dest_numeral s') t')
- else if is_numeral t' then (linear_cmul (dest_numeral t') s')
+ let val s' = lint vars s
+ val t' = lint vars t
+ in if is_numeral s' then (linear_cmul (dest_numeral s') t')
+ else if is_numeral t' then (linear_cmul (dest_numeral t') s')
else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm]))
- end
+ end
| _ => addC $ (mulC $ one $ tm) $ zero;
-fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) =
+fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) =
lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s)
- | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) =
+ | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) =
lin vs (Const (@{const_name HOL.less}, T) $ t $ s)
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
- | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) =
+ | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) =
HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t)
- | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
- (case lint vs (subC$t$s) of
- (t as a$(m$c$y)$r) =>
+ | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
+ (case lint vs (subC$t$s) of
+ (t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
else b$(m$c$y)$(linear_neg r)
| t => b$zero$t)
- | lin (vs as x::_) (b$s$t) =
- (case lint vs (subC$t$s) of
- (t as a$(m$c$y)$r) =>
+ | lin (vs as x::_) (b$s$t) =
+ (case lint vs (subC$t$s) of
+ (t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
else b$(linear_neg r)$(m$c$y)
| t => b$zero$t)
| lin vs fm = fm;
-fun lint_conv ctxt vs ct =
+fun lint_conv ctxt vs ct =
let val t = term_of ct
in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop))
RS eq_reflection
end;
-fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT
- | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT
+fun is_intrel_type T = T = @{typ "int => int => bool"};
+
+fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
+ | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
| is_intrel _ = false;
-
+
fun linearize_conv ctxt vs ct = case term_of ct of
- Const(@{const_name Ring_and_Field.dvd},_)$d$t =>
- let
+ Const(@{const_name Ring_and_Field.dvd},_)$d$t =>
+ let
val th = binop_conv (lint_conv ctxt vs) ct
val (d',t') = Thm.dest_binop (Thm.rhs_of th)
val (dt',tt') = (term_of d', term_of t')
- in if is_numeral dt' andalso is_numeral tt'
+ in if is_numeral dt' andalso is_numeral tt'
then Conv.fconv_rule (arg_conv (Simplifier.rewrite presburger_ss)) th
- else
- let
- val dth =
- ((if dest_numeral (term_of d') < 0 then
+ else
+ let
+ val dth =
+ ((if dest_numeral (term_of d') < 0 then
Conv.fconv_rule (arg_conv (arg1_conv (lint_conv ctxt vs)))
(Thm.transitive th (inst' [d',t'] dvd_uminus))
else th) handle TERM _ => th)
val d'' = Thm.rhs_of dth |> Thm.dest_arg1
in
- case tt' of
- Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$_)$_ =>
+ case tt' of
+ Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$_)$_ =>
let val x = dest_numeral c
in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
(Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
@@ -277,29 +279,29 @@
end
end
| Const (@{const_name Not},_)$(Const(@{const_name Ring_and_Field.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
-| t => if is_intrel t
+| t => if is_intrel t
then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
RS eq_reflection
else reflexive ct;
val dvdc = @{cterm "op dvd :: int => _"};
-fun unify ctxt q =
+fun unify ctxt q =
let
val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
- val x = term_of cx
+ val x = term_of cx
val ins = insert (op = : int * int -> bool)
- fun h (acc,dacc) t =
+ fun h (acc,dacc) t =
case (term_of t) of
- Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
+ Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
if x aconv y andalso member (op =)
["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
- | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
+ | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
if x aconv y andalso member (op =)
- [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
+ [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
- | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) =>
+ | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) =>
if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
| Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
@@ -307,51 +309,53 @@
| _ => (acc, dacc)
val (cs,ds) = h ([],[]) p
val l = Integer.lcms (cs union ds)
- fun cv k ct =
- let val (tm as b$s$t) = term_of ct
+ fun cv k ct =
+ let val (tm as b$s$t) = term_of ct
in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
|> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
- fun nzprop x =
- let
- val th =
- Simplifier.rewrite lin_ss
- (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
- (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
+ fun nzprop x =
+ let
+ val th =
+ Simplifier.rewrite lin_ss
+ (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
+ (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
@{cterm "0::int"})))
in equal_elim (Thm.symmetric th) TrueI end;
- val notz = let val tab = fold Inttab.update
- (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
- in
- (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral))
- handle Option => (writeln "noz: Theorems-Table contains no entry for";
- Display.print_cterm ct ; raise Option)))
- end
- fun unit_conv t =
+ val notz =
+ let val tab = fold Inttab.update
+ (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
+ in
+ fn ct => valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral))
+ handle Option =>
+ (writeln ("noz: Theorems-Table contains no entry for " ^
+ Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
+ end
+ fun unit_conv t =
case (term_of t) of
Const("op &",_)$_$_ => binop_conv unit_conv t
| Const("op |",_)$_$_ => binop_conv unit_conv t
| Const (@{const_name Not},_)$_ => arg_conv unit_conv t
- | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
+ | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
- | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
+ | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
if x=y andalso member (op =)
[@{const_name HOL.less}, @{const_name HOL.less_eq}] s
then cv (l div dest_numeral c) t else Thm.reflexive t
- | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) =>
- if x=y then
- let
+ | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) =>
+ if x=y then
+ let
val k = l div dest_numeral c
val kt = HOLogic.mk_number iT k
- val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
+ val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
val (d',t') = (mulC$kt$d, mulC$kt$r)
val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))
RS eq_reflection
val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop))
RS eq_reflection
- in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end
+ in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end
else Thm.reflexive t
| _ => Thm.reflexive t
val uth = unit_conv p
@@ -359,7 +363,7 @@
val ltx = Thm.capply (Thm.capply cmulC clt) cx
val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
- val thf = transitive th
+ val thf = transitive th
(transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
||> beta_conversion true |>> Thm.symmetric
@@ -372,25 +376,25 @@
fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
val cTrp = @{cterm "Trueprop"};
val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
-val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
+val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
|> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
[asetP,bsetP];
val D_tm = @{cpat "?D::int"};
-fun cooperex_conv ctxt vs q =
-let
+fun cooperex_conv ctxt vs q =
+let
val uth = unify ctxt q
val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))
val ins = insert (op aconvc)
- fun h t (bacc,aacc,dacc) =
+ fun h t (bacc,aacc,dacc) =
case (whatis x t) of
And (p,q) => h q (h p (bacc,aacc,dacc))
| Or (p,q) => h q (h p (bacc,aacc,dacc))
- | Eq t => (ins (minus1 t) bacc,
+ | Eq t => (ins (minus1 t) bacc,
ins (plus1 t) aacc,dacc)
- | NEq t => (ins t bacc,
+ | NEq t => (ins t bacc,
ins t aacc, dacc)
| Lt t => (bacc, ins t aacc, dacc)
| Le t => (bacc, ins (plus1 t) aacc,dacc)
@@ -403,89 +407,92 @@
val d = Integer.lcms ds
val cd = Numeral.mk_cnumber @{ctyp "int"} d
val dt = term_of cd
- fun divprop x =
- let
- val th =
- Simplifier.rewrite lin_ss
- (Thm.capply @{cterm Trueprop}
+ fun divprop x =
+ let
+ val th =
+ Simplifier.rewrite lin_ss
+ (Thm.capply @{cterm Trueprop}
(Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
in equal_elim (Thm.symmetric th) TrueI end;
- val dvd = let val tab = fold Inttab.update
- (ds ~~ (map divprop ds)) Inttab.empty in
- (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral))
- handle Option => (writeln "dvd: Theorems-Table contains no entry for";
- Display.print_cterm ct ; raise Option)))
- end
- val dp =
- let val th = Simplifier.rewrite lin_ss
- (Thm.capply @{cterm Trueprop}
+ val dvd =
+ let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
+ fn ct => valOf (Inttab.lookup tab (term_of ct |> dest_numeral))
+ handle Option =>
+ (writeln ("dvd: Theorems-Table contains no entry for" ^
+ Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
+ end
+ val dp =
+ let val th = Simplifier.rewrite lin_ss
+ (Thm.capply @{cterm Trueprop}
(Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
in equal_elim (Thm.symmetric th) TrueI end;
(* A and B set *)
- local
+ local
val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
in
- fun provein x S =
+ fun provein x S =
case term_of S of
Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
- | Const(@{const_name insert}, _) $ y $ _ =>
+ | Const(@{const_name insert}, _) $ y $ _ =>
let val (cy,S') = Thm.dest_binop S
in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
- else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
+ else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
(provein x S')
end
end
-
+
val al = map (lint vs o term_of) a0
val bl = map (lint vs o term_of) b0
- val (sl,s0,f,abths,cpth) =
- if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
- then
+ val (sl,s0,f,abths,cpth) =
+ if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
+ then
(bl,b0,decomp_minf,
- fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
+ fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
- (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
+ (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
[bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
bsetdisj,infDconj, infDdisj]),
- cpmi)
- else (al,a0,decomp_pinf,fn A =>
+ cpmi)
+ else (al,a0,decomp_pinf,fn A =>
(map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
- (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
+ (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
[asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
asetdisj,infDconj, infDdisj]),cppi)
- val cpth =
+ val cpth =
let
- val sths = map (fn (tl,t0) =>
- if tl = term_of t0
+ val sths = map (fn (tl,t0) =>
+ if tl = term_of t0
then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
- else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)
- |> HOLogic.mk_Trueprop))
+ else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)
+ |> HOLogic.mk_Trueprop))
(sl ~~ s0)
val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths)
val S = mkISet csl
- val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab)
+ val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab)
csl Termtab.empty
val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
- val inS =
- let
- fun transmem th0 th1 =
- Thm.equal_elim
- (Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule
+ val inS =
+ let
+ fun transmem th0 th1 =
+ Thm.equal_elim
+ (Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule
((Thm.dest_fun o Thm.dest_fun o Thm.dest_arg o cprop_of) th1) th0) S)) th1
val tab = fold Termtab.update
- (map (fn eq =>
- let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
- val th = if term_of s = term_of t
+ (map (fn eq =>
+ let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
+ val th = if term_of s = term_of t
then valOf(Termtab.lookup inStab (term_of s))
- else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
+ else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
[eq, valOf(Termtab.lookup inStab (term_of s))]
in (term_of t, th) end)
sths) Termtab.empty
- in fn ct =>
- (valOf (Termtab.lookup tab (term_of ct))
- handle Option => (writeln "inS: No theorem for " ; Display.print_cterm ct ; raise Option))
+ in
+ fn ct => valOf (Termtab.lookup tab (term_of ct))
+ handle Option =>
+ (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
+ raise Option)
end
val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
in [dp, inf, nb, pd] MRS cpth
@@ -494,9 +501,9 @@
in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth'))
end;
-fun literals_conv bops uops env cv =
+fun literals_conv bops uops env cv =
let fun h t =
- case (term_of t) of
+ case (term_of t) of
b$_$_ => if member (op aconv) bops b then binop_conv h t else cv env t
| u$_ => if member (op aconv) uops u then arg_conv h t else cv env t
| _ => cv env t
@@ -506,21 +513,21 @@
nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
local
- val pcv = Simplifier.rewrite
- (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4))
+ val pcv = Simplifier.rewrite
+ (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4))
@ [not_all,all_not_ex, ex_disj_distrib]))
val postcv = Simplifier.rewrite presburger_ss
- fun conv ctxt p =
+ fun conv ctxt p =
let val _ = ()
in
- Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
- (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
- (cooperex_conv ctxt) p
+ Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
+ (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
+ (cooperex_conv ctxt) p
end
handle CTERM s => raise COOPER ("Cooper Failed", CTERM s)
- | THM s => raise COOPER ("Cooper Failed", THM s)
- | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
-in val cooper_conv = conv
+ | THM s => raise COOPER ("Cooper Failed", THM s)
+ | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
+in val cooper_conv = conv
end;
end;
@@ -542,12 +549,12 @@
| Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
| Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
| Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name HOL.times},_)$t1$t2 =>
+ | Const(@{const_name HOL.times},_)$t1$t2 =>
(Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
- handle TERM _ =>
+ handle TERM _ =>
(Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
- | _ => (C (HOLogic.dest_number t |> snd)
+ | _ => (C (HOLogic.dest_number t |> snd)
handle TERM _ => cooper "Reification: unknown term");
fun qf_of_term ps vs t = case t
@@ -555,7 +562,7 @@
| Const("False",_) => F
| Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
| Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 =>
+ | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 =>
(Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd") (* FIXME avoid handle _ *)
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
| @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
@@ -563,42 +570,42 @@
| Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
| Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
| Const (@{const_name Not},_)$t' => Not(qf_of_term ps vs t')
- | Const("Ex",_)$Abs(xn,xT,p) =>
+ | Const("Ex",_)$Abs(xn,xT,p) =>
let val (xn',p') = variant_abs (xn,xT,p)
val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
in E (qf_of_term ps vs' p')
end
- | Const("All",_)$Abs(xn,xT,p) =>
+ | Const("All",_)$Abs(xn,xT,p) =>
let val (xn',p') = variant_abs (xn,xT,p)
val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
in A (qf_of_term ps vs' p')
end
- | _ =>(case AList.lookup (op aconv) ps t of
+ | _ =>(case AList.lookup (op aconv) ps t of
NONE => cooper "Reification: unknown term!"
| SOME n => Closed n);
local
val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
- @{term "op = :: int => _"}, @{term "op < :: int => _"},
- @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
+ @{term "op = :: int => _"}, @{term "op < :: int => _"},
+ @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
@{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
fun ty t = Bool.not (fastype_of t = HOLogic.boolT)
in
fun term_bools acc t =
-case t of
- (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b
+case t of
+ (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b
else insert (op aconv) t acc
- | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a
+ | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a
else insert (op aconv) t acc
| Abs p => term_bools acc (snd (variant_abs p))
| _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
end;
-
+
fun myassoc2 l v =
case l of
- [] => NONE
+ [] => NONE
| (x,v')::xs => if v = v' then SOME x
- else myassoc2 xs v;
+ else myassoc2 xs v;
fun term_of_i vs t = case t
of C i => HOLogic.mk_number HOLogic.intT i
@@ -610,9 +617,9 @@
HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
| Cn (n, i, t') => term_of_i vs (Add (Mul (i, Bound n), t'));
-fun term_of_qf ps vs t =
- case t of
- T => HOLogic.true_const
+fun term_of_qf ps vs t =
+ case t of
+ T => HOLogic.true_const
| F => HOLogic.false_const
| Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
| Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
@@ -620,7 +627,7 @@
| Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
| Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
| NEq t' => term_of_qf ps vs (Not (Eq t'))
- | Dvd(i,t') => @{term "op dvd :: int => _ "} $
+ | Dvd(i,t') => @{term "op dvd :: int => _ "} $
HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
| NDvd(i,t')=> term_of_qf ps vs (Not(Dvd(i,t')))
| Not t' => HOLogic.Not$(term_of_qf ps vs t')
--- a/src/HOL/Tools/TFL/rules.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Sep 01 14:13:34 2009 +0200
@@ -456,7 +456,7 @@
fun is_cong thm =
case (Thm.prop_of thm)
of (Const("==>",_)$(Const("Trueprop",_)$ _) $
- (Const("==",_) $ (Const (@{const_name "Wellfounded.cut"},_) $ f $ R $ a $ x) $ _)) => false
+ (Const("==",_) $ (Const (@{const_name "Recdef.cut"},_) $ f $ R $ a $ x) $ _)) => false
| _ => true;
@@ -544,7 +544,7 @@
(*---------------------------------------------------------------------------
* Trace information for the rewriter
*---------------------------------------------------------------------------*)
-val term_ref = ref[] : term list ref
+val term_ref = ref [] : term list ref
val ss_ref = ref [] : simpset list ref;
val thm_ref = ref [] : thm list ref;
val tracing = ref false;
@@ -554,8 +554,8 @@
fun print_thms s L =
say (cat_lines (s :: map Display.string_of_thm_without_context L));
-fun print_cterms s L =
- say (cat_lines (s :: map Display.string_of_cterm L));
+fun print_cterm s ct =
+ say (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)]);
(*---------------------------------------------------------------------------
@@ -659,7 +659,7 @@
end;
fun restricted t = isSome (S.find_term
- (fn (Const(@{const_name "Wellfounded.cut"},_)) =>true | _ => false)
+ (fn (Const(@{const_name "Recdef.cut"},_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
@@ -683,7 +683,7 @@
(* Unquantified eliminate *)
fun uq_eliminate (thm,imp,thy) =
let val tych = cterm_of thy
- val dummy = print_cterms "To eliminate:" [tych imp]
+ val dummy = print_cterm "To eliminate:" (tych imp)
val ants = map tych (Logic.strip_imp_prems imp)
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
@@ -781,9 +781,8 @@
val antl = case rcontext of [] => []
| _ => [S.list_mk_conj(map cncl rcontext)]
val TC = genl(S.list_mk_imp(antl, A))
- val dummy = print_cterms "func:" [cterm_of thy func]
- val dummy = print_cterms "TC:"
- [cterm_of thy (HOLogic.mk_Trueprop TC)]
+ val dummy = print_cterm "func:" (cterm_of thy func)
+ val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
val dummy = tc_list := (TC :: !tc_list)
val nestedp = isSome (S.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
--- a/src/HOL/Tools/TFL/tfl.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Tue Sep 01 14:13:34 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/res_reconstruct.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Tue Sep 01 14:13:34 2009 +0200
@@ -17,10 +17,10 @@
(* extracting lemma list*)
val find_failure: string -> string option
val lemma_list: bool -> string ->
- string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
+ string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
(* structured proofs *)
val structured_proof: string ->
- string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
+ string * string vector * (int * int) * Proof.context * Thm.thm * int -> string * string list
end;
structure ResReconstruct : RES_RECONSTRUCT =
@@ -554,9 +554,10 @@
fun lemma_list dfg name result =
let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
- in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
+ in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
(if used_conj then ""
- else "\nWarning: Goal is provable because context is inconsistent.")
+ else "\nWarning: Goal is provable because context is inconsistent."),
+ nochained lemmas)
end;
(* === Extracting structured Isar-proof === *)
@@ -567,11 +568,11 @@
val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
val proofextract = get_proof_extract proof
val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
- val one_line_proof = lemma_list false name result
+ val (one_line_proof, lemma_names) = lemma_list false name result
val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
else decode_tstp_file cnfs ctxt goal subgoalno thm_names
in
- one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured
+ (one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured, lemma_names)
end
end;
--- a/src/HOL/Tools/sat_funcs.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Tue Sep 01 14:13:34 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
@@ -92,7 +92,7 @@
==> F \<in> (atMost n) LeadsTo common"
apply (rule LeadsTo_weaken_R)
apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
-apply (simp_all (no_asm_simp))
+apply (simp_all (no_asm_simp) del: Int_insert_right_if1)
apply (rule_tac [2] subset_refl)
apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
done
--- a/src/HOL/Wellfounded.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Wellfounded.thy Tue Sep 01 14:13:34 2009 +0200
@@ -13,14 +13,6 @@
subsection {* Basic Definitions *}
-inductive
- wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
- for R :: "('a * 'a) set"
- and F :: "('a => 'b) => 'a => 'b"
-where
- wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
- wfrec_rel R F x (F g x)"
-
constdefs
wf :: "('a * 'a)set => bool"
"wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
@@ -31,16 +23,6 @@
acyclic :: "('a*'a)set => bool"
"acyclic r == !x. (x,x) ~: r^+"
- cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
- "cut f r x == (%y. if (y,x):r then f y else undefined)"
-
- adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
- "adm_wf R F == ALL f g x.
- (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
-
- wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
- [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
-
abbreviation acyclicP :: "('a => 'a => bool) => bool" where
"acyclicP r == acyclic {(x, y). r x y}"
@@ -425,54 +407,6 @@
by (blast intro: finite_acyclic_wf wf_acyclic)
-subsection{*Well-Founded Recursion*}
-
-text{*cut*}
-
-lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
-by (simp add: expand_fun_eq cut_def)
-
-lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
-by (simp add: cut_def)
-
-text{*Inductive characterization of wfrec combinator; for details see:
-John Harrison, "Inductive definitions: automation and application"*}
-
-lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
-apply (simp add: adm_wf_def)
-apply (erule_tac a=x in wf_induct)
-apply (rule ex1I)
-apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
-apply (fast dest!: theI')
-apply (erule wfrec_rel.cases, simp)
-apply (erule allE, erule allE, erule allE, erule mp)
-apply (fast intro: the_equality [symmetric])
-done
-
-lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
-apply (simp add: adm_wf_def)
-apply (intro strip)
-apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
-apply (rule refl)
-done
-
-lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
-apply (simp add: wfrec_def)
-apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
-apply (rule wfrec_rel.wfrecI)
-apply (intro strip)
-apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
-done
-
-subsection {* Code generator setup *}
-
-consts_code
- "wfrec" ("\<module>wfrec?")
-attach {*
-fun wfrec f x = f (wfrec f) x;
-*}
-
-
subsection {* @{typ nat} is well-founded *}
lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
@@ -696,9 +630,6 @@
apply blast
done
-lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
- by (auto simp:inv_image_def)
-
text {* Measure Datatypes into @{typ nat} *}
definition measure :: "('a => nat) => ('a * 'a)set"
--- a/src/HOL/Word/BinBoolList.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/Word/WordShift.thy Tue Sep 01 14:13:34 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/HOL/ex/Predicate_Compile_ex.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Sep 01 14:13:34 2009 +0200
@@ -99,4 +99,62 @@
values 20 "{(n, m). tranclp succ n m}"
*)
+subsection{* IMP *}
+
+types
+ var = nat
+ state = "int list"
+
+datatype com =
+ Skip |
+ Ass var "state => int" |
+ Seq com com |
+ IF "state => bool" com com |
+ While "state => bool" com
+
+inductive exec :: "com => state => state => bool" where
+"exec Skip s s" |
+"exec (Ass x e) s (s[x := e(s)])" |
+"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
+"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
+"~b s ==> exec (While b c) s s" |
+"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
+
+code_pred exec .
+
+values "{t. exec
+ (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
+ [3,5] t}"
+
+
+subsection{* CCS *}
+
+text{* This example formalizes finite CCS processes without communication or
+recursion. For simplicity, labels are natural numbers. *}
+
+datatype proc = nil | pre nat proc | or proc proc | par proc proc
+
+inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
+"step (pre n p) n p" |
+"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
+"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
+"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
+"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
+
+code_pred step .
+
+inductive steps where
+"steps p [] p" |
+"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
+
+code_pred steps .
+
+values 5
+ "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
+
+(* FIXME
+values 3 "{(a,q). step (par nil nil) a q}"
+*)
+
end
\ No newline at end of file
--- a/src/HOL/ex/ROOT.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/ex/ROOT.ML Tue Sep 01 14:13:34 2009 +0200
@@ -72,25 +72,16 @@
(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
"Hilbert_Classical";
-
use_thy "SVC_Oracle";
-
-fun svc_enabled () = getenv "SVC_HOME" <> "";
-fun if_svc_enabled f x = if svc_enabled () then f x else ();
-
-if_svc_enabled use_thy "svc_test";
-
+if getenv "SVC_HOME" = "" then ()
+else use_thy "svc_test";
-(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
-(* installed: *)
+(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
try use_thy "SAT_Examples";
-Future.shutdown ();
-(* requires zChaff (or some other reasonably fast SAT solver) to be *)
-(* installed: *)
-if getenv "ZCHAFF_HOME" <> "" then
- use_thy "Sudoku"
-else ();
+(*requires zChaff (or some other reasonably fast SAT solver)*)
+if getenv "ZCHAFF_HOME" = "" then ()
+else use_thy "Sudoku";
HTML.with_charset "utf-8" (no_document use_thys)
["Hebrew", "Chinese", "Serbian"];
--- a/src/HOL/ex/Termination.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/HOL/ex/Termination.thy Tue Sep 01 14:13:34 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Termination.thy
- ID: $Id$
Author: Lukas Bulwahn, TU Muenchen
Author: Alexander Krauss, TU Muenchen
*)
@@ -10,12 +9,33 @@
imports Main Multiset
begin
+subsection {* Manually giving termination relations using @{text relation} and
+@{term measure} *}
+
+function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
+by pat_completeness auto
+
+termination by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
+
+function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "foo i N = (if i > N
+ then (if N = 0 then 0 else foo 0 (N - 1))
+ else i + foo (Suc i) N)"
+by pat_completeness auto
+
+termination by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
+
+
+subsection {* @{text lexicographic_order}: Trivial examples *}
+
text {*
- The @{text fun} command uses the method @{text lexicographic_order} by default.
+ The @{text fun} command uses the method @{text lexicographic_order} by default,
+ so it is not explicitly invoked.
*}
-subsection {* Trivial examples *}
-
fun identity :: "nat \<Rightarrow> nat"
where
"identity n = n"
--- a/src/Pure/Concurrent/future.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Sep 01 14:13:34 2009 +0200
@@ -237,7 +237,7 @@
val total = length (! workers);
val active = count_active ();
in
- "SCHEDULE: " ^
+ "SCHEDULE " ^ string_of_int (Time.toMilliseconds now) ^ ": " ^
string_of_int ready ^ " ready, " ^
string_of_int pending ^ " pending, " ^
string_of_int running ^ " running; " ^
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/linear_set.scala Tue Sep 01 14:13:34 2009 +0200
@@ -0,0 +1,118 @@
+/* Title: Pure/General/linear_set.scala
+ Author: Makarius
+ Author: Fabian Immler TU Munich
+
+Sets with canonical linear order, or immutable linked-lists.
+*/
+package isabelle
+
+
+object Linear_Set
+{
+ private case class Rep[A](
+ val first_elem: Option[A], val last_elem: Option[A], val body: Map[A, A])
+
+ private def empty_rep[A] = Rep[A](None, None, Map())
+
+ private def make[A](first_elem: Option[A], last_elem: Option[A], body: Map[A, A]): Linear_Set[A] =
+ new Linear_Set[A] { override val rep = Rep(first_elem, last_elem, body) }
+
+
+ def empty[A]: Linear_Set[A] = new Linear_Set
+ def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
+
+ class Duplicate(s: String) extends Exception(s)
+ class Undefined(s: String) extends Exception(s)
+}
+
+
+class Linear_Set[A] extends scala.collection.immutable.Set[A]
+{
+ /* representation */
+
+ protected val rep = Linear_Set.empty_rep[A]
+
+
+ /* auxiliary operations */
+
+ def next(elem: A) = rep.body.get(elem)
+ def prev(elem: A) = rep.body.find(_._2 == elem).map(_._1) // slow
+
+ private def _insert_after(hook: Option[A], elem: A): Linear_Set[A] =
+ if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
+ else hook match {
+ case Some(hook) =>
+ if (!contains(hook)) throw new Linear_Set.Undefined(hook.toString)
+ else if (rep.body.isDefinedAt(hook))
+ Linear_Set.make(rep.first_elem, rep.last_elem,
+ rep.body - hook + (hook -> elem) + (elem -> rep.body(hook)))
+ else Linear_Set.make(rep.first_elem, Some(elem), rep.body + (hook -> elem))
+ case None =>
+ if (isEmpty) Linear_Set.make(Some(elem), Some(elem), Map())
+ else Linear_Set.make(Some(elem), rep.last_elem, rep.body + (elem -> rep.first_elem.get))
+ }
+
+ def insert_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+ elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
+
+ def delete_after(elem: Option[A]): Linear_Set[A] =
+ elem match {
+ case Some(elem) =>
+ if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
+ else if (!rep.body.isDefinedAt(elem)) throw new Linear_Set.Undefined(null)
+ else if (rep.body(elem) == rep.last_elem.get)
+ Linear_Set.make(rep.first_elem, Some(elem), rep.body - elem)
+ else Linear_Set.make(rep.first_elem, rep.last_elem,
+ rep.body - elem - rep.body(elem) + (elem -> rep.body(rep.body(elem))))
+ case None =>
+ if (isEmpty) throw new Linear_Set.Undefined(null)
+ else if (size == 1) empty
+ else Linear_Set.make(Some(rep.body(rep.first_elem.get)), rep.last_elem, rep.body - rep.first_elem.get)
+ }
+
+ def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] = {
+ if(!rep.first_elem.isDefined) this
+ else {
+ val next =
+ if (from == rep.last_elem) None
+ else if (from == None) rep.first_elem
+ else from.map(rep.body(_))
+ if (next == to) this
+ else delete_after(from).delete_between(from, to)
+ }
+ }
+
+
+ /* Set methods */
+
+ override def stringPrefix = "Linear_Set"
+
+ def empty[B]: Linear_Set[B] = Linear_Set.empty
+
+ override def isEmpty: Boolean = !rep.last_elem.isDefined
+ def size: Int = if (isEmpty) 0 else rep.body.size + 1
+
+ def elements = new Iterator[A] {
+ private var next_elem = rep.first_elem
+ def hasNext = next_elem.isDefined
+ def next = {
+ val elem = next_elem.get
+ next_elem = if (rep.body.isDefinedAt(elem)) Some(rep.body(elem)) else None
+ elem
+ }
+ }
+
+ def contains(elem: A): Boolean =
+ !isEmpty && (rep.last_elem.get == elem || rep.body.isDefinedAt(elem))
+
+ def + (elem: A): Linear_Set[A] = _insert_after(rep.last_elem, elem)
+
+ override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
+ this + elem1 + elem2 ++ elems
+ override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
+ override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
+
+ def - (elem: A): Linear_Set[A] =
+ if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
+ else delete_after(prev(elem))
+}
\ No newline at end of file
--- a/src/Pure/General/markup.scala Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/General/markup.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/General/position.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/General/scan.scala Tue Sep 01 14:13:34 2009 +0200
@@ -11,7 +11,6 @@
object Scan
{
-
/** Lexicon -- position tree **/
object Lexicon
--- a/src/Pure/General/yxml.scala Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/General/yxml.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/IsaMakefile Tue Sep 01 14:13:34 2009 +0200
@@ -117,15 +117,14 @@
## Scala material
-SCALA_FILES = General/event_bus.scala General/markup.scala \
- General/position.scala General/scan.scala General/swing_thread.scala \
- 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
-
+SCALA_FILES = General/event_bus.scala General/linear_set.scala \
+ General/markup.scala General/position.scala General/scan.scala \
+ General/swing_thread.scala 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_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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/Isar/isar.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/Isar/outer_keyword.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/Thy/thy_header.scala Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/display.ML Tue Sep 01 14:13:34 2009 +0200
@@ -27,12 +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 print_ctyp: ctyp -> unit
- val pretty_cterm: cterm -> Pretty.T
- val string_of_cterm: cterm -> string
- val print_cterm: cterm -> unit
val print_syntax: theory -> unit
val pretty_full_theory: bool -> theory -> Pretty.T list
end;
@@ -121,17 +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);
-val print_ctyp = writeln o string_of_ctyp;
-
-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);
-val print_cterm = writeln o string_of_cterm;
-
-
(** print theory **)
--- a/src/Pure/old_goals.ML Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Pure/old_goals.ML Tue Sep 01 14:13:34 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 Tue Sep 01 14:12:18 2009 +0200
+++ b/src/Tools/induct.ML Tue Sep 01 14:13:34 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)))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/more_conv.ML Tue Sep 01 14:13:34 2009 +0200
@@ -0,0 +1,61 @@
+(* Title: Tools/more_conv.ML
+ Author: Sascha Boehme
+
+Further conversions and conversionals.
+*)
+
+signature MORE_CONV =
+sig
+ val rewrs_conv: thm list -> conv
+
+ val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
+ val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
+ val top_conv: (Proof.context -> conv) -> Proof.context -> conv
+ val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
+
+ val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
+
+ val cache_conv: conv -> conv
+end
+
+
+
+structure More_Conv : MORE_CONV =
+struct
+
+
+fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)
+
+
+fun sub_conv conv ctxt =
+ Conv.comb_conv (conv ctxt) else_conv
+ Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv
+ Conv.all_conv
+
+fun bottom_conv conv ctxt ct =
+ (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct
+
+fun top_conv conv ctxt ct =
+ (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct
+
+fun top_sweep_conv conv ctxt ct =
+ (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct
+
+
+fun binder_conv cv ctxt =
+ Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
+
+
+fun cache_conv conv =
+ let
+ val tab = ref Termtab.empty
+ fun add_result t thm =
+ let val _ = change tab (Termtab.insert Thm.eq_thm (t, thm))
+ in thm end
+ fun cconv ct =
+ (case Termtab.lookup (!tab) (Thm.term_of ct) of
+ SOME thm => thm
+ | NONE => add_result (Thm.term_of ct) (conv ct))
+ in cconv end
+
+end
--- a/src/ZF/Datatype_ZF.thy Tue Sep 01 14:12:18 2009 +0200
+++ b/src/ZF/Datatype_ZF.thy Tue Sep 01 14:13:34 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