# HG changeset patch # User Andreas Lochbihler # Date 1341300701 -7200 # Node ID 5016a36205fac50cfcdecb011c3354d4b5a6b489 # Parent 3d9c1ddb9f47807eee79e27b59fd91a4ae9d1881# Parent eb72f99737be80d7f94a5f28034fba7541539222 merged diff -r 3d9c1ddb9f47 -r 5016a36205fa Admin/components.x86-linux --- 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 diff -r 3d9c1ddb9f47 -r 5016a36205fa Admin/components.x86_64-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 diff -r 3d9c1ddb9f47 -r 5016a36205fa Admin/init_components --- 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" diff -r 3d9c1ddb9f47 -r 5016a36205fa Admin/isatest/pmail --- 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" diff -r 3d9c1ddb9f47 -r 5016a36205fa NEWS --- 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 \ 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 diff -r 3d9c1ddb9f47 -r 5016a36205fa doc-src/IsarRef/isar-ref.tex --- 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} diff -r 3d9c1ddb9f47 -r 5016a36205fa doc-src/TutorialI/tutorial.tex --- 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! diff -r 3d9c1ddb9f47 -r 5016a36205fa lib/Tools/mkdir --- 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 @@ %\, \, \, \, \, %\, \, \ -%\usepackage[greek,english]{babel} - %option greek for \ - %option english (default language) for \, \ +%\usepackage{eurosym} + %for \ %\usepackage[only,bigsqcap]{stmaryrd} %for \ diff -r 3d9c1ddb9f47 -r 5016a36205fa lib/texinputs/isabellesym.sty --- 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 diff -r 3d9c1ddb9f47 -r 5016a36205fa src/HOL/IMP/document/root.tex --- 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 \, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage[greek,english]{babel} - %option greek for \ - %option english (default language) for \, \ - -%\usepackage[latin1]{inputenc} - %for \, \, \, \, - %\, \, \ - -%\usepackage[only,bigsqcap]{stmaryrd} - %for \ - -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \ - % this should be the last package used \usepackage{pdfsetup} diff -r 3d9c1ddb9f47 -r 5016a36205fa src/HOL/Library/Function_Algebras.thy --- 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 + diff -r 3d9c1ddb9f47 -r 5016a36205fa src/HOL/SPARK/Manual/Reference.thy --- 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. diff -r 3d9c1ddb9f47 -r 5016a36205fa src/HOL/SPARK/Tools/spark_commands.ML --- 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 diff -r 3d9c1ddb9f47 -r 5016a36205fa src/HOL/SPARK/Tools/spark_vcs.ML --- 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; diff -r 3d9c1ddb9f47 -r 5016a36205fa src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy --- 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 ((\(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \ 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