--- a/Admin/Release/build_library Thu Sep 26 16:52:24 2013 +0200
+++ b/Admin/Release/build_library Fri Sep 27 09:17:25 2013 +0200
@@ -61,7 +61,10 @@
## main
-export COPYFILE_DISABLE=true
+#GNU tar (notably on Mac OS X)
+if [ -x /usr/bin/gnutar ]; then
+ function tar() { /usr/bin/gnutar "$@"; }
+fi
TMP="/var/tmp/isabelle-makedist$$"
mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
--- a/Admin/components/components.sha1 Thu Sep 26 16:52:24 2013 +0200
+++ b/Admin/components/components.sha1 Fri Sep 27 09:17:25 2013 +0200
@@ -37,6 +37,7 @@
5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz
87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz
c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz
+65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
--- a/Admin/components/main Thu Sep 26 16:52:24 2013 +0200
+++ b/Admin/components/main Fri Sep 27 09:17:25 2013 +0200
@@ -4,7 +4,7 @@
exec_process-1.0.3
Haskabelle-2013
jdk-7u40
-jedit_build-20130925
+jedit_build-20130926
jfreechart-1.0.14-1
kodkodi-1.5.2
polyml-5.5.1
--- a/Admin/java/build Thu Sep 26 16:52:24 2013 +0200
+++ b/Admin/java/build Fri Sep 27 09:17:25 2013 +0200
@@ -71,7 +71,10 @@
# content
-export COPYFILE_DISABLE=true
+#GNU tar (notably on Mac OS X)
+if [ -x /usr/bin/gnutar ]; then
+ function tar() { /usr/bin/gnutar "$@"; }
+fi
mkdir "$DIR/x86-linux" "$DIR/x86_64-linux" "$DIR/x86_64-darwin" "$DIR/x86-cygwin"
--- a/Admin/lib/Tools/makedist Thu Sep 26 16:52:24 2013 +0200
+++ b/Admin/lib/Tools/makedist Fri Sep 27 09:17:25 2013 +0200
@@ -199,7 +199,7 @@
chmod -R g=o "$DISTNAME"
echo "$DISTBASE/$DISTNAME.tar.gz"
-env COPYFILE_DISABLE=true tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
+tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
[ "$?" = 0 ] || exit "$?"
--- a/Admin/lib/Tools/makedist_bundle Thu Sep 26 16:52:24 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle Fri Sep 27 09:17:25 2013 +0200
@@ -41,8 +41,6 @@
## main
-export COPYFILE_DISABLE=true
-
TMP="/var/tmp/isabelle-makedist$$"
mkdir "$TMP" || fail "Cannot create directory $TMP"
@@ -172,6 +170,7 @@
mv "$ISABELLE_TARGET/contrib/macos_app" "$TMP/."
perl -pi \
+ -e 's,\Qaction-bar.shortcut=C+ENTER\E,action-bar.shortcut=\naction-bar.shortcut2=C+ENTER,g;' \
-e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
-e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
-e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
--- a/lib/scripts/getsettings Thu Sep 26 16:52:24 2013 +0200
+++ b/lib/scripts/getsettings Fri Sep 27 09:17:25 2013 +0200
@@ -11,6 +11,11 @@
ISABELLE_SETTINGS_PRESENT=true
+#GNU tar (notably on Mac OS X)
+if [ -x /usr/bin/gnutar ]; then
+ function tar() { /usr/bin/gnutar "$@"; }
+fi
+
#Cygwin vs. POSIX
if [ "$OSTYPE" = cygwin ]
then
--- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 27 09:17:25 2013 +0200
@@ -781,9 +781,18 @@
\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
@{thm list.disc_exhaust[no_vars]}
+\item[@{text "t."}\hthm{sel\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
+@{thm list.sel_exhaust[no_vars]}
+
\item[@{text "t."}\hthm{expand}\rm:] ~ \\
@{thm list.expand[no_vars]}
+\item[@{text "t."}\hthm{sel\_split}\rm:] ~ \\
+@{thm list.sel_split[no_vars]}
+
+\item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
+@{thm list.sel_split_asm[no_vars]}
+
\item[@{text "t."}\hthm{case\_conv\_if}\rm:] ~ \\
@{thm list.case_conv_if[no_vars]}
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Fri Sep 27 09:17:25 2013 +0200
@@ -25,8 +25,11 @@
discIs: thm list,
sel_thmss: thm list list,
disc_exhausts: thm list,
+ sel_exhausts: thm list,
collapses: thm list,
expands: thm list,
+ sel_splits: thm list,
+ sel_split_asms: thm list,
case_conv_ifs: thm list};
val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
@@ -78,8 +81,11 @@
discIs: thm list,
sel_thmss: thm list list,
disc_exhausts: thm list,
+ sel_exhausts: thm list,
collapses: thm list,
expands: thm list,
+ sel_splits: thm list,
+ sel_split_asms: thm list,
case_conv_ifs: thm list};
fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
@@ -88,7 +94,7 @@
fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
- disc_exhausts, collapses, expands, case_conv_ifs} =
+ disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_conv_ifs} =
{ctrs = map (Morphism.term phi) ctrs,
casex = Morphism.term phi casex,
discs = map (Morphism.term phi) discs,
@@ -106,8 +112,11 @@
discIs = map (Morphism.thm phi) discIs,
sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
disc_exhausts = map (Morphism.thm phi) disc_exhausts,
+ sel_exhausts = map (Morphism.thm phi) sel_exhausts,
collapses = map (Morphism.thm phi) collapses,
expands = map (Morphism.thm phi) expands,
+ sel_splits = map (Morphism.thm phi) sel_splits,
+ sel_split_asms = map (Morphism.thm phi) sel_split_asms,
case_conv_ifs = map (Morphism.thm phi) case_conv_ifs};
val transfer_ctr_sugar =
@@ -153,6 +162,9 @@
val injectN = "inject";
val nchotomyN = "nchotomy";
val selN = "sel";
+val sel_exhaustN = "sel_exhaust";
+val sel_splitN = "sel_split";
+val sel_split_asmN = "sel_split_asm";
val splitN = "split";
val splitsN = "splits";
val split_asmN = "split_asm";
@@ -240,16 +252,20 @@
(case ctr_sugar_of ctxt s of
SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
if case_name = c then
- let
- val n = length discs0;
- val (branches, obj :: leftovers) = chop n args;
- val discs = map (mk_disc_or_sel Ts) discs0;
- val selss = map (map (mk_disc_or_sel Ts)) selss0;
- val conds = map (rapp obj) discs;
- val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
- val branches' = map2 (curry Term.betapplys) branches branch_argss;
- in
- SOME (conds, branches')
+ let val n = length discs0 in
+ if n < length args then
+ let
+ val (branches, obj :: leftovers) = chop n args;
+ val discs = map (mk_disc_or_sel Ts) discs0;
+ val selss = map (map (mk_disc_or_sel Ts)) selss0;
+ val conds = map (rapp obj) discs;
+ val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
+ val branches' = map2 (curry Term.betapplys) branches branch_argss;
+ in
+ SOME (conds, branches')
+ end
+ else
+ NONE
end
else
NONE
@@ -298,12 +314,10 @@
val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
- fun can_definitely_rely_on_disc k =
- not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
+ fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
fun can_rely_on_disc k =
can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
- fun should_omit_disc_binding k =
- n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
+ fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
fun is_disc_binding_valid b =
not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
@@ -372,10 +386,9 @@
fun mk_case_disj xctr xf xs =
list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf)));
- val case_rhs =
- fold_rev (fold_rev Term.lambda) [fs, [u]]
- (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
- Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
+ val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]]
+ (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
+ Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
|> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs))
@@ -415,10 +428,9 @@
if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
end);
- val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
- sel_defss, lthy') =
+ val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
if no_discs_sels then
- (true, [], [], [], [], [], [], [], [], [], lthy)
+ (true, [], [], [], [], [], lthy)
else
let
fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
@@ -501,15 +513,8 @@
val discs = map (mk_disc_or_sel As) discs0;
val selss = map (map (mk_disc_or_sel As)) selss0;
-
- val udiscs = map (rapp u) discs;
- val uselss = map (map (rapp u)) selss;
-
- val vdiscs = map (rapp v) discs;
- val vselss = map (map (rapp v)) selss;
in
- (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
- sel_defss, lthy')
+ (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy')
end;
fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
@@ -584,13 +589,76 @@
ks goals inject_thmss distinct_thmsss
end;
+ val (case_cong_thm, weak_case_cong_thm) =
+ let
+ fun mk_prem xctr xs xf xg =
+ fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
+ mk_Trueprop_eq (xf, xg)));
+
+ val goal =
+ Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
+ mk_Trueprop_eq (eta_ufcase, eta_vgcase));
+ val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
+ in
+ (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
+ Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
+ |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
+ end;
+
+ val split_lhs = q $ ufcase;
+
+ fun mk_split_conjunct xctr xs f_xs =
+ list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
+ fun mk_split_disjunct xctr xs f_xs =
+ list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
+ HOLogic.mk_not (q $ f_xs)));
+
+ fun mk_split_goal xctrs xss xfs =
+ mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj
+ (map3 mk_split_conjunct xctrs xss xfs));
+ fun mk_split_asm_goal xctrs xss xfs =
+ mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
+ (map3 mk_split_disjunct xctrs xss xfs)));
+
+ fun prove_split selss goal =
+ Goal.prove_sorry lthy [] [] goal (fn _ =>
+ mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
+
+ fun prove_split_asm asm_goal split_thm =
+ Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
+ mk_split_asm_tac ctxt split_thm)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy);
+
+ val (split_thm, split_asm_thm) =
+ let
+ val goal = mk_split_goal xctrs xss xfs;
+ val asm_goal = mk_split_asm_goal xctrs xss xfs;
+
+ val thm = prove_split (replicate n []) goal;
+ val asm_thm = prove_split_asm asm_goal thm;
+ in
+ (thm, asm_thm)
+ end;
+
val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
- disc_exclude_thms, disc_exhaust_thms, all_collapse_thms, safe_collapse_thms,
- expand_thms, case_conv_if_thms) =
+ disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
+ safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms,
+ case_conv_if_thms) =
if no_discs_sels then
- ([], [], [], [], [], [], [], [], [], [], [], [])
+ ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
else
let
+ val udiscs = map (rapp u) discs;
+ val uselss = map (map (rapp u)) selss;
+ val usel_ctrs = map2 (curry Term.list_comb) ctrs uselss;
+ val usel_fs = map2 (curry Term.list_comb) fs uselss;
+
+ val vdiscs = map (rapp v) discs;
+ val vselss = map (map (rapp v)) selss;
+
fun make_sel_thm xs' case_thm sel_def =
zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
@@ -711,15 +779,14 @@
val (safe_collapse_thms, all_collapse_thms) =
let
- fun mk_goal ctr udisc usels =
+ fun mk_goal m ctr udisc usel_ctr =
let
val prem = HOLogic.mk_Trueprop udisc;
- val concl =
- mk_Trueprop_eq ((null usels ? swap) (Term.list_comb (ctr, usels), u));
+ val concl = mk_Trueprop_eq ((usel_ctr, u) |> m = 0 ? swap);
in
(prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl)))
end;
- val (trivs, goals) = map3 mk_goal ctrs udiscs uselss |> split_list;
+ val (trivs, goals) = map4 mk_goal ms ctrs udiscs usel_ctrs |> split_list;
val thms =
map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
@@ -732,7 +799,20 @@
thms)
end;
- val expand_thms =
+ val swapped_all_collapse_thms =
+ map2 (fn m => fn thm => if m = 0 then thm else thm RS sym) ms all_collapse_thms;
+
+ val sel_exhaust_thm =
+ let
+ fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)];
+ val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem usel_ctrs));
+ in
+ Goal.prove_sorry lthy [] [] goal (fn _ =>
+ mk_sel_exhaust_tac n disc_exhaust_thm swapped_all_collapse_thms)
+ |> Thm.close_derivation
+ end;
+
+ val expand_thm =
let
fun mk_prems k udisc usels vdisc vsels =
(if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
@@ -750,76 +830,42 @@
val uncollapse_thms =
map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
in
- [Goal.prove_sorry lthy [] [] goal (fn _ =>
- mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
- (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
- disc_exclude_thmsss')]
- |> map Thm.close_derivation
- |> Proof_Context.export names_lthy lthy
+ Goal.prove_sorry lthy [] [] goal (fn _ =>
+ mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
+ (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
+ disc_exclude_thmsss')
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
- val case_conv_if_thms =
+ val (sel_split_thm, sel_split_asm_thm) =
let
- fun mk_body f usels = Term.list_comb (f, usels);
- val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
+ val zss = map (K []) xss;
+ val goal = mk_split_goal usel_ctrs zss usel_fs;
+ val asm_goal = mk_split_asm_goal usel_ctrs zss usel_fs;
+
+ val thm = prove_split sel_thmss goal;
+ val asm_thm = prove_split_asm asm_goal thm;
in
- [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
- |> map Thm.close_derivation
- |> Proof_Context.export names_lthy lthy
+ (thm, asm_thm)
+ end;
+
+ val case_conv_if_thm =
+ let
+ val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
+ in
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_case_conv_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
end;
in
(all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
- nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], all_collapse_thms,
- safe_collapse_thms, expand_thms, case_conv_if_thms)
+ nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
+ all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
+ [sel_split_asm_thm], [case_conv_if_thm])
end;
- val (case_cong_thm, weak_case_cong_thm) =
- let
- fun mk_prem xctr xs xf xg =
- fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
- mk_Trueprop_eq (xf, xg)));
-
- val goal =
- Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
- mk_Trueprop_eq (eta_ufcase, eta_vgcase));
- val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
- in
- (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
- Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
- |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
- end;
-
- val (split_thm, split_asm_thm) =
- let
- fun mk_conjunct xctr xs f_xs =
- list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
- fun mk_disjunct xctr xs f_xs =
- list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
- HOLogic.mk_not (q $ f_xs)));
-
- val lhs = q $ ufcase;
-
- val goal =
- mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
- val asm_goal =
- mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
- (map3 mk_disjunct xctrs xss xfs)));
-
- val split_thm =
- Goal.prove_sorry lthy [] [] goal
- (fn _ => mk_split_tac lthy uexhaust_thm case_thms inject_thmss distinct_thmsss)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
- val split_asm_thm =
- Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
- mk_split_asm_tac ctxt split_thm)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy);
- in
- (split_thm, split_asm_thm)
- end;
-
val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
@@ -838,6 +884,9 @@
(injectN, inject_thms, iff_attrs @ induct_simp_attrs),
(nchotomyN, [nchotomy_thm], []),
(selN, all_sel_thms, code_nitpick_simp_simp_attrs),
+ (sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]),
+ (sel_splitN, sel_split_thms, []),
+ (sel_split_asmN, sel_split_asm_thms, []),
(splitN, [split_thm], []),
(split_asmN, [split_asm_thm], []),
(splitsN, [split_thm, split_asm_thm], []),
@@ -856,7 +905,9 @@
case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
- collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms};
+ sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
+ sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
+ case_conv_ifs = case_conv_if_thms};
in
(ctr_sugar,
lthy
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Fri Sep 27 09:17:25 2013 +0200
@@ -19,8 +19,9 @@
val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
val mk_nchotomy_tac: int -> thm -> tactic
val mk_other_half_disc_exclude_tac: thm -> tactic
- val mk_split_tac: Proof.context ->
- thm -> thm list -> thm list list -> thm list list list -> tactic
+ val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic
+ val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> thm list
+ list list -> tactic
val mk_split_asm_tac: Proof.context -> thm -> tactic
val mk_unique_disc_def_tac: int -> thm -> tactic
end;
@@ -56,10 +57,16 @@
fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
-fun mk_disc_exhaust_tac n exhaust discIs =
+fun mk_disc_or_sel_exhaust_tac n exhaust destIs =
HEADGOAL (rtac exhaust THEN'
- EVERY' (map2 (fn k => fn discI =>
- dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs));
+ EVERY' (map2 (fn k => fn destI => dtac destI THEN'
+ select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs));
+
+val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
+
+fun mk_sel_exhaust_tac n disc_exhaust collapses =
+ mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
+ HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
fun mk_collapse_tac ctxt m discD sels =
HEADGOAL (dtac discD THEN'
@@ -134,10 +141,10 @@
HEADGOAL (rtac uexhaust THEN'
EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
-fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
+fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
HEADGOAL (rtac uexhaust) THEN
ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
- simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
+ simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
flat (nth distinctsss (k - 1))) ctxt)) k) THEN
ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Sep 27 09:17:25 2013 +0200
@@ -734,7 +734,7 @@
val (defs, exclss') =
co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
- fun prove_excl_tac (c, c', a) =
+ fun excl_tac (c, c', a) =
if a orelse c = c' orelse sequential then SOME (K (mk_primcorec_assumption_tac lthy []))
else if simple then SOME (K (auto_tac lthy))
else NONE;
@@ -745,7 +745,7 @@
*)
val exclss'' = exclss' |> map (map (fn (idx, t) =>
- (idx, (Option.map (Goal.prove lthy [] [] t) (prove_excl_tac idx), t))));
+ (idx, (Option.map (Goal.prove lthy [] [] t) (excl_tac idx), t))));
val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
val (obligation_idxss, obligationss) = exclss''
|> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
@@ -800,9 +800,9 @@
|> HOLogic.mk_Trueprop o HOLogic.mk_eq
|> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
|> curry Logic.list_all (map dest_Free fun_args);
- val (distincts, _, _, splits, split_asms) = case_thms_of_term lthy [] rhs_term;
+ val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
in
- mk_primcorec_sel_tac lthy def_thms distincts splits split_asms nested_maps
+ mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
nested_map_idents nested_map_comps sel_corec k m exclsss
|> K |> Goal.prove lthy [] [] t
|> pair sel
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Fri Sep 27 09:17:25 2013 +0200
@@ -9,8 +9,8 @@
sig
val mk_primcorec_assumption_tac: Proof.context -> thm list -> tactic
val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
- thm list -> int list -> thm list -> tactic
- val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> thm list -> tactic
+ int list -> thm list -> tactic
+ val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> tactic
val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
tactic
@@ -40,16 +40,18 @@
fun mk_primcorec_assumption_tac ctxt discIs =
HEADGOAL (SELECT_GOAL (unfold_thms_tac ctxt
@{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
- SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE'
+ SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
- dresolve_tac discIs THEN' atac)))));
+ dresolve_tac discIs THEN' atac ORELSE'
+ etac notE THEN' atac ORELSE'
+ etac disjE)))));
fun mk_primcorec_same_case_tac m =
HEADGOAL (if m = 0 then rtac TrueI
else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
fun mk_primcorec_different_case_tac ctxt excl =
- unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN
+ unfold_thms_tac ctxt @{thms not_not not_False_eq_True not_True_eq_False} THEN
HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_assumption_tac ctxt []));
fun mk_primcorec_cases_tac ctxt k m exclsss =
@@ -83,33 +85,32 @@
(the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
-(* TODO: do we need "collapses"? *)
(* TODO: reduce code duplication with selector tactic above *)
-fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
+fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN
- HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o
+ HEADGOAL (SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'
- eresolve_tac (falseEs @ map (fn thm => thm RS trans) collapses) ORELSE'
resolve_tac split_connectI ORELSE'
Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
Splitter.split_tac (split_if :: splits) ORELSE'
+ K (mk_primcorec_assumption_tac ctxt discIs) ORELSE'
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
- (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))));
+ (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))));
-fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs collapses splits split_asms ms ctr_thms =
- EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits
- split_asms) ms ctr_thms);
+fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms =
+ EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
+ ms ctr_thms);
-fun mk_primcorec_code_of_raw_tac splits disc_excludes raw collapses =
+fun mk_primcorec_code_of_raw_tac splits disc_excludes raw =
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o
(rtac refl ORELSE'
(TRY o rtac sym) THEN' atac ORELSE'
resolve_tac split_connectI ORELSE'
Splitter.split_tac (split_if :: splits) ORELSE'
etac notE THEN' atac ORELSE'
- dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE'
- eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
+ (TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac));
+
end;
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Fri Sep 27 09:17:25 2013 +0200
@@ -70,7 +70,7 @@
val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
typ list -> term -> 'a -> 'a
val case_thms_of_term: Proof.context -> typ list -> term ->
- thm list * thm list * thm list * thm list * thm list
+ thm list * thm list * thm list * thm list
val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
((term * term list list) list) list -> local_theory ->
@@ -234,7 +234,7 @@
o fld (conds @ s_not_disj cond) else_branch
| (Const (c, _), args as _ :: _ :: _) =>
let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
- if length args > n then
+ if n >= 0 andalso n < length args then
(case fastype_of1 (bound_Ts, nth args n) of
Type (s, Ts) =>
(case dest_case ctxt s Ts t of
@@ -276,7 +276,7 @@
val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T;
val n = length gen_branch_Ts;
in
- if length args > n then
+ if n < length args then
(case gen_body_fun_T of
Type (_, [Type (T_name, _), _]) =>
if case_of ctxt T_name = SOME c then
@@ -397,8 +397,8 @@
val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
in
- (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #collapses ctr_sugars,
- map #split ctr_sugars, map #split_asm ctr_sugars)
+ (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
+ maps #sel_split_asms ctr_sugars)
end;
fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
--- a/src/HOL/Fun.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/Fun.thy Fri Sep 27 09:17:25 2013 +0200
@@ -491,8 +491,11 @@
apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
done
+lemma inj_on_image_eq_iff: "\<lbrakk> inj_on f C; A \<subseteq> C; B \<subseteq> C \<rbrakk> \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
+by(fastforce simp add: inj_on_def)
+
lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
-by(blast dest: inj_onD)
+by(erule inj_on_image_eq_iff) simp_all
lemma inj_on_image_Int:
"[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B"
--- a/src/HOL/Library/Inner_Product.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/Library/Inner_Product.thy Fri Sep 27 09:17:25 2013 +0200
@@ -114,6 +114,9 @@
by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
qed
+lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
+ using Cauchy_Schwarz_ineq2 [of x y] by auto
+
subclass real_normed_vector
proof
fix a :: real and x y :: 'a
@@ -122,7 +125,7 @@
show "norm (x + y) \<le> norm x + norm y"
proof (rule power2_le_imp_le)
have "inner x y \<le> norm x * norm y"
- by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
+ by (rule norm_cauchy_schwarz)
thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
unfolding power2_sum power2_norm_eq_inner
by (simp add: inner_add inner_commute)
--- a/src/HOL/Library/Product_Vector.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/Library/Product_Vector.thy Fri Sep 27 09:17:25 2013 +0200
@@ -231,12 +231,7 @@
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
by (simp add: prod_eq_iff)
thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
- apply (rule disjE)
- apply (drule t0_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
- apply (simp add: open_Times mem_Times_iff)
- apply (drule t0_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
- apply (simp add: open_Times mem_Times_iff)
- done
+ by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
qed
instance prod :: (t1_space, t1_space) t1_space
@@ -245,12 +240,7 @@
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
by (simp add: prod_eq_iff)
thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
- apply (rule disjE)
- apply (drule t1_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
- apply (simp add: open_Times mem_Times_iff)
- apply (drule t1_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
- apply (simp add: open_Times mem_Times_iff)
- done
+ by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
qed
instance prod :: (t2_space, t2_space) t2_space
@@ -259,14 +249,7 @@
hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
by (simp add: prod_eq_iff)
thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
- apply (rule disjE)
- apply (drule hausdorff, clarify)
- apply (rule_tac x="U \<times> UNIV" in exI, rule_tac x="V \<times> UNIV" in exI)
- apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
- apply (drule hausdorff, clarify)
- apply (rule_tac x="UNIV \<times> U" in exI, rule_tac x="UNIV \<times> V" in exI)
- apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
- done
+ by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
qed
subsection {* Product is a metric space *}
@@ -281,10 +264,10 @@
unfolding dist_prod_def by simp
lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
-unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
+ unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1)
lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
-unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
+ unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
instance proof
fix x y :: "'a \<times> 'b"
@@ -362,10 +345,10 @@
end
lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
-unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
+ unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))"
-unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
+ unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
lemma Cauchy_Pair:
assumes "Cauchy X" and "Cauchy Y"
--- a/src/HOL/Lifting.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/Lifting.thy Fri Sep 27 09:17:25 2013 +0200
@@ -38,9 +38,21 @@
obtains "(\<And>x. \<exists>y. R x y)"
using assms unfolding left_total_def by blast
+lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
+by(simp add: left_total_def right_total_def bi_total_def)
+
definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
+by(auto simp add: left_unique_def right_unique_def bi_unique_def)
+
+lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
+unfolding left_unique_def by blast
+
+lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
+unfolding left_unique_def by blast
+
lemma left_total_fun:
"\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
unfolding left_total_def fun_rel_def
--- a/src/HOL/Lifting_Set.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/Lifting_Set.thy Fri Sep 27 09:17:25 2013 +0200
@@ -19,6 +19,10 @@
shows "set_rel R A B"
using assms unfolding set_rel_def by simp
+lemma set_relD1: "\<lbrakk> set_rel R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
+ and set_relD2: "\<lbrakk> set_rel R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
+by(simp_all add: set_rel_def)
+
lemma set_rel_conversep: "set_rel (conversep R) = conversep (set_rel R)"
unfolding set_rel_def by auto
@@ -153,6 +157,15 @@
set_rel set_rel"
unfolding fun_rel_def set_rel_def by fast
+lemma SUPR_parametric [transfer_rule]:
+ "(set_rel R ===> (R ===> op =) ===> op =) SUPR SUPR"
+proof(rule fun_relI)+
+ fix A B f and g :: "'b \<Rightarrow> 'c"
+ assume AB: "set_rel R A B"
+ and fg: "(R ===> op =) f g"
+ show "SUPR A f = SUPR B g"
+ by(rule SUPR_eq)(auto 4 4 dest: set_relD1[OF AB] set_relD2[OF AB] fun_relD[OF fg] intro: rev_bexI)
+qed
subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
@@ -268,6 +281,47 @@
"bi_unique A \<Longrightarrow> (set_rel A ===> op =) card card"
by (rule fun_relI, erule (1) bi_unique_set_rel_lemma, simp add: card_image)
+lemma vimage_parametric [transfer_rule]:
+ assumes [transfer_rule]: "bi_total A" "bi_unique B"
+ shows "((A ===> B) ===> set_rel B ===> set_rel A) vimage vimage"
+unfolding vimage_def[abs_def] by transfer_prover
+
+lemma setsum_parametric [transfer_rule]:
+ assumes "bi_unique A"
+ shows "((A ===> op =) ===> set_rel A ===> op =) setsum setsum"
+proof(rule fun_relI)+
+ fix f :: "'a \<Rightarrow> 'c" and g S T
+ assume fg: "(A ===> op =) f g"
+ and ST: "set_rel A S T"
+ show "setsum f S = setsum g T"
+ proof(rule setsum_reindex_cong)
+ let ?f = "\<lambda>t. THE s. A s t"
+ show "S = ?f ` T"
+ by(blast dest: set_relD1[OF ST] set_relD2[OF ST] bi_uniqueDl[OF assms]
+ intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
+
+ show "inj_on ?f T"
+ proof(rule inj_onI)
+ fix t1 t2
+ assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
+ from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: set_relD2)
+ hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
+ moreover
+ from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: set_relD2)
+ hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
+ ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
+ with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
+ qed
+
+ fix t
+ assume "t \<in> T"
+ with ST obtain s where "A s t" "s \<in> S" by(auto dest: set_relD2)
+ hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
+ moreover from fg `A s t` have "f s = g t" by(rule fun_relD)
+ ultimately show "g t = f (?f t)" by simp
+ qed
+qed
+
end
end
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Sep 27 09:17:25 2013 +0200
@@ -106,7 +106,7 @@
from `0 < e` have "y \<noteq> x"
unfolding y_def by (auto intro!: nonzero_Basis)
from `0 < e` have "dist y x < e"
- unfolding y_def by (simp add: dist_norm norm_Basis)
+ unfolding y_def by (simp add: dist_norm)
from `y \<noteq> x` and `dist y x < e` show "False"
using e by simp
qed
@@ -123,7 +123,7 @@
[simp]: "Basis = {1::real}"
instance
- by default (auto simp add: Basis_real_def)
+ by default auto
end
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Sep 27 09:17:25 2013 +0200
@@ -69,10 +69,6 @@
lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
by simp (* TODO: delete *)
-lemma norm_cauchy_schwarz: "x \<bullet> y \<le> norm x * norm y"
- (* TODO: move to Inner_Product.thy *)
- using Cauchy_Schwarz_ineq2[of x y] by auto
-
lemma norm_triangle_sub:
fixes x y :: "'a::real_normed_vector"
shows "norm x \<le> norm y + norm (x - y)"
@@ -197,7 +193,7 @@
lemma setsum_group:
assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
- shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S"
+ shows "setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) T = setsum g S"
apply (subst setsum_image_gen[OF fS, of g f])
apply (rule setsum_mono_zero_right[OF fT fST])
apply (auto intro: setsum_0')
@@ -479,7 +475,7 @@
assumes lf: "linear f"
shows "linear (adjoint f)"
by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
- adjoint_clauses[OF lf] inner_simps)
+ adjoint_clauses[OF lf] inner_distrib)
lemma adjoint_adjoint:
fixes f:: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
@@ -1509,13 +1505,9 @@
apply (simp add: inner_Basis inner_setsum_right eq_commute)
done
-lemma span_Basis[simp]: "span Basis = (UNIV :: 'a::euclidean_space set)"
- apply (subst span_finite)
- apply simp
- apply (safe intro!: UNIV_I)
- apply (rule_tac x="inner x" in exI)
- apply (simp add: euclidean_representation)
- done
+lemma span_Basis [simp]: "span Basis = UNIV"
+ unfolding span_finite [OF finite_Basis]
+ by (fast intro: euclidean_representation)
lemma in_span_Basis: "x \<in> span Basis"
unfolding span_Basis ..
@@ -1570,70 +1562,33 @@
fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
-proof -
+proof
let ?B = "\<Sum>b\<in>Basis. norm (f b)"
- {
+ show "\<forall>x. norm (f x) \<le> ?B * norm x"
+ proof
fix x :: 'a
let ?g = "\<lambda>b. (x \<bullet> b) *\<^sub>R f b"
have "norm (f x) = norm (f (\<Sum>b\<in>Basis. (x \<bullet> b) *\<^sub>R b))"
unfolding euclidean_representation ..
also have "\<dots> = norm (setsum ?g Basis)"
- using linear_setsum[OF lf finite_Basis, of "\<lambda>b. (x \<bullet> b) *\<^sub>R b", unfolded o_def] linear_cmul[OF lf]
- by auto
+ by (simp add: linear_setsum [OF lf] linear_cmul [OF lf])
finally have th0: "norm (f x) = norm (setsum ?g Basis)" .
- {
+ have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
+ proof
fix i :: 'a
assume i: "i \<in> Basis"
from Basis_le_norm[OF i, of x]
- have "norm (?g i) \<le> norm (f i) * norm x"
+ show "norm (?g i) \<le> norm (f i) * norm x"
unfolding norm_scaleR
apply (subst mult_commute)
apply (rule mult_mono)
apply (auto simp add: field_simps)
done
- }
- then have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
- by metis
+ qed
from setsum_norm_le[of _ ?g, OF th]
- have "norm (f x) \<le> ?B * norm x"
+ show "norm (f x) \<le> ?B * norm x"
unfolding th0 setsum_left_distrib by metis
- }
- then show ?thesis by blast
-qed
-
-lemma linear_bounded_pos:
- fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
- assumes lf: "linear f"
- shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
-proof -
- from linear_bounded[OF lf] obtain B where
- B: "\<forall>x. norm (f x) \<le> B * norm x" by blast
- let ?K = "\<bar>B\<bar> + 1"
- have Kp: "?K > 0" by arith
- {
- assume C: "B < 0"
- def One \<equiv> "\<Sum>Basis ::'a"
- then have "One \<noteq> 0"
- unfolding euclidean_eq_iff[where 'a='a]
- by (simp add: inner_setsum_left inner_Basis setsum_cases)
- then have "norm One > 0" by auto
- with C have "B * norm One < 0"
- by (simp add: mult_less_0_iff)
- with B[rule_format, of One] norm_ge_zero[of "f One"]
- have False by simp
- }
- then have Bp: "B \<ge> 0"
- by (metis not_leE)
- {
- fix x::"'a"
- have "norm (f x) \<le> ?K * norm x"
- using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
- apply (auto simp add: field_simps split add: abs_split)
- apply (erule order_trans, simp)
- done
- }
- then show ?thesis
- using Kp by blast
+ qed
qed
lemma linear_conv_bounded_linear:
@@ -1641,16 +1596,9 @@
shows "linear f \<longleftrightarrow> bounded_linear f"
proof
assume "linear f"
+ then interpret f: linear f .
show "bounded_linear f"
proof
- fix x y
- show "f (x + y) = f x + f y"
- using `linear f` unfolding linear_iff by simp
- next
- fix r x
- show "f (scaleR r x) = scaleR r (f x)"
- using `linear f` unfolding linear_iff by simp
- next
have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
using `linear f` by (rule linear_bounded)
then show "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
@@ -1659,7 +1607,19 @@
next
assume "bounded_linear f"
then interpret f: bounded_linear f .
- show "linear f" by (simp add: f.add f.scaleR linear_iff)
+ show "linear f" ..
+qed
+
+lemma linear_bounded_pos:
+ fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+ assumes lf: "linear f"
+ shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
+proof -
+ have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
+ using lf unfolding linear_conv_bounded_linear
+ by (rule bounded_linear.pos_bounded)
+ then show ?thesis
+ by (simp only: mult_commute)
qed
lemma bounded_linearI':
@@ -1698,30 +1658,6 @@
done
qed
-lemma bilinear_bounded_pos:
- fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
- assumes bh: "bilinear h"
- shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
-proof -
- from bilinear_bounded[OF bh] obtain B where
- B: "\<forall>x y. norm (h x y) \<le> B * norm x * norm y" by blast
- let ?K = "\<bar>B\<bar> + 1"
- have Kp: "?K > 0" by arith
- have KB: "B < ?K" by arith
- {
- fix x :: 'a
- fix y :: 'b
- from KB Kp have "B * norm x * norm y \<le> ?K * norm x * norm y"
- apply -
- apply (rule mult_right_mono, rule mult_right_mono)
- apply auto
- done
- then have "norm (h x y) \<le> ?K * norm x * norm y"
- using B[rule_format, of x y] by simp
- }
- with Kp show ?thesis by blast
-qed
-
lemma bilinear_conv_bounded_bilinear:
fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
@@ -1760,6 +1696,18 @@
using h.bounded_linear_left h.bounded_linear_right by simp
qed
+lemma bilinear_bounded_pos:
+ fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
+ assumes bh: "bilinear h"
+ shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
+proof -
+ have "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> norm x * norm y * B"
+ using bh [unfolded bilinear_conv_bounded_bilinear]
+ by (rule bounded_bilinear.pos_bounded)
+ then show ?thesis
+ by (simp only: mult_ac)
+qed
+
subsection {* We continue. *}
--- a/src/HOL/ROOT Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/ROOT Fri Sep 27 09:17:25 2013 +0200
@@ -560,6 +560,7 @@
IArray_Examples
SVC_Oracle
Simps_Case_Conv_Examples
+ ML
theories [skip_proofs = false]
Meson_Test
theories [condition = SVC_HOME]
--- a/src/HOL/Transfer.thy Thu Sep 26 16:52:24 2013 +0200
+++ b/src/HOL/Transfer.thy Fri Sep 27 09:17:25 2013 +0200
@@ -158,6 +158,18 @@
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
+by(simp add: bi_unique_def)
+
+lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
+by(simp add: bi_unique_def)
+
+lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
+unfolding right_unique_def by blast
+
+lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
+unfolding right_unique_def by blast
+
lemma right_total_alt_def:
"right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
unfolding right_total_def fun_rel_def
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/ML.thy Fri Sep 27 09:17:25 2013 +0200
@@ -0,0 +1,136 @@
+(* Title: HOL/ex/ML.thy
+ Author: Makarius
+*)
+
+header {* Isabelle/ML basics *}
+
+theory "ML"
+imports Main
+begin
+
+section {* ML expressions *}
+
+text {*
+ The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal
+ text. It is type-checked, compiled, and run within that environment.
+
+ Note that side-effects should be avoided, unless the intention is to change
+ global parameters of the run-time environment (rare).
+
+ ML top-level bindings are managed within the theory context.
+*}
+
+ML {* 1 + 1 *}
+
+ML {* val a = 1 *}
+ML {* val b = 1 *}
+ML {* val c = a + b *}
+
+
+section {* Antiquotations *}
+
+text {* There are some language extensions (via antiquotations), as explained in
+ the "Isabelle/Isar implementation manual", chapter 0. *}
+
+ML {* length [] *}
+ML {* @{assert} (length [] = 0) *}
+
+
+text {* Formal entities from the surrounding context may be referenced as
+ follows: *}
+
+term "1 + 1" -- "term within theory source"
+
+ML {*
+ @{term "1 + 1"} (* term as symbolic ML datatype value *)
+*}
+
+ML {*
+ @{term "1 + (1::int)"}
+*}
+
+
+section {* IDE support *}
+
+text {*
+ ML embedded into the Isabelle environment is connected to the Prover IDE.
+ Poly/ML provides:
+ \<bullet> precise positions for warnings / errors
+ \<bullet> markup for defining positions of identifiers
+ \<bullet> markup for inferred types of sub-expressions
+*}
+
+ML {* fn i => fn list => length list + i *}
+
+
+section {* Example: factorial and ackermann function in Isabelle/ML *}
+
+ML {*
+ fun factorial 0 = 1
+ | factorial n = n * factorial (n - 1)
+*}
+
+ML "factorial 42"
+ML "factorial 10000 div factorial 9999"
+
+text {*
+ See http://mathworld.wolfram.com/AckermannFunction.html
+*}
+
+ML {*
+ fun ackermann 0 n = n + 1
+ | ackermann m 0 = ackermann (m - 1) 1
+ | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
+*}
+
+ML {* timeit (fn () => ackermann 3 10) *}
+
+
+section {* Parallel Isabelle/ML *}
+
+text {*
+ Future.fork/join/cancel manage parallel evaluation.
+
+ Note that within Isabelle theory documents, the top-level command boundary may
+ not be transgressed without special precautions. This is normally managed by
+ the system when performing parallel proof checking. *}
+
+ML {*
+ val x = Future.fork (fn () => ackermann 3 10);
+ val y = Future.fork (fn () => ackermann 3 10);
+ val z = Future.join x + Future.join y
+*}
+
+text {*
+ The @{ML_struct Par_List} module provides high-level combinators for
+ parallel list operations. *}
+
+ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
+ML {* timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10)) *}
+
+
+section {* Function specifications in Isabelle/HOL *}
+
+fun factorial :: "nat \<Rightarrow> nat"
+where
+ "factorial 0 = 1"
+| "factorial (Suc n) = Suc n * factorial n"
+
+term "factorial 4" -- "symbolic term"
+value "factorial 4" -- "evaluation via ML code generation in the background"
+
+declare [[ML_trace]]
+ML {* @{term "factorial 4"} *} -- "symbolic term in ML"
+ML {* @{code "factorial"} *} -- "ML code from function specification"
+
+
+fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "ackermann 0 n = n + 1"
+| "ackermann (Suc m) 0 = ackermann m 1"
+| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
+
+value "ackermann 3 5"
+
+end
+
--- a/src/Pure/Tools/doc.scala Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Pure/Tools/doc.scala Fri Sep 27 09:17:25 2013 +0200
@@ -59,6 +59,7 @@
val names =
List(
"src/HOL/ex/Seq.thy",
+ "src/HOL/ex/ML.thy",
"src/HOL/Unix/Unix.thy",
"src/HOL/Isar_Examples/Drinker.thy")
Section("Examples") :: names.map(name => text_file(name).get)
--- a/src/Pure/Tools/main.scala Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Pure/Tools/main.scala Fri Sep 27 09:17:25 2013 +0200
@@ -7,7 +7,7 @@
package isabelle
-import java.lang.{System, ClassLoader}
+import java.lang.{System, Class, ClassLoader}
import java.io.{File => JFile, BufferedReader, InputStreamReader}
import java.nio.file.Files
@@ -116,7 +116,8 @@
System.setProperty("scala.home",
Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
- val jedit = ClassLoader.getSystemClassLoader.loadClass("org.gjt.sp.jedit.jEdit")
+ val jedit =
+ Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
() => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
--- a/src/Tools/jEdit/etc/options Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/etc/options Fri Sep 27 09:17:25 2013 +0200
@@ -30,12 +30,6 @@
public option jedit_symbols_search_limit : int = 50
-- "maximum number of symbols in search result"
-option jedit_macos_application : bool = false
- -- "some native Mac OS X application support (potential conflict with MacOSX plugin)"
-
-option jedit_macos_preferences : bool = false
- -- "native Mac OS X preferences menu"
-
public option jedit_timing_threshold : real = 0.1
-- "default threshold for timing display"
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Sep 27 09:17:25 2013 +0200
@@ -28,7 +28,6 @@
"src/jedit_options.scala"
"src/jedit_thy_load.scala"
"src/monitor_dockable.scala"
- "src/osx_adapter.scala"
"src/output_dockable.scala"
"src/plugin.scala"
"src/pretty_text_area.scala"
--- a/src/Tools/jEdit/patches/brackets Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/patches/brackets Fri Sep 27 09:17:25 2013 +0200
@@ -1,3 +1,17 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2013-07-28 19:03:32.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2013-09-26 16:09:50.131780476 +0200
+@@ -1610,8 +1615,8 @@
+ }
+
+ // Scan backwards, trying to find a bracket
+- String openBrackets = "([{";
+- String closeBrackets = ")]}";
++ String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
++ String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄'";
+ int count = 1;
+ char openBracket = '\0';
+ char closeBracket = '\0';
diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
--- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2013-07-28 19:03:24.000000000 +0200
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-09-05 10:51:09.996193290 +0200
--- a/src/Tools/jEdit/src/jEdit.props Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Fri Sep 27 09:17:25 2013 +0200
@@ -1,4 +1,5 @@
#jEdit properties
+action-bar.shortcut=C+ENTER
buffer.deepIndent=false
buffer.encoding=UTF-8-Isabelle
buffer.indentSize=2
--- a/src/Tools/jEdit/src/modes/isabelle-news.xml Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-news.xml Fri Sep 27 09:17:25 2013 +0200
@@ -5,8 +5,8 @@
<MODE>
<PROPS>
<PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml Fri Sep 27 09:17:25 2013 +0200
@@ -4,9 +4,11 @@
<!-- Isabelle options mode -->
<MODE>
<PROPS>
+ <PROPERTY NAME="commentStart" VALUE="(*"/>
+ <PROPERTY NAME="commentEnd" VALUE="*)"/>
<PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml Fri Sep 27 09:17:25 2013 +0200
@@ -4,9 +4,11 @@
<!-- Isabelle session root mode -->
<MODE>
<PROPS>
+ <PROPERTY NAME="commentStart" VALUE="(*"/>
+ <PROPERTY NAME="commentEnd" VALUE="*)"/>
<PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
--- a/src/Tools/jEdit/src/modes/isabelle.xml Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle.xml Fri Sep 27 09:17:25 2013 +0200
@@ -7,27 +7,9 @@
<PROPERTY NAME="commentStart" VALUE="(*"/>
<PROPERTY NAME="commentEnd" VALUE="*)"/>
<PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
- <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
- <SPAN TYPE="COMMENT1">
- <BEGIN>(*</BEGIN>
- <END>*)</END>
- </SPAN>
- <SPAN TYPE="COMMENT3">
- <BEGIN>{*</BEGIN>
- <END>*}</END>
- </SPAN>
- <SPAN TYPE="LITERAL1">
- <BEGIN>`</BEGIN>
- <END>`</END>
- </SPAN>
- <SPAN TYPE="LITERAL3">
- <BEGIN>"</BEGIN>
- <END>"</END>
- </SPAN>
- </RULES>
</MODE>
--- a/src/Tools/jEdit/src/osx_adapter.scala Thu Sep 26 16:52:24 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-/* Title: Tools/jEdit/src/osx_adapter.scala
- Author: Makarius
-
-Some native OS X support.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.lang.{Class, ClassNotFoundException, NoSuchMethodException}
-import java.lang.reflect.{InvocationHandler, Method, Proxy}
-
-
-object OSX_Adapter
-{
- private lazy val application_class: Class[_] = Class.forName("com.apple.eawt.Application")
- private lazy val application = application_class.getConstructor().newInstance()
-
- def init
- {
- if (PIDE.options.bool("jedit_macos_application")) {
- try {
- set_handler("handleQuit")
- set_handler("handleAbout")
-
- if (PIDE.options.bool("jedit_macos_preferences")) {
- application_class.getDeclaredMethod("setEnabledPreferencesMenu", classOf[Boolean]).
- invoke(application, java.lang.Boolean.valueOf(true))
- set_handler("handlePreferences")
- }
- }
- catch {
- case exn: ClassNotFoundException =>
- java.lang.System.err.println(
- "com.apple.eawt.Application unavailable -- cannot install native OS X handler")
- }
- }
- }
-
- private def set_handler(name: String)
- {
- val handler = PIDE.plugin.getClass.getDeclaredMethod(name)
- val adapter = new OSX_Adapter(name, PIDE.plugin, handler)
- try {
- val application_listener_class: Class[_] =
- Class.forName("com.apple.eawt.ApplicationListener")
- val add_listener_method =
- application_class.getDeclaredMethod("addApplicationListener", application_listener_class)
-
- val osx_adapter_proxy =
- Proxy.newProxyInstance(classOf[OSX_Adapter].getClassLoader,
- Array(application_listener_class), adapter)
- add_listener_method.invoke(application, osx_adapter_proxy)
- }
- catch {
- case exn: ClassNotFoundException =>
- java.lang.System.err.println(
- "com.apple.eawt.Application unavailable -- cannot install native OS X handler")
- }
- }
-}
-
-class OSX_Adapter(proxy_signature: String, target_object: AnyRef, target_method: Method)
- extends InvocationHandler
-{
- override def invoke(proxy: Any, method: Method, args: Array[AnyRef]): AnyRef =
- {
- if (proxy_signature == method.getName && args.length == 1) {
- val result = target_method.invoke(target_object)
- val handled = result == null || result.toString == "true"
-
- val event = args(0)
- if (event != null) {
- try {
- val set_handled_method =
- event.getClass.getDeclaredMethod("setHandled", classOf[java.lang.Boolean])
- set_handled_method.invoke(event, java.lang.Boolean.valueOf(handled))
- }
- catch { case _: NoSuchMethodException => }
- }
- }
- null
- }
-}
-
--- a/src/Tools/jEdit/src/plugin.scala Thu Sep 26 16:52:24 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Fri Sep 27 09:17:25 2013 +0200
@@ -325,8 +325,6 @@
PIDE.options.update(Options.init())
PIDE.completion_history.load()
- // FIXME if (Platform.is_macos) OSX_Adapter.init
-
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
if (ModeProvider.instance.isInstanceOf[ModeProvider])
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)