--- a/src/HOL/Library/Comparator.thy Mon Mar 31 22:46:11 2025 +0100
+++ b/src/HOL/Library/Comparator.thy Mon Mar 31 22:46:18 2025 +0100
@@ -13,146 +13,146 @@
datatype comp = Less | Equiv | Greater
locale comparator =
- fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
- assumes refl [simp]: "\<And>a. cmp a a = Equiv"
- and trans_equiv: "\<And>a b c. cmp a b = Equiv \<Longrightarrow> cmp b c = Equiv \<Longrightarrow> cmp a c = Equiv"
- assumes trans_less: "cmp a b = Less \<Longrightarrow> cmp b c = Less \<Longrightarrow> cmp a c = Less"
- and greater_iff_sym_less: "\<And>b a. cmp b a = Greater \<longleftrightarrow> cmp a b = Less"
+ fixes cmp :: \<open>'a \<Rightarrow> 'a \<Rightarrow> comp\<close>
+ assumes refl [simp]: \<open>\<And>a. cmp a a = Equiv\<close>
+ and trans_equiv: \<open>\<And>a b c. cmp a b = Equiv \<Longrightarrow> cmp b c = Equiv \<Longrightarrow> cmp a c = Equiv\<close>
+ assumes trans_less: \<open>cmp a b = Less \<Longrightarrow> cmp b c = Less \<Longrightarrow> cmp a c = Less\<close>
+ and greater_iff_sym_less: \<open>\<And>b a. cmp b a = Greater \<longleftrightarrow> cmp a b = Less\<close>
begin
text \<open>Dual properties\<close>
lemma trans_greater:
- "cmp a c = Greater" if "cmp a b = Greater" "cmp b c = Greater"
+ \<open>cmp a c = Greater\<close> if \<open>cmp a b = Greater\<close> \<open>cmp b c = Greater\<close>
using that greater_iff_sym_less trans_less by blast
lemma less_iff_sym_greater:
- "cmp b a = Less \<longleftrightarrow> cmp a b = Greater"
+ \<open>cmp b a = Less \<longleftrightarrow> cmp a b = Greater\<close>
by (simp add: greater_iff_sym_less)
text \<open>The equivalence part\<close>
lemma sym:
- "cmp b a = Equiv \<longleftrightarrow> cmp a b = Equiv"
+ \<open>cmp b a = Equiv \<longleftrightarrow> cmp a b = Equiv\<close>
by (metis (full_types) comp.exhaust greater_iff_sym_less)
lemma reflp:
- "reflp (\<lambda>a b. cmp a b = Equiv)"
+ \<open>reflp (\<lambda>a b. cmp a b = Equiv)\<close>
by (rule reflpI) simp
lemma symp:
- "symp (\<lambda>a b. cmp a b = Equiv)"
+ \<open>symp (\<lambda>a b. cmp a b = Equiv)\<close>
by (rule sympI) (simp add: sym)
lemma transp:
- "transp (\<lambda>a b. cmp a b = Equiv)"
+ \<open>transp (\<lambda>a b. cmp a b = Equiv)\<close>
by (rule transpI) (fact trans_equiv)
lemma equivp:
- "equivp (\<lambda>a b. cmp a b = Equiv)"
+ \<open>equivp (\<lambda>a b. cmp a b = Equiv)\<close>
using reflp symp transp by (rule equivpI)
text \<open>The strict part\<close>
lemma irreflp_less:
- "irreflp (\<lambda>a b. cmp a b = Less)"
+ \<open>irreflp (\<lambda>a b. cmp a b = Less)\<close>
by (rule irreflpI) simp
lemma irreflp_greater:
- "irreflp (\<lambda>a b. cmp a b = Greater)"
+ \<open>irreflp (\<lambda>a b. cmp a b = Greater)\<close>
by (rule irreflpI) simp
lemma asym_less:
- "cmp b a \<noteq> Less" if "cmp a b = Less"
+ \<open>cmp b a \<noteq> Less\<close> if \<open>cmp a b = Less\<close>
using that greater_iff_sym_less by force
lemma asym_greater:
- "cmp b a \<noteq> Greater" if "cmp a b = Greater"
+ \<open>cmp b a \<noteq> Greater\<close> if \<open>cmp a b = Greater\<close>
using that greater_iff_sym_less by force
lemma asymp_less:
- "asymp (\<lambda>a b. cmp a b = Less)"
- using irreflp_less by (auto intro: asympI dest: asym_less)
+ \<open>asymp (\<lambda>a b. cmp a b = Less)\<close>
+ using irreflp_less by (auto dest: asym_less)
lemma asymp_greater:
- "asymp (\<lambda>a b. cmp a b = Greater)"
- using irreflp_greater by (auto intro!: asympI dest: asym_greater)
+ \<open>asymp (\<lambda>a b. cmp a b = Greater)\<close>
+ using irreflp_greater by (auto dest: asym_greater)
lemma trans_equiv_less:
- "cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less"
+ \<open>cmp a c = Less\<close> if \<open>cmp a b = Equiv\<close> and \<open>cmp b c = Less\<close>
using that
by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
lemma trans_less_equiv:
- "cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv"
+ \<open>cmp a c = Less\<close> if \<open>cmp a b = Less\<close> and \<open>cmp b c = Equiv\<close>
using that
by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
lemma trans_equiv_greater:
- "cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater"
+ \<open>cmp a c = Greater\<close> if \<open>cmp a b = Equiv\<close> and \<open>cmp b c = Greater\<close>
using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv)
lemma trans_greater_equiv:
- "cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv"
+ \<open>cmp a c = Greater\<close> if \<open>cmp a b = Greater\<close> and \<open>cmp b c = Equiv\<close>
using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less)
lemma transp_less:
- "transp (\<lambda>a b. cmp a b = Less)"
+ \<open>transp (\<lambda>a b. cmp a b = Less)\<close>
by (rule transpI) (fact trans_less)
lemma transp_greater:
- "transp (\<lambda>a b. cmp a b = Greater)"
+ \<open>transp (\<lambda>a b. cmp a b = Greater)\<close>
by (rule transpI) (fact trans_greater)
text \<open>The reflexive part\<close>
lemma reflp_not_less:
- "reflp (\<lambda>a b. cmp a b \<noteq> Less)"
+ \<open>reflp (\<lambda>a b. cmp a b \<noteq> Less)\<close>
by (rule reflpI) simp
lemma reflp_not_greater:
- "reflp (\<lambda>a b. cmp a b \<noteq> Greater)"
+ \<open>reflp (\<lambda>a b. cmp a b \<noteq> Greater)\<close>
by (rule reflpI) simp
lemma quasisym_not_less:
- "cmp a b = Equiv" if "cmp a b \<noteq> Less" and "cmp b a \<noteq> Less"
+ \<open>cmp a b = Equiv\<close> if \<open>cmp a b \<noteq> Less\<close> and \<open>cmp b a \<noteq> Less\<close>
using that comp.exhaust greater_iff_sym_less by auto
lemma quasisym_not_greater:
- "cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater"
+ \<open>cmp a b = Equiv\<close> if \<open>cmp a b \<noteq> Greater\<close> and \<open>cmp b a \<noteq> Greater\<close>
using that comp.exhaust greater_iff_sym_less by auto
lemma trans_not_less:
- "cmp a c \<noteq> Less" if "cmp a b \<noteq> Less" "cmp b c \<noteq> Less"
+ \<open>cmp a c \<noteq> Less\<close> if \<open>cmp a b \<noteq> Less\<close> \<open>cmp b c \<noteq> Less\<close>
using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less)
lemma trans_not_greater:
- "cmp a c \<noteq> Greater" if "cmp a b \<noteq> Greater" "cmp b c \<noteq> Greater"
+ \<open>cmp a c \<noteq> Greater\<close> if \<open>cmp a b \<noteq> Greater\<close> \<open>cmp b c \<noteq> Greater\<close>
using that greater_iff_sym_less trans_not_less by blast
lemma transp_not_less:
- "transp (\<lambda>a b. cmp a b \<noteq> Less)"
+ \<open>transp (\<lambda>a b. cmp a b \<noteq> Less)\<close>
by (rule transpI) (fact trans_not_less)
lemma transp_not_greater:
- "transp (\<lambda>a b. cmp a b \<noteq> Greater)"
+ \<open>transp (\<lambda>a b. cmp a b \<noteq> Greater)\<close>
by (rule transpI) (fact trans_not_greater)
text \<open>Substitution under equivalences\<close>
lemma equiv_subst_left:
- "cmp z y = comp \<longleftrightarrow> cmp x y = comp" if "cmp z x = Equiv" for comp
+ \<open>cmp z y = comp \<longleftrightarrow> cmp x y = comp\<close> if \<open>cmp z x = Equiv\<close> for comp
proof -
- from that have "cmp x z = Equiv"
+ from that have \<open>cmp x z = Equiv\<close>
by (simp add: sym)
with that show ?thesis
by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater)
qed
lemma equiv_subst_right:
- "cmp x z = comp \<longleftrightarrow> cmp x y = comp" if "cmp z y = Equiv" for comp
+ \<open>cmp x z = comp \<longleftrightarrow> cmp x y = comp\<close> if \<open>cmp z y = Equiv\<close> for comp
proof -
- from that have "cmp y z = Equiv"
+ from that have \<open>cmp y z = Equiv\<close>
by (simp add: sym)
with that show ?thesis
by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv)
@@ -160,10 +160,10 @@
end
-typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}"
+typedef 'a comparator = \<open>{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}\<close>
morphisms compare Abs_comparator
proof -
- have "comparator (\<lambda>_ _. Equiv)"
+ have \<open>comparator (\<lambda>_ _. Equiv)\<close>
by standard simp_all
then show ?thesis
by auto
@@ -171,17 +171,17 @@
setup_lifting type_definition_comparator
-global_interpretation compare: comparator "compare cmp"
+global_interpretation compare: comparator \<open>compare cmp\<close>
using compare [of cmp] by simp
-lift_definition flat :: "'a comparator"
- is "\<lambda>_ _. Equiv" by standard simp_all
+lift_definition flat :: \<open>'a comparator\<close>
+ is \<open>\<lambda>_ _. Equiv\<close> by standard simp_all
instantiation comparator :: (linorder) default
begin
-lift_definition default_comparator :: "'a comparator"
- is "\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv"
+lift_definition default_comparator :: \<open>'a comparator\<close>
+ is \<open>\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv\<close>
by standard (auto split: if_splits)
instance ..
@@ -193,8 +193,8 @@
instantiation comparator :: (enum) equal
begin
-lift_definition equal_comparator :: "'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool"
- is "\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x" .
+lift_definition equal_comparator :: \<open>'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool\<close>
+ is \<open>\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x\<close> .
instance
by (standard; transfer) (auto simp add: enum_UNIV)
@@ -202,23 +202,23 @@
end
lemma [code]:
- "HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)"
+ \<open>HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)\<close>
by transfer (simp add: enum_UNIV)
lemma [code nbe]:
- "HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True"
+ \<open>HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True\<close>
by (fact equal_refl)
instantiation comparator :: ("{linorder, typerep}") full_exhaustive
begin
definition full_exhaustive_comparator ::
- "('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
- \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
- where "full_exhaustive_comparator f s =
+ \<open>('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
+ \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option\<close>
+ where \<open>full_exhaustive_comparator f s =
Quickcheck_Exhaustive.orelse
(f (flat, (\<lambda>u. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator))))
- (f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))"
+ (f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))\<close>
instance ..
@@ -227,67 +227,67 @@
subsection \<open>Fundamental comparator combinators\<close>
-lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
- is "\<lambda>cmp a b. cmp b a"
+lift_definition reversed :: \<open>'a comparator \<Rightarrow> 'a comparator\<close>
+ is \<open>\<lambda>cmp a b. cmp b a\<close>
proof -
- fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
- assume "comparator cmp"
+ fix cmp :: \<open>'a \<Rightarrow> 'a \<Rightarrow> comp\<close>
+ assume \<open>comparator cmp\<close>
then interpret comparator cmp .
- show "comparator (\<lambda>a b. cmp b a)"
+ show \<open>comparator (\<lambda>a b. cmp b a)\<close>
by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
qed
-lift_definition key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator"
- is "\<lambda>f cmp a b. cmp (f a) (f b)"
+lift_definition key :: \<open>('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator\<close>
+ is \<open>\<lambda>f cmp a b. cmp (f a) (f b)\<close>
proof -
- fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" and f :: "'b \<Rightarrow> 'a"
- assume "comparator cmp"
+ fix cmp :: \<open>'a \<Rightarrow> 'a \<Rightarrow> comp\<close> and f :: \<open>'b \<Rightarrow> 'a\<close>
+ assume \<open>comparator cmp\<close>
then interpret comparator cmp .
- show "comparator (\<lambda>a b. cmp (f a) (f b))"
+ show \<open>comparator (\<lambda>a b. cmp (f a) (f b))\<close>
by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
qed
subsection \<open>Direct implementations for linear orders on selected types\<close>
-definition comparator_bool :: "bool comparator"
- where [simp, code_abbrev]: "comparator_bool = default"
+definition comparator_bool :: \<open>bool comparator\<close>
+ where [simp, code_abbrev]: \<open>comparator_bool = default\<close>
lemma compare_comparator_bool [code abstract]:
- "compare comparator_bool = (\<lambda>p q.
+ \<open>compare comparator_bool = (\<lambda>p q.
if p then if q then Equiv else Greater
- else if q then Less else Equiv)"
+ else if q then Less else Equiv)\<close>
by (auto simp add: fun_eq_iff) (transfer; simp)+
-definition raw_comparator_nat :: "nat \<Rightarrow> nat \<Rightarrow> comp"
- where [simp]: "raw_comparator_nat = compare default"
+definition raw_comparator_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> comp\<close>
+ where [simp]: \<open>raw_comparator_nat = compare default\<close>
lemma default_comparator_nat [simp, code]:
- "raw_comparator_nat (0::nat) 0 = Equiv"
- "raw_comparator_nat (Suc m) 0 = Greater"
- "raw_comparator_nat 0 (Suc n) = Less"
- "raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n"
+ \<open>raw_comparator_nat (0::nat) 0 = Equiv\<close>
+ \<open>raw_comparator_nat (Suc m) 0 = Greater\<close>
+ \<open>raw_comparator_nat 0 (Suc n) = Less\<close>
+ \<open>raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n\<close>
by (transfer; simp)+
-definition comparator_nat :: "nat comparator"
- where [simp, code_abbrev]: "comparator_nat = default"
+definition comparator_nat :: \<open>nat comparator\<close>
+ where [simp, code_abbrev]: \<open>comparator_nat = default\<close>
lemma compare_comparator_nat [code abstract]:
- "compare comparator_nat = raw_comparator_nat"
+ \<open>compare comparator_nat = raw_comparator_nat\<close>
by simp
-definition comparator_linordered_group :: "'a::linordered_ab_group_add comparator"
- where [simp, code_abbrev]: "comparator_linordered_group = default"
+definition comparator_linordered_group :: \<open>'a::linordered_ab_group_add comparator\<close>
+ where [simp, code_abbrev]: \<open>comparator_linordered_group = default\<close>
lemma comparator_linordered_group [code abstract]:
- "compare comparator_linordered_group = (\<lambda>a b.
+ \<open>compare comparator_linordered_group = (\<lambda>a b.
let c = a - b in if c < 0 then Less
- else if c = 0 then Equiv else Greater)"
+ else if c = 0 then Equiv else Greater)\<close>
proof (rule ext)+
fix a b :: 'a
- show "compare comparator_linordered_group a b =
+ show \<open>compare comparator_linordered_group a b =
(let c = a - b in if c < 0 then Less
- else if c = 0 then Equiv else Greater)"
+ else if c = 0 then Equiv else Greater)\<close>
by (simp add: Let_def not_less) (transfer; auto)
qed
--- a/src/HOL/Library/Sorting_Algorithms.thy Mon Mar 31 22:46:11 2025 +0100
+++ b/src/HOL/Library/Sorting_Algorithms.thy Mon Mar 31 22:46:18 2025 +0100
@@ -8,43 +8,43 @@
section \<open>Stably sorted lists\<close>
-abbreviation (input) stable_segment :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
- where "stable_segment cmp x \<equiv> filter (\<lambda>y. compare cmp x y = Equiv)"
+abbreviation (input) stable_segment :: \<open>'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+ where \<open>stable_segment cmp x \<equiv> filter (\<lambda>y. compare cmp x y = Equiv)\<close>
-fun sorted :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> bool"
- where sorted_Nil: "sorted cmp [] \<longleftrightarrow> True"
- | sorted_single: "sorted cmp [x] \<longleftrightarrow> True"
- | sorted_rec: "sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp y x \<noteq> Greater \<and> sorted cmp (x # xs)"
+fun sorted :: \<open>'a comparator \<Rightarrow> 'a list \<Rightarrow> bool\<close>
+ where sorted_Nil: \<open>sorted cmp [] \<longleftrightarrow> True\<close>
+ | sorted_single: \<open>sorted cmp [x] \<longleftrightarrow> True\<close>
+ | sorted_rec: \<open>sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp y x \<noteq> Greater \<and> sorted cmp (x # xs)\<close>
lemma sorted_ConsI:
- "sorted cmp (x # xs)" if "sorted cmp xs"
- and "\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp x y \<noteq> Greater"
+ \<open>sorted cmp (x # xs)\<close> if \<open>sorted cmp xs\<close>
+ and \<open>\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp x y \<noteq> Greater\<close>
using that by (cases xs) simp_all
lemma sorted_Cons_imp_sorted:
- "sorted cmp xs" if "sorted cmp (x # xs)"
+ \<open>sorted cmp xs\<close> if \<open>sorted cmp (x # xs)\<close>
using that by (cases xs) simp_all
lemma sorted_Cons_imp_not_less:
- "compare cmp y x \<noteq> Greater" if "sorted cmp (y # xs)"
- and "x \<in> set xs"
+ \<open>compare cmp y x \<noteq> Greater\<close> if \<open>sorted cmp (y # xs)\<close>
+ and \<open>x \<in> set xs\<close>
using that by (induction xs arbitrary: y) (auto dest: compare.trans_not_greater)
lemma sorted_induct [consumes 1, case_names Nil Cons, induct pred: sorted]:
- "P xs" if "sorted cmp xs" and "P []"
- and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P xs
- \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P (x # xs)"
+ \<open>P xs\<close> if \<open>sorted cmp xs\<close> and \<open>P []\<close>
+ and *: \<open>\<And>x xs. sorted cmp xs \<Longrightarrow> P xs
+ \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P (x # xs)\<close>
using \<open>sorted cmp xs\<close> proof (induction xs)
case Nil
show ?case
by (rule \<open>P []\<close>)
next
case (Cons x xs)
- from \<open>sorted cmp (x # xs)\<close> have "sorted cmp xs"
+ from \<open>sorted cmp (x # xs)\<close> have \<open>sorted cmp xs\<close>
by (cases xs) simp_all
- moreover have "P xs" using \<open>sorted cmp xs\<close>
+ moreover have \<open>P xs\<close> using \<open>sorted cmp xs\<close>
by (rule Cons.IH)
- moreover have "compare cmp x y \<noteq> Greater" if "y \<in> set xs" for y
+ moreover have \<open>compare cmp x y \<noteq> Greater\<close> if \<open>y \<in> set xs\<close> for y
using that \<open>sorted cmp (x # xs)\<close> proof (induction xs)
case Nil
then show ?case
@@ -58,9 +58,9 @@
by simp
next
case (Cons w ws)
- with Cons.prems have "compare cmp z w \<noteq> Greater" "compare cmp x z \<noteq> Greater"
+ with Cons.prems have \<open>compare cmp z w \<noteq> Greater\<close> \<open>compare cmp x z \<noteq> Greater\<close>
by auto
- then have "compare cmp x w \<noteq> Greater"
+ then have \<open>compare cmp x w \<noteq> Greater\<close>
by (auto dest: compare.trans_not_greater)
with Cons show ?thesis
using Cons.prems Cons.IH by auto
@@ -71,28 +71,28 @@
qed
lemma sorted_induct_remove1 [consumes 1, case_names Nil minimum]:
- "P xs" if "sorted cmp xs" and "P []"
- and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P (remove1 x xs)
+ \<open>P xs\<close> if \<open>sorted cmp xs\<close> and \<open>P []\<close>
+ and *: \<open>\<And>x xs. sorted cmp xs \<Longrightarrow> P (remove1 x xs)
\<Longrightarrow> x \<in> set xs \<Longrightarrow> hd (stable_segment cmp x xs) = x \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater)
- \<Longrightarrow> P xs"
+ \<Longrightarrow> P xs\<close>
using \<open>sorted cmp xs\<close> proof (induction xs)
case Nil
show ?case
by (rule \<open>P []\<close>)
next
case (Cons x xs)
- then have "sorted cmp (x # xs)"
+ then have \<open>sorted cmp (x # xs)\<close>
by (simp add: sorted_ConsI)
moreover note Cons.IH
- moreover have "\<And>y. compare cmp x y = Greater \<Longrightarrow> y \<in> set xs \<Longrightarrow> False"
+ moreover have \<open>\<And>y. compare cmp x y = Greater \<Longrightarrow> y \<in> set xs \<Longrightarrow> False\<close>
using Cons.hyps by simp
ultimately show ?case
- by (auto intro!: * [of "x # xs" x]) blast
+ by (auto intro!: * [of \<open>x # xs\<close> x]) blast
qed
lemma sorted_remove1:
- "sorted cmp (remove1 x xs)" if "sorted cmp xs"
-proof (cases "x \<in> set xs")
+ \<open>sorted cmp (remove1 x xs)\<close> if \<open>sorted cmp xs\<close>
+proof (cases \<open>x \<in> set xs\<close>)
case False
with that show ?thesis
by (simp add: remove1_idem)
@@ -104,21 +104,21 @@
by simp
next
case (Cons y ys)
- show ?case proof (cases "x = y")
+ show ?case proof (cases \<open>x = y\<close>)
case True
with Cons.hyps show ?thesis
by simp
next
case False
- then have "sorted cmp (remove1 x ys)"
+ then have \<open>sorted cmp (remove1 x ys)\<close>
using Cons.IH Cons.prems by auto
- then have "sorted cmp (y # remove1 x ys)"
+ then have \<open>sorted cmp (y # remove1 x ys)\<close>
proof (rule sorted_ConsI)
fix z zs
- assume "remove1 x ys = z # zs"
- with \<open>x \<noteq> y\<close> have "z \<in> set ys"
+ assume \<open>remove1 x ys = z # zs\<close>
+ with \<open>x \<noteq> y\<close> have \<open>z \<in> set ys\<close>
using notin_set_remove1 [of z ys x] by auto
- then show "compare cmp y z \<noteq> Greater"
+ then show \<open>compare cmp y z \<noteq> Greater\<close>
by (rule Cons.hyps(2))
qed
with False show ?thesis
@@ -128,7 +128,7 @@
qed
lemma sorted_stable_segment:
- "sorted cmp (stable_segment cmp x xs)"
+ \<open>sorted cmp (stable_segment cmp x xs)\<close>
proof (induction xs)
case Nil
show ?case
@@ -141,22 +141,22 @@
qed
-primrec insort :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
- where "insort cmp y [] = [y]"
- | "insort cmp y (x # xs) = (if compare cmp y x \<noteq> Greater
+primrec insort :: \<open>'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+ where \<open>insort cmp y [] = [y]\<close>
+ | \<open>insort cmp y (x # xs) = (if compare cmp y x \<noteq> Greater
then y # x # xs
- else x # insort cmp y xs)"
+ else x # insort cmp y xs)\<close>
lemma mset_insort [simp]:
- "mset (insort cmp x xs) = add_mset x (mset xs)"
+ \<open>mset (insort cmp x xs) = add_mset x (mset xs)\<close>
by (induction xs) simp_all
lemma length_insort [simp]:
- "length (insort cmp x xs) = Suc (length xs)"
+ \<open>length (insort cmp x xs) = Suc (length xs)\<close>
by (induction xs) simp_all
lemma sorted_insort:
- "sorted cmp (insort cmp x xs)" if "sorted cmp xs"
+ \<open>sorted cmp (insort cmp x xs)\<close> if \<open>sorted cmp xs\<close>
using that proof (induction xs)
case Nil
then show ?case
@@ -168,37 +168,37 @@
qed
lemma stable_insort_equiv:
- "stable_segment cmp y (insort cmp x xs) = x # stable_segment cmp y xs"
- if "compare cmp y x = Equiv"
+ \<open>stable_segment cmp y (insort cmp x xs) = x # stable_segment cmp y xs\<close>
+ if \<open>compare cmp y x = Equiv\<close>
proof (induction xs)
case Nil
from that show ?case
by simp
next
case (Cons z xs)
- moreover from that have "compare cmp y z = Equiv \<Longrightarrow> compare cmp z x = Equiv"
+ moreover from that have \<open>compare cmp y z = Equiv \<Longrightarrow> compare cmp z x = Equiv\<close>
by (auto intro: compare.trans_equiv simp add: compare.sym)
ultimately show ?case
using that by (auto simp add: compare.greater_iff_sym_less)
qed
lemma stable_insort_not_equiv:
- "stable_segment cmp y (insort cmp x xs) = stable_segment cmp y xs"
- if "compare cmp y x \<noteq> Equiv"
+ \<open>stable_segment cmp y (insort cmp x xs) = stable_segment cmp y xs\<close>
+ if \<open>compare cmp y x \<noteq> Equiv\<close>
using that by (induction xs) simp_all
lemma remove1_insort_same_eq [simp]:
- "remove1 x (insort cmp x xs) = xs"
+ \<open>remove1 x (insort cmp x xs) = xs\<close>
by (induction xs) simp_all
lemma insort_eq_ConsI:
- "insort cmp x xs = x # xs"
- if "sorted cmp xs" "\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater"
+ \<open>insort cmp x xs = x # xs\<close>
+ if \<open>sorted cmp xs\<close> \<open>\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater\<close>
using that by (induction xs) (simp_all add: compare.greater_iff_sym_less)
lemma remove1_insort_not_same_eq [simp]:
- "remove1 y (insort cmp x xs) = insort cmp x (remove1 y xs)"
- if "sorted cmp xs" "x \<noteq> y"
+ \<open>remove1 y (insort cmp x xs) = insort cmp x (remove1 y xs)\<close>
+ if \<open>sorted cmp xs\<close> \<open>x \<noteq> y\<close>
using that proof (induction xs)
case Nil
then show ?case
@@ -206,13 +206,13 @@
next
case (Cons z zs)
show ?case
- proof (cases "compare cmp x z = Greater")
+ proof (cases \<open>compare cmp x z = Greater\<close>)
case True
with Cons show ?thesis
by simp
next
case False
- then have "compare cmp x y \<noteq> Greater" if "y \<in> set zs" for y
+ then have \<open>compare cmp x y \<noteq> Greater\<close> if \<open>y \<in> set zs\<close> for y
using that Cons.hyps
by (auto dest: compare.trans_not_greater)
with Cons show ?thesis
@@ -221,25 +221,25 @@
qed
lemma insort_remove1_same_eq:
- "insort cmp x (remove1 x xs) = xs"
- if "sorted cmp xs" and "x \<in> set xs" and "hd (stable_segment cmp x xs) = x"
+ \<open>insort cmp x (remove1 x xs) = xs\<close>
+ if \<open>sorted cmp xs\<close> and \<open>x \<in> set xs\<close> and \<open>hd (stable_segment cmp x xs) = x\<close>
using that proof (induction xs)
case Nil
then show ?case
by simp
next
case (Cons y ys)
- then have "compare cmp x y \<noteq> Less"
+ then have \<open>compare cmp x y \<noteq> Less\<close>
by (auto simp add: compare.greater_iff_sym_less)
- then consider "compare cmp x y = Greater" | "compare cmp x y = Equiv"
- by (cases "compare cmp x y") auto
+ then consider \<open>compare cmp x y = Greater\<close> | \<open>compare cmp x y = Equiv\<close>
+ by (cases \<open>compare cmp x y\<close>) auto
then show ?case proof cases
case 1
with Cons.prems Cons.IH show ?thesis
by auto
next
case 2
- with Cons.prems have "x = y"
+ with Cons.prems have \<open>x = y\<close>
by simp
with Cons.hyps show ?thesis
by (simp add: insort_eq_ConsI)
@@ -247,8 +247,8 @@
qed
lemma sorted_append_iff:
- "sorted cmp (xs @ ys) \<longleftrightarrow> sorted cmp xs \<and> sorted cmp ys
- \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. compare cmp x y \<noteq> Greater)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?Q")
+ \<open>sorted cmp (xs @ ys) \<longleftrightarrow> sorted cmp xs \<and> sorted cmp ys
+ \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. compare cmp x y \<noteq> Greater)\<close> (is \<open>?P \<longleftrightarrow> ?R \<and> ?S \<and> ?Q\<close>)
proof
assume ?P
have ?R
@@ -260,10 +260,10 @@
moreover have ?Q
using \<open>?P\<close> by (induction xs) (auto simp add: sorted_Cons_imp_not_less,
simp add: sorted_Cons_imp_sorted)
- ultimately show "?R \<and> ?S \<and> ?Q"
+ ultimately show \<open>?R \<and> ?S \<and> ?Q\<close>
by simp
next
- assume "?R \<and> ?S \<and> ?Q"
+ assume \<open>?R \<and> ?S \<and> ?Q\<close>
then have ?R ?S ?Q
by simp_all
then show ?P
@@ -271,65 +271,65 @@
(auto simp add: append_eq_Cons_conv intro!: sorted_ConsI)
qed
-definition sort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
- where "sort cmp xs = foldr (insort cmp) xs []"
+definition sort :: \<open>'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+ where \<open>sort cmp xs = foldr (insort cmp) xs []\<close>
lemma sort_simps [simp]:
- "sort cmp [] = []"
- "sort cmp (x # xs) = insort cmp x (sort cmp xs)"
+ \<open>sort cmp [] = []\<close>
+ \<open>sort cmp (x # xs) = insort cmp x (sort cmp xs)\<close>
by (simp_all add: sort_def)
lemma mset_sort [simp]:
- "mset (sort cmp xs) = mset xs"
+ \<open>mset (sort cmp xs) = mset xs\<close>
by (induction xs) simp_all
lemma length_sort [simp]:
- "length (sort cmp xs) = length xs"
+ \<open>length (sort cmp xs) = length xs\<close>
by (induction xs) simp_all
lemma sorted_sort [simp]:
- "sorted cmp (sort cmp xs)"
+ \<open>sorted cmp (sort cmp xs)\<close>
by (induction xs) (simp_all add: sorted_insort)
lemma stable_sort:
- "stable_segment cmp x (sort cmp xs) = stable_segment cmp x xs"
+ \<open>stable_segment cmp x (sort cmp xs) = stable_segment cmp x xs\<close>
by (induction xs) (simp_all add: stable_insort_equiv stable_insort_not_equiv)
lemma sort_remove1_eq [simp]:
- "sort cmp (remove1 x xs) = remove1 x (sort cmp xs)"
+ \<open>sort cmp (remove1 x xs) = remove1 x (sort cmp xs)\<close>
by (induction xs) simp_all
lemma set_insort [simp]:
- "set (insort cmp x xs) = insert x (set xs)"
+ \<open>set (insort cmp x xs) = insert x (set xs)\<close>
by (induction xs) auto
lemma set_sort [simp]:
- "set (sort cmp xs) = set xs"
+ \<open>set (sort cmp xs) = set xs\<close>
by (induction xs) auto
lemma sort_eqI:
- "sort cmp ys = xs"
- if permutation: "mset ys = mset xs"
- and sorted: "sorted cmp xs"
- and stable: "\<And>y. y \<in> set ys \<Longrightarrow>
- stable_segment cmp y ys = stable_segment cmp y xs"
+ \<open>sort cmp ys = xs\<close>
+ if permutation: \<open>mset ys = mset xs\<close>
+ and sorted: \<open>sorted cmp xs\<close>
+ and stable: \<open>\<And>y. y \<in> set ys \<Longrightarrow>
+ stable_segment cmp y ys = stable_segment cmp y xs\<close>
proof -
- have stable': "stable_segment cmp y ys =
- stable_segment cmp y xs" for y
- proof (cases "\<exists>x\<in>set ys. compare cmp y x = Equiv")
+ have stable': \<open>stable_segment cmp y ys =
+ stable_segment cmp y xs\<close> for y
+ proof (cases \<open>\<exists>x\<in>set ys. compare cmp y x = Equiv\<close>)
case True
- then obtain z where "z \<in> set ys" and "compare cmp y z = Equiv"
+ then obtain z where \<open>z \<in> set ys\<close> and \<open>compare cmp y z = Equiv\<close>
by auto
- then have "compare cmp y x = Equiv \<longleftrightarrow> compare cmp z x = Equiv" for x
+ then have \<open>compare cmp y x = Equiv \<longleftrightarrow> compare cmp z x = Equiv\<close> for x
by (meson compare.sym compare.trans_equiv)
- moreover have "stable_segment cmp z ys =
- stable_segment cmp z xs"
+ moreover have \<open>stable_segment cmp z ys =
+ stable_segment cmp z xs\<close>
using \<open>z \<in> set ys\<close> by (rule stable)
ultimately show ?thesis
by simp
next
case False
- moreover from permutation have "set ys = set xs"
+ moreover from permutation have \<open>set ys = set xs\<close>
by (rule mset_eq_setD)
ultimately show ?thesis
by simp
@@ -341,40 +341,40 @@
by simp
next
case (minimum x xs)
- from \<open>mset ys = mset xs\<close> have ys: "set ys = set xs"
+ from \<open>mset ys = mset xs\<close> have ys: \<open>set ys = set xs\<close>
by (rule mset_eq_setD)
- then have "compare cmp x y \<noteq> Greater" if "y \<in> set ys" for y
+ then have \<open>compare cmp x y \<noteq> Greater\<close> if \<open>y \<in> set ys\<close> for y
using that minimum.hyps by simp
- from minimum.prems have stable: "stable_segment cmp x ys = stable_segment cmp x xs"
+ from minimum.prems have stable: \<open>stable_segment cmp x ys = stable_segment cmp x xs\<close>
by simp
- have "sort cmp (remove1 x ys) = remove1 x xs"
+ have \<open>sort cmp (remove1 x ys) = remove1 x xs\<close>
by (rule minimum.IH) (simp_all add: minimum.prems filter_remove1)
- then have "remove1 x (sort cmp ys) = remove1 x xs"
+ then have \<open>remove1 x (sort cmp ys) = remove1 x xs\<close>
by simp
- then have "insort cmp x (remove1 x (sort cmp ys)) =
- insort cmp x (remove1 x xs)"
+ then have \<open>insort cmp x (remove1 x (sort cmp ys)) =
+ insort cmp x (remove1 x xs)\<close>
by simp
- also from minimum.hyps ys stable have "insort cmp x (remove1 x (sort cmp ys)) = sort cmp ys"
+ also from minimum.hyps ys stable have \<open>insort cmp x (remove1 x (sort cmp ys)) = sort cmp ys\<close>
by (simp add: stable_sort insort_remove1_same_eq)
- also from minimum.hyps have "insort cmp x (remove1 x xs) = xs"
+ also from minimum.hyps have \<open>insort cmp x (remove1 x xs) = xs\<close>
by (simp add: insort_remove1_same_eq)
finally show ?case .
qed
qed
lemma filter_insort:
- "filter P (insort cmp x xs) = insort cmp x (filter P xs)"
- if "sorted cmp xs" and "P x"
+ \<open>filter P (insort cmp x xs) = insort cmp x (filter P xs)\<close>
+ if \<open>sorted cmp xs\<close> and \<open>P x\<close>
using that by (induction xs)
(auto simp add: compare.trans_not_greater insort_eq_ConsI)
lemma filter_insort_triv:
- "filter P (insort cmp x xs) = filter P xs"
- if "\<not> P x"
+ \<open>filter P (insort cmp x xs) = filter P xs\<close>
+ if \<open>\<not> P x\<close>
using that by (induction xs) simp_all
lemma filter_sort:
- "filter P (sort cmp xs) = sort cmp (filter P xs)"
+ \<open>filter P (sort cmp xs) = sort cmp (filter P xs)\<close>
by (induction xs) (auto simp add: filter_insort filter_insort_triv)
@@ -382,80 +382,80 @@
subsection \<open>Quicksort\<close>
-definition quicksort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
- where quicksort_is_sort [simp]: "quicksort = sort"
+definition quicksort :: \<open>'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+ where quicksort_is_sort [simp]: \<open>quicksort = sort\<close>
lemma sort_by_quicksort:
- "sort = quicksort"
+ \<open>sort = quicksort\<close>
by simp
lemma sort_by_quicksort_rec:
- "sort cmp xs = sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Less]
+ \<open>sort cmp xs = sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Less]
@ stable_segment cmp (xs ! (length xs div 2)) xs
- @ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "_ = ?rhs")
+ @ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]\<close> (is \<open>_ = ?rhs\<close>)
proof (rule sort_eqI)
- show "mset xs = mset ?rhs"
+ show \<open>mset xs = mset ?rhs\<close>
by (rule multiset_eqI) (auto simp add: compare.sym intro: comp.exhaust)
next
- show "sorted cmp ?rhs"
+ show \<open>sorted cmp ?rhs\<close>
by (auto simp add: sorted_append_iff sorted_stable_segment compare.equiv_subst_right dest: compare.trans_greater)
next
- let ?pivot = "xs ! (length xs div 2)"
+ let ?pivot = \<open>xs ! (length xs div 2)\<close>
fix l
- have "compare cmp x ?pivot = comp \<and> compare cmp l x = Equiv
- \<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv" for x comp
+ have \<open>compare cmp x ?pivot = comp \<and> compare cmp l x = Equiv
+ \<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv\<close> for x comp
proof -
- have "compare cmp x ?pivot = comp \<longleftrightarrow> compare cmp l ?pivot = comp"
- if "compare cmp l x = Equiv"
+ have \<open>compare cmp x ?pivot = comp \<longleftrightarrow> compare cmp l ?pivot = comp\<close>
+ if \<open>compare cmp l x = Equiv\<close>
using that by (simp add: compare.equiv_subst_left compare.sym)
then show ?thesis by blast
qed
- then show "stable_segment cmp l xs = stable_segment cmp l ?rhs"
+ then show \<open>stable_segment cmp l xs = stable_segment cmp l ?rhs\<close>
by (simp add: stable_sort compare.sym [of _ ?pivot])
- (cases "compare cmp l ?pivot", simp_all)
+ (cases \<open>compare cmp l ?pivot\<close>, simp_all)
qed
context
begin
-qualified definition partition :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list"
- where "partition cmp pivot xs =
- ([x \<leftarrow> xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \<leftarrow> xs. compare cmp x pivot = Greater])"
+qualified definition partition :: \<open>'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list\<close>
+ where \<open>partition cmp pivot xs =
+ ([x \<leftarrow> xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \<leftarrow> xs. compare cmp x pivot = Greater])\<close>
qualified lemma partition_code [code]:
- "partition cmp pivot [] = ([], [], [])"
- "partition cmp pivot (x # xs) =
+ \<open>partition cmp pivot [] = ([], [], [])\<close>
+ \<open>partition cmp pivot (x # xs) =
(let (lts, eqs, gts) = partition cmp pivot xs
in case compare cmp x pivot of
Less \<Rightarrow> (x # lts, eqs, gts)
| Equiv \<Rightarrow> (lts, x # eqs, gts)
- | Greater \<Rightarrow> (lts, eqs, x # gts))"
+ | Greater \<Rightarrow> (lts, eqs, x # gts))\<close>
using comp.exhaust by (auto simp add: partition_def Let_def compare.sym [of _ pivot])
lemma quicksort_code [code]:
- "quicksort cmp xs =
+ \<open>quicksort cmp xs =
(case xs of
[] \<Rightarrow> []
| [x] \<Rightarrow> xs
| [x, y] \<Rightarrow> (if compare cmp x y \<noteq> Greater then xs else [y, x])
| _ \<Rightarrow>
let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs
- in quicksort cmp lts @ eqs @ quicksort cmp gts)"
-proof (cases "length xs \<ge> 3")
+ in quicksort cmp lts @ eqs @ quicksort cmp gts)\<close>
+proof (cases \<open>length xs \<ge> 3\<close>)
case False
- then have "length xs \<in> {0, 1, 2}"
+ then have \<open>length xs \<in> {0, 1, 2}\<close>
by (auto simp add: not_le le_less less_antisym)
- then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]"
+ then consider \<open>xs = []\<close> | x where \<open>xs = [x]\<close> | x y where \<open>xs = [x, y]\<close>
by (auto simp add: length_Suc_conv numeral_2_eq_2)
then show ?thesis
by cases simp_all
next
case True
- then obtain x y z zs where "xs = x # y # z # zs"
+ then obtain x y z zs where \<open>xs = x # y # z # zs\<close>
by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3)
- moreover have "quicksort cmp xs =
+ moreover have \<open>quicksort cmp xs =
(let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs
- in quicksort cmp lts @ eqs @ quicksort cmp gts)"
+ in quicksort cmp lts @ eqs @ quicksort cmp gts)\<close>
using sort_by_quicksort_rec [of cmp xs] by (simp add: partition_def)
ultimately show ?thesis
by simp
@@ -466,38 +466,38 @@
subsection \<open>Mergesort\<close>
-definition mergesort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
- where mergesort_is_sort [simp]: "mergesort = sort"
+definition mergesort :: \<open>'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+ where mergesort_is_sort [simp]: \<open>mergesort = sort\<close>
lemma sort_by_mergesort:
- "sort = mergesort"
+ \<open>sort = mergesort\<close>
by simp
context
- fixes cmp :: "'a comparator"
+ fixes cmp :: \<open>'a comparator\<close>
begin
-qualified function merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
- where "merge [] ys = ys"
- | "merge xs [] = xs"
- | "merge (x # xs) (y # ys) = (if compare cmp x y = Greater
- then y # merge (x # xs) ys else x # merge xs (y # ys))"
+qualified function merge :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+ where \<open>merge [] ys = ys\<close>
+ | \<open>merge xs [] = xs\<close>
+ | \<open>merge (x # xs) (y # ys) = (if compare cmp x y = Greater
+ then y # merge (x # xs) ys else x # merge xs (y # ys))\<close>
by pat_completeness auto
qualified termination by lexicographic_order
lemma mset_merge:
- "mset (merge xs ys) = mset xs + mset ys"
+ \<open>mset (merge xs ys) = mset xs + mset ys\<close>
by (induction xs ys rule: merge.induct) simp_all
lemma merge_eq_Cons_imp:
- "xs \<noteq> [] \<and> z = hd xs \<or> ys \<noteq> [] \<and> z = hd ys"
- if "merge xs ys = z # zs"
+ \<open>xs \<noteq> [] \<and> z = hd xs \<or> ys \<noteq> [] \<and> z = hd ys\<close>
+ if \<open>merge xs ys = z # zs\<close>
using that by (induction xs ys rule: merge.induct) (auto split: if_splits)
lemma filter_merge:
- "filter P (merge xs ys) = merge (filter P xs) (filter P ys)"
- if "sorted cmp xs" and "sorted cmp ys"
+ \<open>filter P (merge xs ys) = merge (filter P xs) (filter P ys)\<close>
+ if \<open>sorted cmp xs\<close> and \<open>sorted cmp ys\<close>
using that proof (induction xs ys rule: merge.induct)
case (1 ys)
then show ?case
@@ -509,47 +509,47 @@
next
case (3 x xs y ys)
show ?case
- proof (cases "compare cmp x y = Greater")
+ proof (cases \<open>compare cmp x y = Greater\<close>)
case True
- with 3 have hyp: "filter P (merge (x # xs) ys) =
- merge (filter P (x # xs)) (filter P ys)"
+ with 3 have hyp: \<open>filter P (merge (x # xs) ys) =
+ merge (filter P (x # xs)) (filter P ys)\<close>
by (simp add: sorted_Cons_imp_sorted)
show ?thesis
- proof (cases "\<not> P x \<and> P y")
+ proof (cases \<open>\<not> P x \<and> P y\<close>)
case False
with \<open>compare cmp x y = Greater\<close> show ?thesis
by (auto simp add: hyp)
next
case True
from \<open>compare cmp x y = Greater\<close> "3.prems"
- have *: "compare cmp z y = Greater" if "z \<in> set (filter P xs)" for z
+ have *: \<open>compare cmp z y = Greater\<close> if \<open>z \<in> set (filter P xs)\<close> for z
using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less)
from \<open>compare cmp x y = Greater\<close> show ?thesis
- by (cases "filter P xs") (simp_all add: hyp *)
+ by (cases \<open>filter P xs\<close>) (simp_all add: hyp *)
qed
next
case False
- with 3 have hyp: "filter P (merge xs (y # ys)) =
- merge (filter P xs) (filter P (y # ys))"
+ with 3 have hyp: \<open>filter P (merge xs (y # ys)) =
+ merge (filter P xs) (filter P (y # ys))\<close>
by (simp add: sorted_Cons_imp_sorted)
show ?thesis
- proof (cases "P x \<and> \<not> P y")
+ proof (cases \<open>P x \<and> \<not> P y\<close>)
case False
with \<open>compare cmp x y \<noteq> Greater\<close> show ?thesis
by (auto simp add: hyp)
next
case True
from \<open>compare cmp x y \<noteq> Greater\<close> "3.prems"
- have *: "compare cmp x z \<noteq> Greater" if "z \<in> set (filter P ys)" for z
+ have *: \<open>compare cmp x z \<noteq> Greater\<close> if \<open>z \<in> set (filter P ys)\<close> for z
using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less)
from \<open>compare cmp x y \<noteq> Greater\<close> show ?thesis
- by (cases "filter P ys") (simp_all add: hyp *)
+ by (cases \<open>filter P ys\<close>) (simp_all add: hyp *)
qed
qed
qed
lemma sorted_merge:
- "sorted cmp (merge xs ys)" if "sorted cmp xs" and "sorted cmp ys"
+ \<open>sorted cmp (merge xs ys)\<close> if \<open>sorted cmp xs\<close> and \<open>sorted cmp ys\<close>
using that proof (induction xs ys rule: merge.induct)
case (1 ys)
then show ?case
@@ -561,15 +561,15 @@
next
case (3 x xs y ys)
show ?case
- proof (cases "compare cmp x y = Greater")
+ proof (cases \<open>compare cmp x y = Greater\<close>)
case True
- with 3 have "sorted cmp (merge (x # xs) ys)"
+ with 3 have \<open>sorted cmp (merge (x # xs) ys)\<close>
by (simp add: sorted_Cons_imp_sorted)
- then have "sorted cmp (y # merge (x # xs) ys)"
+ then have \<open>sorted cmp (y # merge (x # xs) ys)\<close>
proof (rule sorted_ConsI)
fix z zs
- assume "merge (x # xs) ys = z # zs"
- with 3(4) True show "compare cmp y z \<noteq> Greater"
+ assume \<open>merge (x # xs) ys = z # zs\<close>
+ with 3(4) True show \<open>compare cmp y z \<noteq> Greater\<close>
by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp)
(auto simp add: compare.asym_greater sorted_Cons_imp_not_less)
qed
@@ -577,13 +577,13 @@
by simp
next
case False
- with 3 have "sorted cmp (merge xs (y # ys))"
+ with 3 have \<open>sorted cmp (merge xs (y # ys))\<close>
by (simp add: sorted_Cons_imp_sorted)
- then have "sorted cmp (x # merge xs (y # ys))"
+ then have \<open>sorted cmp (x # merge xs (y # ys))\<close>
proof (rule sorted_ConsI)
fix z zs
- assume "merge xs (y # ys) = z # zs"
- with 3(3) False show "compare cmp x z \<noteq> Greater"
+ assume \<open>merge xs (y # ys) = z # zs\<close>
+ with 3(3) False show \<open>compare cmp x z \<noteq> Greater\<close>
by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp)
(auto simp add: compare.asym_greater sorted_Cons_imp_not_less)
qed
@@ -593,45 +593,45 @@
qed
lemma merge_eq_appendI:
- "merge xs ys = xs @ ys"
- if "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> compare cmp x y \<noteq> Greater"
+ \<open>merge xs ys = xs @ ys\<close>
+ if \<open>\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> compare cmp x y \<noteq> Greater\<close>
using that by (induction xs ys rule: merge.induct) simp_all
lemma merge_stable_segments:
- "merge (stable_segment cmp l xs) (stable_segment cmp l ys) =
- stable_segment cmp l xs @ stable_segment cmp l ys"
+ \<open>merge (stable_segment cmp l xs) (stable_segment cmp l ys) =
+ stable_segment cmp l xs @ stable_segment cmp l ys\<close>
by (rule merge_eq_appendI) (auto dest: compare.trans_equiv_greater)
lemma sort_by_mergesort_rec:
- "sort cmp xs =
+ \<open>sort cmp xs =
merge (sort cmp (take (length xs div 2) xs))
- (sort cmp (drop (length xs div 2) xs))" (is "_ = ?rhs")
+ (sort cmp (drop (length xs div 2) xs))\<close> (is \<open>_ = ?rhs\<close>)
proof (rule sort_eqI)
- have "mset (take (length xs div 2) xs) + mset (drop (length xs div 2) xs) =
- mset (take (length xs div 2) xs @ drop (length xs div 2) xs)"
+ have \<open>mset (take (length xs div 2) xs) + mset (drop (length xs div 2) xs) =
+ mset (take (length xs div 2) xs @ drop (length xs div 2) xs)\<close>
by (simp only: mset_append)
- then show "mset xs = mset ?rhs"
+ then show \<open>mset xs = mset ?rhs\<close>
by (simp add: mset_merge)
next
- show "sorted cmp ?rhs"
+ show \<open>sorted cmp ?rhs\<close>
by (simp add: sorted_merge)
next
fix l
- have "stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)
- = stable_segment cmp l xs"
+ have \<open>stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)
+ = stable_segment cmp l xs\<close>
by (simp only: filter_append [symmetric] append_take_drop_id)
- have "merge (stable_segment cmp l (take (length xs div 2) xs))
+ have \<open>merge (stable_segment cmp l (take (length xs div 2) xs))
(stable_segment cmp l (drop (length xs div 2) xs)) =
- stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)"
+ stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)\<close>
by (rule merge_eq_appendI) (auto simp add: compare.trans_equiv_greater)
- also have "\<dots> = stable_segment cmp l xs"
+ also have \<open>\<dots> = stable_segment cmp l xs\<close>
by (simp only: filter_append [symmetric] append_take_drop_id)
- finally show "stable_segment cmp l xs = stable_segment cmp l ?rhs"
+ finally show \<open>stable_segment cmp l xs = stable_segment cmp l ?rhs\<close>
by (simp add: stable_sort filter_merge)
qed
lemma mergesort_code [code]:
- "mergesort cmp xs =
+ \<open>mergesort cmp xs =
(case xs of
[] \<Rightarrow> []
| [x] \<Rightarrow> xs
@@ -641,25 +641,25 @@
half = length xs div 2;
ys = take half xs;
zs = drop half xs
- in merge (mergesort cmp ys) (mergesort cmp zs))"
-proof (cases "length xs \<ge> 3")
+ in merge (mergesort cmp ys) (mergesort cmp zs))\<close>
+proof (cases \<open>length xs \<ge> 3\<close>)
case False
- then have "length xs \<in> {0, 1, 2}"
+ then have \<open>length xs \<in> {0, 1, 2}\<close>
by (auto simp add: not_le le_less less_antisym)
- then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]"
+ then consider \<open>xs = []\<close> | x where \<open>xs = [x]\<close> | x y where \<open>xs = [x, y]\<close>
by (auto simp add: length_Suc_conv numeral_2_eq_2)
then show ?thesis
by cases simp_all
next
case True
- then obtain x y z zs where "xs = x # y # z # zs"
+ then obtain x y z zs where \<open>xs = x # y # z # zs\<close>
by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3)
- moreover have "mergesort cmp xs =
+ moreover have \<open>mergesort cmp xs =
(let
half = length xs div 2;
ys = take half xs;
zs = drop half xs
- in merge (mergesort cmp ys) (mergesort cmp zs))"
+ in merge (mergesort cmp ys) (mergesort cmp zs))\<close>
using sort_by_mergesort_rec [of xs] by (simp add: Let_def)
ultimately show ?thesis
by simp
--- a/src/HOL/Tools/SMT/verit_isar.ML Mon Mar 31 22:46:11 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/Tools/SMT/verit_isar.ML
- Author: Mathias Fleury, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-VeriT proofs as generic ATP proofs for Isar proof reconstruction.
-*)
-
-signature VERIT_ISAR =
-sig
- type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
- val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term ->
- (string * term) list -> int list -> int -> (int * string) list -> Verit_Proof.veriT_step list ->
- (term, string) ATP_Proof.atp_step list
-end;
-
-structure VeriT_Isar: VERIT_ISAR =
-struct
-
-open ATP_Util
-open ATP_Problem
-open ATP_Proof
-open ATP_Proof_Reconstruct
-open SMTLIB_Interface
-open SMTLIB_Isar
-open Verit_Proof
-
-fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
- conjecture_id fact_helper_ids =
- let
- fun steps_of (Verit_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
- let
- val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl
- fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems)
- in
- if rule = input_rule then
- let
- val id_num = snd (SMTLIB_Interface.role_and_index_of_assert_name id)
- val ss = the_list (AList.lookup (op =) fact_helper_ids id_num)
- in
- (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids
- fact_helper_ts hyp_ts concl_t of
- NONE => []
- | SOME (role0, concl00) =>
- let
- val name0 = (id ^ "a", ss)
- val concl0 = unskolemize_names ctxt concl00
- in
- [(name0, role0, concl0, rule, []),
- ((id, []), Plain, concl', rewrite_rule,
- name0 :: normalizing_prems ctxt concl0)]
- end)
- end
- else
- [standard_step (if null prems then Lemma else Plain)]
- end
- in
- maps steps_of
- end
-
-end;
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML Mon Mar 31 22:46:11 2025 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: HOL/Tools/SMT/verit_proof_parse.ML
- Author: Mathias Fleury, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-VeriT proof parsing.
-*)
-
-signature VERIT_PROOF_PARSE =
-sig
- type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
- val parse_proof: SMT_Translate.replay_data ->
- ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
- SMT_Solver.parsed_proof
-end;
-
-structure VeriT_Proof_Parse: VERIT_PROOF_PARSE =
-struct
-
-open ATP_Util
-open ATP_Problem
-open ATP_Proof
-open ATP_Proof_Reconstruct
-open VeriT_Isar
-open Verit_Proof
-
-fun add_used_asserts_in_step (Verit_Proof.VeriT_Step {prems, ...}) =
- union (op =) (map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) prems)
-
-fun parse_proof
- ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data)
- xfacts prems concl output =
- let
- val num_ll_defs = length ll_defs
-
- val id_of_index = Integer.add num_ll_defs
- val index_of_id = Integer.add (~ num_ll_defs)
-
- fun step_of_assume j ((_, role), th) =
- Verit_Proof.VeriT_Step
- {id = SMTLIB_Interface.assert_name_of_role_and_index role (id_of_index j),
- rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []}
-
- val (actual_steps, _) = Verit_Proof.parse typs terms output ctxt
- val used_assert_ids = fold add_used_asserts_in_step actual_steps []
- val used_assm_js =
- map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
- used_assert_ids
- val used_assms = map (nth assms) used_assm_js
- val assm_steps = map2 step_of_assume used_assm_js used_assms
- val steps = assm_steps @ actual_steps
-
- val conjecture_i = 0
- val prems_i = conjecture_i + 1
- val num_prems = length prems
- val facts_i = prems_i + num_prems
- val num_facts = length xfacts
- val helpers_i = facts_i + num_facts
-
- val conjecture_id = id_of_index conjecture_i
- val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1)
- val fact_ids' =
- map_filter (fn j =>
- let val ((i, _), _) = nth assms j in
- try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
- end) used_assm_js
- val helper_ids' =
- map_filter (fn ((i, _), thm) => if i >= helpers_i then SOME (i, thm) else NONE) used_assms
-
- val fact_helper_ts =
- map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @
- map (fn (_, ((s, _), th)) => (s, Thm.prop_of th)) fact_ids'
- val fact_helper_ids' =
- map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids' @ map (apsnd (fst o fst)) fact_ids'
- in
- {outcome = NONE, fact_ids = SOME fact_ids',
- atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl
- fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Mar 31 22:46:11 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Mar 31 22:46:18 2025 +0100
@@ -220,7 +220,7 @@
| apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
(* FIXME *)
-fun proof_method_command meth i n used_chaineds extras =
+fun proof_method_command meth i n extras =
let
val (indirect_facts, direct_facts) =
if is_proof_method_direct meth then ([], extras) else (extras, [])
@@ -247,9 +247,9 @@
Markup.markup (Markup.break {width = 1, indent = 2}) " ")
fun one_line_proof_text ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
- let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
+ let val extra = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts in
map fst extra
- |> proof_method_command meth subgoal subgoal_count (map fst chained)
+ |> proof_method_command meth subgoal subgoal_count
|> (if play = Play_Failed then failed_command_line else try_command_line banner play)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Mon Mar 31 22:46:11 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Mon Mar 31 22:46:18 2025 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
Author: Jasmin Blanchette, LMU Muenchen
+ Author: Martin Desharnais, LMU Muenchen
Isabelle tactics as Sledgehammer provers.
*)
@@ -11,21 +12,6 @@
type prover = Sledgehammer_Prover.prover
type base_slice = Sledgehammer_ATP_Systems.base_slice
- val algebraN : string
- val argoN : string
- val autoN : string
- val blastN : string
- val fastforceN : string
- val forceN : string
- val linarithN : string
- val mesonN : string
- val metisN : string
- val orderN : string
- val presburgerN : string
- val satxN : string
- val simpN : string
-
- val tactic_provers : string list
val is_tactic_prover : string -> bool
val good_slices_of_tactic_prover : string -> base_slice list
val run_tactic_prover : mode -> string -> prover
@@ -34,31 +20,11 @@
structure Sledgehammer_Prover_Tactic : SLEDGEHAMMER_PROVER_TACTIC =
struct
-open ATP_Problem_Generate
open ATP_Proof
-open Sledgehammer_ATP_Systems
open Sledgehammer_Proof_Methods
open Sledgehammer_Prover
-val algebraN = "algebra"
-val argoN = "argo"
-val autoN = "auto"
-val blastN = "blast"
-val fastforceN = "fastforce"
-val forceN = "force"
-val linarithN = "linarith"
-val mesonN = "meson"
-val metisN = "metis"
-val orderN = "order"
-val presburgerN = "presburger"
-val satxN = "satx"
-val simpN = "simp"
-
-val tactic_provers =
- [algebraN, argoN, autoN, blastN, fastforceN, forceN, linarithN, mesonN,
- metisN, orderN, presburgerN, satxN, simpN]
-
-val is_tactic_prover = member (op =) tactic_provers
+val is_tactic_prover : string -> bool = is_some o Try0.get_proof_method
val meshN = "mesh"
@@ -69,24 +35,23 @@
(1, false, false, 8, meshN),
(1, false, false, 32, meshN)]
-fun meth_of name =
- if name = algebraN then Algebra_Method
- else if name = argoN then Argo_Method
- else if name = autoN then Auto_Method
- else if name = blastN then Blast_Method
- else if name = fastforceN then Fastforce_Method
- else if name = forceN then Force_Method
- else if name = linarithN then Linarith_Method
- else if name = mesonN then Meson_Method
- else if name = metisN then Metis_Method (NONE, NONE, [])
- else if name = orderN then Order_Method
- else if name = presburgerN then Presburger_Method
- else if name = satxN then SATx_Method
- else if name = simpN then Simp_Method
- else error ("Unknown tactic: " ^ quote name)
+fun meth_of "algebra" = Algebra_Method
+ | meth_of "argo" = Argo_Method
+ | meth_of "auto" = Auto_Method
+ | meth_of "blast" = Blast_Method
+ | meth_of "fastforce" = Fastforce_Method
+ | meth_of "force" = Force_Method
+ | meth_of "linarith" = Linarith_Method
+ | meth_of "meson" = Meson_Method
+ | meth_of "metis" = Metis_Method (NONE, NONE, [])
+ | meth_of "order" = Order_Method
+ | meth_of "presburger" = Presburger_Method
+ | meth_of "satx" = SATx_Method
+ | meth_of "simp" = Simp_Method
+ | meth_of _ = Metis_Method (NONE, NONE, [])
fun run_tactic_prover mode name ({slices, timeout, ...} : params)
- ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
+ ({state, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
let
val (basic_slice as (slice_size, _, _, _, _), No_Slice) = slice
val facts = facts_of_basic_slice basic_slice factss
--- a/src/Tools/Code/code_printer.ML Mon Mar 31 22:46:11 2025 +0100
+++ b/src/Tools/Code/code_printer.ML Mon Mar 31 22:46:18 2025 +0100
@@ -9,7 +9,6 @@
type itype = Code_Thingol.itype
type iterm = Code_Thingol.iterm
type const = Code_Thingol.const
- type dict = Code_Thingol.dict
val eqn_error: theory -> thm option -> string -> 'a
--- a/src/Tools/Code/code_target.ML Mon Mar 31 22:46:11 2025 +0100
+++ b/src/Tools/Code/code_target.ML Mon Mar 31 22:46:18 2025 +0100
@@ -9,9 +9,6 @@
val cert_tyco: Proof.context -> string -> string
val read_tyco: Proof.context -> string -> string
- datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
- val next_export: theory -> string * theory
-
val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string
-> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list
-> local_theory -> local_theory
@@ -47,16 +44,18 @@
-> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-> ((string list * Bytes.T) list * string) * (Code_Symbol.T -> string option)
+ datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
type serializer
- type literals = Code_Printer.literals
type language
type ancestry
val assert_target: theory -> string -> string
val add_language: string * language -> theory -> theory
val add_derived_target: string * ancestry -> theory -> theory
- val the_literals: Proof.context -> string -> literals
+ val the_literals: Proof.context -> string -> Code_Printer.literals
+
val parse_args: 'a parser -> Token.T list -> 'a
val default_code_width: int Config.T
+ val next_export: theory -> string * theory
type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
@@ -72,7 +71,6 @@
open Basic_Code_Symbol;
open Basic_Code_Thingol;
-type literals = Code_Printer.literals;
type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl =
(string * (string * 'a option) list, string * (string * 'b option) list,
class * (string * 'c option) list, (class * class) * (string * 'd option) list,
@@ -172,7 +170,7 @@
-> Code_Symbol.T list
-> pretty_modules * (Code_Symbol.T -> string option);
-type language = {serializer: serializer, literals: literals,
+type language = {serializer: serializer, literals: Code_Printer.literals,
check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
evaluation_args: Token.T list};