# HG changeset patch # User wenzelm # Date 1377726525 -7200 # Node ID 082d0972096bb8b9c922b111fc889d739e9fbc15 # Parent 16235bb41881acea808e8234eff23daff634d4b7# Parent 220f306f5c4ead7792efcaeda423d1b2762a58d4 merged diff -r 16235bb41881 -r 082d0972096b NEWS --- a/NEWS Wed Aug 28 18:44:50 2013 +0200 +++ b/NEWS Wed Aug 28 23:48:45 2013 +0200 @@ -90,6 +90,11 @@ according to Isabelle/Scala plugin option "jedit_font_reset_size" (cf. keyboard shortcut C+0). +* More reactive and less intrusive completion. Plain words need to be +at least 3 characters long to be completed (was 2 before). Symbols +are only completed in backslash forms, e.g. \forall or \ that +both produce the Isabelle symbol \ in its Unicode rendering. + *** Pure *** diff -r 16235bb41881 -r 082d0972096b etc/symbols --- a/etc/symbols Wed Aug 28 18:44:50 2013 +0200 +++ b/etc/symbols Wed Aug 28 23:48:45 2013 +0200 @@ -240,10 +240,10 @@ \ code: 0x002290 group: relation \ code: 0x002291 group: relation abbrev: [= \ code: 0x002292 group: relation abbrev: =] -\ code: 0x002229 group: operator abbrev: Int -\ code: 0x0022c2 group: operator abbrev: Inter -\ code: 0x00222a group: operator abbrev: Un -\ code: 0x0022c3 group: operator abbrev: Union +\ code: 0x002229 group: operator +\ code: 0x0022c2 group: operator +\ code: 0x00222a group: operator +\ code: 0x0022c3 group: operator \ code: 0x002294 group: operator \ code: 0x002a06 group: operator \ code: 0x002293 group: operator diff -r 16235bb41881 -r 082d0972096b src/HOL/Hoare_Parallel/Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Wed Aug 28 23:48:45 2013 +0200 @@ -40,15 +40,15 @@ edge but has not yet colored the new target. *} definition Redirect_Edge :: "gar_coll_state ann_com" where - "Redirect_Edge \ .{\Mut_init \ \z}. \\E:=\E[R:=(fst(\E!R), T)],, \z:= (\\z)\" + "Redirect_Edge \ \\Mut_init \ \z\ \\E:=\E[R:=(fst(\E!R), T)],, \z:= (\\z)\" definition Color_Target :: "gar_coll_state ann_com" where - "Color_Target \ .{\Mut_init \ \\z}. \\M:=\M[T:=Black],, \z:= (\\z)\" + "Color_Target \ \\Mut_init \ \\z\ \\M:=\M[T:=Black],, \z:= (\\z)\" definition Mutator :: "gar_coll_state ann_com" where "Mutator \ - .{\Mut_init \ \z}. - WHILE True INV .{\Mut_init \ \z}. + \\Mut_init \ \z\ + WHILE True INV \\Mut_init \ \z\ DO Redirect_Edge ;; Color_Target OD" subsubsection {* Correctness of the mutator *} @@ -64,14 +64,14 @@ done lemma Color_Target: - "\ Color_Target .{\Mut_init \ \z}." + "\ Color_Target \\Mut_init \ \z\" apply (unfold mutator_defs) apply annhoare apply(simp_all) done lemma Mutator: - "\ Mutator .{False}." + "\ Mutator \False\" apply(unfold Mutator_def) apply annhoare apply(simp_all add:Redirect_Edge Color_Target) @@ -101,21 +101,21 @@ definition Blacken_Roots :: " gar_coll_state ann_com" where "Blacken_Roots \ - .{\Proper}. + \\Proper\ \ind:=0;; - .{\Proper \ \ind=0}. + \\Proper \ \ind=0\ WHILE \indM - INV .{\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \ind\length \M}. - DO .{\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \indM}. + INV \\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \ind\length \M\ + DO \\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \indM\ IF \ind\Roots THEN - .{\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \indM \ \ind\Roots}. + \\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \indM \ \ind\Roots\ \M:=\M[\ind:=Black] FI;; - .{\Proper \ (\i<\ind+1. i \ Roots \ \M!i=Black) \ \indM}. + \\Proper \ (\i<\ind+1. i \ Roots \ \M!i=Black) \ \indM\ \ind:=\ind+1 OD" lemma Blacken_Roots: - "\ Blacken_Roots .{\Proper \ Roots\Blacks \M}." + "\ Blacken_Roots \\Proper \ Roots\Blacks \M\" apply (unfold Blacken_Roots_def) apply annhoare apply(simp_all add:collector_defs Graph_defs) @@ -135,28 +135,28 @@ definition Propagate_Black_aux :: "gar_coll_state ann_com" where "Propagate_Black_aux \ - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M}. + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M\ \ind:=0;; - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \ind=0}. + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \ind=0\ WHILE \indE - INV .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \ind\length \E}. - DO .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE}. + INV \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \ind\length \E\ + DO \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE\ IF \M!(fst (\E!\ind)) = Black THEN - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE \ \M!fst(\E!\ind)=Black}. + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE \ \M!fst(\E!\ind)=Black\ \M:=\M[snd(\E!\ind):=Black];; - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv (\ind + 1) \ \indE}. + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv (\ind + 1) \ \indE\ \ind:=\ind+1 FI OD" lemma Propagate_Black_aux: "\ Propagate_Black_aux - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ ( \obc < Blacks \M \ \Safe)}." + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ ( \obc < Blacks \M \ \Safe)\" apply (unfold Propagate_Black_aux_def PBInv_def collector_defs) apply annhoare apply(simp_all add:Graph6 Graph7 Graph8 Graph12) @@ -215,32 +215,32 @@ definition Propagate_Black :: " gar_coll_state ann_com" where "Propagate_Black \ - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M}. + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M\ \ind:=0;; - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \ind=0}. + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \ind=0\ WHILE \indE - INV .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \ind\length \E}. - DO .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE}. + INV \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \ind\length \E\ + DO \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE\ IF (\M!(fst (\E!\ind)))=Black THEN - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE \ (\M!fst(\E!\ind))=Black}. + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE \ (\M!fst(\E!\ind))=Black\ \k:=(snd(\E!\ind));; - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \PBInv \ind \ \indE \ (\M!fst(\E!\ind))=Black - \ \Auxk}. + \ \Auxk\ \\M:=\M[\k:=Black],, \ind:=\ind+1\ - ELSE .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE}. + ELSE \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE\ \IF (\M!(fst (\E!\ind)))\Black THEN \ind:=\ind+1 FI\ FI OD" lemma Propagate_Black: "\ Propagate_Black - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ ( \obc < Blacks \M \ \Safe)}." + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ ( \obc < Blacks \M \ \Safe)\" apply (unfold Propagate_Black_def PBInv_def Auxk_def collector_defs) apply annhoare apply(simp_all add: Graph6 Graph7 Graph8 Graph12) @@ -325,42 +325,42 @@ definition Count :: " gar_coll_state ann_com" where "Count \ - .{\Proper \ Roots\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe) \ \bc={}}. + \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe) \ \bc={}\ \ind:=0;; - .{\Proper \ Roots\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe) \ \bc={} - \ \ind=0}. + \ \ind=0\ WHILE \indM - INV .{\Proper \ Roots\Blacks \M + INV \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \CountInv \ind - \ ( \obc < Blacks \Ma \ \Safe) \ \ind\length \M}. - DO .{\Proper \ Roots\Blacks \M + \ ( \obc < Blacks \Ma \ \Safe) \ \ind\length \M\ + DO \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \CountInv \ind - \ ( \obc < Blacks \Ma \ \Safe) \ \indM}. + \ ( \obc < Blacks \Ma \ \Safe) \ \indM\ IF \M!\ind=Black - THEN .{\Proper \ Roots\Blacks \M + THEN \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \CountInv \ind - \ ( \obc < Blacks \Ma \ \Safe) \ \indM \ \M!\ind=Black}. + \ ( \obc < Blacks \Ma \ \Safe) \ \indM \ \M!\ind=Black\ \bc:=insert \ind \bc FI;; - .{\Proper \ Roots\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \CountInv (\ind+1) - \ ( \obc < Blacks \Ma \ \Safe) \ \indM}. + \ ( \obc < Blacks \Ma \ \Safe) \ \indM\ \ind:=\ind+1 OD" lemma Count: "\ Count - .{\Proper \ Roots\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\\bc \ \bc\Blacks \M \ length \Ma=length \M - \ (\obc < Blacks \Ma \ \Safe)}." + \ (\obc < Blacks \Ma \ \Safe)\" apply(unfold Count_def) apply annhoare apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs) @@ -392,24 +392,24 @@ definition Append :: "gar_coll_state ann_com" where "Append \ - .{\Proper \ Roots\Blacks \M \ \Safe}. + \\Proper \ Roots\Blacks \M \ \Safe\ \ind:=0;; - .{\Proper \ Roots\Blacks \M \ \Safe \ \ind=0}. + \\Proper \ Roots\Blacks \M \ \Safe \ \ind=0\ WHILE \indM - INV .{\Proper \ \AppendInv \ind \ \ind\length \M}. - DO .{\Proper \ \AppendInv \ind \ \indM}. + INV \\Proper \ \AppendInv \ind \ \ind\length \M\ + DO \\Proper \ \AppendInv \ind \ \indM\ IF \M!\ind=Black THEN - .{\Proper \ \AppendInv \ind \ \indM \ \M!\ind=Black}. + \\Proper \ \AppendInv \ind \ \indM \ \M!\ind=Black\ \M:=\M[\ind:=White] - ELSE .{\Proper \ \AppendInv \ind \ \indM \ \ind\Reach \E}. + ELSE \\Proper \ \AppendInv \ind \ \indM \ \ind\Reach \E\ \E:=Append_to_free(\ind,\E) FI;; - .{\Proper \ \AppendInv (\ind+1) \ \indM}. + \\Proper \ \AppendInv (\ind+1) \ \indM\ \ind:=\ind+1 OD" lemma Append: - "\ Append .{\Proper}." + "\ Append \\Proper\" apply(unfold Append_def AppendInv_def) apply annhoare apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) @@ -433,30 +433,30 @@ definition Collector :: " gar_coll_state ann_com" where "Collector \ -.{\Proper}. - WHILE True INV .{\Proper}. +\\Proper\ + WHILE True INV \\Proper\ DO Blacken_Roots;; - .{\Proper \ Roots\Blacks \M}. + \\Proper \ Roots\Blacks \M\ \obc:={};; - .{\Proper \ Roots\Blacks \M \ \obc={}}. + \\Proper \ Roots\Blacks \M \ \obc={}\ \bc:=Roots;; - .{\Proper \ Roots\Blacks \M \ \obc={} \ \bc=Roots}. + \\Proper \ Roots\Blacks \M \ \obc={} \ \bc=Roots\ \Ma:=M_init;; - .{\Proper \ Roots\Blacks \M \ \obc={} \ \bc=Roots \ \Ma=M_init}. + \\Proper \ Roots\Blacks \M \ \obc={} \ \bc=Roots \ \Ma=M_init\ WHILE \obc\\bc - INV .{\Proper \ Roots\Blacks \M + INV \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\\bc \ \bc\Blacks \M - \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe)}. - DO .{\Proper \ Roots\Blacks \M \ \bc\Blacks \M}. + \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe)\ + DO \\Proper \ Roots\Blacks \M \ \bc\Blacks \M\ \obc:=\bc;; Propagate_Black;; - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ (\obc < Blacks \M \ \Safe)}. + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ (\obc < Blacks \M \ \Safe)\ \Ma:=\M;; - .{\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma + \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M - \ ( \obc < Blacks \Ma \ \Safe)}. + \ ( \obc < Blacks \Ma \ \Safe)\ \bc:={};; Count OD;; @@ -464,7 +464,7 @@ OD" lemma Collector: - "\ Collector .{False}." + "\ Collector \False\" apply(unfold Collector_def) apply annhoare apply(simp_all add: Blacken_Roots Propagate_Black Count Append) @@ -806,15 +806,15 @@ text {* In total there are 289 verification conditions. *} lemma Gar_Coll: - "\- .{\Proper \ \Mut_init \ \z}. + "\- \\Proper \ \Mut_init \ \z\ COBEGIN Collector - .{False}. + \False\ \ Mutator - .{False}. + \False\ COEND - .{False}." + \False\" apply oghoare apply(force simp add: Mutator_def Collector_def modules) apply(rule Collector) diff -r 16235bb41881 -r 082d0972096b src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Wed Aug 28 23:48:45 2013 +0200 @@ -32,21 +32,21 @@ definition Mul_Redirect_Edge :: "nat \ nat \ mul_gar_coll_state ann_com" where "Mul_Redirect_Edge j n \ - .{\Mul_mut_init n \ Z (\Muts!j)}. + \\Mul_mut_init n \ Z (\Muts!j)\ \IF T(\Muts!j) \ Reach \E THEN \E:= \E[R (\Muts!j):= (fst (\E!R(\Muts!j)), T (\Muts!j))] FI,, \Muts:= \Muts[j:= (\Muts!j) \Z:=False\]\" definition Mul_Color_Target :: "nat \ nat \ mul_gar_coll_state ann_com" where "Mul_Color_Target j n \ - .{\Mul_mut_init n \ \ Z (\Muts!j)}. + \\Mul_mut_init n \ \ Z (\Muts!j)\ \\M:=\M[T (\Muts!j):=Black],, \Muts:=\Muts[j:= (\Muts!j) \Z:=True\]\" definition Mul_Mutator :: "nat \ nat \ mul_gar_coll_state ann_com" where "Mul_Mutator j n \ - .{\Mul_mut_init n \ Z (\Muts!j)}. + \\Mul_mut_init n \ Z (\Muts!j)\ WHILE True - INV .{\Mul_mut_init n \ Z (\Muts!j)}. + INV \\Mul_mut_init n \ Z (\Muts!j)\ DO Mul_Redirect_Edge j n ;; Mul_Color_Target j n OD" @@ -67,7 +67,7 @@ lemma Mul_Color_Target: "0\j \ j \ Mul_Color_Target j n - .{\Mul_mut_init n \ Z (\Muts!j)}." + \\Mul_mut_init n \ Z (\Muts!j)\" apply (unfold mul_mutator_defs) apply annhoare apply(simp_all) @@ -76,7 +76,7 @@ done lemma Mul_Mutator: "0\j \ j - \ Mul_Mutator j n .{False}." + \ Mul_Mutator j n \False\" apply(unfold Mul_Mutator_def) apply annhoare apply(simp_all add:Mul_Redirect_Edge Mul_Color_Target) @@ -139,13 +139,13 @@ subsubsection {* Modular Parameterized Mutators *} lemma Mul_Parameterized_Mutators: "0 - \- .{\Mul_mut_init n \ (\iMuts!i))}. + \- \\Mul_mut_init n \ (\iMuts!i))\ COBEGIN SCHEME [0\ j< n] Mul_Mutator j n - .{False}. + \False\ COEND - .{False}." + \False\" apply oghoare apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update) apply(erule Mul_Mutator) @@ -175,22 +175,22 @@ definition Mul_Blacken_Roots :: "nat \ mul_gar_coll_state ann_com" where "Mul_Blacken_Roots n \ - .{\Mul_Proper n}. + \\Mul_Proper n\ \ind:=0;; - .{\Mul_Proper n \ \ind=0}. + \\Mul_Proper n \ \ind=0\ WHILE \indM - INV .{\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \ind\length \M}. - DO .{\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \indM}. + INV \\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \ind\length \M\ + DO \\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \indM\ IF \ind\Roots THEN - .{\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \indM \ \ind\Roots}. + \\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \indM \ \ind\Roots\ \M:=\M[\ind:=Black] FI;; - .{\Mul_Proper n \ (\i<\ind+1. i\Roots \ \M!i=Black) \ \indM}. + \\Mul_Proper n \ (\i<\ind+1. i\Roots \ \M!i=Black) \ \indM\ \ind:=\ind+1 OD" lemma Mul_Blacken_Roots: "\ Mul_Blacken_Roots n - .{\Mul_Proper n \ Roots \ Blacks \M}." + \\Mul_Proper n \ Roots \ Blacks \M\" apply (unfold Mul_Blacken_Roots_def) apply annhoare apply(simp_all add:mul_collector_defs Graph_defs) @@ -213,40 +213,40 @@ definition Mul_Propagate_Black :: "nat \ mul_gar_coll_state ann_com" where "Mul_Propagate_Black n \ - .{\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \l\\Queue \ \obc\Blacks \M)}. + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ (\Safe \ \l\\Queue \ \obc\Blacks \M)\ \ind:=0;; - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ Blacks \M\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \l\\Queue \ \obc\Blacks \M) \ \ind=0}. + \ (\Safe \ \l\\Queue \ \obc\Blacks \M) \ \ind=0\ WHILE \indE - INV .{\Mul_Proper n \ Roots\Blacks \M + INV \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \Mul_PBInv \ \ind\length \E}. - DO .{\Mul_Proper n \ Roots\Blacks \M + \ \Mul_PBInv \ \ind\length \E\ + DO \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \Mul_PBInv \ \indE}. + \ \Mul_PBInv \ \indE\ IF \M!(fst (\E!\ind))=Black THEN - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \Mul_PBInv \ (\M!fst(\E!\ind))=Black \ \indE}. + \ \Mul_PBInv \ (\M!fst(\E!\ind))=Black \ \indE\ \k:=snd(\E!\ind);; - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ (\Safe \ \obc\Blacks \M \ \l<\Queue \ (\i<\ind. \BtoW(\E!i,\M)) \ \l\\Queue \ \Mul_Auxk ) \ \kM \ \M!fst(\E!\ind)=Black - \ \indE}. + \ \indE\ \\M:=\M[\k:=Black],,\ind:=\ind+1\ - ELSE .{\Mul_Proper n \ Roots\Blacks \M + ELSE \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \Mul_PBInv \ \indE}. + \ \Mul_PBInv \ \indE\ \IF \M!(fst (\E!\ind))\Black THEN \ind:=\ind+1 FI\ FI OD" lemma Mul_Propagate_Black: "\ Mul_Propagate_Black n - .{\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \obc\Blacks \M \ \l<\Queue \ (\l\\Queue \ \obc\Blacks \M))}." + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ (\Safe \ \obc\Blacks \M \ \l<\Queue \ (\l\\Queue \ \obc\Blacks \M))\" apply(unfold Mul_Propagate_Black_def) apply annhoare apply(simp_all add:Mul_PBInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def) @@ -295,51 +295,51 @@ definition Mul_Count :: "nat \ mul_gar_coll_state ann_com" where "Mul_Count n \ - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M) ) - \ \q \bc={}}. + \ \q \bc={}\ \ind:=0;; - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M) ) - \ \q \bc={} \ \ind=0}. + \ \q \bc={} \ \ind=0\ WHILE \indM - INV .{\Mul_Proper n \ Roots\Blacks \M + INV \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \Mul_CountInv \ind \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \ind\length \M}. - DO .{\Mul_Proper n \ Roots\Blacks \M + \ \q \ind\length \M\ + DO \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \Mul_CountInv \ind \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \indM}. + \ \q \indM\ IF \M!\ind=Black - THEN .{\Mul_Proper n \ Roots\Blacks \M + THEN \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \Mul_CountInv \ind \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \indM \ \M!\ind=Black}. + \ \q \indM \ \M!\ind=Black\ \bc:=insert \ind \bc FI;; - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \Mul_CountInv (\ind+1) \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \indM}. + \ \q \indM\ \ind:=\ind+1 OD" lemma Mul_Count: "\ Mul_Count n - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ Blacks \Ma\\bc \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \q" apply (unfold Mul_Count_def) apply annhoare apply(simp_all add:Mul_CountInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def) @@ -393,26 +393,26 @@ definition Mul_Append :: "nat \ mul_gar_coll_state ann_com" where "Mul_Append n \ - .{\Mul_Proper n \ Roots\Blacks \M \ \Safe}. + \\Mul_Proper n \ Roots\Blacks \M \ \Safe\ \ind:=0;; - .{\Mul_Proper n \ Roots\Blacks \M \ \Safe \ \ind=0}. + \\Mul_Proper n \ Roots\Blacks \M \ \Safe \ \ind=0\ WHILE \indM - INV .{\Mul_Proper n \ \Mul_AppendInv \ind \ \ind\length \M}. - DO .{\Mul_Proper n \ \Mul_AppendInv \ind \ \indM}. + INV \\Mul_Proper n \ \Mul_AppendInv \ind \ \ind\length \M\ + DO \\Mul_Proper n \ \Mul_AppendInv \ind \ \indM\ IF \M!\ind=Black THEN - .{\Mul_Proper n \ \Mul_AppendInv \ind \ \indM \ \M!\ind=Black}. + \\Mul_Proper n \ \Mul_AppendInv \ind \ \indM \ \M!\ind=Black\ \M:=\M[\ind:=White] ELSE - .{\Mul_Proper n \ \Mul_AppendInv \ind \ \indM \ \ind\Reach \E}. + \\Mul_Proper n \ \Mul_AppendInv \ind \ \indM \ \ind\Reach \E\ \E:=Append_to_free(\ind,\E) FI;; - .{\Mul_Proper n \ \Mul_AppendInv (\ind+1) \ \indM}. + \\Mul_Proper n \ \Mul_AppendInv (\ind+1) \ \indM\ \ind:=\ind+1 OD" lemma Mul_Append: "\ Mul_Append n - .{\Mul_Proper n}." + \\Mul_Proper n\" apply(unfold Mul_Append_def) apply annhoare apply(simp_all add: mul_collector_defs Mul_AppendInv_def @@ -431,52 +431,52 @@ definition Mul_Collector :: "nat \ mul_gar_coll_state ann_com" where "Mul_Collector n \ -.{\Mul_Proper n}. -WHILE True INV .{\Mul_Proper n}. +\\Mul_Proper n\ +WHILE True INV \\Mul_Proper n\ DO Mul_Blacken_Roots n ;; -.{\Mul_Proper n \ Roots\Blacks \M}. +\\Mul_Proper n \ Roots\Blacks \M\ \obc:={};; -.{\Mul_Proper n \ Roots\Blacks \M \ \obc={}}. +\\Mul_Proper n \ Roots\Blacks \M \ \obc={}\ \bc:=Roots;; -.{\Mul_Proper n \ Roots\Blacks \M \ \obc={} \ \bc=Roots}. +\\Mul_Proper n \ Roots\Blacks \M \ \obc={} \ \bc=Roots\ \l:=0;; -.{\Mul_Proper n \ Roots\Blacks \M \ \obc={} \ \bc=Roots \ \l=0}. +\\Mul_Proper n \ Roots\Blacks \M \ \obc={} \ \bc=Roots \ \l=0\ WHILE \lMul_Proper n \ Roots\Blacks \M \ \bc\Blacks \M \ - (\Safe \ (\l\\Queue \ \bc\Blacks \M) \ \lMul_Proper n \ Roots\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \l\\Queue \ \bc\Blacks \M)}. + INV \\Mul_Proper n \ Roots\Blacks \M \ \bc\Blacks \M \ + (\Safe \ (\l\\Queue \ \bc\Blacks \M) \ \l + DO \\Mul_Proper n \ Roots\Blacks \M \ \bc\Blacks \M + \ (\Safe \ \l\\Queue \ \bc\Blacks \M)\ \obc:=\bc;; Mul_Propagate_Black n;; - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ (\Safe \ \obc\Blacks \M \ \l<\Queue - \ (\l\\Queue \ \obc\Blacks \M))}. + \ (\l\\Queue \ \obc\Blacks \M))\ \bc:={};; - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ (\Safe \ \obc\Blacks \M \ \l<\Queue - \ (\l\\Queue \ \obc\Blacks \M)) \ \bc={}}. + \ (\l\\Queue \ \obc\Blacks \M)) \ \bc={}\ \ \Ma:=\M,, \q:=\Queue \;; Mul_Count n;; - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ Blacks \Ma\\bc \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \q IF \obc=\bc THEN - .{\Mul_Proper n \ Roots\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ Blacks \Ma\\bc \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \obc=\bc}. + \ \q \obc=\bc\ \l:=\l+1 - ELSE .{\Mul_Proper n \ Roots\Blacks \M + ELSE \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ Blacks \Ma\\bc \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \obc\\bc}. + \ \q \obc\\bc\ \l:=0 FI OD;; Mul_Append n @@ -488,7 +488,7 @@ lemma Mul_Collector: "\ Mul_Collector n - .{False}." + \False\" apply(unfold Mul_Collector_def) apply annhoare apply(simp_all only:pre.simps Mul_Blacken_Roots @@ -1237,16 +1237,16 @@ text {* The total number of verification conditions is 328 *} lemma Mul_Gar_Coll: - "\- .{\Mul_Proper n \ \Mul_mut_init n \ (\iMuts!i))}. + "\- \\Mul_Proper n \ \Mul_mut_init n \ (\iMuts!i))\ COBEGIN Mul_Collector n - .{False}. + \False\ \ SCHEME [0\ j< n] Mul_Mutator j n - .{False}. + \False\ COEND - .{False}." + \False\" apply oghoare --{* Strengthening the precondition *} apply(rule Int_greatest) diff -r 16235bb41881 -r 082d0972096b src/HOL/Hoare_Parallel/OG_Examples.thy --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Wed Aug 28 23:48:45 2013 +0200 @@ -16,30 +16,30 @@ hold :: nat lemma Petersons_mutex_1: - "\- .{\pr1=0 \ \\in1 \ \pr2=0 \ \\in2 }. - COBEGIN .{\pr1=0 \ \\in1}. - WHILE True INV .{\pr1=0 \ \\in1}. + "\- \\pr1=0 \ \\in1 \ \pr2=0 \ \\in2 \ + COBEGIN \\pr1=0 \ \\in1\ + WHILE True INV \\pr1=0 \ \\in1\ DO - .{\pr1=0 \ \\in1}. \ \in1:=True,,\pr1:=1 \;; - .{\pr1=1 \ \in1}. \ \hold:=1,,\pr1:=2 \;; - .{\pr1=2 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)}. + \\pr1=0 \ \\in1\ \ \in1:=True,,\pr1:=1 \;; + \\pr1=1 \ \in1\ \ \hold:=1,,\pr1:=2 \;; + \\pr1=2 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)\ AWAIT (\\in2 \ \(\hold=1)) THEN \pr1:=3 END;; - .{\pr1=3 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)}. + \\pr1=3 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)\ \\in1:=False,,\pr1:=0\ - OD .{\pr1=0 \ \\in1}. + OD \\pr1=0 \ \\in1\ \ - .{\pr2=0 \ \\in2}. - WHILE True INV .{\pr2=0 \ \\in2}. + \\pr2=0 \ \\in2\ + WHILE True INV \\pr2=0 \ \\in2\ DO - .{\pr2=0 \ \\in2}. \ \in2:=True,,\pr2:=1 \;; - .{\pr2=1 \ \in2}. \ \hold:=2,,\pr2:=2 \;; - .{\pr2=2 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))}. + \\pr2=0 \ \\in2\ \ \in2:=True,,\pr2:=1 \;; + \\pr2=1 \ \in2\ \ \hold:=2,,\pr2:=2 \;; + \\pr2=2 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))\ AWAIT (\\in1 \ \(\hold=2)) THEN \pr2:=3 END;; - .{\pr2=3 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))}. + \\pr2=3 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))\ \\in2:=False,,\pr2:=0\ - OD .{\pr2=0 \ \\in2}. + OD \\pr2=0 \ \\in2\ COEND - .{\pr1=0 \ \\in1 \ \pr2=0 \ \\in2}." + \\pr1=0 \ \\in1 \ \pr2=0 \ \\in2\" apply oghoare --{* 104 verification conditions. *} apply auto @@ -57,37 +57,37 @@ after2 :: bool lemma Busy_wait_mutex: - "\- .{True}. + "\- \True\ \flag1:=False,, \flag2:=False,, - COBEGIN .{\\flag1}. + COBEGIN \\\flag1\ WHILE True - INV .{\\flag1}. - DO .{\\flag1}. \ \flag1:=True,,\after1:=False \;; - .{\flag1 \ \\after1}. \ \turn:=1,,\after1:=True \;; - .{\flag1 \ \after1 \ (\turn=1 \ \turn=2)}. + INV \\\flag1\ + DO \\\flag1\ \ \flag1:=True,,\after1:=False \;; + \\flag1 \ \\after1\ \ \turn:=1,,\after1:=True \;; + \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ WHILE \(\flag2 \ \turn=2) - INV .{\flag1 \ \after1 \ (\turn=1 \ \turn=2)}. - DO .{\flag1 \ \after1 \ (\turn=1 \ \turn=2)}. SKIP OD;; - .{\flag1 \ \after1 \ (\flag2 \ \after2 \ \turn=2)}. + INV \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ + DO \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ SKIP OD;; + \\flag1 \ \after1 \ (\flag2 \ \after2 \ \turn=2)\ \flag1:=False OD - .{False}. + \False\ \ - .{\\flag2}. + \\\flag2\ WHILE True - INV .{\\flag2}. - DO .{\\flag2}. \ \flag2:=True,,\after2:=False \;; - .{\flag2 \ \\after2}. \ \turn:=2,,\after2:=True \;; - .{\flag2 \ \after2 \ (\turn=1 \ \turn=2)}. + INV \\\flag2\ + DO \\\flag2\ \ \flag2:=True,,\after2:=False \;; + \\flag2 \ \\after2\ \ \turn:=2,,\after2:=True \;; + \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ WHILE \(\flag1 \ \turn=1) - INV .{\flag2 \ \after2 \ (\turn=1 \ \turn=2)}. - DO .{\flag2 \ \after2 \ (\turn=1 \ \turn=2)}. SKIP OD;; - .{\flag2 \ \after2 \ (\flag1 \ \after1 \ \turn=1)}. + INV \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ + DO \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ SKIP OD;; + \\flag2 \ \after2 \ (\flag1 \ \after1 \ \turn=1)\ \flag2:=False OD - .{False}. + \False\ COEND - .{False}." + \False\" apply oghoare --{* 122 vc *} apply auto @@ -100,21 +100,21 @@ who :: nat lemma Semaphores_mutex: - "\- .{i\j}. + "\- \i\j\ \out:=True ,, - COBEGIN .{i\j}. - WHILE True INV .{i\j}. - DO .{i\j}. AWAIT \out THEN \out:=False,, \who:=i END;; - .{\\out \ \who=i \ i\j}. \out:=True OD - .{False}. + COBEGIN \i\j\ + WHILE True INV \i\j\ + DO \i\j\ AWAIT \out THEN \out:=False,, \who:=i END;; + \\\out \ \who=i \ i\j\ \out:=True OD + \False\ \ - .{i\j}. - WHILE True INV .{i\j}. - DO .{i\j}. AWAIT \out THEN \out:=False,,\who:=j END;; - .{\\out \ \who=j \ i\j}. \out:=True OD - .{False}. + \i\j\ + WHILE True INV \i\j\ + DO \i\j\ AWAIT \out THEN \out:=False,,\who:=j END;; + \\\out \ \who=j \ i\j\ \out:=True OD + \False\ COEND - .{False}." + \False\" apply oghoare --{* 38 vc *} apply auto @@ -123,17 +123,17 @@ subsubsection {* Peterson's Algorithm III: Parameterized version: *} lemma Semaphores_parameterized_mutex: - "0 \- .{True}. + "0 \- \True\ \out:=True ,, COBEGIN SCHEME [0\ i< n] - .{True}. - WHILE True INV .{True}. - DO .{True}. AWAIT \out THEN \out:=False,, \who:=i END;; - .{\\out \ \who=i}. \out:=True OD - .{False}. + \True\ + WHILE True INV \True\ + DO \True\ AWAIT \out THEN \out:=False,, \who:=i END;; + \\\out \ \who=i\ \out:=True OD + \False\ COEND - .{False}." + \False\" apply oghoare --{* 20 vc *} apply auto @@ -150,22 +150,22 @@ lemma Ticket_mutex: "\ 0n=length \turn \ 0<\nextv \ (\k l. k l k\l \ \turn!k < \num \ (\turn!k =0 \ \turn!k\\turn!l))\ \ - \ \- .{n=length \turn}. + \ \- \n=length \turn\ \index:= 0,, - WHILE \index < n INV .{n=length \turn \ (\i<\index. \turn!i=0)}. + WHILE \index < n INV \n=length \turn \ (\i<\index. \turn!i=0)\ DO \turn:= \turn[\index:=0],, \index:=\index +1 OD,, \num:=1 ,, \nextv:=1 ,, COBEGIN SCHEME [0\ i< n] - .{\I}. - WHILE True INV .{\I}. - DO .{\I}. \ \turn :=\turn[i:=\num],, \num:=\num+1 \;; - .{\I}. WAIT \turn!i=\nextv END;; - .{\I \ \turn!i=\nextv}. \nextv:=\nextv+1 + \\I\ + WHILE True INV \\I\ + DO \\I\ \ \turn :=\turn[i:=\num],, \num:=\num+1 \;; + \\I\ WAIT \turn!i=\nextv END;; + \\I \ \turn!i=\nextv\ \nextv:=\nextv+1 OD - .{False}. + \False\ COEND - .{False}." + \False\" apply oghoare --{* 35 vc *} apply simp_all @@ -259,40 +259,40 @@ \ (\\found \ a<\ x \ f(\x)\0) \ ; I2= \\y\a+1 \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) \ (\\found \ \y\a \ f(\y)\0) \ \ \ - \- .{\ u. f(u)=0}. + \- \\ u. f(u)=0\ \turn:=1,, \found:= False,, \x:=a,, \y:=a+1 ,, - COBEGIN .{\I1}. + COBEGIN \\I1\ WHILE \\found - INV .{\I1}. - DO .{a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)}. + INV \\I1\ + DO \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ WAIT \turn=1 END;; - .{a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)}. + \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ \turn:=2;; - .{a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)}. + \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ \ \x:=\x+1,, IF f(\x)=0 THEN \found:=True ELSE SKIP FI\ OD;; - .{\I1 \ \found}. + \\I1 \ \found\ \turn:=2 - .{\I1 \ \found}. + \\I1 \ \found\ \ - .{\I2}. + \\I2\ WHILE \\found - INV .{\I2}. - DO .{\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)}. + INV \\I2\ + DO \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ WAIT \turn=2 END;; - .{\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)}. + \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ \turn:=1;; - .{\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)}. + \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ \ \y:=(\y - 1),, IF f(\y)=0 THEN \found:=True ELSE SKIP FI\ OD;; - .{\I2 \ \found}. + \\I2 \ \found\ \turn:=1 - .{\I2 \ \found}. + \\I2 \ \found\ COEND - .{f(\x)=0 \ f(\y)=0}." + \f(\x)=0 \ f(\y)=0\" apply oghoare --{* 98 verification conditions *} apply auto @@ -306,26 +306,26 @@ \ (\\found \ a<\x \ f(\x)\0)\; I2= \\y\a+1 \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) \ (\\found \ \y\a \ f(\y)\0)\\ \ - \- .{\u. f(u)=0}. + \- \\u. f(u)=0\ \found:= False,, \x:=a,, \y:=a+1,, - COBEGIN .{\I1}. + COBEGIN \\I1\ WHILE \\found - INV .{\I1}. - DO .{a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)}. + INV \\I1\ + DO \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ \ \x:=\x+1,,IF f(\x)=0 THEN \found:=True ELSE SKIP FI\ OD - .{\I1 \ \found}. + \\I1 \ \found\ \ - .{\I2}. + \\I2\ WHILE \\found - INV .{\I2}. - DO .{\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)}. + INV \\I2\ + DO \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ \ \y:=(\y - 1),,IF f(\y)=0 THEN \found:=True ELSE SKIP FI\ OD - .{\I2 \ \found}. + \\I2 \ \found\ COEND - .{f(\x)=0 \ f(\y)=0}." + \f(\x)=0 \ f(\y)=0\" apply oghoare --{* 20 vc *} apply auto @@ -390,44 +390,44 @@ p1= \\I1 \ \li=\ins\ ; I2 = \\I \ (\k<\lj. (a ! k)=(\b ! k)) \ \lj\length a\ ; p2 = \\I2 \ \lj=\outs\ \ \ - \- .{\INIT}. + \- \\INIT\ \ins:=0,, \outs:=0,, \li:=0,, \lj:=0,, - COBEGIN .{\p1 \ \INIT}. + COBEGIN \\p1 \ \INIT\ WHILE \li p1 \ \INIT}. - DO .{\p1 \ \INIT \ \li\p1 \ \INIT\ + DO \\p1 \ \INIT \ \li \vx:= (a ! \li);; - .{\p1 \ \INIT \ \li \vx=(a ! \li)}. + \\p1 \ \INIT \ \li \vx=(a ! \li)\ WAIT \ins-\outs < length \buffer END;; - .{\p1 \ \INIT \ \li \vx=(a ! \li) - \ \ins-\outs < length \buffer}. + \\p1 \ \INIT \ \li \vx=(a ! \li) + \ \ins-\outs < length \buffer\ \buffer:=(list_update \buffer (\ins mod (length \buffer)) \vx);; - .{\p1 \ \INIT \ \li\p1 \ \INIT \ \li (a ! \li)=(\buffer ! (\ins mod (length \buffer))) - \ \ins-\outs buffer}. + \ \ins-\outs buffer\ \ins:=\ins+1;; - .{\I1 \ \INIT \ (\li+1)=\ins \ \li\I1 \ \INIT \ (\li+1)=\ins \ \li \li:=\li+1 OD - .{\p1 \ \INIT \ \li=length a}. + \\p1 \ \INIT \ \li=length a\ \ - .{\p2 \ \INIT}. + \\p2 \ \INIT\ WHILE \lj < length a - INV .{\p2 \ \INIT}. - DO .{\p2 \ \lj \INIT}. + INV \\p2 \ \INIT\ + DO \\p2 \ \lj \INIT\ WAIT \outs<\ins END;; - .{\p2 \ \lj \outs<\ins \ \INIT}. + \\p2 \ \lj \outs<\ins \ \INIT\ \vy:=(\buffer ! (\outs mod (length \buffer)));; - .{\p2 \ \lj \outs<\ins \ \vy=(a ! \lj) \ \INIT}. + \\p2 \ \lj \outs<\ins \ \vy=(a ! \lj) \ \INIT\ \outs:=\outs+1;; - .{\I2 \ (\lj+1)=\outs \ \lj \vy=(a ! \lj) \ \INIT}. + \\I2 \ (\lj+1)=\outs \ \lj \vy=(a ! \lj) \ \INIT\ \b:=(list_update \b \lj \vy);; - .{\I2 \ (\lj+1)=\outs \ \lj (a ! \lj)=(\b ! \lj) \ \INIT}. + \\I2 \ (\lj+1)=\outs \ \lj (a ! \lj)=(\b ! \lj) \ \INIT\ \lj:=\lj+1 OD - .{\p2 \ \lj=length a \ \INIT}. + \\p2 \ \lj=length a \ \INIT\ COEND - .{ \kb ! k)}." + \ \kb ! k)\" apply oghoare --{* 138 vc *} apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) @@ -455,9 +455,9 @@ a :: "nat \ nat" lemma Example1: - "\- .{True}. - COBEGIN SCHEME [0\ia:=\a (i:=0) .{\a i=0}. COEND - .{\i < n. \a i = 0}." + "\- \True\ + COBEGIN SCHEME [0\iTrue\ \a:=\a (i:=0) \\a i=0\ COEND + \\i < n. \a i = 0\" apply oghoare apply simp_all done @@ -466,11 +466,11 @@ record Example1_list = A :: "nat list" lemma Example1_list: - "\- .{n < length \A}. + "\- \n < length \A\ COBEGIN - SCHEME [0\iA}. \A:=\A[i:=0] .{\A!i=0}. + SCHEME [0\in < length \A\ \A:=\A[i:=0] \\A!i=0\ COEND - .{\i < n. \A!i = 0}." + \\i < n. \A!i = 0\" apply oghoare apply force+ done @@ -525,14 +525,14 @@ x :: nat lemma Example_2: "0 - \- .{\x=0 \ (\i=0..c i)=0}. + \- \\x=0 \ (\i=0..c i)=0\ COBEGIN SCHEME [0\ix=(\i=0..c i) \ \c i=0}. + \\x=(\i=0..c i) \ \c i=0\ \ \x:=\x+(Suc 0),, \c:=\c (i:=(Suc 0)) \ - .{\x=(\i=0..c i) \ \c i=(Suc 0)}. + \\x=(\i=0..c i) \ \c i=(Suc 0)\ COEND - .{\x=n}." + \\x=n\" apply oghoare apply (simp_all cong del: strong_setsum_cong) apply (tactic {* ALLGOALS (clarify_tac @{context}) *}) diff -r 16235bb41881 -r 082d0972096b src/HOL/Hoare_Parallel/OG_Syntax.thy --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Wed Aug 28 23:48:45 2013 +0200 @@ -44,15 +44,15 @@ ("(0WHILE _ //DO _ /OD)" [0, 0] 61) translations - "IF b THEN c1 ELSE c2 FI" \ "CONST Cond .{b}. c1 c2" + "IF b THEN c1 ELSE c2 FI" \ "CONST Cond \b\ c1 c2" "IF b THEN c FI" \ "IF b THEN c ELSE SKIP FI" - "WHILE b INV i DO c OD" \ "CONST While .{b}. i c" + "WHILE b INV i DO c OD" \ "CONST While \b\ i c" "WHILE b DO c OD" \ "WHILE b INV CONST undefined DO c OD" - "r IF b THEN c1 ELSE c2 FI" \ "CONST AnnCond1 r .{b}. c1 c2" - "r IF b THEN c FI" \ "CONST AnnCond2 r .{b}. c" - "r WHILE b INV i DO c OD" \ "CONST AnnWhile r .{b}. i c" - "r AWAIT b THEN c END" \ "CONST AnnAwait r .{b}. c" + "r IF b THEN c1 ELSE c2 FI" \ "CONST AnnCond1 r \b\ c1 c2" + "r IF b THEN c FI" \ "CONST AnnCond2 r \b\ c" + "r WHILE b INV i DO c OD" \ "CONST AnnWhile r \b\ i c" + "r AWAIT b THEN c END" \ "CONST AnnAwait r \b\ c" "r \c\" \ "r AWAIT CONST True THEN c END" "r WAIT b END" \ "r AWAIT b THEN SKIP END" diff -r 16235bb41881 -r 082d0972096b src/HOL/Hoare_Parallel/Quote_Antiquote.thy --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Wed Aug 28 23:48:45 2013 +0200 @@ -6,13 +6,10 @@ syntax "_quote" :: "'b \ ('a \ 'b)" ("(\_\)" [0] 1000) "_antiquote" :: "('a \ 'b) \ 'b" ("\_" [1000] 1000) - "_Assert" :: "'a \ 'a set" ("(.{_}.)" [0] 1000) - -syntax (xsymbols) - "_Assert" :: "'a \ 'a set" ("(\_\)" [0] 1000) + "_Assert" :: "'a \ 'a set" ("(\_\)" [0] 1000) translations - ".{b}." \ "CONST Collect \b\" + "\b\" \ "CONST Collect \b\" parse_translation {* let diff -r 16235bb41881 -r 082d0972096b src/HOL/Hoare_Parallel/RG_Syntax.thy --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Wed Aug 28 23:48:45 2013 +0200 @@ -20,10 +20,10 @@ translations "\x := a" \ "CONST Basic \\(_update_name x (\_. a))\" - "IF b THEN c1 ELSE c2 FI" \ "CONST Cond .{b}. c1 c2" + "IF b THEN c1 ELSE c2 FI" \ "CONST Cond \b\ c1 c2" "IF b THEN c FI" \ "IF b THEN c ELSE SKIP FI" - "WHILE b DO c OD" \ "CONST While .{b}. c" - "AWAIT b THEN c END" \ "CONST Await .{b}. c" + "WHILE b DO c OD" \ "CONST While \b\ c" + "AWAIT b THEN c END" \ "CONST Await \b\ c" "\c\" \ "AWAIT CONST True THEN c END" "WAIT b END" \ "AWAIT b THEN SKIP END" diff -r 16235bb41881 -r 082d0972096b src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Library/Infinite_Set.thy Wed Aug 28 23:48:45 2013 +0200 @@ -16,20 +16,18 @@ lemmas may not work well with @{text "blast"}. *} -abbreviation - infinite :: "'a set \ bool" where - "infinite S == \ finite S" +abbreviation infinite :: "'a set \ bool" + where "infinite S \ \ finite S" text {* Infinite sets are non-empty, and if we remove some elements from an infinite set, the result is still infinite. *} -lemma infinite_imp_nonempty: "infinite S ==> S \ {}" +lemma infinite_imp_nonempty: "infinite S \ S \ {}" by auto -lemma infinite_remove: - "infinite S \ infinite (S - {a})" +lemma infinite_remove: "infinite S \ infinite (S - {a})" by simp lemma Diff_infinite_finite: @@ -72,7 +70,7 @@ lemma finite_nat_bounded: assumes S: "finite (S::nat set)" shows "\k. S \ {..k. ?bounded S k") -using S + using S proof induct have "?bounded {} 0" by simp then show "\k. ?bounded {} k" .. @@ -92,7 +90,7 @@ qed lemma finite_nat_iff_bounded: - "finite (S::nat set) = (\k. S \ {.. (\k. S \ {.. ?rhs") proof assume ?lhs then show ?rhs by (rule finite_nat_bounded) @@ -104,7 +102,7 @@ qed lemma finite_nat_iff_bounded_le: - "finite (S::nat set) = (\k. S \ {..k})" (is "?lhs = ?rhs") + "finite (S::nat set) \ (\k. S \ {..k})" (is "?lhs \ ?rhs") proof assume ?lhs then obtain k where "S \ {..m. \n. m n\S)" - (is "?lhs = ?rhs") + "infinite (S::nat set) \ (\m. \n. m < n \ n \ S)" + (is "?lhs \ ?rhs") proof assume ?lhs show ?rhs proof (rule ccontr) assume "\ ?rhs" - then obtain m where m: "\n. m n\S" by blast + then obtain m where m: "\n. m < n \ n \ S" by blast then have "S \ {..m}" by (auto simp add: sym [OF linorder_not_less]) with `?lhs` show False @@ -139,22 +137,22 @@ assume "finite S" then obtain m where "S \ {..m}" by (auto simp add: finite_nat_iff_bounded_le) - then have "\n. m n\S" by auto + then have "\n. m < n \ n \ S" by auto with `?rhs` show False by blast qed qed lemma infinite_nat_iff_unbounded_le: - "infinite (S::nat set) = (\m. \n. m\n \ n\S)" - (is "?lhs = ?rhs") + "infinite (S::nat set) \ (\m. \n. m \ n \ n \ S)" + (is "?lhs \ ?rhs") proof assume ?lhs show ?rhs proof fix m - from `?lhs` obtain n where "m n\S" + from `?lhs` obtain n where "m < n \ n \ S" by (auto simp add: infinite_nat_iff_unbounded) - then have "m\n \ n\S" by simp + then have "m \ n \ n \ S" by simp then show "\n. m \ n \ n \ S" .. qed next @@ -162,9 +160,9 @@ show ?lhs proof (auto simp add: infinite_nat_iff_unbounded) fix m - from `?rhs` obtain n where "Suc m \ n \ n\S" + from `?rhs` obtain n where "Suc m \ n \ n \ S" by blast - then have "m n\S" by simp + then have "m < n \ n \ S" by simp then show "\n. m < n \ n \ S" .. qed qed @@ -176,18 +174,18 @@ *} lemma unbounded_k_infinite: - assumes k: "\m. k (\n. m n\S)" + assumes k: "\m. k < m \ (\n. m < n \ n \ S)" shows "infinite (S::nat set)" proof - { - fix m have "\n. m n\S" - proof (cases "kn. m < n \ n \ S" + proof (cases "k < m") case True with k show ?thesis by blast next case False - from k obtain n where "Suc k < n \ n\S" by auto - with False have "m n\S" by auto + from k obtain n where "Suc k < n \ n \ S" by auto + with False have "m < n \ n \ S" by auto then show ?thesis .. qed } @@ -217,13 +215,14 @@ then show False by simp qed -lemma int_infinite [simp]: - shows "infinite (UNIV::int set)" +lemma int_infinite [simp]: "infinite (UNIV::int set)" proof - - from inj_int have "infinite (range int)" by (rule range_inj_infinite) + from inj_int have "infinite (range int)" + by (rule range_inj_infinite) moreover have "range int \ (UNIV::int set)" by simp - ultimately show "infinite (UNIV::int set)" by (simp add: infinite_super) + ultimately show "infinite (UNIV::int set)" + by (simp add: infinite_super) qed text {* @@ -235,7 +234,7 @@ *} lemma linorder_injI: - assumes hyp: "!!x y. x < (y::'a::linorder) ==> f x \ f y" + assumes hyp: "\x y. x < (y::'a::linorder) \ f x \ f y" shows "inj f" proof (rule inj_onI) fix x y @@ -284,7 +283,8 @@ proof - fix n show "pick n \ Sseq n" - proof (unfold pick_def, rule someI_ex) + unfolding pick_def + proof (rule someI_ex) from Sseq_inf have "infinite (Sseq n)" . then have "Sseq n \ {}" by auto then show "\x. x \ Sseq n" by auto @@ -324,7 +324,7 @@ qed lemma infinite_iff_countable_subset: - "infinite S = (\f. inj (f::nat \ 'a) \ range f \ S)" + "infinite S \ (\f. inj (f::nat \ 'a) \ range f \ S)" by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super) text {* @@ -359,13 +359,11 @@ we introduce corresponding binders and their proof rules. *} -definition - Inf_many :: "('a \ bool) \ bool" (binder "INFM " 10) where - "Inf_many P = infinite {x. P x}" +definition Inf_many :: "('a \ bool) \ bool" (binder "INFM " 10) + where "Inf_many P \ infinite {x. P x}" -definition - Alm_all :: "('a \ bool) \ bool" (binder "MOST " 10) where - "Alm_all P = (\ (INFM x. \ P x))" +definition Alm_all :: "('a \ bool) \ bool" (binder "MOST " 10) + where "Alm_all P \ \ (INFM x. \ P x)" notation (xsymbols) Inf_many (binder "\\<^sub>\" 10) and @@ -397,15 +395,21 @@ unfolding Alm_all_def by simp lemma INFM_EX: "(\\<^sub>\x. P x) \ (\x. P x)" - by (erule contrapos_pp, simp) + apply (erule contrapos_pp) + apply simp + done lemma ALL_MOST: "\x. P x \ \\<^sub>\x. P x" by simp -lemma INFM_E: assumes "INFM x. P x" obtains x where "P x" +lemma INFM_E: + assumes "INFM x. P x" + obtains x where "P x" using INFM_EX [OF assms] by (rule exE) -lemma MOST_I: assumes "\x. P x" shows "MOST x. P x" +lemma MOST_I: + assumes "\x. P x" + shows "MOST x. P x" using assms by simp lemma INFM_mono: @@ -476,15 +480,18 @@ text {* Properties of quantifiers with injective functions. *} -lemma INFM_inj: - "INFM x. P (f x) \ inj f \ INFM x. P x" +lemma INFM_inj: "INFM x. P (f x) \ inj f \ INFM x. P x" unfolding INFM_iff_infinite - by (clarify, drule (1) finite_vimageI, simp) + apply clarify + apply (drule (1) finite_vimageI) + apply simp + done -lemma MOST_inj: - "MOST x. P x \ inj f \ MOST x. P (f x)" +lemma MOST_inj: "MOST x. P x \ inj f \ MOST x. P (f x)" unfolding MOST_iff_cofinite - by (drule (1) finite_vimageI, simp) + apply (drule (1) finite_vimageI) + apply simp + done text {* Properties of quantifiers with singletons. *} @@ -515,16 +522,16 @@ text {* Properties of quantifiers over the naturals. *} -lemma INFM_nat: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m P n)" +lemma INFM_nat: "(\\<^sub>\n. P (n::nat)) \ (\m. \n. m < n \ P n)" by (simp add: Inf_many_def infinite_nat_iff_unbounded) -lemma INFM_nat_le: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m\n \ P n)" +lemma INFM_nat_le: "(\\<^sub>\n. P (n::nat)) \ (\m. \n. m \ n \ P n)" by (simp add: Inf_many_def infinite_nat_iff_unbounded_le) -lemma MOST_nat: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m P n)" +lemma MOST_nat: "(\\<^sub>\n. P (n::nat)) \ (\m. \n. m < n \ P n)" by (simp add: Alm_all_def INFM_nat) -lemma MOST_nat_le: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m\n \ P n)" +lemma MOST_nat_le: "(\\<^sub>\n. P (n::nat)) \ (\m. \n. m \ n \ P n)" by (simp add: Alm_all_def INFM_nat_le) @@ -534,20 +541,20 @@ The set's element type must be wellordered (e.g. the natural numbers). *} -primrec (in wellorder) enumerate :: "'a set \ nat \ 'a" where - enumerate_0: "enumerate S 0 = (LEAST n. n \ S)" - | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \ S}) n" +primrec (in wellorder) enumerate :: "'a set \ nat \ 'a" +where + enumerate_0: "enumerate S 0 = (LEAST n. n \ S)" +| enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \ S}) n" -lemma enumerate_Suc': - "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n" +lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n" by simp lemma enumerate_in_set: "infinite S \ enumerate S n : S" -apply (induct n arbitrary: S) - apply (fastforce intro: LeastI dest!: infinite_imp_nonempty) -apply simp -apply (metis DiffE infinite_remove) -done + apply (induct n arbitrary: S) + apply (fastforce intro: LeastI dest!: infinite_imp_nonempty) + apply simp + apply (metis DiffE infinite_remove) + done declare enumerate_0 [simp del] enumerate_Suc [simp del] @@ -573,31 +580,38 @@ shows "n \ enumerate S n" using S proof (induct n) + case 0 + then show ?case by simp +next case (Suc n) then have "n \ enumerate S n" by simp also note enumerate_mono[of n "Suc n", OF _ `infinite S`] finally show ?case by simp -qed simp +qed lemma enumerate_Suc'': fixes S :: "'a::wellorder set" - shows "infinite S \ enumerate S (Suc n) = (LEAST s. s \ S \ enumerate S n < s)" + assumes "infinite S" + shows "enumerate S (Suc n) = (LEAST s. s \ S \ enumerate S n < s)" + using assms proof (induct n arbitrary: S) case 0 - then have "\s\S. enumerate S 0 \ s" + then have "\s \ S. enumerate S 0 \ s" by (auto simp: enumerate.simps intro: Least_le) then show ?case unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"] - by (intro arg_cong[where f=Least] ext) auto + by (intro arg_cong[where f = Least] ext) auto next case (Suc n S) show ?case using enumerate_mono[OF zero_less_Suc `infinite S`, of n] `infinite S` apply (subst (1 2) enumerate_Suc') apply (subst Suc) - apply (insert `infinite S`, simp) - by (intro arg_cong[where f=Least] ext) - (auto simp: enumerate_Suc'[symmetric]) + using `infinite S` + apply simp + apply (intro arg_cong[where f = Least] ext) + apply (auto simp: enumerate_Suc'[symmetric]) + done qed lemma enumerate_Ex: @@ -609,9 +623,12 @@ proof cases let ?y = "Max {s'\S. s' < s}" assume "\y\S. y < s" - then have y: "\x. ?y < x \ (\s'\S. s' < s \ s' < x)" by (subst Max_less_iff) auto - then have y_in: "?y \ {s'\S. s' < s}" by (intro Max_in) auto - with less.hyps[of ?y] obtain n where "enumerate S n = ?y" by auto + then have y: "\x. ?y < x \ (\s'\S. s' < s \ s' < x)" + by (subst Max_less_iff) auto + then have y_in: "?y \ {s'\S. s' < s}" + by (intro Max_in) auto + with less.hyps[of ?y] obtain n where "enumerate S n = ?y" + by auto with S have "enumerate S (Suc n) = s" by (auto simp: y less enumerate_Suc'' intro!: Least_equality) then show ?case by auto @@ -632,7 +649,7 @@ using enumerate_mono[OF _ `infinite S`] by (auto simp: neq_iff) then have "inj (enumerate S)" by (auto simp: inj_on_def) - moreover have "\s\S. \i. enumerate S i = s" + moreover have "\s \ S. \i. enumerate S i = s" using enumerate_Ex[OF S] by auto moreover note `infinite S` ultimately show ?thesis @@ -646,9 +663,8 @@ These simplify the reasoning about deterministic automata. *} -definition - atmost_one :: "'a set \ bool" where - "atmost_one S = (\x y. x\S \ y\S \ x=y)" +definition atmost_one :: "'a set \ bool" + where "atmost_one S \ (\x y. x\S \ y\S \ x = y)" lemma atmost_one_empty: "S = {} \ atmost_one S" by (simp add: atmost_one_def) diff -r 16235bb41881 -r 082d0972096b src/HOL/Library/Lattice_Algebras.thy --- a/src/HOL/Library/Lattice_Algebras.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Library/Lattice_Algebras.thy Wed Aug 28 23:48:45 2013 +0200 @@ -9,20 +9,19 @@ class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf begin -lemma add_inf_distrib_left: - "a + inf b c = inf (a + b) (a + c)" -apply (rule antisym) -apply (simp_all add: le_infI) -apply (rule add_le_imp_le_left [of "uminus a"]) -apply (simp only: add_assoc [symmetric], simp) -apply rule -apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+ -done +lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)" + apply (rule antisym) + apply (simp_all add: le_infI) + apply (rule add_le_imp_le_left [of "uminus a"]) + apply (simp only: add_assoc [symmetric], simp) + apply rule + apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+ + done -lemma add_inf_distrib_right: - "inf a b + c = inf (a + c) (b + c)" +lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)" proof - - have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left) + have "c + inf a b = inf (c+a) (c+b)" + by (simp add: add_inf_distrib_left) thus ?thesis by (simp add: add_commute) qed @@ -31,19 +30,17 @@ class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup begin -lemma add_sup_distrib_left: - "a + sup b c = sup (a + b) (a + c)" -apply (rule antisym) -apply (rule add_le_imp_le_left [of "uminus a"]) -apply (simp only: add_assoc[symmetric], simp) -apply rule -apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+ -apply (rule le_supI) -apply (simp_all) -done +lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)" + apply (rule antisym) + apply (rule add_le_imp_le_left [of "uminus a"]) + apply (simp only: add_assoc[symmetric], simp) + apply rule + apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+ + apply (rule le_supI) + apply (simp_all) + done -lemma add_sup_distrib_right: - "sup a b + c = sup (a+c) (b+c)" +lemma add_sup_distrib_right: "sup a b + c = sup (a+c) (b+c)" proof - have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left) thus ?thesis by (simp add: add_commute) @@ -57,69 +54,61 @@ subclass semilattice_inf_ab_group_add .. subclass semilattice_sup_ab_group_add .. -lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left +lemmas add_sup_inf_distribs = + add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)" proof (rule inf_unique) - fix a b :: 'a + fix a b c :: 'a show "- sup (-a) (-b) \ a" by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) (simp, simp add: add_sup_distrib_left) -next - fix a b :: 'a show "- sup (-a) (-b) \ b" by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) (simp, simp add: add_sup_distrib_left) -next - fix a b c :: 'a assume "a \ b" "a \ c" - then show "a \ - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric]) - (simp add: le_supI) + then show "a \ - sup (-b) (-c)" + by (subst neg_le_iff_le [symmetric]) (simp add: le_supI) qed - + lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)" proof (rule sup_unique) - fix a b :: 'a + fix a b c :: 'a show "a \ - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) (simp, simp add: add_inf_distrib_left) -next - fix a b :: 'a show "b \ - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) (simp, simp add: add_inf_distrib_left) -next - fix a b c :: 'a assume "a \ c" "b \ c" - then show "- inf (-a) (-b) \ c" by (subst neg_le_iff_le [symmetric]) - (simp add: le_infI) + then show "- inf (-a) (-b) \ c" by (subst neg_le_iff_le [symmetric]) (simp add: le_infI) qed lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)" -by (simp add: inf_eq_neg_sup) + by (simp add: inf_eq_neg_sup) lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)" -by (simp add: sup_eq_neg_inf) + by (simp add: sup_eq_neg_inf) lemma add_eq_inf_sup: "a + b = sup a b + inf a b" proof - - have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute) - hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup) + have "0 = - inf 0 (a-b) + inf (a-b) 0" + by (simp add: inf_commute) + hence "0 = sup 0 (b-a) + inf (a-b) 0" + by (simp add: inf_eq_neg_sup) hence "0 = (-a + sup a b) + (inf a b + (-b))" - by (simp add: add_sup_distrib_left add_inf_distrib_right) - (simp add: algebra_simps) + by (simp add: add_sup_distrib_left add_inf_distrib_right) (simp add: algebra_simps) thus ?thesis by (simp add: algebra_simps) qed + subsection {* Positive Part, Negative Part, Absolute Value *} -definition - nprt :: "'a \ 'a" where - "nprt x = inf x 0" +definition nprt :: "'a \ 'a" + where "nprt x = inf x 0" -definition - pprt :: "'a \ 'a" where - "pprt x = sup x 0" +definition pprt :: "'a \ 'a" + where "pprt x = sup x 0" lemma pprt_neg: "pprt (- x) = - nprt x" proof - @@ -137,27 +126,29 @@ qed lemma prts: "a = pprt a + nprt a" -by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) + by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) lemma zero_le_pprt[simp]: "0 \ pprt a" -by (simp add: pprt_def) + by (simp add: pprt_def) lemma nprt_le_zero[simp]: "nprt a \ 0" -by (simp add: nprt_def) + by (simp add: nprt_def) lemma le_eq_neg: "a \ - b \ a + b \ 0" (is "?l = ?r") -proof - - have a: "?l \ ?r" - apply (auto) +proof + assume ?l + then show ?r + apply - apply (rule add_le_imp_le_right[of _ "uminus b" _]) apply (simp add: add_assoc) done - have b: "?r \ ?l" - apply (auto) +next + assume ?r + then show ?l + apply - apply (rule add_le_imp_le_right[of _ "b" _]) - apply (simp) + apply simp done - from a b show ?thesis by blast qed lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def) @@ -181,7 +172,7 @@ fix a::'a assume hyp: "sup a (-a) = 0" hence "sup a (-a) + a = a" by (simp) - hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) + hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) hence "sup (a+a) 0 <= a" by (simp) hence "0 <= a" by (blast intro: order_trans inf_sup_ord) } @@ -192,16 +183,22 @@ qed lemma inf_0_imp_0: "inf a (-a) = 0 \ a = 0" -apply (simp add: inf_eq_neg_sup) -apply (simp add: sup_commute) -apply (erule sup_0_imp_0) -done + apply (simp add: inf_eq_neg_sup) + apply (simp add: sup_commute) + apply (erule sup_0_imp_0) + done lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \ a = 0" -by (rule, erule inf_0_imp_0) simp + apply rule + apply (erule inf_0_imp_0) + apply simp + done lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \ a = 0" -by (rule, erule sup_0_imp_0) simp + apply rule + apply (erule sup_0_imp_0) + apply simp + done lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \ a + a \ 0 \ a" @@ -218,39 +215,48 @@ show "0 <= a + a" by (simp add: add_mono[OF a a, simplified]) qed -lemma double_zero [simp]: - "a + a = 0 \ a = 0" +lemma double_zero [simp]: "a + a = 0 \ a = 0" proof assume assm: "a + a = 0" then have "a + a + - a = - a" by simp then have "a + (a + - a) = - a" by (simp only: add_assoc) then have a: "- a = a" by simp - show "a = 0" apply (rule antisym) - apply (unfold neg_le_iff_le [symmetric, of a]) - unfolding a apply simp - unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] - unfolding assm unfolding le_less apply simp_all done + show "a = 0" + apply (rule antisym) + apply (unfold neg_le_iff_le [symmetric, of a]) + unfolding a + apply simp + unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] + unfolding assm + unfolding le_less + apply simp_all + done next - assume "a = 0" then show "a + a = 0" by simp + assume "a = 0" + then show "a + a = 0" by simp qed -lemma zero_less_double_add_iff_zero_less_single_add [simp]: - "0 < a + a \ 0 < a" +lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \ 0 < a" proof (cases "a = 0") - case True then show ?thesis by auto + case True + then show ?thesis by auto next - case False then show ?thesis (*FIXME tune proof*) - unfolding less_le apply simp apply rule - apply clarify - apply rule - apply assumption - apply (rule notI) - unfolding double_zero [symmetric, of a] apply simp - done + case False + then show ?thesis + unfolding less_le + apply simp + apply rule + apply clarify + apply rule + apply assumption + apply (rule notI) + unfolding double_zero [symmetric, of a] + apply simp + done qed lemma double_add_le_zero_iff_single_add_le_zero [simp]: - "a + a \ 0 \ a \ 0" + "a + a \ 0 \ a \ 0" proof - have "a + a \ 0 \ 0 \ - (a + a)" by (subst le_minus_iff, simp) moreover have "\ \ a \ 0" by simp @@ -270,7 +276,7 @@ lemma le_minus_self_iff: "a \ - a \ a \ 0" proof - from add_le_cancel_left [of "uminus a" "plus a a" zero] - have "(a <= -a) = (a+a <= 0)" + have "(a <= -a) = (a+a <= 0)" by (simp add: add_assoc[symmetric]) thus ?thesis by simp qed @@ -278,28 +284,28 @@ lemma minus_le_self_iff: "- a \ a \ 0 \ a" proof - from add_le_cancel_left [of "uminus a" zero "plus a a"] - have "(-a <= a) = (0 <= a+a)" + have "(-a <= a) = (0 <= a+a)" by (simp add: add_assoc[symmetric]) thus ?thesis by simp qed lemma zero_le_iff_zero_nprt: "0 \ a \ nprt a = 0" -unfolding le_iff_inf by (simp add: nprt_def inf_commute) + unfolding le_iff_inf by (simp add: nprt_def inf_commute) lemma le_zero_iff_zero_pprt: "a \ 0 \ pprt a = 0" -unfolding le_iff_sup by (simp add: pprt_def sup_commute) + unfolding le_iff_sup by (simp add: pprt_def sup_commute) lemma le_zero_iff_pprt_id: "0 \ a \ pprt a = a" -unfolding le_iff_sup by (simp add: pprt_def sup_commute) + unfolding le_iff_sup by (simp add: pprt_def sup_commute) lemma zero_le_iff_nprt_id: "a \ 0 \ nprt a = a" -unfolding le_iff_inf by (simp add: nprt_def inf_commute) + unfolding le_iff_inf by (simp add: nprt_def inf_commute) lemma pprt_mono [simp, no_atp]: "a \ b \ pprt a \ pprt b" -unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a]) + unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a]) lemma nprt_mono [simp, no_atp]: "a \ b \ nprt a \ nprt b" -unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a]) + unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a]) end @@ -320,8 +326,7 @@ then have "0 \ sup a (- a)" unfolding abs_lattice . then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1) then show ?thesis - by (simp add: add_sup_inf_distribs sup_aci - pprt_def nprt_def diff_minus abs_lattice) + by (simp add: add_sup_inf_distribs sup_aci pprt_def nprt_def diff_minus abs_lattice) qed subclass ordered_ab_group_add_abs @@ -329,8 +334,10 @@ have abs_ge_zero [simp]: "\a. 0 \ \a\" proof - fix a b - have a: "a \ \a\" and b: "- a \ \a\" by (auto simp add: abs_lattice) - show "0 \ \a\" by (rule add_mono [OF a b, simplified]) + have a: "a \ \a\" and b: "- a \ \a\" + by (auto simp add: abs_lattice) + show "0 \ \a\" + by (rule add_mono [OF a b, simplified]) qed have abs_leI: "\a b. a \ b \ - a \ b \ \a\ \ b" by (simp add: abs_lattice le_supI) @@ -340,18 +347,25 @@ by (auto simp add: abs_lattice) show "\-a\ = \a\" by (simp add: abs_lattice sup_commute) - show "a \ b \ - a \ b \ \a\ \ b" by (fact abs_leI) + { + assume "a \ b" + then show "- a \ b \ \a\ \ b" + by (rule abs_leI) + } show "\a + b\ \ \a\ + \b\" proof - have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus) - have a:"a+b <= sup ?m ?n" by (simp) - have b:"-a-b <= ?n" by (simp) - have c:"?n <= sup ?m ?n" by (simp) - from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) + have a: "a + b <= sup ?m ?n" by simp + have b: "- a - b <= ?n" by simp + have c: "?n <= sup ?m ?n" by simp + from b c have d: "-a-b <= sup ?m ?n" by (rule order_trans) have e:"-a-b = -(a+b)" by (simp add: diff_minus) - from a d e have "abs(a+b) <= sup ?m ?n" - by (drule_tac abs_leI, auto) + from a d e have "abs(a+b) <= sup ?m ?n" + apply - + apply (drule abs_leI) + apply auto + done with g[symmetric] show ?thesis by simp qed qed @@ -370,10 +384,10 @@ lemma abs_if_lattice: fixes a :: "'a\{lattice_ab_group_add_abs, linorder}" shows "\a\ = (if a < 0 then - a else a)" -by auto + by auto lemma estimate_by_abs: - "a + b <= (c::'a::lattice_ab_group_add_abs) \ a <= c + abs b" + "a + b <= (c::'a::lattice_ab_group_add_abs) \ a <= c + abs b" proof - assume "a+b <= c" then have "a <= c+(-b)" by (simp add: algebra_simps) @@ -390,7 +404,7 @@ end -lemma abs_le_mult: "abs (a * b) \ (abs a) * (abs (b::'a::lattice_ring))" +lemma abs_le_mult: "abs (a * b) \ (abs a) * (abs (b::'a::lattice_ring))" proof - let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b" let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" @@ -398,11 +412,11 @@ by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps) { fix u v :: 'a - have bh: "\u = a; v = b\ \ - u * v = pprt a * pprt b + pprt a * nprt b + + have bh: "\u = a; v = b\ \ + u * v = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" apply (subst prts[of u], subst prts[of v]) - apply (simp add: algebra_simps) + apply (simp add: algebra_simps) done } note b = this[OF refl[of a] refl[of b]] @@ -432,7 +446,7 @@ show "abs (a*b) = abs a * abs b" proof - have s: "(0 <= a*b) | (a*b <= 0)" - apply (auto) + apply (auto) apply (rule_tac split_mult_pos_le) apply (rule_tac contrapos_np[of "a*b <= 0"]) apply (simp) @@ -448,8 +462,8 @@ then show ?thesis apply (simp_all add: mulprts abs_prts) apply (insert a) - apply (auto simp add: - algebra_simps + apply (auto simp add: + algebra_simps iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt] iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id]) apply(drule (1) mult_nonneg_nonpos[of a b], simp) @@ -470,15 +484,14 @@ qed lemma mult_le_prts: - assumes - "a1 <= (a::'a::lattice_ring)" - "a <= a2" - "b1 <= b" - "b <= b2" - shows - "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" -proof - - have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" + assumes "a1 <= (a::'a::lattice_ring)" + and "a <= a2" + and "b1 <= b" + and "b <= b2" + shows "a * b <= + pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" +proof - + have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" apply (subst prts[symmetric])+ apply simp done @@ -496,7 +509,7 @@ by simp qed moreover have "nprt a * pprt b <= nprt a2 * pprt b1" - proof - + proof - have "nprt a * pprt b <= nprt a2 * pprt b" by (simp add: mult_right_mono assms) moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1" @@ -514,29 +527,33 @@ by simp qed ultimately show ?thesis - by - (rule add_mono | simp)+ + apply - + apply (rule add_mono | simp)+ + done qed lemma mult_ge_prts: - assumes - "a1 <= (a::'a::lattice_ring)" - "a <= a2" - "b1 <= b" - "b <= b2" - shows - "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1" -proof - - from assms have a1:"- a2 <= -a" by auto - from assms have a2: "-a <= -a1" by auto - from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg] - have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp + assumes "a1 <= (a::'a::lattice_ring)" + and "a <= a2" + and "b1 <= b" + and "b <= b2" + shows "a * b >= + nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1" +proof - + from assms have a1:"- a2 <= -a" + by auto + from assms have a2: "-a <= -a1" + by auto + from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg] + have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" + by simp then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b" by (simp only: minus_le_iff) then show ?thesis by simp qed instance int :: lattice_ring -proof +proof fix k :: int show "abs k = sup k (- k)" by (auto simp add: sup_int_def) diff -r 16235bb41881 -r 082d0972096b src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Library/Permutation.thy Wed Aug 28 23:48:45 2013 +0200 @@ -8,13 +8,12 @@ imports Multiset begin -inductive - perm :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) - where - Nil [intro!]: "[] <~~> []" - | swap [intro!]: "y # x # l <~~> x # y # l" - | Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys" - | trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs" +inductive perm :: "'a list \ 'a list \ bool" ("_ <~~> _" [50, 50] 50) (* FIXME proper infix, without ambiguity!? *) +where + Nil [intro!]: "[] <~~> []" +| swap [intro!]: "y # x # l <~~> x # y # l" +| Cons [intro!]: "xs <~~> ys \ z # xs <~~> z # ys" +| trans [intro]: "xs <~~> ys \ ys <~~> zs \ xs <~~> zs" lemma perm_refl [iff]: "l <~~> l" by (induct l) auto @@ -22,7 +21,7 @@ subsection {* Some examples of rule induction on permutations *} -lemma xperm_empty_imp: "[] <~~> ys ==> ys = []" +lemma xperm_empty_imp: "[] <~~> ys \ ys = []" by (induct xs == "[]::'a list" ys pred: perm) simp_all @@ -30,13 +29,13 @@ \medskip This more general theorem is easier to understand! *} -lemma perm_length: "xs <~~> ys ==> length xs = length ys" +lemma perm_length: "xs <~~> ys \ length xs = length ys" by (induct pred: perm) simp_all -lemma perm_empty_imp: "[] <~~> xs ==> xs = []" +lemma perm_empty_imp: "[] <~~> xs \ xs = []" by (drule perm_length) auto -lemma perm_sym: "xs <~~> ys ==> ys <~~> xs" +lemma perm_sym: "xs <~~> ys \ ys <~~> xs" by (induct pred: perm) auto @@ -64,10 +63,10 @@ apply (blast intro!: perm_append_single intro: perm_sym) done -lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys" +lemma perm_append1: "xs <~~> ys \ l @ xs <~~> l @ ys" by (induct l) auto -lemma perm_append2: "xs <~~> ys ==> xs @ l <~~> ys @ l" +lemma perm_append2: "xs <~~> ys \ xs @ l <~~> ys @ l" by (blast intro!: perm_append_swap perm_append1) @@ -81,7 +80,7 @@ apply (erule perm_sym [THEN perm_empty_imp]) done -lemma perm_sing_imp: "ys <~~> xs ==> xs = [y] ==> ys = [y]" +lemma perm_sing_imp: "ys <~~> xs \ xs = [y] \ ys = [y]" by (induct pred: perm) auto lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])" @@ -93,29 +92,26 @@ subsection {* Removing elements *} -lemma perm_remove: "x \ set ys ==> ys <~~> x # remove1 x ys" +lemma perm_remove: "x \ set ys \ ys <~~> x # remove1 x ys" by (induct ys) auto text {* \medskip Congruence rule *} -lemma perm_remove_perm: "xs <~~> ys ==> remove1 z xs <~~> remove1 z ys" +lemma perm_remove_perm: "xs <~~> ys \ remove1 z xs <~~> remove1 z ys" by (induct pred: perm) auto lemma remove_hd [simp]: "remove1 z (z # xs) = xs" by auto -lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys" +lemma cons_perm_imp_perm: "z # xs <~~> z # ys \ xs <~~> ys" by (drule_tac z = z in perm_remove_perm) auto lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)" by (blast intro: cons_perm_imp_perm) -lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys ==> xs <~~> ys" - apply (induct zs arbitrary: xs ys rule: rev_induct) - apply (simp_all (no_asm_use)) - apply blast - done +lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys \ xs <~~> ys" + by (induct zs arbitrary: xs ys rule: rev_induct) auto lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)" by (blast intro: append_perm_imp_perm perm_append1) @@ -135,38 +131,38 @@ apply (induct_tac xs, auto) apply (erule_tac x = "remove1 a x" in allE, drule sym, simp) apply (subgoal_tac "a \ set x") - apply (drule_tac z=a in perm.Cons) + apply (drule_tac z = a in perm.Cons) apply (erule perm.trans, rule perm_sym, erule perm_remove) apply (drule_tac f=set_of in arg_cong, simp) done -lemma multiset_of_le_perm_append: - "multiset_of xs \ multiset_of ys \ (\zs. xs @ zs <~~> ys)" +lemma multiset_of_le_perm_append: "multiset_of xs \ multiset_of ys \ (\zs. xs @ zs <~~> ys)" apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) apply (insert surj_multiset_of, drule surjD) apply (blast intro: sym)+ done -lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys" +lemma perm_set_eq: "xs <~~> ys \ set xs = set ys" by (metis multiset_of_eq_perm multiset_of_eq_setD) -lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys" +lemma perm_distinct_iff: "xs <~~> ys \ distinct xs = distinct ys" apply (induct pred: perm) apply simp_all apply fastforce apply (metis perm_set_eq) done -lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys" +lemma eq_set_perm_remdups: "set xs = set ys \ remdups xs <~~> remdups ys" apply (induct xs arbitrary: ys rule: length_induct) - apply (case_tac "remdups xs", simp, simp) - apply (subgoal_tac "a : set (remdups ys)") + apply (case_tac "remdups xs") + apply simp_all + apply (subgoal_tac "a \ set (remdups ys)") prefer 2 apply (metis set.simps(2) insert_iff set_remdups) apply (drule split_list) apply(elim exE conjE) apply (drule_tac x=list in spec) apply(erule impE) prefer 2 apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2 apply simp - apply (subgoal_tac "a#list <~~> a#ysa@zs") + apply (subgoal_tac "a # list <~~> a # ysa @ zs") apply (metis Cons_eq_appendI perm_append_Cons trans) apply (metis Cons Cons_eq_appendI distinct.simps(2) distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff) @@ -180,21 +176,23 @@ apply (rule length_remdups_leq) done -lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)" +lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \ (set x = set y)" by (metis List.set_remdups perm_set_eq eq_set_perm_remdups) lemma permutation_Ex_bij: assumes "xs <~~> ys" shows "\f. bij_betw f {.. (\ii Suc ` {.. Suc ` {..iif"] conjI allI impI) + proof (intro exI[of _ "g \ f"] conjI allI impI) show "bij_betw (g \ f) {.. f) i" - using trans(1,3)[THEN perm_length] perm by force + using trans(1,3)[THEN perm_length] perm by auto qed qed diff -r 16235bb41881 -r 082d0972096b src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Aug 28 23:48:45 2013 +0200 @@ -29,7 +29,8 @@ apply (cases "b=0") defer apply (rule divide_nonneg_pos) - using assms apply auto + using assms + apply auto done lemma brouwer_compactness_lemma: @@ -95,12 +96,15 @@ shows "setsum g C = setsum g A + setsum g B" using setsum_Un_disjoint[OF assms(1-3)] and assms(4) by auto -lemma kuhn_counting_lemma: assumes "finite faces" "finite simplices" - "\f\faces. bnd f \ (card {s \ simplices. face f s} = 1)" - "\f\faces. \ bnd f \ (card {s \ simplices. face f s} = 2)" - "\s\simplices. compo s \ (card {f \ faces. face f s \ compo' f} = 1)" - "\s\simplices. \ compo s \ (card {f \ faces. face f s \ compo' f} = 0) \ - (card {f \ faces. face f s \ compo' f} = 2)" +lemma kuhn_counting_lemma: + assumes + "finite faces" + "finite simplices" + "\f\faces. bnd f \ (card {s \ simplices. face f s} = 1)" + "\f\faces. \ bnd f \ (card {s \ simplices. face f s} = 2)" + "\s\simplices. compo s \ (card {f \ faces. face f s \ compo' f} = 1)" + "\s\simplices. \ compo s \ + (card {f \ faces. face f s \ compo' f} = 0) \ (card {f \ faces. face f s \ compo' f} = 2)" "odd(card {f \ faces. compo' f \ bnd f})" shows "odd(card {s \ simplices. compo s})" proof - @@ -117,28 +121,39 @@ using assms(1) apply (auto simp add: card_Un_Int, auto simp add:conj_commute) done - have lem2:"setsum (\j. card {f \ {f \ faces. compo' f \ bnd f}. face f j}) simplices = - 1 * card {f \ faces. compo' f \ bnd f}" - "setsum (\j. card {f \ {f \ faces. compo' f \ \ bnd f}. face f j}) simplices = - 2 * card {f \ faces. compo' f \ \ bnd f}" + have lem2: + "setsum (\j. card {f \ {f \ faces. compo' f \ bnd f}. face f j}) simplices = + 1 * card {f \ faces. compo' f \ bnd f}" + "setsum (\j. card {f \ {f \ faces. compo' f \ \ bnd f}. face f j}) simplices = + 2 * card {f \ faces. compo' f \ \ bnd f}" apply(rule_tac[!] setsum_multicount) using assms apply auto done - have lem3:"setsum (\s. card {f \ faces. face f s \ compo' f}) simplices = - setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. compo s}+ - setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. \ compo s}" - apply(rule setsum_Un_disjoint') using assms(2) by auto - have lem4:"setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. compo s} - = setsum (\s. 1) {s \ simplices. compo s}" - apply(rule setsum_cong2) using assms(5) by auto + have lem3: + "setsum (\s. card {f \ faces. face f s \ compo' f}) simplices = + setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. compo s}+ + setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. \ compo s}" + apply (rule setsum_Un_disjoint') + using assms(2) + apply auto + done + have lem4: "setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. compo s} = + setsum (\s. 1) {s \ simplices. compo s}" + apply (rule setsum_cong2) + using assms(5) + apply auto + done have lem5: "setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. \ compo s} = setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. (\ compo s) \ (card {f \ faces. face f s \ compo' f} = 0)} + setsum (\s. card {f \ faces. face f s \ compo' f}) {s \ simplices. (\ compo s) \ (card {f \ faces. face f s \ compo' f} = 2)}" - apply(rule setsum_Un_disjoint') using assms(2,6) by auto - have *:"int (\s\{s \ simplices. compo s}. card {f \ faces. face f s \ compo' f}) = + apply (rule setsum_Un_disjoint') + using assms(2,6) + apply auto + done + have *: "int (\s\{s \ simplices. compo s}. card {f \ faces. face f s \ compo' f}) = int (card {f \ faces. compo' f \ bnd f} + 2 * card {f \ faces. compo' f \ \ bnd f}) - int (card {s \ simplices. \ compo s \ card {f \ faces. face f s \ compo' f} = 2} * 2)" using lem1[unfolded lem3 lem2 lem5] by auto @@ -175,7 +190,8 @@ apply (rule as(2)[rule_format]) using as(1) apply auto done - show "card s = Suc 0" unfolding * using card_insert by auto + show "card s = Suc 0" + unfolding * using card_insert by auto qed auto lemma card_2_exists: "card s = 2 \ (\x\s. \y\s. x \ y \ (\z\s. (z = x) \ (z = y)))" @@ -227,7 +243,8 @@ apply (rule set_eqI) unfolding singleton_iff apply (rule, rule inj[unfolded inj_on_def, rule_format]) - unfolding a using a(2) and assms and inj[unfolded inj_on_def] apply auto + unfolding a using a(2) and assms and inj[unfolded inj_on_def] + apply auto done show ?thesis apply (rule image_lemma_0) @@ -245,7 +262,8 @@ then show ?thesis apply - apply (rule disjI1, rule image_lemma_0) - using assms(1) apply auto + using assms(1) + apply auto done next let ?M = "{a\s. f ` (s - {a}) = t - {b}}" @@ -317,7 +335,9 @@ using assms(3) by (auto intro: card_ge_0_finite) show "finite {f. \s\simplices. face f s}" unfolding assms(2)[rule_format] and * - apply (rule finite_UN_I[OF assms(1)]) using ** apply auto + apply (rule finite_UN_I[OF assms(1)]) + using ** + apply auto done have *: "\P f s. s\simplices \ (f \ {f. \s\simplices. \a\s. f = s - {a}}) \ (\a\s. (f = s - {a})) \ P f \ (\a\s. (f = s - {a}) \ P f)" by auto @@ -334,7 +354,8 @@ show "rl ` s = {0..n+1} \ card ?S = 1" "rl ` s \ {0..n+1} \ card ?S = 0 \ card ?S = 2" unfolding S apply(rule_tac[!] image_lemma_1 image_lemma_2) - using ** assms(4) and s apply auto + using ** assms(4) and s + apply auto done qed @@ -427,9 +448,9 @@ lemma pointwise_antisym: fixes x :: "nat \ nat" - shows "(\j. x j \ y j) \ (\j. y j \ x j) \ (x = y)" + shows "(\j. x j \ y j) \ (\j. y j \ x j) \ x = y" apply (rule, rule ext, erule conjE) - apply (erule_tac x=xa in allE)+ + apply (erule_tac x = xa in allE)+ apply auto done @@ -489,11 +510,12 @@ apply (rule pointwise_minimal_pointwise_maximal(1)[OF assms(1-2)]) apply (rule, rule) apply (drule_tac assms(3)[rule_format], assumption) - using kle_imp_pointwise apply auto + using kle_imp_pointwise + apply auto done then guess a .. note a = this show ?thesis - apply (rule_tac x=a in bexI) + apply (rule_tac x = a in bexI) proof fix x assume "x \ s" @@ -502,13 +524,14 @@ apply - proof (erule disjE) assume "kle n x a" - hence "x = a" + then have "x = a" apply - unfolding pointwise_antisym[symmetric] apply (drule kle_imp_pointwise) - using a(2)[rule_format,OF `x\s`] apply auto + using a(2)[rule_format,OF `x\s`] + apply auto done - thus ?thesis using kle_refl by auto + then show ?thesis using kle_refl by auto qed qed (insert a, auto) qed @@ -563,16 +586,18 @@ "m1 \ card {k\{1..n}. x k < y k}" "m2 \ card {k\{1..n}. y k < z k}" shows "kle n x z \ m1 + m2 \ card {k\{1..n}. x k < z k}" - apply (rule, rule kle_trans[OF assms(1-3)]) + apply (rule, rule kle_trans[OF assms(1-3)]) proof - have "\j. x j < y j \ x j < z j" apply (rule less_le_trans) - using kle_imp_pointwise[OF assms(2)] apply auto + using kle_imp_pointwise[OF assms(2)] + apply auto done moreover have "\j. y j < z j \ x j < z j" apply (rule le_less_trans) - using kle_imp_pointwise[OF assms(1)] apply auto + using kle_imp_pointwise[OF assms(1)] + apply auto done ultimately have *: "{k\{1..n}. x k < y k} \ {k\{1..n}. y k < z k} = {k\{1..n}. x k < z k}" @@ -653,12 +678,14 @@ have "1 \ card {k \ {1..n}. a k < x k}" "m \ card {k \ {1..n}. x k < b k}" apply (rule kle_strict_set) apply (rule a(2)[rule_format]) - using a and xb apply auto + using a and xb + apply auto done thus ?thesis apply (rule_tac x=a in bexI, rule_tac x=b in bexI) using kle_range_combine[OF a(2)[rule_format] xb(3) Suc(5)[rule_format], of 1 "m"] - using a(1) xb(1-2) apply auto + using a(1) xb(1-2) + apply auto done next case True @@ -691,7 +718,8 @@ show ?thesis unfolding kle_def apply (rule_tac x="kk1 \ kk2" in exI) - apply (rule) defer + apply rule + defer proof fix i show "c i = a i + (if i \ kk1 \ kk2 then 1 else 0)" @@ -742,7 +770,7 @@ lemma kle_adjacent: assumes "\j. b j = (if j = k then a(j) + 1 else a j)" "kle n a x" "kle n x b" - shows "(x = a) \ (x = b)" + shows "x = a \ x = b" proof (cases "x k = a k") case True show ?thesis @@ -757,17 +785,22 @@ using True apply auto done - thus "x j = a j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto + then show "x j = a j" + using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] by auto qed next case False show ?thesis apply(rule disjI2,rule ext) proof - fix j - have "x j \ b j" using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] - unfolding assms(1)[rule_format] apply-apply(cases "j=k") + have "x j \ b j" + using kle_imp_pointwise[OF assms(2),THEN spec[where x=j]] + unfolding assms(1)[rule_format] + apply - + apply(cases "j = k") using False by auto - thus "x j = b j" using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]] + then show "x j = b j" + using kle_imp_pointwise[OF assms(3),THEN spec[where x=j]] by auto qed qed @@ -818,16 +851,18 @@ using `s\{}` assm using kle_minimal[of s n] by auto obtain b where b: "b \ s" "\x\s. kle n x b" using `s\{}` assm using kle_maximal[of s n] by auto - obtain c d where c_d: "c\s" "d\s" "kle n c d" "n \ card {k \ {1..n}. c k < d k}" + obtain c d where c_d: "c \ s" "d \ s" "kle n c d" "n \ card {k \ {1..n}. c k < d k}" using kle_range_induct[of s n n] using assm by auto have "kle n c b \ n \ card {k \ {1..n}. c k < b k}" apply (rule kle_range_combine_r[where y=d]) - using c_d a b apply auto + using c_d a b + apply auto done hence "kle n a b \ n \ card {k\{1..n}. a(k) < b(k)}" apply - apply (rule kle_range_combine_l[where y=c]) - using a `c\s` `b\s` apply auto + using a `c \ s` `b \ s` + apply auto done moreover have "card {1..n} \ card {k\{1..n}. a(k) < b(k)}" @@ -897,16 +932,18 @@ case False then obtain b where b: "b\s" "\ kle n b a" "\x\{x \ s. \ kle n x a}. kle n b x" using kle_minimal[of "{x\s. \ kle n x a}" n] and assm by auto - hence **: "1 \ card {k\{1..n}. a k < b k}" + then have **: "1 \ card {k\{1..n}. a k < b k}" apply - apply (rule kle_strict_set) - using assm(6) and `a\s` apply (auto simp add:kle_refl) + using assm(6) and `a\s` + apply (auto simp add:kle_refl) done let ?kle1 = "{x \ s. \ kle n x a}" have "card ?kle1 > 0" apply (rule ccontr) - using assm(2) and False apply auto + using assm(2) and False + apply auto done hence sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)" using assm(2) by auto @@ -917,7 +954,8 @@ let ?kle2 = "{x \ s. kle n x a}" have "card ?kle2 > 0" apply (rule ccontr) - using assm(6)[rule_format,of a a] and `a\s` and assm(2) apply auto + using assm(6)[rule_format,of a a] and `a\s` and assm(2) + apply auto done hence sizekle2: "card ?kle2 = Suc (card ?kle2 - 1)" using assm(2) by auto @@ -940,11 +978,13 @@ by auto have "kle n e a \ card {x \ s. kle n x a} - 1 \ card {k \ {1..n}. e k < a k}" apply (rule kle_range_combine_r[where y=f]) - using e_f using `a\s` assm(6) apply auto + using e_f using `a\s` assm(6) + apply auto done moreover have "kle n b d \ card {x \ s. \ kle n x a} - 1 \ card {k \ {1..n}. b k < d k}" apply (rule kle_range_combine_l[where y=c]) - using c_d using assm(6) and b apply auto + using c_d using assm(6) and b + apply auto done hence "kle n a d \ 2 + (card {x \ s. \ kle n x a} - 1) \ card {k \ {1..n}. a k < d k}" apply - @@ -975,24 +1015,27 @@ have kkk: "k \ kk" apply (rule ccontr) using k(1) - unfolding kk apply auto + unfolding kk + apply auto done show "b j = (if j = k then a j + 1 else a j)" proof (cases "j \ kk") case True - hence "j = k" - apply - apply (rule k(2)[rule_format]) - using kk_raw kkk apply auto - done - thus ?thesis unfolding kk using kkk by auto + then have "j = k" + apply - + apply (rule k(2)[rule_format]) + using kk_raw kkk + apply auto + done + then show ?thesis unfolding kk using kkk by auto next case False - hence "j \ k" + then have "j \ k" using k(2)[rule_format, of j k] and kk_raw kkk by auto - thus ?thesis unfolding kk using kkk and False + then show ?thesis unfolding kk using kkk and False by auto qed - qed(insert k(1) `b\s`, auto) + qed (insert k(1) `b\s`, auto) qed lemma ksimplex_predecessor: @@ -1009,13 +1052,15 @@ hence **: "1 \ card {k\{1..n}. a k > b k}" apply - apply (rule kle_strict_set) - using assm(6) and `a\s` apply (auto simp add: kle_refl) + using assm(6) and `a\s` + apply (auto simp add: kle_refl) done let ?kle1 = "{x \ s. \ kle n a x}" have "card ?kle1 > 0" apply (rule ccontr) - using assm(2) and False apply auto + using assm(2) and False + apply auto done hence sizekle1: "card ?kle1 = Suc (card ?kle1 - 1)" using assm(2) by auto @@ -1026,7 +1071,8 @@ let ?kle2 = "{x \ s. kle n a x}" have "card ?kle2 > 0" apply (rule ccontr) - using assm(6)[rule_format,of a a] and `a\s` and assm(2) apply auto + using assm(6)[rule_format,of a a] and `a\s` and assm(2) + apply auto done hence sizekle2:"card ?kle2 = Suc (card ?kle2 - 1)" using assm(2) by auto @@ -1049,11 +1095,13 @@ by auto have "kle n a e \ card {x \ s. kle n a x} - 1 \ card {k \ {1..n}. e k > a k}" apply (rule kle_range_combine_l[where y=f]) - using e_f and `a\s` assm(6) apply auto + using e_f and `a\s` assm(6) + apply auto done moreover have "kle n d b \ card {x \ s. \ kle n a x} - 1 \ card {k \ {1..n}. b k > d k}" apply (rule kle_range_combine_r[where y=c]) - using c_d and assm(6) and b apply auto + using c_d and assm(6) and b + apply auto done hence "kle n d a \ (card {x \ s. \ kle n a x} - 1) + 2 \ card {k \ {1..n}. a k > d k}" apply - @@ -1063,7 +1111,8 @@ ultimately have "kle n d e \ (card ?kle1 - 1 + 2) + (card ?kle2 - 1) \ card {k\{1..n}. e k > d k}" apply - apply (rule kle_range_combine[where y=a]) - using assm(6)[rule_format,OF `e\s` `d\s`] apply blast+ + using assm(6)[rule_format,OF `e\s` `d\s`] + apply blast+ done moreover have "card {k \ {1..n}. e k > d k} \ card {1..n}" by (rule card_mono) auto @@ -1092,7 +1141,8 @@ hence "j = k" apply - apply (rule k(2)[rule_format]) - using kk_raw kkk apply auto + using kk_raw kkk + apply auto done thus ?thesis unfolding kk using kkk by auto next @@ -1115,14 +1165,14 @@ using assms apply - proof (induct m arbitrary: s) - have *:"{f. \x. f x = d} = {\x. d}" + case 0 + have [simp]: "{f. \x. f x = d} = {\x. d}" apply (rule set_eqI,rule) unfolding mem_Collect_eq apply (rule, rule ext) apply auto done - case 0 - thus ?case by(auto simp add: *) + from 0 show ?case by auto next case (Suc m) guess a using card_eq_SucD[OF Suc(4)] .. @@ -1246,9 +1296,8 @@ then guess k unfolding kle_def .. note k = this hence *: "n + 1 \ k" using xyp by auto have "\ (\x\k. x\{1..n})" - apply (rule ccontr) - unfolding not_not - apply(erule bexE) + apply (rule notI) + apply (erule bexE) proof - fix x assume as: "x \ k" "x \ {1..n}" @@ -1268,23 +1317,25 @@ hence "kle (n + 1) y x" using ksimplexD(6)[OF sa(1),rule_format, of x y] and as by auto then guess k unfolding kle_def .. note k = this - hence *: "n + 1 \ k" using xyp by auto - hence "\ (\x\k. x\{1..n})" + then have *: "n + 1 \ k" using xyp by auto + then have "\ (\x\k. x\{1..n})" apply - - apply (rule ccontr) - unfolding not_not + apply (rule notI) apply (erule bexE) proof - fix x assume as: "x \ k" "x \ {1..n}" have "x \ n + 1" using as and * by auto - thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto + then show False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed - thus ?thesis + then show ?thesis apply - apply (rule disjI2) unfolding kle_def - using k apply (rule_tac x = k in exI) by auto + using k + apply (rule_tac x = k in exI) + apply auto + done qed next fix x j @@ -1298,13 +1349,14 @@ qed (insert sa ksimplexD[OF sa(1)], auto) next assume ?rs note rs=ksimplexD[OF this] - guess a b apply (rule ksimplex_extrema[OF `?rs`]) . note ab = this + guess a b by (rule ksimplex_extrema[OF `?rs`]) note ab = this def c \ "\i. if i = (n + 1) then p - 1 else a i" have "c \ f" - apply (rule ccontr) unfolding not_not + apply (rule notI) apply (drule assms(2)[rule_format]) unfolding c_def - using assms(1) apply auto + using assms(1) + apply auto done thus ?ls apply (rule_tac x = "insert c f" in exI, rule_tac x = c in exI) @@ -1326,12 +1378,16 @@ show ?thesis unfolding True c_def apply (cases "j=n+1") - using ab(1) and rs(4) apply auto + using ab(1) and rs(4) + apply auto done qed (insert x rs(4), auto simp add:c_def) show "j \ {1..n + 1} \ x j = p" apply (cases "x = c") - using x ab(1) rs(5) unfolding c_def by auto + using x ab(1) rs(5) + unfolding c_def + apply auto + done { fix z assume z: "z \ insert c f" @@ -1359,9 +1415,9 @@ assume y: "y \ insert c f" show "kle (n + 1) x y \ kle (n + 1) y x" proof (cases "x = c \ y = c") - case False hence **:"x\f" "y\f" using x y by auto + case False hence **: "x \ f" "y \ f" using x y by auto show ?thesis using rs(6)[rule_format,OF **] - by(auto dest: kle_Suc) + by (auto dest: kle_Suc) qed (insert * x y, auto) qed (insert rs, auto) qed @@ -1377,7 +1433,9 @@ apply (rule ccontr) using *[OF assms(3), of a0 a1] unfolding assms(6)[THEN spec[where x=j]] - using assms(1-2,4-5) by auto + using assms(1-2,4-5) + apply auto + done qed lemma ksimplex_fix_plane_0: @@ -1399,11 +1457,11 @@ proof (rule ccontr) note s = ksimplexD[OF assms(1),rule_format] assume as: "a \ a0" - hence *: "a0 \ s - {a}" + then have *: "a0 \ s - {a}" using assms(5) by auto - hence "a1 = a" + then have "a1 = a" using ksimplex_fix_plane[OF assms(2-)] by auto - thus False + then show False using as and assms(3,5) and assms(7)[rule_format,of j] unfolding assms(4)[rule_format,OF *] using s(4)[OF assms(6), of j] @@ -1422,7 +1480,8 @@ guess a0 a1 by (rule ksimplex_extrema_strong[OF assms(1,3)]) note exta = this[rule_format] have a:"a = a1" apply (rule ksimplex_fix_plane_0[OF assms(2,4-5)]) - using exta(1-2,5) apply auto + using exta(1-2,5) + apply auto done moreover guess b0 b1 by (rule ksimplex_extrema_strong[OF goal1(1) assms(3)]) @@ -1430,7 +1489,9 @@ have a': "a' = b1" apply (rule ksimplex_fix_plane_0[OF goal1(2) assms(4), of b0]) unfolding goal1(3) - using assms extb goal1 apply auto done + using assms extb goal1 + apply auto + done moreover have "b0 = a0" unfolding kle_antisym[symmetric, of b0 a0 n] @@ -1446,7 +1507,8 @@ show "s' = s" apply - apply (rule *[of _ a1 b1]) - using exta(1-2) extb(1-2) goal1 apply auto + using exta(1-2) extb(1-2) goal1 + apply auto done qed show ?thesis @@ -1457,7 +1519,8 @@ defer apply (erule conjE bexE)+ apply (rule_tac a'=b in **) - using assms(1,2) apply auto + using assms(1,2) + apply auto done qed @@ -2774,46 +2837,148 @@ lemma kuhn_induction: assumes "0 < p" "\x. \j\{1..n+1}. (\j. x j \ p) \ (x j = 0) \ (lab x j = 0)" - "\x. \j\{1..n+1}. (\j. x j \ p) \ (x j = p) \ (lab x j = 1)" - "odd (card {f. ksimplex p n f \ ((reduced lab n) ` f = {0..n})})" - shows "odd (card {s. ksimplex p (n+1) s \((reduced lab (n+1)) ` s = {0..n+1})})" proof- - have *:"\s t. odd (card s) \ s = t \ odd (card t)" "\s f. (\x. f x \ n +1 ) \ f ` s \ {0..n+1}" by auto - show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling) - apply(rule *(1)[OF assms(4)]) apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*) - fix f assume as:"ksimplex p n f" "reduced lab n ` f = {0..n}" - have *:"\x\f. \j\{1..n + 1}. x j = 0 \ lab x j = 0" "\x\f. \j\{1..n + 1}. x j = p \ lab x j = 1" + "\x. \j\{1..n+1}. (\j. x j \ p) \ (x j = p) \ (lab x j = 1)" + "odd (card {f. ksimplex p n f \ ((reduced lab n) ` f = {0..n})})" + shows "odd (card {s. ksimplex p (n+1) s \((reduced lab (n+1)) ` s = {0..n+1})})" +proof - + have *: "\s t. odd (card s) \ s = t \ odd (card t)" + "\s f. (\x. f x \ n +1 ) \ f ` s \ {0..n+1}" by auto + show ?thesis + apply (rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) + apply (rule, rule, rule *, rule reduced_labelling) + apply (rule *(1)[OF assms(4)]) + apply (rule set_eqI) + unfolding mem_Collect_eq + apply (rule, erule conjE) + defer + apply rule + proof - + fix f + assume as: "ksimplex p n f" "reduced lab n ` f = {0..n}" + have *: "\x\f. \j\{1..n + 1}. x j = 0 \ lab x j = 0" + "\x\f. \j\{1..n + 1}. x j = p \ lab x j = 1" using assms(2-3) using as(1)[unfolded ksimplex_def] by auto - have allp:"\x\f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto - { fix x assume "x\f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_nonzero) - defer using assms(3) using as(1)[unfolded ksimplex_def] by auto - hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto } - hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[symmetric] apply- apply(rule set_eqI) unfolding image_iff by auto - moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] .. then guess a .. + have allp: "\x\f. x (n + 1) = p" + using assms(2) using as(1)[unfolded ksimplex_def] by auto + { + fix x + assume "x \ f" + hence "reduced lab (n + 1) x < n + 1" + apply - + apply (rule reduced_labelling_nonzero) + defer using assms(3) using as(1)[unfolded ksimplex_def] + apply auto + done + hence "reduced lab (n + 1) x = reduced lab n x" + apply - + apply (rule reduced_labelling_Suc) + using reduced_labelling(1) + apply auto + done + } + hence "reduced lab (n + 1) ` f = {0..n}" + unfolding as(2)[symmetric] + apply - + apply (rule set_eqI) + unfolding image_iff + apply auto + done + moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] .. + then guess a .. ultimately show "\s a. ksimplex p (n + 1) s \ a \ s \ f = s - {a} \ reduced lab (n + 1) ` f = {0..n} \ ((\j\{1..n + 1}. \x\f. x j = 0) \ (\j\{1..n + 1}. \x\f. x j = p))" (is ?ex) - apply(rule_tac x=s in exI,rule_tac x=a in exI) unfolding complete_face_top[OF *] using allp as(1) by auto - next fix f assume as:"\s a. ksimplex p (n + 1) s \ + apply (rule_tac x = s in exI) + apply (rule_tac x = a in exI) + unfolding complete_face_top[OF *] + using allp as(1) + apply auto + done + next + fix f + assume as: "\s a. ksimplex p (n + 1) s \ a \ s \ f = s - {a} \ reduced lab (n + 1) ` f = {0..n} \ ((\j\{1..n + 1}. \x\f. x j = 0) \ (\j\{1..n + 1}. \x\f. x j = p))" (is ?ex) - then guess s .. then guess a apply-apply(erule exE,(erule conjE)+) . note sa=this - { fix x assume "x\f" hence "reduced lab (n + 1) x \ reduced lab (n + 1) ` f" by auto - hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto - hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) - using reduced_labelling(1) by auto } - thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[symmetric] apply-apply(rule set_eqI) unfolding image_iff by auto - have *:"\x\f. x (n + 1) = p" proof(cases "\j\{1..n + 1}. \x\f. x j = 0") - case True then guess j .. hence "\x. x\f \ reduced lab (n + 1) x \ j - 1" apply-apply(rule reduced_labelling_zero) apply assumption - apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover + then guess s .. + then guess a + apply - + apply (erule exE,(erule conjE)+) + done + note sa = this + { + fix x + assume "x \ f" + hence "reduced lab (n + 1) x \ reduced lab (n + 1) ` f" + by auto + hence "reduced lab (n + 1) x < n + 1" + using sa(4) by auto + hence "reduced lab (n + 1) x = reduced lab n x" + apply - + apply (rule reduced_labelling_Suc) + using reduced_labelling(1) + apply auto + done + } + thus part1: "reduced lab n ` f = {0..n}" + unfolding sa(4)[symmetric] + apply - + apply (rule set_eqI) + unfolding image_iff + apply auto + done + have *: "\x\f. x (n + 1) = p" + proof (cases "\j\{1..n + 1}. \x\f. x j = 0") + case True + then guess j .. + hence "\x. x \ f \ reduced lab (n + 1) x \ j - 1" + apply - + apply (rule reduced_labelling_zero) + apply assumption + apply (rule assms(2)[rule_format]) + using sa(1)[unfolded ksimplex_def] + unfolding sa + apply auto + done + moreover have "j - 1 \ {0..n}" using `j\{1..n+1}` by auto - ultimately have False unfolding sa(4)[symmetric] unfolding image_iff by fastforce thus ?thesis by auto next - case False hence "\j\{1..n + 1}. \x\f. x j = p" using sa(5) by fastforce then guess j .. note j=this - thus ?thesis proof(cases "j = n+1") - case False hence *:"j\{1..n}" using j by auto - hence "\x. x\f \ reduced lab n x < j" apply(rule reduced_labelling_nonzero) proof- fix x assume "x\f" - hence "lab x j = 1" apply-apply(rule assms(3)[rule_format,OF j(1)]) - using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \ 0" by auto qed - moreover have "j\{0..n}" using * by auto - ultimately have False unfolding part1[symmetric] using * unfolding image_iff by auto thus ?thesis by auto qed auto qed - thus "ksimplex p n f" using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto qed qed + ultimately have False + unfolding sa(4)[symmetric] + unfolding image_iff + by fastforce + thus ?thesis by auto + next + case False + hence "\j\{1..n + 1}. \x\f. x j = p" + using sa(5) by fastforce then guess j .. note j=this + thus ?thesis + proof (cases "j = n + 1") + case False hence *: "j \ {1..n}" + using j by auto + hence "\x. x \ f \ reduced lab n x < j" + apply (rule reduced_labelling_nonzero) + proof - + fix x + assume "x \ f" + hence "lab x j = 1" + apply - + apply (rule assms(3)[rule_format,OF j(1)]) + using sa(1)[unfolded ksimplex_def] + using j + unfolding sa + apply auto + done + thus "lab x j \ 0" by auto + qed + moreover have "j \ {0..n}" using * by auto + ultimately have False + unfolding part1[symmetric] + using * unfolding image_iff + by auto + thus ?thesis by auto + qed auto + qed + thus "ksimplex p n f" + using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto + qed +qed lemma kuhn_induction_Suc: assumes "0 < p" "\x. \j\{1..Suc n}. (\j. x j \ p) \ (x j = 0) \ (lab x j = 0)" @@ -2822,51 +2987,135 @@ shows "odd (card {s. ksimplex p (Suc n) s \((reduced lab (Suc n)) ` s = {0..Suc n})})" using assms unfolding Suc_eq_plus1 by(rule kuhn_induction) + subsection {* And so we get the final combinatorial result. *} -lemma ksimplex_0: "ksimplex p 0 s \ s = {(\x. p)}" (is "?l = ?r") proof - assume l:?l guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a=this - have "a = (\x. p)" using ksimplexD(5)[OF l, rule_format, OF a(1)] by(rule,auto) thus ?r using a by auto next - assume r:?r show ?l unfolding r ksimplex_eq by auto qed +lemma ksimplex_0: "ksimplex p 0 s \ s = {(\x. p)}" (is "?l = ?r") +proof + assume l: ?l + guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a = this + have "a = (\x. p)" + using ksimplexD(5)[OF l, rule_format, OF a(1)] by rule auto + thus ?r using a by auto +next + assume r: ?r + show ?l unfolding r ksimplex_eq by auto +qed -lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0" apply(rule reduced_labelling_unique) by auto +lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0" + by (rule reduced_labelling_unique) auto lemma kuhn_combinatorial: assumes "0 < p" "\x j. (\j. x(j) \ p) \ 1 \ j \ j \ n \ (x j = 0) \ (lab x j = 0)" - "\x j. (\j. x(j) \ p) \ 1 \ j \ j \ n \ (x j = p) \ (lab x j = 1)" - shows " odd (card {s. ksimplex p n s \ ((reduced lab n) ` s = {0..n})})" using assms proof(induct n) + "\x j. (\j. x(j) \ p) \ 1 \ j \ j \ n \ (x j = p) \ (lab x j = 1)" + shows " odd (card {s. ksimplex p n s \ ((reduced lab n) ` s = {0..n})})" + using assms +proof (induct n) let ?M = "\n. {s. ksimplex p n s \ ((reduced lab n) ` s = {0..n})}" - { case 0 have *:"?M 0 = {{(\x. p)}}" unfolding ksimplex_0 by auto show ?case unfolding * by auto } - case (Suc n) have "odd (card (?M n))" apply(rule Suc(1)[OF Suc(2)]) using Suc(3-) by auto - thus ?case apply-apply(rule kuhn_induction_Suc) using Suc(2-) by auto qed + { + case 0 + have *: "?M 0 = {{(\x. p)}}" + unfolding ksimplex_0 by auto + show ?case unfolding * by auto + next + case (Suc n) + have "odd (card (?M n))" + apply (rule Suc(1)[OF Suc(2)]) + using Suc(3-) + apply auto + done + thus ?case + apply - + apply (rule kuhn_induction_Suc) + using Suc(2-) + apply auto + done + } +qed -lemma kuhn_lemma: assumes "0 < (p::nat)" "0 < (n::nat)" - "\x. (\i\{1..n}. x i \ p) \ (\i\{1..n}. (label x i = (0::nat)) \ (label x i = 1))" - "\x. (\i\{1..n}. x i \ p) \ (\i\{1..n}. (x i = 0) \ (label x i = 0))" - "\x. (\i\{1..n}. x i \ p) \ (\i\{1..n}. (x i = p) \ (label x i = 1))" +lemma kuhn_lemma: + assumes "0 < (p::nat)" "0 < (n::nat)" + "\x. (\i\{1..n}. x i \ p) \ (\i\{1..n}. (label x i = (0::nat)) \ (label x i = 1))" + "\x. (\i\{1..n}. x i \ p) \ (\i\{1..n}. (x i = 0) \ (label x i = 0))" + "\x. (\i\{1..n}. x i \ p) \ (\i\{1..n}. (x i = p) \ (label x i = 1))" obtains q where "\i\{1..n}. q i < p" - "\i\{1..n}. \r s. (\j\{1..n}. q(j) \ r(j) \ r(j) \ q(j) + 1) \ - (\j\{1..n}. q(j) \ s(j) \ s(j) \ q(j) + 1) \ - ~(label r i = label s i)" proof- - let ?A = "{s. ksimplex p n s \ reduced label n ` s = {0..n}}" have "n\0" using assms by auto - have conjD:"\P Q. P \ Q \ P" "\P Q. P \ Q \ Q" by auto - have "odd (card ?A)" apply(rule kuhn_combinatorial[of p n label]) using assms by auto - hence "card ?A \ 0" apply-apply(rule ccontr) by auto hence "?A \ {}" unfolding card_eq_0_iff by auto - then obtain s where "s\?A" by auto note s=conjD[OF this[unfolded mem_Collect_eq]] - guess a b apply(rule ksimplex_extrema_strong[OF s(1) `n\0`]) . note ab=this - show ?thesis apply(rule that[of a]) proof(rule_tac[!] ballI) fix i assume "i\{1..n}" - hence "a i + 1 \ p" apply-apply(rule order_trans[of _ "b i"]) apply(subst ab(5)[THEN spec[where x=i]]) - using s(1)[unfolded ksimplex_def] defer apply- apply(erule conjE)+ apply(drule_tac bspec[OF _ ab(2)])+ by auto + "\i\{1..n}. \r s. (\j\{1..n}. q(j) \ r(j) \ r(j) \ q(j) + 1) \ + (\j\{1..n}. q(j) \ s(j) \ s(j) \ q(j) + 1) \ + ~(label r i = label s i)" +proof - + let ?A = "{s. ksimplex p n s \ reduced label n ` s = {0..n}}" + have "n \ 0" using assms by auto + have conjD:"\P Q. P \ Q \ P" "\P Q. P \ Q \ Q" + by auto + have "odd (card ?A)" + apply (rule kuhn_combinatorial[of p n label]) + using assms + apply auto + done + hence "card ?A \ 0" + apply - + apply (rule ccontr) + apply auto + done + hence "?A \ {}" unfolding card_eq_0_iff by auto + then obtain s where "s \ ?A" + by auto note s=conjD[OF this[unfolded mem_Collect_eq]] + guess a b by (rule ksimplex_extrema_strong[OF s(1) `n\0`]) note ab = this + show ?thesis + apply (rule that[of a]) + apply (rule_tac[!] ballI) + proof - + fix i + assume "i\{1..n}" + hence "a i + 1 \ p" + apply - + apply (rule order_trans[of _ "b i"]) + apply (subst ab(5)[THEN spec[where x=i]]) + using s(1)[unfolded ksimplex_def] + defer + apply - + apply (erule conjE)+ + apply (drule_tac bspec[OF _ ab(2)])+ + apply auto + done thus "a i < p" by auto - case goal2 hence "i \ reduced label n ` s" using s by auto then guess u unfolding image_iff .. note u=this - from goal2 have "i - 1 \ reduced label n ` s" using s by auto then guess v unfolding image_iff .. note v=this - show ?case apply(rule_tac x=u in exI, rule_tac x=v in exI) apply(rule conjI) defer apply(rule conjI) defer 2 proof(rule_tac[1-2] ballI) - show "label u i \ label v i" using reduced_labelling[of label n u] reduced_labelling[of label n v] - unfolding u(2)[symmetric] v(2)[symmetric] using goal2 by auto - fix j assume j:"j\{1..n}" show "a j \ u j \ u j \ a j + 1" "a j \ v j \ v j \ a j + 1" - using conjD[OF ab(4)[rule_format, OF u(1)]] and conjD[OF ab(4)[rule_format, OF v(1)]] apply- - apply(drule_tac[!] kle_imp_pointwise)+ apply(erule_tac[!] x=j in allE)+ unfolding ab(5)[rule_format] using j - by auto qed qed qed + next + case goal2 + hence "i \ reduced label n ` s" using s by auto + then guess u unfolding image_iff .. note u = this + from goal2 have "i - 1 \ reduced label n ` s" + using s by auto + then guess v unfolding image_iff .. note v = this + show ?case + apply (rule_tac x = u in exI) + apply (rule_tac x = v in exI) + apply (rule conjI) + defer + apply (rule conjI) + defer 2 + apply (rule_tac[1-2] ballI) + proof - + show "label u i \ label v i" + using reduced_labelling [of label n u] reduced_labelling [of label n v] + unfolding u(2)[symmetric] v(2)[symmetric] + using goal2 + apply auto + done + fix j + assume j: "j \ {1..n}" + show "a j \ u j \ u j \ a j + 1" "a j \ v j \ v j \ a j + 1" + using conjD[OF ab(4)[rule_format, OF u(1)]] + and conjD[OF ab(4)[rule_format, OF v(1)]] + apply - + apply (drule_tac[!] kle_imp_pointwise)+ + apply (erule_tac[!] x=j in allE)+ + unfolding ab(5)[rule_format] + using j + apply auto + done + qed + qed +qed subsection {* The main result for the unit cube. *} @@ -2946,11 +3195,13 @@ using i label(1)[of i y] by auto show "x \ i \ f x \ i" apply (rule label(4)[rule_format]) - using xy lx i(2) apply auto + using xy lx i(2) + apply auto done show "f y \ i \ y \ i" apply (rule label(5)[rule_format]) - using xy ly i(2) apply auto + using xy ly i(2) + apply auto done next assume "label x i \ 0" @@ -2958,11 +3209,13 @@ using i label(1)[of i x] label(1)[of i y] by auto show "f x \ i \ x \ i" apply (rule label(5)[rule_format]) - using xy l i(2) apply auto + using xy l i(2) + apply auto done show "y \ i \ f y \ i" apply (rule label(4)[rule_format]) - using xy l i(2) apply auto + using xy l i(2) + apply auto done qed also have "\ \ norm (f y - f x) + norm (y - x)" @@ -2986,7 +3239,8 @@ note e=this[rule_format,unfolded dist_norm] show ?thesis apply (rule_tac x="min (e/2) (d/real n/8)" in exI) - proof safe + apply safe + proof - show "0 < min (e / 2) (d / real n / 8)" using d' e by auto fix x y z i @@ -3011,21 +3265,25 @@ unfolding norm_minus_commute by auto also have "\ < e / 2 + e / 2" apply (rule add_strict_mono) - using as(4,5) apply auto + using as(4,5) + apply auto done finally show "norm (f y - f x) < d / real n / 8" apply - apply (rule e(2)) - using as apply auto + using as + apply auto done have "norm (y - z) + norm (x - z) < d / real n / 8 + d / real n / 8" apply (rule add_strict_mono) - using as apply auto + using as + apply auto done thus "norm (y - x) < 2 * (d / real n / 8)" using tria by auto show "norm (f x - f z) < d / real n / 8" apply (rule e(2)) - using as e(1) apply auto + using as e(1) + apply auto done qed (insert as, auto) qed @@ -3036,9 +3294,10 @@ apply (rule add_pos_pos) defer apply (rule divide_pos_pos) - using e(1) n apply auto + using e(1) n + apply auto done - hence "p > 0" using p by auto + then have "p > 0" using p by auto obtain b :: "nat \ 'a" where b: "bij_betw b {1..n} Basis" by atomize_elim (auto simp: n_def intro!: finite_same_card_bij) @@ -3121,7 +3380,8 @@ have "\i. i \ Basis \ r (b' i) \ p" apply (rule order_trans) apply (rule rs(1)[OF b'_im,THEN conjunct2]) - using q(1)[rule_format,OF b'_im] apply (auto simp add: Suc_le_eq) + using q(1)[rule_format,OF b'_im] + apply (auto simp add: Suc_le_eq) done hence "r' \ {0..\Basis}" unfolding r'_def mem_interval using b'_Basis @@ -3130,7 +3390,8 @@ have "\i. i\Basis \ s (b' i) \ p" apply (rule order_trans) apply (rule rs(2)[OF b'_im, THEN conjunct2]) - using q(1)[rule_format,OF b'_im] apply (auto simp add: Suc_le_eq) + using q(1)[rule_format,OF b'_im] + apply (auto simp add: Suc_le_eq) done hence "s' \ {0..\Basis}" unfolding s'_def mem_interval using b'_Basis @@ -3141,7 +3402,8 @@ have *: "\x. 1 + real x = real (Suc x)" by auto { have "(\i\Basis. \real (r (b' i)) - real (q (b' i))\) \ (\(i::'a)\Basis. 1)" apply (rule setsum_mono) - using rs(1)[OF b'_im] apply (auto simp add:* field_simps) + using rs(1)[OF b'_im] + apply (auto simp add:* field_simps) done also have "\ < e * real p" using p `e>0` `p>0` by (auto simp add: field_simps n_def real_of_nat_def) @@ -3150,7 +3412,8 @@ moreover { have "(\i\Basis. \real (s (b' i)) - real (q (b' i))\) \ (\(i::'a)\Basis. 1)" apply (rule setsum_mono) - using rs(2)[OF b'_im] apply (auto simp add:* field_simps) + using rs(2)[OF b'_im] + apply (auto simp add:* field_simps) done also have "\ < e * real p" using p `e > 0` `p > 0` by (auto simp add: field_simps n_def real_of_nat_def) @@ -3216,7 +3479,7 @@ and t :: "('b::euclidean_space) set" assumes "s homeomorphic t" shows "(\f. continuous_on s f \ f ` s \ s \ (\x\s. f x = x)) \ - (\g. continuous_on t g \ g ` t \ t \ (\y\t. g y = y))" + (\g. continuous_on t g \ g ` t \ t \ (\y\t. g y = y))" proof - guess r using assms[unfolded homeomorphic_def homeomorphism_def] .. then guess i .. @@ -3244,8 +3507,9 @@ apply - apply (rule invertible_fixpoint_property[OF continuous_on_id _ _ _ _ assms(2), of t h g]) prefer 7 - apply (rule_tac y=y in that) - using assms apply auto + apply (rule_tac y = y in that) + using assms + apply auto done qed @@ -3253,7 +3517,7 @@ subsection {*So the Brouwer theorem for any set with nonempty interior. *} lemma brouwer_weak: - fixes f::"'a::ordered_euclidean_space \ 'a::ordered_euclidean_space" + fixes f :: "'a::ordered_euclidean_space \ 'a::ordered_euclidean_space" assumes "compact s" "convex s" "interior s \ {}" "continuous_on s f" "f ` s \ s" obtains x where "x \ s" "f x = x" proof - @@ -3271,7 +3535,8 @@ defer apply (erule bexE) apply (rule_tac x=y in that) - using assms apply auto + using assms + apply auto done qed @@ -3290,7 +3555,8 @@ rather involved @{text "HOMEOMORPHIC_CONVEX_COMPACT"} theorem, just using a scaling and translation to put the set inside the unit cube. *} -lemma brouwer: fixes f::"'a::ordered_euclidean_space \ 'a" +lemma brouwer: + fixes f::"'a::ordered_euclidean_space \ 'a" assumes "compact s" "convex s" "s \ {}" "continuous_on s f" "f ` s \ s" obtains x where "x \ s" "f x = x" proof - @@ -3353,7 +3619,8 @@ apply (simp add: * norm_minus_commute) done note x = this - hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by (auto simp add:algebra_simps) + hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" + by (auto simp add: algebra_simps) hence "a = x" unfolding scaleR_left_distrib[symmetric] by auto thus False using x assms by auto qed @@ -3361,14 +3628,15 @@ subsection {*Bijections between intervals. *} -definition interval_bij :: "'a \ 'a \ 'a \ 'a \ 'a \ 'a::ordered_euclidean_space" where - "interval_bij \ \(a, b) (u, v) x. (\i\Basis. (u\i + (x\i - a\i) / (b\i - a\i) * (v\i - u\i)) *\<^sub>R i)" +definition interval_bij :: "'a \ 'a \ 'a \ 'a \ 'a \ 'a::ordered_euclidean_space" + where "interval_bij = + (\(a, b) (u, v) x. (\i\Basis. (u\i + (x\i - a\i) / (b\i - a\i) * (v\i - u\i)) *\<^sub>R i))" lemma interval_bij_affine: "interval_bij (a,b) (u,v) = (\x. (\i\Basis. ((v\i - u\i) / (b\i - a\i) * (x\i)) *\<^sub>R i) + (\i\Basis. (u\i - (v\i - u\i) / (b\i - a\i) * (a\i)) *\<^sub>R i))" by (auto simp: setsum_addf[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff - field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong) + field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum_cong) lemma continuous_interval_bij: "continuous (at x) (interval_bij (a,b::'a::ordered_euclidean_space) (u,v::'a))" @@ -3384,7 +3652,8 @@ assumes "x \ {a..b}" "{u..v} \ {}" shows "interval_bij (a,b) (u,v) x \ {u..v}" apply (simp only: interval_bij_def split_conv mem_interval inner_setsum_left_Basis cong: ball_cong) -proof safe + apply safe +proof - fix i :: 'a assume i: "i \ Basis" have "{a..b} \ {}" using assms by auto @@ -3399,7 +3668,8 @@ have "((x \ i - a \ i) / (b \ i - a \ i)) * (v \ i - u \ i) \ 1 * (v \ i - u \ i)" apply (rule mult_right_mono) unfolding divide_le_eq_1 - using * x apply auto + using * x + apply auto done thus "u \ i + (x \ i - a \ i) / (b \ i - a \ i) * (v \ i - u \ i) \ v \ i" using * by auto diff -r 16235bb41881 -r 082d0972096b src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Wed Aug 28 23:48:45 2013 +0200 @@ -11,14 +11,18 @@ begin subsection{* First some facts about products*} -lemma setprod_insert_eq: "finite A \ setprod f (insert a A) = (if a \ A then setprod f A else f a * setprod f A)" -apply clarsimp -by(subgoal_tac "insert a A = A", auto) + +lemma setprod_insert_eq: + "finite A \ setprod f (insert a A) = (if a \ A then setprod f A else f a * setprod f A)" + apply clarsimp + apply (subgoal_tac "insert a A = A") + apply auto + done lemma setprod_add_split: assumes mn: "(m::nat) <= n + 1" shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}" -proof- +proof - let ?A = "{m .. n+p}" let ?B = "{m .. n}" let ?C = "{n+1..n+p}" @@ -30,47 +34,56 @@ lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\i. f (i + p)) {m..n}" -apply (rule setprod_reindex_cong[where f="op + p"]) -apply (auto simp add: image_iff Bex_def inj_on_def) -apply arith -apply (rule ext) -apply (simp add: add_commute) -done + apply (rule setprod_reindex_cong[where f="op + p"]) + apply (auto simp add: image_iff Bex_def inj_on_def) + apply presburger + apply (rule ext) + apply (simp add: add_commute) + done -lemma setprod_singleton: "setprod f {x} = f x" by simp - -lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" by simp +lemma setprod_singleton: "setprod f {x} = f x" + by simp -lemma setprod_numseg: "setprod f {m..0} = (if m=0 then f 0 else 1)" - "setprod f {m .. Suc n} = (if m \ Suc n then f (Suc n) * setprod f {m..n} - else setprod f {m..n})" +lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" + by simp + +lemma setprod_numseg: + "setprod f {m..0} = (if m = 0 then f 0 else 1)" + "setprod f {m .. Suc n} = + (if m \ Suc n then f (Suc n) * setprod f {m..n} else setprod f {m..n})" by (auto simp add: atLeastAtMostSuc_conv) -lemma setprod_le: assumes fS: "finite S" and fg: "\x\S. f x \ 0 \ f x \ (g x :: 'a::linordered_idom)" +lemma setprod_le: + assumes fS: "finite S" + and fg: "\x\S. f x \ 0 \ f x \ (g x :: 'a::linordered_idom)" shows "setprod f S \ setprod g S" -using fS fg -apply(induct S) -apply simp -apply auto -apply (rule mult_mono) -apply (auto intro: setprod_nonneg) -done + using fS fg + apply (induct S) + apply simp + apply auto + apply (rule mult_mono) + apply (auto intro: setprod_nonneg) + done (* FIXME: In Finite_Set there is a useless further assumption *) -lemma setprod_inversef: "finite A ==> setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)" +lemma setprod_inversef: + "finite A \ setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)" apply (erule finite_induct) apply (simp) apply simp done -lemma setprod_le_1: assumes fS: "finite S" and f: "\x\S. f x \ 0 \ f x \ (1::'a::linordered_idom)" +lemma setprod_le_1: + assumes fS: "finite S" + and f: "\x\S. f x \ 0 \ f x \ (1::'a::linordered_idom)" shows "setprod f S \ 1" -using setprod_le[OF fS f] unfolding setprod_1 . + using setprod_le[OF fS f] unfolding setprod_1 . -subsection{* Trace *} + +subsection {* Trace *} -definition trace :: "'a::semiring_1^'n^'n \ 'a" where - "trace A = setsum (\i. ((A$i)$i)) (UNIV::'n set)" +definition trace :: "'a::semiring_1^'n^'n \ 'a" + where "trace A = setsum (\i. ((A$i)$i)) (UNIV::'n set)" lemma trace_0: "trace(mat 0) = 0" by (simp add: trace_def mat_def) @@ -87,14 +100,17 @@ lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)" apply (simp add: trace_def matrix_matrix_mult_def) apply (subst setsum_commute) - by (simp add: mult_commute) + apply (simp add: mult_commute) + done (* ------------------------------------------------------------------------- *) (* Definition of determinant. *) (* ------------------------------------------------------------------------- *) definition det:: "'a::comm_ring_1^'n^'n \ 'a" where - "det A = setsum (\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}" + "det A = + setsum (\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)) + {p. p permutes (UNIV :: 'n set)}" (* ------------------------------------------------------------------------- *) (* A few general lemmas we need below. *) @@ -105,7 +121,8 @@ shows "setprod f S = setprod (f o p) S" using assms by (fact setprod.permute) -lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" +lemma setproduct_permute_nat_interval: + "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" by (blast intro!: setprod_permute) (* ------------------------------------------------------------------------- *) @@ -113,52 +130,71 @@ (* ------------------------------------------------------------------------- *) lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" -proof- +proof - let ?di = "\A i j. A$i$j" let ?U = "(UNIV :: 'n set)" have fU: "finite ?U" by simp - {fix p assume p: "p \ {p. p permutes ?U}" + { + fix p + assume p: "p \ {p. p permutes ?U}" from p have pU: "p permutes ?U" by blast have sth: "sign (inv p) = sign p" by (metis sign_inverse fU p mem_Collect_eq permutation_permutes) from permutes_inj[OF pU] have pi: "inj_on p ?U" by (blast intro: subset_inj_on) from permutes_image[OF pU] - have "setprod (\i. ?di (transpose A) i (inv p i)) ?U = setprod (\i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp + have "setprod (\i. ?di (transpose A) i (inv p i)) ?U = + setprod (\i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp also have "\ = setprod ((\i. ?di (transpose A) i (inv p i)) o p) ?U" unfolding setprod_reindex[OF pi] .. also have "\ = setprod (\i. ?di A i (p i)) ?U" - proof- - {fix i assume i: "i \ ?U" + proof - + { + fix i + assume i: "i \ ?U" from i permutes_inv_o[OF pU] permutes_in_image[OF pU] have "((\i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)" - unfolding transpose_def by (simp add: fun_eq_iff)} - then show "setprod ((\i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) + unfolding transpose_def by (simp add: fun_eq_iff) + } + then show "setprod ((\i. ?di (transpose A) i (inv p i)) o p) ?U = + setprod (\i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) qed - finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" using sth - by simp} - then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse) - apply (rule setsum_cong2) by blast + finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transpose A) i (inv p i)) ?U) = + of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" using sth by simp + } + then show ?thesis + unfolding det_def + apply (subst setsum_permutations_inverse) + apply (rule setsum_cong2) + apply blast + done qed lemma det_lowerdiagonal: fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})" assumes ld: "\i j. i < j \ A$i$j = 0" shows "det A = setprod (\i. A$i$i) (UNIV:: 'n set)" -proof- +proof - let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)" have fU: "finite ?U" by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . have id0: "{id} \ ?PU" by (auto simp add: permutes_id) - {fix p assume p: "p \ ?PU -{id}" - from p have pU: "p permutes ?U" and pid: "p \ id" by blast+ - from permutes_natset_le[OF pU] pid obtain i where - i: "p i > i" by (metis not_le) - from ld[OF i] have ex:"\i \ ?U. A$i$p i = 0" by blast - from setprod_zero[OF fU ex] have "?pp p = 0" by simp} - then have p0: "\p \ ?PU -{id}. ?pp p = 0" by blast + { + fix p + assume p: "p \ ?PU -{id}" + from p have pU: "p permutes ?U" and pid: "p \ id" + by blast+ + from permutes_natset_le[OF pU] pid obtain i where i: "p i > i" + by (metis not_le) + from ld[OF i] have ex:"\i \ ?U. A$i$p i = 0" + by blast + from setprod_zero[OF fU ex] have "?pp p = 0" + by simp + } + then have p0: "\p \ ?PU -{id}. ?pp p = 0" + by blast from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed @@ -167,21 +203,26 @@ fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}" assumes ld: "\i j. i > j \ A$i$j = 0" shows "det A = setprod (\i. A$i$i) (UNIV:: 'n set)" -proof- +proof - let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "(\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set))" have fU: "finite ?U" by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . have id0: "{id} \ ?PU" by (auto simp add: permutes_id) - {fix p assume p: "p \ ?PU -{id}" - from p have pU: "p permutes ?U" and pid: "p \ id" by blast+ - from permutes_natset_ge[OF pU] pid obtain i where - i: "p i < i" by (metis not_le) + { + fix p + assume p: "p \ ?PU -{id}" + from p have pU: "p permutes ?U" and pid: "p \ id" + by blast+ + from permutes_natset_ge[OF pU] pid obtain i where i: "p i < i" + by (metis not_le) from ld[OF i] have ex:"\i \ ?U. A$i$p i = 0" by blast - from setprod_zero[OF fU ex] have "?pp p = 0" by simp} - then have p0: "\p \ ?PU -{id}. ?pp p = 0" by blast - from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis + from setprod_zero[OF fU ex] have "?pp p = 0" by simp + } + then have p0: "\p \ ?PU -{id}. ?pp p = 0" + by blast + from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed @@ -189,14 +230,16 @@ fixes A :: "'a::comm_ring_1^'n^'n" assumes ld: "\i j. i \ j \ A$i$j = 0" shows "det A = setprod (\i. A$i$i) (UNIV::'n set)" -proof- +proof - let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)" have fU: "finite ?U" by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . have id0: "{id} \ ?PU" by (auto simp add: permutes_id) - {fix p assume p: "p \ ?PU - {id}" + { + fix p + assume p: "p \ ?PU - {id}" then have "p \ id" by simp then obtain i where i: "p i \ i" unfolding fun_eq_iff by auto from ld [OF i [symmetric]] have ex:"\i \ ?U. A$i$p i = 0" by blast @@ -207,16 +250,22 @@ qed lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" -proof- +proof - let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n" let ?U = "UNIV :: 'n set" let ?f = "\i j. ?A$i$j" - {fix i assume i: "i \ ?U" - have "?f i i = 1" using i by (vector mat_def)} - hence th: "setprod (\i. ?f i i) ?U = setprod (\x. 1) ?U" + { + fix i + assume i: "i \ ?U" + have "?f i i = 1" using i by (vector mat_def) + } + then have th: "setprod (\i. ?f i i) ?U = setprod (\x. 1) ?U" by (auto intro: setprod_cong) - {fix i j assume i: "i \ ?U" and j: "j \ ?U" and ij: "i \ j" - have "?f i j = 0" using i j ij by (vector mat_def) } + { + fix i j + assume i: "i \ ?U" and j: "j \ ?U" and ij: "i \ j" + have "?f i j = 0" using i j ij by (vector mat_def) + } then have "det ?A = setprod (\i. ?f i i) ?U" using det_diagonal by blast also have "\ = 1" unfolding th setprod_1 .. @@ -232,23 +281,27 @@ shows "det(\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric]) apply (subst sum_permutations_compose_right[OF p]) -proof(rule setsum_cong2) +proof (rule setsum_cong2) let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" - fix q assume qPU: "q \ ?PU" + fix q + assume qPU: "q \ ?PU" have fU: "finite ?U" by simp - from qPU have q: "q permutes ?U" by blast + from qPU have q: "q permutes ?U" + by blast from p q have pp: "permutation p" and qp: "permutation q" by (metis fU permutation_permutes)+ from permutes_inv[OF p] have ip: "inv p permutes ?U" . - have "setprod (\i. A$p i$ (q o p) i) ?U = setprod ((\i. A$p i$(q o p) i) o inv p) ?U" - by (simp only: setprod_permute[OF ip, symmetric]) - also have "\ = setprod (\i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U" - by (simp only: o_def) - also have "\ = setprod (\i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p]) - finally have thp: "setprod (\i. A$p i$ (q o p) i) ?U = setprod (\i. A$i$q i) ?U" - by blast - show "of_int (sign (q o p)) * setprod (\i. A$ p i$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\i. A$i$q i) ?U" + have "setprod (\i. A$p i$ (q o p) i) ?U = setprod ((\i. A$p i$(q o p) i) o inv p) ?U" + by (simp only: setprod_permute[OF ip, symmetric]) + also have "\ = setprod (\i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U" + by (simp only: o_def) + also have "\ = setprod (\i. A$i$q i) ?U" + by (simp only: o_def permutes_inverses[OF p]) + finally have thp: "setprod (\i. A$p i$ (q o p) i) ?U = setprod (\i. A$i$q i) ?U" + by blast + show "of_int (sign (q o p)) * setprod (\i. A$ p i$ (q o p) i) ?U = + of_int (sign p) * of_int (sign q) * setprod (\i. A$i$q i) ?U" by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult) qed @@ -256,7 +309,7 @@ fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n set)" shows "det(\ i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" -proof- +proof - let ?Ap = "\ i j. A$i$ p j :: 'a^'n^'n" let ?At = "transpose A" have "of_int (sign p) * det A = det (transpose (\ i. transpose A $ p i))" @@ -270,16 +323,16 @@ lemma det_identical_rows: fixes A :: "'a::linordered_idom^'n^'n" assumes ij: "i \ j" - and r: "row i A = row j A" + and r: "row i A = row j A" shows "det A = 0" proof- - have tha: "\(a::'a) b. a = b ==> b = - a ==> a = 0" + have tha: "\(a::'a) b. a = b \ b = - a \ a = 0" by simp have th1: "of_int (-1) = - 1" by simp let ?p = "Fun.swap i j id" let ?A = "\ i. A $ ?p i" from r have "A = ?A" by (simp add: vec_eq_iff row_def swap_def) - hence "det A = det ?A" by simp + then have "det A = det ?A" by simp moreover have "det A = - det ?A" by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1) ultimately show "det A = 0" by (metis tha) @@ -288,21 +341,22 @@ lemma det_identical_columns: fixes A :: "'a::linordered_idom^'n^'n" assumes ij: "i \ j" - and r: "column i A = column j A" + and r: "column i A = column j A" shows "det A = 0" -apply (subst det_transpose[symmetric]) -apply (rule det_identical_rows[OF ij]) -by (metis row_transpose r) + apply (subst det_transpose[symmetric]) + apply (rule det_identical_rows[OF ij]) + apply (metis row_transpose r) + done lemma det_zero_row: fixes A :: "'a::{idom, ring_char_0}^'n^'n" assumes r: "row i A = 0" shows "det A = 0" -using r -apply (simp add: row_def det_def vec_eq_iff) -apply (rule setsum_0') -apply (auto simp: sign_nz) -done + using r + apply (simp add: row_def det_def vec_eq_iff) + apply (rule setsum_0') + apply (auto simp: sign_nz) + done lemma det_zero_column: fixes A :: "'a::{idom,ring_char_0}^'n^'n" @@ -310,27 +364,32 @@ shows "det A = 0" apply (subst det_transpose[symmetric]) apply (rule det_zero_row [of i]) - by (metis row_transpose r) + apply (metis row_transpose r) + done lemma det_row_add: fixes a b c :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = - det((\ i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + - det((\ i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" -unfolding det_def vec_lambda_beta setsum_addf[symmetric] + det((\ i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + + det((\ i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" + unfolding det_def vec_lambda_beta setsum_addf[symmetric] proof (rule setsum_cong2) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" let ?f = "(\i. if i = k then a i + b i else c i)::'n \ 'a::comm_ring_1^'n" let ?g = "(\ i. if i = k then a i else c i)::'n \ 'a::comm_ring_1^'n" let ?h = "(\ i. if i = k then b i else c i)::'n \ 'a::comm_ring_1^'n" - fix p assume p: "p \ ?pU" + fix p + assume p: "p \ ?pU" let ?Uk = "?U - {k}" from p have pU: "p permutes ?U" by blast have kU: "?U = insert k ?Uk" by blast - {fix j assume j: "j \ ?Uk" + { + fix j + assume j: "j \ ?Uk" from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j" - by simp_all} + by simp_all + } then have th1: "setprod (\i. ?f i $ p i) ?Uk = setprod (\i. ?g i $ p i) ?Uk" and th2: "setprod (\i. ?f i $ p i) ?Uk = setprod (\i. ?h i $ p i) ?Uk" apply - @@ -342,36 +401,45 @@ also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" apply (rule setprod_insert) apply simp - by blast - also have "\ = (a k $ p k * setprod (\i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?f i $ p i) ?Uk)" by (simp add: field_simps) - also have "\ = (a k $ p k * setprod (\i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?h i $ p i) ?Uk)" by (metis th1 th2) + apply blast + done + also have "\ = (a k $ p k * setprod (\i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?f i $ p i) ?Uk)" + by (simp add: field_simps) + also have "\ = (a k $ p k * setprod (\i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\i. ?h i $ p i) ?Uk)" + by (metis th1 th2) also have "\ = setprod (\i. ?g i $ p i) (insert k ?Uk) + setprod (\i. ?h i $ p i) (insert k ?Uk)" unfolding setprod_insert[OF th3] by simp - finally have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?g i $ p i) ?U + setprod (\i. ?h i $ p i) ?U" unfolding kU[symmetric] . - then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = of_int (sign p) * setprod (\i. ?g i $ p i) ?U + of_int (sign p) * setprod (\i. ?h i $ p i) ?U" + finally have "setprod (\i. ?f i $ p i) ?U = + setprod (\i. ?g i $ p i) ?U + setprod (\i. ?h i $ p i) ?U" unfolding kU[symmetric] . + then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = + of_int (sign p) * setprod (\i. ?g i $ p i) ?U + of_int (sign p) * setprod (\i. ?h i $ p i) ?U" by (simp add: field_simps) qed lemma det_row_mul: fixes a b :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = - c* det((\ i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" - -unfolding det_def vec_lambda_beta setsum_right_distrib + c * det((\ i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" + unfolding det_def vec_lambda_beta setsum_right_distrib proof (rule setsum_cong2) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" let ?f = "(\i. if i = k then c*s a i else b i)::'n \ 'a::comm_ring_1^'n" let ?g = "(\ i. if i = k then a i else b i)::'n \ 'a::comm_ring_1^'n" - fix p assume p: "p \ ?pU" + fix p + assume p: "p \ ?pU" let ?Uk = "?U - {k}" from p have pU: "p permutes ?U" by blast have kU: "?U = insert k ?Uk" by blast - {fix j assume j: "j \ ?Uk" - from j have "?f j $ p j = ?g j $ p j" by simp} + { + fix j + assume j: "j \ ?Uk" + from j have "?f j $ p j = ?g j $ p j" by simp + } then have th1: "setprod (\i. ?f i $ p i) ?Uk = setprod (\i. ?g i $ p i) ?Uk" apply - - apply (rule setprod_cong, simp_all) + apply (rule setprod_cong) + apply simp_all done have th3: "finite ?Uk" "k \ ?Uk" by auto have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?f i $ p i) (insert k ?Uk)" @@ -379,29 +447,34 @@ also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" apply (rule setprod_insert) apply simp - by blast - also have "\ = (c*s a k) $ p k * setprod (\i. ?f i $ p i) ?Uk" by (simp add: field_simps) + apply blast + done + also have "\ = (c*s a k) $ p k * setprod (\i. ?f i $ p i) ?Uk" + by (simp add: field_simps) also have "\ = c* (a k $ p k * setprod (\i. ?g i $ p i) ?Uk)" unfolding th1 by (simp add: mult_ac) also have "\ = c* (setprod (\i. ?g i $ p i) (insert k ?Uk))" - unfolding setprod_insert[OF th3] by simp - finally have "setprod (\i. ?f i $ p i) ?U = c* (setprod (\i. ?g i $ p i) ?U)" unfolding kU[symmetric] . - then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = c * (of_int (sign p) * setprod (\i. ?g i $ p i) ?U)" + unfolding setprod_insert[OF th3] by simp + finally have "setprod (\i. ?f i $ p i) ?U = c* (setprod (\i. ?g i $ p i) ?U)" + unfolding kU[symmetric] . + then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = + c * (of_int (sign p) * setprod (\i. ?g i $ p i) ?U)" by (simp add: field_simps) qed lemma det_row_0: fixes b :: "'n::finite \ _ ^ 'n" shows "det((\ i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" -using det_row_mul[of k 0 "\i. 1" b] -apply (simp) - unfolding vector_smult_lzero . + using det_row_mul[of k 0 "\i. 1" b] + apply simp + apply (simp only: vector_smult_lzero) + done lemma det_row_operation: fixes A :: "'a::linordered_idom^'n^'n" assumes ij: "i \ j" shows "det (\ k. if k = i then row i A + c *s row j A else row k A) = det A" -proof- +proof - let ?Z = "(\ k. if k = i then row j A else row k A) :: 'a ^'n^'n" have th: "row i ?Z = row j ?Z" by (vector row_def) have th2: "((\ k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" @@ -415,30 +488,38 @@ fixes A :: "real^'n^'n" assumes x: "x \ span {row j A |j. j \ i}" shows "det (\ k. if k = i then row i A + x else row k A) = det A" -proof- +proof - let ?U = "UNIV :: 'n set" let ?S = "{row j A |j. j \ i}" let ?d = "\x. det (\ k. if k = i then x else row k A)" let ?P = "\x. ?d (row i A + x) = det A" - {fix k - - have "(if k = i then row i A + 0 else row k A) = row k A" by simp} + { + fix k + have "(if k = i then row i A + 0 else row k A) = row k A" by simp + } then have P0: "?P 0" apply - apply (rule cong[of det, OF refl]) - by (vector row_def) + apply (vector row_def) + done moreover - {fix c z y assume zS: "z \ ?S" and Py: "?P y" + { + fix c z y + assume zS: "z \ ?S" and Py: "?P y" from zS obtain j where j: "z = row j A" "i \ j" by blast let ?w = "row i A + y" have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector have thz: "?d z = 0" apply (rule det_identical_rows[OF j(2)]) - using j by (vector row_def) - have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 .. - then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i] - by simp } - + using j + apply (vector row_def) + done + have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" + unfolding th0 .. + then have "?P (c*s z + y)" + unfolding thz Py det_row_mul[of i] det_row_add[of i] + by simp + } ultimately show ?thesis apply - apply (rule span_induct_alt[of ?P ?S, OF P0, folded scalar_mult_eq_scaleR]) @@ -456,53 +537,68 @@ fixes A:: "real^'n^'n" assumes d: "dependent (rows A)" shows "det A = 0" -proof- +proof - let ?U = "UNIV :: 'n set" from d obtain i where i: "row i A \ span (rows A - {row i A})" unfolding dependent_def rows_def by blast - {fix j k assume jk: "j \ k" - and c: "row j A = row k A" - from det_identical_rows[OF jk c] have ?thesis .} + { + fix j k + assume jk: "j \ k" and c: "row j A = row k A" + from det_identical_rows[OF jk c] have ?thesis . + } moreover - {assume H: "\ i j. i \ j \ row i A \ row j A" + { + assume H: "\ i j. i \ j \ row i A \ row j A" have th0: "- row i A \ span {row j A|j. j \ i}" apply (rule span_neg) apply (rule set_rev_mp) apply (rule i) apply (rule span_mono) - using H i by (auto simp add: rows_def) + using H i + apply (auto simp add: rows_def) + done from det_row_span[OF th0] have "det A = det (\ k. if k = i then 0 *s 1 else row k A)" unfolding right_minus vector_smult_lzero .. with det_row_mul[of i "0::real" "\i. 1"] - have "det A = 0" by simp} + have "det A = 0" by simp + } ultimately show ?thesis by blast qed -lemma det_dependent_columns: assumes d: "dependent(columns (A::real^'n^'n))" shows "det A = 0" -by (metis d det_dependent_rows rows_transpose det_transpose) +lemma det_dependent_columns: + assumes d: "dependent (columns (A::real^'n^'n))" + shows "det A = 0" + by (metis d det_dependent_rows rows_transpose det_transpose) (* ------------------------------------------------------------------------- *) (* Multilinearity and the multiplication formula. *) (* ------------------------------------------------------------------------- *) lemma Cart_lambda_cong: "(\x. f x = g x) \ (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" - apply (rule iffD1[OF vec_lambda_unique]) by vector + by (rule iffD1[OF vec_lambda_unique]) vector lemma det_linear_row_setsum: assumes fS: "finite S" - shows "det ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" -proof(induct rule: finite_induct[OF fS]) - case 1 thus ?case apply simp unfolding setsum_empty det_row_0[of k] .. + shows "det ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = + setsum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" +proof (induct rule: finite_induct[OF fS]) + case 1 + then show ?case + apply simp + unfolding setsum_empty det_row_0[of k] + apply rule + done next case (2 x F) - then show ?case by (simp add: det_row_add cong del: if_weak_cong) + then show ?case + by (simp add: det_row_add cong del: if_weak_cong) qed lemma finite_bounded_functions: assumes fS: "finite S" shows "finite {f. (\i \ {1.. (k::nat)}. f i \ S) \ (\i. i \ {1 .. k} \ f i = i)}" -proof(induct k) +proof (induct k) case 0 have th: "{f. \i. f i = i} = {id}" by auto show ?case by (auto simp add: th) @@ -526,13 +622,14 @@ lemma det_linear_rows_setsum_lemma: assumes fS: "finite S" and fT: "finite T" shows "det((\ i. if i \ T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = - setsum (\f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)) - {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" -using fT -proof(induct T arbitrary: a c set: finite) + setsum (\f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)) + {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" + using fT +proof (induct T arbitrary: a c set: finite) case empty - have th0: "\x y. (\ i. if i \ {} then x i else y i) = (\ i. y i)" by vector - from "empty.prems" show ?case unfolding th0 by simp + have th0: "\x y. (\ i. if i \ {} then x i else y i) = (\ i. y i)" + by vector + from empty.prems show ?case unfolding th0 by simp next case (insert z T a c) let ?F = "\T. {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" @@ -540,42 +637,48 @@ let ?k = "\h. (h(z),(\i. if i = z then i else h i))" let ?s = "\ k a c f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)" let ?c = "\i. if i = z then a i j else c i" - have thif: "\a b c d. (if a \ b then c else d) = (if a then c else if b then c else d)" by simp + have thif: "\a b c d. (if a \ b then c else d) = (if a then c else if b then c else d)" + by simp have thif2: "\a b c d e. (if a then b else if c then d else e) = - (if c then (if a then b else d) else (if a then b else e))" by simp - from `z \ T` have nz: "\i. i \ T \ i = z \ False" by auto + (if c then (if a then b else d) else (if a then b else e))" + by simp + from `z \ T` have nz: "\i. i \ T \ i = z \ False" + by auto have "det (\ i. if i \ insert z T then setsum (a i) S else c i) = - det (\ i. if i = z then setsum (a i) S - else if i \ T then setsum (a i) S else c i)" + det (\ i. if i = z then setsum (a i) S else if i \ T then setsum (a i) S else c i)" unfolding insert_iff thif .. - also have "\ = (\j\S. det (\ i. if i \ T then setsum (a i) S - else if i = z then a i j else c i))" + also have "\ = (\j\S. det (\ i. if i \ T then setsum (a i) S else if i = z then a i j else c i))" unfolding det_linear_row_setsum[OF fS] apply (subst thif2) - using nz by (simp cong del: if_weak_cong cong add: if_cong) + using nz + apply (simp cong del: if_weak_cong cong add: if_cong) + done finally have tha: "det (\ i. if i \ insert z T then setsum (a i) S else c i) = (\(j, f)\S \ ?F T. det (\ i. if i \ T then a i (f i) else if i = z then a i j else c i))" - unfolding insert.hyps unfolding setsum_cartesian_product by blast + unfolding insert.hyps unfolding setsum_cartesian_product by blast show ?case unfolding tha - apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"], + apply (rule setsum_eq_general_reverses[where h= "?h" and k= "?k"], blast intro: finite_cartesian_product fS finite, blast intro: finite_cartesian_product fS finite) using `z \ T` apply auto apply (rule cong[OF refl[of det]]) - by vector + apply vector + done qed lemma det_linear_rows_setsum: assumes fS: "finite (S::'n::finite set)" - shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \i. f i \ S}" -proof- - have th0: "\x y. ((\ i. if i \ (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\ i. x i)" by vector - - from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] show ?thesis by simp + shows "det (\ i. setsum (a i) S) = + setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \i. f i \ S}" +proof - + have th0: "\x y. ((\ i. if i \ (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\ i. x i)" + by vector + from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] + show ?thesis by simp qed lemma matrix_mul_setsum_alt: @@ -585,75 +688,93 @@ lemma det_rows_mul: "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) = - setprod (\i. c i) (UNIV:: 'n set) * det((\ i. a i)::'a^'n^'n)" + setprod (\i. c i) (UNIV:: 'n set) * det((\ i. a i)::'a^'n^'n)" proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2) let ?U = "UNIV :: 'n set" let ?PU = "{p. p permutes ?U}" - fix p assume pU: "p \ ?PU" + fix p + assume pU: "p \ ?PU" let ?s = "of_int (sign p)" - from pU have p: "p permutes ?U" by blast + from pU have p: "p permutes ?U" + by blast have "setprod (\i. c i * a i $ p i) ?U = setprod c ?U * setprod (\i. a i $ p i) ?U" unfolding setprod_timesf .. then show "?s * (\xa\?U. c xa * a xa $ p xa) = - setprod c ?U * (?s* (\xa\?U. a xa $ p xa))" by (simp add: field_simps) + setprod c ?U * (?s* (\xa\?U. a xa $ p xa))" by (simp add: field_simps) qed lemma det_mul: fixes A B :: "'a::linordered_idom^'n^'n" shows "det (A ** B) = det A * det B" -proof- +proof - let ?U = "UNIV :: 'n set" let ?F = "{f. (\i\ ?U. f i \ ?U) \ (\i. i \ ?U \ f i = i)}" let ?PU = "{p. p permutes ?U}" have fU: "finite ?U" by simp have fF: "finite ?F" by (rule finite) - {fix p assume p: "p permutes ?U" - + { + fix p + assume p: "p permutes ?U" have "p \ ?F" unfolding mem_Collect_eq permutes_in_image[OF p] - using p[unfolded permutes_def] by simp} + using p[unfolded permutes_def] by simp + } then have PUF: "?PU \ ?F" by blast - {fix f assume fPU: "f \ ?F - ?PU" + { + fix f + assume fPU: "f \ ?F - ?PU" have fUU: "f ` ?U \ ?U" using fPU by auto - from fPU have f: "\i \ ?U. f i \ ?U" - "\i. i \ ?U \ f i = i" "\(\y. \!x. f x = y)" unfolding permutes_def - by auto + from fPU have f: "\i \ ?U. f i \ ?U" "\i. i \ ?U \ f i = i" "\(\y. \!x. f x = y)" + unfolding permutes_def by auto let ?A = "(\ i. A$i$f i *s B$f i) :: 'a^'n^'n" let ?B = "(\ i. B$f i) :: 'a^'n^'n" - {assume fni: "\ inj_on f ?U" + { + assume fni: "\ inj_on f ?U" then obtain i j where ij: "f i = f j" "i \ j" unfolding inj_on_def by blast from ij have rth: "row i ?B = row j ?B" by (vector row_def) from det_identical_rows[OF ij(2) rth] have "det (\ i. A$i$f i *s B$f i) = 0" - unfolding det_rows_mul by simp} + unfolding det_rows_mul by simp + } moreover - {assume fi: "inj_on f ?U" + { + assume fi: "inj_on f ?U" from f fi have fith: "\i j. f i = f j \ i = j" unfolding inj_on_def by metis note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]] - {fix y + { + fix y from fs f have "\x. f x = y" by blast then obtain x where x: "f x = y" by blast - {fix z assume z: "f z = y" from fith x z have "z = x" by metis} - with x have "\!x. f x = y" by blast} - with f(3) have "det (\ i. A$i$f i *s B$f i) = 0" by blast} - ultimately have "det (\ i. A$i$f i *s B$f i) = 0" by blast} - hence zth: "\ f\ ?F - ?PU. det (\ i. A$i$f i *s B$f i) = 0" by simp - {fix p assume pU: "p \ ?PU" + { + fix z + assume z: "f z = y" + from fith x z have "z = x" by metis + } + with x have "\!x. f x = y" by blast + } + with f(3) have "det (\ i. A$i$f i *s B$f i) = 0" by blast + } + ultimately have "det (\ i. A$i$f i *s B$f i) = 0" by blast + } + hence zth: "\ f\ ?F - ?PU. det (\ i. A$i$f i *s B$f i) = 0" + by simp + { + fix p + assume pU: "p \ ?PU" from pU have p: "p permutes ?U" by blast let ?s = "\p. of_int (sign p)" - let ?f = "\q. ?s p * (\i\ ?U. A $ i $ p i) * - (?s q * (\i\ ?U. B $ i $ q i))" + let ?f = "\q. ?s p * (\i\ ?U. A $ i $ p i) * (?s q * (\i\ ?U. B $ i $ q i))" have "(setsum (\q. ?s q * - (\i\ ?U. (\ i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = - (setsum (\q. ?s p * (\i\ ?U. A $ i $ p i) * - (?s q * (\i\ ?U. B $ i $ q i))) ?PU)" + (\i\ ?U. (\ i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = + (setsum (\q. ?s p * (\i\ ?U. A $ i $ p i) * (?s q * (\i\ ?U. B $ i $ q i))) ?PU)" unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] proof(rule setsum_cong2) - fix q assume qU: "q \ ?PU" + fix q + assume qU: "q \ ?PU" hence q: "q permutes ?U" by blast from p q have pp: "permutation p" and pq: "permutation q" unfolding permutation_permutes by auto @@ -666,11 +787,15 @@ by (simp add: th00 mult_ac sign_idempotent sign_compose) have th001: "setprod (\i. B$i$ q (inv p i)) ?U = setprod ((\i. B$i$ q (inv p i)) o p) ?U" by (rule setprod_permute[OF p]) - have thp: "setprod (\i. (\ i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U = setprod (\i. A$i$p i) ?U * setprod (\i. B$i$ q (inv p i)) ?U" + have thp: "setprod (\i. (\ i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U = + setprod (\i. A$i$p i) ?U * setprod (\i. B$i$ q (inv p i)) ?U" unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p] apply (rule setprod_cong[OF refl]) - using permutes_in_image[OF q] by vector - show "?s q * setprod (\i. (((\ i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = ?s p * (setprod (\i. A$i$p i) ?U) * (?s (q o inv p) * setprod (\i. B$i$(q o inv p) i) ?U)" + using permutes_in_image[OF q] + apply vector + done + show "?s q * setprod (\i. (((\ i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = + ?s p * (setprod (\i. A$i$p i) ?U) * (?s (q o inv p) * setprod (\i. B$i$(q o inv p) i) ?U)" using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose) qed @@ -703,22 +828,24 @@ lemma invertible_det_nz: fixes A::"real ^'n^'n" shows "invertible A \ det A \ 0" -proof- - {assume "invertible A" +proof - + { + assume "invertible A" then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1" unfolding invertible_righ_inverse by blast hence "det (A ** B) = det (mat 1 :: real ^'n^'n)" by simp - hence "det A \ 0" - apply (simp add: det_mul det_I) by algebra } + hence "det A \ 0" by (simp add: det_mul det_I) algebra + } moreover - {assume H: "\ invertible A" + { + assume H: "\ invertible A" let ?U = "UNIV :: 'n set" have fU: "finite ?U" by simp from H obtain c i where c: "setsum (\i. c i *s row i A) ?U = 0" and iU: "i \ ?U" and ci: "c i \ 0" unfolding invertible_righ_inverse unfolding matrix_right_invertible_independent_rows by blast - have stupid: "\(a::real^'n) b. a + b = 0 \ -a = b" + have *: "\(a::real^'n) b. a + b = 0 \ -a = b" apply (drule_tac f="op + (- a)" in cong[OF refl]) apply (simp only: ab_left_minus add_assoc[symmetric]) apply simp @@ -729,7 +856,7 @@ apply - apply (rule vector_mul_lcancel_imp[OF ci]) apply (auto simp add: field_simps) - unfolding stupid .. + unfolding * .. have thr: "- row i A \ span {row j A| j. j \ i}" unfolding thr0 apply (rule span_setsum) @@ -743,7 +870,8 @@ have thrb: "row i ?B = 0" using iU by (vector row_def) have "det A = 0" unfolding det_row_span[OF thr, symmetric] right_minus - unfolding det_zero_row[OF thrb] ..} + unfolding det_zero_row[OF thrb] .. + } ultimately show ?thesis by blast qed @@ -756,7 +884,7 @@ shows "det ((\ i. if i = k then setsum (\i. x$i *s row i A) (UNIV::'n set) else row i A)::real^'n^'n) = x$k * det A" (is "?lhs = ?rhs") -proof- +proof - let ?U = "UNIV :: 'n set" let ?Uk = "?U - {k}" have U: "?U = insert k ?Uk" by blast @@ -766,7 +894,8 @@ by (vector field_simps) have th001: "\f k . (\x. if x = k then f k else f x) = f" by auto have "(\ i. row i A) = A" by (vector row_def) - then have thd1: "det (\ i. row i A) = det A" by simp + then have thd1: "det (\ i. row i A) = det A" + by simp have thd0: "det (\ i. if i = k then row k A + (\i \ ?Uk. x $ i *s row i A) else row i A) = det A" apply (rule det_row_span) apply (rule span_setsum[OF fUk]) @@ -784,37 +913,44 @@ unfolding thd0 unfolding det_row_mul unfolding th001[of k "\i. row i A"] - unfolding thd1 by (simp add: field_simps) + unfolding thd1 + apply (simp add: field_simps) + done qed lemma cramer_lemma: fixes A :: "real^'n^'n" shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: real^'n^'n) = x$k * det A" -proof- +proof - let ?U = "UNIV :: 'n set" - have stupid: "\c. setsum (\i. c i *s row i (transpose A)) ?U = setsum (\i. c i *s column i A) ?U" + have *: "\c. setsum (\i. c i *s row i (transpose A)) ?U = setsum (\i. c i *s column i A) ?U" by (auto simp add: row_transpose intro: setsum_cong2) show ?thesis unfolding matrix_mult_vsum - unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] - unfolding stupid[of "\i. x$i"] - apply (subst det_transpose[symmetric]) - apply (rule cong[OF refl[of det]]) by (vector transpose_def column_def row_def) + unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] + unfolding *[of "\i. x$i"] + apply (subst det_transpose[symmetric]) + apply (rule cong[OF refl[of det]]) + apply (vector transpose_def column_def row_def) + done qed lemma cramer: fixes A ::"real^'n^'n" assumes d0: "det A \ 0" shows "A *v x = b \ x = (\ k. det(\ i j. if j=k then b$i else A$i$j) / det A)" -proof- +proof - from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" unfolding invertible_det_nz[symmetric] invertible_def by blast have "(A ** B) *v b = b" by (simp add: B matrix_vector_mul_lid) - hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc) + then have "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc) then have xe: "\x. A*v x = b" by blast - {fix x assume x: "A *v x = b" - have "x = (\ k. det(\ i j. if j=k then b$i else A$i$j) / det A)" - unfolding x[symmetric] - using d0 by (simp add: vec_eq_iff cramer_lemma field_simps)} + { + fix x + assume x: "A *v x = b" + have "x = (\ k. det(\ i j. if j=k then b$i else A$i$j) / det A)" + unfolding x[symmetric] + using d0 by (simp add: vec_eq_iff cramer_lemma field_simps) + } with xe show ?thesis by auto qed @@ -824,16 +960,19 @@ definition "orthogonal_transformation f \ linear f \ (\v w. f v \ f w = v \ w)" -lemma orthogonal_transformation: "orthogonal_transformation f \ linear f \ (\(v::real ^_). norm (f v) = norm v)" +lemma orthogonal_transformation: + "orthogonal_transformation f \ linear f \ (\(v::real ^_). norm (f v) = norm v)" unfolding orthogonal_transformation_def apply auto apply (erule_tac x=v in allE)+ apply (simp add: norm_eq_sqrt_inner) - by (simp add: dot_norm linear_add[symmetric]) + apply (simp add: dot_norm linear_add[symmetric]) + done -definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ transpose Q ** Q = mat 1 \ Q ** transpose Q = mat 1" +definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ + transpose Q ** Q = mat 1 \ Q ** transpose Q = mat 1" -lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transpose Q ** Q = mat 1" +lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transpose Q ** Q = mat 1" by (metis matrix_left_right_inverse orthogonal_matrix_def) lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)" @@ -842,28 +981,31 @@ lemma orthogonal_matrix_mul: fixes A :: "real ^'n^'n" assumes oA : "orthogonal_matrix A" - and oB: "orthogonal_matrix B" + and oB: "orthogonal_matrix B" shows "orthogonal_matrix(A ** B)" using oA oB unfolding orthogonal_matrix matrix_transpose_mul apply (subst matrix_mul_assoc) apply (subst matrix_mul_assoc[symmetric]) - by (simp add: matrix_mul_rid) + apply (simp add: matrix_mul_rid) + done lemma orthogonal_transformation_matrix: fixes f:: "real^'n \ real^'n" shows "orthogonal_transformation f \ linear f \ orthogonal_matrix(matrix f)" (is "?lhs \ ?rhs") -proof- +proof - let ?mf = "matrix f" let ?ot = "orthogonal_transformation f" let ?U = "UNIV :: 'n set" have fU: "finite ?U" by simp let ?m1 = "mat 1 :: real ^'n^'n" - {assume ot: ?ot + { + assume ot: ?ot from ot have lf: "linear f" and fd: "\v w. f v \ f w = v \ w" unfolding orthogonal_transformation_def orthogonal_matrix by blast+ - {fix i j + { + fix i j let ?A = "transpose ?mf ** ?mf" have th0: "\b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" "\b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" @@ -871,16 +1013,22 @@ from fd[rule_format, of "axis i 1" "axis j 1", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] have "?A$i$j = ?m1 $ i $ j" by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def - th0 setsum_delta[OF fU] mat_def axis_def) } - hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector - with lf have ?rhs by blast} + th0 setsum_delta[OF fU] mat_def axis_def) + } + then have "orthogonal_matrix ?mf" unfolding orthogonal_matrix + by vector + with lf have ?rhs by blast + } moreover - {assume lf: "linear f" and om: "orthogonal_matrix ?mf" + { + assume lf: "linear f" and om: "orthogonal_matrix ?mf" from lf om have ?lhs unfolding orthogonal_matrix_def norm_eq orthogonal_transformation unfolding matrix_works[OF lf, symmetric] apply (subst dot_matrix_vector_mul) - by (simp add: dot_matrix_product matrix_mul_lid)} + apply (simp add: dot_matrix_product matrix_mul_lid) + done + } ultimately show ?thesis by blast qed @@ -888,21 +1036,26 @@ fixes Q:: "'a::linordered_idom^'n^'n" assumes oQ: "orthogonal_matrix Q" shows "det Q = 1 \ det Q = - 1" -proof- - +proof - have th: "\x::'a. x = 1 \ x = - 1 \ x*x = 1" (is "\x::'a. ?ths x") - proof- + proof - fix x:: 'a - have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: field_simps) + have th0: "x*x - 1 = (x - 1)*(x + 1)" + by (simp add: field_simps) have th1: "\(x::'a) y. x = - y \ x + y = 0" - apply (subst eq_iff_diff_eq_0) by simp - have "x*x = 1 \ x*x - 1 = 0" by simp + apply (subst eq_iff_diff_eq_0) + apply simp + done + have "x * x = 1 \ x*x - 1 = 0" by simp also have "\ \ x = 1 \ x = - 1" unfolding th0 th1 by simp finally show "?ths x" .. qed - from oQ have "Q ** transpose Q = mat 1" by (metis orthogonal_matrix_def) - hence "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" by simp - hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transpose) + from oQ have "Q ** transpose Q = mat 1" + by (metis orthogonal_matrix_def) + then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" + by simp + then have "det Q * det Q = 1" + by (simp add: det_mul det_I det_transpose) then show ?thesis unfolding th . qed @@ -911,25 +1064,29 @@ (* ------------------------------------------------------------------------- *) lemma scaling_linear: fixes f :: "real ^'n \ real ^'n" - assumes f0: "f 0 = 0" and fd: "\x y. dist (f x) (f y) = c * dist x y" + assumes f0: "f 0 = 0" + and fd: "\x y. dist (f x) (f y) = c * dist x y" shows "linear f" -proof- - {fix v w - {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] } +proof - + { + fix v w + { + fix x + note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] + } note th0 = this have "f v \ f w = c\<^sup>2 * (v \ w)" unfolding dot_norm_neg dist_norm[symmetric] unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} note fc = this show ?thesis - unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR + unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR by (simp add: inner_add fc field_simps) qed lemma isometry_linear: - "f (0:: real^'n) = (0:: real^'n) \ \x y. dist(f x) (f y) = dist x y - \ linear f" -by (rule scaling_linear[where c=1]) simp_all + "f (0:: real^'n) = (0:: real^'n) \ \x y. dist(f x) (f y) = dist x y \ linear f" + by (rule scaling_linear[where c=1]) simp_all (* ------------------------------------------------------------------------- *) (* Hence another formulation of orthogonal transformation. *) @@ -948,7 +1105,8 @@ apply clarify apply (erule_tac x=v in allE) apply (erule_tac x=0 in allE) - by (simp add: dist_norm) + apply (simp add: dist_norm) + done (* ------------------------------------------------------------------------- *) (* Can extend an isometry from unit sphere. *) @@ -957,15 +1115,19 @@ lemma isometry_sphere_extend: fixes f:: "real ^'n \ real ^'n" assumes f1: "\x. norm x = 1 \ norm (f x) = 1" - and fd1: "\ x y. norm x = 1 \ norm y = 1 \ dist (f x) (f y) = dist x y" + and fd1: "\ x y. norm x = 1 \ norm y = 1 \ dist (f x) (f y) = dist x y" shows "\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" -proof- - {fix x y x' y' x0 y0 x0' y0' :: "real ^'n" - assume H: "x = norm x *\<^sub>R x0" "y = norm y *\<^sub>R y0" - "x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'" - "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" - "norm(x0' - y0') = norm(x0 - y0)" - hence *:"x0 \ y0 = x0' \ y0' + y0' \ x0' - y0 \ x0 " by(simp add: norm_eq norm_eq_1 inner_add inner_diff) +proof - + { + fix x y x' y' x0 y0 x0' y0' :: "real ^'n" + assume H: + "x = norm x *\<^sub>R x0" + "y = norm y *\<^sub>R y0" + "x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'" + "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" + "norm(x0' - y0') = norm(x0 - y0)" + hence *: "x0 \ y0 = x0' \ y0' + y0' \ x0' - y0 \ x0 " + by (simp add: norm_eq norm_eq_1 inner_add inner_diff) have "norm(x' - y') = norm(x - y)" apply (subst H(1)) apply (subst H(2)) @@ -974,48 +1136,71 @@ using H(5-9) apply (simp add: norm_eq norm_eq_1) apply (simp add: inner_diff scalar_mult_eq_scaleR) unfolding * - by (simp add: field_simps) } + apply (simp add: field_simps) + done + } note th0 = this let ?g = "\x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" - {fix x:: "real ^'n" assume nx: "norm x = 1" - have "?g x = f x" using nx by auto} - hence thfg: "\x. norm x = 1 \ ?g x = f x" by blast + { + fix x:: "real ^'n" + assume nx: "norm x = 1" + have "?g x = f x" using nx by auto + } + then have thfg: "\x. norm x = 1 \ ?g x = f x" + by blast have g0: "?g 0 = 0" by simp - {fix x y :: "real ^'n" - {assume "x = 0" "y = 0" - then have "dist (?g x) (?g y) = dist x y" by simp } + { + fix x y :: "real ^'n" + { + assume "x = 0" "y = 0" + then have "dist (?g x) (?g y) = dist x y" by simp + } moreover - {assume "x = 0" "y \ 0" + { + assume "x = 0" "y \ 0" then have "dist (?g x) (?g y) = dist x y" apply (simp add: dist_norm) apply (rule f1[rule_format]) - by(simp add: field_simps)} + apply (simp add: field_simps) + done + } moreover - {assume "x \ 0" "y = 0" + { + assume "x \ 0" "y = 0" then have "dist (?g x) (?g y) = dist x y" apply (simp add: dist_norm) apply (rule f1[rule_format]) - by(simp add: field_simps)} + apply (simp add: field_simps) + done + } moreover - {assume z: "x \ 0" "y \ 0" - have th00: "x = norm x *\<^sub>R (inverse (norm x) *\<^sub>R x)" "y = norm y *\<^sub>R (inverse (norm y) *\<^sub>R y)" "norm x *\<^sub>R f ((inverse (norm x) *\<^sub>R x)) = norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" + { + assume z: "x \ 0" "y \ 0" + have th00: + "x = norm x *\<^sub>R (inverse (norm x) *\<^sub>R x)" + "y = norm y *\<^sub>R (inverse (norm y) *\<^sub>R y)" + "norm x *\<^sub>R f ((inverse (norm x) *\<^sub>R x)) = norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" "norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y) = norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y)" "norm (inverse (norm x) *\<^sub>R x) = 1" "norm (f (inverse (norm x) *\<^sub>R x)) = 1" "norm (inverse (norm y) *\<^sub>R y) = 1" "norm (f (inverse (norm y) *\<^sub>R y)) = 1" "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) = - norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)" + norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)" using z by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm]) from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" - by (simp add: dist_norm)} - ultimately have "dist (?g x) (?g y) = dist x y" by blast} + by (simp add: dist_norm) + } + ultimately have "dist (?g x) (?g y) = dist x y" by blast + } note thd = this show ?thesis apply (rule exI[where x= ?g]) unfolding orthogonal_transformation_isometry - using g0 thfg thd by metis + using g0 thfg thd + apply metis + done qed (* ------------------------------------------------------------------------- *) @@ -1029,14 +1214,17 @@ fixes Q :: "'a::linordered_idom^'n^'n" shows " orthogonal_matrix Q \ rotation_matrix Q \ rotoinversion_matrix Q" by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) + (* ------------------------------------------------------------------------- *) (* Explicit formulas for low dimensions. *) (* ------------------------------------------------------------------------- *) -lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp +lemma setprod_1: "setprod f {(1::nat)..1} = f 1" + by simp lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2" by (simp add: eval_nat_numeral setprod_numseg mult_commute) + lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3" by (simp add: eval_nat_numeral setprod_numseg mult_commute) @@ -1044,33 +1232,33 @@ by (simp add: det_def sign_id) lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" -proof- +proof - have f12: "finite {2::2}" "1 \ {2::2}" by auto show ?thesis - unfolding det_def UNIV_2 - unfolding setsum_over_permutations_insert[OF f12] - unfolding permutes_sing - by (simp add: sign_swap_id sign_id swap_id_eq) + unfolding det_def UNIV_2 + unfolding setsum_over_permutations_insert[OF f12] + unfolding permutes_sing + by (simp add: sign_swap_id sign_id swap_id_eq) qed -lemma det_3: "det (A::'a::comm_ring_1^3^3) = - A$1$1 * A$2$2 * A$3$3 + - A$1$2 * A$2$3 * A$3$1 + - A$1$3 * A$2$1 * A$3$2 - - A$1$1 * A$2$3 * A$3$2 - - A$1$2 * A$2$1 * A$3$3 - - A$1$3 * A$2$2 * A$3$1" -proof- +lemma det_3: + "det (A::'a::comm_ring_1^3^3) = + A$1$1 * A$2$2 * A$3$3 + + A$1$2 * A$2$3 * A$3$1 + + A$1$3 * A$2$1 * A$3$2 - + A$1$1 * A$2$3 * A$3$2 - + A$1$2 * A$2$1 * A$3$3 - + A$1$3 * A$2$2 * A$3$1" +proof - have f123: "finite {2::3, 3}" "1 \ {2::3, 3}" by auto have f23: "finite {3::3}" "2 \ {3::3}" by auto show ?thesis - unfolding det_def UNIV_3 - unfolding setsum_over_permutations_insert[OF f123] - unfolding setsum_over_permutations_insert[OF f23] - - unfolding permutes_sing - by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) + unfolding det_def UNIV_3 + unfolding setsum_over_permutations_insert[OF f123] + unfolding setsum_over_permutations_insert[OF f23] + unfolding permutes_sing + by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) qed end diff -r 16235bb41881 -r 082d0972096b src/HOL/Multivariate_Analysis/Operator_Norm.thy --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Wed Aug 28 18:44:50 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Wed Aug 28 23:48:45 2013 +0200 @@ -11,72 +11,83 @@ definition "onorm f = Sup {norm (f x)| x. norm x = 1}" lemma norm_bound_generalize: - fixes f:: "'a::euclidean_space \ 'b::euclidean_space" + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes lf: "linear f" - shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" (is "?lhs \ ?rhs") -proof- - {assume H: ?rhs - {fix x :: "'a" assume x: "norm x = 1" - from H[rule_format, of x] x have "norm (f x) \ b" by simp} - then have ?lhs by blast } + shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" + (is "?lhs \ ?rhs") +proof + assume H: ?rhs + { + fix x :: "'a" + assume x: "norm x = 1" + from H[rule_format, of x] x have "norm (f x) \ b" by simp + } + then show ?lhs by blast +next + assume H: ?lhs + have bp: "b \ 0" + apply - + apply (rule order_trans [OF norm_ge_zero]) + apply (rule H[rule_format, of "SOME x::'a. x \ Basis"]) + apply (auto intro: SOME_Basis norm_Basis) + done + { + fix x :: "'a" + { + assume "x = 0" + then have "norm (f x) \ b * norm x" + by (simp add: linear_0[OF lf] bp) + } + moreover + { + assume x0: "x \ 0" + then have n0: "norm x \ 0" by (metis norm_eq_zero) + let ?c = "1/ norm x" + have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0) + with H have "norm (f (?c *\<^sub>R x)) \ b" by blast + then have "?c * norm (f x) \ b" + by (simp add: linear_cmul[OF lf]) + then have "norm (f x) \ b * norm x" + using n0 norm_ge_zero[of x] by (auto simp add: field_simps) + } + ultimately have "norm (f x) \ b * norm x" by blast + } + then show ?rhs by blast +qed - moreover - {assume H: ?lhs - have bp: "b \ 0" - apply - - apply(rule order_trans [OF norm_ge_zero]) - apply(rule H[rule_format, of "SOME x::'a. x \ Basis"]) - by (auto intro: SOME_Basis norm_Basis) - {fix x :: "'a" - {assume "x = 0" - then have "norm (f x) \ b * norm x" by (simp add: linear_0[OF lf] bp)} - moreover - {assume x0: "x \ 0" - hence n0: "norm x \ 0" by (metis norm_eq_zero) - let ?c = "1/ norm x" - have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0) - with H have "norm (f (?c *\<^sub>R x)) \ b" by blast - hence "?c * norm (f x) \ b" - by (simp add: linear_cmul[OF lf]) - hence "norm (f x) \ b * norm x" - using n0 norm_ge_zero[of x] by (auto simp add: field_simps)} - ultimately have "norm (f x) \ b * norm x" by blast} - then have ?rhs by blast} - ultimately show ?thesis by blast -qed - lemma onorm: fixes f:: "'a::euclidean_space \ 'b::euclidean_space" assumes lf: "linear f" - shows "norm (f x) <= onorm f * norm x" - and "\x. norm (f x) <= b * norm x \ onorm f <= b" -proof- - { - let ?S = "{norm (f x) |x. norm x = 1}" - have "norm (f (SOME i. i \ Basis)) \ ?S" - by (auto intro!: exI[of _ "SOME i. i \ Basis"] norm_Basis SOME_Basis) - hence Se: "?S \ {}" by auto - from linear_bounded[OF lf] have b: "\ b. ?S *<= b" - unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) - { from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] - show "norm (f x) <= onorm f * norm x" - apply - - apply (rule spec[where x = x]) - unfolding norm_bound_generalize[OF lf, symmetric] - by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} - { - show "\x. norm (f x) <= b * norm x \ onorm f <= b" - using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] - unfolding norm_bound_generalize[OF lf, symmetric] - by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} - } + shows "norm (f x) \ onorm f * norm x" + and "\x. norm (f x) \ b * norm x \ onorm f \ b" +proof - + let ?S = "{norm (f x) |x. norm x = 1}" + have "norm (f (SOME i. i \ Basis)) \ ?S" + by (auto intro!: exI[of _ "SOME i. i \ Basis"] norm_Basis SOME_Basis) + then have Se: "?S \ {}" by auto + from linear_bounded[OF lf] have b: "\ b. ?S *<= b" + unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) + from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] + show "norm (f x) <= onorm f * norm x" + apply - + apply (rule spec[where x = x]) + unfolding norm_bound_generalize[OF lf, symmetric] + apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def) + done + show "\x. norm (f x) <= b * norm x \ onorm f <= b" + using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]] + unfolding norm_bound_generalize[OF lf, symmetric] + by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def) qed -lemma onorm_pos_le: assumes lf: "linear (f::'n::euclidean_space \ 'm::euclidean_space)" shows "0 <= onorm f" - using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \ Basis"]] +lemma onorm_pos_le: + assumes lf: "linear (f::'n::euclidean_space \ 'm::euclidean_space)" + shows "0 \ onorm f" + using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \ Basis"]] by (simp add: SOME_Basis) -lemma onorm_eq_0: assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" +lemma onorm_eq_0: + assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" shows "onorm f = 0 \ (\x. f x = 0)" using onorm[OF lf] apply (auto simp add: onorm_pos_le) @@ -87,47 +98,53 @@ done lemma onorm_const: "onorm(\x::'a::euclidean_space. (y::'b::euclidean_space)) = norm y" -proof- +proof - let ?f = "\x::'a. (y::'b)" have th: "{norm (?f x)| x. norm x = 1} = {norm y}" by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \ Basis"]) show ?thesis unfolding onorm_def th - apply (rule cSup_unique) by (simp_all add: setle_def) + apply (rule cSup_unique) + apply (simp_all add: setle_def) + done qed -lemma onorm_pos_lt: assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" +lemma onorm_pos_lt: + assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" shows "0 < onorm f \ ~(\x. f x = 0)" unfolding onorm_eq_0[OF lf, symmetric] using onorm_pos_le[OF lf] by arith lemma onorm_compose: assumes lf: "linear (f::'n::euclidean_space \ 'm::euclidean_space)" - and lg: "linear (g::'k::euclidean_space \ 'n::euclidean_space)" - shows "onorm (f o g) <= onorm f * onorm g" - apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) - unfolding o_def - apply (subst mult_assoc) - apply (rule order_trans) - apply (rule onorm(1)[OF lf]) - apply (rule mult_left_mono) - apply (rule onorm(1)[OF lg]) - apply (rule onorm_pos_le[OF lf]) - done + and lg: "linear (g::'k::euclidean_space \ 'n::euclidean_space)" + shows "onorm (f o g) \ onorm f * onorm g" + apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) + unfolding o_def + apply (subst mult_assoc) + apply (rule order_trans) + apply (rule onorm(1)[OF lf]) + apply (rule mult_left_mono) + apply (rule onorm(1)[OF lg]) + apply (rule onorm_pos_le[OF lf]) + done -lemma onorm_neg_lemma: assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" +lemma onorm_neg_lemma: + assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" shows "onorm (\x. - f x) \ onorm f" using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] unfolding norm_minus_cancel by metis -lemma onorm_neg: assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" +lemma onorm_neg: + assumes lf: "linear (f::'a::euclidean_space \ 'b::euclidean_space)" shows "onorm (\x. - f x) = onorm f" using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] by simp lemma onorm_triangle: - assumes lf: "linear (f::'n::euclidean_space \ 'm::euclidean_space)" and lg: "linear g" - shows "onorm (\x. f x + g x) <= onorm f + onorm g" + assumes lf: "linear (f::'n::euclidean_space \ 'm::euclidean_space)" + and lg: "linear g" + shows "onorm (\x. f x + g x) \ onorm f + onorm g" apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) apply (rule order_trans) apply (rule norm_triangle_ineq) @@ -137,17 +154,20 @@ apply (rule onorm(1)[OF lg]) done -lemma onorm_triangle_le: "linear (f::'n::euclidean_space \ 'm::euclidean_space) \ linear g \ onorm(f) + onorm(g) <= e - \ onorm(\x. f x + g x) <= e" +lemma onorm_triangle_le: + "linear (f::'n::euclidean_space \ 'm::euclidean_space) \ + linear g \ onorm f + onorm g \ e \ onorm (\x. f x + g x) \ e" apply (rule order_trans) apply (rule onorm_triangle) apply assumption+ done -lemma onorm_triangle_lt: "linear (f::'n::euclidean_space \ 'm::euclidean_space) \ linear g \ onorm(f) + onorm(g) < e - ==> onorm(\x. f x + g x) < e" +lemma onorm_triangle_lt: + "linear (f::'n::euclidean_space \ 'm::euclidean_space) \ linear g \ + onorm f + onorm g < e \ onorm(\x. f x + g x) < e" apply (rule order_le_less_trans) apply (rule onorm_triangle) - by assumption+ + apply assumption+ + done end diff -r 16235bb41881 -r 082d0972096b src/Pure/Thy/completion.scala --- a/src/Pure/Thy/completion.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Pure/Thy/completion.scala Wed Aug 28 23:48:45 2013 +0200 @@ -27,12 +27,13 @@ def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r - def word: Parser[String] = "[a-zA-Z0-9_']{2,}".r + def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r + def word: Parser[String] = """[a-zA-Z0-9_']{3,}""".r def read(in: CharSequence): Option[String] = { val reverse_in = new Library.Reverse(in) - parse((reverse_symbol | reverse_symb | word) ^^ (_.reverse), reverse_in) match { + parse((reverse_symbol | reverse_symb | escape | word) ^^ (_.reverse), reverse_in) match { case Success(result, _) => Some(result) case _ => None } @@ -61,7 +62,7 @@ { val words = (for ((x, _) <- Symbol.names) yield (x, x)).toList ::: - (for ((x, y) <- Symbol.names) yield (y, x)).toList ::: + (for ((x, y) <- Symbol.names) yield ("\\" + y, x)).toList ::: (for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList val abbrs = diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/etc/options Wed Aug 28 23:48:45 2013 +0200 @@ -9,18 +9,18 @@ public option jedit_font_scale : real = 1.0 -- "scale factor of add-on panels wrt. main text area" +public option jedit_popup_font_scale : real = 0.85 + -- "scale factor of popups wrt. main text area" + +public option jedit_popup_bounds : real = 0.5 + -- "relative bounds of popup window wrt. logical screen size" + public option jedit_tooltip_delay : real = 0.75 -- "open/close delay for document tooltips" -public option jedit_tooltip_font_scale : real = 0.85 - -- "scale factor of tooltips wrt. main text area" - public option jedit_tooltip_margin : int = 60 -- "margin for tooltip pretty-printing" -public option jedit_tooltip_bounds : real = 0.5 - -- "relative bounds of tooltip window wrt. logical screen size" - public option jedit_text_overview_limit : int = 100000 -- "maximum amount of text to visualize in overview column" diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Wed Aug 28 23:48:45 2013 +0200 @@ -33,6 +33,7 @@ "src/osx_adapter.scala" "src/output_dockable.scala" "src/plugin.scala" + "src/popup.scala" "src/pretty_text_area.scala" "src/pretty_tooltip.scala" "src/process_indicator.scala" diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Wed Aug 28 23:48:45 2013 +0200 @@ -1,7 +1,7 @@ /* Title: Tools/jEdit/src/completion_popup.scala Author: Makarius -Completion popup based on javax.swing.PopupFactory. +Completion popup. */ package isabelle.jedit @@ -9,56 +9,162 @@ import isabelle._ -import java.awt.{Point, BorderLayout, Dimension} -import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} -import javax.swing.{JPanel, JComponent, PopupFactory} +import java.awt.{Font, Point, BorderLayout, Dimension} +import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} +import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities} import scala.swing.{ListView, ScrollPane} import scala.swing.event.MouseClicked import org.gjt.sp.jedit.View +import org.gjt.sp.jedit.textarea.JEditTextArea object Completion_Popup { - sealed case class Item(name: String, text: String) - { override def toString: String = text } + /* items */ + + private sealed case class Item(original: String, replacement: String, description: String) + { override def toString: String = description } + + + /* maintain single instance */ - def apply( - opt_view: Option[View], - parent: JComponent, - screen_point: Point, - items: List[Item], - complete: Item => Unit): Completion_Popup = + def dismissed(layered: JLayeredPane): Boolean = + { + Swing_Thread.require() + + layered.getClientProperty(Completion_Popup) match { + case old_completion: Completion_Popup => + old_completion.hide_popup() + true + case _ => + false + } + } + + private def register(layered: JLayeredPane, completion: Completion_Popup) { Swing_Thread.require() - require(!items.isEmpty) + dismissed(layered) + layered.putClientProperty(Completion_Popup, completion) + } + + + /* jEdit text area operations */ + + object Text_Area + { + private def insert(text_area: JEditTextArea, item: Item) + { + Swing_Thread.require() + + val buffer = text_area.getBuffer + val len = item.original.length + if (buffer.isEditable && len > 0) { + JEdit_Lib.buffer_edit(buffer) { + val caret = text_area.getCaretPosition + JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match { + case Some(text) if text == item.original => + buffer.remove(caret - len, len) + buffer.insert(caret - len, item.replacement) + case _ => + } + } + } + } + + def input(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent) + { + Swing_Thread.require() + + val view = text_area.getView + val layered = view.getLayeredPane + val buffer = text_area.getBuffer + val painter = text_area.getPainter + + if (buffer.isEditable && !evt.isConsumed) { + dismissed(layered) - val completion = new Completion_Popup(opt_view, parent, screen_point, items, complete) - completion.show_popup() - completion + get_syntax match { + case Some(syntax) => + val caret = text_area.getCaretPosition + val result = + { + val line = buffer.getLineOfOffset(caret) + val start = buffer.getLineStartOffset(line) + val text = buffer.getSegment(start, caret - start) + + syntax.completion.complete(text) match { + case Some((word, cs)) => + val ds = + (if (Isabelle_Encoding.is_active(buffer)) + cs.map(Symbol.decode(_)).sorted + else cs).filter(_ != word) + if (ds.isEmpty) None + else Some((word, ds.map(s => Item(word, s, s)))) + case None => None + } + } + result match { + case Some((original, items)) => + val popup_font = + painter.getFont.deriveFont( + (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat + max 10.0f) + + val loc1 = text_area.offsetToXY(caret - original.length) + if (loc1 != null) { + val loc2 = + SwingUtilities.convertPoint(painter, + loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) + val completion = + new Completion_Popup(layered, loc2, popup_font, items) { + override def complete(item: Item) { insert(text_area, item) } + override def propagate(e: KeyEvent) { + JEdit_Lib.propagate_key(view, e) + input(text_area, get_syntax, e) + } + override def refocus() { text_area.requestFocus } + } + register(layered, completion) + completion.show_popup() + } + case None => + } + case None => + } + } + } } } class Completion_Popup private( - opt_view: Option[View], - parent: JComponent, - screen_point: Point, - items: List[Completion_Popup.Item], - complete: Completion_Popup.Item => Unit) extends JPanel(new BorderLayout) + layered: JLayeredPane, + location: Point, + popup_font: Font, + items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout) { completion => Swing_Thread.require() + require(!items.isEmpty) + + + /* actions */ + + def complete(item: Completion_Popup.Item) { } + def propagate(evt: KeyEvent) { } + def refocus() { } /* list view */ private val list_view = new ListView(items) { - font = parent.getFont + font = popup_font } list_view.selection.intervalMode = ListView.IntervalMode.Single list_view.peer.setFocusTraversalKeysEnabled(false) @@ -92,49 +198,33 @@ /* event handling */ - private val key_handler = new KeyAdapter { - override def keyPressed(e: KeyEvent) - { - if (!e.isConsumed) { - e.getKeyCode match { - case KeyEvent.VK_TAB => - if (complete_selected()) e.consume - hide_popup() - case KeyEvent.VK_ESCAPE => - hide_popup() - e.consume - case KeyEvent.VK_UP => move_items(-1); e.consume - case KeyEvent.VK_DOWN => move_items(1); e.consume - case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume - case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume - case _ => - if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) - hide_popup() - } - } - if (!e.isConsumed) pass_to_view(e) - } + private val key_listener = + JEdit_Lib.key_listener( + key_pressed = (e: KeyEvent) => + { + if (!e.isConsumed) { + e.getKeyCode match { + case KeyEvent.VK_TAB => + if (complete_selected()) e.consume + hide_popup() + case KeyEvent.VK_ESCAPE => + hide_popup() + e.consume + case KeyEvent.VK_UP => move_items(-1); e.consume + case KeyEvent.VK_DOWN => move_items(1); e.consume + case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume + case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume + case _ => + if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) + hide_popup() + } + } + propagate(e) + }, + key_typed = propagate _ + ) - override def keyTyped(e: KeyEvent) - { - if (!e.isConsumed) pass_to_view(e) - } - } - - private def pass_to_view(e: KeyEvent) - { - opt_view match { - case Some(view) if view.getKeyEventInterceptor == key_handler => - try { - view.setKeyEventInterceptor(null) - view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false) - } - finally { view.setKeyEventInterceptor(key_handler) } - case _ => - } - } - - list_view.peer.addKeyListener(key_handler) + list_view.peer.addKeyListener(key_listener) list_view.peer.addMouseListener(new MouseAdapter { override def mouseClicked(e: MouseEvent) { @@ -159,37 +249,29 @@ private val popup = { - val screen_bounds = JEdit_Lib.screen_bounds(screen_point) - - val geometry = JEdit_Lib.window_geometry(completion, completion) - - val w = geometry.width min (screen_bounds.width / 2) - val h = geometry.height min (screen_bounds.height / 2) - - completion.setSize(new Dimension(w, h)) - completion.setPreferredSize(new Dimension(w, h)) - - val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w) - val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h) - PopupFactory.getSharedInstance.getPopup(parent, completion, x, y) + val screen = JEdit_Lib.screen_location(layered, location) + val size = + { + val geometry = JEdit_Lib.window_geometry(completion, completion) + val bounds = Rendering.popup_bounds + val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth + val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight + new Dimension(w, h) + } + new Popup(layered, completion, screen.relative(layered, size), size) } - def show_popup() + private def show_popup() { - opt_view.foreach(view => view.setKeyEventInterceptor(key_handler)) popup.show list_view.requestFocus } - def hide_popup() + private def hide_popup() { - opt_view match { - case Some(view) if view.getKeyEventInterceptor == key_handler => - view.setKeyEventInterceptor(null) - case _ => - } + val had_focus = list_view.peer.isFocusOwner popup.hide - parent.requestFocus + if (had_focus) refocus() } } diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Wed Aug 28 23:48:45 2013 +0200 @@ -17,7 +17,7 @@ import java.lang.System import java.text.BreakIterator import java.awt.{Color, Graphics2D, Point} -import java.awt.event.{KeyEvent, KeyAdapter} +import java.awt.event.KeyEvent import javax.swing.event.{CaretListener, CaretEvent} import org.gjt.sp.jedit.{jEdit, Debug} @@ -149,13 +149,15 @@ /* key listener */ - private val key_listener = new KeyAdapter { - override def keyTyped(evt: KeyEvent) - { - if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all()) - evt.consume - } - } + private val key_listener = + JEdit_Lib.key_listener( + key_pressed = (evt: KeyEvent) => + { + if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView)) + evt.consume + }, + key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _) + ) /* caret handling */ diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Aug 28 23:48:45 2013 +0200 @@ -9,7 +9,7 @@ import isabelle._ -import javax.swing.{SwingUtilities, JComponent} +import javax.swing.JComponent import java.awt.Point import java.awt.event.{WindowFocusListener, WindowEvent} @@ -66,10 +66,8 @@ Pretty_Tooltip.invoke(() => { val rendering = Rendering(snapshot, PIDE.options.value) - val screen_point = new Point(x, y) - SwingUtilities.convertPointToScreen(screen_point, parent) val info = Text.Info(Text.Range(~1), body) - Pretty_Tooltip(view, parent, rendering, screen_point, Command.Results.empty, info) + Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info) }) null } diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Aug 28 23:48:45 2013 +0200 @@ -188,6 +188,9 @@ class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure( "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name) +{ + override def supportsCompletion = false +} class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure( diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Aug 28 23:48:45 2013 +0200 @@ -9,28 +9,56 @@ import isabelle._ -import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle} -import javax.swing.{Icon, ImageIcon, JWindow} +import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension} +import java.awt.event.{KeyEvent, KeyListener} +import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} import scala.annotation.tailrec import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities} +import org.gjt.sp.jedit.gui.KeyEventWorkaround import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} object JEdit_Lib { - /* bounds within multi-screen environment */ + /* location within multi-screen environment */ + + final case class Screen_Location(point: Point, bounds: Rectangle) + { + def relative(parent: Component, size: Dimension): Point = + { + val w = size.width + val h = size.height - def screen_bounds(screen_point: Point): Rectangle = + val x0 = parent.getLocationOnScreen.x + val y0 = parent.getLocationOnScreen.y + val x1 = x0 + parent.getWidth - w + val y1 = y0 + parent.getHeight - h + val x2 = point.x min (bounds.x + bounds.width - w) + val y2 = point.y min (bounds.y + bounds.height - h) + + val location = new Point((x2 min x1) max x0, (y2 min y1) max y0) + SwingUtilities.convertPointFromScreen(location, parent) + location + } + } + + def screen_location(component: Component, point: Point): Screen_Location = { + val screen_point = new Point(point.x, point.y) + SwingUtilities.convertPointToScreen(screen_point, component) + val ge = GraphicsEnvironment.getLocalGraphicsEnvironment - (for { - device <- ge.getScreenDevices.iterator - config <- device.getConfigurations.iterator - bounds = config.getBounds - } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds + val screen_bounds = + (for { + device <- ge.getScreenDevices.iterator + config <- device.getConfigurations.iterator + bounds = config.getBounds + } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds + + Screen_Location(screen_point, screen_bounds) } @@ -106,21 +134,6 @@ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath - /* focus of main window */ - - def request_focus_view: Unit = - { - jEdit.getActiveView() match { - case null => - case view => - view.getTextArea match { - case null => - case text_area => text_area.requestFocus - } - } - } - - /* main jEdit components */ def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator @@ -300,5 +313,42 @@ case icon: ImageIcon => icon case _ => error("Bad image icon: " + name) } + + + /* key event handling */ + + def request_focus_view + { + val view = jEdit.getActiveView() + if (view != null) { + val text_area = view.getTextArea + if (text_area != null) text_area.requestFocus + } + } + + def propagate_key(view: View, evt: KeyEvent) + { + if (view != null && !evt.isConsumed) + view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false) + } + + def key_listener( + key_typed: KeyEvent => Unit = _ => (), + key_pressed: KeyEvent => Unit = _ => (), + key_released: KeyEvent => Unit = _ => ()): KeyListener = + { + def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit) + { + val evt = KeyEventWorkaround.processKeyEvent(evt0) + if (evt != null) handle(evt) + } + + new KeyListener + { + def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) } + def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) } + def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) } + } + } } diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 28 23:48:45 2013 +0200 @@ -53,6 +53,16 @@ lazy val editor = new JEdit_Editor + /* popups */ + + def dismissed_popups(view: View): Boolean = + { + val b1 = Completion_Popup.dismissed(view.getLayeredPane) + val b2 = Pretty_Tooltip.dismissed_all() + b1 || b2 + } + + /* document model and view */ def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer) @@ -265,7 +275,7 @@ PIDE.init_view(buffer, text_area) } else { - Pretty_Tooltip.dismissed_all() + PIDE.dismissed_popups(text_area.getView) PIDE.exit_view(buffer, text_area) } } diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/popup.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/popup.scala Wed Aug 28 23:48:45 2013 +0200 @@ -0,0 +1,40 @@ +/* Title: Tools/jEdit/src/popup.scala + Author: Makarius + +Popup within layered pane. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.awt.{Point, Dimension} +import javax.swing.{JLayeredPane, JComponent} + + +class Popup( + layered: JLayeredPane, + component: JComponent, + location: Point, + size: Dimension) +{ + def show + { + component.setLocation(location) + component.setSize(size) + component.setPreferredSize(size) + component.setOpaque(true) + layered.add(component, JLayeredPane.POPUP_LAYER) + layered.moveToFront(component) + layered.repaint(component.getBounds()) + } + + def hide + { + val bounds = component.getBounds() + layered.remove(component) + layered.repaint(bounds) + } +} + diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Aug 28 23:48:45 2013 +0200 @@ -11,7 +11,7 @@ import isabelle._ import java.awt.{Color, Font, FontMetrics, Toolkit, Window} -import java.awt.event.{KeyEvent, KeyAdapter} +import java.awt.event.KeyEvent import org.gjt.sp.jedit.{jEdit, View, Registers} import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea} @@ -162,33 +162,33 @@ /* key handling */ - addKeyListener(new KeyAdapter { - override def keyPressed(evt: KeyEvent) - { - evt.getKeyCode match { - case KeyEvent.VK_C - if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => - Registers.copy(text_area, '$') - evt.consume - case KeyEvent.VK_A - if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => - text_area.selectAll - evt.consume - case _ => + addKeyListener(JEdit_Lib.key_listener( + key_pressed = (evt: KeyEvent) => + { + evt.getKeyCode match { + case KeyEvent.VK_C + if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => + Registers.copy(text_area, '$') + evt.consume + + case KeyEvent.VK_A + if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 => + text_area.selectAll + evt.consume + + case KeyEvent.VK_ESCAPE => + if (PIDE.dismissed_popups(view)) evt.consume + + case _ => + } + if (propagate_keys) JEdit_Lib.propagate_key(view, evt) + }, + key_typed = (evt: KeyEvent) => + { + if (propagate_keys) JEdit_Lib.propagate_key(view, evt) } - if (propagate_keys && !evt.isConsumed) - view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false) - } - - override def keyTyped(evt: KeyEvent) - { - if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all()) - evt.consume - - if (propagate_keys && !evt.isConsumed) - view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false) - } - }) + ) + ) /* init */ diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Aug 28 23:48:45 2013 +0200 @@ -1,7 +1,7 @@ /* Title: Tools/jEdit/src/pretty_tooltip.scala Author: Makarius -Enhanced tooltip window based on Pretty_Text_Area. +Tooltip based on Pretty_Text_Area. */ package isabelle.jedit @@ -11,7 +11,7 @@ import java.awt.{Color, Point, BorderLayout, Dimension} import java.awt.event.{FocusAdapter, FocusEvent} -import javax.swing.{JPanel, JComponent, PopupFactory} +import javax.swing.{JPanel, JComponent, SwingUtilities} import javax.swing.border.LineBorder import scala.swing.{FlowPanel, Label} @@ -39,8 +39,8 @@ def apply( view: View, parent: JComponent, + location: Point, rendering: Rendering, - screen_point: Point, results: Command.Results, info: Text.Info[XML.Body]): Pretty_Tooltip = { @@ -56,7 +56,8 @@ } old.foreach(_.hide_popup) - val tip = new Pretty_Tooltip(view, rendering, screen_point, results, info) + val loc = SwingUtilities.convertPoint(parent, location, view.getLayeredPane) + val tip = new Pretty_Tooltip(view, loc, rendering, results, info) stack = tip :: rest tip.show_popup tip @@ -138,8 +139,8 @@ class Pretty_Tooltip private( view: View, + location: Point, rendering: Rendering, - screen_point: Point, private val results: Command.Results, private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout) { @@ -195,7 +196,7 @@ }) pretty_text_area.resize(Rendering.font_family(), - Rendering.font_size("jedit_tooltip_font_scale").round) + Rendering.font_size("jedit_popup_font_scale").round) /* main content */ @@ -217,15 +218,9 @@ private val popup = { - val screen_bounds = JEdit_Lib.screen_bounds(screen_point) - - val root = view.getRootPane - val x0 = root.getLocationOnScreen.x - val y0 = root.getLocationOnScreen.y - val w0 = root.getWidth - val h0 = root.getHeight - - val (w, h) = + val layered = view.getLayeredPane + val screen = JEdit_Lib.screen_location(layered, location) + val size = { val painter = pretty_text_area.getPainter val metric = JEdit_Lib.pretty_metric(painter) @@ -237,10 +232,11 @@ (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length) val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter) - val bounds = rendering.tooltip_bounds + val bounds = Rendering.popup_bounds + val h0 = layered.getHeight val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height - val h2 = h0 min (screen_bounds.height * bounds).toInt + val h2 = h0 min (screen.bounds.height * bounds).toInt val h = h1 min h2 val margin1 = @@ -248,25 +244,14 @@ (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) }) else margin + val w0 = layered.getWidth val w1 = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width - val w2 = w0 min (screen_bounds.width * bounds).toInt + val w2 = w0 min (screen.bounds.width * bounds).toInt val w = w1 min w2 - (w, h) + new Dimension(w, h) } - - val (x, y) = - { - val x1 = x0 + w0 - w - val y1 = y0 + h0 - h - val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w) - val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h) - ((x2 min x1) max x0, (y2 min y1) max y0) - } - - tip.setSize(new Dimension(w, h)) - tip.setPreferredSize(new Dimension(w, h)) - PopupFactory.getSharedInstance.getPopup(root, tip, x, y) + new Popup(layered, tip, screen.relative(layered, size), size) } private def show_popup diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Wed Aug 28 23:48:45 2013 +0200 @@ -49,6 +49,11 @@ (jEdit.getIntegerProperty("view.fontsize", 16) * PIDE.options.real(scale)).toFloat + /* popup window bounds */ + + def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8 + + /* token markup -- text styles */ private val command_style: Map[String, Byte] = @@ -372,7 +377,6 @@ } val tooltip_margin: Int = options.int("jedit_tooltip_margin") - val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8 lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon")) diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Aug 28 23:48:45 2013 +0200 @@ -208,10 +208,9 @@ case None => case Some(tip) => val painter = text_area.getPainter - val screen_point = evt.getLocationOnScreen - screen_point.translate(0, painter.getFontMetrics.getHeight / 2) + val loc = new Point(x, y + painter.getFontMetrics.getHeight / 2) val results = rendering.command_results(range) - Pretty_Tooltip(view, painter, rendering, screen_point, results, tip) + Pretty_Tooltip(view, painter, loc, rendering, results, tip) } } } diff -r 16235bb41881 -r 082d0972096b src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Wed Aug 28 18:44:50 2013 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Wed Aug 28 23:48:45 2013 +0200 @@ -285,7 +285,11 @@ def refresh_buffer(buffer: JEditBuffer) { buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker) - markers.get(buffer.getMode.getName).map(buffer.setTokenMarker(_)) + // FIXME potential NPE ahead!?! + val mode = buffer.getMode + val name = mode.getName + val marker = markers.get(name) + marker.map(buffer.setTokenMarker(_)) } }