--- a/Admin/components.x86-linux Tue Jul 03 09:26:52 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-contrib/jdk-6u31_x86-linux
--- a/Admin/components.x86_64-linux Tue Jul 03 09:26:52 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-contrib/jdk-6u31_x86_64-linux
--- a/Admin/init_components Tue Jul 03 09:26:52 2012 +0200
+++ b/Admin/init_components Tue Jul 03 09:31:41 2012 +0200
@@ -16,14 +16,11 @@
fi
}
-for COMPONENTS_FILE in "${ISABELLE_HOME}/Admin/components" "${ISABELLE_HOME}/Admin/components.${ML_PLATFORM}"
+while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
do
- while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
- do
- case "${REPLY}" in
- \#* | "") ;;
- /*) init_component_liberal "${REPLY}" ;;
- *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
- esac
- done < "${COMPONENTS_FILE}"
-done
+ case "${REPLY}" in
+ \#* | "") ;;
+ /*) init_component_liberal "${REPLY}" ;;
+ *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
+ esac
+done < "${ISABELLE_HOME}/Admin/components"
--- a/Admin/isatest/pmail Tue Jul 03 09:26:52 2012 +0200
+++ b/Admin/isatest/pmail Tue Jul 03 09:31:41 2012 +0200
@@ -95,7 +95,7 @@
case `uname` in
Linux) for F in $@; do ATTACH="$ATTACH -a $F"; done
- cat "$BODY" | mail -Ssmtp=mailbroy.informatik.tu-muenchen.de -s "$SUBJECT" $ATTACH "$TO"
+ cat "$BODY" | mail -s "$SUBJECT" $ATTACH "$TO"
;;
SunOS)
print_body "$SUBJECT" "$BODY" $@ | mail -t "$TO"
--- a/NEWS Tue Jul 03 09:26:52 2012 +0200
+++ b/NEWS Tue Jul 03 09:31:41 2012 +0200
@@ -13,6 +13,12 @@
in old "ref" manual.
+*** Document preparation ***
+
+* Default for \<euro> is now based on eurosym package, instead of
+slightly exotic babel/greek.
+
+
*** System ***
* Discontinued support for Poly/ML 5.2.1, which was the last version
--- a/doc-src/IsarRef/isar-ref.tex Tue Jul 03 09:26:52 2012 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Tue Jul 03 09:31:41 2012 +0200
@@ -1,6 +1,7 @@
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{amssymb}
-\usepackage[greek,english]{babel}
+\usepackage{eurosym}
+\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{textcomp}
\usepackage{latexsym}
--- a/doc-src/TutorialI/tutorial.tex Tue Jul 03 09:26:52 2012 +0200
+++ b/doc-src/TutorialI/tutorial.tex Tue Jul 03 09:31:41 2012 +0200
@@ -3,7 +3,8 @@
\usepackage{cl2emono-modified,../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
\usepackage{../proof,amsmath,amsfonts}
\usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}
-\usepackage[greek,english]{babel}
+\usepackage{eurosym}
+\usepackage[english]{babel}
\usepackage{../pdfsetup}
%last package!
--- a/lib/Tools/mkdir Tue Jul 03 09:26:52 2012 +0200
+++ b/lib/Tools/mkdir Tue Jul 03 09:31:41 2012 +0200
@@ -217,9 +217,8 @@
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
-%\usepackage[greek,english]{babel}
- %option greek for \<euro>
- %option english (default language) for \<guillemotleft>, \<guillemotright>
+%\usepackage{eurosym}
+ %for \<euro>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
--- a/lib/texinputs/isabellesym.sty Tue Jul 03 09:26:52 2012 +0200
+++ b/lib/texinputs/isabellesym.sty Tue Jul 03 09:31:41 2012 +0200
@@ -336,7 +336,7 @@
\newcommand{\isasymparagraph}{\isatext{\rm\P}}
\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
-\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
+\newcommand{\isasymeuro}{\isatext{\euro}} %requires eurosym
\newcommand{\isasympounds}{\isamath{\pounds}}
\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
--- a/src/HOL/IMP/document/root.tex Tue Jul 03 09:26:52 2012 +0200
+++ b/src/HOL/IMP/document/root.tex Tue Jul 03 09:31:41 2012 +0200
@@ -6,28 +6,6 @@
\usepackage{latexsym}
-%\usepackage{amssymb}
- %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
- %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
- %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage[greek,english]{babel}
- %option greek for \<euro>
- %option english (default language) for \<guillemotleft>, \<guillemotright>
-
-%\usepackage[latin1]{inputenc}
- %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
- %\<threesuperior>, \<threequarters>, \<degree>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
- %for \<Sqinter>
-
-%\usepackage{eufrak}
- %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
- %for \<cent>, \<currency>
-
% this should be the last package used
\usepackage{pdfsetup}
--- a/src/HOL/Library/Function_Algebras.thy Tue Jul 03 09:26:52 2012 +0200
+++ b/src/HOL/Library/Function_Algebras.thy Tue Jul 03 09:31:41 2012 +0200
@@ -18,6 +18,10 @@
end
+lemma plus_fun_apply [simp]:
+ "(f + g) x = f x + g x"
+ by (simp add: plus_fun_def)
+
instantiation "fun" :: (type, zero) zero
begin
@@ -26,6 +30,10 @@
end
+lemma zero_fun_apply [simp]:
+ "0 x = 0"
+ by (simp add: zero_fun_def)
+
instantiation "fun" :: (type, times) times
begin
@@ -34,6 +42,10 @@
end
+lemma times_fun_apply [simp]:
+ "(f * g) x = f x * g x"
+ by (simp add: times_fun_def)
+
instantiation "fun" :: (type, one) one
begin
@@ -42,23 +54,27 @@
end
+lemma one_fun_apply [simp]:
+ "1 x = 1"
+ by (simp add: one_fun_def)
+
text {* Additive structures *}
instance "fun" :: (type, semigroup_add) semigroup_add
- by default (simp add: plus_fun_def add.assoc)
+ by default (simp add: fun_eq_iff add.assoc)
instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
- by default (simp_all add: plus_fun_def fun_eq_iff)
+ by default (simp_all add: fun_eq_iff)
instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
- by default (simp add: plus_fun_def add.commute)
+ by default (simp add: fun_eq_iff add.commute)
instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
by default simp
instance "fun" :: (type, monoid_add) monoid_add
- by default (simp_all add: plus_fun_def zero_fun_def)
+ by default (simp_all add: fun_eq_iff)
instance "fun" :: (type, comm_monoid_add) comm_monoid_add
by default simp
@@ -67,7 +83,7 @@
instance "fun" :: (type, group_add) group_add
by default
- (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+ (simp_all add: fun_eq_iff diff_minus)
instance "fun" :: (type, ab_group_add) ab_group_add
by default (simp_all add: diff_minus)
@@ -76,16 +92,16 @@
text {* Multiplicative structures *}
instance "fun" :: (type, semigroup_mult) semigroup_mult
- by default (simp add: times_fun_def mult.assoc)
+ by default (simp add: fun_eq_iff mult.assoc)
instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
- by default (simp add: times_fun_def mult.commute)
+ by default (simp add: fun_eq_iff mult.commute)
instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
- by default (simp add: times_fun_def)
+ by default (simp add: fun_eq_iff)
instance "fun" :: (type, monoid_mult) monoid_mult
- by default (simp_all add: times_fun_def one_fun_def)
+ by default (simp_all add: fun_eq_iff)
instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
by default simp
@@ -96,19 +112,19 @@
instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
instance "fun" :: (type, mult_zero) mult_zero
- by default (simp_all add: zero_fun_def times_fun_def)
+ by default (simp_all add: fun_eq_iff)
instance "fun" :: (type, zero_neq_one) zero_neq_one
- by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
+ by default (simp add: fun_eq_iff)
text {* Ring structures *}
instance "fun" :: (type, semiring) semiring
- by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
+ by default (simp_all add: fun_eq_iff algebra_simps)
instance "fun" :: (type, comm_semiring) comm_semiring
- by default (simp add: plus_fun_def times_fun_def algebra_simps)
+ by default (simp add: fun_eq_iff algebra_simps)
instance "fun" :: (type, semiring_0) semiring_0 ..
@@ -133,6 +149,10 @@
finally show ?thesis by (simp add: of_nat_def comp)
qed
+lemma of_nat_fun_apply [simp]:
+ "of_nat n x = of_nat n"
+ by (simp add: of_nat_fun)
+
instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
@@ -162,12 +182,12 @@
text {* Ordereded structures *}
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
- by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
+ by default (auto simp add: le_fun_def intro: add_left_mono)
instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
- by default (simp add: plus_fun_def le_fun_def)
+ by default (simp add: le_fun_def)
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
@@ -175,7 +195,7 @@
instance "fun" :: (type, ordered_semiring) ordered_semiring
by default
- (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
+ (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
by default (fact mult_left_mono)
@@ -195,3 +215,4 @@
lemmas func_one = one_fun_def
end
+
--- a/src/HOL/SPARK/Manual/Reference.thy Tue Jul 03 09:26:52 2012 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy Tue Jul 03 09:31:41 2012 +0200
@@ -67,8 +67,9 @@
must be followed by a sequence of proof commands. The command introduces the
hypotheses \texttt{H1} \dots \texttt{H$n$}, as well as the identifiers
\texttt{?C1} \dots \texttt{?C$m$} corresponding to the conclusions of the VC.
-@{rail "@'spark_end'"}
-Closes the current verification environment. All VCs must have been proved,
+@{rail "@'spark_end' '(incomplete)'?"}
+Closes the current verification environment. Unless the \texttt{incomplete}
+option is given, all VCs must have been proved,
otherwise the command issues an error message. As a side effect, the command
generates a proof review (\texttt{*.prv}) file to inform POGS of the proved
VCs.
--- a/src/HOL/SPARK/Tools/spark_commands.ML Tue Jul 03 09:26:52 2012 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Tue Jul 03 09:31:41 2012 +0200
@@ -44,7 +44,7 @@
SPARK_VCs.add_type (s, (Syntax.read_typ_global thy raw_typ, cmap)) thy;
fun get_vc thy vc_name =
- (case SPARK_VCs.lookup_vc thy vc_name of
+ (case SPARK_VCs.lookup_vc thy false vc_name of
SOME (ctxt, (_, proved, ctxt', stmt)) =>
if is_some proved then
error ("The verification condition " ^
@@ -71,7 +71,7 @@
let
val thy = Toplevel.theory_of state;
- val (context, defs, vcs) = SPARK_VCs.get_vcs thy;
+ val (context, defs, vcs) = SPARK_VCs.get_vcs thy true;
val vcs' = AList.coalesce (op =) (map_filter
(fn (name, (trace, status, ctxt, stmt)) =>
@@ -144,7 +144,9 @@
val _ =
Outer_Syntax.command @{command_spec "spark_end"}
"close the current SPARK environment"
- (Scan.succeed (Toplevel.theory SPARK_VCs.close));
+ (Scan.optional (@{keyword "("} |-- Parse.!!!
+ (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
+ (Toplevel.theory o SPARK_VCs.close));
val setup = Theory.at_end (fn thy =>
let
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Jul 03 09:26:52 2012 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Tue Jul 03 09:31:41 2012 +0200
@@ -13,13 +13,13 @@
string * ((string list * string) option * 'a) ->
theory -> theory
val add_type: string * (typ * (string * string) list) -> theory -> theory
- val lookup_vc: theory -> string -> (Element.context_i list *
+ val lookup_vc: theory -> bool -> string -> (Element.context_i list *
(string * thm list option * Element.context_i * Element.statement_i)) option
- val get_vcs: theory ->
+ val get_vcs: theory -> bool ->
Element.context_i list * (binding * thm) list * (string *
(string * thm list option * Element.context_i * Element.statement_i)) list
val mark_proved: string -> thm list -> theory -> theory
- val close: theory -> theory
+ val close: bool -> theory -> theory
val is_closed: theory -> bool
end;
@@ -756,9 +756,23 @@
(** the VC store **)
-fun err_vcs names = error (Pretty.string_of
- (Pretty.big_list "The following verification conditions have not been proved:"
- (map Pretty.str names)))
+fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs);
+
+fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved."
+ | pp_open_vcs vcs = pp_vcs
+ "The following verification conditions remain to be proved:" vcs;
+
+fun partition_vcs vcs = VCtab.fold_rev
+ (fn (name, (trace, SOME thms, ps, cs)) =>
+ apfst (cons (name, (trace, thms, ps, cs)))
+ | (name, (trace, NONE, ps, cs)) =>
+ apsnd (cons (name, (trace, ps, cs))))
+ vcs ([], []);
+
+fun insert_break prt = Pretty.blk (0, [Pretty.fbrk, prt]);
+
+fun print_open_vcs f vcs =
+ (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);
fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
{pfuns, type_map, env = NONE} =>
@@ -767,7 +781,7 @@
env = SOME
{ctxt = ctxt, defs = defs, types = types, funs = funs,
pfuns = check_pfuns_types thy prefix funs pfuns,
- ids = ids, proving = false, vcs = vcs, path = path,
+ ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path,
prefix = prefix}}
| _ => err_unfinished ()) thy;
@@ -775,7 +789,7 @@
SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
| NONE => error ("Bad conclusion identifier: C" ^ s));
-fun mk_vc thy prfx types pfuns ids (tr, proved, ps, cs) =
+fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
let val prop_of =
HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
in
@@ -783,7 +797,9 @@
Element.Assumes (map (fn (s', e) =>
((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
Element.Shows (map (fn (s', e) =>
- (Attrib.empty_binding, [(prop_of e, mk_pat s')])) cs))
+ (if name_concl then (Binding.name ("C" ^ s'), [])
+ else Attrib.empty_binding,
+ [(prop_of e, mk_pat s')])) cs))
end;
fun fold_vcs f vcs =
@@ -898,25 +914,28 @@
val is_closed = is_none o #env o VCs.get;
-fun lookup_vc thy name =
+fun lookup_vc thy name_concl name =
(case VCs.get thy of
{env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
(case VCtab.lookup vcs name of
SOME vc =>
let val (pfuns', ctxt', ids') =
declare_missing_pfuns thy prefix funs pfuns vcs ids
- in SOME (ctxt @ [ctxt'], mk_vc thy prefix types pfuns' ids' vc) end
+ in
+ SOME (ctxt @ [ctxt'],
+ mk_vc thy prefix types pfuns' ids' name_concl vc)
+ end
| NONE => NONE)
| _ => NONE);
-fun get_vcs thy = (case VCs.get thy of
+fun get_vcs thy name_concl = (case VCs.get thy of
{env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} =>
let val (pfuns', ctxt', ids') =
declare_missing_pfuns thy prefix funs pfuns vcs ids
in
(ctxt @ [ctxt'], defs,
VCtab.dest vcs |>
- map (apsnd (mk_vc thy prefix types pfuns' ids')))
+ map (apsnd (mk_vc thy prefix types pfuns' ids' name_concl)))
end
| _ => ([], [], []));
@@ -930,25 +949,34 @@
types = types, funs = funs, pfuns = pfuns_env,
ids = ids,
proving = true,
- vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
- (trace, SOME thms, ps, cs)) vcs,
+ vcs = print_open_vcs insert_break (VCtab.map_entry name
+ (fn (trace, _, ps, cs) => (trace, SOME thms, ps, cs)) vcs),
path = path,
prefix = prefix}}
| x => x);
-fun close thy =
+fun close incomplete thy =
thy |>
VCs.map (fn
{pfuns, type_map, env = SOME {vcs, path, ...}} =>
- (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
- (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
- (proved, []) =>
- (Thm.join_proofs (maps (the o #2 o snd) proved);
- File.write (Path.ext "prv" path)
- (implode (map (fn (s, _) => snd (strip_number s) ^
- " -- proved by " ^ Distribution.version ^ "\n") proved));
- {pfuns = pfuns, type_map = type_map, env = NONE})
- | (_, unproved) => err_vcs (map fst unproved))
+ let
+ val (proved, unproved) = partition_vcs vcs;
+ val _ = Thm.join_proofs (maps (#2 o snd) proved);
+ val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
+ exists (#oracle o Thm.status_of) thms) proved
+ in
+ (if null unproved then ()
+ else (if incomplete then warning else error)
+ (Pretty.string_of (pp_open_vcs unproved));
+ if null proved' then ()
+ else warning (Pretty.string_of (pp_vcs
+ "The following VCs are not marked as proved \
+ \because their proofs contain oracles:" proved'));
+ File.write (Path.ext "prv" path)
+ (implode (map (fn (s, _) => snd (strip_number s) ^
+ " -- proved by " ^ Distribution.version ^ "\n") proved''));
+ {pfuns = pfuns, type_map = type_map, env = NONE})
+ end
| _ => error "No SPARK environment is currently open") |>
Sign.parent_path;
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Tue Jul 03 09:26:52 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Tue Jul 03 09:31:41 2012 +0200
@@ -64,4 +64,14 @@
= finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))"
by simp
+lemma
+ assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
+proof -
+ have eq: "{(a,b,c,d). ([a, b], [c, d]) : S} = ((%(a, b, c, d). ([a, b], [c, d])) -` S)"
+ unfolding vimage_def by (auto split: prod.split) (* to be proved with the simproc *)
+ from `finite S` show ?thesis
+ unfolding eq by (auto intro!: finite_vimageI simp add: inj_on_def)
+ (* to be automated with further rules and automation *)
+qed
+
end