# HG changeset patch # User paulson # Date 1464098887 -3600 # Node ID e5cb3440af74fe00f067c95013b02e44daf4729c # Parent 24708cf4ba61d12ee7d24ea158299768100ce33c# Parent 284e1802bc5c8bceabfe7fe0b1e4b7bf9ee4e834 Merge diff -r 24708cf4ba61 -r e5cb3440af74 NEWS --- 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 "\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 diff -r 24708cf4ba61 -r e5cb3440af74 src/CCL/CCL.thy --- 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 = \ - 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})) \ diff -r 24708cf4ba61 -r e5cb3440af74 src/CCL/Wfd.thy --- 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 = \ - 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))) diff -r 24708cf4ba61 -r e5cb3440af74 src/CTT/CTT.thy --- 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 = \Scan.succeed (SIMPLE_METHOD o eqintr_tac)\ method_setup NE = \ - 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)) \ method_setup pc = \Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\ method_setup add_mp = \Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\ diff -r 24708cf4ba61 -r e5cb3440af74 src/Doc/Isar_Ref/Document_Preparation.thy --- 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 + ',') ')' diff -r 24708cf4ba61 -r e5cb3440af74 src/Doc/Isar_Ref/Outer_Syntax.thy --- 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 \ @{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} ')' \} @@ -209,6 +209,24 @@ \ +subsection \Embedded content\ + +text \ + 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 \ + @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} | + @{syntax ident} | @{syntax longident} | @{syntax symident} | + @{syntax nat} + \} +\ + + subsection \Comments \label{sec:comments}\ text \ @@ -260,10 +278,10 @@ as \<^verbatim>\=\ or \<^verbatim>\+\). @{rail \ - @{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} \} diff -r 24708cf4ba61 -r e5cb3440af74 src/Doc/Prog_Prove/LaTeXsugar.thy --- 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])) diff -r 24708cf4ba61 -r e5cb3440af74 src/FOL/FOL.thy --- 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 @@ \ method_setup case_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, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes)) \ "case_tac emulation (dynamic instantiation!)" diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/Eisbach/parse_tools.ML --- 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; diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/HOLCF/IOA/CompoScheds.thy --- 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 @@ \ method_setup mkex_induct = \ - 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)) \ diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/HOLCF/IOA/Sequence.thy --- 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 @@ \ method_setup Seq_case = - \Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\ + \Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_tac ctxt s))\ method_setup Seq_case_simp = - \Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\ + \Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (Seq_case_simp_tac ctxt s))\ method_setup Seq_induct = - \Scan.lift Args.name -- + \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))\ @@ -1010,10 +1010,10 @@ \Scan.succeed (SIMPLE_METHOD' o Seq_Finite_induct_tac)\ method_setup pair = - \Scan.lift Args.name >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\ + \Scan.lift Args.embedded >> (fn s => fn ctxt => SIMPLE_METHOD' (pair_tac ctxt s))\ method_setup pair_induct = - \Scan.lift Args.name -- + \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))\ diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/Library/LaTeXsugar.thy --- 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])) diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy --- 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 \ 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 \ prefixeq yl xl" +shows "prefix xl yl \ prefix yl xl" using shift_prefix[OF assms] by (cases "length xl \ length yl") (metis, metis assms nat_le_linear shift_prefix) @@ -297,17 +297,17 @@ moreover obtain yl ys1 where xs2: "xs = yl @- ys1" and \\: "alw \ ys1" using \ by (metis ev_imp_shift) ultimately have 0: "xl @- xs1 = yl @- ys1" by auto - hence "prefixeq xl yl \ prefixeq yl xl" using shift_prefix_cases by auto + hence "prefix xl yl \ 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 \ ys1" using \\ unfolding xs1' by (metis alw_shift) hence "alw (\ aand \) ys1" using \\ 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 \ xs1" using \\ unfolding ys1' by (metis alw_shift) hence "alw (\ aand \) xs1" using \\ unfolding alw_aand by auto diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/Library/Prefix_Order.thy --- 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) \ ys \ prefixeq xs ys" +definition "(xs::'a list) \ ys \ prefix xs ys" definition "(xs::'a list) < ys \ xs \ ys \ \ (ys \ 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 \ 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 diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/Library/Sublist.thy --- 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 \Prefix order on lists\ -definition prefixeq :: "'a list \ 'a list \ bool" - where "prefixeq xs ys \ (\zs. ys = xs @ zs)" +definition prefix :: "'a list \ 'a list \ bool" + where "prefix xs ys \ (\zs. ys = xs @ zs)" -definition prefix :: "'a list \ 'a list \ bool" - where "prefix xs ys \ prefixeq xs ys \ xs \ ys" +definition strict_prefix :: "'a list \ 'a list \ bool" + where "strict_prefix xs ys \ prefix xs ys \ xs \ 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 \ prefixeq xs ys" - unfolding prefixeq_def by blast +lemma prefixI [intro?]: "ys = xs @ zs \ 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 \ prefix xs ys" - unfolding prefix_def prefixeq_def by blast +lemma strict_prefixI' [intro?]: "ys = xs @ z # zs \ 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 \prefix xs ys\ obtain us where "ys = xs @ us" and "xs \ ys" - unfolding prefix_def prefixeq_def by blast + from \strict_prefix xs ys\ obtain us where "ys = xs @ us" and "xs \ 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 \ xs \ ys \ prefix xs ys" - unfolding prefix_def by blast +lemma strict_prefixI [intro?]: "prefix xs ys \ xs \ ys \ 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 \ ys" - using assms unfolding prefix_def by blast + assumes "strict_prefix xs ys" + obtains "prefix xs ys" and "xs \ ys" + using assms unfolding strict_prefix_def by blast subsection \Basic properties of prefixes\ -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]) \ xs = ys @ [y] \ prefixeq xs ys" +lemma prefix_snoc [simp]: "prefix xs (ys @ [y]) \ xs = ys @ [y] \ 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] \ prefixeq xs ys" - by (metis append_Nil2 butlast_append butlast_snoc prefixeqI zs) + show "xs = ys @ [y] \ prefix xs ys" + by (metis append_Nil2 butlast_append butlast_snoc prefixI zs) next - assume "xs = ys @ [y] \ prefixeq xs ys" - then show "prefixeq xs (ys @ [y])" - by (metis prefix_order.eq_iff prefix_order.order_trans prefixeqI) + assume "xs = ys @ [y] \ 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 \ prefixeq xs ys)" - by (auto simp add: prefixeq_def) +lemma Cons_prefix_Cons [simp]: "prefix (x # xs) (y # ys) = (x = y \ prefix xs ys)" + by (auto simp add: prefix_def) -lemma prefixeq_code [code]: - "prefixeq [] xs \ True" - "prefixeq (x # xs) [] \ False" - "prefixeq (x # xs) (y # ys) \ x = y \ prefixeq xs ys" +lemma prefix_code [code]: + "prefix [] xs \ True" + "prefix (x # xs) [] \ False" + "prefix (x # xs) (y # ys) \ x = y \ 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 \ prefixeq xs (ys @ zs)" - by (metis prefix_order.le_less_trans prefixeqI prefixE prefixI) +lemma prefix_prefix [simp]: "prefix xs ys \ prefix xs (ys @ zs)" + by (metis prefix_order.le_less_trans prefixI strict_prefixE strict_prefixI) -lemma append_prefixeqD: "prefixeq (xs @ ys) zs \ prefixeq xs zs" - by (auto simp add: prefixeq_def) +lemma append_prefixD: "prefix (xs @ ys) zs \ prefix xs zs" + by (auto simp add: prefix_def) -theorem prefixeq_Cons: "prefixeq xs (y # ys) = (xs = [] \ (\zs. xs = y # zs \ prefixeq zs ys))" - by (cases xs) (auto simp add: prefixeq_def) +theorem prefix_Cons: "prefix xs (y # ys) = (xs = [] \ (\zs. xs = y # zs \ prefix zs ys))" + by (cases xs) (auto simp add: prefix_def) -theorem prefixeq_append: - "prefixeq xs (ys @ zs) = (prefixeq xs ys \ (\us. xs = ys @ us \ prefixeq us zs))" +theorem prefix_append: + "prefix xs (ys @ zs) = (prefix xs ys \ (\us. xs = ys @ us \ 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 \ length xs < length ys \ prefixeq (xs @ [ys ! length xs]) ys" - proof (unfold prefixeq_def) +lemma append_one_prefix: + "prefix xs ys \ length xs < length ys \ prefix (xs @ [ys ! length xs]) ys" + proof (unfold prefix_def) assume a1: "\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 "\zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce qed -theorem prefixeq_length_le: "prefixeq xs ys \ length xs \ length ys" - by (auto simp add: prefixeq_def) +theorem prefix_length_le: "prefix xs ys \ length xs \ length ys" + by (auto simp add: prefix_def) -lemma prefixeq_same_cases: - "prefixeq (xs\<^sub>1::'a list) ys \ prefixeq xs\<^sub>2 ys \ prefixeq xs\<^sub>1 xs\<^sub>2 \ 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 \ prefix xs\<^sub>2 ys \ prefix xs\<^sub>1 xs\<^sub>2 \ prefix xs\<^sub>2 xs\<^sub>1" + unfolding prefix_def by (force simp: append_eq_append_conv2) -lemma set_mono_prefixeq: "prefixeq xs ys \ set xs \ set ys" - by (auto simp add: prefixeq_def) +lemma set_mono_prefix: "prefix xs ys \ set xs \ 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 \ prefixeq (map f xs) (map f ys)" - by (auto simp: prefixeq_def) +lemma map_prefixI: "prefix xs ys \ prefix (map f xs) (map f ys)" + by (auto simp: prefix_def) -lemma prefixeq_length_less: "prefix xs ys \ length xs < length ys" - by (auto simp: prefix_def prefixeq_def) +lemma prefix_length_less: "strict_prefix xs ys \ length xs < length ys" + by (auto simp: strict_prefix_def prefix_def) -lemma prefix_simps [simp, code]: - "prefix xs [] \ False" - "prefix [] (x # xs) \ True" - "prefix (x # xs) (y # ys) \ x = y \ prefix xs ys" - by (simp_all add: prefix_def cong: conj_cong) +lemma strict_prefix_simps [simp, code]: + "strict_prefix xs [] \ False" + "strict_prefix [] (x # xs) \ True" + "strict_prefix (x # xs) (y # ys) \ x = y \ strict_prefix xs ys" + by (simp_all add: strict_prefix_def cong: conj_cong) -lemma take_prefix: "prefix xs ys \ prefix (take n xs) ys" +lemma take_strict_prefix: "strict_prefix xs ys \ 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: "\ prefixeq ps ls" +lemma not_prefix_cases: + assumes pfx: "\ prefix ps ls" obtains (c1) "ps \ []" and "ls = []" - | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\ prefixeq as xs" + | (c2) a as x xs where "ps = a#as" and "ls = x#xs" and "x = a" and "\ prefix as xs" | (c3) a as x xs where "ps = a#as" and "ls = x#xs" and "x \ a" proof (cases ps) case Nil @@ -162,13 +162,13 @@ note c = \ps = a#as\ 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 "\ prefixeq as xs" using pfx c Cons True by simp + have "\ 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: "\ prefixeq ps ls" +lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]: + assumes np: "\ prefix ps ls" and base: "\x xs. P (x#xs) []" and r1: "\x xs y ys. x \ y \ P (x#xs) (y#ys)" - and r2: "\x xs y ys. \ x = y; \ prefixeq xs ys; P xs ys \ \ P (x#xs) (y#ys)" + and r2: "\x xs y ys. \ x = y; \ prefix xs ys; P xs ys \ \ 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: "\ prefixeq ps (y # ys)" by simp + then have npfx: "\ 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 \Parallel lists\ definition parallel :: "'a list \ 'a list \ bool" (infixl "\" 50) - where "(xs \ ys) = (\ prefixeq xs ys \ \ prefixeq ys xs)" + where "(xs \ ys) = (\ prefix xs ys \ \ prefix ys xs)" -lemma parallelI [intro]: "\ prefixeq xs ys \ \ prefixeq ys xs \ xs \ ys" +lemma parallelI [intro]: "\ prefix xs ys \ \ prefix ys xs \ xs \ ys" unfolding parallel_def by blast lemma parallelE [elim]: assumes "xs \ ys" - obtains "\ prefixeq xs ys \ \ prefixeq ys xs" + obtains "\ prefix xs ys \ \ prefix ys xs" using assms unfolding parallel_def by blast -theorem prefixeq_cases: - obtains "prefixeq xs ys" | "prefix ys xs" | "xs \ ys" - unfolding parallel_def prefix_def by blast +theorem prefix_cases: + obtains "prefix xs ys" | "strict_prefix ys xs" | "xs \ ys" + unfolding parallel_def strict_prefix_def by blast theorem parallel_decomp: "xs \ ys \ \as b bs c cs. b \ c \ xs = as @ b # bs \ 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 \ 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 \ b \ a @ c \ 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 \ ys \ x = xs @ xs' \ y = ys @ ys' \ x \ y" @@ -327,14 +327,14 @@ by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI) qed -lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \ prefixeq (rev xs) (rev ys)" +lemma suffixeq_to_prefix [code]: "suffixeq xs ys \ 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 \ y \ \ prefixeq x y" +lemma parallelD1: "x \ y \ \ prefix x y" by blast -lemma parallelD2: "x \ y \ \ prefixeq y x" +lemma parallelD2: "x \ y \ \ prefix y x" by blast lemma parallel_Nil1 [simp]: "\ x \ []" @@ -395,7 +395,7 @@ by auto lemma Cons_parallelI2: "\ a = b; as \ bs \ \ a # as \ b # bs" - by (metis Cons_prefixeq_Cons parallelE parallelI) + by (metis Cons_prefix_Cons parallelE parallelI) lemma not_equal_is_parallel: assumes neq: "xs \ ys" diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- 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 \Results connected with topological dimension.\ theory Brouwer_Fixpoint -imports Path_Connected +imports Path_Connected Homeomorphism begin lemma bij_betw_singleton_eq: diff -r 24708cf4ba61 -r e5cb3440af74 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 \Homeomorphism of all convex compact sets with nonempty interior\ - -lemma compact_frontier_line_lemma: - fixes s :: "'a::euclidean_space set" - assumes "compact s" - and "0 \ s" - and "x \ 0" - obtains u where "0 \ u" and "(u *\<^sub>R x) \ frontier s" "\v>u. (v *\<^sub>R x) \ s" -proof - - obtain b where b: "b > 0" "\x\s. norm x \ b" - using compact_imp_bounded[OF assms(1), unfolded bounded_pos] by auto - let ?A = "{y. \u. 0 \ u \ u \ b / norm(x) \ (y = u *\<^sub>R x)}" - have A: "?A = (\u. u *\<^sub>R x) ` {0 .. b / norm x}" - by auto - have *: "\x A B. x\A \ x\B \ A\B \ {}" 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. \u\0. u \ b / norm x \ y = u *\<^sub>R x} \ s \ {}" - apply(rule *[OF _ assms(2)]) - unfolding mem_Collect_eq - using \b > 0\ assms(3) - apply auto - done - ultimately obtain u y where obt: "u\0" "u \ b / norm x" "y = u *\<^sub>R x" - "y \ ?A" "y \ s" "\z\?A \ s. dist 0 z \ 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 \ s" - then have "v \ b / norm x" - using b(2)[rule_format, OF as(2)] - using \u\0\ - unfolding pos_le_divide_eq[OF \norm x > 0\] - by auto - then have "norm (v *\<^sub>R x) \ 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) \u\0\ - apply (auto simp add: field_simps) - done - then have False - unfolding obt(3) using \u\0\ \norm x > 0\ \v > u\ - by (auto simp add:field_simps) - } note u_max = this - - have "u *\<^sub>R x \ 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 \ s" - then have "u + e / 2 / norm x > u" - using \norm x > 0\ by (auto simp del:zero_less_norm_iff) - then show False using u_max[OF _ as] by auto - qed (insert \y\s\, 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 \ s " - and "\x\s. \u. 0 \ u \ u < 1 \ u *\<^sub>R x \ s - frontier s" - shows "s homeomorphic (cball (0::'a::euclidean_space) 1)" -proof - - have fs: "frontier s \ 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 \ 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: "\x y. pi x = pi y \ norm x = norm y \ 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: "\x. x \ 0 \ pi x \ sphere" "\x u. u>0 \ pi (u *\<^sub>R x) = pi x" - unfolding pi_def sphere_def by auto - - have "0 \ s" - using assms(2) and centre_in_cball[of 0 1] by auto - have front_smul: "\x\frontier s. \u\0. u *\<^sub>R x \ s \ u \ 1" - proof (rule,rule,rule) - fix x and u :: real - assume x: "x \ frontier s" and "0 \ u" - then have "x \ 0" - using \0 \ frontier s\ by auto - obtain v where v: "0 \ v" "v *\<^sub>R x \ frontier s" "\w>v. w *\<^sub>R x \