--- a/CONTRIBUTORS Sat Jun 01 11:29:59 2019 +0200
+++ b/CONTRIBUTORS Sat Jun 01 13:53:23 2019 +0200
@@ -3,6 +3,10 @@
listed as an author in one of the source files of this Isabelle distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
+
Contributions to Isabelle2019
-----------------------------
--- a/NEWS Sat Jun 01 11:29:59 2019 +0200
+++ b/NEWS Sat Jun 01 13:53:23 2019 +0200
@@ -4,6 +4,10 @@
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
+New in this Isabelle version
+----------------------------
+
+
New in Isabelle2019 (June 2019)
-------------------------------
--- a/src/Doc/Functions/Functions.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/Doc/Functions/Functions.thy Sat Jun 01 13:53:23 2019 +0200
@@ -347,6 +347,15 @@
method a bit stronger: it can then use multiset orders internally.
\<close>
+subsection \<open>Configuring simplification rules for termination proofs\<close>
+
+text \<open>
+ Since both \<open>lexicographic_order\<close> and \<open>size_change\<close> rely on the simplifier internally,
+ there can sometimes be the need for adding additional simp rules to them.
+ This can be done either as arguments to the methods themselves, or globally via the
+ theorem attribute \<open>termination_simp\<close>, which is useful in rare cases.
+\<close>
+
section \<open>Mutual Recursion\<close>
text \<open>
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sat Jun 01 13:53:23 2019 +0200
@@ -489,6 +489,7 @@
@{method_def (HOL) relation} & : & \<open>method\<close> \\
@{method_def (HOL) lexicographic_order} & : & \<open>method\<close> \\
@{method_def (HOL) size_change} & : & \<open>method\<close> \\
+ @{attribute_def (HOL) termination_simp} & : & \<open>attribute\<close> \\
@{method_def (HOL) induction_schema} & : & \<open>method\<close> \\
\end{matharray}
@@ -535,6 +536,10 @@
For local descent proofs, the @{syntax clasimpmod} modifiers are accepted
(as for @{method auto}).
+ \<^descr> @{attribute (HOL) termination_simp} declares extra rules for the
+ simplifier, when invoked in termination proofs. This can be useful, e.g.,
+ for special rules involving size estimations.
+
\<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
from well-founded induction and completeness of patterns. This factors out
some operations that are done internally by the function package and makes
--- a/src/HOL/Analysis/Bochner_Integration.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Sat Jun 01 13:53:23 2019 +0200
@@ -1932,6 +1932,24 @@
integral\<^sup>L M f \<le> integral\<^sup>L M g"
by (intro integral_mono_AE) auto
+lemma integral_norm_bound_integral:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach,second_countable_topology}"
+ assumes "integrable M f" "integrable M g" "\<And>x. x \<in> space M \<Longrightarrow> norm(f x) \<le> g x"
+ shows "norm (\<integral>x. f x \<partial>M) \<le> (\<integral>x. g x \<partial>M)"
+proof -
+ have "norm (\<integral>x. f x \<partial>M) \<le> (\<integral>x. norm (f x) \<partial>M)"
+ by (rule integral_norm_bound)
+ also have "... \<le> (\<integral>x. g x \<partial>M)"
+ using assms integrable_norm integral_mono by blast
+ finally show ?thesis .
+qed
+
+lemma integral_abs_bound_integral:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes "integrable M f" "integrable M g" "\<And>x. x \<in> space M \<Longrightarrow> \<bar>f x\<bar> \<le> g x"
+ shows "\<bar>\<integral>x. f x \<partial>M\<bar> \<le> (\<integral>x. g x \<partial>M)"
+ by (metis integral_norm_bound_integral assms real_norm_def)
+
text \<open>The next two statements are useful to bound Lebesgue integrals, as they avoid one
integrability assumption. The price to pay is that the upper function has to be nonnegative,
but this is often true and easy to check in computations.\<close>
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Jun 01 13:53:23 2019 +0200
@@ -3119,12 +3119,29 @@
using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
qed (use le in \<open>force intro!: always_eventually split: split_indicator\<close>)
+corollary absolutely_integrable_on_const [simp]:
+ fixes c :: "'a::euclidean_space"
+ assumes "S \<in> lmeasurable"
+ shows "(\<lambda>x. c) absolutely_integrable_on S"
+ by (metis (full_types) assms absolutely_integrable_integrable_bound integrable_on_const order_refl)
+
lemma absolutely_integrable_continuous:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "continuous_on (cbox a b) f \<Longrightarrow> f absolutely_integrable_on cbox a b"
using absolutely_integrable_integrable_bound
by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)
+lemma continous_imp_integrable:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "continuous_on (cbox a b) f"
+ shows "integrable (lebesgue_on (cbox a b)) f"
+proof -
+ have "f absolutely_integrable_on cbox a b"
+ by (simp add: absolutely_integrable_continuous assms)
+ then show ?thesis
+ by (simp add: integrable_restrict_space set_integrable_def)
+qed
+
subsection \<open>Componentwise\<close>
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Sat Jun 01 13:53:23 2019 +0200
@@ -304,15 +304,10 @@
qed (auto simp: Ioc_inj mono_F)
lemma measure_interval_measure_Ioc:
- assumes "a \<le> b"
- assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
- assumes right_cont_F : "\<And>a. continuous (at_right a) F"
+ assumes "a \<le> b" and "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y" and "\<And>a. continuous (at_right a) F"
shows "measure (interval_measure F) {a <.. b} = F b - F a"
unfolding measure_def
- apply (subst emeasure_interval_measure_Ioc)
- apply fact+
- apply (simp add: assms)
- done
+ by (simp add: assms emeasure_interval_measure_Ioc)
lemma emeasure_interval_measure_Ioc_eq:
"(\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow>
@@ -409,6 +404,11 @@
shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
+lemma integrable_lebesgue_on_UNIV_eq:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
+ shows "integrable (lebesgue_on UNIV) f = integrable lebesgue f"
+ by (auto simp: integrable_restrict_space)
+
text\<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
lemma continuous_imp_measurable_on_sets_lebesgue:
--- a/src/HOL/Data_Structures/Sorting.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy Sat Jun 01 13:53:23 2019 +0200
@@ -242,7 +242,7 @@
qed
qed
-(* Beware of conversions: *)
+(* Beware of implicit conversions: *)
lemma c_msort_log: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)"
using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps)
by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
@@ -250,7 +250,6 @@
subsection "Bottom-Up Merge Sort"
-(* Exercise: make tail recursive *)
fun merge_adj :: "('a::linorder) list list \<Rightarrow> 'a list list" where
"merge_adj [] = []" |
"merge_adj [xs] = [xs]" |
--- a/src/HOL/Data_Structures/Tree23.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Data_Structures/Tree23.thy Sat Jun 01 13:53:23 2019 +0200
@@ -34,13 +34,13 @@
text \<open>Balanced:\<close>
-fun bal :: "'a tree23 \<Rightarrow> bool" where
-"bal Leaf = True" |
-"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
-"bal (Node3 l _ m _ r) =
- (bal l & bal m & bal r & height l = height m & height m = height r)"
+fun complete :: "'a tree23 \<Rightarrow> bool" where
+"complete Leaf = True" |
+"complete (Node2 l _ r) = (complete l & complete r & height l = height r)" |
+"complete (Node3 l _ m _ r) =
+ (complete l & complete m & complete r & height l = height m & height m = height r)"
-lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
+lemma ht_sz_if_complete: "complete t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
by (induction t) auto
end
--- a/src/HOL/Data_Structures/Tree23_Map.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Data_Structures/Tree23_Map.thy Sat Jun 01 13:53:23 2019 +0200
@@ -22,37 +22,37 @@
EQ \<Rightarrow> Some b2 |
GT \<Rightarrow> lookup r x))"
-fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
-"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
+fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) upI" where
+"upd x y Leaf = OF Leaf (x,y) Leaf" |
"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
LT \<Rightarrow> (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)) |
- EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
+ TI l' => TI (Node2 l' ab r)
+ | OF l1 ab' l2 => TI (Node3 l1 ab' l2 ab r)) |
+ EQ \<Rightarrow> TI (Node2 l (x,y) r) |
GT \<Rightarrow> (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)))" |
+ TI r' => TI (Node2 l ab r')
+ | OF r1 ab' r2 => TI (Node3 l ab r1 ab' r2)))" |
"upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
LT \<Rightarrow> (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)) |
- EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
+ TI l' => TI (Node3 l' ab1 m ab2 r)
+ | OF l1 ab' l2 => OF (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) |
+ EQ \<Rightarrow> TI (Node3 l (x,y) m ab2 r) |
GT \<Rightarrow> (case cmp x (fst ab2) of
LT \<Rightarrow> (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)) |
- EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
+ TI m' => TI (Node3 l ab1 m' ab2 r)
+ | OF m1 ab' m2 => OF (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) |
+ EQ \<Rightarrow> TI (Node3 l ab1 m (x,y) r) |
GT \<Rightarrow> (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))))"
+ TI r' => TI (Node3 l ab1 m ab2 r')
+ | OF r1 ab' r2 => OF (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)"
+"update a b t = treeI(upd a b t)"
-fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
-"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
+fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) upD" where
+"del x Leaf = TD Leaf" |
+"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then UF Leaf else TD(Node2 Leaf ab1 Leaf))" |
+"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = TD(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) = (case cmp x (fst ab1) of
LT \<Rightarrow> node21 (del x l) ab1 r |
@@ -67,7 +67,7 @@
GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
-"delete x t = tree\<^sub>d(del x t)"
+"delete x t = treeD(del x t)"
subsection \<open>Functional Correctness\<close>
@@ -78,50 +78,50 @@
lemma inorder_upd:
- "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)"
-by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
+ "sorted1(inorder t) \<Longrightarrow> inorder(treeI(upd x y t)) = upd_list x y (inorder t)"
+by(induction t) (auto simp: upd_list_simps split: upI.splits)
corollary inorder_update:
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
by(simp add: update_def inorder_upd)
-lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
- inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
+lemma inorder_del: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+ inorder(treeD (del x t)) = del_list x (inorder t)"
by(induction t rule: del.induct)
(auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
-corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
+corollary inorder_delete: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
by(simp add: delete_def inorder_del)
subsection \<open>Balancedness\<close>
-lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
-by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *)
+lemma complete_upd: "complete t \<Longrightarrow> complete (treeI(upd x y t)) \<and> height(upd x y t) = height t"
+by (induct t) (auto split!: if_split upI.split)(* 16 secs in 2015 *)
-corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)"
-by (simp add: update_def bal_upd)
+corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)"
+by (simp add: update_def complete_upd)
-lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
by(induction x t rule: del.induct)
(auto simp add: heights max_def height_split_min split: prod.split)
-lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
+lemma complete_treeD_del: "complete t \<Longrightarrow> complete(treeD(del x t))"
by(induction x t rule: del.induct)
- (auto simp: bals bal_split_min height_del height_split_min split: prod.split)
+ (auto simp: completes complete_split_min height_del height_split_min split: prod.split)
-corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
-by(simp add: delete_def bal_tree\<^sub>d_del)
+corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)"
+by(simp add: delete_def complete_treeD_del)
subsection \<open>Overall Correctness\<close>
interpretation M: Map_by_Ordered
where empty = empty and lookup = lookup and update = update and delete = delete
-and inorder = inorder and inv = bal
+and inorder = inorder and inv = complete
proof (standard, goal_cases)
case 1 thus ?case by(simp add: empty_def)
next
@@ -133,9 +133,9 @@
next
case 5 thus ?case by(simp add: empty_def)
next
- case 6 thus ?case by(simp add: bal_update)
+ case 6 thus ?case by(simp add: complete_update)
next
- case 7 thus ?case by(simp add: bal_delete)
+ case 7 thus ?case by(simp add: complete_delete)
qed
end
--- a/src/HOL/Data_Structures/Tree23_Set.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Sat Jun 01 13:53:23 2019 +0200
@@ -31,104 +31,104 @@
EQ \<Rightarrow> True |
GT \<Rightarrow> isin r x))"
-datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
+datatype 'a upI = TI "'a tree23" | OF "'a tree23" 'a "'a tree23"
-fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
-"tree\<^sub>i (T\<^sub>i t) = t" |
-"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
+fun treeI :: "'a upI \<Rightarrow> 'a tree23" where
+"treeI (TI t) = t" |
+"treeI (OF l a r) = Node2 l a r"
-fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
-"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
+fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a upI" where
+"ins x Leaf = OF Leaf x Leaf" |
"ins x (Node2 l a r) =
(case cmp x a of
LT \<Rightarrow>
(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)) |
- EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
+ TI l' => TI (Node2 l' a r) |
+ OF l1 b l2 => TI (Node3 l1 b l2 a r)) |
+ EQ \<Rightarrow> TI (Node2 l x r) |
GT \<Rightarrow>
(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)))" |
+ TI r' => TI (Node2 l a r') |
+ OF r1 b r2 => TI (Node3 l a r1 b r2)))" |
"ins x (Node3 l a m b r) =
(case cmp x a of
LT \<Rightarrow>
(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)) |
- EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
+ TI l' => TI (Node3 l' a m b r) |
+ OF l1 c l2 => OF (Node2 l1 c l2) a (Node2 m b r)) |
+ EQ \<Rightarrow> TI (Node3 l a m b r) |
GT \<Rightarrow>
(case cmp x b of
GT \<Rightarrow>
(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)) |
- EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
+ TI r' => TI (Node3 l a m b r') |
+ OF r1 c r2 => OF (Node2 l a m) b (Node2 r1 c r2)) |
+ EQ \<Rightarrow> TI (Node3 l a m b r) |
LT \<Rightarrow>
(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))))"
+ TI m' => TI (Node3 l a m' b r) |
+ OF m1 c m2 => OF (Node2 l a m1) c (Node2 m2 b r))))"
hide_const insert
definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
-"insert x t = tree\<^sub>i(ins x t)"
+"insert x t = treeI(ins x t)"
-datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
+datatype 'a upD = TD "'a tree23" | UF "'a tree23"
-fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
-"tree\<^sub>d (T\<^sub>d t) = t" |
-"tree\<^sub>d (Up\<^sub>d t) = t"
+fun treeD :: "'a upD \<Rightarrow> 'a tree23" where
+"treeD (TD t) = t" |
+"treeD (UF t) = t"
(* Variation: return None to signal no-change *)
-fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
-"node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" |
-"node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" |
-"node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
+fun node21 :: "'a upD \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
+"node21 (TD t1) a t2 = TD(Node2 t1 a t2)" |
+"node21 (UF t1) a (Node2 t2 b t3) = UF(Node3 t1 a t2 b t3)" |
+"node21 (UF t1) a (Node3 t2 b t3 c t4) = TD(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
-fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
-"node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" |
-"node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" |
-"node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
+fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a upD \<Rightarrow> 'a upD" where
+"node22 t1 a (TD t2) = TD(Node2 t1 a t2)" |
+"node22 (Node2 t1 b t2) a (UF t3) = UF(Node3 t1 b t2 a t3)" |
+"node22 (Node3 t1 b t2 c t3) a (UF t4) = TD(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
-fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
-"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
-"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
-"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"
+fun node31 :: "'a upD \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
+"node31 (TD t1) a t2 b t3 = TD(Node3 t1 a t2 b t3)" |
+"node31 (UF t1) a (Node2 t2 b t3) c t4 = TD(Node2 (Node3 t1 a t2 b t3) c t4)" |
+"node31 (UF t1) a (Node3 t2 b t3 c t4) d t5 = TD(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"
-fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
-"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
-"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
-"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
+fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a upD \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
+"node32 t1 a (TD t2) b t3 = TD(Node3 t1 a t2 b t3)" |
+"node32 t1 a (UF t2) b (Node2 t3 c t4) = TD(Node2 t1 a (Node3 t2 b t3 c t4))" |
+"node32 t1 a (UF t2) b (Node3 t3 c t4 d t5) = TD(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
-fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
-"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
-"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
-"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
+fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a upD \<Rightarrow> 'a upD" where
+"node33 l a m b (TD r) = TD(Node3 l a m b r)" |
+"node33 t1 a (Node2 t2 b t3) c (UF t4) = TD(Node2 t1 a (Node3 t2 b t3 c t4))" |
+"node33 t1 a (Node3 t2 b t3 c t4) d (UF t5) = TD(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
-fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
-"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
-"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
+fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a upD" where
+"split_min (Node2 Leaf a Leaf) = (a, UF Leaf)" |
+"split_min (Node3 Leaf a Leaf b Leaf) = (a, TD(Node2 Leaf b Leaf))" |
"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
text \<open>In the base cases of \<open>split_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
in which case balancedness implies that so are the others. Exercise.\<close>
-fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
-"del x Leaf = T\<^sub>d Leaf" |
+fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
+"del x Leaf = TD Leaf" |
"del x (Node2 Leaf a Leaf) =
- (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
+ (if x = a then UF Leaf else TD(Node2 Leaf a Leaf))" |
"del x (Node3 Leaf a Leaf b Leaf) =
- T\<^sub>d(if x = a then Node2 Leaf b Leaf else
+ TD(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) =
(case cmp x a of
LT \<Rightarrow> node21 (del x l) a r |
GT \<Rightarrow> node22 l a (del x r) |
- EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
+ EQ \<Rightarrow> let (a',r') = split_min r in node22 l a' r')" |
"del x (Node3 l a m b r) =
(case cmp x a of
LT \<Rightarrow> node31 (del x l) a m b r |
@@ -140,7 +140,7 @@
GT \<Rightarrow> node33 l a m b (del x r)))"
definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
-"delete x t = tree\<^sub>d(del x t)"
+"delete x t = treeD(del x t)"
subsection "Functional Correctness"
@@ -154,8 +154,8 @@
subsubsection "Proofs for insert"
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)
+ "sorted(inorder t) \<Longrightarrow> inorder(treeI(ins x t)) = ins_list x (inorder t)"
+by(induction t) (auto simp: ins_list_simps split: upI.splits)
lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
@@ -165,40 +165,40 @@
subsubsection "Proofs for delete"
lemma inorder_node21: "height r > 0 \<Longrightarrow>
- inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
+ inorder (treeD (node21 l' a r)) = inorder (treeD l') @ a # inorder r"
by(induct l' a r rule: node21.induct) auto
lemma inorder_node22: "height l > 0 \<Longrightarrow>
- inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
+ inorder (treeD (node22 l a r')) = inorder l @ a # inorder (treeD r')"
by(induct l a r' rule: node22.induct) auto
lemma inorder_node31: "height m > 0 \<Longrightarrow>
- inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
+ inorder (treeD (node31 l' a m b r)) = inorder (treeD l') @ a # inorder m @ b # inorder r"
by(induct l' a m b r rule: node31.induct) auto
lemma inorder_node32: "height r > 0 \<Longrightarrow>
- inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
+ inorder (treeD (node32 l a m' b r)) = inorder l @ a # inorder (treeD m') @ b # inorder r"
by(induct l a m' b r rule: node32.induct) auto
lemma inorder_node33: "height m > 0 \<Longrightarrow>
- inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
+ inorder (treeD (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (treeD r')"
by(induct l a m b r' rule: node33.induct) auto
lemmas inorder_nodes = inorder_node21 inorder_node22
inorder_node31 inorder_node32 inorder_node33
lemma split_minD:
- "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
- x # inorder(tree\<^sub>d t') = inorder t"
+ "split_min t = (x,t') \<Longrightarrow> complete t \<Longrightarrow> height t > 0 \<Longrightarrow>
+ x # inorder(treeD t') = inorder t"
by(induction t arbitrary: t' rule: split_min.induct)
(auto simp: inorder_nodes split: prod.splits)
-lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
- inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
+lemma inorder_del: "\<lbrakk> complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+ inorder(treeD (del x t)) = del_list x (inorder t)"
by(induction t rule: del.induct)
(auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
-lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
+lemma inorder_delete: "\<lbrakk> complete t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
inorder(delete x t) = del_list x (inorder t)"
by(simp add: delete_def inorder_del)
@@ -208,21 +208,21 @@
subsubsection "Proofs for insert"
-text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>bal\<close>.\<close>
+text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>complete\<close>.\<close>
-instantiation up\<^sub>i :: (type)height
+instantiation upI :: (type)height
begin
-fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
-"height (T\<^sub>i t) = height t" |
-"height (Up\<^sub>i l a r) = height l"
+fun height_upI :: "'a upI \<Rightarrow> nat" where
+"height (TI t) = height t" |
+"height (OF l a r) = height l"
instance ..
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!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
+lemma complete_ins: "complete t \<Longrightarrow> complete (treeI(ins a t)) \<and> height(ins a t) = height t"
+by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *)
text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
two properties (balance and height) are combined in one predicate.\<close>
@@ -257,30 +257,30 @@
lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
by (induct set: full, simp_all)
-lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
+lemma full_imp_complete: "full n t \<Longrightarrow> complete t"
by (induct set: full, auto dest: full_imp_height)
-lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
+lemma complete_imp_full: "complete t \<Longrightarrow> full (height t) t"
by (induct t, simp_all)
-lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
- by (auto elim!: bal_imp_full full_imp_bal)
+lemma complete_iff_full: "complete t \<longleftrightarrow> (\<exists>n. full n t)"
+ by (auto elim!: complete_imp_full full_imp_complete)
text \<open>The \<^const>\<open>insert\<close> function either preserves the height of the
-tree, or increases it by one. The constructor returned by the \<^term>\<open>insert\<close> function determines which: A return value of the form \<^term>\<open>T\<^sub>i t\<close> indicates that the height will be the same. A value of the
-form \<^term>\<open>Up\<^sub>i l p r\<close> indicates an increase in height.\<close>
+tree, or increases it by one. The constructor returned by the \<^term>\<open>insert\<close> function determines which: A return value of the form \<^term>\<open>TI t\<close> indicates that the height will be the same. A value of the
+form \<^term>\<open>OF l p r\<close> indicates an increase in height.\<close>
-fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
-"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
-"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
+fun full\<^sub>i :: "nat \<Rightarrow> 'a upI \<Rightarrow> bool" where
+"full\<^sub>i n (TI t) \<longleftrightarrow> full n t" |
+"full\<^sub>i n (OF l p r) \<longleftrightarrow> full n l \<and> full n r"
lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
-by (induct rule: full.induct) (auto split: up\<^sub>i.split)
+by (induct rule: full.induct) (auto split: upI.split)
-text \<open>The \<^const>\<open>insert\<close> operation preserves balance.\<close>
+text \<open>The \<^const>\<open>insert\<close> operation preserves completeance.\<close>
-lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
-unfolding bal_iff_full insert_def
+lemma complete_insert: "complete t \<Longrightarrow> complete (insert a t)"
+unfolding complete_iff_full insert_def
apply (erule exE)
apply (drule full\<^sub>i_ins [of _ _ a])
apply (cases "ins a t")
@@ -290,42 +290,42 @@
subsection "Proofs for delete"
-instantiation up\<^sub>d :: (type)height
+instantiation upD :: (type)height
begin
-fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
-"height (T\<^sub>d t) = height t" |
-"height (Up\<^sub>d t) = height t + 1"
+fun height_upD :: "'a upD \<Rightarrow> nat" where
+"height (TD t) = height t" |
+"height (UF t) = height t + 1"
instance ..
end
-lemma bal_tree\<^sub>d_node21:
- "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))"
+lemma complete_treeD_node21:
+ "\<lbrakk>complete r; complete (treeD l'); height r = height l' \<rbrakk> \<Longrightarrow> complete (treeD (node21 l' a r))"
by(induct l' a r rule: node21.induct) auto
-lemma bal_tree\<^sub>d_node22:
- "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))"
+lemma complete_treeD_node22:
+ "\<lbrakk>complete(treeD r'); complete l; height r' = height l \<rbrakk> \<Longrightarrow> complete (treeD (node22 l a r'))"
by(induct l a r' rule: node22.induct) auto
-lemma bal_tree\<^sub>d_node31:
- "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk>
- \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))"
+lemma complete_treeD_node31:
+ "\<lbrakk> complete (treeD l'); complete m; complete r; height l' = height r; height m = height r \<rbrakk>
+ \<Longrightarrow> complete (treeD (node31 l' a m b r))"
by(induct l' a m b r rule: node31.induct) auto
-lemma bal_tree\<^sub>d_node32:
- "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk>
- \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))"
+lemma complete_treeD_node32:
+ "\<lbrakk> complete l; complete (treeD m'); complete r; height l = height r; height m' = height r \<rbrakk>
+ \<Longrightarrow> complete (treeD (node32 l a m' b r))"
by(induct l a m' b r rule: node32.induct) auto
-lemma bal_tree\<^sub>d_node33:
- "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
- \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))"
+lemma complete_treeD_node33:
+ "\<lbrakk> complete l; complete m; complete(treeD r'); height l = height r'; height m = height r' \<rbrakk>
+ \<Longrightarrow> complete (treeD (node33 l a m b r'))"
by(induct l a m b r' rule: node33.induct) auto
-lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
- bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
+lemmas completes = complete_treeD_node21 complete_treeD_node22
+ complete_treeD_node31 complete_treeD_node32 complete_treeD_node33
lemma height'_node21:
"height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
@@ -354,32 +354,32 @@
height'_node31 height'_node32 height'_node33
lemma height_split_min:
- "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
+ "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> complete t \<Longrightarrow> height t' = height t"
by(induct t arbitrary: x t' rule: split_min.induct)
(auto simp: heights split: prod.splits)
-lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
+lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t"
by(induction x t rule: del.induct)
(auto simp: heights max_def height_split_min split: prod.splits)
-lemma bal_split_min:
- "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
+lemma complete_split_min:
+ "\<lbrakk> split_min t = (x, t'); complete t; height t > 0 \<rbrakk> \<Longrightarrow> complete (treeD t')"
by(induct t arbitrary: x t' rule: split_min.induct)
- (auto simp: heights height_split_min bals split: prod.splits)
+ (auto simp: heights height_split_min completes split: prod.splits)
-lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
+lemma complete_treeD_del: "complete t \<Longrightarrow> complete(treeD(del x t))"
by(induction x t rule: del.induct)
- (auto simp: bals bal_split_min height_del height_split_min split: prod.splits)
+ (auto simp: completes complete_split_min height_del height_split_min split: prod.splits)
-corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
-by(simp add: delete_def bal_tree\<^sub>d_del)
+corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)"
+by(simp add: delete_def complete_treeD_del)
subsection \<open>Overall Correctness\<close>
interpretation S: Set_by_Ordered
where empty = empty and isin = isin and insert = insert and delete = delete
-and inorder = inorder and inv = bal
+and inorder = inorder and inv = complete
proof (standard, goal_cases)
case 2 thus ?case by(simp add: isin_set)
next
@@ -387,9 +387,9 @@
next
case 4 thus ?case by(simp add: inorder_delete)
next
- case 6 thus ?case by(simp add: bal_insert)
+ case 6 thus ?case by(simp add: complete_insert)
next
- case 7 thus ?case by(simp add: bal_delete)
+ case 7 thus ?case by(simp add: complete_delete)
qed (simp add: empty_def)+
end
--- a/src/HOL/Data_Structures/Trie_Fun.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Data_Structures/Trie_Fun.thy Sat Jun 01 13:53:23 2019 +0200
@@ -10,6 +10,9 @@
datatype 'a trie = Nd bool "'a \<Rightarrow> 'a trie option"
+definition empty :: "'a trie" where
+[simp]: "empty = Nd False (\<lambda>_. None)"
+
fun isin :: "'a trie \<Rightarrow> 'a list \<Rightarrow> bool" where
"isin (Nd b m) [] = b" |
"isin (Nd b m) (k # xs) = (case m k of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
@@ -17,7 +20,7 @@
fun insert :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
"insert [] (Nd b m) = Nd True m" |
"insert (x#xs) (Nd b m) =
- Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> Nd False (\<lambda>_. None) | Some t \<Rightarrow> t))))"
+ Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> empty | Some t \<Rightarrow> t))))"
fun delete :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
"delete [] (Nd b m) = Nd False m" |
@@ -73,7 +76,7 @@
qed
interpretation S: Set
-where empty = "Nd False (\<lambda>_. None)" and isin = isin and insert = insert and delete = delete
+where empty = empty and isin = isin and insert = insert and delete = delete
and set = set and invar = "\<lambda>_. True"
proof (standard, goal_cases)
case 1 show ?case by (simp)
--- a/src/HOL/Data_Structures/Trie_Map.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Data_Structures/Trie_Map.thy Sat Jun 01 13:53:23 2019 +0200
@@ -29,6 +29,10 @@
apply(auto split: if_splits)
done
+
+definition empty :: "'a trie_map" where
+[simp]: "empty = Nd False Leaf"
+
fun isin :: "('a::linorder) trie_map \<Rightarrow> 'a list \<Rightarrow> bool" where
"isin (Nd b m) [] = b" |
"isin (Nd b m) (x # xs) = (case lookup m x of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
@@ -36,7 +40,7 @@
fun insert :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where
"insert [] (Nd b m) = Nd True m" |
"insert (x#xs) (Nd b m) =
- Nd b (update x (insert xs (case lookup m x of None \<Rightarrow> Nd False Leaf | Some t \<Rightarrow> t)) m)"
+ Nd b (update x (insert xs (case lookup m x of None \<Rightarrow> empty | Some t \<Rightarrow> t)) m)"
fun delete :: "('a::linorder) list \<Rightarrow> 'a trie_map \<Rightarrow> 'a trie_map" where
"delete [] (Nd b m) = Nd False m" |
@@ -84,7 +88,7 @@
text \<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close>
interpretation S2: Set
-where empty = "Nd False Leaf" and isin = isin and insert = insert and delete = delete
+where empty = empty and isin = isin and insert = insert and delete = delete
and set = "set o abs" and invar = invar
proof (standard, goal_cases)
case 1 show ?case by (simp)
--- a/src/HOL/Data_Structures/Tries_Binary.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Data_Structures/Tries_Binary.thy Sat Jun 01 13:53:23 2019 +0200
@@ -21,6 +21,9 @@
datatype trie = Lf | Nd bool "trie * trie"
+definition empty :: trie where
+[simp]: "empty = Lf"
+
fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
"isin Lf ks = False" |
"isin (Nd b lr) ks =
@@ -34,8 +37,8 @@
"insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
"insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"
-lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
-apply(induction as t arbitrary: bs rule: insert.induct)
+lemma isin_insert: "isin (insert xs t) ys = (xs = ys \<or> isin t ys)"
+apply(induction xs t arbitrary: ys rule: insert.induct)
apply (auto split: list.splits if_splits)
done
@@ -65,8 +68,8 @@
[] \<Rightarrow> node False lr |
k#ks' \<Rightarrow> node b (mod2 (delete ks') k lr))"
-lemma isin_delete: "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
-apply(induction as t arbitrary: bs rule: delete.induct)
+lemma isin_delete: "isin (delete xs t) ys = (xs \<noteq> ys \<and> isin t ys)"
+apply(induction xs t arbitrary: ys rule: delete.induct)
apply simp
apply (auto split: list.splits if_splits)
apply (metis isin.simps(1))
@@ -76,28 +79,37 @@
definition set_trie :: "trie \<Rightarrow> bool list set" where
"set_trie t = {xs. isin t xs}"
+lemma set_trie_empty: "set_trie empty = {}"
+by(simp add: set_trie_def)
+
+lemma set_trie_isin: "isin t xs = (xs \<in> set_trie t)"
+by(simp add: set_trie_def)
+
lemma set_trie_insert: "set_trie(insert xs t) = set_trie t \<union> {xs}"
by(auto simp add: isin_insert set_trie_def)
+lemma set_trie_delete: "set_trie(delete xs t) = set_trie t - {xs}"
+by(auto simp add: isin_delete set_trie_def)
+
interpretation S: Set
-where empty = Lf and isin = isin and insert = insert and delete = delete
+where empty = empty and isin = isin and insert = insert and delete = delete
and set = set_trie and invar = "\<lambda>t. True"
proof (standard, goal_cases)
- case 1 show ?case by (simp add: set_trie_def)
+ case 1 show ?case by (rule set_trie_empty)
next
- case 2 thus ?case by(simp add: set_trie_def)
+ case 2 show ?case by(rule set_trie_isin)
next
case 3 thus ?case by(auto simp: set_trie_insert)
next
- case 4 thus ?case by(auto simp: isin_delete set_trie_def)
+ case 4 show ?case by(rule set_trie_delete)
qed (rule TrueI)+
subsection "Patricia Trie"
-datatype ptrie = LfP | NdP "bool list" bool "ptrie * ptrie"
+datatype trieP = LfP | NdP "bool list" bool "trieP * trieP"
-fun isinP :: "ptrie \<Rightarrow> bool list \<Rightarrow> bool" where
+fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where
"isinP LfP ks = False" |
"isinP (NdP ps b lr) ks =
(let n = length ps in
@@ -105,6 +117,9 @@
then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (sel2 k lr) ks'
else False)"
+definition emptyP :: trieP where
+[simp]: "emptyP = LfP"
+
fun split where
"split [] ys = ([],[],ys)" |
"split xs [] = ([],xs,[])" |
@@ -118,7 +133,8 @@
\<Longrightarrow> mod2 f k lr= mod2 f' k' lr'"
by(cases lr, cases lr', auto)
-fun insertP :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+
+fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
"insertP ks LfP = NdP ks True (LfP,LfP)" |
"insertP ks (NdP ps b lr) =
(case split ks ps of
@@ -133,10 +149,10 @@
(qs,[],[]) \<Rightarrow> NdP ps True lr)"
-fun nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> ptrie * ptrie \<Rightarrow> ptrie" where
+fun nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> trieP * trieP \<Rightarrow> trieP" where
"nodeP ps b lr = (if \<not> b \<and> lr = (LfP,LfP) then LfP else NdP ps b lr)"
-fun deleteP :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
"deleteP ks LfP = LfP" |
"deleteP ks (NdP ps b lr) =
(case split ks ps of
@@ -147,16 +163,16 @@
subsubsection \<open>Functional Correctness\<close>
-text \<open>First step: @{typ ptrie} implements @{typ trie} via the abstraction function \<open>abs_ptrie\<close>:\<close>
+text \<open>First step: @{typ trieP} implements @{typ trie} via the abstraction function \<open>abs_trieP\<close>:\<close>
fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
"prefix_trie [] t = t" |
"prefix_trie (k#ks) t =
(let t' = prefix_trie ks t in Nd False (if k then (Lf,t') else (t',Lf)))"
-fun abs_ptrie :: "ptrie \<Rightarrow> trie" where
-"abs_ptrie LfP = Lf" |
-"abs_ptrie (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_ptrie l, abs_ptrie r))"
+fun abs_trieP :: "trieP \<Rightarrow> trie" where
+"abs_trieP LfP = Lf" |
+"abs_trieP (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_trieP l, abs_trieP r))"
text \<open>Correctness of @{const isinP}:\<close>
@@ -168,9 +184,9 @@
apply(auto split: list.split)
done
-lemma isinP:
- "isinP t ks = isin (abs_ptrie t) ks"
-apply(induction t arbitrary: ks rule: abs_ptrie.induct)
+lemma abs_trieP_isinP:
+ "isinP t ks = isin (abs_trieP t) ks"
+apply(induction t arbitrary: ks rule: abs_trieP.induct)
apply(auto simp: isin_prefix_trie split: list.split)
done
@@ -204,8 +220,8 @@
apply(auto split: prod.splits if_splits)
done
-lemma abs_ptrie_insertP:
- "abs_ptrie (insertP ks t) = insert ks (abs_ptrie t)"
+lemma abs_trieP_insertP:
+ "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
apply(induction t arbitrary: ks)
apply(auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
dest!: split_if split: list.split prod.split if_splits)
@@ -217,7 +233,7 @@
lemma prefix_trie_Lf: "prefix_trie xs t = Lf \<longleftrightarrow> xs = [] \<and> t = Lf"
by(cases xs)(auto)
-lemma abs_ptrie_Lf: "abs_ptrie t = Lf \<longleftrightarrow> t = LfP"
+lemma abs_trieP_Lf: "abs_trieP t = Lf \<longleftrightarrow> t = LfP"
by(cases t) (auto simp: prefix_trie_Lf)
lemma delete_prefix_trie:
@@ -230,35 +246,40 @@
= (if delete ys t = Lf then Lf else prefix_trie xs (delete ys t))"
by(induction xs)(auto simp: prefix_trie_Lf)
-lemma delete_abs_ptrie:
- "delete ks (abs_ptrie t) = abs_ptrie (deleteP ks t)"
+lemma delete_abs_trieP:
+ "delete ks (abs_trieP t) = abs_trieP (deleteP ks t)"
apply(induction t arbitrary: ks)
apply(auto simp: delete_prefix_trie delete_append_prefix_trie
- prefix_trie_append prefix_trie_Lf abs_ptrie_Lf
+ prefix_trie_append prefix_trie_Lf abs_trieP_Lf
dest!: split_if split: if_splits list.split prod.split)
done
text \<open>The overall correctness proof. Simply composes correctness lemmas.\<close>
-definition set_ptrie :: "ptrie \<Rightarrow> bool list set" where
-"set_ptrie = set_trie o abs_ptrie"
+definition set_trieP :: "trieP \<Rightarrow> bool list set" where
+"set_trieP = set_trie o abs_trieP"
+
+lemma isinP_set_trieP: "isinP t xs = (xs \<in> set_trieP t)"
+by(simp add: abs_trieP_isinP set_trie_isin set_trieP_def)
-lemma set_ptrie_insertP: "set_ptrie (insertP xs t) = set_ptrie t \<union> {xs}"
-by(simp add: abs_ptrie_insertP set_trie_insert set_ptrie_def)
+lemma set_trieP_insertP: "set_trieP (insertP xs t) = set_trieP t \<union> {xs}"
+by(simp add: abs_trieP_insertP set_trie_insert set_trieP_def)
+
+lemma set_trieP_deleteP: "set_trieP (deleteP xs t) = set_trieP t - {xs}"
+by(auto simp: set_trie_delete set_trieP_def simp flip: delete_abs_trieP)
interpretation SP: Set
-where empty = LfP and isin = isinP and insert = insertP and delete = deleteP
-and set = set_ptrie and invar = "\<lambda>t. True"
+where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
+and set = set_trieP and invar = "\<lambda>t. True"
proof (standard, goal_cases)
- case 1 show ?case by (simp add: set_ptrie_def set_trie_def)
+ case 1 show ?case by (simp add: set_trieP_def set_trie_def)
next
- case 2 thus ?case by(simp add: isinP set_ptrie_def set_trie_def)
+ case 2 show ?case by(rule isinP_set_trieP)
next
- case 3 thus ?case by (auto simp: set_ptrie_insertP)
+ case 3 thus ?case by (auto simp: set_trieP_insertP)
next
- case 4 thus ?case
- by(auto simp: isin_delete set_ptrie_def set_trie_def simp flip: delete_abs_ptrie)
+ case 4 thus ?case by(auto simp: set_trieP_deleteP)
qed (rule TrueI)+
end
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Sat Jun 01 13:53:23 2019 +0200
@@ -956,6 +956,15 @@
lemma ennreal_numeral[simp]: "ennreal (numeral n) = numeral n"
using ennreal_of_nat_eq_real_of_nat[of "numeral n"] by simp
+lemma ennreal_less_numeral_iff [simp]: "ennreal n < numeral w \<longleftrightarrow> n < numeral w"
+ by (metis ennreal_less_iff ennreal_numeral less_le not_less zero_less_numeral)
+
+lemma numeral_less_ennreal_iff [simp]: "numeral w < ennreal n \<longleftrightarrow> numeral w < n"
+ using ennreal_less_iff zero_le_numeral by fastforce
+
+lemma numeral_le_ennreal_iff [simp]: "numeral n \<le> ennreal m \<longleftrightarrow> numeral n \<le> m"
+ by (metis not_le ennreal_less_numeral_iff)
+
lemma min_ennreal: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> min (ennreal x) (ennreal y) = ennreal (min x y)"
by (auto split: split_min)
--- a/src/HOL/Library/Finite_Map.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Library/Finite_Map.thy Sat Jun 01 13:53:23 2019 +0200
@@ -254,6 +254,15 @@
lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def)
lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def)
+lemma fmupd_reorder_neq:
+ assumes "a \<noteq> b"
+ shows "fmupd a x (fmupd b y m) = fmupd b y (fmupd a x m)"
+using assms
+by transfer' (auto simp: map_upd_def)
+
+lemma fmupd_idem[simp]: "fmupd a x (fmupd a y m) = fmupd a x m"
+by transfer' (auto simp: map_upd_def)
+
lift_definition fmfilter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
is map_filter
parametric map_filter_transfer
@@ -357,6 +366,18 @@
lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \<subseteq> A" unfolding fmfilter_alt_defs by auto
lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\<subseteq>| A" unfolding fmfilter_alt_defs by auto
+lemma fmdrop_fmupd: "fmdrop x (fmupd y z m) = (if x = y then fmdrop x m else fmupd y z (fmdrop x m))"
+by transfer' (auto simp: map_drop_def map_filter_def map_upd_def)
+
+lemma fmdrop_idle: "x |\<notin>| fmdom B \<Longrightarrow> fmdrop x B = B"
+by transfer' (auto simp: map_drop_def map_filter_def)
+
+lemma fmdrop_idle': "x \<notin> fmdom' B \<Longrightarrow> fmdrop x B = B"
+by transfer' (auto simp: map_drop_def map_filter_def)
+
+lemma fmdrop_fmupd_same: "fmdrop x (fmupd x y m) = fmdrop x m"
+by transfer' (auto simp: map_drop_def map_filter_def map_upd_def)
+
lemma fmdom'_restrict_set_precise: "fmdom' (fmrestrict_set A m) = fmdom' m \<inter> A"
unfolding fmfilter_alt_defs by auto
@@ -404,6 +425,12 @@
lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
unfolding fmfilter_alt_defs by simp
+lemma fmdrop_fset_fmdom[simp]: "fmdrop_fset (fmdom A) A = fmempty"
+by transfer' (auto simp: map_drop_set_def map_filter_def)
+
+lemma fmdrop_set_fmdom[simp]: "fmdrop_set (fmdom' A) A = fmempty"
+by transfer' (auto simp: map_drop_set_def map_filter_def)
+
lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
unfolding fmfilter_alt_defs by simp
@@ -1028,6 +1055,8 @@
including fset.lifting
by transfer' (auto simp: set_of_map_def)
+lemma fmmap_fmupd: "fmmap f (fmupd x y m) = fmupd x (f y) (fmmap f m)"
+by transfer' (auto simp: fun_eq_iff map_upd_def)
subsection \<open>\<^const>\<open>size\<close> setup\<close>
--- a/src/HOL/List.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/List.thy Sat Jun 01 13:53:23 2019 +0200
@@ -791,7 +791,7 @@
by (fact measure_induct)
lemma induct_list012:
- "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
+ "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. \<lbrakk> P zs; P (y # zs) \<rbrakk> \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
by induction_schema (pat_completeness, lexicographic_order)
lemma list_nonempty_induct [consumes 1, case_names single cons]:
@@ -5486,26 +5486,7 @@
text \<open>Stability of \<^const>\<open>sort_key\<close>:\<close>
lemma sort_key_stable: "filter (\<lambda>y. f y = k) (sort_key f xs) = filter (\<lambda>y. f y = k) xs"
-proof (induction xs)
- case Nil thus ?case by simp
-next
- case (Cons a xs)
- thus ?case
- proof (cases "f a = k")
- case False thus ?thesis
- using Cons.IH by (metis (mono_tags) filter.simps(2) filter_sort)
- next
- case True
- hence ler: "filter (\<lambda>y. f y = k) (a # xs) = a # filter (\<lambda>y. f y = f a) xs" by simp
- have "\<forall>y \<in> set (sort_key f (filter (\<lambda>y. f y = f a) xs)). f y = f a" by simp
- hence "insort_key f a (sort_key f (filter (\<lambda>y. f y = f a) xs))
- = a # (sort_key f (filter (\<lambda>y. f y = f a) xs))"
- by (simp add: insort_is_Cons)
- hence lel: "filter (\<lambda>y. f y = k) (sort_key f (a # xs)) = a # filter (\<lambda>y. f y = f a) (sort_key f xs)"
- by (metis True filter_sort ler sort_key_simps(2))
- from lel ler show ?thesis using Cons.IH True by (auto)
- qed
-qed
+by (induction xs) (auto simp: filter_insort insort_is_Cons filter_insort_triv)
corollary stable_sort_key_sort_key: "stable_sort_key sort_key"
by(simp add: stable_sort_key_def sort_key_stable)
--- a/src/HOL/Num.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Num.thy Sat Jun 01 13:53:23 2019 +0200
@@ -606,11 +606,9 @@
end
-subsubsection \<open>Comparisons: class \<open>linordered_semidom\<close>\<close>
+subsubsection \<open>Comparisons: class \<open>linordered_nonzero_semiring\<close>\<close>
-text \<open>Could be perhaps more general than here.\<close>
-
-context linordered_semidom
+context linordered_nonzero_semiring
begin
lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n"
@@ -621,10 +619,10 @@
qed
lemma one_le_numeral: "1 \<le> numeral n"
- using numeral_le_iff [of One n] by (simp add: numeral_One)
+ using numeral_le_iff [of num.One n] by (simp add: numeral_One)
-lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One"
- using numeral_le_iff [of n One] by (simp add: numeral_One)
+lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> num.One"
+ using numeral_le_iff [of n num.One] by (simp add: numeral_One)
lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n"
proof -
@@ -634,16 +632,16 @@
qed
lemma not_numeral_less_one: "\<not> numeral n < 1"
- using numeral_less_iff [of n One] by (simp add: numeral_One)
+ using numeral_less_iff [of n num.One] by (simp add: numeral_One)
-lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> One < n"
- using numeral_less_iff [of One n] by (simp add: numeral_One)
+lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> num.One < n"
+ using numeral_less_iff [of num.One n] by (simp add: numeral_One)
lemma zero_le_numeral: "0 \<le> numeral n"
- by (induct n) (simp_all add: numeral.simps)
+ using dual_order.trans one_le_numeral zero_le_one by blast
lemma zero_less_numeral: "0 < numeral n"
- by (induct n) (simp_all add: numeral.simps add_pos_pos)
+ using less_linear not_numeral_less_one order.strict_trans zero_less_one by blast
lemma not_numeral_le_zero: "\<not> numeral n \<le> 0"
by (simp add: not_le zero_less_numeral)
--- a/src/HOL/Real.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Real.thy Sat Jun 01 13:53:23 2019 +0200
@@ -1261,7 +1261,7 @@
@{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1},
@{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
@{thm of_int_mult}, @{thm of_int_of_nat_eq},
- @{thm of_nat_numeral}, @{thm of_nat_numeral}, @{thm of_int_neg_numeral}]
+ @{thm of_nat_numeral}, @{thm of_int_numeral}, @{thm of_int_neg_numeral}]
#> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> real\<close>)
#> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> real\<close>))
\<close>
--- a/src/HOL/Transcendental.thy Sat Jun 01 11:29:59 2019 +0200
+++ b/src/HOL/Transcendental.thy Sat Jun 01 13:53:23 2019 +0200
@@ -2771,8 +2771,8 @@
using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
by (auto simp: field_simps powr_minus)
-lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
- by (metis of_nat_numeral powr_realpow)
+lemma powr_numeral [simp]: "0 \<le> x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
+ by (metis less_le power_zero_numeral powr_0 of_nat_numeral powr_realpow)
lemma powr_int:
assumes "x > 0"
--- a/src/Tools/VSCode/extension/README.md Sat Jun 01 11:29:59 2019 +0200
+++ b/src/Tools/VSCode/extension/README.md Sat Jun 01 13:53:23 2019 +0200
@@ -1,15 +1,14 @@
# Isabelle Prover IDE support
This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
-requires Isabelle2019.
+requires a repository version of Isabelle.
The implementation is centered around the VSCode Language Server protocol, but
with many add-ons that are specific to VSCode and Isabelle/PIDE.
See also:
- * <https://isabelle.in.tum.de/website-Isabelle2019>
- * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2019/src/Tools/VSCode>
+ * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
* <https://github.com/Microsoft/language-server-protocol>
@@ -59,8 +58,8 @@
### Isabelle/VSCode Installation
- * Download Isabelle2019 from <https://isabelle.in.tum.de/website-Isabelle2019>
- or any of its mirror sites.
+ * Download a recent Isabelle development snapshot from
+ <https://isabelle.in.tum.de/devel/release_snapshot>
* Unpack and run the main Isabelle/jEdit application as usual, to ensure that
the logic image is built properly and Isabelle works as expected.
@@ -69,7 +68,7 @@
* Open the VSCode *Extensions* view and install the following:
- + *Isabelle2019* (needs to fit to the underlying Isabelle release).
+ + *Isabelle* (needs to fit to the underlying Isabelle release).
+ *Prettify Symbols Mode* (important for display of Isabelle symbols).
@@ -90,17 +89,17 @@
+ Linux:
```
- "isabelle.home": "/home/makarius/Isabelle2019"
+ "isabelle.home": "/home/makarius/Isabelle"
```
+ Mac OS X:
```
- "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2019"
+ "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
```
+ Windows:
```
- "isabelle.home": "C:\\Users\\makarius\\Isabelle2019"
+ "isabelle.home": "C:\\Users\\makarius\\Isabelle"
```
* Restart the VSCode application to ensure that all extensions are properly
--- a/src/Tools/VSCode/extension/package.json Sat Jun 01 11:29:59 2019 +0200
+++ b/src/Tools/VSCode/extension/package.json Sat Jun 01 13:53:23 2019 +0200
@@ -1,6 +1,6 @@
{
- "name": "Isabelle2019",
- "displayName": "Isabelle2019",
+ "name": "Isabelle",
+ "displayName": "Isabelle",
"description": "Isabelle Prover IDE",
"keywords": [
"theorem prover",