--- a/NEWS Fri Sep 25 23:39:08 2015 +0200
+++ b/NEWS Fri Sep 25 23:41:24 2015 +0200
@@ -188,7 +188,7 @@
* Abbreviations in type classes now carry proper sort constraint.
Rare INCOMPATIBILITY in situations where the previous misbehaviour
-has been exploited previously.
+has been exploited.
* Refinement of user-space type system in type classes: pseudo-local
operations behave more similar to abbreviations. Potential
@@ -212,16 +212,10 @@
* Combinator to represent case distinction on products is named "uncurry",
with "split" and "prod_case" retained as input abbreviations.
-Partially applied occurences of "uncurry" with eta-contracted body
-terms are not printed with special syntax, to provide a compact
-notation and getting rid of a special-case print translation.
Hence, the "uncurry"-expressions are printed the following way:
a) fully applied "uncurry f p": explicit case-expression;
-b) partially applied with explicit double lambda abstraction in
-the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
-c) partially applied with eta-contracted body term "uncurry f":
-no special syntax, plain "uncurry" combinator.
-This aims for maximum readability in a given subterm.
+b) partially applied "uncurry f": explicit paired abstraction;
+c) unapplied "uncurry": as it is.
INCOMPATIBILITY.
* Some old and rarely used ASCII replacement syntax has been removed.
--- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 25 23:41:24 2015 +0200
@@ -1000,9 +1000,30 @@
The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin
(Section~\ref{ssec:lifting}).
+\item[@{text "t."}\hthm{rel_mono_strong}\rm:] ~ \\
+@{thm list.rel_mono_strong[no_vars]}
+
+\item[@{text "t."}\hthm{rel_cong} @{text "[fundef_cong]"}\rm:] ~ \\
+@{thm list.rel_cong[no_vars]}
+
+\item[@{text "t."}\hthm{rel_cong_simp}\rm:] ~ \\
+@{thm list.rel_cong_simp[no_vars]}
+
\item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
@{thm list.rel_refl[no_vars]}
+\item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\
+@{thm list.rel_refl_strong[no_vars]}
+
+\item[@{text "t."}\hthm{rel_reflp}\rm:] ~ \\
+@{thm list.rel_reflp[no_vars]}
+
+\item[@{text "t."}\hthm{rel_symp}\rm:] ~ \\
+@{thm list.rel_symp[no_vars]}
+
+\item[@{text "t."}\hthm{rel_transp}\rm:] ~ \\
+@{thm list.rel_transp[no_vars]}
+
\item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
@{thm list.rel_transfer[no_vars]} \\
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
--- a/src/HOL/BNF_Def.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/BNF_Def.thy Fri Sep 25 23:41:24 2015 +0200
@@ -234,6 +234,18 @@
lemma ge_eq_refl: "op = \<le> R \<Longrightarrow> R x x"
by auto
+lemma reflp_eq: "reflp R = (op = \<le> R)"
+ by (auto simp: reflp_def fun_eq_iff)
+
+lemma transp_relcompp: "transp r \<longleftrightarrow> r OO r \<le> r"
+ by (auto simp: transp_def)
+
+lemma symp_conversep: "symp R = (R\<inverse>\<inverse> \<le> R)"
+ by (auto simp: symp_def fun_eq_iff)
+
+lemma diag_imp_eq_le: "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> \<forall>x y. x \<in> A \<longrightarrow> y \<in> A \<longrightarrow> x = y \<longrightarrow> R x y"
+ by blast
+
ML_file "Tools/BNF/bnf_util.ML"
ML_file "Tools/BNF/bnf_tactics.ML"
ML_file "Tools/BNF/bnf_def_tactics.ML"
--- a/src/HOL/Codegenerator_Test/Candidates.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Fri Sep 25 23:41:24 2015 +0200
@@ -8,6 +8,8 @@
Complex_Main
"~~/src/HOL/Library/Library"
"~~/src/HOL/Library/Sublist_Order"
+ "~~/src/HOL/Data_Structures/Tree_Map"
+ "~~/src/HOL/Data_Structures/Tree_Set"
"~~/src/HOL/Number_Theory/Eratosthenes"
"~~/src/HOL/ex/Records"
begin
--- a/src/HOL/Data_Structures/AList_Upd_Del.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/AList_Upd_Del.thy Fri Sep 25 23:41:24 2015 +0200
@@ -17,7 +17,7 @@
"map_of [] = (\<lambda>a. None)" |
"map_of ((x,y)#ps) = (\<lambda>a. if x=a then Some y else map_of ps a)"
-text \<open>Updating into an association list:\<close>
+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)]" |
@@ -58,6 +58,7 @@
by (meson le_less_trans map_of_None2 not_less sorted_snoc_iff)
lemmas map_of_sorteds = map_of_sorted_Cons map_of_sorted_snoc
+lemmas map_of_simps = sorted_lems map_of_append map_of_sorteds
subsection \<open>Lemmas for @{const upd_list}\<close>
@@ -136,4 +137,6 @@
lemmas del_list_sorted =
del_list_sorted1 del_list_sorted2 del_list_sorted3 del_list_sorted4 del_list_sorted5
+lemmas del_list_simps = sorted_lems del_list_sorted
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/AVL_Map.thy Fri Sep 25 23:41:24 2015 +0200
@@ -0,0 +1,54 @@
+(* Author: Tobias Nipkow *)
+
+section "AVL Tree Implementation of Maps"
+
+theory AVL_Map
+imports
+ AVL_Set
+ Lookup2
+begin
+
+fun update :: "'a::order \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
+"update x y Leaf = Node 1 Leaf (x,y) Leaf" |
+"update x y (Node h l (a,b) r) =
+ (if x = a then Node h l (x,y) r else
+ if x < a then node_bal_l (update x y l) (a,b) r
+ else node_bal_r l (a,b) (update x y r))"
+
+fun delete :: "'a::order \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
+"delete _ Leaf = Leaf" |
+"delete x (Node h l (a,b) r) = (
+ if x = a then delete_root (Node h l (a,b) r) else
+ if x < a then node_bal_r (delete x l) (a,b) r
+ else node_bal_l l (a,b) (delete x r))"
+
+
+subsection {* Functional Correctness Proofs *}
+
+theorem inorder_update:
+ "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
+by (induct t)
+ (auto simp: upd_list_simps inorder_node_bal_l inorder_node_bal_r)
+
+
+theorem inorder_delete:
+ "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
+by(induction t)
+ (auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r
+ inorder_delete_root inorder_delete_maxD split: prod.splits)
+
+
+interpretation Map_by_Ordered
+where empty = Leaf and lookup = lookup and update = update and delete = delete
+and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+ case 1 show ?case by simp
+next
+ case 2 thus ?case by(simp add: lookup_eq)
+next
+ case 3 thus ?case by(simp add: inorder_update)
+next
+ case 4 thus ?case by(simp add: inorder_delete)
+qed (rule TrueI)+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/AVL_Set.thy Fri Sep 25 23:41:24 2015 +0200
@@ -0,0 +1,457 @@
+(*
+Author: Tobias Nipkow
+Derived from AFP entry AVL.
+*)
+
+section "AVL Tree Implementation of Sets"
+
+theory AVL_Set
+imports Isin2
+begin
+
+type_synonym 'a avl_tree = "('a,nat) tree"
+
+text {* Invariant: *}
+
+fun avl :: "'a avl_tree \<Rightarrow> bool" where
+"avl Leaf = True" |
+"avl (Node h l a r) =
+ ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and>
+ h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
+
+fun ht :: "'a avl_tree \<Rightarrow> nat" where
+"ht Leaf = 0" |
+"ht (Node h l a r) = h"
+
+definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+"node l a r = Node (max (ht l) (ht r) + 1) l a r"
+
+definition node_bal_l :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+"node_bal_l l a r = (
+ if ht l = ht r + 2 then (case l of
+ Node _ bl b br \<Rightarrow> (if ht bl < ht br
+ then case br of
+ Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
+ else node bl b (node br a r)))
+ else node l a r)"
+
+definition node_bal_r :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+"node_bal_r l a r = (
+ if ht r = ht l + 2 then (case r of
+ Node _ bl b br \<Rightarrow> (if ht bl > ht br
+ then case bl of
+ Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
+ else node (node l a bl) b br))
+ else node l a r)"
+
+fun insert :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+"insert x Leaf = Node 1 Leaf x Leaf" |
+"insert x (Node h l a r) =
+ (if x=a then Node h l a r
+ else if x<a
+ then node_bal_l (insert x l) a r
+ else node_bal_r l a (insert x r))"
+
+fun delete_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
+"delete_max (Node _ l a Leaf) = (l,a)" |
+"delete_max (Node _ l a r) = (
+ let (r',a') = delete_max r in
+ (node_bal_l l a r', a'))"
+
+lemmas delete_max_induct = delete_max.induct[case_names Leaf Node]
+
+fun delete_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
+"delete_root (Node h Leaf a r) = r" |
+"delete_root (Node h l a Leaf) = l" |
+"delete_root (Node h l a r) =
+ (let (l', a') = delete_max l in node_bal_r l' a' r)"
+
+lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node]
+
+fun delete :: "'a::order \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+"delete _ Leaf = Leaf" |
+"delete x (Node h l a r) = (
+ if x = a then delete_root (Node h l a r)
+ else if x < a then node_bal_r (delete x l) a r
+ else node_bal_l l a (delete x r))"
+
+
+subsection {* Functional Correctness Proofs *}
+
+text{* Very different from the AFP/AVL proofs *}
+
+
+subsubsection "Proofs for insert"
+
+lemma inorder_node_bal_l:
+ "inorder (node_bal_l l a r) = inorder l @ a # inorder r"
+by (auto simp: node_def node_bal_l_def split:tree.splits)
+
+lemma inorder_node_bal_r:
+ "inorder (node_bal_r l a r) = inorder l @ a # inorder r"
+by (auto simp: node_def node_bal_r_def split:tree.splits)
+
+theorem inorder_insert:
+ "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
+by (induct t)
+ (auto simp: ins_list_simps inorder_node_bal_l inorder_node_bal_r)
+
+
+subsubsection "Proofs for delete"
+
+lemma inorder_delete_maxD:
+ "\<lbrakk> delete_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
+ inorder t' @ [a] = inorder t"
+by(induction t arbitrary: t' rule: delete_max.induct)
+ (auto simp: inorder_node_bal_l split: prod.splits tree.split)
+
+lemma inorder_delete_root:
+ "inorder (delete_root (Node h l a r)) = inorder l @ inorder r"
+by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct)
+ (auto simp: inorder_node_bal_r inorder_delete_maxD split: prod.splits)
+
+theorem inorder_delete:
+ "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
+by(induction t)
+ (auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r
+ inorder_delete_root inorder_delete_maxD split: prod.splits)
+
+
+subsubsection "Overall functional correctness"
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and wf = "\<lambda>_. True"
+proof (standard, goal_cases)
+ case 1 show ?case by simp
+next
+ case 2 thus ?case by(simp add: isin_set)
+next
+ case 3 thus ?case by(simp add: inorder_insert)
+next
+ case 4 thus ?case by(simp add: inorder_delete)
+next
+ case 5 thus ?case ..
+qed
+
+
+subsection {* AVL invariants *}
+
+text{* Essentially the AFP/AVL proofs *}
+
+
+subsubsection {* Insertion maintains AVL balance *}
+
+declare Let_def [simp]
+
+lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
+by (induct t) simp_all
+
+lemma height_node_bal_l:
+ "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
+ height (node_bal_l l a r) = height r + 2 \<or>
+ height (node_bal_l l a r) = height r + 3"
+by (cases l) (auto simp:node_def node_bal_l_def split:tree.split)
+
+lemma height_node_bal_r:
+ "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
+ height (node_bal_r l a r) = height l + 2 \<or>
+ height (node_bal_r l a r) = height l + 3"
+by (cases r) (auto simp add:node_def node_bal_r_def split:tree.split)
+
+lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
+by (simp add: node_def)
+
+lemma avl_node:
+ "\<lbrakk> avl l; avl r;
+ height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
+ \<rbrakk> \<Longrightarrow> avl(node l a r)"
+by (auto simp add:max_def node_def)
+
+lemma height_node_bal_l2:
+ "\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
+ height (node_bal_l l a r) = (1 + max (height l) (height r))"
+by (cases l, cases r) (simp_all add: node_bal_l_def)
+
+lemma height_node_bal_r2:
+ "\<lbrakk> avl l; avl r; height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
+ height (node_bal_r l a r) = (1 + max (height l) (height r))"
+by (cases l, cases r) (simp_all add: node_bal_r_def)
+
+lemma avl_node_bal_l:
+ assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
+ \<or> height r = height l + 1 \<or> height l = height r + 2"
+ shows "avl(node_bal_l l a r)"
+proof(cases l)
+ case Leaf
+ with assms show ?thesis by (simp add: node_def node_bal_l_def)
+next
+ case (Node ln ll lr lh)
+ with assms show ?thesis
+ proof(cases "height l = height r + 2")
+ case True
+ from True Node assms show ?thesis
+ by (auto simp: node_bal_l_def intro!: avl_node split: tree.split) arith+
+ next
+ case False
+ with assms show ?thesis by (simp add: avl_node node_bal_l_def)
+ qed
+qed
+
+lemma avl_node_bal_r:
+ assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
+ \<or> height r = height l + 1 \<or> height r = height l + 2"
+ shows "avl(node_bal_r l a r)"
+proof(cases r)
+ case Leaf
+ with assms show ?thesis by (simp add: node_def node_bal_r_def)
+next
+ case (Node rn rl rr rh)
+ with assms show ?thesis
+ proof(cases "height r = height l + 2")
+ case True
+ from True Node assms show ?thesis
+ by (auto simp: node_bal_r_def intro!: avl_node split: tree.split) arith+
+ next
+ case False
+ with assms show ?thesis by (simp add: node_bal_r_def avl_node)
+ qed
+qed
+
+(* It appears that these two properties need to be proved simultaneously: *)
+
+text{* Insertion maintains the AVL property: *}
+
+theorem avl_insert_aux:
+ assumes "avl t"
+ shows "avl(insert x t)"
+ "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
+using assms
+proof (induction t)
+ case (Node h l a r)
+ case 1
+ with Node show ?case
+ proof(cases "x = a")
+ case True
+ with Node 1 show ?thesis by simp
+ next
+ case False
+ with Node 1 show ?thesis
+ proof(cases "x<a")
+ case True
+ with Node 1 show ?thesis by (auto simp add:avl_node_bal_l)
+ next
+ case False
+ with Node 1 `x\<noteq>a` show ?thesis by (auto simp add:avl_node_bal_r)
+ qed
+ qed
+ case 2
+ from 2 Node show ?case
+ proof(cases "x = a")
+ case True
+ with Node 1 show ?thesis by simp
+ next
+ case False
+ with Node 1 show ?thesis
+ proof(cases "x<a")
+ case True
+ with Node 2 show ?thesis
+ proof(cases "height (insert x l) = height r + 2")
+ case False with Node 2 `x < a` show ?thesis by (auto simp: height_node_bal_l2)
+ next
+ case True
+ hence "(height (node_bal_l (insert x l) a r) = height r + 2) \<or>
+ (height (node_bal_l (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
+ using Node 2 by (intro height_node_bal_l) simp_all
+ thus ?thesis
+ proof
+ assume ?A
+ with 2 `x < a` show ?thesis by (auto)
+ next
+ assume ?B
+ with True 1 Node(2) `x < a` show ?thesis by (simp) arith
+ qed
+ qed
+ next
+ case False
+ with Node 2 show ?thesis
+ proof(cases "height (insert x r) = height l + 2")
+ case False
+ with Node 2 `\<not>x < a` show ?thesis by (auto simp: height_node_bal_r2)
+ next
+ case True
+ hence "(height (node_bal_r l a (insert x r)) = height l + 2) \<or>
+ (height (node_bal_r l a (insert x r)) = height l + 3)" (is "?A \<or> ?B")
+ using Node 2 by (intro height_node_bal_r) simp_all
+ thus ?thesis
+ proof
+ assume ?A
+ with 2 `\<not>x < a` show ?thesis by (auto)
+ next
+ assume ?B
+ with True 1 Node(4) `\<not>x < a` show ?thesis by (simp) arith
+ qed
+ qed
+ qed
+ qed
+qed simp_all
+
+
+subsubsection {* Deletion maintains AVL balance *}
+
+lemma avl_delete_max:
+ assumes "avl x" and "x \<noteq> Leaf"
+ shows "avl (fst (delete_max x))" "height x = height(fst (delete_max x)) \<or>
+ height x = height(fst (delete_max x)) + 1"
+using assms
+proof (induct x rule: delete_max_induct)
+ case (Node h l a rh rl b rr)
+ case 1
+ with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto
+ with 1 Node have "avl (node_bal_l l a (fst (delete_max (Node rh rl b rr))))"
+ by (intro avl_node_bal_l) fastforce+
+ thus ?case
+ by (auto simp: height_node_bal_l height_node_bal_l2
+ linorder_class.max.absorb1 linorder_class.max.absorb2
+ split:prod.split)
+next
+ case (Node h l a rh rl b rr)
+ case 2
+ let ?r = "Node rh rl b rr"
+ let ?r' = "fst (delete_max ?r)"
+ from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all
+ thus ?case using Node 2 height_node_bal_l[of l ?r' a] height_node_bal_l2[of l ?r' a]
+ apply (auto split:prod.splits simp del:avl.simps) by arith+
+qed auto
+
+lemma avl_delete_root:
+ assumes "avl t" and "t \<noteq> Leaf"
+ shows "avl(delete_root t)"
+using assms
+proof (cases t rule:delete_root_cases)
+ case (Node_Node h lh ll ln lr n rh rl rn rr)
+ let ?l = "Node lh ll ln lr"
+ let ?r = "Node rh rl rn rr"
+ let ?l' = "fst (delete_max ?l)"
+ from `avl t` and Node_Node have "avl ?r" by simp
+ from `avl t` and Node_Node have "avl ?l" by simp
+ hence "avl(?l')" "height ?l = height(?l') \<or>
+ height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+
+ with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
+ \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
+ with `avl ?l'` `avl ?r` have "avl(node_bal_r ?l' (snd(delete_max ?l)) ?r)"
+ by (rule avl_node_bal_r)
+ with Node_Node show ?thesis by (auto split:prod.splits)
+qed simp_all
+
+lemma height_delete_root:
+ assumes "avl t" and "t \<noteq> Leaf"
+ shows "height t = height(delete_root t) \<or> height t = height(delete_root t) + 1"
+using assms
+proof (cases t rule: delete_root_cases)
+ case (Node_Node h lh ll ln lr n rh rl rn rr)
+ let ?l = "Node lh ll ln lr"
+ let ?r = "Node rh rl rn rr"
+ let ?l' = "fst (delete_max ?l)"
+ let ?t' = "node_bal_r ?l' (snd(delete_max ?l)) ?r"
+ from `avl t` and Node_Node have "avl ?r" by simp
+ from `avl t` and Node_Node have "avl ?l" by simp
+ hence "avl(?l')" by (rule avl_delete_max,simp)
+ have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_delete_max) auto
+ have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp
+ have "height t = height ?t' \<or> height t = height ?t' + 1" using `avl t` Node_Node
+ proof(cases "height ?r = height ?l' + 2")
+ case False
+ show ?thesis using l'_height t_height False by (subst height_node_bal_r2[OF `avl ?l'` `avl ?r` False])+ arith
+ next
+ case True
+ show ?thesis
+ proof(cases rule: disjE[OF height_node_bal_r[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]])
+ case 1
+ thus ?thesis using l'_height t_height True by arith
+ next
+ case 2
+ thus ?thesis using l'_height t_height True by arith
+ qed
+ qed
+ thus ?thesis using Node_Node by (auto split:prod.splits)
+qed simp_all
+
+text{* Deletion maintains the AVL property: *}
+
+theorem avl_delete_aux:
+ assumes "avl t"
+ shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
+using assms
+proof (induct t)
+ case (Node h l n r)
+ case 1
+ with Node show ?case
+ proof(cases "x = n")
+ case True
+ with Node 1 show ?thesis by (auto simp:avl_delete_root)
+ next
+ case False
+ with Node 1 show ?thesis
+ proof(cases "x<n")
+ case True
+ with Node 1 show ?thesis by (auto simp add:avl_node_bal_r)
+ next
+ case False
+ with Node 1 `x\<noteq>n` show ?thesis by (auto simp add:avl_node_bal_l)
+ qed
+ qed
+ case 2
+ with Node show ?case
+ proof(cases "x = n")
+ case True
+ with 1 have "height (Node h l n r) = height(delete_root (Node h l n r))
+ \<or> height (Node h l n r) = height(delete_root (Node h l n r)) + 1"
+ by (subst height_delete_root,simp_all)
+ with True show ?thesis by simp
+ next
+ case False
+ with Node 1 show ?thesis
+ proof(cases "x<n")
+ case True
+ show ?thesis
+ proof(cases "height r = height (delete x l) + 2")
+ case False with Node 1 `x < n` show ?thesis by(auto simp: node_bal_r_def)
+ next
+ case True
+ hence "(height (node_bal_r (delete x l) n r) = height (delete x l) + 2) \<or>
+ height (node_bal_r (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
+ using Node 2 by (intro height_node_bal_r) auto
+ thus ?thesis
+ proof
+ assume ?A
+ with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
+ next
+ assume ?B
+ with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def)
+ qed
+ qed
+ next
+ case False
+ show ?thesis
+ proof(cases "height l = height (delete x r) + 2")
+ case False with Node 1 `\<not>x < n` `x \<noteq> n` show ?thesis by(auto simp: node_bal_l_def)
+ next
+ case True
+ hence "(height (node_bal_l l n (delete x r)) = height (delete x r) + 2) \<or>
+ height (node_bal_l l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
+ using Node 2 by (intro height_node_bal_l) auto
+ thus ?thesis
+ proof
+ assume ?A
+ with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
+ next
+ assume ?B
+ with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: node_bal_l_def)
+ qed
+ qed
+ qed
+ qed
+qed simp_all
+
+end
--- a/src/HOL/Data_Structures/Isin2.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/Isin2.thy Fri Sep 25 23:41:24 2015 +0200
@@ -13,9 +13,9 @@
"isin (Node _ l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)"
lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
-by (induction t) (auto simp: elems_simps)
+by (induction t) (auto simp: elems_simps1)
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
-by (induction t) (auto simp: elems_simps dest: sortedD)
+by (induction t) (auto simp: elems_simps2)
end
\ No newline at end of file
--- a/src/HOL/Data_Structures/List_Ins_Del.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/List_Ins_Del.thy Fri Sep 25 23:41:24 2015 +0200
@@ -26,15 +26,26 @@
"sorted(xs @ [x]) = (sorted xs \<and> (\<forall>y \<in> elems xs. y < x))"
by(simp add: elems_eq_set Sorted_Less.sorted_snoc_iff)
+text{* The above two rules introduce quantifiers. It turns out
+that in practice this is not a problem because of the simplicity of
+the "isin" functions that implement @{const elems}. Nevertheless
+it is possible to avoid the quantifiers with the help of some rewrite rules: *}
+
lemma sorted_ConsD: "sorted (y # xs) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> y < x"
by (simp add: sorted_Cons_iff)
lemma sorted_snocD: "sorted (xs @ [y]) \<Longrightarrow> x \<in> elems xs \<Longrightarrow> x < y"
by (simp add: sorted_snoc_iff)
-lemmas elems_simps0 = sorted_lems elems_app
-lemmas elems_simps = elems_simps0 sorted_Cons_iff sorted_snoc_iff
-lemmas sortedD = sorted_ConsD sorted_snocD
+lemma sorted_ConsD2: "sorted (y # xs) \<Longrightarrow> x \<le> y \<Longrightarrow> x \<notin> elems xs"
+using leD sorted_ConsD by blast
+
+lemma sorted_snocD2: "sorted (xs @ [y]) \<Longrightarrow> y \<le> x \<Longrightarrow> x \<notin> elems xs"
+using leD sorted_snocD by blast
+
+lemmas elems_simps = sorted_lems elems_app
+lemmas elems_simps1 = elems_simps sorted_Cons_iff sorted_snoc_iff
+lemmas elems_simps2 = elems_simps sorted_ConsD sorted_snocD sorted_ConsD2 sorted_snocD2
subsection \<open>Inserting into an ordered list without duplicates:\<close>
@@ -63,7 +74,7 @@
ins_list x (xs @ y # ys) = ins_list x xs @ (y#ys)"
by(induction xs) (auto simp: sorted_lems)
-lemmas ins_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
+lemmas ins_list_simps = sorted_lems ins_list_sorted1 ins_list_sorted2
subsection \<open>Delete one occurrence of an element from a list:\<close>
@@ -112,7 +123,7 @@
del_list a (xs @ x # ys @ y # zs @ z # us) @ u # vs"
by (induction xs) (auto simp: sorted_Cons_iff del_list_sorted4)
-lemmas del_simps = sorted_lems
+lemmas del_list_simps = sorted_lems
del_list_sorted1
del_list_sorted2
del_list_sorted3
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Lookup2.thy Fri Sep 25 23:41:24 2015 +0200
@@ -0,0 +1,21 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Function \textit{lookup} for Tree2\<close>
+
+theory Lookup2
+imports
+ Tree2
+ Map_by_Ordered
+begin
+
+fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
+"lookup Leaf x = None" |
+"lookup (Node _ l (a,b) r) x =
+ (if x < a then lookup l x else
+ if x > a then lookup r x else Some b)"
+
+lemma lookup_eq:
+ "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+by(induction t) (auto simp: map_of_simps split: option.split)
+
+end
\ No newline at end of file
--- a/src/HOL/Data_Structures/RBT.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/RBT.thy Fri Sep 25 23:41:24 2015 +0200
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)
-section \<open>Red-Black Trees\<close>
+section \<open>Red-Black Tree\<close>
theory RBT
imports Tree2
--- a/src/HOL/Data_Structures/RBT_Map.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/RBT_Map.thy Fri Sep 25 23:41:24 2015 +0200
@@ -5,15 +5,9 @@
theory RBT_Map
imports
RBT_Set
- Map_by_Ordered
+ Lookup2
begin
-fun lookup :: "('a::linorder * 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b option" where
-"lookup Leaf x = None" |
-"lookup (Node _ l (a,b) r) x =
- (if x < a then lookup l x else
- if x > a then lookup r x else Some b)"
-
fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
"update x y Leaf = R Leaf (x,y) Leaf" |
"update x y (B l (a,b) r) =
@@ -41,12 +35,6 @@
subsection "Functional Correctness Proofs"
-lemma lookup_eq:
- "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
-by(induction t)
- (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
-
-
lemma inorder_update:
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
by(induction x y t rule: update.induct)
@@ -60,7 +48,7 @@
"sorted1(inorder t2) \<Longrightarrow> inorder(deleteR x t1 a t2) =
inorder t1 @ a # del_list x (inorder t2)"
by(induction x t1 and x t1 a t2 and x t1 a t2 rule: delete_deleteL_deleteR.induct)
- (auto simp: del_list_sorted sorted_lems inorder_combine inorder_balL inorder_balR)
+ (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
interpretation Map_by_Ordered
--- a/src/HOL/Data_Structures/RBT_Set.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy Fri Sep 25 23:41:24 2015 +0200
@@ -35,29 +35,27 @@
lemma inorder_bal:
"inorder(bal l a r) = inorder l @ a # inorder r"
-by(induction l a r rule: bal.induct) (auto simp: sorted_lems)
+by(induction l a r rule: bal.induct) (auto)
lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
-by(induction a t rule: insert.induct) (auto simp: ins_simps inorder_bal)
+by(induction a t rule: insert.induct) (auto simp: ins_list_simps inorder_bal)
lemma inorder_red: "inorder(red t) = inorder t"
-by(induction t) (auto simp: sorted_lems)
+by(induction t) (auto)
lemma inorder_balL:
"inorder(balL l a r) = inorder l @ a # inorder r"
-by(induction l a r rule: balL.induct)
- (auto simp: sorted_lems inorder_bal inorder_red)
+by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_red)
lemma inorder_balR:
"inorder(balR l a r) = inorder l @ a # inorder r"
-by(induction l a r rule: balR.induct)
- (auto simp: sorted_lems inorder_bal inorder_red)
+by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_red)
lemma inorder_combine:
"inorder(combine l r) = inorder l @ inorder r"
by(induction l r rule: combine.induct)
- (auto simp: sorted_lems inorder_balL inorder_balR split: tree.split color.split)
+ (auto simp: inorder_balL inorder_balR split: tree.split color.split)
lemma inorder_delete:
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" and
@@ -66,7 +64,7 @@
"sorted(inorder r) \<Longrightarrow> inorder(deleteR x l a r) =
inorder l @ a # del_list x (inorder r)"
by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct)
- (auto simp: del_simps inorder_combine inorder_balL inorder_balR)
+ (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
interpretation Set_by_Ordered
where empty = Leaf and isin = isin and insert = insert and delete = delete
--- a/src/HOL/Data_Structures/Tree_Map.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/Tree_Map.thy Fri Sep 25 23:41:24 2015 +0200
@@ -4,7 +4,7 @@
theory Tree_Map
imports
- "~~/src/HOL/Library/Tree"
+ Tree_Set
Map_by_Ordered
begin
@@ -20,10 +20,6 @@
else if a=x then Node l (a,b) r
else Node l (x,y) (update a b 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*'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
@@ -35,9 +31,7 @@
lemma lookup_eq:
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
-apply (induction t)
-apply (auto simp: sorted_lems map_of_append map_of_sorteds split: option.split)
-done
+by (induction t) (auto simp: map_of_simps split: option.split)
lemma inorder_update:
@@ -49,12 +43,11 @@
"del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
x # inorder t' = inorder t"
by(induction t arbitrary: t' rule: del_min.induct)
- (auto simp: sorted_lems split: prod.splits)
+ (auto simp: del_list_simps split: prod.splits)
lemma inorder_delete:
"sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(induction t)
- (auto simp: del_list_sorted sorted_lems dest!: del_minD split: prod.splits)
+by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
interpretation Map_by_Ordered
--- a/src/HOL/Data_Structures/Tree_Set.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy Fri Sep 25 23:41:24 2015 +0200
@@ -35,15 +35,15 @@
subsection "Functional Correctness Proofs"
lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps)
+by (induction t) (auto simp: elems_simps1)
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
-by (induction t) (auto simp: elems_simps0 dest: sortedD)
+by (induction t) (auto simp: elems_simps2)
lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
-by(induction t) (auto simp: ins_simps)
+by(induction t) (auto simp: ins_list_simps)
lemma del_minD:
@@ -54,7 +54,7 @@
lemma inorder_delete:
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
-by(induction t) (auto simp: del_simps del_minD split: prod.splits)
+by(induction t) (auto simp: del_list_simps del_minD split: prod.splits)
interpretation Set_by_Ordered
--- a/src/HOL/Data_Structures/document/root.bib Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Data_Structures/document/root.bib Fri Sep 25 23:41:24 2015 +0200
@@ -6,7 +6,3 @@
@book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
publisher="Cambridge University Press",year=1998}
-
-@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
-title={Concrete Semantics with Isabelle/HOL},publisher=Springer,
-year=2014}
--- a/src/HOL/Fields.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Fields.thy Fri Sep 25 23:41:24 2015 +0200
@@ -333,6 +333,9 @@
lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
by (simp add: divide_inverse ac_simps)
+lemma divide_inverse_commute: "a / b = inverse b * a"
+ by (simp add: divide_inverse mult.commute)
+
lemma add_frac_eq:
assumes "y \<noteq> 0" and "z \<noteq> 0"
shows "x / y + w / z = (x * z + w * y) / (y * z)"
@@ -1169,6 +1172,38 @@
end
+text \<open>Min/max Simplification Rules\<close>
+
+lemma min_mult_distrib_left:
+ fixes x::"'a::linordered_idom"
+ shows "p * min x y = (if 0 \<le> p then min (p*x) (p*y) else max (p*x) (p*y))"
+by (auto simp add: min_def max_def mult_le_cancel_left)
+
+lemma min_mult_distrib_right:
+ fixes x::"'a::linordered_idom"
+ shows "min x y * p = (if 0 \<le> p then min (x*p) (y*p) else max (x*p) (y*p))"
+by (auto simp add: min_def max_def mult_le_cancel_right)
+
+lemma min_divide_distrib_right:
+ fixes x::"'a::linordered_field"
+ shows "min x y / p = (if 0 \<le> p then min (x/p) (y/p) else max (x/p) (y/p))"
+by (simp add: min_mult_distrib_right divide_inverse)
+
+lemma max_mult_distrib_left:
+ fixes x::"'a::linordered_idom"
+ shows "p * max x y = (if 0 \<le> p then max (p*x) (p*y) else min (p*x) (p*y))"
+by (auto simp add: min_def max_def mult_le_cancel_left)
+
+lemma max_mult_distrib_right:
+ fixes x::"'a::linordered_idom"
+ shows "max x y * p = (if 0 \<le> p then max (x*p) (y*p) else min (x*p) (y*p))"
+by (auto simp add: min_def max_def mult_le_cancel_right)
+
+lemma max_divide_distrib_right:
+ fixes x::"'a::linordered_field"
+ shows "max x y / p = (if 0 \<le> p then max (x/p) (y/p) else min (x/p) (y/p))"
+by (simp add: max_mult_distrib_right divide_inverse)
+
hide_fact (open) field_inverse field_divide_inverse field_inverse_zero
code_identifier
--- a/src/HOL/Filter.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Filter.thy Fri Sep 25 23:41:24 2015 +0200
@@ -390,6 +390,9 @@
lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
by (simp add: frequently_const_iff)
+lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
+ by (metis frequentlyE eventually_frequently)
+
abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
where "trivial_limit F \<equiv> F = bot"
@@ -994,7 +997,9 @@
by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
-by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
+apply (simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
+apply (safe; metis)
+done
lemma is_filter_parametric_aux:
assumes "is_filter F"
@@ -1038,7 +1043,8 @@
apply(rule iffI)
apply(erule (3) is_filter_parametric_aux)
apply(erule is_filter_parametric_aux[where A="conversep A"])
-apply(auto simp add: rel_fun_def)
+apply (simp_all add: rel_fun_def)
+apply metis
done
lemma left_total_rel_filter [transfer_rule]:
--- a/src/HOL/IMP/document/root.bib Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/IMP/document/root.bib Fri Sep 25 23:41:24 2015 +0200
@@ -15,6 +15,6 @@
editor={V. Chandru and V. Vinay},
publisher=Springer,series=LNCS,volume=1180,year=1996,pages={180--192}}
-@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
-title={Concrete Semantics. A Proof Assistant Approach},publisher=Springer,
-note={To appear}}
+@book{NipkowK2014,author={Tobias Nipkow and Gerwin Klein},
+title={Concrete Semantics with Isabelle/HOL},publisher="Springer",
+year=2014,note={\url{http://concrete-semantics.org}}}
--- a/src/HOL/IMP/document/root.tex Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/IMP/document/root.tex Fri Sep 25 23:41:24 2015 +0200
@@ -23,6 +23,10 @@
\author{Tobias Nipkow \& Gerwin Klein}
\maketitle
+\begin{abstract}
+This document presents formalizations of the semantics of a simple imperative programming language together with a number of applications: a compiler, type systems, various program analyses and abstract interpreters. These theories form the basis of the book \emph{Concrete Semantics with Isabelle/HOL} by Nipkow and Klein \cite{NipkowK2014}.
+\end{abstract}
+
\setcounter{tocdepth}{2}
\tableofcontents
\newpage
--- a/src/HOL/Int.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Int.thy Fri Sep 25 23:41:24 2015 +0200
@@ -258,6 +258,10 @@
"0 = of_int z \<longleftrightarrow> z = 0"
using of_int_eq_iff [of 0 z] by simp
+lemma of_int_eq_1_iff [iff]:
+ "of_int z = 1 \<longleftrightarrow> z = 1"
+ using of_int_eq_iff [of z 1] by simp
+
end
context linordered_idom
@@ -291,8 +295,49 @@
"of_int z < 0 \<longleftrightarrow> z < 0"
using of_int_less_iff [of z 0] by simp
+lemma of_int_1_le_iff [simp]:
+ "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z"
+ using of_int_le_iff [of 1 z] by simp
+
+lemma of_int_le_1_iff [simp]:
+ "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1"
+ using of_int_le_iff [of z 1] by simp
+
+lemma of_int_1_less_iff [simp]:
+ "1 < of_int z \<longleftrightarrow> 1 < z"
+ using of_int_less_iff [of 1 z] by simp
+
+lemma of_int_less_1_iff [simp]:
+ "of_int z < 1 \<longleftrightarrow> z < 1"
+ using of_int_less_iff [of z 1] by simp
+
end
+text \<open>Comparisons involving @{term of_int}.\<close>
+
+lemma of_int_eq_numeral_iff [iff]:
+ "of_int z = (numeral n :: 'a::ring_char_0)
+ \<longleftrightarrow> z = numeral n"
+ using of_int_eq_iff by fastforce
+
+lemma of_int_le_numeral_iff [simp]:
+ "of_int z \<le> (numeral n :: 'a::linordered_idom)
+ \<longleftrightarrow> z \<le> numeral n"
+ using of_int_le_iff [of z "numeral n"] by simp
+
+lemma of_int_numeral_le_iff [simp]:
+ "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
+ using of_int_le_iff [of "numeral n"] by simp
+
+lemma of_int_less_numeral_iff [simp]:
+ "of_int z < (numeral n :: 'a::linordered_idom)
+ \<longleftrightarrow> z < numeral n"
+ using of_int_less_iff [of z "numeral n"] by simp
+
+lemma of_int_numeral_less_iff [simp]:
+ "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
+ using of_int_less_iff [of "numeral n" z] by simp
+
lemma of_nat_less_of_int_iff:
"(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
by (metis of_int_of_nat_eq of_int_less_iff)
--- a/src/HOL/Library/Extended_Real.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Sep 25 23:41:24 2015 +0200
@@ -1732,6 +1732,14 @@
apply (auto split: ereal.split simp: ereal_uminus_reorder) []
done
+lemma at_infty_ereal_eq_at_top: "at \<infinity> = filtermap ereal at_top"
+ unfolding filter_eq_iff eventually_at_filter eventually_at_top_linorder eventually_filtermap
+ top_ereal_def[symmetric]
+ apply (subst eventually_nhds_top[of 0])
+ apply (auto simp: top_ereal_def less_le ereal_all_split ereal_ex_split)
+ apply (metis PInfty_neq_ereal(2) ereal_less_eq(3) ereal_top le_cases order_trans)
+ done
+
lemma ereal_Lim_uminus: "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
by auto
@@ -3589,6 +3597,34 @@
unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
using lim_ereal by (simp_all add: comp_def)
+lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)"
+proof -
+ have **: "((\<lambda>x. ereal (inverse x)) ---> ereal 0) at_infinity"
+ by (intro tendsto_intros tendsto_inverse_0)
+
+ show ?thesis
+ by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def)
+ (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity
+ intro!: filterlim_mono_eventually[OF **])
+qed
+
+lemma inverse_ereal_tendsto_pos:
+ fixes x :: ereal assumes "0 < x"
+ shows "inverse -- x --> inverse x"
+proof (cases x)
+ case (real r)
+ with `0 < x` have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
+ by (auto intro!: tendsto_inverse)
+ from real \<open>0 < x\<close> show ?thesis
+ by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
+ intro!: Lim_transform_eventually[OF _ **] t1_space_nhds)
+qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0)
+
+lemma inverse_ereal_tendsto_at_right_0: "(inverse ---> \<infinity>) (at_right (0::ereal))"
+ unfolding tendsto_compose_filtermap[symmetric] at_right_ereal zero_ereal_def
+ by (subst filterlim_cong[OF refl refl, where g="\<lambda>x. ereal (inverse x)"])
+ (auto simp: eventually_at_filter tendsto_PInfty_eq_at_top filterlim_inverse_at_top_right)
+
lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2
lemma continuous_at_iff_ereal:
--- a/src/HOL/Library/Liminf_Limsup.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy Fri Sep 25 23:41:24 2015 +0200
@@ -150,6 +150,17 @@
shows "Limsup F X \<le> C"
using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
+lemma le_Limsup:
+ assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
+ shows "l \<le> Limsup F f"
+proof -
+ have "l = Limsup F (\<lambda>x. l)"
+ using F by (simp add: Limsup_const)
+ also have "\<dots> \<le> Limsup F f"
+ by (intro Limsup_mono x)
+ finally show ?thesis .
+qed
+
lemma le_Liminf_iff:
fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
@@ -308,4 +319,33 @@
then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
qed
+lemma continuous_on_imp_continuous_within: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
+ unfolding continuous_on_eq_continuous_within by (auto simp: continuous_within intro: tendsto_within_subset)
+
+lemma Liminf_compose_continuous_antimono:
+ fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
+ assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
+ shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
+proof -
+ { fix P assume "eventually P F"
+ have "\<exists>x. P x"
+ proof (rule ccontr)
+ assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
+ by auto
+ with \<open>eventually P F\<close> F show False
+ by auto
+ qed }
+ note * = this
+
+ have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
+ unfolding Limsup_def INF_def
+ by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
+ (auto intro: eventually_True)
+ also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
+ by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
+ (auto dest!: eventually_happens simp: F)
+ finally show ?thesis
+ by (auto simp: Liminf_def)
+qed
+
end
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Fri Sep 25 23:41:24 2015 +0200
@@ -22,8 +22,8 @@
lemma shift_prefix_cases:
assumes "xl @- xs = yl @- ys"
shows "prefixeq xl yl \<or> prefixeq yl xl"
-using shift_prefix[OF assms] apply(cases "length xl \<le> length yl")
-by (metis, metis assms nat_le_linear shift_prefix)
+using shift_prefix[OF assms]
+by (cases "length xl \<le> length yl") (metis, metis assms nat_le_linear shift_prefix)
section\<open>Linear temporal logic\<close>
@@ -111,12 +111,12 @@
lemma ev_mono:
assumes ev: "ev \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs"
shows "ev \<psi> xs"
-using ev by induct (auto intro: ev.intros simp: 0)
+using ev by induct (auto simp: 0)
lemma alw_mono:
assumes alw: "alw \<phi> xs" and 0: "\<And> xs. \<phi> xs \<Longrightarrow> \<psi> xs"
shows "alw \<psi> xs"
-using alw by coinduct (auto elim: alw.cases simp: 0)
+using alw by coinduct (auto simp: 0)
lemma until_monoL:
assumes until: "(\<phi>1 until \<psi>) xs" and 0: "\<And> xs. \<phi>1 xs \<Longrightarrow> \<phi>2 xs"
@@ -137,55 +137,55 @@
lemma until_false: "\<phi> until false = alw \<phi>"
proof-
{fix xs assume "(\<phi> until false) xs" hence "alw \<phi> xs"
- apply coinduct by (auto elim: UNTIL.cases)
+ by coinduct (auto elim: UNTIL.cases)
}
moreover
{fix xs assume "alw \<phi> xs" hence "(\<phi> until false) xs"
- apply coinduct by (auto elim: alw.cases)
+ by coinduct auto
}
ultimately show ?thesis by blast
qed
lemma ev_nxt: "ev \<phi> = (\<phi> or nxt (ev \<phi>))"
-apply(rule ext) by (metis ev.simps nxt.simps)
+by (rule ext) (metis ev.simps nxt.simps)
lemma alw_nxt: "alw \<phi> = (\<phi> aand nxt (alw \<phi>))"
-apply(rule ext) by (metis alw.simps nxt.simps)
+by (rule ext) (metis alw.simps nxt.simps)
lemma ev_ev[simp]: "ev (ev \<phi>) = ev \<phi>"
proof-
{fix xs
assume "ev (ev \<phi>) xs" hence "ev \<phi> xs"
- by induct (auto intro: ev.intros)
+ by induct auto
}
- thus ?thesis by (auto intro: ev.intros)
+ thus ?thesis by auto
qed
lemma alw_alw[simp]: "alw (alw \<phi>) = alw \<phi>"
proof-
{fix xs
assume "alw \<phi> xs" hence "alw (alw \<phi>) xs"
- by coinduct (auto elim: alw.cases)
+ by coinduct auto
}
- thus ?thesis by (auto elim: alw.cases)
+ thus ?thesis by auto
qed
lemma ev_shift:
assumes "ev \<phi> xs"
shows "ev \<phi> (xl @- xs)"
-using assms by (induct xl) (auto intro: ev.intros)
+using assms by (induct xl) auto
lemma ev_imp_shift:
assumes "ev \<phi> xs" shows "\<exists> xl xs2. xs = xl @- xs2 \<and> \<phi> xs2"
using assms by induct (metis shift.simps(1), metis shift.simps(2) stream.collapse)+
lemma alw_ev_shift: "alw \<phi> xs1 \<Longrightarrow> ev (alw \<phi>) (xl @- xs1)"
-by (auto intro: ev_shift ev.intros)
+by (auto intro: ev_shift)
lemma alw_shift:
assumes "alw \<phi> (xl @- xs)"
shows "alw \<phi> xs"
-using assms by (induct xl) (auto elim: alw.cases)
+using assms by (induct xl) auto
lemma ev_ex_nxt:
assumes "ev \<phi> xs"
@@ -224,15 +224,15 @@
using assms nxt_wait_least unfolding nxt_sdrop by auto
lemma nxt_ev: "(nxt ^^ n) \<phi> xs \<Longrightarrow> ev \<phi> xs"
-by (induct n arbitrary: xs) (auto intro: ev.intros)
+by (induct n arbitrary: xs) auto
lemma not_ev: "not (ev \<phi>) = alw (not \<phi>)"
proof(rule ext, safe)
fix xs assume "not (ev \<phi>) xs" thus "alw (not \<phi>) xs"
- by (coinduct) (auto intro: ev.intros)
+ by (coinduct) auto
next
fix xs assume "ev \<phi> xs" and "alw (not \<phi>) xs" thus False
- by (induct) (auto elim: alw.cases)
+ by (induct) auto
qed
lemma not_alw: "not (alw \<phi>) = ev (not \<phi>)"
@@ -256,9 +256,7 @@
lemma ev_alw_imp_alw_ev:
assumes "ev (alw \<phi>) xs" shows "alw (ev \<phi>) xs"
-using assms apply induct
- apply (metis (full_types) alw_mono ev.base)
- by (metis alw alw_nxt ev.step)
+using assms by induct (metis (full_types) alw_mono ev.base, metis alw alw_nxt ev.step)
lemma alw_aand: "alw (\<phi> aand \<psi>) = alw \<phi> aand alw \<psi>"
proof-
@@ -267,7 +265,7 @@
}
moreover
{fix xs assume "(alw \<phi> aand alw \<psi>) xs" hence "alw (\<phi> aand \<psi>) xs"
- by coinduct (auto elim: alw.cases)
+ by coinduct auto
}
ultimately show ?thesis by blast
qed
@@ -279,7 +277,7 @@
}
moreover
{fix xs assume "ev (\<phi> or \<psi>) xs" hence "(ev \<phi> or ev \<psi>) xs"
- by induct (auto intro: ev.intros)
+ by induct auto
}
ultimately show ?thesis by blast
qed
@@ -314,7 +312,7 @@
lemma ev_alw_alw_impl:
assumes "ev (alw \<phi>) xs" and "alw (alw \<phi> impl ev \<psi>) xs"
shows "ev \<psi> xs"
-using assms by induct (auto intro: ev.intros elim: alw.cases)
+using assms by induct auto
lemma ev_alw_stl[simp]: "ev (alw \<phi>) (stl x) \<longleftrightarrow> ev (alw \<phi>) x"
by (metis (full_types) alw_nxt ev_nxt nxt.simps)
@@ -323,18 +321,18 @@
"alw (alw \<phi> impl ev \<psi>) = (ev (alw \<phi>) impl alw (ev \<psi>))" (is "?A = ?B")
proof-
{fix xs assume "?A xs \<and> ev (alw \<phi>) xs" hence "alw (ev \<psi>) xs"
- apply coinduct using ev_nxt by (auto elim: ev_alw_alw_impl alw.cases intro: ev.intros)
+ by coinduct (auto elim: ev_alw_alw_impl)
}
moreover
{fix xs assume "?B xs" hence "?A xs"
- apply coinduct by (auto elim: alw.cases intro: ev.intros)
+ by coinduct auto
}
ultimately show ?thesis by blast
qed
lemma ev_alw_impl:
assumes "ev \<phi> xs" and "alw (\<phi> impl \<psi>) xs" shows "ev \<psi> xs"
-using assms by induct (auto intro: ev.intros elim: alw.cases)
+using assms by induct auto
lemma ev_alw_impl_ev:
assumes "ev \<phi> xs" and "alw (\<phi> impl ev \<psi>) xs" shows "ev \<psi> xs"
@@ -345,7 +343,7 @@
shows "alw \<psi> xs"
proof-
{assume "alw \<phi> xs \<and> alw (\<phi> impl \<psi>) xs" hence ?thesis
- apply coinduct by (auto elim: alw.cases)
+ by coinduct auto
}
thus ?thesis using assms by auto
qed
@@ -362,7 +360,7 @@
lemma alw_impl_ev_alw:
assumes "alw (\<phi> impl ev \<psi>) xs"
shows "alw (ev \<phi> impl ev \<psi>) xs"
-using assms by coinduct (auto elim: alw.cases dest: ev_alw_impl intro: ev.intros)
+using assms by coinduct (auto dest: ev_alw_impl)
lemma ev_holds_sset:
"ev (holds P) xs \<longleftrightarrow> (\<exists> x \<in> sset xs. P x)" (is "?L \<longleftrightarrow> ?R")
@@ -379,7 +377,7 @@
shows "alw \<phi> xs"
proof-
{assume "\<phi> xs \<and> alw (\<phi> impl nxt \<phi>) xs" hence ?thesis
- apply coinduct by(auto elim: alw.cases)
+ by coinduct auto
}
thus ?thesis using assms by auto
qed
@@ -390,7 +388,7 @@
proof-
{assume "\<not> ev \<psi> xs" hence "alw (not \<psi>) xs" unfolding not_ev[symmetric] .
moreover have "alw (not \<psi> impl (\<phi> impl nxt \<phi>)) xs"
- using 2 by coinduct (auto elim: alw.cases)
+ using 2 by coinduct auto
ultimately have "alw (\<phi> impl nxt \<phi>) xs" by(auto dest: alw_mp)
with 1 have "alw \<phi> xs" by(rule alw_invar)
}
@@ -404,7 +402,7 @@
obtain xl xs1 where xs: "xs = xl @- xs1" and \<phi>: "\<phi> xs1"
using e by (metis ev_imp_shift)
have "\<phi> xs1 \<and> alw (\<phi> impl (nxt \<phi>)) xs1" using a \<phi> unfolding xs by (metis alw_shift)
- hence "alw \<phi> xs1" by(coinduct xs1 rule: alw.coinduct) (auto elim: alw.cases)
+ hence "alw \<phi> xs1" by(coinduct xs1 rule: alw.coinduct) auto
thus ?thesis unfolding xs by (auto intro: alw_ev_shift)
qed
@@ -602,7 +600,7 @@
using suntil.induct[of \<phi> \<psi> x P] by blast
lemma ev_suntil: "(\<phi> suntil \<psi>) \<omega> \<Longrightarrow> ev \<psi> \<omega>"
- by (induct rule: suntil.induct) (auto intro: ev.intros)
+ by (induct rule: suntil.induct) auto
lemma suntil_inv:
assumes stl: "\<And>s. f (stl s) = stl (f s)"
--- a/src/HOL/Library/RBT_Impl.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Fri Sep 25 23:41:24 2015 +0200
@@ -331,6 +331,8 @@
subsection \<open>Insertion\<close>
+text \<open>The function definitions are based on the book by Okasaki.\<close>
+
fun (* slow, due to massive case splitting *)
balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
@@ -554,6 +556,9 @@
lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
by (cases t rule: rbt_cases) auto
+text \<open>The function definitions are based on the Haskell code by Stefan Kahrs
+at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close>
+
fun
balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
--- a/src/HOL/MicroJava/DFA/Product.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/MicroJava/DFA/Product.thy Fri Sep 25 23:41:24 2015 +0200
@@ -43,7 +43,7 @@
"order(Product.le rA rB) = (order rA & order rB)"
apply (unfold Semilat.order_def)
apply simp
-apply blast
+apply meson
done
lemma acc_le_prodI [intro!]:
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri Sep 25 23:41:24 2015 +0200
@@ -501,10 +501,10 @@
unfolding holomorphic_on_def by (metis complex_differentiable_setsum)
definition deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
- "deriv f x \<equiv> THE D. DERIV f x :> D"
+ "deriv f x \<equiv> SOME D. DERIV f x :> D"
lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
- unfolding deriv_def by (metis the_equality DERIV_unique)
+ unfolding deriv_def by (metis some_equality DERIV_unique)
lemma DERIV_deriv_iff_real_differentiable:
fixes x :: real
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Sep 25 23:41:24 2015 +0200
@@ -2200,18 +2200,35 @@
definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
-lemma vector_derivative_unique_at:
- assumes "(f has_vector_derivative f') (at x)"
- and "(f has_vector_derivative f'') (at x)"
+lemma vector_derivative_unique_within:
+ assumes not_bot: "at x within s \<noteq> bot"
+ and f': "(f has_vector_derivative f') (at x within s)"
+ and f'': "(f has_vector_derivative f'') (at x within s)"
shows "f' = f''"
proof -
have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
- using assms [unfolded has_vector_derivative_def]
- by (rule frechet_derivative_unique_at)
+ proof (rule frechet_derivative_unique_within)
+ show "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> x + d *\<^sub>R i \<in> s"
+ proof clarsimp
+ fix e :: real assume "0 < e"
+ with islimpt_approachable_real[of x s] not_bot
+ obtain x' where "x' \<in> s" "x' \<noteq> x" "\<bar>x' - x\<bar> < e"
+ by (auto simp add: trivial_limit_within)
+ then show "\<exists>d. d \<noteq> 0 \<and> \<bar>d\<bar> < e \<and> x + d \<in> s"
+ by (intro exI[of _ "x' - x"]) auto
+ qed
+ qed (insert f' f'', auto simp: has_vector_derivative_def)
then show ?thesis
unfolding fun_eq_iff by auto
qed
+lemma vector_derivative_unique_at:
+ "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f'') (at x) \<Longrightarrow> f' = f''"
+ by (rule vector_derivative_unique_within) auto
+
+lemma differentiableI_vector: "(f has_vector_derivative y) F \<Longrightarrow> f differentiable F"
+ by (auto simp: differentiable_def has_vector_derivative_def)
+
lemma vector_derivative_works:
"f differentiable net \<longleftrightarrow> (f has_vector_derivative (vector_derivative f net)) net"
(is "?l = ?r")
@@ -2226,38 +2243,44 @@
by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f')
qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def)
+lemma vector_derivative_within:
+ assumes not_bot: "at x within s \<noteq> bot" and y: "(f has_vector_derivative y) (at x within s)"
+ shows "vector_derivative f (at x within s) = y"
+ using y
+ by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
+ (auto simp: differentiable_def has_vector_derivative_def)
+
+lemma islimpt_closure_open:
+ fixes s :: "'a::perfect_space set"
+ assumes "open s" and t: "t = closure s" "x \<in> t"
+ shows "x islimpt t"
+proof cases
+ assume "x \<in> s"
+ { fix T assume "x \<in> T" "open T"
+ then have "open (s \<inter> T)"
+ using \<open>open s\<close> by auto
+ then have "s \<inter> T \<noteq> {x}"
+ using not_open_singleton[of x] by auto
+ with \<open>x \<in> T\<close> \<open>x \<in> s\<close> have "\<exists>y\<in>t. y \<in> T \<and> y \<noteq> x"
+ using closure_subset[of s] by (auto simp: t) }
+ then show ?thesis
+ by (auto intro!: islimptI)
+next
+ assume "x \<notin> s" with t show ?thesis
+ unfolding t closure_def by (auto intro: islimpt_subset)
+qed
+
lemma vector_derivative_unique_within_closed_interval:
- assumes "a < b"
- and "x \<in> cbox a b"
- assumes "(f has_vector_derivative f') (at x within cbox a b)"
- assumes "(f has_vector_derivative f'') (at x within cbox a b)"
+ assumes ab: "a < b" "x \<in> cbox a b"
+ assumes D: "(f has_vector_derivative f') (at x within cbox a b)" "(f has_vector_derivative f'') (at x within cbox a b)"
shows "f' = f''"
-proof -
- have *: "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
- apply (rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
- using assms(3-)[unfolded has_vector_derivative_def]
- using assms(1-2)
- apply auto
- done
- show ?thesis
- proof (rule ccontr)
- assume **: "f' \<noteq> f''"
- with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
- by (auto simp: fun_eq_iff)
- with ** show False
- unfolding o_def by auto
- qed
-qed
+ using ab
+ by (intro vector_derivative_unique_within[OF _ D])
+ (auto simp: trivial_limit_within intro!: islimpt_closure_open[where s="{a <..< b}"])
lemma vector_derivative_at:
"(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
- apply (rule vector_derivative_unique_at)
- defer
- apply assumption
- unfolding vector_derivative_works[symmetric] differentiable_def
- unfolding has_vector_derivative_def
- apply auto
- done
+ by (intro vector_derivative_within at_neq_bot)
lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
by (simp add: vector_derivative_at)
@@ -2292,15 +2315,12 @@
done
lemma vector_derivative_within_closed_interval:
- assumes "a < b"
- and "x \<in> cbox a b"
- assumes "(f has_vector_derivative f') (at x within cbox a b)"
+ assumes ab: "a < b" "x \<in> cbox a b"
+ assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
shows "vector_derivative f (at x within cbox a b) = f'"
- apply (rule vector_derivative_unique_within_closed_interval)
- using vector_derivative_works[unfolded differentiable_def]
- using assms
- apply (auto simp add:has_vector_derivative_def)
- done
+ by (intro vector_derivative_unique_within_closed_interval[OF ab _ f]
+ vector_derivative_works[THEN iffD1] differentiableI_vector)
+ fact
lemma has_vector_derivative_within_subset:
"(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Sep 25 23:41:24 2015 +0200
@@ -313,6 +313,46 @@
apply (metis INF_absorb centre_in_ball)
done
+lemma continuous_on_inverse_ereal: "continuous_on {0::ereal ..} inverse"
+ unfolding continuous_on_def
+proof clarsimp
+ fix x :: ereal assume "0 \<le> x"
+ moreover have "at 0 within {0 ..} = at_right (0::ereal)"
+ by (auto simp: filter_eq_iff eventually_at_filter le_less)
+ moreover have "0 < x \<Longrightarrow> at x within {0 ..} = at x"
+ using at_within_interior[of x "{0 ..}"] by (simp add: interior_Ici[of "- \<infinity>"])
+ ultimately show "(inverse ---> inverse x) (at x within {0..})"
+ by (auto simp: le_less inverse_ereal_tendsto_at_right_0 inverse_ereal_tendsto_pos)
+qed
+
+
+lemma Liminf_inverse_ereal:
+ assumes nneg: "\<forall>\<^sub>F x in F. f x \<ge> (0 :: ereal)" and "F \<noteq> bot"
+ shows "Liminf F (\<lambda>n. inverse (f n)) = inverse (Limsup F f)"
+proof -
+ def I \<equiv> "\<lambda>x::ereal. if x \<le> 0 then \<infinity> else inverse x"
+ have "Liminf F (\<lambda>n. I (f n)) = I (Limsup F f)"
+ proof (rule Liminf_compose_continuous_antimono)
+ have "continuous_on ({.. 0} \<union> {0 ..}) I"
+ unfolding I_def by (intro continuous_on_cases) (auto intro: continuous_on_const continuous_on_inverse_ereal)
+ also have "{.. 0} \<union> {0::ereal ..} = UNIV"
+ by auto
+ finally show "continuous_on UNIV I" .
+ show "antimono I"
+ unfolding antimono_def I_def by (auto intro: ereal_inverse_antimono)
+ qed fact
+ also have "Liminf F (\<lambda>n. I (f n)) = Liminf F (\<lambda>n. inverse (f n))"
+ proof (rule Liminf_eq)
+ show "\<forall>\<^sub>F x in F. I (f x) = inverse (f x)"
+ using nneg by eventually_elim (auto simp: I_def)
+ qed
+ also have "0 \<le> Limsup F f"
+ by (intro le_Limsup) fact+
+ then have "I (Limsup F f) = inverse (Limsup F f)"
+ by (auto simp: I_def)
+ finally show ?thesis .
+qed
+
subsection \<open>monoset\<close>
definition (in order) mono_set:
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Sep 25 23:41:24 2015 +0200
@@ -7,6 +7,7 @@
theory Integration
imports
Derivative
+ Uniform_Limit
"~~/src/HOL/Library/Indicator_Function"
begin
@@ -11609,6 +11610,73 @@
qed auto
+subsection \<open>Exchange uniform limit and integral\<close>
+
+lemma
+ uniform_limit_integral:
+ fixes f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
+ assumes u: "uniform_limit (cbox a b) f g F"
+ assumes c: "\<And>n. continuous_on (cbox a b) (f n)"
+ assumes [simp]: "F \<noteq> bot"
+ obtains I J where
+ "\<And>n. (f n has_integral I n) (cbox a b)"
+ "(g has_integral J) (cbox a b)"
+ "(I ---> J) F"
+proof -
+ have fi[simp]: "f n integrable_on (cbox a b)" for n
+ by (auto intro!: integrable_continuous assms)
+ then obtain I where I: "\<And>n. (f n has_integral I n) (cbox a b)"
+ by atomize_elim (auto simp: integrable_on_def intro!: choice)
+
+ moreover
+
+ have gi[simp]: "g integrable_on (cbox a b)"
+ by (auto intro!: integrable_continuous uniform_limit_theorem[OF _ u] eventuallyI c)
+ then obtain J where J: "(g has_integral J) (cbox a b)"
+ by blast
+
+ moreover
+
+ have "(I ---> J) F"
+ proof cases
+ assume "content (cbox a b) = 0"
+ hence "I = (\<lambda>_. 0)" "J = 0"
+ by (auto intro!: has_integral_unique I J)
+ thus ?thesis by simp
+ next
+ assume content_nonzero: "content (cbox a b) \<noteq> 0"
+ show ?thesis
+ proof (rule tendstoI)
+ fix e::real
+ assume "e > 0"
+ def e' \<equiv> "e / 2"
+ with \<open>e > 0\<close> have "e' > 0" by simp
+ then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)"
+ using u content_nonzero content_pos_le[of a b]
+ by (auto simp: uniform_limit_iff dist_norm)
+ then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
+ proof eventually_elim
+ case (elim n)
+ have "I n = integral (cbox a b) (f n)"
+ "J = integral (cbox a b) g"
+ using I[of n] J by (simp_all add: integral_unique)
+ then have "dist (I n) J = norm (integral (cbox a b) (\<lambda>x. f n x - g x))"
+ by (simp add: integral_sub dist_norm)
+ also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))"
+ using elim
+ by (intro integral_norm_bound_integral)
+ (auto intro!: integrable_sub absolutely_integrable_onI)
+ also have "\<dots> < e"
+ using \<open>0 < e\<close>
+ by (simp add: e'_def)
+ finally show ?case .
+ qed
+ qed
+ qed
+ ultimately show ?thesis ..
+qed
+
+
subsection \<open>Dominated convergence\<close>
(* GENERALIZE the following theorems *)
--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy Fri Sep 25 23:41:24 2015 +0200
@@ -6,7 +6,6 @@
Ordered_Euclidean_Space
Complex_Analysis_Basics
Bounded_Continuous_Function
- Uniform_Limit
Weierstrass
begin
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Sep 25 23:41:24 2015 +0200
@@ -1551,6 +1551,43 @@
qed
qed
+lemma interior_Ici:
+ fixes x :: "'a :: {dense_linorder, linorder_topology}"
+ assumes "b < x"
+ shows "interior { x ..} = { x <..}"
+proof (rule interior_unique)
+ fix T assume "T \<subseteq> {x ..}" "open T"
+ moreover have "x \<notin> T"
+ proof
+ assume "x \<in> T"
+ obtain y where "y < x" "{y <.. x} \<subseteq> T"
+ using open_left[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>b < x\<close>] by auto
+ with dense[OF \<open>y < x\<close>] obtain z where "z \<in> T" "z < x"
+ by (auto simp: subset_eq Ball_def)
+ with \<open>T \<subseteq> {x ..}\<close> show False by auto
+ qed
+ ultimately show "T \<subseteq> {x <..}"
+ by (auto simp: subset_eq less_le)
+qed auto
+
+lemma interior_Iic:
+ fixes x :: "'a :: {dense_linorder, linorder_topology}"
+ assumes "x < b"
+ shows "interior {.. x} = {..< x}"
+proof (rule interior_unique)
+ fix T assume "T \<subseteq> {.. x}" "open T"
+ moreover have "x \<notin> T"
+ proof
+ assume "x \<in> T"
+ obtain y where "x < y" "{x ..< y} \<subseteq> T"
+ using open_right[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>x < b\<close>] by auto
+ with dense[OF \<open>x < y\<close>] obtain z where "z \<in> T" "x < z"
+ by (auto simp: subset_eq Ball_def less_le)
+ with \<open>T \<subseteq> {.. x}\<close> show False by auto
+ qed
+ ultimately show "T \<subseteq> {..< x}"
+ by (auto simp: subset_eq less_le)
+qed auto
subsection \<open>Closure of a Set\<close>
@@ -1763,10 +1800,6 @@
text \<open>Some property holds "sufficiently close" to the limit point.\<close>
-lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
- unfolding trivial_limit_def
- by (auto elim: eventually_rev_mp)
-
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
by simp
--- a/src/HOL/Product_Type.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Product_Type.thy Fri Sep 25 23:41:24 2015 +0200
@@ -311,6 +311,41 @@
The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
not @{text pttrn}.\<close>
+text \<open>print @{term "uncurry f"} as @{term "\<lambda>(x, y). f x y"} and
+ @{term "uncurry (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
+
+typed_print_translation \<open>
+ let
+ fun uncurry_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
+ | uncurry_guess_names_tr' T [Abs (x, xT, t)] =
+ (case (head_of t) of
+ Const (@{const_syntax uncurry}, _) => raise Match
+ | _ =>
+ let
+ val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+ val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+ end)
+ | uncurry_guess_names_tr' T [t] =
+ (case head_of t of
+ Const (@{const_syntax uncurry}, _) => raise Match
+ | _ =>
+ let
+ val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+ val (y, t') =
+ Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
+ val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
+ in
+ Syntax.const @{syntax_const "_abs"} $
+ (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+ end)
+ | uncurry_guess_names_tr' _ _ = raise Match;
+ in [(@{const_syntax uncurry}, K uncurry_guess_names_tr')] end
+\<close>
+
subsubsection \<open>Code generator setup\<close>
--- a/src/HOL/ROOT Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/ROOT Fri Sep 25 23:41:24 2015 +0200
@@ -176,6 +176,7 @@
theories
Tree_Set
Tree_Map
+ AVL_Map
RBT_Map
document_files "root.tex" "root.bib"
--- a/src/HOL/Tools/BNF/bnf_comp.ML Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Fri Sep 25 23:41:24 2015 +0200
@@ -325,13 +325,12 @@
fun rel_OO_Grp_tac ctxt =
let
val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
- val outer_rel_cong = rel_cong_of_bnf outer;
val thm =
(trans OF [in_alt_thm RS @{thm OO_Grp_cong},
trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
[trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
- trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
+ trans OF [rel_OO_of_bnf outer RS sym, rel_cong0_of_bnf outer OF
(map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym);
in
unfold_thms_tac ctxt set'_eq_sets THEN rtac ctxt thm 1
@@ -441,7 +440,7 @@
trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
[trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
rel_conversep_of_bnf bnf RS sym], rel_Grp],
- trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+ trans OF [rel_OO_of_bnf bnf RS sym, rel_cong0_of_bnf bnf OF
(replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
replicate (live - n) @{thm Grp_fst_snd})]]] RS sym);
in
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 25 23:41:24 2015 +0200
@@ -76,12 +76,18 @@
val rel_Grp_of_bnf: bnf -> thm
val rel_OO_of_bnf: bnf -> thm
val rel_OO_Grp_of_bnf: bnf -> thm
+ val rel_cong0_of_bnf: bnf -> thm
val rel_cong_of_bnf: bnf -> thm
+ val rel_cong_simp_of_bnf: bnf -> thm
val rel_conversep_of_bnf: bnf -> thm
val rel_mono_of_bnf: bnf -> thm
val rel_mono_strong0_of_bnf: bnf -> thm
val rel_mono_strong_of_bnf: bnf -> thm
val rel_refl_of_bnf: bnf -> thm
+ val rel_refl_strong_of_bnf: bnf -> thm
+ val rel_reflp_of_bnf: bnf -> thm
+ val rel_symp_of_bnf: bnf -> thm
+ val rel_transp_of_bnf: bnf -> thm
val rel_map_of_bnf: bnf -> thm list
val rel_transfer_of_bnf: bnf -> thm
val rel_eq_of_bnf: bnf -> thm
@@ -244,7 +250,9 @@
rel_eq: thm lazy,
rel_flip: thm lazy,
set_map: thm lazy list,
+ rel_cong0: thm lazy,
rel_cong: thm lazy,
+ rel_cong_simp: thm lazy,
rel_map: thm list lazy,
rel_mono: thm lazy,
rel_mono_strong0: thm lazy,
@@ -254,13 +262,18 @@
rel_conversep: thm lazy,
rel_OO: thm lazy,
rel_refl: thm lazy,
+ rel_refl_strong: thm lazy,
+ rel_reflp: thm lazy,
+ rel_symp: thm lazy,
+ rel_transp: thm lazy,
rel_transfer: thm lazy
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
- inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident
- map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong
- set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer = {
+ inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident map_transfer
+ rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0
+ rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp
+ rel_symp rel_transp rel_transfer = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -281,7 +294,9 @@
rel_eq = rel_eq,
rel_flip = rel_flip,
set_map = set_map,
+ rel_cong0 = rel_cong0,
rel_cong = rel_cong,
+ rel_cong_simp = rel_cong_simp,
rel_map = rel_map,
rel_mono = rel_mono,
rel_mono_strong0 = rel_mono_strong0,
@@ -291,6 +306,10 @@
rel_conversep = rel_conversep,
rel_OO = rel_OO,
rel_refl = rel_refl,
+ rel_refl_strong = rel_refl_strong,
+ rel_reflp = rel_reflp,
+ rel_symp = rel_symp,
+ rel_transp = rel_transp,
set_transfer = set_transfer};
fun map_facts f {
@@ -314,7 +333,9 @@
rel_eq,
rel_flip,
set_map,
+ rel_cong0,
rel_cong,
+ rel_cong_simp,
rel_map,
rel_mono,
rel_mono_strong0,
@@ -324,6 +345,10 @@
rel_conversep,
rel_OO,
rel_refl,
+ rel_refl_strong,
+ rel_reflp,
+ rel_symp,
+ rel_transp,
set_transfer} =
{bd_Card_order = f bd_Card_order,
bd_Cinfinite = f bd_Cinfinite,
@@ -345,7 +370,9 @@
rel_eq = Lazy.map f rel_eq,
rel_flip = Lazy.map f rel_flip,
set_map = map (Lazy.map f) set_map,
+ rel_cong0 = Lazy.map f rel_cong0,
rel_cong = Lazy.map f rel_cong,
+ rel_cong_simp = Lazy.map f rel_cong_simp,
rel_map = Lazy.map (map f) rel_map,
rel_mono = Lazy.map f rel_mono,
rel_mono_strong0 = Lazy.map f rel_mono_strong0,
@@ -355,6 +382,10 @@
rel_conversep = Lazy.map f rel_conversep,
rel_OO = Lazy.map f rel_OO,
rel_refl = Lazy.map f rel_refl,
+ rel_refl_strong = Lazy.map f rel_refl_strong,
+ rel_reflp = Lazy.map f rel_reflp,
+ rel_symp = Lazy.map f rel_symp,
+ rel_transp = Lazy.map f rel_transp,
set_transfer = Lazy.map (map f) set_transfer};
val morph_facts = map_facts o Morphism.thm;
@@ -482,11 +513,17 @@
val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
val set_transfer_of_bnf = Lazy.force o #set_transfer o #facts o rep_bnf;
+val rel_cong0_of_bnf = Lazy.force o #rel_cong0 o #facts o rep_bnf;
val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
+val rel_cong_simp_of_bnf = Lazy.force o #rel_cong_simp o #facts o rep_bnf;
val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf;
+val rel_refl_strong_of_bnf = Lazy.force o #rel_refl_strong o #facts o rep_bnf;
+val rel_reflp_of_bnf = Lazy.force o #rel_reflp o #facts o rep_bnf;
+val rel_symp_of_bnf = Lazy.force o #rel_symp o #facts o rep_bnf;
+val rel_transp_of_bnf = Lazy.force o #rel_transp o #facts o rep_bnf;
val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf;
val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
@@ -670,7 +707,13 @@
val rel_monoN = "rel_mono";
val rel_mono_strong0N = "rel_mono_strong0";
val rel_mono_strongN = "rel_mono_strong";
+val rel_congN = "rel_cong";
+val rel_cong_simpN = "rel_cong_simp";
val rel_reflN = "rel_refl";
+val rel_refl_strongN = "rel_refl_strong";
+val rel_reflpN = "rel_reflp";
+val rel_sympN = "rel_symp";
+val rel_transpN = "rel_transp";
val rel_transferN = "rel_transfer";
val rel_comppN = "rel_compp";
val rel_compp_GrpN = "rel_compp_Grp";
@@ -742,7 +785,13 @@
(rel_mapN, Lazy.force (#rel_map facts), []),
(rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
(rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []),
+ (rel_congN, [Lazy.force (#rel_cong facts)], fundefcong_attrs),
+ (rel_cong_simpN, [Lazy.force (#rel_cong_simp facts)], []),
(rel_reflN, [Lazy.force (#rel_refl facts)], []),
+ (rel_refl_strongN, [Lazy.force (#rel_refl_strong facts)], []),
+ (rel_reflpN, [Lazy.force (#rel_reflp facts)], []),
+ (rel_sympN, [Lazy.force (#rel_symp facts)], []),
+ (rel_transpN, [Lazy.force (#rel_transp facts)], []),
(rel_transferN, [Lazy.force (#rel_transfer facts)], []),
(set_mapN, map Lazy.force (#set_map facts), []),
(set_transferN, Lazy.force (#set_transfer facts), [])]
@@ -784,7 +833,7 @@
let
val live = length set_rhss;
- val def_qualify = Binding.concealed o Binding.qualify false (Binding.name_of bnf_b);
+ val def_qualify = Binding.qualify false (Binding.name_of bnf_b);
fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
@@ -804,7 +853,7 @@
let val b = b () in
apfst (apsnd snd)
((if internal then Local_Theory.define_internal else Local_Theory.define)
- ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy)
+ ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), rhs)) lthy)
end
end;
@@ -1033,7 +1082,7 @@
fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
val pre_names_lthy = lthy;
- val ((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), zs), zs'), ys), As),
+ val (((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), y'), zs), zs'), ys), As),
As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), S_BsEs),
transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
|> mk_Frees "f" (map2 (curry op -->) As' Bs')
@@ -1044,6 +1093,7 @@
||>> yield_singleton (mk_Frees "x") CA'
||>> yield_singleton (mk_Frees "x") CA'
||>> yield_singleton (mk_Frees "y") CB'
+ ||>> yield_singleton (mk_Frees "y") CB'
||>> mk_Frees "z" As'
||>> mk_Frees "z" As'
||>> mk_Frees "y" Bs'
@@ -1060,7 +1110,8 @@
||>> mk_Frees "S" transfer_ranRTs;
val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs;
- val x_copy = retype_const_or_free CA' y;
+ val x_copy = retype_const_or_free CA' y';
+ val y_copy = retype_const_or_free CB' x';
val rel = mk_bnf_rel pred2RTs CA' CB';
val relCsEs = mk_bnf_rel pred2RTsCsEs CC' CE';
@@ -1289,7 +1340,7 @@
val rel_Grp = Lazy.lazy mk_rel_Grp;
- fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
+ fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy;
fun mk_rel_concl f = HOLogic.mk_Trueprop
(f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
@@ -1305,7 +1356,7 @@
|> Thm.close_derivation
end;
- fun mk_rel_cong () =
+ fun mk_rel_cong0 () =
let
val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
val cong_concl = mk_rel_concl HOLogic.mk_eq;
@@ -1317,14 +1368,14 @@
end;
val rel_mono = Lazy.lazy mk_rel_mono;
- val rel_cong = Lazy.lazy mk_rel_cong;
+ val rel_cong0 = Lazy.lazy mk_rel_cong0;
fun mk_rel_eq () =
Goal.prove_sorry lthy [] []
(mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
HOLogic.eq_const CA'))
(fn {context = ctxt, prems = _} =>
- mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms))
+ mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong0) (#map_id0 axioms))
|> Thm.close_derivation;
val rel_eq = Lazy.lazy mk_rel_eq;
@@ -1400,6 +1451,30 @@
val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
+ fun mk_rel_cong_prem mk_implies x x' z z' set set' R R_copy =
+ Logic.all z (Logic.all z'
+ (mk_implies (mk_Trueprop_mem (z, set $ x), mk_implies (mk_Trueprop_mem (z', set' $ x'),
+ mk_Trueprop_eq (R $ z $ z', R_copy $ z $ z')))));
+
+ fun mk_rel_cong mk_implies () =
+ let
+ val prem0 = mk_Trueprop_eq (x, x_copy);
+ val prem1 = mk_Trueprop_eq (y, y_copy);
+ val prems = @{map 6} (mk_rel_cong_prem mk_implies x_copy y_copy)
+ zs ys bnf_sets_As bnf_sets_Bs Rs Rs_copy;
+ val eq = mk_Trueprop_eq (Term.list_comb (rel, Rs) $ x $ y,
+ Term.list_comb (rel, Rs_copy) $ x_copy $ y_copy);
+ in
+ Goal.prove_sorry lthy [] (prem0 :: prem1 :: prems) eq
+ (fn {context = ctxt, prems} =>
+ mk_rel_cong_tac ctxt (chop 2 prems) (Lazy.force rel_mono_strong))
+ |> Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
+ end;
+
+ val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies);
+ val rel_cong_simp = Lazy.lazy (mk_rel_cong (fn (a, b) => @{term simp_implies} $ a $ b));
+
fun mk_rel_map () =
let
fun mk_goal lhs rhs =
@@ -1432,6 +1507,33 @@
val rel_refl = Lazy.lazy mk_rel_refl;
+ fun mk_rel_refl_strong () =
+ (rule_by_tactic lthy (ALLGOALS (Object_Logic.full_atomize_tac lthy))
+ ((Lazy.force rel_eq RS @{thm predicate2_eqD}) RS @{thm iffD2[OF _ refl]} RS
+ Lazy.force rel_mono_strong)) OF
+ (replicate live @{thm diag_imp_eq_le})
+
+ val rel_refl_strong = Lazy.lazy mk_rel_refl_strong;
+
+ fun mk_rel_preserves mk_prop prop_conv_thm thm () =
+ let
+ val Rs = map2 retype_const_or_free self_pred2RTs Rs;
+ val prems = map (HOLogic.mk_Trueprop o mk_prop) Rs;
+ val goal = HOLogic.mk_Trueprop (mk_prop (Term.list_comb (relAsAs, Rs)));
+ in
+ Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+ (fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt [prop_conv_thm] THEN
+ HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans})
+ THEN' rtac ctxt (Lazy.force rel_mono) THEN_ALL_NEW assume_tac ctxt))
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation
+ end;
+
+ val rel_reflp = Lazy.lazy (mk_rel_preserves mk_reflp @{thm reflp_eq} rel_eq);
+ val rel_symp = Lazy.lazy (mk_rel_preserves mk_symp @{thm symp_conversep} rel_conversep);
+ val rel_transp = Lazy.lazy (mk_rel_preserves mk_transp @{thm transp_relcompp} rel_OO);
+
fun mk_map_transfer () =
let
val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
@@ -1519,8 +1621,9 @@
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0
- map_ident map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
- rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_transfer;
+ map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map
+ rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO
+ rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer;
val wits = map2 mk_witness bnf_wits wit_thms;
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Fri Sep 25 23:41:24 2015 +0200
@@ -28,6 +28,7 @@
val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic
val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic
val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
@@ -356,4 +357,15 @@
REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps);
+fun mk_rel_cong_tac ctxt (eqs, prems) mono =
+ let
+ fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt;
+ fun mk_tacs iffD = etac ctxt mono ::
+ map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD)
+ |> Drule.rotate_prems ~1 |> mk_tac) prems;
+ in
+ unfold_thms_tac ctxt eqs THEN
+ HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2))
+ end;
+
end;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 25 23:41:24 2015 +0200
@@ -219,7 +219,7 @@
val map_ids = map map_id_of_bnf bnfs;
val set_bdss = map set_bd_of_bnf bnfs;
val set_mapss = map set_map_of_bnf bnfs;
- val rel_congs = map rel_cong_of_bnf bnfs;
+ val rel_congs = map rel_cong0_of_bnf bnfs;
val rel_converseps = map rel_conversep_of_bnf bnfs;
val rel_Grps = map rel_Grp_of_bnf bnfs;
val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
--- a/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 25 23:41:24 2015 +0200
@@ -61,6 +61,9 @@
val mk_rel_comp: term * term -> term
val mk_rel_compp: term * term -> term
val mk_vimage2p: term -> term -> term
+ val mk_reflp: term -> term
+ val mk_symp: term -> term
+ val mk_transp: term -> term
(*parameterized terms*)
val mk_nthN: int -> term -> int -> term
@@ -348,6 +351,12 @@
(T1 --> T2) --> (U1 --> U2) --> mk_pred2T T2 U2 --> mk_pred2T T1 U1) $ f $ g
end;
+fun mk_pred name R =
+ Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
+val mk_reflp = mk_pred @{const_name reflp};
+val mk_symp = mk_pred @{const_name symp};
+val mk_transp = mk_pred @{const_name transp};
+
fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
fun mk_sym thm = thm RS sym;
--- a/src/HOL/Topological_Spaces.thy Fri Sep 25 23:39:08 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Fri Sep 25 23:41:24 2015 +0200
@@ -377,6 +377,21 @@
lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
+lemma at_within_open_NO_MATCH:
+ "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
+ by (simp only: at_within_open)
+
+lemma at_within_nhd:
+ assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
+ shows "at x within T = at x within U"
+ unfolding filter_eq_iff eventually_at_filter
+proof (intro allI eventually_subst)
+ have "eventually (\<lambda>x. x \<in> S) (nhds x)"
+ using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
+ then show "\<forall>\<^sub>F n in nhds x. (n \<noteq> x \<longrightarrow> n \<in> T \<longrightarrow> P n) = (n \<noteq> x \<longrightarrow> n \<in> U \<longrightarrow> P n)" for P
+ by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
+qed
+
lemma at_within_empty [simp]: "at a within {} = bot"
unfolding at_within_def by simp
@@ -1570,7 +1585,7 @@
"continuous (at (x::'a::linorder_topology)) f = (continuous (at_left x) f \<and> continuous (at_right x) f)"
by (simp add: continuous_within filterlim_at_split)
-subsubsection\<open>Open-cover compactness\<close>
+subsubsection \<open>Open-cover compactness\<close>
context topological_space
begin