--- a/NEWS Tue May 24 13:57:34 2016 +0100
+++ b/NEWS Tue May 24 15:08:07 2016 +0100
@@ -9,6 +9,10 @@
*** General ***
+* Embedded content (e.g. the inner syntax of types, terms, props) may be
+delimited uniformly via cartouches. This works better than old-fashioned
+quotes when sub-languages are nested.
+
* Type-inference improves sorts of newly introduced type variables for
the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
@@ -95,6 +99,9 @@
has been removed for output. It is retained for input only, until it is
eliminated altogether.
+* Sledgehammer:
+ - Produce syntactically correct Vampire 4.0 problem files.
+
* (Co)datatype package:
- New commands for defining corecursive functions and reasoning about
them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
@@ -196,6 +203,8 @@
pave way for a possible future different type class instantiation
for polynomials over factorial rings. INCOMPATIBILITY.
+* Library/Sublist.thy: renamed prefixeq -> prefix and prefix -> strict_prefix
+
* Dropped various legacy fact bindings, whose replacements are often
of a more general type also:
lcm_left_commute_nat ~> lcm.left_commute
--- a/src/CCL/CCL.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/CCL/CCL.thy Tue May 24 15:08:07 2016 +0100
@@ -474,7 +474,7 @@
done
method_setup eq_coinduct3 = \<open>
- Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
+ Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD'
(Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
\<close>
--- a/src/CCL/Wfd.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/CCL/Wfd.thy Tue May 24 15:08:07 2016 +0100
@@ -47,7 +47,7 @@
done
method_setup wfd_strengthen = \<open>
- Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
+ Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD' (fn i =>
Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i
THEN assume_tac ctxt (i + 1)))
--- a/src/CTT/CTT.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/CTT/CTT.thy Tue May 24 15:08:07 2016 +0100
@@ -449,7 +449,7 @@
method_setup eqintr = \<open>Scan.succeed (SIMPLE_METHOD o eqintr_tac)\<close>
method_setup NE = \<open>
- Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
+ Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
\<close>
method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close>
method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close>
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Tue May 24 15:08:07 2016 +0100
@@ -177,8 +177,8 @@
@@{antiquotation const} options @{syntax term} |
@@{antiquotation abbrev} options @{syntax term} |
@@{antiquotation typ} options @{syntax type} |
- @@{antiquotation type} options @{syntax name} |
- @@{antiquotation class} options @{syntax name} |
+ @@{antiquotation type} options @{syntax embedded} |
+ @@{antiquotation class} options @{syntax embedded} |
(@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
options @{syntax name}
;
@@ -197,7 +197,7 @@
@@{antiquotation verbatim} options @{syntax text} |
@@{antiquotation "file"} options @{syntax name} |
@@{antiquotation file_unchecked} options @{syntax name} |
- @@{antiquotation url} options @{syntax name} |
+ @@{antiquotation url} options @{syntax embedded} |
@@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
;
styles: '(' (style + ',') ')'
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Tue May 24 15:08:07 2016 +0100
@@ -184,7 +184,7 @@
@{rail \<open>
@{syntax_def name}: @{syntax ident} | @{syntax longident} |
- @{syntax symident} | @{syntax string} | @{syntax nat}
+ @{syntax symident} | @{syntax nat} | @{syntax string}
;
@{syntax_def par_name}: '(' @{syntax name} ')'
\<close>}
@@ -209,6 +209,24 @@
\<close>
+subsection \<open>Embedded content\<close>
+
+text \<open>
+ Entity @{syntax embedded} refers to content of other languages: cartouches
+ allow arbitrary nesting of sub-languages that respect the recursive
+ balancing of cartouche delimiters. Quoted strings are possible as well, but
+ require escaped quotes when nested. As a shortcut, tokens that appear as
+ plain identifiers in the outer language may be used as inner language
+ content without delimiters.
+
+ @{rail \<open>
+ @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
+ @{syntax ident} | @{syntax longident} | @{syntax symident} |
+ @{syntax nat}
+ \<close>}
+\<close>
+
+
subsection \<open>Comments \label{sec:comments}\<close>
text \<open>
@@ -260,10 +278,10 @@
as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
@{rail \<open>
- @{syntax_def type}: @{syntax name} | @{syntax typefree} |
+ @{syntax_def type}: @{syntax embedded} | @{syntax typefree} |
@{syntax typevar}
;
- @{syntax_def term}: @{syntax name} | @{syntax var}
+ @{syntax_def term}: @{syntax embedded} | @{syntax var}
;
@{syntax_def prop}: @{syntax term}
\<close>}
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Tue May 24 15:08:07 2016 +0100
@@ -52,7 +52,7 @@
end
in
Thy_Output.antiquotation @{binding "const_typ"}
- (Scan.lift Args.name_inner_syntax)
+ (Scan.lift Args.embedded_inner_syntax)
(fn {source = src, context = ctxt, ...} => fn arg =>
Thy_Output.output ctxt
(Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
--- a/src/FOL/FOL.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/FOL/FOL.thy Tue May 24 15:08:07 2016 +0100
@@ -72,7 +72,7 @@
\<close>
method_setup case_tac = \<open>
- Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+ Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
\<close> "case_tac emulation (dynamic instantiation!)"
--- a/src/HOL/Eisbach/parse_tools.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Eisbach/parse_tools.ML Tue May 24 15:08:07 2016 +0100
@@ -34,7 +34,7 @@
(fn ((_, SOME t), _) => Real_Val t
| ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Term t)) tok)));
-val name_term = parse_term_val Args.name_inner_syntax;
+val name_term = parse_term_val Args.embedded_inner_syntax;
fun is_real_val (Real_Val _) = true
| is_real_val _ = false;
--- a/src/HOL/HOLCF/IOA/CompoScheds.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/HOLCF/IOA/CompoScheds.thy Tue May 24 15:08:07 2016 +0100
@@ -289,7 +289,7 @@
\<close>
method_setup mkex_induct = \<open>
- Scan.lift (Args.name -- Args.name -- Args.name)
+ Scan.lift (Args.embedded -- Args.embedded -- Args.embedded)
>> (fn ((sch, exA), exB) => fn ctxt =>
SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
\<close>
--- a/src/HOL/HOLCF/IOA/Sequence.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Tue May 24 15:08:07 2016 +0100
@@ -996,13 +996,13 @@
\<close>
method_setup Seq_case =
- \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
+ \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\<close>
method_setup Seq_case_simp =
- \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
+ \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\<close>
method_setup Seq_induct =
- \<open>Scan.lift Args.name --
+ \<open>Scan.lift Args.embedded --
Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
>> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (Seq_induct_tac ctxt s rws))\<close>
@@ -1010,10 +1010,10 @@
\<open>Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)\<close>
method_setup pair =
- \<open>Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
+ \<open>Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\<close>
method_setup pair_induct =
- \<open>Scan.lift Args.name --
+ \<open>Scan.lift Args.embedded --
Scan.optional ((Scan.lift (Args.$$$ "simp" -- Args.colon) |-- Attrib.thms)) []
>> (fn (s, rws) => fn ctxt => SIMPLE_METHOD' (pair_induct_tac ctxt s rws))\<close>
--- a/src/HOL/Library/LaTeXsugar.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Tue May 24 15:08:07 2016 +0100
@@ -105,7 +105,7 @@
end
in
Thy_Output.antiquotation @{binding "const_typ"}
- (Scan.lift Args.name_inner_syntax)
+ (Scan.lift Args.embedded_inner_syntax)
(fn {source = src, context = ctxt, ...} => fn arg =>
Thy_Output.output ctxt
(Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Tue May 24 15:08:07 2016 +0100
@@ -13,7 +13,7 @@
lemma shift_prefix:
assumes "xl @- xs = yl @- ys" and "length xl \<le> length yl"
-shows "prefixeq xl yl"
+shows "prefix xl yl"
using assms proof(induct xl arbitrary: yl xs ys)
case (Cons x xl yl xs ys)
thus ?case by (cases yl) auto
@@ -21,7 +21,7 @@
lemma shift_prefix_cases:
assumes "xl @- xs = yl @- ys"
-shows "prefixeq xl yl \<or> prefixeq yl xl"
+shows "prefix xl yl \<or> prefix yl xl"
using shift_prefix[OF assms]
by (cases "length xl \<le> length yl") (metis, metis assms nat_le_linear shift_prefix)
@@ -297,17 +297,17 @@
moreover obtain yl ys1 where xs2: "xs = yl @- ys1" and \<psi>\<psi>: "alw \<psi> ys1"
using \<psi> by (metis ev_imp_shift)
ultimately have 0: "xl @- xs1 = yl @- ys1" by auto
- hence "prefixeq xl yl \<or> prefixeq yl xl" using shift_prefix_cases by auto
+ hence "prefix xl yl \<or> prefix yl xl" using shift_prefix_cases by auto
thus ?thesis proof
- assume "prefixeq xl yl"
- then obtain yl1 where yl: "yl = xl @ yl1" by (elim prefixeqE)
+ assume "prefix xl yl"
+ then obtain yl1 where yl: "yl = xl @ yl1" by (elim prefixE)
have xs1': "xs1 = yl1 @- ys1" using 0 unfolding yl by simp
have "alw \<phi> ys1" using \<phi>\<phi> unfolding xs1' by (metis alw_shift)
hence "alw (\<phi> aand \<psi>) ys1" using \<psi>\<psi> unfolding alw_aand by auto
thus ?thesis unfolding xs2 by (auto intro: alw_ev_shift)
next
- assume "prefixeq yl xl"
- then obtain xl1 where xl: "xl = yl @ xl1" by (elim prefixeqE)
+ assume "prefix yl xl"
+ then obtain xl1 where xl: "xl = yl @ xl1" by (elim prefixE)
have ys1': "ys1 = xl1 @- xs1" using 0 unfolding xl by simp
have "alw \<psi> xs1" using \<psi>\<psi> unfolding ys1' by (metis alw_shift)
hence "alw (\<phi> aand \<psi>) xs1" using \<phi>\<phi> unfolding alw_aand by auto
--- a/src/HOL/Library/Prefix_Order.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Library/Prefix_Order.thy Tue May 24 15:08:07 2016 +0100
@@ -11,7 +11,7 @@
instantiation list :: (type) order
begin
-definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
+definition "(xs::'a list) \<le> ys \<equiv> prefix xs ys"
definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
instance
@@ -19,23 +19,26 @@
end
-lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
-lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def]
-lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def]
-lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
-lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
-lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
-lemmas Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
-lemmas prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
-lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
-lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
-lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
-lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
-lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def]
-lemmas prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
-lemmas prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
-lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def]
+lemma less_list_def': "(xs::'a list) < ys \<longleftrightarrow> strict_prefix xs ys"
+by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
+
+lemmas prefixI [intro?] = prefixI [folded less_eq_list_def]
+lemmas prefixE [elim?] = prefixE [folded less_eq_list_def]
+lemmas strict_prefixI' [intro?] = strict_prefixI' [folded less_list_def']
+lemmas strict_prefixE' [elim?] = strict_prefixE' [folded less_list_def']
+lemmas strict_prefixI [intro?] = strict_prefixI [folded less_list_def']
+lemmas strict_prefixE [elim?] = strict_prefixE [folded less_list_def']
+lemmas Nil_prefix [iff] = Nil_prefix [folded less_eq_list_def]
+lemmas prefix_Nil [simp] = prefix_Nil [folded less_eq_list_def]
+lemmas prefix_snoc [simp] = prefix_snoc [folded less_eq_list_def]
+lemmas Cons_prefix_Cons [simp] = Cons_prefix_Cons [folded less_eq_list_def]
+lemmas same_prefix_prefix [simp] = same_prefix_prefix [folded less_eq_list_def]
+lemmas same_prefix_nil [iff] = same_prefix_nil [folded less_eq_list_def]
+lemmas prefix_prefix [simp] = prefix_prefix [folded less_eq_list_def]
+lemmas prefix_Cons = prefix_Cons [folded less_eq_list_def]
+lemmas prefix_length_le = prefix_length_le [folded less_eq_list_def]
+lemmas strict_prefix_simps [simp, code] = strict_prefix_simps [folded less_list_def']
lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
- not_prefixeq_induct [folded less_eq_list_def]
+ not_prefix_induct [folded less_eq_list_def]
end
--- a/src/HOL/Library/Sublist.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Library/Sublist.thy Tue May 24 15:08:07 2016 +0100
@@ -11,103 +11,103 @@
subsection \<open>Prefix order on lists\<close>
-definition prefixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
- where "prefixeq xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
+definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "prefix xs ys \<longleftrightarrow> (\<exists>zs. ys = xs @ zs)"
-definition prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
- where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
+definition strict_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "strict_prefix xs ys \<longleftrightarrow> prefix xs ys \<and> xs \<noteq> ys"
-interpretation prefix_order: order prefixeq prefix
- by standard (auto simp: prefixeq_def prefix_def)
+interpretation prefix_order: order prefix strict_prefix
+ by standard (auto simp: prefix_def strict_prefix_def)
-interpretation prefix_bot: order_bot Nil prefixeq prefix
- by standard (simp add: prefixeq_def)
+interpretation prefix_bot: order_bot Nil prefix strict_prefix
+ by standard (simp add: prefix_def)
-lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
- unfolding prefixeq_def by blast
+lemma prefixI [intro?]: "ys = xs @ zs \<Longrightarrow> prefix xs ys"
+ unfolding prefix_def by blast
-lemma prefixeqE [elim?]:
- assumes "prefixeq xs ys"
+lemma prefixE [elim?]:
+ assumes "prefix xs ys"
obtains zs where "ys = xs @ zs"
- using assms unfolding prefixeq_def by blast
+ using assms unfolding prefix_def by blast
-lemma prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> prefix xs ys"
- unfolding prefix_def prefixeq_def by blast
+lemma strict_prefixI' [intro?]: "ys = xs @ z # zs \<Longrightarrow> strict_prefix xs ys"
+ unfolding strict_prefix_def prefix_def by blast
-lemma prefixE' [elim?]:
- assumes "prefix xs ys"
+lemma strict_prefixE' [elim?]:
+ assumes "strict_prefix xs ys"
obtains z zs where "ys = xs @ z # zs"
proof -
- from \<open>prefix xs ys\<close> obtain us where "ys = xs @ us" and "xs \<noteq> ys"
- unfolding prefix_def prefixeq_def by blast
+ from \<open>strict_prefix xs ys\<close> obtain us where "ys = xs @ us" and "xs \<noteq> ys"
+ unfolding strict_prefix_def prefix_def by blast
with that show ?thesis by (auto simp add: neq_Nil_conv)
qed
-lemma prefixI [intro?]: "prefixeq xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> prefix xs ys"
- unfolding prefix_def by blast
+lemma strict_prefixI [intro?]: "prefix xs ys \<Longrightarrow> xs \<noteq> ys \<Longrightarrow> strict_prefix xs ys"
+ unfolding strict_prefix_def by blast
-lemma prefixE [elim?]:
+lemma strict_prefixE [elim?]:
fixes xs ys :: "'a list"
- assumes "prefix xs ys"
- obtains "prefixeq xs ys" and "xs \<noteq> ys"
- using assms unfolding prefix_def by blast
+ assumes "strict_prefix xs ys"
+ obtains "prefix xs ys" and "xs \<noteq> ys"
+ using assms unfolding strict_prefix_def by blast
subsection \<open>Basic properties of prefixes\<close>
-theorem Nil_prefixeq [iff]: "prefixeq [] xs"
- by (simp add: prefixeq_def)
+theorem Nil_prefix [iff]: "prefix [] xs"
+ by (simp add: prefix_def)
-theorem prefixeq_Nil [simp]: "(prefixeq xs []) = (xs = [])"
- by (induct xs) (simp_all add: prefixeq_def)
+theorem prefix_Nil [simp]: "(prefix xs []) = (xs = [])"
+ by (induct xs) (simp_all add: prefix_def)
-lemma prefixeq_snoc [simp]: "prefixeq xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefixeq xs ys"
+lemma prefix_snoc [simp]: "prefix xs (ys @ [y]) \<longleftrightarrow> xs = ys @ [y] \<or> prefix xs ys"
proof
- assume "prefixeq xs (ys @ [y])"
+ assume "prefix xs (ys @ [y])"
then obtain zs where zs: "ys @ [y] = xs @ zs" ..
- show "xs = ys @ [y] \<or> prefixeq xs ys"
- by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs)
+ show "xs = ys @ [y] \<or> prefix xs ys"
+ by (metis append_Nil2 butlast_append butlast_snoc prefixI zs)
next
- assume "xs = ys @ [y] \<or> prefixeq xs ys"
- then show "prefixeq xs (ys @ [y])"
- by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI)
+ assume "xs = ys @ [y] \<or> prefix xs ys"
+ then show "prefix xs (ys @ [y])"
+ by (metis prefix_order.eq_iff prefix_order.order_trans prefixI)
qed
-lemma Cons_prefixeq_Cons [simp]: "prefixeq (x # xs) (y # ys) = (x = y \<and> prefixeq xs ys)"
- by (auto simp add: prefixeq_def)
+lemma Cons_prefix_Cons [simp]: "prefix (x # xs) (y # ys) = (x = y \<and> prefix xs ys)"
+ by (auto simp add: prefix_def)
-lemma prefixeq_code [code]:
- "prefixeq [] xs \<longleftrightarrow> True"
- "prefixeq (x # xs) [] \<longleftrightarrow> False"
- "prefixeq (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefixeq xs ys"
+lemma prefix_code [code]:
+ "prefix [] xs \<longleftrightarrow> True"
+ "prefix (x # xs) [] \<longleftrightarrow> False"
+ "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
by simp_all
-lemma same_prefixeq_prefixeq [simp]: "prefixeq (xs @ ys) (xs @ zs) = prefixeq ys zs"
+lemma same_prefix_prefix [simp]: "prefix (xs @ ys) (xs @ zs) = prefix ys zs"
by (induct xs) simp_all
-lemma same_prefixeq_nil [iff]: "prefixeq (xs @ ys) xs = (ys = [])"
- by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixeqI)
+lemma same_prefix_nil [iff]: "prefix (xs @ ys) xs = (ys = [])"
+ by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixI)
-lemma prefixeq_prefixeq [simp]: "prefixeq xs ys \<Longrightarrow> prefixeq xs (ys @ zs)"
- by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI)
+lemma prefix_prefix [simp]: "prefix xs ys \<Longrightarrow> prefix xs (ys @ zs)"
+ by (metis prefix_order.le_less_trans prefixI strict_prefixE strict_prefixI)
-lemma append_prefixeqD: "prefixeq (xs @ ys) zs \<Longrightarrow> prefixeq xs zs"
- by (auto simp add: prefixeq_def)
+lemma append_prefixD: "prefix (xs @ ys) zs \<Longrightarrow> prefix xs zs"
+ by (auto simp add: prefix_def)
-theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefixeq zs ys))"
- by (cases xs) (auto simp add: prefixeq_def)
+theorem prefix_Cons: "prefix xs (y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> prefix zs ys))"
+ by (cases xs) (auto simp add: prefix_def)
-theorem prefixeq_append:
- "prefixeq xs (ys @ zs) = (prefixeq xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefixeq us zs))"
+theorem prefix_append:
+ "prefix xs (ys @ zs) = (prefix xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefix us zs))"
apply (induct zs rule: rev_induct)
apply force
apply (simp del: append_assoc add: append_assoc [symmetric])
apply (metis append_eq_appendI)
done
-lemma append_one_prefixeq:
- "prefixeq xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefixeq (xs @ [ys ! length xs]) ys"
- proof (unfold prefixeq_def)
+lemma append_one_prefix:
+ "prefix xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefix (xs @ [ys ! length xs]) ys"
+ proof (unfold prefix_def)
assume a1: "\<exists>zs. ys = xs @ zs"
then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
assume a2: "length xs < length ys"
@@ -117,42 +117,42 @@
thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
qed
-theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys"
- by (auto simp add: prefixeq_def)
+theorem prefix_length_le: "prefix xs ys \<Longrightarrow> length xs \<le> length ys"
+ by (auto simp add: prefix_def)
-lemma prefixeq_same_cases:
- "prefixeq (xs\<^sub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^sub>2 ys \<Longrightarrow> prefixeq xs\<^sub>1 xs\<^sub>2 \<or> prefixeq xs\<^sub>2 xs\<^sub>1"
- unfolding prefixeq_def by (force simp: append_eq_append_conv2)
+lemma prefix_same_cases:
+ "prefix (xs\<^sub>1::'a list) ys \<Longrightarrow> prefix xs\<^sub>2 ys \<Longrightarrow> prefix xs\<^sub>1 xs\<^sub>2 \<or> prefix xs\<^sub>2 xs\<^sub>1"
+ unfolding prefix_def by (force simp: append_eq_append_conv2)
-lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys"
- by (auto simp add: prefixeq_def)
+lemma set_mono_prefix: "prefix xs ys \<Longrightarrow> set xs \<subseteq> set ys"
+ by (auto simp add: prefix_def)
-lemma take_is_prefixeq: "prefixeq (take n xs) xs"
- unfolding prefixeq_def by (metis append_take_drop_id)
+lemma take_is_prefix: "prefix (take n xs) xs"
+ unfolding prefix_def by (metis append_take_drop_id)
-lemma map_prefixeqI: "prefixeq xs ys \<Longrightarrow> prefixeq (map f xs) (map f ys)"
- by (auto simp: prefixeq_def)
+lemma map_prefixI: "prefix xs ys \<Longrightarrow> prefix (map f xs) (map f ys)"
+ by (auto simp: prefix_def)
-lemma prefixeq_length_less: "prefix xs ys \<Longrightarrow> length xs < length ys"
- by (auto simp: prefix_def prefixeq_def)
+lemma prefix_length_less: "strict_prefix xs ys \<Longrightarrow> length xs < length ys"
+ by (auto simp: strict_prefix_def prefix_def)
-lemma prefix_simps [simp, code]:
- "prefix xs [] \<longleftrightarrow> False"
- "prefix [] (x # xs) \<longleftrightarrow> True"
- "prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> prefix xs ys"
- by (simp_all add: prefix_def cong: conj_cong)
+lemma strict_prefix_simps [simp, code]:
+ "strict_prefix xs [] \<longleftrightarrow> False"
+ "strict_prefix [] (x # xs) \<longleftrightarrow> True"
+ "strict_prefix (x # xs) (y # ys) \<longleftrightarrow> x = y \<and> strict_prefix xs ys"
+ by (simp_all add: strict_prefix_def cong: conj_cong)
-lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
+lemma take_strict_prefix: "strict_prefix xs ys \<Longrightarrow> strict_prefix (take n xs) ys"
apply (induct n arbitrary: xs ys)
apply (case_tac ys; simp)
- apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
+ apply (metis prefix_order.less_trans strict_prefixI take_is_prefix)
done
-lemma not_prefixeq_cases:
- assumes pfx: "\<not> prefixeq ps ls"
+lemma not_prefix_cases:
+ assumes pfx: "\<not> prefix ps ls"
obtains
(c1) "ps \<noteq> []" and "ls = []"
- | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefixeq as xs"
+ | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\<not> prefix as xs"
| (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \<noteq> a"
proof (cases ps)
case Nil
@@ -162,13 +162,13 @@
note c = \<open>ps = a#as\<close>
show ?thesis
proof (cases ls)
- case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefixeq_nil)
+ case Nil then show ?thesis by (metis append_Nil2 pfx c1 same_prefix_nil)
next
case (Cons x xs)
show ?thesis
proof (cases "x = a")
case True
- have "\<not> prefixeq as xs" using pfx c Cons True by simp
+ have "\<not> prefix as xs" using pfx c Cons True by simp
with c Cons True show ?thesis by (rule c2)
next
case False
@@ -177,40 +177,40 @@
qed
qed
-lemma not_prefixeq_induct [consumes 1, case_names Nil Neq Eq]:
- assumes np: "\<not> prefixeq ps ls"
+lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:
+ assumes np: "\<not> prefix ps ls"
and base: "\<And>x xs. P (x#xs) []"
and r1: "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
- and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefixeq xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
+ and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefix xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
shows "P ps ls" using np
proof (induct ls arbitrary: ps)
case Nil then show ?case
- by (auto simp: neq_Nil_conv elim!: not_prefixeq_cases intro!: base)
+ by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
next
case (Cons y ys)
- then have npfx: "\<not> prefixeq ps (y # ys)" by simp
+ then have npfx: "\<not> prefix ps (y # ys)" by simp
then obtain x xs where pv: "ps = x # xs"
- by (rule not_prefixeq_cases) auto
- show ?case by (metis Cons.hyps Cons_prefixeq_Cons npfx pv r1 r2)
+ by (rule not_prefix_cases) auto
+ show ?case by (metis Cons.hyps Cons_prefix_Cons npfx pv r1 r2)
qed
subsection \<open>Parallel lists\<close>
definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "\<parallel>" 50)
- where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
+ where "(xs \<parallel> ys) = (\<not> prefix xs ys \<and> \<not> prefix ys xs)"
-lemma parallelI [intro]: "\<not> prefixeq xs ys \<Longrightarrow> \<not> prefixeq ys xs \<Longrightarrow> xs \<parallel> ys"
+lemma parallelI [intro]: "\<not> prefix xs ys \<Longrightarrow> \<not> prefix ys xs \<Longrightarrow> xs \<parallel> ys"
unfolding parallel_def by blast
lemma parallelE [elim]:
assumes "xs \<parallel> ys"
- obtains "\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs"
+ obtains "\<not> prefix xs ys \<and> \<not> prefix ys xs"
using assms unfolding parallel_def by blast
-theorem prefixeq_cases:
- obtains "prefixeq xs ys" | "prefix ys xs" | "xs \<parallel> ys"
- unfolding parallel_def prefix_def by blast
+theorem prefix_cases:
+ obtains "prefix xs ys" | "strict_prefix ys xs" | "xs \<parallel> ys"
+ unfolding parallel_def strict_prefix_def by blast
theorem parallel_decomp:
"xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
@@ -221,13 +221,13 @@
next
case (snoc x xs)
show ?case
- proof (rule prefixeq_cases)
- assume le: "prefixeq xs ys"
+ proof (rule prefix_cases)
+ assume le: "prefix xs ys"
then obtain ys' where ys: "ys = xs @ ys'" ..
show ?thesis
proof (cases ys')
assume "ys' = []"
- then show ?thesis by (metis append_Nil2 parallelE prefixeqI snoc.prems ys)
+ then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys)
next
fix c cs assume ys': "ys' = c # cs"
have "x \<noteq> c" using snoc.prems ys ys' by fastforce
@@ -235,8 +235,8 @@
using ys ys' by blast
qed
next
- assume "prefix ys xs"
- then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def)
+ assume "strict_prefix ys xs"
+ then have "prefix ys (xs @ [x])" by (simp add: strict_prefix_def)
with snoc have False by blast
then show ?thesis ..
next
@@ -252,7 +252,7 @@
lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
apply (rule parallelI)
apply (erule parallelE, erule conjE,
- induct rule: not_prefixeq_induct, simp+)+
+ induct rule: not_prefix_induct, simp+)+
done
lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"
@@ -327,14 +327,14 @@
by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI)
qed
-lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> prefixeq (rev xs) (rev ys)"
+lemma suffixeq_to_prefix [code]: "suffixeq xs ys \<longleftrightarrow> prefix (rev xs) (rev ys)"
proof
assume "suffixeq xs ys"
then obtain zs where "ys = zs @ xs" ..
then have "rev ys = rev xs @ rev zs" by simp
- then show "prefixeq (rev xs) (rev ys)" ..
+ then show "prefix (rev xs) (rev ys)" ..
next
- assume "prefixeq (rev xs) (rev ys)"
+ assume "prefix (rev xs) (rev ys)"
then obtain zs where "rev ys = rev xs @ zs" ..
then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp
then have "ys = rev zs @ xs" by simp
@@ -379,10 +379,10 @@
qed
qed
-lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefixeq x y"
+lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefix x y"
by blast
-lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefixeq y x"
+lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefix y x"
by blast
lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
@@ -395,7 +395,7 @@
by auto
lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
- by (metis Cons_prefixeq_Cons parallelE parallelI)
+ by (metis Cons_prefix_Cons parallelE parallelI)
lemma not_equal_is_parallel:
assumes neq: "xs \<noteq> ys"
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue May 24 15:08:07 2016 +0100
@@ -19,7 +19,7 @@
section \<open>Results connected with topological dimension.\<close>
theory Brouwer_Fixpoint
-imports Path_Connected
+imports Path_Connected Homeomorphism
begin
lemma bij_betw_singleton_eq:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue May 24 15:08:07 2016 +0100
@@ -5297,500 +5297,6 @@
done
-subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
-
-lemma compact_frontier_line_lemma:
- fixes s :: "'a::euclidean_space set"
- assumes "compact s"
- and "0 \<in> s"
- and "x \<noteq> 0"
- obtains u where "0 \<le> u" and "(u *\<^sub>R x) \<in> frontier s" "\<forall>v>u. (v *\<^sub>R x) \<notin> s"
-proof -
- obtain b where b: "b > 0" "\<forall>x\<in>s. norm x \<le> b"
- using compact_imp_bounded[OF assms(1), unfolded bounded_pos] by auto
- let ?A = "{y. \<exists>u. 0 \<le> u \<and> u \<le> b / norm(x) \<and> (y = u *\<^sub>R x)}"
- have A: "?A = (\<lambda>u. u *\<^sub>R x) ` {0 .. b / norm x}"
- by auto
- have *: "\<And>x A B. x\<in>A \<Longrightarrow> x\<in>B \<Longrightarrow> A\<inter>B \<noteq> {}" by blast
- have "compact ?A"
- unfolding A
- apply (rule compact_continuous_image)
- apply (rule continuous_at_imp_continuous_on)
- apply rule
- apply (intro continuous_intros)
- apply (rule compact_Icc)
- done
- moreover have "{y. \<exists>u\<ge>0. u \<le> b / norm x \<and> y = u *\<^sub>R x} \<inter> s \<noteq> {}"
- apply(rule *[OF _ assms(2)])
- unfolding mem_Collect_eq
- using \<open>b > 0\<close> assms(3)
- apply auto
- done
- ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
- "y \<in> ?A" "y \<in> s" "\<forall>z\<in>?A \<inter> s. dist 0 z \<le> dist 0 y"
- using distance_attains_sup[OF compact_Int[OF _ assms(1), of ?A], of 0] by blast
- have "norm x > 0"
- using assms(3)[unfolded zero_less_norm_iff[symmetric]] by auto
- {
- fix v
- assume as: "v > u" "v *\<^sub>R x \<in> s"
- then have "v \<le> b / norm x"
- using b(2)[rule_format, OF as(2)]
- using \<open>u\<ge>0\<close>
- unfolding pos_le_divide_eq[OF \<open>norm x > 0\<close>]
- by auto
- then have "norm (v *\<^sub>R x) \<le> norm y"
- apply (rule_tac obt(6)[rule_format, unfolded dist_0_norm])
- apply (rule IntI)
- defer
- apply (rule as(2))
- unfolding mem_Collect_eq
- apply (rule_tac x=v in exI)
- using as(1) \<open>u\<ge>0\<close>
- apply (auto simp add: field_simps)
- done
- then have False
- unfolding obt(3) using \<open>u\<ge>0\<close> \<open>norm x > 0\<close> \<open>v > u\<close>
- by (auto simp add:field_simps)
- } note u_max = this
-
- have "u *\<^sub>R x \<in> frontier s"
- unfolding frontier_straddle
- apply (rule,rule,rule)
- apply (rule_tac x="u *\<^sub>R x" in bexI)
- unfolding obt(3)[symmetric]
- prefer 3
- apply (rule_tac x="(u + (e / 2) / norm x) *\<^sub>R x" in exI)
- apply (rule, rule)
- proof -
- fix e
- assume "e > 0" and as: "(u + e / 2 / norm x) *\<^sub>R x \<in> s"
- then have "u + e / 2 / norm x > u"
- using \<open>norm x > 0\<close> by (auto simp del:zero_less_norm_iff)
- then show False using u_max[OF _ as] by auto
- qed (insert \<open>y\<in>s\<close>, auto simp add: dist_norm scaleR_left_distrib obt(3))
- then show ?thesis by(metis that[of u] u_max obt(1))
-qed
-
-lemma starlike_compact_projective:
- assumes "compact s"
- and "cball (0::'a::euclidean_space) 1 \<subseteq> s "
- and "\<forall>x\<in>s. \<forall>u. 0 \<le> u \<and> u < 1 \<longrightarrow> u *\<^sub>R x \<in> s - frontier s"
- shows "s homeomorphic (cball (0::'a::euclidean_space) 1)"
-proof -
- have fs: "frontier s \<subseteq> s"
- apply (rule frontier_subset_closed)
- using compact_imp_closed[OF assms(1)]
- apply simp
- done
- define pi where [abs_def]: "pi x = inverse (norm x) *\<^sub>R x" for x :: 'a
- have "0 \<notin> frontier s"
- unfolding frontier_straddle
- apply (rule notI)
- apply (erule_tac x=1 in allE)
- using assms(2)[unfolded subset_eq Ball_def mem_cball]
- apply auto
- done
- have injpi: "\<And>x y. pi x = pi y \<and> norm x = norm y \<longleftrightarrow> x = y"
- unfolding pi_def by auto
-
- have contpi: "continuous_on (UNIV - {0}) pi"
- apply (rule continuous_at_imp_continuous_on)
- apply rule unfolding pi_def
- apply (intro continuous_intros)
- apply simp
- done
- define sphere :: "'a set" where "sphere = {x. norm x = 1}"
- have pi: "\<And>x. x \<noteq> 0 \<Longrightarrow> pi x \<in> sphere" "\<And>x u. u>0 \<Longrightarrow> pi (u *\<^sub>R x) = pi x"
- unfolding pi_def sphere_def by auto
-
- have "0 \<in> s"
- using assms(2) and centre_in_cball[of 0 1] by auto
- have front_smul: "\<forall>x\<in>frontier s. \<forall>u\<ge>0. u *\<^sub>R x \<in> s \<longleftrightarrow> u \<le> 1"
- proof (rule,rule,rule)
- fix x and u :: real
- assume x: "x \<in> frontier s" and "0 \<le> u"
- then have "x \<noteq> 0"
- using \<open>0 \<notin> frontier s\<close> by auto
- obtain v where v: "0 \<le> v" "v *\<^sub>R x \<in> frontier s" "\<forall>w>v. w *\<^sub>R x \<notin> s"
- using compact_frontier_line_lemma[OF assms(1) \<open>0\<in>s\<close> \<open>x\<noteq>0\<close>] by auto
- have "v = 1"
- apply (rule ccontr)
- unfolding neq_iff
- apply (erule disjE)
- proof -
- assume "v < 1"
- then show False
- using v(3)[THEN spec[where x=1]] using x fs by (simp add: pth_1 subset_iff)
- next
- assume "v > 1"
- then show False
- using assms(3)[THEN bspec[where x="v *\<^sub>R x"], THEN spec[where x="inverse v"]]
- using v and x and fs
- unfolding inverse_less_1_iff by auto
- qed
- show "u *\<^sub>R x \<in> s \<longleftrightarrow> u \<le> 1"
- apply rule
- using v(3)[unfolded \<open>v=1\<close>, THEN spec[where x=u]]
- proof -
- assume "u \<le> 1"
- then show "u *\<^sub>R x \<in> s"
- apply (cases "u = 1")
- using assms(3)[THEN bspec[where x=x], THEN spec[where x=u]]
- using \<open>0\<le>u\<close> and x and fs
- by auto
- qed auto
- qed
-
- have "\<exists>surf. homeomorphism (frontier s) sphere pi surf"
- apply (rule homeomorphism_compact)
- apply (rule compact_frontier[OF assms(1)])
- apply (rule continuous_on_subset[OF contpi])
- defer
- apply (rule set_eqI)
- apply rule
- unfolding inj_on_def
- prefer 3
- apply(rule,rule,rule)
- proof -
- fix x
- assume "x \<in> pi ` frontier s"
- then obtain y where "y \<in> frontier s" "x = pi y" by auto
- then show "x \<in> sphere"
- using pi(1)[of y] and \<open>0 \<notin> frontier s\<close> by auto
- next
- fix x
- assume "x \<in> sphere"
- then have "norm x = 1" "x \<noteq> 0"
- unfolding sphere_def by auto
- then obtain u where "0 \<le> u" "u *\<^sub>R x \<in> frontier s" "\<forall>v>u. v *\<^sub>R x \<notin> s"
- using compact_frontier_line_lemma[OF assms(1) \<open>0\<in>s\<close>, of x] by auto
- then show "x \<in> pi ` frontier s"
- unfolding image_iff le_less pi_def
- apply (rule_tac x="u *\<^sub>R x" in bexI)
- using \<open>norm x = 1\<close> \<open>0 \<notin> frontier s\<close>
- apply auto
- done
- next
- fix x y
- assume as: "x \<in> frontier s" "y \<in> frontier s" "pi x = pi y"
- then have xys: "x \<in> s" "y \<in> s"
- using fs by auto
- from as(1,2) have nor: "norm x \<noteq> 0" "norm y \<noteq> 0"
- using \<open>0\<notin>frontier s\<close> by auto
- from nor have x: "x = norm x *\<^sub>R ((inverse (norm y)) *\<^sub>R y)"
- unfolding as(3)[unfolded pi_def, symmetric] by auto
- from nor have y: "y = norm y *\<^sub>R ((inverse (norm x)) *\<^sub>R x)"
- unfolding as(3)[unfolded pi_def] by auto
- have "0 \<le> norm y * inverse (norm x)" and "0 \<le> norm x * inverse (norm y)"
- using nor
- apply auto
- done
- then have "norm x = norm y"
- apply -
- apply (rule ccontr)
- unfolding neq_iff
- using x y and front_smul[THEN bspec, OF as(1), THEN spec[where x="norm y * (inverse (norm x))"]]
- using front_smul[THEN bspec, OF as(2), THEN spec[where x="norm x * (inverse (norm y))"]]
- using xys nor
- apply (auto simp add: field_simps)
- done
- then show "x = y"
- apply (subst injpi[symmetric])
- using as(3)
- apply auto
- done
- qed (insert \<open>0 \<notin> frontier s\<close>, auto)
- then obtain surf where
- surf: "\<forall>x\<in>frontier s. surf (pi x) = x" "pi ` frontier s = sphere" "continuous_on (frontier s) pi"
- "\<forall>y\<in>sphere. pi (surf y) = y" "surf ` sphere = frontier s" "continuous_on sphere surf"
- unfolding homeomorphism_def by auto
-
- have cont_surfpi: "continuous_on (UNIV - {0}) (surf \<circ> pi)"
- apply (rule continuous_on_compose)
- apply (rule contpi)
- apply (rule continuous_on_subset[of sphere])
- apply (rule surf(6))
- using pi(1)
- apply auto
- done
-
- {
- fix x
- assume as: "x \<in> cball (0::'a) 1"
- have "norm x *\<^sub>R surf (pi x) \<in> s"
- proof (cases "x=0 \<or> norm x = 1")
- case False
- then have "pi x \<in> sphere" "norm x < 1"
- using pi(1)[of x] as by(auto simp add: dist_norm)
- then show ?thesis
- apply (rule_tac assms(3)[rule_format, THEN DiffD1])
- apply (rule_tac fs[unfolded subset_eq, rule_format])
- unfolding surf(5)[symmetric]
- apply auto
- done
- next
- case True
- then show ?thesis
- apply rule
- defer
- unfolding pi_def
- apply (rule fs[unfolded subset_eq, rule_format])
- unfolding surf(5)[unfolded sphere_def, symmetric]
- using \<open>0\<in>s\<close>
- apply auto
- done
- qed
- } note hom = this
-
- {
- fix x
- assume "x \<in> s"
- then have "x \<in> (\<lambda>x. norm x *\<^sub>R surf (pi x)) ` cball 0 1"
- proof (cases "x = 0")
- case True
- show ?thesis
- unfolding image_iff True
- apply (rule_tac x=0 in bexI)
- apply auto
- done
- next
- let ?a = "inverse (norm (surf (pi x)))"
- case False
- then have invn: "inverse (norm x) \<noteq> 0" by auto
- from False have pix: "pi x\<in>sphere" using pi(1) by auto
- then have "pi (surf (pi x)) = pi x"
- apply (rule_tac surf(4)[rule_format])
- apply assumption
- done
- then have **: "norm x *\<^sub>R (?a *\<^sub>R surf (pi x)) = x"
- apply (rule_tac scaleR_left_imp_eq[OF invn])
- unfolding pi_def
- using invn
- apply auto
- done
- then have *: "?a * norm x > 0" and "?a > 0" "?a \<noteq> 0"
- using surf(5) \<open>0\<notin>frontier s\<close>
- apply -
- apply (rule mult_pos_pos)
- using False[unfolded zero_less_norm_iff[symmetric]]
- apply auto
- done
- have "norm (surf (pi x)) \<noteq> 0"
- using ** False by auto
- then have "norm x = norm ((?a * norm x) *\<^sub>R surf (pi x))"
- unfolding norm_scaleR abs_mult abs_norm_cancel abs_of_pos[OF \<open>?a > 0\<close>] by auto
- moreover have "pi x = pi ((inverse (norm (surf (pi x))) * norm x) *\<^sub>R surf (pi x))"
- unfolding pi(2)[OF *] surf(4)[rule_format, OF pix] ..
- moreover have "surf (pi x) \<in> frontier s"
- using surf(5) pix by auto
- then have "dist 0 (inverse (norm (surf (pi x))) *\<^sub>R x) \<le> 1"
- unfolding dist_norm
- using ** and *
- using front_smul[THEN bspec[where x="surf (pi x)"], THEN spec[where x="norm x * ?a"]]
- using False \<open>x\<in>s\<close>
- by (auto simp add: field_simps)
- ultimately show ?thesis
- unfolding image_iff
- apply (rule_tac x="inverse (norm (surf(pi x))) *\<^sub>R x" in bexI)
- apply (subst injpi[symmetric])
- unfolding abs_mult abs_norm_cancel abs_of_pos[OF \<open>?a > 0\<close>]
- unfolding pi(2)[OF \<open>?a > 0\<close>]
- apply auto
- done
- qed
- } note hom2 = this
-
- show ?thesis
- apply (subst homeomorphic_sym)
- apply (rule homeomorphic_compact[where f="\<lambda>x. norm x *\<^sub>R surf (pi x)"])
- apply (rule compact_cball)
- defer
- apply (rule set_eqI)
- apply rule
- apply (erule imageE)
- apply (drule hom)
- prefer 4
- apply (rule continuous_at_imp_continuous_on)
- apply rule
- apply (rule_tac [3] hom2)
- proof -
- fix x :: 'a
- assume as: "x \<in> cball 0 1"
- then show "continuous (at x) (\<lambda>x. norm x *\<^sub>R surf (pi x))"
- proof (cases "x = 0")
- case False
- then show ?thesis
- apply (intro continuous_intros)
- using cont_surfpi
- unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def
- apply auto
- done
- next
- case True
- obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
- using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
- then have "B > 0"
- using assms(2)
- unfolding subset_eq
- apply (erule_tac x="SOME i. i\<in>Basis" in ballE)
- defer
- apply (erule_tac x="SOME i. i\<in>Basis" in ballE)
- unfolding Ball_def mem_cball dist_norm
- using DIM_positive[where 'a='a]
- apply (auto simp: SOME_Basis)
- done
- show ?thesis
- unfolding True continuous_at Lim_at
- apply(rule,rule)
- apply(rule_tac x="e / B" in exI)
- apply rule
- apply (rule divide_pos_pos)
- prefer 3
- apply(rule,rule,erule conjE)
- unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel
- proof -
- fix e and x :: 'a
- assume as: "norm x < e / B" "0 < norm x" "e > 0"
- then have "surf (pi x) \<in> frontier s"
- using pi(1)[of x] unfolding surf(5)[symmetric] by auto
- then have "norm (surf (pi x)) \<le> B"
- using B fs by auto
- then have "norm x * norm (surf (pi x)) \<le> norm x * B"
- using as(2) by auto
- also have "\<dots> < e / B * B"
- apply (rule mult_strict_right_mono)
- using as(1) \<open>B>0\<close>
- apply auto
- done
- also have "\<dots> = e" using \<open>B > 0\<close> by auto
- finally show "norm x * norm (surf (pi x)) < e" .
- qed (insert \<open>B>0\<close>, auto)
- qed
- next
- {
- fix x
- assume as: "surf (pi x) = 0"
- have "x = 0"
- proof (rule ccontr)
- assume "x \<noteq> 0"
- then have "pi x \<in> sphere"
- using pi(1) by auto
- then have "surf (pi x) \<in> frontier s"
- using surf(5) by auto
- then show False
- using \<open>0\<notin>frontier s\<close> unfolding as by simp
- qed
- } note surf_0 = this
- show "inj_on (\<lambda>x. norm x *\<^sub>R surf (pi x)) (cball 0 1)"
- unfolding inj_on_def
- proof (rule,rule,rule)
- fix x y
- assume as: "x \<in> cball 0 1" "y \<in> cball 0 1" "norm x *\<^sub>R surf (pi x) = norm y *\<^sub>R surf (pi y)"
- then show "x = y"
- proof (cases "x=0 \<or> y=0")
- case True
- then show ?thesis
- using as by (auto elim: surf_0)
- next
- case False
- then have "pi (surf (pi x)) = pi (surf (pi y))"
- using as(3)
- using pi(2)[of "norm x" "surf (pi x)"] pi(2)[of "norm y" "surf (pi y)"]
- by auto
- moreover have "pi x \<in> sphere" "pi y \<in> sphere"
- using pi(1) False by auto
- ultimately have *: "pi x = pi y"
- using surf(4)[THEN bspec[where x="pi x"]] surf(4)[THEN bspec[where x="pi y"]]
- by auto
- moreover have "norm x = norm y"
- using as(3)[unfolded *] using False
- by (auto dest:surf_0)
- ultimately show ?thesis
- using injpi by auto
- qed
- qed
- qed auto
-qed
-
-lemma homeomorphic_convex_compact_lemma:
- fixes s :: "'a::euclidean_space set"
- assumes "convex s"
- and "compact s"
- and "cball 0 1 \<subseteq> s"
- shows "s homeomorphic (cball (0::'a) 1)"
-proof (rule starlike_compact_projective[OF assms(2-3)], clarify)
- fix x u
- assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
- have "open (ball (u *\<^sub>R x) (1 - u))"
- by (rule open_ball)
- moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
- unfolding centre_in_ball using \<open>u < 1\<close> by simp
- moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
- proof
- fix y
- assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
- then have "dist (u *\<^sub>R x) y < 1 - u"
- unfolding mem_ball .
- with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
- by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
- with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
- with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
- using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
- then show "y \<in> s" using \<open>u < 1\<close>
- by simp
- qed
- ultimately have "u *\<^sub>R x \<in> interior s" ..
- then show "u *\<^sub>R x \<in> s - frontier s"
- using frontier_def and interior_subset by auto
-qed
-
-lemma homeomorphic_convex_compact_cball:
- fixes e :: real
- and s :: "'a::euclidean_space set"
- assumes "convex s"
- and "compact s"
- and "interior s \<noteq> {}"
- and "e > 0"
- shows "s homeomorphic (cball (b::'a) e)"
-proof -
- obtain a where "a \<in> interior s"
- using assms(3) by auto
- then obtain d where "d > 0" and d: "cball a d \<subseteq> s"
- unfolding mem_interior_cball by auto
- let ?d = "inverse d" and ?n = "0::'a"
- have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
- apply rule
- apply (rule_tac x="d *\<^sub>R x + a" in image_eqI)
- defer
- apply (rule d[unfolded subset_eq, rule_format])
- using \<open>d > 0\<close>
- unfolding mem_cball dist_norm
- apply (auto simp add: mult_right_le_one_le)
- done
- then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` s homeomorphic cball ?n 1"
- using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
- OF convex_affinity compact_affinity]
- using assms(1,2)
- by (auto simp add: scaleR_right_diff_distrib)
- then show ?thesis
- apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
- apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
- using \<open>d>0\<close> \<open>e>0\<close>
- apply (auto simp add: scaleR_right_diff_distrib)
- done
-qed
-
-lemma homeomorphic_convex_compact:
- fixes s :: "'a::euclidean_space set"
- and t :: "'a set"
- assumes "convex s" "compact s" "interior s \<noteq> {}"
- and "convex t" "compact t" "interior t \<noteq> {}"
- shows "s homeomorphic t"
- using assms
- by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
-
-
subsection \<open>Epigraphs of convex functions\<close>
definition "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Tue May 24 15:08:07 2016 +0100
@@ -3,6 +3,7 @@
Fashoda
Extended_Real_Limits
Determinants
+ Homeomorphism
Ordered_Euclidean_Space
Bounded_Continuous_Function
Weierstrass
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 24 15:08:07 2016 +0100
@@ -532,7 +532,7 @@
(Unprovable, "Termination reason: Satisfiable"),
(Interrupted, "Aborted by signal SIGINT")] @
known_szs_status_failures,
- prem_role = Conjecture,
+ prem_role = Hypothesis,
best_slices = fn ctxt =>
(* FUDGE *)
(if is_vampire_beyond_1_8 () then
@@ -724,7 +724,7 @@
remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
(K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_vampire =
- remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5"]
+ remotify_atp vampire "Vampire" ["4.0", "3.0", "2.6"]
(K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue May 24 15:08:07 2016 +0100
@@ -1018,7 +1018,7 @@
val _ =
Outer_Syntax.local_theory @{command_keyword lifting_forget}
"unsetup Lifting and Transfer for the given lifting bundle"
- (Parse.position Parse.name >> (lifting_forget_cmd))
+ (Parse.position Parse.name >> lifting_forget_cmd)
(* lifting_update *)
--- a/src/HOL/Tools/functor.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Tools/functor.ML Tue May 24 15:08:07 2016 +0100
@@ -277,7 +277,6 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword functor}
"register operations managing the functorial structure of a type"
- (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
- >> (fn (prfx, t) => functor_cmd prfx t));
+ (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term >> uncurry functor_cmd);
end;
--- a/src/HOL/UNITY/UNITY_Main.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy Tue May 24 15:08:07 2016 +0100
@@ -16,7 +16,7 @@
"for proving safety properties"
method_setup ensures_tac = {*
- Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
+ Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
*} "for proving progress properties"
--- a/src/HOL/Unix/Unix.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Unix/Unix.thy Tue May 24 15:08:07 2016 +0100
@@ -924,7 +924,7 @@
with tr obtain opt where root': "root' = update (path_of x) opt root"
by cases auto
show ?thesis
- proof (rule prefixeq_cases)
+ proof (rule prefix_cases)
assume "path_of x \<parallel> path"
with inv root'
have "\<And>perms. access root' path user\<^sub>1 perms = access root path user\<^sub>1 perms"
@@ -932,7 +932,7 @@
with inv show "invariant root' path"
by (simp only: invariant_def)
next
- assume "prefixeq (path_of x) path"
+ assume "prefix (path_of x) path"
then obtain ys where path: "path = path_of x @ ys" ..
show ?thesis
@@ -969,7 +969,7 @@
by (simp only: invariant_def access_def)
qed
next
- assume "prefix path (path_of x)"
+ assume "strict_prefix path (path_of x)"
then obtain y ys where path: "path_of x = path @ y # ys" ..
obtain dir' where
--- a/src/HOL/ex/Cartouche_Examples.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue May 24 15:08:07 2016 +0100
@@ -7,7 +7,7 @@
theory Cartouche_Examples
imports Main
keywords
- "cartouche" "term_cartouche" :: diag and
+ "cartouche" :: diag and
"text_cartouche" :: thy_decl
begin
@@ -19,21 +19,23 @@
notepad
begin
- txt \<open>Moreover, cartouches work as additional syntax in the
- \<open>altstring\<close> category, for literal fact references. For example:\<close>
+ txt \<open>Cartouches work as additional syntax for embedded language tokens
+ (types, terms, props) and as a replacement for the \<open>altstring\<close> category
+ (for literal fact references). For example:\<close>
fix x y :: 'a
- assume "x = y"
+ assume \<open>x = y\<close>
note \<open>x = y\<close>
- have "x = y" by (rule \<open>x = y\<close>)
- from \<open>x = y\<close> have "x = y" .
+ have \<open>x = y\<close> by (rule \<open>x = y\<close>)
+ from \<open>x = y\<close> have \<open>x = y\<close> .
txt \<open>Of course, this can be nested inside formal comments and
antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
[OF \<open>x = y\<close>]}.\<close>
- have "x = y"
- by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>) \<comment> \<open>more cartouches involving ML\<close>
+ have \<open>x = y\<close>
+ by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>)
+ \<comment> \<open>more cartouches involving ML\<close>
end
@@ -78,92 +80,55 @@
end;
\<close>
-syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> string" ("_")
+syntax "_cartouche_string" :: \<open>cartouche_position \<Rightarrow> string\<close> ("_")
parse_translation \<open>
[(@{syntax_const "_cartouche_string"},
K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
\<close>
-term "\<open>\<close>"
-term "\<open>abc\<close>"
-term "\<open>abc\<close> @ \<open>xyz\<close>"
-term "\<open>\<newline>\<close>"
-term "\<open>\001\010\100\<close>"
+term \<open>\<open>\<close>\<close>
+term \<open>\<open>abc\<close>\<close>
+term \<open>\<open>abc\<close> @ \<open>xyz\<close>\<close>
+term \<open>\<open>\<newline>\<close>\<close>
subsection \<open>Alternate outer and inner syntax: string literals\<close>
subsubsection \<open>Nested quotes\<close>
-syntax "_string_string" :: "string_position \<Rightarrow> string" ("_")
+syntax "_string_string" :: \<open>string_position \<Rightarrow> string\<close> ("_")
parse_translation \<open>
[(@{syntax_const "_string_string"}, K (string_tr Lexicon.explode_string))]
\<close>
-term "\"\""
-term "\"abc\""
-term "\"abc\" @ \"xyz\""
-term "\"\<newline>\""
-term "\"\001\010\100\""
-
-
-subsubsection \<open>Term cartouche and regular quotes\<close>
-
-ML \<open>
- Outer_Syntax.command @{command_keyword term_cartouche} ""
- (Parse.inner_syntax Parse.cartouche >> (fn s =>
- Toplevel.keep (fn state =>
- let
- val ctxt = Toplevel.context_of state;
- val t = Syntax.read_term ctxt s;
- in writeln (Syntax.string_of_term ctxt t) end)))
-\<close>
-
-term_cartouche \<open>""\<close>
-term_cartouche \<open>"abc"\<close>
-term_cartouche \<open>"abc" @ "xyz"\<close>
-term_cartouche \<open>"\<newline>"\<close>
-term_cartouche \<open>"\001\010\100"\<close>
+term \<open>""\<close>
+term \<open>"abc"\<close>
+term \<open>"abc" @ "xyz"\<close>
+term \<open>"\<newline>"\<close>
+term \<open>"\001\010\100"\<close>
subsubsection \<open>Further nesting: antiquotations\<close>
-setup \<comment> "ML antiquotation"
-\<open>
- ML_Antiquotation.inline @{binding term_cartouche}
- (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
- (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
-\<close>
-
-setup \<comment> "document antiquotation"
-\<open>
- Thy_Output.antiquotation @{binding ML_cartouche}
- (Scan.lift Args.cartouche_input) (fn {context, ...} => fn source =>
- let
- val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
- val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
- in "" end);
-\<close>
-
ML \<open>
- @{term_cartouche \<open>""\<close>};
- @{term_cartouche \<open>"abc"\<close>};
- @{term_cartouche \<open>"abc" @ "xyz"\<close>};
- @{term_cartouche \<open>"\<newline>"\<close>};
- @{term_cartouche \<open>"\001\010\100"\<close>};
+ @{term \<open>""\<close>};
+ @{term \<open>"abc"\<close>};
+ @{term \<open>"abc" @ "xyz"\<close>};
+ @{term \<open>"\<newline>"\<close>};
+ @{term \<open>"\001\010\100"\<close>};
\<close>
text \<open>
- @{ML_cartouche
+ @{ML
\<open>
(
- @{term_cartouche \<open>""\<close>};
- @{term_cartouche \<open>"abc"\<close>};
- @{term_cartouche \<open>"abc" @ "xyz"\<close>};
- @{term_cartouche \<open>"\<newline>"\<close>};
- @{term_cartouche \<open>"\001\010\100"\<close>}
+ @{term \<open>""\<close>};
+ @{term \<open>"abc"\<close>};
+ @{term \<open>"abc" @ "xyz"\<close>};
+ @{term \<open>"\<newline>"\<close>};
+ @{term \<open>"\001\010\100"\<close>}
)
\<close>
}
@@ -181,14 +146,14 @@
text_cartouche
\<open>
- @{ML_cartouche
+ @{ML
\<open>
(
- @{term_cartouche \<open>""\<close>};
- @{term_cartouche \<open>"abc"\<close>};
- @{term_cartouche \<open>"abc" @ "xyz"\<close>};
- @{term_cartouche \<open>"\<newline>"\<close>};
- @{term_cartouche \<open>"\001\010\100"\<close>}
+ @{term \<open>""\<close>};
+ @{term \<open>"abc"\<close>};
+ @{term \<open>"abc" @ "xyz"\<close>};
+ @{term \<open>"\<newline>"\<close>};
+ @{term \<open>"\001\010\100"\<close>}
)
\<close>
}
@@ -226,18 +191,18 @@
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
\<close>
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
apply (ml_tactic \<open>resolve_tac @{context} @{thms impI} 1\<close>)
apply (ml_tactic \<open>eresolve_tac @{context} @{thms conjE} 1\<close>)
apply (ml_tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
apply (ml_tactic \<open>ALLGOALS (assume_tac @{context})\<close>)
done
-lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)
-ML \<open>@{lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>
+ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>
-text \<open>@{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"}\<close>
+text \<open>@{ML \<open>@{lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by (ml_tactic \<open>blast_tac ctxt 1\<close>)}\<close>}\<close>
subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close>
@@ -247,14 +212,14 @@
>> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
\<close>
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
apply \<open>resolve_tac @{context} @{thms impI} 1\<close>
apply \<open>eresolve_tac @{context} @{thms conjE} 1\<close>
apply \<open>resolve_tac @{context} @{thms conjI} 1\<close>
apply \<open>ALLGOALS (assume_tac @{context})\<close>
done
-lemma "A \<and> B \<longrightarrow> B \<and> A"
+lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close>
by (\<open>resolve_tac @{context} @{thms impI} 1\<close>,
\<open>eresolve_tac @{context} @{thms conjE} 1\<close>,
\<open>resolve_tac @{context} @{thms conjI} 1\<close>,
--- a/src/LCF/LCF.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/LCF/LCF.thy Tue May 24 15:08:07 2016 +0100
@@ -319,7 +319,7 @@
adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
method_setup induct = \<open>
- Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt =>
+ Scan.lift Args.embedded_inner_syntax >> (fn v => fn ctxt =>
SIMPLE_METHOD' (fn i =>
Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] [] @{thm induct} i THEN
REPEAT (resolve_tac ctxt @{thms adm_lemmas} i)))
--- a/src/Pure/Isar/args.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/Pure/Isar/args.ML Tue May 24 15:08:07 2016 +0100
@@ -23,12 +23,14 @@
val mode: string -> bool parser
val maybe: 'a parser -> 'a option parser
val name_token: Token.T parser
- val name_inner_syntax: string parser
- val name_input: Input.source parser
val name: string parser
val cartouche_inner_syntax: string parser
val cartouche_input: Input.source parser
val text_token: Token.T parser
+ val embedded_token: Token.T parser
+ val embedded_inner_syntax: string parser
+ val embedded_input: Input.source parser
+ val embedded: string parser
val text_input: Input.source parser
val text: string parser
val binding: binding parser
@@ -104,15 +106,18 @@
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
val name_token = ident || string;
-val name_inner_syntax = name_token >> Token.inner_syntax_of;
-val name_input = name_token >> Token.input_of;
val name = name_token >> Token.content_of;
val cartouche = Parse.token Parse.cartouche;
val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
val cartouche_input = cartouche >> Token.input_of;
-val text_token = name_token || Parse.token (Parse.verbatim || Parse.cartouche);
+val embedded_token = ident || string || cartouche;
+val embedded_inner_syntax = embedded_token >> Token.inner_syntax_of;
+val embedded_input = embedded_token >> Token.input_of;
+val embedded = embedded_token >> Token.content_of;
+
+val text_token = embedded_token || Parse.token Parse.verbatim;
val text_input = text_token >> Token.input_of;
val text = text_token >> Token.content_of;
@@ -120,8 +125,9 @@
val alt_name = alt_string >> Token.content_of;
val liberal_name = (symbolic >> Token.content_of) || name;
-val var = (ident >> Token.content_of) :|-- (fn x =>
- (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
+val var =
+ (ident >> Token.content_of) :|-- (fn x =>
+ (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
(* values *)
@@ -141,10 +147,10 @@
internal_source || name_token >> Token.evaluate Token.Source read;
fun named_typ read =
- internal_typ || name_token >> Token.evaluate Token.Typ (read o Token.inner_syntax_of);
+ internal_typ || embedded_token >> Token.evaluate Token.Typ (read o Token.inner_syntax_of);
fun named_term read =
- internal_term || name_token >> Token.evaluate Token.Term (read o Token.inner_syntax_of);
+ internal_term || embedded_token >> Token.evaluate Token.Term (read o Token.inner_syntax_of);
fun named_fact get =
internal_fact ||
--- a/src/Pure/Isar/parse.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/Pure/Isar/parse.ML Tue May 24 15:08:07 2016 +0100
@@ -62,8 +62,9 @@
val list: 'a parser -> 'a list parser
val list1: 'a parser -> 'a list parser
val properties: Properties.T parser
- val name: bstring parser
+ val name: string parser
val binding: binding parser
+ val embedded: string parser
val text: string parser
val path: string parser
val theory_name: string parser
@@ -257,16 +258,21 @@
val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
-(* names and text *)
+(* names and embedded content *)
val name =
- group (fn () => "name") (short_ident || long_ident || sym_ident || string || number);
+ group (fn () => "name")
+ (short_ident || long_ident || sym_ident || number || string);
val binding = position name >> Binding.make;
+val embedded =
+ group (fn () => "embedded content")
+ (short_ident || long_ident || sym_ident || number || string || cartouche);
+
val text =
group (fn () => "text")
- (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
+ (short_ident || long_ident || sym_ident || number || string || verbatim || cartouche);
val path = group (fn () => "file name/path specification") name;
@@ -280,11 +286,11 @@
(* type classes *)
-val class = group (fn () => "type class") (inner_syntax name);
+val class = group (fn () => "type class") (inner_syntax embedded);
-val sort = group (fn () => "sort") (inner_syntax name);
+val sort = group (fn () => "sort") (inner_syntax embedded);
-val type_const = inner_syntax (group (fn () => "type constructor") name);
+val type_const = group (fn () => "type constructor") (inner_syntax embedded);
val arity = type_const -- ($$$ "::" |-- !!!
(Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> Scan.triple2;
@@ -297,7 +303,8 @@
val typ_group =
group (fn () => "type")
- (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
+ (short_ident || long_ident || sym_ident || type_ident || type_var || number ||
+ string || cartouche);
val typ = inner_syntax typ_group;
@@ -386,15 +393,13 @@
(* terms *)
-val tm = short_ident || long_ident || sym_ident || term_var || number || string;
-
-val term_group = group (fn () => "term") tm;
-val prop_group = group (fn () => "proposition") tm;
+val term_group = group (fn () => "term") (term_var || embedded);
+val prop_group = group (fn () => "proposition") (term_var || embedded);
val term = inner_syntax term_group;
val prop = inner_syntax prop_group;
-val const = inner_syntax (group (fn () => "constant") name);
+val const = group (fn () => "constant") (inner_syntax embedded);
val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
--- a/src/Pure/ML/ml_antiquotations.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Tue May 24 15:08:07 2016 +0100
@@ -17,7 +17,7 @@
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
ML_Antiquotation.declaration @{binding print}
- (Scan.lift (Scan.optional Args.name "Output.writeln"))
+ (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
(fn src => fn output => fn ctxt =>
let
val struct_name = ML_Context.struct_name ctxt;
@@ -86,7 +86,7 @@
(* type classes *)
-fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
+fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
Proof_Context.read_class ctxt s
|> syn ? Lexicon.mark_class
|> ML_Syntax.print_string);
@@ -96,13 +96,13 @@
ML_Antiquotation.inline @{binding class_syntax} (class true) #>
ML_Antiquotation.inline @{binding sort}
- (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
+ (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
(* type constructors *)
-fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
+fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
>> (fn (ctxt, (s, pos)) =>
let
val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
@@ -126,7 +126,7 @@
(* constants *)
-fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
+fun const_name check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
>> (fn (ctxt, (s, pos)) =>
let
val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
@@ -143,13 +143,13 @@
(const_name (fn (_, c) => Lexicon.mark_const c)) #>
ML_Antiquotation.inline @{binding syntax_const}
- (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
+ (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) =>
if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
then ML_Syntax.print_string c
else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
ML_Antiquotation.inline @{binding const}
- (Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) -- Scan.optional
+ (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, (raw_c, pos)), Ts) =>
let
--- a/src/Pure/ML/ml_thms.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/Pure/ML/ml_thms.ML Tue May 24 15:08:07 2016 +0100
@@ -77,7 +77,7 @@
val and_ = Args.$$$ "and";
val by = Parse.reserved "by";
-val goal = Scan.unless (by || and_) Args.name_inner_syntax;
+val goal = Scan.unless (by || and_) Args.embedded_inner_syntax;
val _ = Theory.setup
(ML_Antiquotation.declaration @{binding lemma}
--- a/src/Pure/Thy/document_antiquotations.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Tue May 24 15:08:07 2016 +0100
@@ -195,7 +195,7 @@
(* URLs *)
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
+ (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.embedded))
(fn {context = ctxt, ...} => fn (name, pos) =>
(Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
enclose "\\url{" "}" name)));
--- a/src/Pure/Thy/thy_output.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue May 24 15:08:07 2016 +0100
@@ -645,10 +645,10 @@
basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
- basic_entity @{binding abbrev} (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
+ basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
- basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
+ basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #>
+ basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #>
basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
--- a/src/Pure/Tools/rule_insts.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/Pure/Tools/rule_insts.ML Tue May 24 15:08:07 2016 +0100
@@ -177,7 +177,8 @@
(* where: named instantiation *)
val named_insts =
- Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax))
+ Parse.and_list1
+ (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.embedded_inner_syntax))
-- Parse.for_fixes;
val _ = Theory.setup
@@ -191,7 +192,7 @@
local
-val inst = Args.maybe Args.name_inner_syntax;
+val inst = Args.maybe Args.embedded_inner_syntax;
val concl = Args.$$$ "concl" -- Args.colon;
val insts =
@@ -330,12 +331,12 @@
Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
"cut rule (dynamic instantiation)" #>
Method.setup @{binding subgoal_tac}
- (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (props, fixes)) => fn ctxt =>
SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
"insert subgoal (dynamic instantiation)" #>
Method.setup @{binding thin_tac}
- (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
"remove premise (dynamic instantiation)");
--- a/src/Tools/induct_tacs.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/Tools/induct_tacs.ML Tue May 24 15:08:07 2016 +0100
@@ -122,14 +122,14 @@
val varss =
Parse.and_list'
- (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax))));
+ (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.embedded_inner_syntax))));
in
val _ =
Theory.setup
(Method.setup @{binding case_tac}
- (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) -- opt_rule >>
+ (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
(fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
"unstructured case analysis on types" #>
Method.setup @{binding induct_tac}
--- a/src/ZF/Tools/ind_cases.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/ZF/Tools/ind_cases.ML Tue May 24 15:08:07 2016 +0100
@@ -64,7 +64,7 @@
val _ =
Theory.setup
(Method.setup @{binding "ind_cases"}
- (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
+ (Scan.lift (Scan.repeat1 Args.embedded_inner_syntax) >>
(fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
"dynamic case analysis on sets");
--- a/src/ZF/Tools/induct_tacs.ML Tue May 24 13:57:34 2016 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Tue May 24 15:08:07 2016 +0100
@@ -179,11 +179,11 @@
val _ =
Theory.setup
(Method.setup @{binding induct_tac}
- (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
(fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs)))
"induct_tac emulation (dynamic instantiation!)" #>
Method.setup @{binding case_tac}
- (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+ (Args.goal_spec -- Scan.lift (Args.embedded -- Parse.for_fixes) >>
(fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs)))
"datatype case_tac emulation (dynamic instantiation!)");
--- a/src/ZF/UNITY/SubstAx.thy Tue May 24 13:57:34 2016 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Tue May 24 15:08:07 2016 +0100
@@ -373,7 +373,7 @@
\<close>
method_setup ensures = \<open>
- Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
+ Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
\<close> "for proving progress properties"