summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | eberlm |

Tue, 03 Nov 2015 11:20:21 +0100 | |

changeset 61553 | 933eb9e6a1cc |

parent 61533 | 980dd46a03fb (current diff) |

parent 61552 | 078c9fd2e052 (diff) |

child 61554 | 84901b8aa4f5 |

child 61609 | 77b453bd616f |

Merged

src/HOL/Isar_Examples/document/style.tex | file | annotate | diff | comparison | revisions |

--- a/Admin/components/components.sha1 Mon Nov 02 16:17:09 2015 +0100 +++ b/Admin/components/components.sha1 Tue Nov 03 11:20:21 2015 +0100 @@ -2,6 +2,7 @@ 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz 4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz +b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz 03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz 842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz

--- a/Admin/components/main Mon Nov 02 16:17:09 2015 +0100 +++ b/Admin/components/main Tue Nov 03 11:20:21 2015 +0100 @@ -1,6 +1,6 @@ #main components for everyday use, without big impact on overall build time csdp-6.x -cvc4-1.5pre-2 +cvc4-1.5pre-3 e-1.8 exec_process-1.0.3 Haskabelle-2015

--- a/NEWS Mon Nov 02 16:17:09 2015 +0100 +++ b/NEWS Tue Nov 03 11:20:21 2015 +0100 @@ -79,6 +79,9 @@ standard Isabelle fonts provide glyphs to render important control symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". +* System option "document_symbols" determines completion of Isabelle +symbols within document source. + * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. Consequently, \<open>...\<close> without any decoration prints literal quasi-formal text. Command-line tool "isabelle update_cartouches -t" helps to update @@ -397,6 +400,9 @@ - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF structure on the raw type to an abstract type defined using typedef. - Always generate "case_transfer" theorem. + - Allow discriminators and selectors with the same name as the type + being defined. + - Avoid various internal name clashes (e.g., 'datatype f = f'). * Transfer: - new methods for interactive debugging of 'transfer' and

--- a/etc/options Mon Nov 02 16:17:09 2015 +0100 +++ b/etc/options Tue Nov 03 11:20:21 2015 +0100 @@ -164,3 +164,5 @@ public option completion_limit : int = 40 -- "limit for completion within the formal context" +public option document_symbols : bool = false + -- "completion of Isabelle symbols within document source"

--- a/src/HOL/BNF_Fixpoint_Base.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/BNF_Fixpoint_Base.thy Tue Nov 03 11:20:21 2015 +0100 @@ -14,9 +14,6 @@ imports BNF_Composition Basic_BNFs begin -lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True" - by standard simp_all - lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)" by standard simp_all

--- a/src/HOL/Data_Structures/AList_Upd_Del.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Data_Structures/AList_Upd_Del.thy Tue Nov 03 11:20:21 2015 +0100 @@ -14,39 +14,39 @@ hide_const (open) map_of fun map_of :: "('a*'b)list \<Rightarrow> 'a \<Rightarrow> 'b option" where -"map_of [] = (\<lambda>a. None)" | -"map_of ((x,y)#ps) = (\<lambda>a. if x=a then Some y else map_of ps a)" +"map_of [] = (\<lambda>x. None)" | +"map_of ((a,b)#ps) = (\<lambda>x. if x=a then Some b else map_of ps x)" text \<open>Updating an association list:\<close> fun upd_list :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) list \<Rightarrow> ('a*'b) list" where -"upd_list a b [] = [(a,b)]" | -"upd_list a b ((x,y)#ps) = - (if a < x then (a,b)#(x,y)#ps else - if a=x then (a,b)#ps else (x,y) # upd_list a b ps)" +"upd_list x y [] = [(x,y)]" | +"upd_list x y ((a,b)#ps) = + (if x < a then (x,y)#(a,b)#ps else + if x = a then (x,y)#ps else (a,b) # upd_list x y ps)" fun del_list :: "'a::linorder \<Rightarrow> ('a*'b)list \<Rightarrow> ('a*'b)list" where -"del_list a [] = []" | -"del_list a ((x,y)#ps) = (if a=x then ps else (x,y) # del_list a ps)" +"del_list x [] = []" | +"del_list x ((a,b)#ps) = (if x = a then ps else (a,b) # del_list x ps)" subsection \<open>Lemmas for @{const map_of}\<close> -lemma map_of_ins_list: "map_of (upd_list a b ps) = (map_of ps)(a := Some b)" +lemma map_of_ins_list: "map_of (upd_list x y ps) = (map_of ps)(x := Some y)" by(induction ps) auto -lemma map_of_append: "map_of (ps @ qs) a = - (case map_of ps a of None \<Rightarrow> map_of qs a | Some b \<Rightarrow> Some b)" +lemma map_of_append: "map_of (ps @ qs) x = + (case map_of ps x of None \<Rightarrow> map_of qs x | Some y \<Rightarrow> Some y)" by(induction ps)(auto) -lemma map_of_None: "sorted (a # map fst ps) \<Longrightarrow> map_of ps a = None" +lemma map_of_None: "sorted (x # map fst ps) \<Longrightarrow> map_of ps x = None" by (induction ps) (auto simp: sorted_lems sorted_Cons_iff) -lemma map_of_None2: "sorted (map fst ps @ [a]) \<Longrightarrow> map_of ps a = None" +lemma map_of_None2: "sorted (map fst ps @ [x]) \<Longrightarrow> map_of ps x = None" by (induction ps) (auto simp: sorted_lems) lemma map_of_del_list: "sorted1 ps \<Longrightarrow> - map_of(del_list a ps) = (map_of ps)(a := None)" + map_of(del_list x ps) = (map_of ps)(x := None)" by(induction ps) (auto simp: map_of_None sorted_lems fun_eq_iff) lemma map_of_sorted_Cons: "sorted (a # map fst ps) \<Longrightarrow> x < a \<Longrightarrow> @@ -63,19 +63,19 @@ subsection \<open>Lemmas for @{const upd_list}\<close> -lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list a b ps)" -apply(induction ps) +lemma sorted_upd_list: "sorted1 ps \<Longrightarrow> sorted1 (upd_list x y ps)" +apply(induction ps) apply simp apply(case_tac ps) apply auto done -lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [x]); a < x \<rbrakk> \<Longrightarrow> - upd_list a b (ps @ (x,y) # qs) = upd_list a b ps @ (x,y) # qs" +lemma upd_list_sorted1: "\<lbrakk> sorted (map fst ps @ [a]); x < a \<rbrakk> \<Longrightarrow> + upd_list x y (ps @ (a,b) # qs) = upd_list x y ps @ (a,b) # qs" by(induction ps) (auto simp: sorted_lems) -lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [x]); x \<le> a \<rbrakk> \<Longrightarrow> - upd_list a b (ps @ (x,y) # qs) = ps @ upd_list a b ((x,y)#qs)" +lemma upd_list_sorted2: "\<lbrakk> sorted (map fst ps @ [a]); a \<le> x \<rbrakk> \<Longrightarrow> + upd_list x y (ps @ (a,b) # qs) = ps @ upd_list x y ((a,b) # qs)" by(induction ps) (auto simp: sorted_lems) lemmas upd_list_simps = sorted_lems upd_list_sorted1 upd_list_sorted2 @@ -110,28 +110,28 @@ lemma del_list_idem: "x \<notin> set(map fst xs) \<Longrightarrow> del_list x xs = xs" by (induct xs) auto -lemma del_list_sorted1: "sorted1 (xs @ [(x,y)]) \<Longrightarrow> x \<le> a \<Longrightarrow> - del_list a (xs @ (x,y) # ys) = xs @ del_list a ((x,y) # ys)" +lemma del_list_sorted1: "sorted1 (xs @ [(a,b)]) \<Longrightarrow> a \<le> x \<Longrightarrow> + del_list x (xs @ (a,b) # ys) = xs @ del_list x ((a,b) # ys)" by (induction xs) (auto simp: sorted_mid_iff2) -lemma del_list_sorted2: "sorted1 (xs @ (x,y) # ys) \<Longrightarrow> a < x \<Longrightarrow> - del_list a (xs @ (x,y) # ys) = del_list a xs @ (x,y) # ys" +lemma del_list_sorted2: "sorted1 (xs @ (a,b) # ys) \<Longrightarrow> x < a \<Longrightarrow> + del_list x (xs @ (a,b) # ys) = del_list x xs @ (a,b) # ys" by (induction xs) (fastforce simp: sorted_Cons_iff intro!: del_list_idem)+ lemma del_list_sorted3: - "sorted1 (xs @ (x,x') # ys @ (y,y') # zs) \<Longrightarrow> a < y \<Longrightarrow> - del_list a (xs @ (x,x') # ys @ (y,y') # zs) = del_list a (xs @ (x,x') # ys) @ (y,y') # zs" + "sorted1 (xs @ (a,a') # ys @ (b,b') # zs) \<Longrightarrow> x < b \<Longrightarrow> + del_list x (xs @ (a,a') # ys @ (b,b') # zs) = del_list x (xs @ (a,a') # ys) @ (b,b') # zs" by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2 ball_Un) lemma del_list_sorted4: - "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) \<Longrightarrow> a < z \<Longrightarrow> - del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) = del_list a (xs @ (x,x') # ys @ (y,y') # zs) @ (z,z') # us" + "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) \<Longrightarrow> x < c \<Longrightarrow> + del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) = del_list x (xs @ (a,a') # ys @ (b,b') # zs) @ (c,c') # us" by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3) lemma del_list_sorted5: - "sorted1 (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) \<Longrightarrow> a < u \<Longrightarrow> - del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us @ (u,u') # vs) = - del_list a (xs @ (x,x') # ys @ (y,y') # zs @ (z,z') # us) @ (u,u') # vs" + "sorted1 (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) \<Longrightarrow> x < d \<Longrightarrow> + del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us @ (d,d') # vs) = + del_list x (xs @ (a,a') # ys @ (b,b') # zs @ (c,c') # us) @ (d,d') # vs" by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4) lemmas del_list_sorted =

--- a/src/HOL/Data_Structures/List_Ins_Del.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Data_Structures/List_Ins_Del.thy Tue Nov 03 11:20:21 2015 +0100 @@ -52,8 +52,8 @@ fun ins_list :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where "ins_list x [] = [x]" | -"ins_list x (y#zs) = - (if x < y then x#y#zs else if x=y then x#zs else y # ins_list x zs)" +"ins_list x (a#xs) = + (if x < a then x#a#xs else if x=a then a#xs else a # ins_list x xs)" lemma set_ins_list[simp]: "elems (ins_list x xs) = insert x (elems xs)" by(induction xs) auto @@ -66,12 +66,12 @@ lemma sorted_ins_list: "sorted xs \<Longrightarrow> sorted(ins_list x xs)" by(induction xs rule: sorted.induct) auto -lemma ins_list_sorted1: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> - ins_list x (xs @ y # ys) = xs @ ins_list x (y#ys)" +lemma ins_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> + ins_list x (xs @ a # ys) = xs @ ins_list x (a#ys)" by(induction xs) (auto simp: sorted_lems) -lemma ins_list_sorted2: "sorted (xs @ [y]) \<Longrightarrow> x < y \<Longrightarrow> - ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)" +lemma ins_list_sorted2: "sorted (xs @ [a]) \<Longrightarrow> x < a \<Longrightarrow> + ins_list x (xs @ a # ys) = ins_list x xs @ (a#ys)" by(induction xs) (auto simp: sorted_lems) lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2 @@ -80,8 +80,8 @@ subsection \<open>Delete one occurrence of an element from a list:\<close> fun del_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where -"del_list a [] = []" | -"del_list a (x#xs) = (if a=x then xs else x # del_list a xs)" +"del_list x [] = []" | +"del_list x (a#xs) = (if x=a then xs else a # del_list x xs)" lemma del_list_idem: "x \<notin> elems xs \<Longrightarrow> del_list x xs = xs" by (induct xs) simp_all @@ -99,28 +99,28 @@ apply auto by (meson order.strict_trans sorted_Cons_iff) -lemma del_list_sorted1: "sorted (xs @ [x]) \<Longrightarrow> x \<le> y \<Longrightarrow> - del_list y (xs @ x # ys) = xs @ del_list y (x # ys)" +lemma del_list_sorted1: "sorted (xs @ [a]) \<Longrightarrow> a \<le> x \<Longrightarrow> + del_list x (xs @ a # ys) = xs @ del_list x (a # ys)" by (induction xs) (auto simp: sorted_mid_iff2) -lemma del_list_sorted2: "sorted (xs @ x # ys) \<Longrightarrow> y < x \<Longrightarrow> - del_list y (xs @ x # ys) = del_list y xs @ x # ys" +lemma del_list_sorted2: "sorted (xs @ a # ys) \<Longrightarrow> x < a \<Longrightarrow> + del_list x (xs @ a # ys) = del_list x xs @ a # ys" by (induction xs) (auto simp: sorted_Cons_iff intro!: del_list_idem) lemma del_list_sorted3: - "sorted (xs @ x # ys @ y # zs) \<Longrightarrow> a < y \<Longrightarrow> - del_list a (xs @ x # ys @ y # zs) = del_list a (xs @ x # ys) @ y # zs" + "sorted (xs @ a # ys @ b # zs) \<Longrightarrow> x < b \<Longrightarrow> + del_list x (xs @ a # ys @ b # zs) = del_list x (xs @ a # ys) @ b # zs" by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted2) lemma del_list_sorted4: - "sorted (xs @ x # ys @ y # zs @ z # us) \<Longrightarrow> a < z \<Longrightarrow> - del_list a (xs @ x # ys @ y # zs @ z # us) = del_list a (xs @ x # ys @ y # zs) @ z # us" + "sorted (xs @ a # ys @ b # zs @ c # us) \<Longrightarrow> x < c \<Longrightarrow> + del_list x (xs @ a # ys @ b # zs @ c # us) = del_list x (xs @ a # ys @ b # zs) @ c # us" by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted3) lemma del_list_sorted5: - "sorted (xs @ x # ys @ y # zs @ z # us @ u # vs) \<Longrightarrow> a < u \<Longrightarrow> - del_list a (xs @ x # ys @ y # zs @ z # us @ u # vs) = - del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs" + "sorted (xs @ a # ys @ b # zs @ c # us @ d # vs) \<Longrightarrow> x < d \<Longrightarrow> + del_list x (xs @ a # ys @ b # zs @ c # us @ d # vs) = + del_list x (xs @ a # ys @ b # zs @ c # us) @ d # vs" by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4) lemmas del_list_simps = sorted_lems

--- a/src/HOL/Data_Structures/RBT.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Data_Structures/RBT.thy Tue Nov 03 11:20:21 2015 +0100 @@ -27,23 +27,23 @@ "red (Node _ l a r) = R l a r" fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where -"balL (R t1 x t2) s t3 = R (B t1 x t2) s t3" | +"balL (R t1 x t2) y t3 = R (B t1 x t2) y t3" | "balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" | "balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (red t3))" | "balL t1 x t2 = R t1 x t2" fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where "balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" | -"balR (B t1 x t2) y bl = bal (R t1 x t2) y bl" | -"balR (R t1 x (B t2 y t3)) z bl = R (bal (red t1) x t2) y (B t3 z bl)" | +"balR (B t1 x t2) y t3 = bal (R t1 x t2) y t3" | +"balR (R t1 x (B t2 y t3)) z t4 = R (bal (red t1) x t2) y (B t3 z t4)" | "balR t1 x t2 = R t1 x t2" fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where "combine Leaf t = t" | "combine t Leaf = t" | -"combine (R a x b) (R c y d) = (case combine b c of - R b2 z c2 \<Rightarrow> (R (R a x b2) z (R c2 y d)) | - bc \<Rightarrow> R a x (R bc y d))" | +"combine (R t1 a t2) (R t3 c t4) = (case combine t2 t3 of + R u2 b u3 \<Rightarrow> (R (R t1 a u2) b (R u3 c t4)) | + t23 \<Rightarrow> R t1 a (R t23 c t4))" | "combine (B t1 a t2) (B t3 c t4) = (case combine t2 t3 of R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) | t23 \<Rightarrow> balL t1 a (B t23 c t4))" |

--- a/src/HOL/Data_Structures/Set_by_Ordered.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Data_Structures/Set_by_Ordered.thy Tue Nov 03 11:20:21 2015 +0100 @@ -13,13 +13,13 @@ fixes isin :: "'s \<Rightarrow> 'a \<Rightarrow> bool" fixes set :: "'s \<Rightarrow> 'a set" fixes invar :: "'s \<Rightarrow> bool" -assumes "set empty = {}" -assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)" -assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)" -assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}" -assumes "invar empty" -assumes "invar s \<Longrightarrow> invar(insert a s)" -assumes "invar s \<Longrightarrow> invar(delete a s)" +assumes set_empty: "set empty = {}" +assumes set_isin: "invar s \<Longrightarrow> isin s x = (x \<in> set s)" +assumes set_insert: "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)" +assumes set_delete: "invar s \<Longrightarrow> set(delete x s) = set s - {x}" +assumes invar_empty: "invar empty" +assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)" +assumes invar_delete: "invar s \<Longrightarrow> invar(delete x s)" locale Set_by_Ordered = fixes empty :: "'t" @@ -30,14 +30,14 @@ fixes wf :: "'t \<Rightarrow> bool" assumes empty: "inorder empty = []" assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow> - isin t a = (a \<in> elems (inorder t))" + isin t x = (x \<in> elems (inorder t))" assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> - inorder(insert a t) = ins_list a (inorder t)" + inorder(insert x t) = ins_list x (inorder t)" assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> - inorder(delete a t) = del_list a (inorder t)" + inorder(delete x t) = del_list x (inorder t)" assumes wf_empty: "wf empty" -assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)" -assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)" +assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert x t)" +assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete x t)" begin sublocale Set @@ -49,8 +49,8 @@ next case 3 thus ?case by(simp add: insert) next - case (4 s a) show ?case - using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted) + case (4 s x) show ?case + using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted) next case 5 thus ?case by(simp add: empty wf_empty) next

--- a/src/HOL/Data_Structures/Tree23_Map.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Data_Structures/Tree23_Map.thy Tue Nov 03 11:20:21 2015 +0100 @@ -21,53 +21,53 @@ else lookup r x)" fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where -"upd a b Leaf = Up\<^sub>i Leaf (a,b) Leaf" | -"upd a b (Node2 l xy r) = - (if a < fst xy then - (case upd a b l of - T\<^sub>i l' => T\<^sub>i (Node2 l' xy r) - | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 xy r)) - else if a = fst xy then T\<^sub>i (Node2 l (a,b) r) +"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" | +"upd x y (Node2 l ab r) = + (if x < fst ab then + (case upd x y l of + T\<^sub>i l' => T\<^sub>i (Node2 l' ab r) + | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) + else if x = fst ab then T\<^sub>i (Node2 l (x,y) r) else - (case upd a b r of - T\<^sub>i r' => T\<^sub>i (Node2 l xy r') - | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l xy r1 q r2)))" | -"upd a b (Node3 l xy1 m xy2 r) = - (if a < fst xy1 then - (case upd a b l of - T\<^sub>i l' => T\<^sub>i (Node3 l' xy1 m xy2 r) - | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) xy1 (Node2 m xy2 r)) - else if a = fst xy1 then T\<^sub>i (Node3 l (a,b) m xy2 r) - else if a < fst xy2 then - (case upd a b m of - T\<^sub>i m' => T\<^sub>i (Node3 l xy1 m' xy2 r) - | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l xy1 m1) q (Node2 m2 xy2 r)) - else if a = fst xy2 then T\<^sub>i (Node3 l xy1 m (a,b) r) + (case upd x y r of + T\<^sub>i r' => T\<^sub>i (Node2 l ab r') + | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" | +"upd x y (Node3 l ab1 m ab2 r) = + (if x < fst ab1 then + (case upd x y l of + T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r) + | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) + else if x = fst ab1 then T\<^sub>i (Node3 l (x,y) m ab2 r) + else if x < fst ab2 then + (case upd x y m of + T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r) + | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) + else if x = fst ab2 then T\<^sub>i (Node3 l ab1 m (x,y) r) else - (case upd a b r of - T\<^sub>i r' => T\<^sub>i (Node3 l xy1 m xy2 r') - | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l xy1 m) xy2 (Node2 r1 q r2)))" + (case upd x y r of + T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r') + | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2)))" definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where "update a b t = tree\<^sub>i(upd a b t)" fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where -"del k Leaf = T\<^sub>d Leaf" | -"del k (Node2 Leaf p Leaf) = (if k=fst p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" | -"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=fst p then Node2 Leaf q Leaf - else if k=fst q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" | -"del k (Node2 l a r) = (if k<fst a then node21 (del k l) a r else - if k > fst a then node22 l a (del k r) else - let (a',t) = del_min r in node22 l a' t)" | -"del k (Node3 l a m b r) = (if k<fst a then node31 (del k l) a m b r else - if k = fst a then let (a',m') = del_min m in node32 l a' m' b r else - if k < fst b then node32 l a (del k m) b r else - if k = fst b then let (b',r') = del_min r in node33 l a m b' r' - else node33 l a m b (del k r))" +"del x Leaf = T\<^sub>d Leaf" | +"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" | +"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf + else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" | +"del x (Node2 l ab1 r) = (if x<fst ab1 then node21 (del x l) ab1 r else + if x > fst ab1 then node22 l ab1 (del x r) else + let (ab1',t) = del_min r in node22 l ab1' t)" | +"del x (Node3 l ab1 m ab2 r) = (if x<fst ab1 then node31 (del x l) ab1 m ab2 r else + if x = fst ab1 then let (ab1',m') = del_min m in node32 l ab1' m' ab2 r else + if x < fst ab2 then node32 l ab1 (del x m) ab2 r else + if x = fst ab2 then let (ab2',r') = del_min r in node33 l ab1 m ab2' r' + else node33 l ab1 m ab2 (del x r))" definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where -"delete k t = tree\<^sub>d(del k t)" +"delete x t = tree\<^sub>d(del x t)" subsection \<open>Functional Correctness\<close>

--- a/src/HOL/Data_Structures/Tree23_Set.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Data_Structures/Tree23_Set.thy Tue Nov 03 11:20:21 2015 +0100 @@ -12,7 +12,7 @@ "isin Leaf x = False" | "isin (Node2 l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)" | "isin (Node3 l a m b r) x = - (x < a \<and> isin l x \<or> x = a \<or> (x < b \<and> isin m x \<or> x = b \<or> isin r x))" + (x < a \<and> isin l x \<or> x > b \<and> isin r x \<or> x = a \<or> x = b \<or> isin m x)" datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23" @@ -21,37 +21,38 @@ "tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r" fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where -"ins a Leaf = Up\<^sub>i Leaf a Leaf" | -"ins a (Node2 l x r) = - (if a < x then - case ins a l of - T\<^sub>i l' => T\<^sub>i (Node2 l' x r) - | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 x r) - else if a=x then T\<^sub>i (Node2 l x r) +"ins x Leaf = Up\<^sub>i Leaf x Leaf" | +"ins x (Node2 l a r) = + (if x < a then + case ins x l of + T\<^sub>i l' => T\<^sub>i (Node2 l' a r) + | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r) + else if x=a then T\<^sub>i (Node2 l x r) else - case ins a r of - T\<^sub>i r' => T\<^sub>i (Node2 l x r') - | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l x r1 q r2))" | -"ins a (Node3 l x1 m x2 r) = - (if a < x1 then - case ins a l of - T\<^sub>i l' => T\<^sub>i (Node3 l' x1 m x2 r) - | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) x1 (Node2 m x2 r) - else if a=x1 then T\<^sub>i (Node3 l x1 m x2 r) - else if a < x2 then - case ins a m of - T\<^sub>i m' => T\<^sub>i (Node3 l x1 m' x2 r) - | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l x1 m1) q (Node2 m2 x2 r) - else if a=x2 then T\<^sub>i (Node3 l x1 m x2 r) - else - case ins a r of - T\<^sub>i r' => T\<^sub>i (Node3 l x1 m x2 r') - | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l x1 m) x2 (Node2 r1 q r2))" + case ins x r of + T\<^sub>i r' => T\<^sub>i (Node2 l a r') + | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2))" | +"ins x (Node3 l a m b r) = + (if x < a then + case ins x l of + T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) + | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r) + else + if x > b then + case ins x r of + T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') + | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2) + else + if x=a \<or> x = b then T\<^sub>i (Node3 l a m b r) + else + case ins x m of + T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) + | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))" hide_const insert definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where -"insert a t = tree\<^sub>i(ins a t)" +"insert x t = tree\<^sub>i(ins x t)" datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23" @@ -94,21 +95,21 @@ fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where -"del k Leaf = T\<^sub>d Leaf" | -"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" | -"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf - else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" | -"del k (Node2 l a r) = (if k<a then node21 (del k l) a r else - if k > a then node22 l a (del k r) else +"del x Leaf = T\<^sub>d Leaf" | +"del x (Node2 Leaf a Leaf) = (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" | +"del x (Node3 Leaf a Leaf b Leaf) = T\<^sub>d(if x = a then Node2 Leaf b Leaf + else if x = b then Node2 Leaf a Leaf else Node3 Leaf a Leaf b Leaf)" | +"del x (Node2 l a r) = (if x<a then node21 (del x l) a r else + if x > a then node22 l a (del x r) else let (a',t) = del_min r in node22 l a' t)" | -"del k (Node3 l a m b r) = (if k<a then node31 (del k l) a m b r else - if k = a then let (a',m') = del_min m in node32 l a' m' b r else - if k < b then node32 l a (del k m) b r else - if k = b then let (b',r') = del_min r in node33 l a m b' r' - else node33 l a m b (del k r))" +"del x (Node3 l a m b r) = (if x<a then node31 (del x l) a m b r else + if x = a then let (a',m') = del_min m in node32 l a' m' b r else + if x < b then node32 l a (del x m) b r else + if x = b then let (b',r') = del_min r in node33 l a m b' r' + else node33 l a m b (del x r))" definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where -"delete k t = tree\<^sub>d(del k t)" +"delete x t = tree\<^sub>d(del x t)" subsection "Functional Correctness" @@ -127,7 +128,7 @@ lemma inorder_ins: "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)" -by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits) +by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits) (* 38 secs in 2015 *) lemma inorder_insert: "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)" @@ -194,7 +195,7 @@ end lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t" -by (induct t) (auto split: up\<^sub>i.split) (* 25 secs in 2015 *) +by (induct t) (auto split: up\<^sub>i.split) (* 87 secs in 2015 *) text{* Now an alternative proof (by Brian Huffman) that runs faster because two properties (balance and height) are combined in one predicate. *}

--- a/src/HOL/Data_Structures/Tree_Map.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Data_Structures/Tree_Map.thy Tue Nov 03 11:20:21 2015 +0100 @@ -14,16 +14,16 @@ if x > a then lookup r x else Some b)" fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where -"update a b Leaf = Node Leaf (a,b) Leaf" | -"update a b (Node l (x,y) r) = - (if a < x then Node (update a b l) (x,y) r - else if a=x then Node l (a,b) r - else Node l (x,y) (update a b r))" +"update x y Leaf = Node Leaf (x,y) Leaf" | +"update x y (Node l (a,b) r) = + (if x < a then Node (update x y l) (a,b) r + else if x = a then Node l (x,y) r + else Node l (a,b) (update x y r))" fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where -"delete k Leaf = Leaf" | -"delete k (Node l (a,b) r) = (if k<a then Node (delete k l) (a,b) r else - if k > a then Node l (a,b) (delete k r) else +"delete x Leaf = Leaf" | +"delete x (Node l (a,b) r) = (if x < a then Node (delete x l) (a,b) r else + if x > a then Node l (a,b) (delete x r) else if r = Leaf then l else let (ab',r') = del_min r in Node l ab' r')"

--- a/src/HOL/Data_Structures/Tree_Set.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Data_Structures/Tree_Set.thy Tue Nov 03 11:20:21 2015 +0100 @@ -15,20 +15,20 @@ hide_const (open) insert fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where -"insert a Leaf = Node Leaf a Leaf" | -"insert a (Node l x r) = - (if a < x then Node (insert a l) x r - else if a=x then Node l x r - else Node l x (insert a r))" +"insert x Leaf = Node Leaf x Leaf" | +"insert x (Node l a r) = + (if x < a then Node (insert x l) a r else + if x = a then Node l a r + else Node l a (insert x r))" fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where "del_min (Node Leaf a r) = (a, r)" | "del_min (Node l a r) = (let (x,l') = del_min l in (x, Node l' a r))" fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where -"delete k Leaf = Leaf" | -"delete k (Node l a r) = (if k<a then Node (delete k l) a r else - if k > a then Node l a (delete k r) else +"delete x Leaf = Leaf" | +"delete x (Node l a r) = (if x < a then Node (delete x l) a r else + if x > a then Node l a (delete x r) else if r = Leaf then l else let (a',r') = del_min r in Node l a' r')"

--- a/src/HOL/Hahn_Banach/Function_Norm.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy Tue Nov 03 11:20:21 2015 +0100 @@ -11,14 +11,13 @@ subsection \<open>Continuous linear forms\<close> text \<open> - A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"} - is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e. + A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, + iff it is bounded, i.e. \begin{center} - @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} + \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> \end{center} - In our application no other functions than linear forms are - considered, so we can define continuous linear forms as bounded - linear forms: + In our application no other functions than linear forms are considered, so + we can define continuous linear forms as bounded linear forms: \<close> locale continuous = linearform + @@ -42,34 +41,31 @@ subsection \<open>The norm of a linear form\<close> text \<open> - The least real number @{text c} for which holds + The least real number \<open>c\<close> for which holds \begin{center} - @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} + \<open>\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> \end{center} - is called the \<^emph>\<open>norm\<close> of @{text f}. + is called the \<^emph>\<open>norm\<close> of \<open>f\<close>. - For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be - defined as + For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as \begin{center} - @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"} + \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> \end{center} - For the case @{text "V = {0}"} the supremum would be taken from an - empty set. Since @{text \<real>} is unbounded, there would be no supremum. - To avoid this situation it must be guaranteed that there is an - element in this set. This element must be @{text "{} \<ge> 0"} so that - @{text fn_norm} has the norm properties. Furthermore it does not - have to change the norm in all other cases, so it must be @{text 0}, - as all other elements are @{text "{} \<ge> 0"}. + For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. + Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this + situation it must be guaranteed that there is an element in this set. This + element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. + Furthermore it does not have to change the norm in all other cases, so it + must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>. - Thus we define the set @{text B} where the supremum is taken from as - follows: + Thus we define the set \<open>B\<close> where the supremum is taken from as follows: \begin{center} - @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"} + \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close> \end{center} - @{text fn_norm} is equal to the supremum of @{text B}, if the - supremum exists (otherwise it is undefined). + \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists + (otherwise it is undefined). \<close> locale fn_norm = @@ -84,8 +80,8 @@ by (simp add: B_def) text \<open> - The following lemma states that every continuous linear form on a - normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm. + The following lemma states that every continuous linear form on a normed + space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm. \<close> lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: @@ -98,19 +94,19 @@ non-empty bounded set of reals has a supremum.\<close> have "\<exists>a. lub (B V f) a" proof (rule real_complete) - txt \<open>First we have to show that @{text B} is non-empty:\<close> + txt \<open>First we have to show that \<open>B\<close> is non-empty:\<close> have "0 \<in> B V f" .. then show "\<exists>x. x \<in> B V f" .. - txt \<open>Then we have to show that @{text B} is bounded:\<close> + txt \<open>Then we have to show that \<open>B\<close> is bounded:\<close> show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" proof - - txt \<open>We know that @{text f} is bounded by some value @{text c}.\<close> + txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close> from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. - txt \<open>To prove the thesis, we have to show that there is some - @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in> - B"}. Due to the definition of @{text B} there are two cases.\<close> + txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such + that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are + two cases.\<close> def b \<equiv> "max c 0" have "\<forall>y \<in> B V f. y \<le> b" @@ -121,8 +117,8 @@ assume "y = 0" then show ?thesis unfolding b_def by arith next - txt \<open>The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some - @{text "x \<in> V"} with @{text "x \<noteq> 0"}.\<close> + txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some + \<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<close> assume "y \<noteq> 0" with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" and x: "x \<in> V" and neq: "x \<noteq> 0" @@ -130,7 +126,7 @@ from x neq have gt: "0 < \<parallel>x\<parallel>" .. txt \<open>The thesis follows by a short calculation using the - fact that @{text f} is bounded.\<close> + fact that \<open>f\<close> is bounded.\<close> note y_rep also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" @@ -177,16 +173,16 @@ from this and b show ?thesis .. qed -text \<open>The norm of a continuous function is always @{text "\<ge> 0"}.\<close> +text \<open>The norm of a continuous function is always \<open>\<ge> 0\<close>.\<close> lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]: assumes "continuous V f norm" shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V" proof - interpret continuous V f norm by fact - txt \<open>The function norm is defined as the supremum of @{text B}. - So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> - 0"}, provided the supremum exists and @{text B} is not empty.\<close> + txt \<open>The function norm is defined as the supremum of \<open>B\<close>. + So it is \<open>\<ge> 0\<close> if all elements in \<open>B\<close> are \<open>\<ge> + 0\<close>, provided the supremum exists and \<open>B\<close> is not empty.\<close> have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" using \<open>continuous V f norm\<close> by (rule fn_norm_works) moreover have "0 \<in> B V f" .. @@ -197,7 +193,7 @@ \<^medskip> The fundamental property of function norms is: \begin{center} - @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} + \<open>\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close> \end{center} \<close> @@ -237,10 +233,10 @@ text \<open> \<^medskip> - The function norm is the least positive real number for - which the following inequation holds: + The function norm is the least positive real number for which the + following inequality holds: \begin{center} - @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} + \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> \end{center} \<close>

--- a/src/HOL/Hahn_Banach/Function_Order.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Function_Order.thy Tue Nov 03 11:20:21 2015 +0100 @@ -11,10 +11,10 @@ subsection \<open>The graph of a function\<close> text \<open> - We define the \<^emph>\<open>graph\<close> of a (real) function @{text f} with - domain @{text F} as the set + We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with + domain \<open>F\<close> as the set \begin{center} - @{text "{(x, f x). x \<in> F}"} + \<open>{(x, f x). x \<in> F}\<close> \end{center} So we are modeling partial functions by specifying the domain and the mapping function. We use the term ``function'' also for its @@ -41,8 +41,8 @@ subsection \<open>Functions ordered by domain extension\<close> text \<open> - A function @{text h'} is an extension of @{text h}, iff the graph of - @{text h} is a subset of the graph of @{text h'}. + A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of + \<open>h\<close> is a subset of the graph of \<open>h'\<close>. \<close> lemma graph_extI: @@ -60,8 +60,7 @@ subsection \<open>Domain and function of a graph\<close> text \<open> - The inverse functions to @{text graph} are @{text domain} and @{text - funct}. + The inverse functions to \<open>graph\<close> are \<open>domain\<close> and \<open>funct\<close>. \<close> definition domain :: "'a graph \<Rightarrow> 'a set" @@ -71,8 +70,8 @@ where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))" text \<open> - The following lemma states that @{text g} is the graph of a function - if the relation induced by @{text g} is unique. + The following lemma states that \<open>g\<close> is the graph of a function if the + relation induced by \<open>g\<close> is unique. \<close> lemma graph_domain_funct: @@ -94,10 +93,9 @@ subsection \<open>Norm-preserving extensions of a function\<close> text \<open> - Given a linear form @{text f} on the space @{text F} and a seminorm - @{text p} on @{text E}. The set of all linear extensions of @{text - f}, to superspaces @{text H} of @{text F}, which are bounded by - @{text p}, is defined as follows. + Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The + set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are + bounded by \<open>p\<close>, is defined as follows. \<close> definition

--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Tue Nov 03 11:20:21 2015 +0100 @@ -9,42 +9,39 @@ begin text \<open> - We present the proof of two different versions of the Hahn-Banach - Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}. + We present the proof of two different versions of the Hahn-Banach Theorem, + closely following @{cite \<open>\S36\<close> "Heuser:1986"}. \<close> + subsection \<open>The Hahn-Banach Theorem for vector spaces\<close> paragraph \<open>Hahn-Banach Theorem.\<close> text \<open> - Let @{text F} be a subspace of a real vector space @{text E}, let @{text - p} be a semi-norm on @{text E}, and @{text f} be a linear form defined on - @{text F} such that @{text f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in> - F. f x \<le> p x"}. Then @{text f} can be extended to a linear form @{text h} - on @{text E} such that @{text h} is norm-preserving, i.e. @{text h} is - also bounded by @{text p}. + Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm + on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded + by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear + form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded + by \<open>p\<close>. \<close> paragraph \<open>Proof Sketch.\<close> text \<open> - \<^enum> Define @{text M} as the set of norm-preserving extensions of - @{text f} to subspaces of @{text E}. The linear forms in @{text M} - are ordered by domain extension. + \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces + of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension. - \<^enum> We show that every non-empty chain in @{text M} has an upper - bound in @{text M}. + \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>. + + \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in + \<open>M\<close>. - \<^enum> With Zorn's Lemma we conclude that there is a maximal function - @{text g} in @{text M}. - - \<^enum> The domain @{text H} of @{text g} is the whole space @{text - E}, as shown by classical contradiction: + \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical + contradiction: - \<^item> Assuming @{text g} is not defined on whole @{text E}, it can - still be extended in a norm-preserving way to a super-space @{text - H'} of @{text H}. + \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in + a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>. - \<^item> Thus @{text g} can not be maximal. Contradiction! + \<^item> Thus \<open>g\<close> can not be maximal. Contradiction! \<close> theorem Hahn_Banach: @@ -52,9 +49,9 @@ and "seminorm E p" and "linearform F f" assumes fp: "\<forall>x \<in> F. f x \<le> p x" shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)" - -- \<open>Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E},\<close> - -- \<open>and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p},\<close> - -- \<open>then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \<^smallskip>\<close> + -- \<open>Let \<open>E\<close> be a vector space, \<open>F\<close> a subspace of \<open>E\<close>, \<open>p\<close> a seminorm on \<open>E\<close>,\<close> + -- \<open>and \<open>f\<close> a linear form on \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>,\<close> + -- \<open>then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> in a norm-preserving way. \<^smallskip>\<close> proof - interpret vectorspace E by fact interpret subspace F E by fact @@ -67,8 +64,8 @@ { fix c assume cM: "c \<in> chains M" and ex: "\<exists>x. x \<in> c" have "\<Union>c \<in> M" - -- \<open>Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}:\<close> - -- \<open>@{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}.\<close> + -- \<open>Show that every non-empty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close> + -- \<open>\<open>\<Union>c\<close> is greater than any element of the chain \<open>c\<close>, so it suffices to show \<open>\<Union>c \<in> M\<close>.\<close> unfolding M_def proof (rule norm_pres_extensionI) let ?H = "domain (\<Union>c)" @@ -98,9 +95,9 @@ qed } then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g" - -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \<^smallskip>\<close> + -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in \<open>M\<close>. \<^smallskip>\<close> proof (rule Zorn's_Lemma) - -- \<open>We show that @{text M} is non-empty:\<close> + -- \<open>We show that \<open>M\<close> is non-empty:\<close> show "graph F f \<in> M" unfolding M_def proof (rule norm_pres_extensionI2) @@ -119,18 +116,18 @@ and HE: "H \<unlhd> E" and FH: "F \<unlhd> H" and graphs: "graph F f \<subseteq> graph H h" and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def .. - -- \<open>@{text g} is a norm-preserving extension of @{text f}, in other words:\<close> - -- \<open>@{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E},\<close> - -- \<open>and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \<^smallskip>\<close> + -- \<open>\<open>g\<close> is a norm-preserving extension of \<open>f\<close>, in other words:\<close> + -- \<open>\<open>g\<close> is the graph of some linear form \<open>h\<close> defined on a subspace \<open>H\<close> of \<open>E\<close>,\<close> + -- \<open>and \<open>h\<close> is an extension of \<open>f\<close> that is again bounded by \<open>p\<close>. \<^smallskip>\<close> from HE E have H: "vectorspace H" by (rule subspace.vectorspace) have HE_eq: "H = E" - -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \<^smallskip>\<close> + -- \<open>We show that \<open>h\<close> is defined on whole \<open>E\<close> by classical contradiction. \<^smallskip>\<close> proof (rule classical) assume neq: "H \<noteq> E" - -- \<open>Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended\<close> - -- \<open>in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \<^smallskip>\<close> + -- \<open>Assume \<open>h\<close> is not defined on whole \<open>E\<close>. Then show that \<open>h\<close> can be extended\<close> + -- \<open>in a norm-preserving way to a function \<open>h'\<close> with the graph \<open>g'\<close>. \<^smallskip>\<close> have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'" proof - from HE have "H \<subseteq> E" .. @@ -146,7 +143,7 @@ qed def H' \<equiv> "H + lin x'" - -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \<^smallskip>\<close> + -- \<open>Define \<open>H'\<close> as the direct sum of \<open>H\<close> and the linear closure of \<open>x'\<close>. \<^smallskip>\<close> have HH': "H \<unlhd> H'" proof (unfold H'_def) from x'E have "vectorspace (lin x')" .. @@ -156,8 +153,8 @@ obtain xi where xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y" - -- \<open>Pick a real number @{text \<xi>} that fulfills certain inequations; this will\<close> - -- \<open>be used to establish that @{text h'} is a norm-preserving extension of @{text h}. + -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close> + -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>. \label{ex-xi-use}\<^smallskip>\<close> proof - from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi @@ -185,10 +182,10 @@ def h' \<equiv> "\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi" - -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \<^smallskip>\<close> + -- \<open>Define the extension \<open>h'\<close> of \<open>h\<close> to \<open>H'\<close> using \<open>\<xi>\<close>. \<^smallskip>\<close> have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'" - -- \<open>@{text h'} is an extension of @{text h} \dots \<^smallskip>\<close> + -- \<open>\<open>h'\<close> is an extension of \<open>h\<close> \dots \<^smallskip>\<close> proof show "g \<subseteq> graph H' h'" proof - @@ -225,7 +222,7 @@ qed qed moreover have "graph H' h' \<in> M" - -- \<open>and @{text h'} is norm-preserving. \<^smallskip>\<close> + -- \<open>and \<open>h'\<close> is norm-preserving. \<^smallskip>\<close> proof (unfold M_def) show "graph H' h' \<in> norm_pres_extensions E p F f" proof (rule norm_pres_extensionI2) @@ -273,7 +270,7 @@ ultimately show ?thesis .. qed then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp - -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \<^smallskip>\<close> + -- \<open>So the graph \<open>g\<close> of \<open>h\<close> cannot be maximal. Contradiction! \<^smallskip>\<close> with gx show "H = E" by contradiction qed @@ -295,14 +292,14 @@ text \<open> The following alternative formulation of the Hahn-Banach - Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear - form @{text f} and a seminorm @{text p} the following inequations - are equivalent:\footnote{This was shown in lemma @{thm [source] - abs_ineq_iff} (see page \pageref{abs-ineq-iff}).} + Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form + \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are + equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff} + (see page \pageref{abs-ineq-iff}).} \begin{center} \begin{tabular}{lll} - @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and & - @{text "\<forall>x \<in> H. h x \<le> p x"} \\ + \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & + \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\ \end{tabular} \end{center} \<close> @@ -339,9 +336,9 @@ subsection \<open>The Hahn-Banach Theorem for normed spaces\<close> text \<open> - Every continuous linear form @{text f} on a subspace @{text F} of a - norm space @{text E}, can be extended to a continuous linear form - @{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}. + Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, + can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = + \<parallel>g\<parallel>\<close>. \<close> theorem norm_Hahn_Banach: @@ -370,22 +367,22 @@ by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero [OF normed_vectorspace_with_fn_norm.intro, OF F_norm \<open>continuous F f norm\<close> , folded B_def fn_norm_def]) - txt \<open>We define a function @{text p} on @{text E} as follows: - @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}\<close> + txt \<open>We define a function \<open>p\<close> on \<open>E\<close> as follows: + \<open>p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>\<close> def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>" - txt \<open>@{text p} is a seminorm on @{text E}:\<close> + txt \<open>\<open>p\<close> is a seminorm on \<open>E\<close>:\<close> have q: "seminorm E p" proof fix x y a assume x: "x \<in> E" and y: "y \<in> E" - txt \<open>@{text p} is positive definite:\<close> + txt \<open>\<open>p\<close> is positive definite:\<close> have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) moreover from x have "0 \<le> \<parallel>x\<parallel>" .. ultimately show "0 \<le> p x" by (simp add: p_def zero_le_mult_iff) - txt \<open>@{text p} is absolutely homogeneous:\<close> + txt \<open>\<open>p\<close> is absolutely homogeneous:\<close> show "p (a \<cdot> x) = \<bar>a\<bar> * p x" proof - @@ -396,7 +393,7 @@ finally show ?thesis . qed - txt \<open>Furthermore, @{text p} is subadditive:\<close> + txt \<open>Furthermore, \<open>p\<close> is subadditive:\<close> show "p (x + y) \<le> p x + p y" proof - @@ -411,7 +408,7 @@ qed qed - txt \<open>@{text f} is bounded by @{text p}.\<close> + txt \<open>\<open>f\<close> is bounded by \<open>p\<close>.\<close> have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x" proof @@ -423,10 +420,10 @@ OF F_norm, folded B_def fn_norm_def]) qed - txt \<open>Using the fact that @{text p} is a seminorm and @{text f} is bounded - by @{text p} we can apply the Hahn-Banach Theorem for real vector - spaces. So @{text f} can be extended in a norm-preserving way to - some function @{text g} on the whole vector space @{text E}.\<close> + txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we + can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be + extended in a norm-preserving way to some function \<open>g\<close> on the whole + vector space \<open>E\<close>.\<close> with E FE linearform q obtain g where linearformE: "linearform E g" @@ -434,7 +431,7 @@ and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x" by (rule abs_Hahn_Banach [elim_format]) iprover - txt \<open>We furthermore have to show that @{text g} is also continuous:\<close> + txt \<open>We furthermore have to show that \<open>g\<close> is also continuous:\<close> have g_cont: "continuous E g norm" using linearformE proof @@ -443,25 +440,25 @@ by (simp only: p_def) qed - txt \<open>To complete the proof, we show that @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}.\<close> + txt \<open>To complete the proof, we show that \<open>\<parallel>g\<parallel> = \<parallel>f\<parallel>\<close>.\<close> have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F" proof (rule order_antisym) txt \<open> - First we show @{text "\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>"}. The function norm @{text - "\<parallel>g\<parallel>"} is defined as the smallest @{text "c \<in> \<real>"} such that + First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the + smallest \<open>c \<in> \<real>\<close> such that \begin{center} \begin{tabular}{l} - @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} + \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> \end{tabular} \end{center} - \noindent Furthermore holds + \<^noindent> Furthermore holds \begin{center} \begin{tabular}{l} - @{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} + \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close> \end{tabular} \end{center} -\<close> + \<close> from g_cont _ ge_zero show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"

--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Tue Nov 03 11:20:21 2015 +0100 @@ -9,34 +9,30 @@ begin text \<open> - In this section the following context is presumed. Let @{text E} be - a real vector space with a seminorm @{text q} on @{text E}. @{text - F} is a subspace of @{text E} and @{text f} a linear function on - @{text F}. We consider a subspace @{text H} of @{text E} that is a - superspace of @{text F} and a linear form @{text h} on @{text - H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is - an element in @{text "E - H"}. @{text H} is extended to the direct - sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"} - the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is - unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y + - a \<cdot> \<xi>"} for a certain @{text \<xi>}. + In this section the following context is presumed. Let \<open>E\<close> be a real + vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> + a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a + superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> + and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' + = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> + with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> + for a certain \<open>\<xi>\<close>. - Subsequently we show some properties of this extension @{text h'} of - @{text h}. + Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. \<^medskip> - This lemma will be used to show the existence of a linear - extension of @{text f} (see page \pageref{ex-xi-use}). It is a - consequence of the completeness of @{text \<real>}. To show + This lemma will be used to show the existence of a linear extension of \<open>f\<close> + (see page \pageref{ex-xi-use}). It is a consequence of the completeness of + \<open>\<real>\<close>. To show \begin{center} \begin{tabular}{l} - @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"} + \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close> \end{tabular} \end{center} - \noindent it suffices to show that + \<^noindent> it suffices to show that \begin{center} \begin{tabular}{l} - @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"} + \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close> \end{tabular} \end{center} \<close> @@ -48,7 +44,7 @@ proof - interpret vectorspace F by fact txt \<open>From the completeness of the reals follows: - The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is + The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is non-empty and has an upper bound.\<close> let ?S = "{a u | u. u \<in> F}" @@ -86,9 +82,8 @@ text \<open> \<^medskip> - The function @{text h'} is defined as a @{text "h' x = h y - + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of - @{text h} to @{text H'}. + The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where + \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>. \<close> lemma h'_lf: @@ -194,8 +189,8 @@ text \<open> \<^medskip> - The linear extension @{text h'} of @{text h} - is bounded by the seminorm @{text p}.\<close> + The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>. +\<close> lemma h'_norm_pres: assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) = @@ -235,8 +230,8 @@ also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp finally show ?thesis . next - txt \<open>In the case @{text "a < 0"}, we use @{text "a\<^sub>1"} - with @{text ya} taken as @{text "y / a"}:\<close> + txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close> + with \<open>ya\<close> taken as \<open>y / a\<close>:\<close> assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp from a1 ay have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" .. @@ -257,8 +252,8 @@ finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . then show ?thesis by simp next - txt \<open>In the case @{text "a > 0"}, we use @{text "a\<^sub>2"} - with @{text ya} taken as @{text "y / a"}:\<close> + txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close> + with \<open>ya\<close> taken as \<open>y / a\<close>:\<close> assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp from a2 ay have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..

--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Tue Nov 03 11:20:21 2015 +0100 @@ -2,27 +2,25 @@ Author: Gertrud Bauer, TU Munich *) -section \<open>The supremum w.r.t.~the function order\<close> +section \<open>The supremum wrt.\ the function order\<close> theory Hahn_Banach_Sup_Lemmas imports Function_Norm Zorn_Lemma begin text \<open> - This section contains some lemmas that will be used in the proof of - the Hahn-Banach Theorem. In this section the following context is - presumed. Let @{text E} be a real vector space with a seminorm - @{text p} on @{text E}. @{text F} is a subspace of @{text E} and - @{text f} a linear form on @{text F}. We consider a chain @{text c} - of norm-preserving extensions of @{text f}, such that @{text "\<Union>c = - graph H h"}. We will show some properties about the limit function - @{text h}, i.e.\ the supremum of the chain @{text c}. + This section contains some lemmas that will be used in the proof of the + Hahn-Banach Theorem. In this section the following context is presumed. + Let \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a + subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of + norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will + show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of + the chain \<open>c\<close>. \<^medskip> - Let @{text c} be a chain of norm-preserving extensions of - the function @{text f} and let @{text "graph H h"} be the supremum - of @{text c}. Every element in @{text H} is member of one of the - elements of the chain. + Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and + let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of + one of the elements of the chain. \<close> lemmas [dest?] = chainsD @@ -57,11 +55,10 @@ text \<open> \<^medskip> - Let @{text c} be a chain of norm-preserving extensions of - the function @{text f} and let @{text "graph H h"} be the supremum - of @{text c}. Every element in the domain @{text H} of the supremum - function is member of the domain @{text H'} of some function @{text - h'}, such that @{text h} extends @{text h'}. + Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and + let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of + the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, + such that \<open>h\<close> extends \<open>h'\<close>. \<close> lemma some_H'h': @@ -86,10 +83,9 @@ text \<open> \<^medskip> - Any two elements @{text x} and @{text y} in the domain - @{text H} of the supremum function @{text h} are both in the domain - @{text H'} of some function @{text h'}, such that @{text h} extends - @{text h'}. + Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function + \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> + extends \<open>h'\<close>. \<close> lemma some_H'h'2: @@ -103,8 +99,8 @@ \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" proof - - txt \<open>@{text y} is in the domain @{text H''} of some function @{text h''}, - such that @{text h} extends @{text h''}.\<close> + txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, + such that \<open>h\<close> extends \<open>h''\<close>.\<close> from M cM u and y obtain H' h' where y_hy: "(y, h y) \<in> graph H' h'" @@ -114,8 +110,8 @@ "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" by (rule some_H'h't [elim_format]) blast - txt \<open>@{text x} is in the domain @{text H'} of some function @{text h'}, - such that @{text h} extends @{text h'}.\<close> + txt \<open>\<open>x\<close> is in the domain \<open>H'\<close> of some function \<open>h'\<close>, + such that \<open>h\<close> extends \<open>h'\<close>.\<close> from M cM u and x obtain H'' h'' where x_hx: "(x, h x) \<in> graph H'' h''" @@ -125,9 +121,9 @@ "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x" by (rule some_H'h't [elim_format]) blast - txt \<open>Since both @{text h'} and @{text h''} are elements of the chain, - @{text h''} is an extension of @{text h'} or vice versa. Thus both - @{text x} and @{text y} are contained in the greater + txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, + \<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both + \<open>x\<close> and \<open>y\<close> are contained in the greater one. \label{cases1}\<close> from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''" @@ -159,8 +155,8 @@ text \<open> \<^medskip> - The relation induced by the graph of the supremum of a - chain @{text c} is definite, i.~e.~t is the graph of a function. + The relation induced by the graph of the supremum of a chain \<open>c\<close> is + definite, i.e.\ it is the graph of a function. \<close> lemma sup_definite: @@ -182,9 +178,8 @@ then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" unfolding M_def by blast - txt \<open>@{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"} - or vice versa, since both @{text "G\<^sub>1"} and @{text - "G\<^sub>2"} are members of @{text c}. \label{cases2}\<close> + txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close> + are members of \<open>c\<close>. \label{cases2}\<close> from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1" by (blast dest: chainsD) @@ -210,12 +205,11 @@ text \<open> \<^medskip> - The limit function @{text h} is linear. Every element - @{text x} in the domain of @{text h} is in the domain of a function - @{text h'} in the chain of norm preserving extensions. Furthermore, - @{text h} is an extension of @{text h'} so the function values of - @{text x} are identical for @{text h'} and @{text h}. Finally, the - function @{text h'} is linear by construction of @{text M}. + The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> + is in the domain of a function \<open>h'\<close> in the chain of norm preserving + extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function + values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> + is linear by construction of \<open>M\<close>. \<close> lemma sup_lf: @@ -266,10 +260,9 @@ text \<open> \<^medskip> - The limit of a non-empty chain of norm preserving - extensions of @{text f} is an extension of @{text f}, since every - element of the chain is an extension of @{text f} and the supremum - is an extension for every element of the chain. + The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an + extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close> + and the supremum is an extension for every element of the chain. \<close> lemma sup_ext: @@ -293,10 +286,9 @@ text \<open> \<^medskip> - The domain @{text H} of the limit function is a superspace - of @{text F}, since @{text F} is a subset of @{text H}. The - existence of the @{text 0} element in @{text F} and the closure - properties follow from the fact that @{text F} is a vector space. + The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is + a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure + properties follow from the fact that \<open>F\<close> is a vector space. \<close> lemma sup_supF: @@ -319,8 +311,7 @@ text \<open> \<^medskip> - The domain @{text H} of the limit function is a subspace of - @{text E}. + The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>. \<close> lemma sup_subE: @@ -376,8 +367,8 @@ text \<open> \<^medskip> - The limit function is bounded by the norm @{text p} as - well, since all elements in the chain are bounded by @{text p}. + The limit function is bounded by the norm \<open>p\<close> as well, since all elements + in the chain are bounded by \<open>p\<close>. \<close> lemma sup_norm_pres: @@ -398,14 +389,14 @@ text \<open> \<^medskip> - The following lemma is a property of linear forms on real - vector spaces. It will be used for the lemma @{text abs_Hahn_Banach} - (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real - vector spaces the following inequations are equivalent: + The following lemma is a property of linear forms on real vector spaces. + It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page + \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces + the following inequality are equivalent: \begin{center} \begin{tabular}{lll} - @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and & - @{text "\<forall>x \<in> H. h x \<le> p x"} \\ + \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & + \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\ \end{tabular} \end{center} \<close>

--- a/src/HOL/Hahn_Banach/Linearform.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Linearform.thy Tue Nov 03 11:20:21 2015 +0100 @@ -9,8 +9,8 @@ begin text \<open> - A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals - that is additive and multiplicative. + A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is + additive and multiplicative. \<close> locale linearform = @@ -44,7 +44,7 @@ finally show ?thesis by simp qed -text \<open>Every linear form yields @{text 0} for the @{text 0} vector.\<close> +text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close> lemma (in linearform) zero [iff]: assumes "vectorspace V"

--- a/src/HOL/Hahn_Banach/Normed_Space.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy Tue Nov 03 11:20:21 2015 +0100 @@ -11,9 +11,9 @@ subsection \<open>Quasinorms\<close> text \<open> - A \<^emph>\<open>seminorm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space - into the reals that has the following properties: it is positive - definite, absolute homogeneous and subadditive. + A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals + that has the following properties: it is positive definite, absolute + homogeneous and subadditive. \<close> locale seminorm = @@ -57,8 +57,8 @@ subsection \<open>Norms\<close> text \<open> - A \<^emph>\<open>norm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the - @{text 0} vector to @{text 0}. + A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the + \<open>0\<close> vector to \<open>0\<close>. \<close> locale norm = seminorm +

--- a/src/HOL/Hahn_Banach/Subspace.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Subspace.thy Tue Nov 03 11:20:21 2015 +0100 @@ -11,9 +11,8 @@ subsection \<open>Definition\<close> text \<open> - A non-empty subset @{text U} of a vector space @{text V} is a - \<^emph>\<open>subspace\<close> of @{text V}, iff @{text U} is closed under addition - and scalar multiplication. + A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff + \<open>U\<close> is closed under addition and scalar multiplication. \<close> locale subspace = @@ -51,9 +50,9 @@ text \<open> \<^medskip> - Similar as for linear spaces, the existence of the zero - element in every subspace follows from the non-emptiness of the - carrier set and by vector space laws. + Similar as for linear spaces, the existence of the zero element in every + subspace follows from the non-emptiness of the carrier set and by vector + space laws. \<close> lemma (in subspace) zero [intro]: @@ -140,8 +139,8 @@ subsection \<open>Linear closure\<close> text \<open> - The \<^emph>\<open>linear closure\<close> of a vector @{text x} is the set of all - scalar multiples of @{text x}. + The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples + of \<open>x\<close>. \<close> definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set" @@ -227,8 +226,8 @@ subsection \<open>Sum of two vectorspaces\<close> text \<open> - The \<^emph>\<open>sum\<close> of two vectorspaces @{text U} and @{text V} is the - set of all sums of elements from @{text U} and @{text V}. + The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the set of all sums of + elements from \<open>U\<close> and \<open>V\<close>. \<close> lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}" @@ -246,7 +245,7 @@ "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V" unfolding sum_def by blast -text \<open>@{text U} is a subspace of @{text "U + V"}.\<close> +text \<open>\<open>U\<close> is a subspace of \<open>U + V\<close>.\<close> lemma subspace_sum1 [iff]: assumes "vectorspace U" "vectorspace V" @@ -329,11 +328,10 @@ subsection \<open>Direct sums\<close> text \<open> - The sum of @{text U} and @{text V} is called \<^emph>\<open>direct\<close>, iff the - zero element is the only common element of @{text U} and @{text - V}. For every element @{text x} of the direct sum of @{text U} and - @{text V} the decomposition in @{text "x = u + v"} with - @{text "u \<in> U"} and @{text "v \<in> V"} is unique. + The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the + only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct + sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and + \<open>v \<in> V\<close> is unique. \<close> lemma decomp: @@ -378,12 +376,10 @@ qed text \<open> - An application of the previous lemma will be used in the proof of - the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any - element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a - vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"} - the components @{text "y \<in> H"} and @{text a} are uniquely - determined. + An application of the previous lemma will be used in the proof of the + Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any element + \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a vectorspace \<open>H\<close> and the linear closure + of \<open>x\<^sub>0\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely determined. \<close> lemma decomp_H': @@ -437,10 +433,9 @@ qed text \<open> - Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a - vectorspace @{text H} and the linear closure of @{text x'} the - components @{text "y \<in> H"} and @{text a} are unique, it follows from - @{text "y \<in> H"} that @{text "a = 0"}. + Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close> + and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, + it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>. \<close> lemma decomp_H'_H: @@ -465,9 +460,8 @@ qed text \<open> - The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"} - are unique, so the function @{text h'} defined by - @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite. + The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> are unique, so the function + \<open>h'\<close> defined by \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite. \<close> lemma h'_definite:

--- a/src/HOL/Hahn_Banach/Vector_Space.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Tue Nov 03 11:20:21 2015 +0100 @@ -11,9 +11,9 @@ subsection \<open>Signature\<close> text \<open> - For the definition of real vector spaces a type @{typ 'a} of the - sort @{text "{plus, minus, zero}"} is considered, on which a real - scalar multiplication @{text \<cdot>} is declared. + For the definition of real vector spaces a type @{typ 'a} of the sort + \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication + \<open>\<cdot>\<close> is declared. \<close> consts @@ -23,14 +23,13 @@ subsection \<open>Vector space laws\<close> text \<open> - A \<^emph>\<open>vector space\<close> is a non-empty set @{text V} of elements from - @{typ 'a} with the following vector space laws: The set @{text V} is - closed under addition and scalar multiplication, addition is - associative and commutative; @{text "- x"} is the inverse of @{text - x} w.~r.~t.~addition and @{text 0} is the neutral element of - addition. Addition and multiplication are distributive; scalar - multiplication is associative and the real number @{text "1"} is - the neutral element of scalar multiplication. + A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with + the following vector space laws: The set \<open>V\<close> is closed under addition and + scalar multiplication, addition is associative and commutative; \<open>- x\<close> is + the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of + addition. Addition and multiplication are distributive; scalar + multiplication is associative and the real number \<open>1\<close> is the neutral + element of scalar multiplication. \<close> locale vectorspace = @@ -65,7 +64,8 @@ lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V" by (simp add: negate_eq1) -lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)" +lemma add_left_commute: + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)" proof - assume xyz: "x \<in> V" "y \<in> V" "z \<in> V" then have "x + (y + z) = (x + y) + z" @@ -78,8 +78,8 @@ lemmas add_ac = add_assoc add_commute add_left_commute -text \<open>The existence of the zero element of a vector space - follows from the non-emptiness of carrier set.\<close> +text \<open>The existence of the zero element of a vector space follows from the + non-emptiness of carrier set.\<close> lemma zero [iff]: "0 \<in> V" proof - @@ -214,7 +214,8 @@ then show "x + y = x + z" by (simp only:) qed -lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)" +lemma add_right_cancel: + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)" by (simp only: add_commute add_left_cancel) lemma add_assoc_cong: @@ -372,4 +373,3 @@ end end -

--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy Tue Nov 03 11:20:21 2015 +0100 @@ -10,13 +10,12 @@ text \<open> Zorn's Lemmas states: if every linear ordered subset of an ordered - set @{text S} has an upper bound in @{text S}, then there exists a - maximal element in @{text S}. In our application, @{text S} is a + set \<open>S\<close> has an upper bound in \<open>S\<close>, then there exists a + maximal element in \<open>S\<close>. In our application, \<open>S\<close> is a set of sets ordered by set inclusion. Since the union of a chain of sets is an upper bound for all elements of the chain, the conditions - of Zorn's lemma can be modified: if @{text S} is non-empty, it - suffices to show that for every non-empty chain @{text c} in @{text - S} the union of @{text c} also lies in @{text S}. + of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it + suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> also lies in \<open>S\<close>. \<close> theorem Zorn's_Lemma: @@ -30,14 +29,14 @@ show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" proof cases - txt \<open>If @{text c} is an empty chain, then every element in - @{text S} is an upper bound of @{text c}.\<close> + txt \<open>If \<open>c\<close> is an empty chain, then every element in + \<open>S\<close> is an upper bound of \<open>c\<close>.\<close> assume "c = {}" with aS show ?thesis by fast - txt \<open>If @{text c} is non-empty, then @{text "\<Union>c"} is an upper - bound of @{text c}, lying in @{text S}.\<close> + txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper + bound of \<open>c\<close>, lying in \<open>S\<close>.\<close> next assume "c \<noteq> {}"

--- a/src/HOL/Hahn_Banach/document/root.tex Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Hahn_Banach/document/root.tex Tue Nov 03 11:20:21 2015 +0100 @@ -16,7 +16,7 @@ \pagenumbering{arabic} \title{The Hahn-Banach Theorem \\ for Real Vector Spaces} -\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}} +\author{Gertrud Bauer} \maketitle \begin{abstract}

--- a/src/HOL/Isar_Examples/Basic_Logic.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Basic_Logic.thy Tue Nov 03 11:20:21 2015 +0100 @@ -13,10 +13,9 @@ subsection \<open>Pure backward reasoning\<close> -text \<open>In order to get a first idea of how Isabelle/Isar proof - documents may look like, we consider the propositions @{text I}, - @{text K}, and @{text S}. The following (rather explicit) proofs - should require little extra explanations.\<close> +text \<open>In order to get a first idea of how Isabelle/Isar proof documents may + look like, we consider the propositions \<open>I\<close>, \<open>K\<close>, and \<open>S\<close>. The following + (rather explicit) proofs should require little extra explanations.\<close> lemma I: "A \<longrightarrow> A" proof @@ -51,14 +50,12 @@ qed qed -text \<open>Isar provides several ways to fine-tune the reasoning, - avoiding excessive detail. Several abbreviated language elements - are available, enabling the writer to express proofs in a more - concise way, even without referring to any automated proof tools - yet. +text \<open>Isar provides several ways to fine-tune the reasoning, avoiding + excessive detail. Several abbreviated language elements are available, + enabling the writer to express proofs in a more concise way, even without + referring to any automated proof tools yet. - First of all, proof by assumption may be abbreviated as a single - dot.\<close> + First of all, proof by assumption may be abbreviated as a single dot.\<close> lemma "A \<longrightarrow> A" proof @@ -66,21 +63,21 @@ show A by fact+ qed -text \<open>In fact, concluding any (sub-)proof already involves solving - any remaining goals by assumption\footnote{This is not a completely - trivial operation, as proof by assumption may involve full - higher-order unification.}. Thus we may skip the rather vacuous - body of the above proof as well.\<close> +text \<open>In fact, concluding any (sub-)proof already involves solving any + remaining goals by assumption\footnote{This is not a completely trivial + operation, as proof by assumption may involve full higher-order + unification.}. Thus we may skip the rather vacuous body of the above proof + as well.\<close> lemma "A \<longrightarrow> A" proof qed -text \<open>Note that the \isacommand{proof} command refers to the @{text - rule} method (without arguments) by default. Thus it implicitly - applies a single rule, as determined from the syntactic form of the - statements involved. The \isacommand{by} command abbreviates any - proof with empty body, so the proof may be further pruned.\<close> +text \<open>Note that the \isacommand{proof} command refers to the \<open>rule\<close> method + (without arguments) by default. Thus it implicitly applies a single rule, + as determined from the syntactic form of the statements involved. The + \isacommand{by} command abbreviates any proof with empty body, so the + proof may be further pruned.\<close> lemma "A \<longrightarrow> A" by rule @@ -89,19 +86,18 @@ lemma "A \<longrightarrow> A" .. -text \<open>Thus we have arrived at an adequate representation of the - proof of a tautology that holds by a single standard - rule.\footnote{Apparently, the rule here is implication - introduction.}\<close> +text \<open>Thus we have arrived at an adequate representation of the proof of a + tautology that holds by a single standard rule.\footnote{Apparently, the + rule here is implication introduction.} -text \<open>Let us also reconsider @{text K}. Its statement is composed - of iterated connectives. Basic decomposition is by a single rule at - a time, which is why our first version above was by nesting two - proofs. + \<^medskip> + Let us also reconsider \<open>K\<close>. Its statement is composed of iterated + connectives. Basic decomposition is by a single rule at a time, which is + why our first version above was by nesting two proofs. - The @{text intro} proof method repeatedly decomposes a goal's - conclusion.\footnote{The dual method is @{text elim}, acting on a - goal's premises.}\<close> + The \<open>intro\<close> proof method repeatedly decomposes a goal's + conclusion.\footnote{The dual method is \<open>elim\<close>, acting on a goal's + premises.}\<close> lemma "A \<longrightarrow> B \<longrightarrow> A" proof (intro impI) @@ -114,29 +110,27 @@ lemma "A \<longrightarrow> B \<longrightarrow> A" by (intro impI) -text \<open>Just like @{text rule}, the @{text intro} and @{text elim} - proof methods pick standard structural rules, in case no explicit - arguments are given. While implicit rules are usually just fine for - single rule application, this may go too far with iteration. Thus - in practice, @{text intro} and @{text elim} would be typically - restricted to certain structures by giving a few rules only, e.g.\ - \isacommand{proof}~@{text "(intro impI allI)"} to strip implications - and universal quantifiers. +text \<open>Just like \<open>rule\<close>, the \<open>intro\<close> and \<open>elim\<close> proof methods pick standard + structural rules, in case no explicit arguments are given. While implicit + rules are usually just fine for single rule application, this may go too + far with iteration. Thus in practice, \<open>intro\<close> and \<open>elim\<close> would be + typically restricted to certain structures by giving a few rules only, + e.g.\ \isacommand{proof}~\<open>(intro impI allI)\<close> to strip implications and + universal quantifiers. - Such well-tuned iterated decomposition of certain structures is the - prime application of @{text intro} and @{text elim}. In contrast, - terminal steps that solve a goal completely are usually performed by - actual automated proof methods (such as \isacommand{by}~@{text - blast}.\<close> + Such well-tuned iterated decomposition of certain structures is the prime + application of \<open>intro\<close> and \<open>elim\<close>. In contrast, terminal steps that solve + a goal completely are usually performed by actual automated proof methods + (such as \isacommand{by}~\<open>blast\<close>.\<close> subsection \<open>Variations of backward vs.\ forward reasoning\<close> -text \<open>Certainly, any proof may be performed in backward-style only. - On the other hand, small steps of reasoning are often more naturally - expressed in forward-style. Isar supports both backward and forward - reasoning as a first-class concept. In order to demonstrate the - difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}. +text \<open>Certainly, any proof may be performed in backward-style only. On the + other hand, small steps of reasoning are often more naturally expressed in + forward-style. Isar supports both backward and forward reasoning as a + first-class concept. In order to demonstrate the difference, we consider + several proofs of \<open>A \<and> B \<longrightarrow> B \<and> A\<close>. The first version is purely backward.\<close> @@ -150,13 +144,12 @@ qed qed -text \<open>Above, the @{text "conjunct_1/2"} projection rules had to be - named explicitly, since the goals @{text B} and @{text A} did not - provide any structural clue. This may be avoided using - \isacommand{from} to focus on the @{text "A \<and> B"} assumption as the - current facts, enabling the use of double-dot proofs. Note that - \isacommand{from} already does forward-chaining, involving the - @{text conjE} rule here.\<close> +text \<open>Above, the projection rules \<open>conjunct1\<close> / \<open>conjunct2\<close> had to be named + explicitly, since the goals \<open>B\<close> and \<open>A\<close> did not provide any structural + clue. This may be avoided using \isacommand{from} to focus on the \<open>A \<and> B\<close> + assumption as the current facts, enabling the use of double-dot proofs. + Note that \isacommand{from} already does forward-chaining, involving the + \<open>conjE\<close> rule here.\<close> lemma "A \<and> B \<longrightarrow> B \<and> A" proof @@ -168,27 +161,26 @@ qed qed -text \<open>In the next version, we move the forward step one level - upwards. Forward-chaining from the most recent facts is indicated - by the \isacommand{then} command. Thus the proof of @{text "B \<and> A"} - from @{text "A \<and> B"} actually becomes an elimination, rather than an - introduction. The resulting proof structure directly corresponds to - that of the @{text conjE} rule, including the repeated goal - proposition that is abbreviated as @{text ?thesis} below.\<close> +text \<open>In the next version, we move the forward step one level upwards. + Forward-chaining from the most recent facts is indicated by the + \isacommand{then} command. Thus the proof of \<open>B \<and> A\<close> from \<open>A \<and> B\<close> actually + becomes an elimination, rather than an introduction. The resulting proof + structure directly corresponds to that of the \<open>conjE\<close> rule, including the + repeated goal proposition that is abbreviated as \<open>?thesis\<close> below.\<close> lemma "A \<and> B \<longrightarrow> B \<and> A" proof assume "A \<and> B" then show "B \<and> A" - proof -- \<open>rule @{text conjE} of @{text "A \<and> B"}\<close> + proof -- \<open>rule \<open>conjE\<close> of \<open>A \<and> B\<close>\<close> assume B A - then show ?thesis .. -- \<open>rule @{text conjI} of @{text "B \<and> A"}\<close> + then show ?thesis .. -- \<open>rule \<open>conjI\<close> of \<open>B \<and> A\<close>\<close> qed qed -text \<open>In the subsequent version we flatten the structure of the main - body by doing forward reasoning all the time. Only the outermost - decomposition step is left as backward.\<close> +text \<open>In the subsequent version we flatten the structure of the main body by + doing forward reasoning all the time. Only the outermost decomposition + step is left as backward.\<close> lemma "A \<and> B \<longrightarrow> B \<and> A" proof @@ -198,9 +190,9 @@ from \<open>B\<close> \<open>A\<close> show "B \<and> A" .. qed -text \<open>We can still push forward-reasoning a bit further, even at the - risk of getting ridiculous. Note that we force the initial proof - step to do nothing here, by referring to the ``-'' proof method.\<close> +text \<open>We can still push forward-reasoning a bit further, even at the risk of + getting ridiculous. Note that we force the initial proof step to do + nothing here, by referring to the \<open>-\<close> proof method.\<close> lemma "A \<and> B \<longrightarrow> B \<and> A" proof - @@ -210,27 +202,28 @@ from \<open>A \<and> B\<close> have B .. from \<open>B\<close> \<open>A\<close> have "B \<and> A" .. } - then show ?thesis .. -- \<open>rule @{text impI}\<close> + then show ?thesis .. -- \<open>rule \<open>impI\<close>\<close> qed -text \<open>\medskip With these examples we have shifted through a whole - range from purely backward to purely forward reasoning. Apparently, - in the extreme ends we get slightly ill-structured proofs, which - also require much explicit naming of either rules (backward) or - local facts (forward). +text \<open> + \<^medskip> + With these examples we have shifted through a whole range from purely + backward to purely forward reasoning. Apparently, in the extreme ends we + get slightly ill-structured proofs, which also require much explicit + naming of either rules (backward) or local facts (forward). - The general lesson learned here is that good proof style would - achieve just the \emph{right} balance of top-down backward - decomposition, and bottom-up forward composition. In general, there - is no single best way to arrange some pieces of formal reasoning, of - course. Depending on the actual applications, the intended audience - etc., rules (and methods) on the one hand vs.\ facts on the other - hand have to be emphasized in an appropriate way. This requires the - proof writer to develop good taste, and some practice, of course.\<close> + The general lesson learned here is that good proof style would achieve + just the \<^emph>\<open>right\<close> balance of top-down backward decomposition, and + bottom-up forward composition. In general, there is no single best way to + arrange some pieces of formal reasoning, of course. Depending on the + actual applications, the intended audience etc., rules (and methods) on + the one hand vs.\ facts on the other hand have to be emphasized in an + appropriate way. This requires the proof writer to develop good taste, and + some practice, of course. -text \<open>For our example the most appropriate way of reasoning is - probably the middle one, with conjunction introduction done after - elimination.\<close> + \<^medskip> + For our example the most appropriate way of reasoning is probably the + middle one, with conjunction introduction done after elimination.\<close> lemma "A \<and> B \<longrightarrow> B \<and> A" proof @@ -246,50 +239,48 @@ subsection \<open>A few examples from ``Introduction to Isabelle''\<close> -text \<open>We rephrase some of the basic reasoning examples of - @{cite "isabelle-intro"}, using HOL rather than FOL.\<close> +text \<open>We rephrase some of the basic reasoning examples of @{cite + "isabelle-intro"}, using HOL rather than FOL.\<close> subsubsection \<open>A propositional proof\<close> -text \<open>We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof - below involves forward-chaining from @{text "P \<or> P"}, followed by an - explicit case-analysis on the two \emph{identical} cases.\<close> +text \<open>We consider the proposition \<open>P \<or> P \<longrightarrow> P\<close>. The proof below involves + forward-chaining from \<open>P \<or> P\<close>, followed by an explicit case-analysis on + the two \<^emph>\<open>identical\<close> cases.\<close> lemma "P \<or> P \<longrightarrow> P" proof assume "P \<or> P" then show P - proof -- \<open> - rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$} -\<close> + proof -- \<open>rule \<open>disjE\<close>: \smash{$\infer{\<open>C\<close>}{\<open>A \<or> B\<close> & \infer*{\<open>C\<close>}{[\<open>A\<close>]} & \infer*{\<open>C\<close>}{[\<open>B\<close>]}}$}\<close> assume P show P by fact next assume P show P by fact qed qed -text \<open>Case splits are \emph{not} hardwired into the Isar language as - a special feature. The \isacommand{next} command used to separate - the cases above is just a short form of managing block structure. +text \<open>Case splits are \<^emph>\<open>not\<close> hardwired into the Isar language as a + special feature. The \isacommand{next} command used to separate the cases + above is just a short form of managing block structure. - \medskip In general, applying proof methods may split up a goal into - separate ``cases'', i.e.\ new subgoals with individual local - assumptions. The corresponding proof text typically mimics this by - establishing results in appropriate contexts, separated by blocks. + \<^medskip> + In general, applying proof methods may split up a goal into separate + ``cases'', i.e.\ new subgoals with individual local assumptions. The + corresponding proof text typically mimics this by establishing results in + appropriate contexts, separated by blocks. In order to avoid too much explicit parentheses, the Isar system implicitly opens an additional block for any new goal, the - \isacommand{next} statement then closes one block level, opening a - new one. The resulting behavior is what one would expect from - separating cases, only that it is more flexible. E.g.\ an induction - base case (which does not introduce local assumptions) would - \emph{not} require \isacommand{next} to separate the subsequent step - case. + \isacommand{next} statement then closes one block level, opening a new + one. The resulting behaviour is what one would expect from separating + cases, only that it is more flexible. E.g.\ an induction base case (which + does not introduce local assumptions) would \<^emph>\<open>not\<close> require + \isacommand{next} to separate the subsequent step case. - \medskip In our example the situation is even simpler, since the two - cases actually coincide. Consequently the proof may be rephrased as - follows.\<close> + \<^medskip> + In our example the situation is even simpler, since the two cases actually + coincide. Consequently the proof may be rephrased as follows.\<close> lemma "P \<or> P \<longrightarrow> P" proof @@ -316,37 +307,33 @@ subsubsection \<open>A quantifier proof\<close> -text \<open>To illustrate quantifier reasoning, let us prove @{text - "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"}. Informally, this holds because any - @{text a} with @{text "P (f a)"} may be taken as a witness for the - second existential statement. +text \<open>To illustrate quantifier reasoning, let us prove + \<open>(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)\<close>. Informally, this holds because any \<open>a\<close> with + \<open>P (f a)\<close> may be taken as a witness for the second existential statement. - The first proof is rather verbose, exhibiting quite a lot of - (redundant) detail. It gives explicit rules, even with some - instantiation. Furthermore, we encounter two new language elements: - the \isacommand{fix} command augments the context by some new - ``arbitrary, but fixed'' element; the \isacommand{is} annotation - binds term abbreviations by higher-order pattern matching.\<close> + The first proof is rather verbose, exhibiting quite a lot of (redundant) + detail. It gives explicit rules, even with some instantiation. + Furthermore, we encounter two new language elements: the \isacommand{fix} + command augments the context by some new ``arbitrary, but fixed'' element; + the \isacommand{is} annotation binds term abbreviations by higher-order + pattern matching.\<close> lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)" proof assume "\<exists>x. P (f x)" then show "\<exists>y. P y" - proof (rule exE) -- \<open> - rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$} -\<close> + proof (rule exE) -- \<open>rule \<open>exE\<close>: \smash{$\infer{\<open>B\<close>}{\<open>\<exists>x. A(x)\<close> & \infer*{\<open>B\<close>}{[\<open>A(x)\<close>]_x}}$}\<close> fix a assume "P (f a)" (is "P ?witness") then show ?thesis by (rule exI [of P ?witness]) qed qed -text \<open>While explicit rule instantiation may occasionally improve - readability of certain aspects of reasoning, it is usually quite - redundant. Above, the basic proof outline gives already enough - structural clues for the system to infer both the rules and their - instances (by higher-order unification). Thus we may as well prune - the text as follows.\<close> +text \<open>While explicit rule instantiation may occasionally improve readability + of certain aspects of reasoning, it is usually quite redundant. Above, the + basic proof outline gives already enough structural clues for the system + to infer both the rules and their instances (by higher-order unification). + Thus we may as well prune the text as follows.\<close> lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)" proof @@ -359,10 +346,9 @@ qed qed -text \<open>Explicit @{text \<exists>}-elimination as seen above can become quite - cumbersome in practice. The derived Isar language element - ``\isakeyword{obtain}'' provides a more handsome way to do - generalized existence reasoning.\<close> +text \<open>Explicit \<open>\<exists>\<close>-elimination as seen above can become quite cumbersome in + practice. The derived Isar language element ``\isakeyword{obtain}'' + provides a more handsome way to do generalized existence reasoning.\<close> lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)" proof @@ -371,21 +357,19 @@ then show "\<exists>y. P y" .. qed -text \<open>Technically, \isakeyword{obtain} is similar to - \isakeyword{fix} and \isakeyword{assume} together with a soundness - proof of the elimination involved. Thus it behaves similar to any - other forward proof element. Also note that due to the nature of - general existence reasoning involved here, any result exported from - the context of an \isakeyword{obtain} statement may \emph{not} refer - to the parameters introduced there.\<close> +text \<open>Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and + \isakeyword{assume} together with a soundness proof of the elimination + involved. Thus it behaves similar to any other forward proof element. Also + note that due to the nature of general existence reasoning involved here, + any result exported from the context of an \isakeyword{obtain} statement + may \<^emph>\<open>not\<close> refer to the parameters introduced there.\<close> subsubsection \<open>Deriving rules in Isabelle\<close> -text \<open>We derive the conjunction elimination rule from the - corresponding projections. The proof is quite straight-forward, - since Isabelle/Isar supports non-atomic goals and assumptions fully - transparently.\<close> +text \<open>We derive the conjunction elimination rule from the corresponding + projections. The proof is quite straight-forward, since Isabelle/Isar + supports non-atomic goals and assumptions fully transparently.\<close> theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C" proof -

--- a/src/HOL/Isar_Examples/Cantor.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Cantor.thy Tue Nov 03 11:20:21 2015 +0100 @@ -12,17 +12,17 @@ the Isabelle/HOL manual @{cite "isabelle-HOL"}.}\<close> text \<open>Cantor's Theorem states that every set has more subsets than - it has elements. It has become a favorite basic example in pure - higher-order logic since it is so easily expressed: \[\all{f::\alpha - \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} - \all{x::\alpha} f \ap x \not= S\] + it has elements. It has become a favourite basic example in pure + higher-order logic since it is so easily expressed: + + @{text [display] + \<open>\<forall>f::\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool. \<exists>S::\<alpha> \<Rightarrow> bool. \<forall>x::\<alpha>. f x \<noteq> S\<close>} - Viewing types as sets, $\alpha \To \idt{bool}$ represents the - powerset of $\alpha$. This version of the theorem states that for - every function from $\alpha$ to its powerset, some subset is outside - its range. The Isabelle/Isar proofs below uses HOL's set theory, - with the type $\alpha \ap \idt{set}$ and the operator - $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.\<close> + Viewing types as sets, \<open>\<alpha> \<Rightarrow> bool\<close> represents the powerset of \<open>\<alpha>\<close>. This + version of the theorem states that for every function from \<open>\<alpha>\<close> to its + powerset, some subset is outside its range. The Isabelle/Isar proofs below + uses HOL's set theory, with the type \<open>\<alpha> set\<close> and the operator + \<open>range :: (\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> \<beta> set\<close>.\<close> theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" proof @@ -46,20 +46,19 @@ qed qed -text \<open>How much creativity is required? As it happens, Isabelle can - prove this theorem automatically using best-first search. - Depth-first search would diverge, but best-first search successfully - navigates through the large search space. The context of Isabelle's - classical prover contains rules for the relevant constructs of HOL's - set theory.\<close> +text \<open>How much creativity is required? As it happens, Isabelle can prove + this theorem automatically using best-first search. Depth-first search + would diverge, but best-first search successfully navigates through the + large search space. The context of Isabelle's classical prover contains + rules for the relevant constructs of HOL's set theory.\<close> theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" by best -text \<open>While this establishes the same theorem internally, we do not - get any idea of how the proof actually works. There is currently no - way to transform internal system-level representations of Isabelle - proofs back into Isar text. Writing intelligible proof documents - really is a creative process, after all.\<close> +text \<open>While this establishes the same theorem internally, we do not get any + idea of how the proof actually works. There is currently no way to + transform internal system-level representations of Isabelle proofs back + into Isar text. Writing intelligible proof documents really is a creative + process, after all.\<close> end

--- a/src/HOL/Isar_Examples/Drinker.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Drinker.thy Tue Nov 03 11:20:21 2015 +0100 @@ -9,8 +9,8 @@ begin text \<open>Here is another example of classical reasoning: the Drinker's - Principle says that for some person, if he is drunk, everybody else - is drunk! + Principle says that for some person, if he is drunk, everybody else is + drunk! We first prove a classical part of de-Morgan's law.\<close>

--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Nov 03 11:20:21 2015 +0100 @@ -10,17 +10,16 @@ imports Main begin -text \<open>This is a (rather trivial) example of program verification. - We model a compiler for translating expressions to stack machine - instructions, and prove its correctness wrt.\ some evaluation - semantics.\<close> +text \<open>This is a (rather trivial) example of program verification. We model a + compiler for translating expressions to stack machine instructions, and + prove its correctness wrt.\ some evaluation semantics.\<close> subsection \<open>Binary operations\<close> -text \<open>Binary operations are just functions over some type of values. - This is both for abstract syntax and semantics, i.e.\ we use a - ``shallow embedding'' here.\<close> +text \<open>Binary operations are just functions over some type of values. This is + both for abstract syntax and semantics, i.e.\ we use a ``shallow + embedding'' here.\<close> type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val" @@ -28,16 +27,15 @@ subsection \<open>Expressions\<close> text \<open>The language of expressions is defined as an inductive type, - consisting of variables, constants, and binary operations on - expressions.\<close> + consisting of variables, constants, and binary operations on expressions.\<close> datatype (dead 'adr, dead 'val) expr = Variable 'adr | Constant 'val | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr" -text \<open>Evaluation (wrt.\ some environment of variable assignments) is - defined by primitive recursion over the structure of expressions.\<close> +text \<open>Evaluation (wrt.\ some environment of variable assignments) is defined + by primitive recursion over the structure of expressions.\<close> primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val" where @@ -48,16 +46,15 @@ subsection \<open>Machine\<close> -text \<open>Next we model a simple stack machine, with three - instructions.\<close> +text \<open>Next we model a simple stack machine, with three instructions.\<close> datatype (dead 'adr, dead 'val) instr = Const 'val | Load 'adr | Apply "'val binop" -text \<open>Execution of a list of stack machine instructions is easily - defined as follows.\<close> +text \<open>Execution of a list of stack machine instructions is easily defined as + follows.\<close> primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list" where @@ -75,8 +72,8 @@ subsection \<open>Compiler\<close> -text \<open>We are ready to define the compilation function of expressions - to lists of stack machine instructions.\<close> +text \<open>We are ready to define the compilation function of expressions to + lists of stack machine instructions.\<close> primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list" where @@ -85,9 +82,8 @@ | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]" -text \<open>The main result of this development is the correctness theorem - for @{text compile}. We first establish a lemma about @{text exec} - and list append.\<close> +text \<open>The main result of this development is the correctness theorem for + \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.\<close> lemma exec_append: "exec (xs @ ys) stack env = @@ -127,11 +123,14 @@ qed -text \<open>\bigskip In the proofs above, the @{text simp} method does - quite a lot of work behind the scenes (mostly ``functional program - execution''). Subsequently, the same reasoning is elaborated in - detail --- at most one recursive function definition is used at a - time. Thus we get a better idea of what is actually going on.\<close> +text \<open> + \<^bigskip> + In the proofs above, the \<open>simp\<close> method does quite a lot of work behind the + scenes (mostly ``functional program execution''). Subsequently, the same + reasoning is elaborated in detail --- at most one recursive function + definition is used at a time. Thus we get a better idea of what is + actually going on. +\<close> lemma exec_append': "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"

--- a/src/HOL/Isar_Examples/Group.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Group.thy Tue Nov 03 11:20:21 2015 +0100 @@ -10,18 +10,17 @@ subsection \<open>Groups and calculational reasoning\<close> -text \<open>Groups over signature $({\times} :: \alpha \To \alpha \To - \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ - are defined as an axiomatic type class as follows. Note that the - parent class $\idt{times}$ is provided by the basic HOL theory.\<close> +text \<open>Groups over signature \<open>(\<times> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, one :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close> + are defined as an axiomatic type class as follows. Note that the parent + class \<open>\<times>\<close> is provided by the basic HOL theory.\<close> class group = times + one + inverse + assumes group_assoc: "(x * y) * z = x * (y * z)" and group_left_one: "1 * x = x" and group_left_inverse: "inverse x * x = 1" -text \<open>The group axioms only state the properties of left one and - inverse, the right versions may be derived as follows.\<close> +text \<open>The group axioms only state the properties of left one and inverse, + the right versions may be derived as follows.\<close> theorem (in group) group_right_inverse: "x * inverse x = 1" proof - @@ -44,9 +43,8 @@ finally show ?thesis . qed -text \<open>With \name{group-right-inverse} already available, - \name{group-right-one}\label{thm:group-right-one} is now established - much easier.\<close> +text \<open>With \<open>group_right_inverse\<close> already available, \<open>group_right_one\<close> + \label{thm:group-right-one} is now established much easier.\<close> theorem (in group) group_right_one: "x * 1 = x" proof - @@ -61,27 +59,27 @@ finally show ?thesis . qed -text \<open>\medskip The calculational proof style above follows typical - presentations given in any introductory course on algebra. The - basic technique is to form a transitive chain of equations, which in - turn are established by simplifying with appropriate rules. The - low-level logical details of equational reasoning are left implicit. +text \<open> + \<^medskip> + The calculational proof style above follows typical presentations given in + any introductory course on algebra. The basic technique is to form a + transitive chain of equations, which in turn are established by + simplifying with appropriate rules. The low-level logical details of + equational reasoning are left implicit. - Note that ``$\dots$'' is just a special term variable that is bound - automatically to the argument\footnote{The argument of a curried - infix expression happens to be its right-hand side.} of the last - fact achieved by any local assumption or proven statement. In - contrast to $\var{thesis}$, the ``$\dots$'' variable is bound - \emph{after} the proof is finished, though. + Note that ``\<open>\<dots>\<close>'' is just a special term variable that is bound + automatically to the argument\footnote{The argument of a curried infix + expression happens to be its right-hand side.} of the last fact achieved + by any local assumption or proven statement. In contrast to \<open>?thesis\<close>, the + ``\<open>\<dots>\<close>'' variable is bound \<^emph>\<open>after\<close> the proof is finished. There are only two separate Isar language elements for calculational - proofs: ``\isakeyword{also}'' for initial or intermediate - calculational steps, and ``\isakeyword{finally}'' for exhibiting the - result of a calculation. These constructs are not hardwired into - Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. - Expanding the \isakeyword{also} and \isakeyword{finally} derived - language elements, calculations may be simulated by hand as - demonstrated below.\<close> + proofs: ``\isakeyword{also}'' for initial or intermediate calculational + steps, and ``\isakeyword{finally}'' for exhibiting the result of a + calculation. These constructs are not hardwired into Isabelle/Isar, but + defined on top of the basic Isar/VM interpreter. Expanding the + \isakeyword{also} and \isakeyword{finally} derived language elements, + calculations may be simulated by hand as demonstrated below.\<close> theorem (in group) "x * 1 = x" proof - @@ -114,51 +112,49 @@ show ?thesis . qed -text \<open>Note that this scheme of calculations is not restricted to - plain transitivity. Rules like anti-symmetry, or even forward and - backward substitution work as well. For the actual implementation - of \isacommand{also} and \isacommand{finally}, Isabelle/Isar - maintains separate context information of ``transitivity'' rules. - Rule selection takes place automatically by higher-order - unification.\<close> +text \<open>Note that this scheme of calculations is not restricted to plain + transitivity. Rules like anti-symmetry, or even forward and backward + substitution work as well. For the actual implementation of + \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains + separate context information of ``transitivity'' rules. Rule selection + takes place automatically by higher-order unification.\<close> subsection \<open>Groups as monoids\<close> -text \<open>Monoids over signature $({\times} :: \alpha \To \alpha \To - \alpha, \idt{one} :: \alpha)$ are defined like this.\<close> +text \<open>Monoids over signature \<open>(\<times> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, one :: \<alpha>)\<close> are defined like + this.\<close> class monoid = times + one + assumes monoid_assoc: "(x * y) * z = x * (y * z)" and monoid_left_one: "1 * x = x" and monoid_right_one: "x * 1 = x" -text \<open>Groups are \emph{not} yet monoids directly from the - definition. For monoids, \name{right-one} had to be included as an - axiom, but for groups both \name{right-one} and \name{right-inverse} - are derivable from the other axioms. With \name{group-right-one} - derived as a theorem of group theory (see +text \<open>Groups are \<^emph>\<open>not\<close> yet monoids directly from the definition. For + monoids, \<open>right_one\<close> had to be included as an axiom, but for groups both + \<open>right_one\<close> and \<open>right_inverse\<close> are derivable from the other axioms. With + \<open>group_right_one\<close> derived as a theorem of group theory (see page~\pageref{thm:group-right-one}), we may still instantiate - $\idt{group} \subseteq \idt{monoid}$ properly as follows.\<close> + \<open>group \<subseteq> monoid\<close> properly as follows.\<close> -instance group < monoid +instance group \<subseteq> monoid by intro_classes (rule group_assoc, rule group_left_one, rule group_right_one) text \<open>The \isacommand{instance} command actually is a version of - \isacommand{theorem}, setting up a goal that reflects the intended - class relation (or type constructor arity). Thus any Isar proof - language element may be involved to establish this statement. When - concluding the proof, the result is transformed into the intended - type signature extension behind the scenes.\<close> + \isacommand{theorem}, setting up a goal that reflects the intended class + relation (or type constructor arity). Thus any Isar proof language element + may be involved to establish this statement. When concluding the proof, + the result is transformed into the intended type signature extension + behind the scenes.\<close> subsection \<open>More theorems of group theory\<close> text \<open>The one element is already uniquely determined by preserving - an \emph{arbitrary} group element.\<close> + an \<^emph>\<open>arbitrary\<close> group element.\<close> theorem (in group) group_one_equality: assumes eq: "e * x = x"

--- a/src/HOL/Isar_Examples/Hoare.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Tue Nov 03 11:20:21 2015 +0100 @@ -12,11 +12,10 @@ subsection \<open>Abstract syntax and semantics\<close> -text \<open>The following abstract syntax and semantics of Hoare Logic - over \texttt{WHILE} programs closely follows the existing tradition - in Isabelle/HOL of formalizing the presentation given in - @{cite \<open>\S6\<close> "Winskel:1993"}. See also @{file "~~/src/HOL/Hoare"} and - @{cite "Nipkow:1998:Winskel"}.\<close> +text \<open>The following abstract syntax and semantics of Hoare Logic over + \<^verbatim>\<open>WHILE\<close> programs closely follows the existing tradition in Isabelle/HOL + of formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See + also @{file "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.\<close> type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" @@ -60,14 +59,15 @@ subsection \<open>Primitive Hoare rules\<close> -text \<open>From the semantics defined above, we derive the standard set - of primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. - Usually, variant forms of these rules are applied in actual proof, - see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}. +text \<open>From the semantics defined above, we derive the standard set of + primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually, + variant forms of these rules are applied in actual proof, see also + \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}. - \medskip The \name{basic} rule represents any kind of atomic access - to the state space. This subsumes the common rules of \name{skip} - and \name{assign}, as formulated in \S\ref{sec:hoare-isar}.\<close> + \<^medskip> + The \<open>basic\<close> rule represents any kind of atomic access to the state space. + This subsumes the common rules of \<open>skip\<close> and \<open>assign\<close>, as formulated in + \S\ref{sec:hoare-isar}.\<close> theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P" proof @@ -79,7 +79,7 @@ qed text \<open>The rules for sequential commands and semantic consequences are - established in a straight forward manner as follows.\<close> + established in a straight forward manner as follows.\<close> theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R" proof @@ -105,8 +105,8 @@ qed text \<open>The rule for conditional commands is directly reflected by the - corresponding semantics; in the proof we just have to look closely - which cases apply.\<close> + corresponding semantics; in the proof we just have to look closely which + cases apply.\<close> theorem cond: assumes case_b: "\<turnstile> (P \<inter> b) c1 Q" @@ -134,12 +134,11 @@ qed qed -text \<open>The @{text while} rule is slightly less trivial --- it is the - only one based on recursion, which is expressed in the semantics by - a Kleene-style least fixed-point construction. The auxiliary - statement below, which is by induction on the number of iterations - is the main point to be proven; the rest is by routine application - of the semantics of \texttt{WHILE}.\<close> +text \<open>The \<open>while\<close> rule is slightly less trivial --- it is the only one based + on recursion, which is expressed in the semantics by a Kleene-style least + fixed-point construction. The auxiliary statement below, which is by + induction on the number of iterations is the main point to be proven; the + rest is by routine application of the semantics of \<^verbatim>\<open>WHILE\<close>.\<close> theorem while: assumes body: "\<turnstile> (P \<inter> b) c P" @@ -167,24 +166,23 @@ text \<open>We now introduce concrete syntax for describing commands (with embedded expressions) and assertions. The basic technique is that of - semantic ``quote-antiquote''. A \emph{quotation} is a syntactic - entity delimited by an implicit abstraction, say over the state - space. An \emph{antiquotation} is a marked expression within a - quotation that refers the implicit argument; a typical antiquotation - would select (or even update) components from the state. + semantic ``quote-antiquote''. A \<^emph>\<open>quotation\<close> is a syntactic entity + delimited by an implicit abstraction, say over the state space. An + \<^emph>\<open>antiquotation\<close> is a marked expression within a quotation that refers the + implicit argument; a typical antiquotation would select (or even update) + components from the state. - We will see some examples later in the concrete rules and - applications.\<close> + We will see some examples later in the concrete rules and applications. -text \<open>The following specification of syntax and translations is for - Isabelle experts only; feel free to ignore it. + \<^medskip> + The following specification of syntax and translations is for Isabelle + experts only; feel free to ignore it. - While the first part is still a somewhat intelligible specification - of the concrete syntactic representation of our Hoare language, the - actual ``ML drivers'' is quite involved. Just note that the we - re-use the basic quote/antiquote translations as already defined in - Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and - @{ML Syntax_Trans.quote_tr'},).\<close> + While the first part is still a somewhat intelligible specification of the + concrete syntactic representation of our Hoare language, the actual ``ML + drivers'' is quite involved. Just note that the we re-use the basic + quote/antiquote translations as already defined in Isabelle/Pure (see @{ML + Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},).\<close> syntax "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" @@ -213,10 +211,9 @@ in [(@{syntax_const "_quote"}, K quote_tr)] end \<close> -text \<open>As usual in Isabelle syntax translations, the part for - printing is more complicated --- we cannot express parts as macro - rules as above. Don't look here, unless you have to do similar - things for yourself.\<close> +text \<open>As usual in Isabelle syntax translations, the part for printing is + more complicated --- we cannot express parts as macro rules as above. + Don't look here, unless you have to do similar things for yourself.\<close> print_translation \<open> let @@ -245,13 +242,14 @@ subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close> -text \<open>We are now ready to introduce a set of Hoare rules to be used - in single-step structured proofs in Isabelle/Isar. We refer to the - concrete syntax introduce above. +text \<open>We are now ready to introduce a set of Hoare rules to be used in + single-step structured proofs in Isabelle/Isar. We refer to the concrete + syntax introduce above. - \medskip Assertions of Hoare Logic may be manipulated in - calculational proofs, with the inclusion expressed in terms of sets - or predicates. Reversed order is supported as well.\<close> + \<^medskip> + Assertions of Hoare Logic may be manipulated in calculational proofs, with + the inclusion expressed in terms of sets or predicates. Reversed order is + supported as well.\<close> lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q" by (unfold Valid_def) blast @@ -278,10 +276,10 @@ by (simp add: Valid_def) -text \<open>Identity and basic assignments.\footnote{The $\idt{hoare}$ - method introduced in \S\ref{sec:hoare-vcg} is able to provide proper - instances for any number of basic assignments, without producing - additional verification conditions.}\<close> +text \<open>Identity and basic assignments.\footnote{The \<open>hoare\<close> method introduced + in \S\ref{sec:hoare-vcg} is able to provide proper instances for any + number of basic assignments, without producing additional verification + conditions.}\<close> lemma skip [intro?]: "\<turnstile> P SKIP P" proof - @@ -293,19 +291,19 @@ by (rule basic) text \<open>Note that above formulation of assignment corresponds to our - preferred way to model state spaces, using (extensible) record types - in HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field - $x$, Isabelle/HOL provides a functions $x$ (selector) and - $\idt{x{\dsh}update}$ (update). Above, there is only a place-holder - appearing for the latter kind of function: due to concrete syntax - \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that - due to the external nature of HOL record fields, we could not even - state a general theorem relating selector and update functions (if - this were required here); this would only work for any particular - instance of record fields introduced so far.}\<close> + preferred way to model state spaces, using (extensible) record types in + HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>, + Isabelle/HOL provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update). + Above, there is only a place-holder appearing for the latter kind of + function: due to concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains + \<open>x_update\<close>.\footnote{Note that due to the external nature of HOL record + fields, we could not even state a general theorem relating selector and + update functions (if this were required here); this would only work for + any particular instance of record fields introduced so far.} -text \<open>Sequential composition --- normalizing with associativity - achieves proper of chunks of code verified separately.\<close> + \<^medskip> + Sequential composition --- normalizing with associativity achieves proper + of chunks of code verified separately.\<close> lemmas [trans, intro?] = seq @@ -344,16 +342,15 @@ subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close> -text \<open>We now load the \emph{original} ML file for proof scripts and - tactic definition for the Hoare Verification Condition Generator - (see @{file "~~/src/HOL/Hoare/"}). As far as we - are concerned here, the result is a proof method \name{hoare}, which - may be applied to a Hoare Logic assertion to extract purely logical - verification conditions. It is important to note that the method - requires \texttt{WHILE} loops to be fully annotated with invariants - beforehand. Furthermore, only \emph{concrete} pieces of code are - handled --- the underlying tactic fails ungracefully if supplied - with meta-variables or parameters, for example.\<close> +text \<open>We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic + definition for the Hoare Verification Condition Generator (see @{file + "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a + proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to + extract purely logical verification conditions. It is important to note + that the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with + invariants beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are + handled --- the underlying tactic fails ungracefully if supplied with + meta-variables or parameters, for example.\<close> lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" by (auto simp add: Valid_def)

--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Nov 03 11:20:21 2015 +0100 @@ -6,9 +6,9 @@ subsection \<open>State spaces\<close> -text \<open>First of all we provide a store of program variables that - occur in any of the programs considered later. Slightly unexpected - things may happen when attempting to work with undeclared variables.\<close> +text \<open>First of all we provide a store of program variables that occur in any + of the programs considered later. Slightly unexpected things may happen + when attempting to work with undeclared variables.\<close> record vars = I :: nat @@ -16,29 +16,28 @@ N :: nat S :: nat -text \<open>While all of our variables happen to have the same type, - nothing would prevent us from working with many-sorted programs as - well, or even polymorphic ones. Also note that Isabelle/HOL's - extensible record types even provides simple means to extend the - state space later.\<close> +text \<open>While all of our variables happen to have the same type, nothing would + prevent us from working with many-sorted programs as well, or even + polymorphic ones. Also note that Isabelle/HOL's extensible record types + even provides simple means to extend the state space later.\<close> subsection \<open>Basic examples\<close> -text \<open>We look at few trivialities involving assignment and - sequential composition, in order to get an idea of how to work with - our formulation of Hoare Logic.\<close> +text \<open>We look at few trivialities involving assignment and sequential + composition, in order to get an idea of how to work with our formulation + of Hoare Logic.\<close> -text \<open>Using the basic @{text assign} rule directly is a bit +text \<open>Using the basic \<open>assign\<close> rule directly is a bit cumbersome.\<close> lemma "\<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>" by (rule assign) -text \<open>Certainly we want the state modification already done, e.g.\ - by simplification. The \name{hoare} method performs the basic state - update for us; we may apply the Simplifier afterwards to achieve - ``obvious'' consequences as well.\<close> +text \<open>Certainly we want the state modification already done, e.g.\ by + simplification. The \<open>hoare\<close> method performs the basic state update for us; + we may apply the Simplifier afterwards to achieve ``obvious'' consequences + as well.\<close> lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>" by hoare @@ -67,8 +66,8 @@ \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>" by hoare simp -text \<open>It is important to note that statements like the following one - can only be proven for each individual program variable. Due to the +text \<open>It is important to note that statements like the following one can + only be proven for each individual program variable. Due to the extra-logical nature of record fields, we cannot formulate a theorem relating record selectors and updates schematically.\<close> @@ -84,9 +83,9 @@ oops -text \<open>In the following assignments we make use of the consequence - rule in order to achieve the intended precondition. Certainly, the - \name{hoare} method is able to handle this case, too.\<close> +text \<open>In the following assignments we make use of the consequence rule in + order to achieve the intended precondition. Certainly, the \<open>hoare\<close> method + is able to handle this case, too.\<close> lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>" proof - @@ -114,10 +113,10 @@ subsection \<open>Multiplication by addition\<close> -text \<open>We now do some basic examples of actual \texttt{WHILE} - programs. This one is a loop for calculating the product of two - natural numbers, by iterated addition. We first give detailed - structured proof based on single-step Hoare rules.\<close> +text \<open>We now do some basic examples of actual \<^verbatim>\<open>WHILE\<close> programs. This one is + a loop for calculating the product of two natural numbers, by iterated + addition. We first give detailed structured proof based on single-step + Hoare rules.\<close> lemma "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> @@ -141,10 +140,10 @@ finally show ?thesis . qed -text \<open>The subsequent version of the proof applies the @{text hoare} - method to reduce the Hoare statement to a purely logical problem - that can be solved fully automatically. Note that we have to - specify the \texttt{WHILE} loop invariant in the original statement.\<close> +text \<open>The subsequent version of the proof applies the \<open>hoare\<close> method to + reduce the Hoare statement to a purely logical problem that can be solved + fully automatically. Note that we have to specify the \<^verbatim>\<open>WHILE\<close> loop + invariant in the original statement.\<close> lemma "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> @@ -157,15 +156,15 @@ subsection \<open>Summing natural numbers\<close> -text \<open>We verify an imperative program to sum natural numbers up to a - given limit. First some functional definition for proper - specification of the problem.\<close> +text \<open>We verify an imperative program to sum natural numbers up to a given + limit. First some functional definition for proper specification of the + problem. -text \<open>The following proof is quite explicit in the individual steps - taken, with the \name{hoare} method only applied locally to take - care of assignment and sequential composition. Note that we express - intermediate proof obligation in pure logic, without referring to - the state space.\<close> + \<^medskip> + The following proof is quite explicit in the individual steps taken, with + the \<open>hoare\<close> method only applied locally to take care of assignment and + sequential composition. Note that we express intermediate proof obligation + in pure logic, without referring to the state space.\<close> theorem "\<turnstile> \<lbrace>True\<rbrace> @@ -203,9 +202,8 @@ finally show ?thesis . qed -text \<open>The next version uses the @{text hoare} method, while still - explaining the resulting proof obligations in an abstract, - structured manner.\<close> +text \<open>The next version uses the \<open>hoare\<close> method, while still explaining the + resulting proof obligations in an abstract, structured manner.\<close> theorem "\<turnstile> \<lbrace>True\<rbrace> @@ -230,8 +228,8 @@ qed qed -text \<open>Certainly, this proof may be done fully automatic as well, - provided that the invariant is given beforehand.\<close> +text \<open>Certainly, this proof may be done fully automatic as well, provided + that the invariant is given beforehand.\<close> theorem "\<turnstile> \<lbrace>True\<rbrace> @@ -248,8 +246,8 @@ subsection \<open>Time\<close> -text \<open>A simple embedding of time in Hoare logic: function @{text - timeit} inserts an extra variable to keep track of the elapsed time.\<close> +text \<open>A simple embedding of time in Hoare logic: function \<open>timeit\<close> inserts + an extra variable to keep track of the elapsed time.\<close> record tstate = time :: nat

--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy Tue Nov 03 11:20:21 2015 +0100 @@ -14,30 +14,27 @@ subsection \<open>Prose version\<close> text \<open>According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"}, - the Knaster-Tarski fixpoint theorem is as - follows.\footnote{We have dualized the argument, and tuned the - notation a little bit.} - - \textbf{The Knaster-Tarski Fixpoint Theorem.} Let @{text L} be a - complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map. - Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}. + the Knaster-Tarski fixpoint theorem is as follows.\footnote{We have + dualized the argument, and tuned the notation a little bit.} - \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a = - \<Sqinter>H"}. For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text - "f(a) \<le> f(x) \<le> x"}. Thus @{text "f(a)"} is a lower bound of @{text - H}, whence @{text "f(a) \<le> a"}. We now use this inequality to prove - the reverse one (!) and thereby complete the proof that @{text a} is - a fixpoint. Since @{text f} is order-preserving, @{text "f(f(a)) \<le> - f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.\<close> + \<^bold>\<open>The Knaster-Tarski Fixpoint Theorem.\<close> Let \<open>L\<close> be a complete lattice and + \<open>f: L \<rightarrow> L\<close> an order-preserving map. Then \<open>\<Sqinter>{x \<in> L | f(x) \<le> x}\<close> is a + fixpoint of \<open>f\<close>. + + \<^bold>\<open>Proof.\<close> Let \<open>H = {x \<in> L | f(x) \<le> x}\<close> and \<open>a = \<Sqinter>H\<close>. For all \<open>x \<in> H\<close> we + have \<open>a \<le> x\<close>, so \<open>f(a) \<le> f(x) \<le> x\<close>. Thus \<open>f(a)\<close> is a lower bound of \<open>H\<close>, + whence \<open>f(a) \<le> a\<close>. We now use this inequality to prove the reverse one (!) + and thereby complete the proof that \<open>a\<close> is a fixpoint. Since \<open>f\<close> is + order-preserving, \<open>f(f(a)) \<le> f(a)\<close>. This says \<open>f(a) \<in> H\<close>, so \<open>a \<le> f(a)\<close>.\<close> subsection \<open>Formal versions\<close> -text \<open>The Isar proof below closely follows the original - presentation. Virtually all of the prose narration has been - rephrased in terms of formal Isar language elements. Just as many - textbook-style proofs, there is a strong bias towards forward proof, - and several bends in the course of reasoning.\<close> +text \<open>The Isar proof below closely follows the original presentation. + Virtually all of the prose narration has been rephrased in terms of formal + Isar language elements. Just as many textbook-style proofs, there is a + strong bias towards forward proof, and several bends in the course of + reasoning.\<close> theorem Knaster_Tarski: fixes f :: "'a::complete_lattice \<Rightarrow> 'a" @@ -67,15 +64,15 @@ qed qed -text \<open>Above we have used several advanced Isar language elements, - such as explicit block structure and weak assumptions. Thus we have - mimicked the particular way of reasoning of the original text. +text \<open>Above we have used several advanced Isar language elements, such as + explicit block structure and weak assumptions. Thus we have mimicked the + particular way of reasoning of the original text. - In the subsequent version the order of reasoning is changed to - achieve structured top-down decomposition of the problem at the - outer level, while only the inner steps of reasoning are done in a - forward manner. We are certainly more at ease here, requiring only - the most basic features of the Isar language.\<close> + In the subsequent version the order of reasoning is changed to achieve + structured top-down decomposition of the problem at the outer level, while + only the inner steps of reasoning are done in a forward manner. We are + certainly more at ease here, requiring only the most basic features of the + Isar language.\<close> theorem Knaster_Tarski': fixes f :: "'a::complete_lattice \<Rightarrow> 'a"

--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Tue Nov 03 11:20:21 2015 +0100 @@ -9,8 +9,8 @@ imports Main begin -text \<open>The Mutilated Checker Board Problem, formalized inductively. - See @{cite "paulson-mutilated-board"} for the original tactic script version.\<close> +text \<open>The Mutilated Checker Board Problem, formalized inductively. See @{cite + "paulson-mutilated-board"} for the original tactic script version.\<close> subsection \<open>Tilings\<close>

--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Nov 03 11:20:21 2015 +0100 @@ -20,7 +20,7 @@ lemmas subst_simps = subst_term.simps subst_term_list.simps -text \<open>\medskip A simple lemma about composition of substitutions.\<close> +text \<open>\<^medskip> A simple lemma about composition of substitutions.\<close> lemma "subst_term (subst_term f1 \<circ> f2) t =

--- a/src/HOL/Isar_Examples/Peirce.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Peirce.thy Tue Nov 03 11:20:21 2015 +0100 @@ -8,16 +8,15 @@ imports Main begin -text \<open>We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. - This is an inherently non-intuitionistic statement, so its proof - will certainly involve some form of classical contradiction. +text \<open>We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently + non-intuitionistic statement, so its proof will certainly involve some + form of classical contradiction. - The first proof is again a well-balanced combination of plain - backward and forward reasoning. The actual classical step is where - the negated goal may be introduced as additional assumption. This - eventually leads to a contradiction.\footnote{The rule involved - there is negation elimination; it holds in intuitionistic logic as - well.}\<close> + The first proof is again a well-balanced combination of plain backward and + forward reasoning. The actual classical step is where the negated goal may + be introduced as additional assumption. This eventually leads to a + contradiction.\footnote{The rule involved there is negation elimination; + it holds in intuitionistic logic as well.}\<close> theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" proof @@ -34,19 +33,17 @@ qed qed -text \<open>In the subsequent version the reasoning is rearranged by means - of ``weak assumptions'' (as introduced by \isacommand{presume}). - Before assuming the negated goal $\neg A$, its intended consequence - $A \impl B$ is put into place in order to solve the main problem. - Nevertheless, we do not get anything for free, but have to establish - $A \impl B$ later on. The overall effect is that of a logical - \emph{cut}. +text \<open>In the subsequent version the reasoning is rearranged by means of + ``weak assumptions'' (as introduced by \isacommand{presume}). Before + assuming the negated goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put + into place in order to solve the main problem. Nevertheless, we do not get + anything for free, but have to establish \<open>A \<longrightarrow> B\<close> later on. The overall + effect is that of a logical \<^emph>\<open>cut\<close>. - Technically speaking, whenever some goal is solved by - \isacommand{show} in the context of weak assumptions then the latter - give rise to new subgoals, which may be established separately. In - contrast, strong assumptions (as introduced by \isacommand{assume}) - are solved immediately.\<close> + Technically speaking, whenever some goal is solved by \isacommand{show} in + the context of weak assumptions then the latter give rise to new subgoals, + which may be established separately. In contrast, strong assumptions (as + introduced by \isacommand{assume}) are solved immediately.\<close> theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" proof @@ -65,21 +62,20 @@ qed qed -text \<open>Note that the goals stemming from weak assumptions may be even - left until qed time, where they get eventually solved ``by - assumption'' as well. In that case there is really no fundamental - difference between the two kinds of assumptions, apart from the - order of reducing the individual parts of the proof configuration. +text \<open>Note that the goals stemming from weak assumptions may be even left + until qed time, where they get eventually solved ``by assumption'' as + well. In that case there is really no fundamental difference between the + two kinds of assumptions, apart from the order of reducing the individual + parts of the proof configuration. - Nevertheless, the ``strong'' mode of plain assumptions is quite - important in practice to achieve robustness of proof text - interpretation. By forcing both the conclusion \emph{and} the - assumptions to unify with the pending goal to be solved, goal - selection becomes quite deterministic. For example, decomposition - with rules of the ``case-analysis'' type usually gives rise to - several goals that only differ in there local contexts. With strong - assumptions these may be still solved in any order in a predictable - way, while weak ones would quickly lead to great confusion, - eventually demanding even some backtracking.\<close> + Nevertheless, the ``strong'' mode of plain assumptions is quite important + in practice to achieve robustness of proof text interpretation. By forcing + both the conclusion \<^emph>\<open>and\<close> the assumptions to unify with the pending goal + to be solved, goal selection becomes quite deterministic. For example, + decomposition with rules of the ``case-analysis'' type usually gives rise + to several goals that only differ in there local contexts. With strong + assumptions these may be still solved in any order in a predictable way, + while weak ones would quickly lead to great confusion, eventually + demanding even some backtracking.\<close> end

--- a/src/HOL/Isar_Examples/Puzzle.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Puzzle.thy Tue Nov 03 11:20:21 2015 +0100 @@ -8,9 +8,8 @@ Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias Nipkow.}\<close> -text \<open>\textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ - such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$. - Demonstrate that $f$ is the identity.\<close> +text \<open>\<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that + \<open>f (f n) < f (Suc n)\<close> for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.\<close> theorem assumes f_ax: "\<And>n. f (f n) < f (Suc n)"

--- a/src/HOL/Isar_Examples/Summation.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/Summation.thy Tue Nov 03 11:20:21 2015 +0100 @@ -9,16 +9,16 @@ begin text \<open>Subsequently, we prove some summation laws of natural numbers - (including odds, squares, and cubes). These examples demonstrate - how plain natural deduction (including induction) may be combined - with calculational proof.\<close> + (including odds, squares, and cubes). These examples demonstrate how plain + natural deduction (including induction) may be combined with calculational + proof.\<close> subsection \<open>Summation laws\<close> -text \<open>The sum of natural numbers $0 + \cdots + n$ equals $n \times - (n + 1)/2$. Avoiding formal reasoning about division we prove this - equation multiplied by $2$.\<close> +text \<open>The sum of natural numbers \<open>0 + \<cdots> + n\<close> equals \<open>n \<times> (n + 1)/2\<close>. + Avoiding formal reasoning about division we prove this equation multiplied + by \<open>2\<close>.\<close> theorem sum_of_naturals: "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)" @@ -35,47 +35,39 @@ by simp qed -text \<open>The above proof is a typical instance of mathematical - induction. The main statement is viewed as some $\var{P} \ap n$ - that is split by the induction method into base case $\var{P} \ap - 0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap - n)$ for arbitrary $n$. +text \<open>The above proof is a typical instance of mathematical induction. The + main statement is viewed as some \<open>?P n\<close> that is split by the induction + method into base case \<open>?P 0\<close>, and step case \<open>?P n \<Longrightarrow> ?P (Suc n)\<close> for + arbitrary \<open>n\<close>. - The step case is established by a short calculation in forward - manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of - the thesis, the final result is achieved by transformations - involving basic arithmetic reasoning (using the Simplifier). The - main point is where the induction hypothesis $\var{S} \ap n = n - \times (n + 1)$ is introduced in order to replace a certain subterm. - So the ``transitivity'' rule involved here is actual - \emph{substitution}. Also note how the occurrence of ``\dots'' in - the subsequent step documents the position where the right-hand side - of the hypothesis got filled in. + The step case is established by a short calculation in forward manner. + Starting from the left-hand side \<open>?S (n + 1)\<close> of the thesis, the final + result is achieved by transformations involving basic arithmetic reasoning + (using the Simplifier). The main point is where the induction hypothesis + \<open>?S n = n \<times> (n + 1)\<close> is introduced in order to replace a certain subterm. + So the ``transitivity'' rule involved here is actual \<^emph>\<open>substitution\<close>. Also + note how the occurrence of ``\dots'' in the subsequent step documents the + position where the right-hand side of the hypothesis got filled in. - \medskip A further notable point here is integration of calculations - with plain natural deduction. This works so well in Isar for two - reasons. - \begin{enumerate} - - \item Facts involved in \isakeyword{also}~/ \isakeyword{finally} - calculational chains may be just anything. There is nothing special - about \isakeyword{have}, so the natural deduction element - \isakeyword{assume} works just as well. + \<^medskip> + A further notable point here is integration of calculations with plain + natural deduction. This works so well in Isar for two reasons. - \item There are two \emph{separate} primitives for building natural - deduction contexts: \isakeyword{fix}~$x$ and - \isakeyword{assume}~$A$. Thus it is possible to start reasoning - with some new ``arbitrary, but fixed'' elements before bringing in - the actual assumption. In contrast, natural deduction is - occasionally formalized with basic context elements of the form - $x:A$ instead. + \<^enum> Facts involved in \isakeyword{also}~/ \isakeyword{finally} + calculational chains may be just anything. There is nothing special + about \isakeyword{have}, so the natural deduction element + \isakeyword{assume} works just as well. + + \<^enum> There are two \<^emph>\<open>separate\<close> primitives for building natural deduction + contexts: \isakeyword{fix}~\<open>x\<close> and \isakeyword{assume}~\<open>A\<close>. Thus it is + possible to start reasoning with some new ``arbitrary, but fixed'' + elements before bringing in the actual assumption. In contrast, natural + deduction is occasionally formalized with basic context elements of the + form \<open>x:A\<close> instead. - \end{enumerate} -\<close> - -text \<open>\medskip We derive further summation laws for odds, squares, - and cubes as follows. The basic technique of induction plus - calculation is the same as before.\<close> + \<^medskip> + We derive further summation laws for odds, squares, and cubes as follows. + The basic technique of induction plus calculation is the same as before.\<close> theorem sum_of_odds: "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)" @@ -93,9 +85,8 @@ by simp qed -text \<open>Subsequently we require some additional tweaking of Isabelle - built-in arithmetic simplifications, such as bringing in - distributivity by hand.\<close> +text \<open>Subsequently we require some additional tweaking of Isabelle built-in + arithmetic simplifications, such as bringing in distributivity by hand.\<close> lemmas distrib = add_mult_distrib add_mult_distrib2 @@ -134,15 +125,13 @@ text \<open>Note that in contrast to older traditions of tactical proof scripts, the structured proof applies induction on the original, - unsimplified statement. This allows to state the induction cases - robustly and conveniently. Simplification (or other automated) - methods are then applied in terminal position to solve certain - sub-problems completely. + unsimplified statement. This allows to state the induction cases robustly + and conveniently. Simplification (or other automated) methods are then + applied in terminal position to solve certain sub-problems completely. - As a general rule of good proof style, automatic methods such as - $\idt{simp}$ or $\idt{auto}$ should normally be never used as - initial proof methods with a nested sub-proof to address the - automatically produced situation, but only as terminal ones to solve - sub-problems.\<close> + As a general rule of good proof style, automatic methods such as \<open>simp\<close> or + \<open>auto\<close> should normally be never used as initial proof methods with a + nested sub-proof to address the automatically produced situation, but only + as terminal ones to solve sub-problems.\<close> end

--- a/src/HOL/Isar_Examples/document/root.tex Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Isar_Examples/document/root.tex Tue Nov 03 11:20:21 2015 +0100 @@ -1,11 +1,22 @@ -\input{style} +\documentclass[11pt,a4paper]{article} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{ifthen,proof,amssymb,isabelle,isabellesym} +\isabellestyle{it} +\usepackage{pdfsetup}\urlstyle{rm} + +\renewcommand{\isacommand}[1] +{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof} + {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}} + +\newcommand{\DUMMYPROOF}{{\langle\mathit{proof}\rangle}} +\newcommand{\dummyproof}{$\DUMMYPROOF$} \hyphenation{Isabelle} \begin{document} \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic} -\author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex] +\author{Markus Wenzel \\[2ex] With contributions by Gertrud Bauer and Tobias Nipkow} \maketitle

--- a/src/HOL/Isar_Examples/document/style.tex Mon Nov 02 16:17:09 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ -\documentclass[11pt,a4paper]{article} -\usepackage[only,bigsqcap]{stmaryrd} -\usepackage{ifthen,proof,amssymb,isabelle,isabellesym} -\isabellestyle{it} -\usepackage{pdfsetup}\urlstyle{rm} - -\renewcommand{\isacommand}[1] -{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof} - {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}} - -\newcommand{\DUMMYPROOF}{{\langle\idt{proof}\rangle}} -\newcommand{\dummyproof}{$\DUMMYPROOF$} - -\newcommand{\name}[1]{\textsl{#1}} - -\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}} -\newcommand{\var}[1]{{?\!\idt{#1}}} -\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} -\newcommand{\dsh}{\dshsym} - -\newcommand{\To}{\to} -\newcommand{\dt}{{\mathpunct.}} -\newcommand{\ap}{\mathbin{\!}} -\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;} -\newcommand{\all}[1]{\forall #1\dt\;} -\newcommand{\ex}[1]{\exists #1\dt\;} -\newcommand{\impl}{\to} -\newcommand{\conj}{\land} -\newcommand{\disj}{\lor} -\newcommand{\Impl}{\Longrightarrow} - -\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End:

--- a/src/HOL/Library/Lattice_Algebras.thy Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Library/Lattice_Algebras.thy Tue Nov 03 11:20:21 2015 +0100 @@ -1,4 +1,4 @@ -(* Author: Steven Obua, TU Muenchen *) +(* Author: Steven Obua, TU Muenchen *) section \<open>Various algebraic structures combined with a lattice\<close> @@ -224,7 +224,7 @@ proof - from that have a: "inf (a + a) 0 = 0" by (simp add: inf_commute inf_absorb1) - have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a" (is "?l=_") + have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a" (is "?l = _") by (simp add: add_sup_inf_distribs inf_aci) then have "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute) @@ -619,4 +619,3 @@ qed end -

--- a/src/HOL/ROOT Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/ROOT Tue Nov 03 11:20:21 2015 +0100 @@ -647,7 +647,6 @@ document_files "root.bib" "root.tex" - "style.tex" session "HOL-Eisbach" in Eisbach = HOL + description {*

--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Nov 03 11:20:21 2015 +0100 @@ -397,15 +397,20 @@ val dfg = (case format of DFG _ => true | _ => false) fun str _ (AType ((s, _), [])) = if dfg andalso s = tptp_individual_type then dfg_individual_type else s - | str _ (AType ((s, _), tys)) = - let val ss = tys |> map (str false) in - if s = tptp_product_type then - ss |> space_implode - (if dfg then ", " else " " ^ tptp_product_type ^ " ") - |> (not dfg andalso length ss > 1) ? parens - else - tptp_string_of_app format s ss - end + | str rhs (AType ((s, _), tys)) = + if s = tptp_fun_type then + let val [ty1, ty2] = tys in + str rhs (AFun (ty1, ty2)) + end + else + let val ss = tys |> map (str false) in + if s = tptp_product_type then + ss |> space_implode + (if dfg then ", " else " " ^ tptp_product_type ^ " ") + |> (not dfg andalso length ss > 1) ? parens + else + tptp_string_of_app format s ss + end | str rhs (AFun (ty1, ty2)) = (str false ty1 |> dfg ? parens) ^ " " ^ (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Nov 03 11:20:21 2015 +0100 @@ -105,14 +105,13 @@ val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms val transfer_gfp_sugar_thms: theory -> gfp_sugar_thms -> gfp_sugar_thms - val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list -> - typ list -> typ list -> int list -> int list list -> term list -> Proof.context -> - (term list - * (typ list list * typ list list list list * term list list * term list list list list) option - * (string * term list * term list list - * (((term list list * term list list * term list list list list * term list list list list) - * term list list list) * typ list)) option) - * Proof.context + val mk_co_recs_prelims: Proof.context -> BNF_Util.fp_kind -> typ list list list -> typ list -> + typ list -> typ list -> typ list -> int list -> int list list -> term list -> + term list + * (typ list list * typ list list list list * term list list * term list list list list) option + * (string * term list * term list list + * (((term list list * term list list * term list list list list * term list list list list) + * term list list list) * typ list)) option val repair_nullary_single_ctr: typ list list -> typ list list val mk_corec_p_pred_types: typ list -> int list -> typ list list val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list -> @@ -1176,7 +1175,7 @@ | unzip_recT _ (Type (@{type_name prod}, Ts as [_, TFree _])) = Ts | unzip_recT _ T = [T]; -fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy = +fun mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts = let val Css = map2 replicate ns Cs; val x_Tssss = @@ -1188,11 +1187,11 @@ val x_Tsss' = map (map flat_rec_arg_args) x_Tssss; val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css; - val ((fss, xssss), lthy) = lthy + val ((fss, xssss), _) = ctxt |> mk_Freess "f" f_Tss ||>> mk_Freessss "x" x_Tssss; in - ((f_Tss, x_Tssss, fss, xssss), lthy) + (f_Tss, x_Tssss, fss, xssss) end; fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] @@ -1222,14 +1221,14 @@ mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss (binder_fun_types (fastype_of dtor_corec))); -fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy = +fun mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts = let val p_Tss = mk_corec_p_pred_types Cs ns; val (q_Tssss, g_Tsss, g_Tssss, corec_types) = mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts; - val (((((Free (x, _), cs), pss), qssss), gssss), lthy) = lthy + val (((((Free (x, _), cs), pss), qssss), gssss), _) = ctxt |> yield_singleton (mk_Frees "x") dummyT ||>> mk_Frees "a" Cs ||>> mk_Freess "p" p_Tss @@ -1238,7 +1237,7 @@ val cpss = map2 (map o rapp) cs pss; - fun build_sum_inj mk_inj = build_map lthy [] (uncurry mk_inj o dest_sumT o snd); + fun build_sum_inj mk_inj = build_map ctxt [] (uncurry mk_inj o dest_sumT o snd); fun build_dtor_corec_arg _ [] [cg] = cg | build_dtor_corec_arg T [cq] [cg, cg'] = @@ -1250,25 +1249,25 @@ val cgssss = map2 (map o map o map o rapp) cs gssss; val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss; in - ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy) + (x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)) end; -fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy = +fun mk_co_recs_prelims ctxt fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 = let - val thy = Proof_Context.theory_of lthy; + val thy = Proof_Context.theory_of ctxt; val (xtor_co_rec_fun_Ts, xtor_co_recs) = mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd); - val ((recs_args_types, corecs_args_types), lthy') = + val (recs_args_types, corecs_args_types) = if fp = Least_FP then - mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy - |>> (rpair NONE o SOME) + mk_recs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts + |> (rpair NONE o SOME) else - mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy - |>> (pair NONE o SOME); + mk_corecs_args_types ctxt ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts + |> (pair NONE o SOME); in - ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') + (xtor_co_recs, recs_args_types, corecs_args_types) end; fun mk_preds_getterss_join c cps absT abs cqgss = @@ -2175,8 +2174,9 @@ val kss = map (fn n => 1 upto n) ns; val mss = map (map length) ctr_Tsss; - val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') = - mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; + val (xtor_co_recs, recs_args_types, corecs_args_types) = + mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0; + val lthy' = lthy; fun define_ctrs_dtrs_for_type fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Nov 03 11:20:21 2015 +0100 @@ -255,8 +255,8 @@ val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs; val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As; - val ((xtor_co_recs, recs_args_types, corecs_args_types), _) = - mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy; + val (xtor_co_recs, recs_args_types, corecs_args_types) = + mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0; fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Nov 02 16:17:09 2015 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Nov 03 11:20:21 2015 +0100 @@ -462,16 +462,22 @@ else sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms raw_sel_bindingss; + val add_bindings = + Variable.add_fixes (distinct (op =) (filter Symbol_Pos.is_identifier + (map Binding.name_of (disc_bindings @ flat sel_bindingss)))) + #> snd; + val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss; - val ((((((((exh_y, xss), yss), fs), gs), u), w), (p, p'))) = + val ((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))) = no_defs_lthy - |> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *) + |> add_bindings + |> yield_singleton (mk_Frees fc_b_name) fcT + ||>> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *) ||>> mk_Freess "x" ctr_Tss ||>> mk_Freess "y" ctr_Tss ||>> mk_Frees "f" case_Ts ||>> mk_Frees "g" case_Ts - ||>> yield_singleton (mk_Frees fc_b_name) fcT ||>> yield_singleton (mk_Frees "z") B ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT |> fst; @@ -673,13 +679,14 @@ fun after_qed ([exhaust_thm] :: thmss) lthy = let - val ((((((((xss, xss'), fs), gs), h), (u, u')), v), p), _) = + val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) = lthy - |> mk_Freess' "x" ctr_Tss + |> add_bindings + |> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT + ||>> mk_Freess' "x" ctr_Tss ||>> mk_Frees "f" case_Ts ||>> mk_Frees "g" case_Ts ||>> yield_singleton (mk_Frees "h") (B --> C) - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT ||>> yield_singleton (mk_Frees (fc_b_name ^ "'")) fcT ||>> yield_singleton (mk_Frees "P") HOLogic.boolT; @@ -687,18 +694,18 @@ val xgs = map2 (curry Term.list_comb) gs xss; val fcase = Term.list_comb (casex, fs); - + val ufcase = fcase $ u; val vfcase = fcase $ v; - + val eta_fcase = Term.list_comb (casex, eta_fs); val eta_gcase = Term.list_comb (casex, eta_gs); - + val eta_ufcase = eta_fcase $ u; val eta_vgcase = eta_gcase $ v; fun mk_uu_eq () = HOLogic.mk_eq (u, u); - + val uv_eq = mk_Trueprop_eq (u, v); val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;

--- a/src/Pure/PIDE/markup.ML Mon Nov 02 16:17:09 2015 +0100 +++ b/src/Pure/PIDE/markup.ML Tue Nov 03 11:20:21 2015 +0100 @@ -36,7 +36,7 @@ val language_prop: bool -> T val language_ML: bool -> T val language_SML: bool -> T - val language_document: bool -> T + val language_document: {symbols: bool, delimited: bool} -> T val language_antiquotation: T val language_text: bool -> T val language_rail: T @@ -310,7 +310,8 @@ val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; -val language_document = language' {name = "document", symbols = false, antiquotes = true}; +fun language_document {symbols, delimited} = + language' {name = "document", symbols = symbols, antiquotes = true} delimited; val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; val language_text = language' {name = "text", symbols = true, antiquotes = false};

--- a/src/Pure/PIDE/query_operation.scala Mon Nov 02 16:17:09 2015 +0100 +++ b/src/Pure/PIDE/query_operation.scala Tue Nov 03 11:20:21 2015 +0100 @@ -16,6 +16,26 @@ val RUNNING = Value("running") val FINISHED = Value("finished") } + + object State + { + val empty: State = State() + + def make(command: Command, query: List[String]): State = + State(instance = Document_ID.make().toString, + location = Some(command), + query = query, + status = Status.WAITING) + } + + sealed case class State( + instance: String = Document_ID.none.toString, + location: Option[Command] = None, + query: List[String] = Nil, + update_pending: Boolean = false, + output: List[XML.Tree] = Nil, + status: Status.Value = Status.FINISHED, + exec_id: Document_ID.Exec = Document_ID.none) } class Query_Operation[Editor_Context]( @@ -26,37 +46,19 @@ consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) { private val print_function = operation_name + "_query" - private val instance = Document_ID.make().toString /* implicit state -- owned by GUI thread */ - @volatile private var current_location: Option[Command] = None - @volatile private var current_query: List[String] = Nil - @volatile private var current_update_pending = false - @volatile private var current_output: List[XML.Tree] = Nil - @volatile private var current_status = Query_Operation.Status.FINISHED - @volatile private var current_exec_id = Document_ID.none - - def get_location: Option[Command] = current_location + private val current_state = Synchronized(Query_Operation.State.empty) - private def reset_state() - { - current_location = None - current_query = Nil - current_update_pending = false - current_output = Nil - current_status = Query_Operation.Status.FINISHED - current_exec_id = Document_ID.none - } + def get_location: Option[Command] = current_state.value.location private def remove_overlay() { - current_location match { - case None => - case Some(command) => - editor.remove_overlay(command, print_function, instance :: current_query) - editor.flush() + val state = current_state.value + for (command <- state.location) { + editor.remove_overlay(command, print_function, state.instance :: state.query) } } @@ -70,29 +72,31 @@ /* snapshot */ - val (snapshot, command_results, removed) = - current_location match { + val state0 = current_state.value + + val (snapshot, command_results, results, removed) = + state0.location match { case Some(cmd) => val snapshot = editor.node_snapshot(cmd.node_name) val command_results = snapshot.state.command_results(snapshot.version, cmd) + val results = + (for { + (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator + if props.contains((Markup.INSTANCE, state0.instance)) + } yield elem).toList val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) - (snapshot, command_results, removed) + (snapshot, command_results, results, removed) case None => - (Document.Snapshot.init, Command.Results.empty, true) + (Document.Snapshot.init, Command.Results.empty, Nil, true) } - val results = - (for { - (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator - if props.contains((Markup.INSTANCE, instance)) - } yield elem).toList /* resolve sendback: static command id */ def resolve_sendback(body: XML.Body): XML.Body = { - current_location match { + state0.location match { case None => body case Some(command) => def resolve(body: XML.Body): XML.Body = @@ -101,7 +105,7 @@ case XML.Elem(Markup(Markup.SENDBACK, props), b) => val props1 = props.map({ - case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id => + case (Markup.ID, Properties.Value.Long(id)) if id == state0.exec_id => (Markup.ID, Properties.Value.Long(command.id)) case p => p }) @@ -137,27 +141,27 @@ get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse Query_Operation.Status.WAITING + + /* state update */ + if (new_status == Query_Operation.Status.RUNNING) results.collectFirst( { case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem)) if elem.name == Markup.RUNNING => id - }).foreach(id => current_exec_id = id) - - - /* state update */ + }).foreach(id => current_state.change(_.copy(exec_id = id))) - if (current_output != new_output || current_status != new_status) { + if (state0.output != new_output || state0.status != new_status) { if (snapshot.is_outdated) - current_update_pending = true + current_state.change(_.copy(update_pending = true)) else { - current_update_pending = false - if (current_output != new_output && !removed) { - current_output = new_output + current_state.change(_.copy(update_pending = false)) + if (state0.output != new_output && !removed) { + current_state.change(_.copy(output = new_output)) consume_output(snapshot, command_results, new_output) } - if (current_status != new_status) { - current_status = new_status + if (state0.status != new_status) { + current_state.change(_.copy(status = new_status)) consume_status(new_status) if (new_status == Query_Operation.Status.FINISHED) remove_overlay() @@ -170,7 +174,7 @@ /* query operations */ def cancel_query(): Unit = - GUI_Thread.require { editor.session.cancel_exec(current_exec_id) } + GUI_Thread.require { editor.session.cancel_exec(current_state.value.exec_id) } def apply_query(query: List[String]) { @@ -179,19 +183,18 @@ editor.current_node_snapshot(editor_context) match { case Some(snapshot) => remove_overlay() - reset_state() + current_state.change(_ => Query_Operation.State.empty) consume_output(Document.Snapshot.init, Command.Results.empty, Nil) if (!snapshot.is_outdated) { editor.current_command(editor_context, snapshot) match { case Some(command) => - current_location = Some(command) - current_query = query - current_status = Query_Operation.Status.WAITING - editor.insert_overlay(command, print_function, instance :: query) + val state = Query_Operation.State.make(command, query) + current_state.change(_ => state) + editor.insert_overlay(command, print_function, state.instance :: query) case None => } } - consume_status(current_status) + consume_status(current_state.value.status) editor.flush() case None => } @@ -201,8 +204,9 @@ { GUI_Thread.require {} + val state = current_state.value for { - command <- current_location + command <- state.location snapshot = editor.node_snapshot(command.node_name) link <- editor.hyperlink_command(true, snapshot, command) } link.follow(editor_context) @@ -214,10 +218,11 @@ private val main = Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => - current_location match { + val state = current_state.value + state.location match { case Some(command) - if current_update_pending || - (current_status != Query_Operation.Status.FINISHED && + if state.update_pending || + (state.status != Query_Operation.Status.FINISHED && changed.commands.contains(command)) => GUI_Thread.later { content_update() } case _ => @@ -231,8 +236,8 @@ def deactivate() { editor.session.commands_changed -= main remove_overlay() - reset_state() + current_state.change(_ => Query_Operation.State.empty) consume_output(Document.Snapshot.init, Command.Results.empty, Nil) - consume_status(current_status) + consume_status(Query_Operation.Status.FINISHED) } }

--- a/src/Pure/Thy/thy_info.scala Mon Nov 02 16:17:09 2015 +0100 +++ b/src/Pure/Thy/thy_info.scala Tue Nov 03 11:20:21 2015 +0100 @@ -35,23 +35,25 @@ object Dependencies { - val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty) + val empty = new Dependencies(Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty) } final class Dependencies private( rev_deps: List[Thy_Info.Dep], val keywords: Thy_Header.Keywords, + val seen: Set[Document.Node.Name], val seen_names: Multi_Map[String, Document.Node.Name], val seen_positions: Multi_Map[String, Position.T]) { def :: (dep: Thy_Info.Dep): Dependencies = new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, - seen_names, seen_positions) + seen, seen_names, seen_positions) def + (thy: (Document.Node.Name, Position.T)): Dependencies = { val (name, pos) = thy new Dependencies(rev_deps, keywords, + seen + name, seen_names + (name.theory -> name), seen_positions + (name.theory -> pos)) } @@ -102,15 +104,13 @@ required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies = { val (name, require_pos) = thy - val theory = name.theory def message: String = - "The error(s) above occurred for theory " + quote(theory) + + "The error(s) above occurred for theory " + quote(name.theory) + required_by(initiators) + Position.here(require_pos) val required1 = required + thy - if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory)) - required1 + if (required.seen(name) || resources.loaded_theories(name.theory)) required1 else { try { if (initiators.contains(name)) error(cycle_msg(initiators))

--- a/src/Pure/Thy/thy_output.ML Mon Nov 02 16:17:09 2015 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Nov 03 11:20:21 2015 +0100 @@ -196,7 +196,10 @@ fun output_text state {markdown} source = let val pos = Input.pos_of source; - val _ = Position.report pos (Markup.language_document (Input.is_delimited source)); + val _ = + Position.report pos + (Markup.language_document + {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source}); val syms = Input.source_explode source; val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;

--- a/src/Tools/jEdit/src/document_model.scala Mon Nov 02 16:17:09 2015 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Nov 03 11:20:21 2015 +0100 @@ -255,6 +255,9 @@ reset_blob() reset_bibtex() + for (doc_view <- PIDE.document_views(buffer)) + doc_view.rich_text_area.active_reset() + if (clear) { pending_clear = true pending.clear

--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Nov 02 16:17:09 2015 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 03 11:20:21 2015 +0100 @@ -41,7 +41,7 @@ name => (name, Document.Node.no_perspective_text)) val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective - if (edits.nonEmpty) session.update(doc_blobs, edits) + session.update(doc_blobs, edits) } private val delay_flush =