feat(*) bump isabelle version + required changes

AFP_VERSION

@@ -1 +1 @@
-56a32058201c086e05604a44bd5e8713b312e86c
+d3b63921557cc38bb6b3fda0a139279ffca49c81

HOTG/Arithmetics/HOTG_Addition.thy

@@ -7,9 +7,9 @@ theory HOTG_Addition
     HOTG_Epsilon_Recursion
 begin
 
-unbundle
-  no_HOL_groups_syntax
-  no_HOL_order_syntax
+unbundle no HOL_groups_syntax
+  and no HOL_order_syntax
+  and no HOL_ascii_syntax
 
 paragraph \<open>Summary\<close>
 text \<open>Translation of generalised set addition from \<^cite>\<open>kirby_set_arithemtics\<close> and
@@ -18,11 +18,7 @@ monotone and injective in the second argument, but it is not commutative.\<close
 
 definition "add X \<equiv> mem_rec (\<lambda>addX Y. X \<union> image addX Y)"
 
-bundle hotg_add_syntax begin notation add (infixl "+" 65) end
-bundle no_hotg_add_syntax begin no_notation add (infixl "+" 65) end
-unbundle
-  hotg_add_syntax
-  no_HOL_ascii_syntax
+open_bundle hotg_add_syntax begin notation add (infixl "+" 65) end
 
 lemma add_eq_bin_union_repl_add: "X + Y = X \<union> {X + y | y \<in> Y}"
   unfolding add_def supply mem_rec_eq[uhint] by (urule refl)

HOTG/Arithmetics/HOTG_Arithmetics_Cardinal_Arithmetics.thy

@@ -10,8 +10,8 @@ theory HOTG_Arithmetics_Cardinal_Arithmetics
     HOTG_Multiplication
 begin
 
-unbundle no_HOL_groups_syntax
-unbundle no_HOL_order_syntax
+unbundle no HOL_groups_syntax
+  and no HOL_order_syntax
 
 lemma cardinality_lift_eq_cardinality_right [simp]: "|lift X Y| = |Y|"
 proof (intro cardinality_eq_if_equipollent equipollentI)

HOTG/Arithmetics/HOTG_Multiplication.thy

@@ -9,7 +9,7 @@ theory HOTG_Multiplication
     HOTG_Ranks
 begin
 
-unbundle no_HOL_groups_syntax
+unbundle no HOL_groups_syntax
 
 paragraph \<open>Summary\<close>
 text \<open>Translation of generalised set multiplication for sets from \<^cite>\<open>kirby_set_arithemtics\<close>
@@ -18,9 +18,7 @@ but it is not commutative (not proven here).\<close>
 
 definition "mul X \<equiv> mem_rec (\<lambda>mulX Y. \<Union>y \<in> Y. lift (mulX y) X)"
 
-bundle hotg_mul_syntax begin notation mul (infixl "*" 70) end
-bundle no_hotg_mul_syntax begin no_notation mul (infixl "*" 70) end
-unbundle hotg_mul_syntax
+open_bundle hotg_mul_syntax begin notation mul (infixl "*" 70) end
 
 lemma mul_eq_idx_union_lift_mul: "X * Y = (\<Union>y \<in> Y. lift (X * y) X)"
   unfolding mul_def by (urule mem_rec_eq)

HOTG/Binary_Relations/HOTG_Binary_Relations_Base.thy

@@ -8,7 +8,7 @@ theory HOTG_Binary_Relations_Base
     Transport.Dependent_Binary_Relations
 begin
 
-unbundle no_HOL_ascii_syntax
+unbundle no HOL_ascii_syntax
 
 definition "rel R x y \<equiv> \<langle>x, y\<rangle> \<in> R"
 

HOTG/Binary_Relations/Recursions/HOTG_Epsilon_Recursion.thy

@@ -8,10 +8,10 @@ theory HOTG_Epsilon_Recursion
     Transport.Wellfounded_Transitive_Recursion
 begin
 
-unbundle no_HOL_order_syntax
+unbundle no HOL_order_syntax
 
 context
-  includes fun_restrict_syntax no_rel_restrict_syntax
+  includes fun_restrict_syntax and no rel_restrict_syntax
 begin
 
 definition mem_rec :: "((set \<Rightarrow> 'a) \<Rightarrow> set \<Rightarrow> 'a) \<Rightarrow> set \<Rightarrow> 'a" where

HOTG/Cardinals/HOTG_Cardinals_Addition.thy

@@ -7,7 +7,7 @@ theory HOTG_Cardinals_Addition
     HOTG_Coproduct
 begin
 
-unbundle no_HOL_groups_syntax
+unbundle no HOL_groups_syntax
 
 paragraph \<open>Summary\<close>
 text \<open>Cardinal addition is the cardinality of the disjoint union of two sets.
@@ -16,9 +16,7 @@ We also derive the connection between set addition and cardinal addition.\<close
 
 definition "cardinal_add X Y \<equiv> |X \<Coprod> Y|"
 
-bundle hotg_cardinal_add_syntax begin notation cardinal_add (infixl "\<oplus>" 65) end
-bundle no_hotg_cardinal_add_syntax begin no_notation cardinal_add (infixl "\<oplus>" 65) end
-unbundle hotg_cardinal_add_syntax
+open_bundle hotg_cardinal_add_syntax begin notation cardinal_add (infixl "\<oplus>" 65) end
 
 lemma cardinal_add_eq_cardinality_coprod: "X \<oplus> Y = |X \<Coprod> Y|"
   unfolding cardinal_add_def ..

HOTG/Cardinals/HOTG_Cardinals_Base.thy

@@ -10,8 +10,8 @@ theory HOTG_Cardinals_Base
     HOTG_Less_Than
 begin
 
-unbundle no_HOL_groups_syntax
-unbundle no_HOL_order_syntax
+unbundle no HOL_groups_syntax
+  and no HOL_order_syntax
 
 paragraph \<open>Summary\<close>
 text \<open>Translation of cardinality from HOL-Library and \<^cite>\<open>ZFC_in_HOL_AFP\<close>.
@@ -22,9 +22,7 @@ Further details can be found in \<^url>\<open>https://en.wikipedia.org/wiki/Card
 
 definition "cardinality (X :: set) \<equiv> least_wrt_rel (\<le>) (ordinal \<sqinter> ((\<approx>) X))"
 
-bundle hotg_cardinality_syntax begin notation cardinality ("|_|") end
-bundle no_hotg_cardinality_syntax begin no_notation cardinality ("|_|") end
-unbundle hotg_cardinality_syntax
+open_bundle hotg_cardinality_syntax begin notation cardinality ("|_|") end
 
 lemma cardinality_eq_if_equipollent_if_le_if_ordinal:
   assumes "ordinal Y"

HOTG/Cardinals/HOTG_Cardinals_Multiplication.thy

@@ -4,13 +4,11 @@ theory HOTG_Cardinals_Multiplication
   imports HOTG_Cardinals_Base HOTG_Pairs
 begin
 
-unbundle no_HOL_groups_syntax
+unbundle no HOL_groups_syntax
 
 definition "cardinal_mul X Y \<equiv> |X \<times> Y|"
 
-bundle hotg_cardinal_mul_syntax begin notation cardinal_mul (infixl "\<otimes>" 65) end
-bundle no_hotg_cardinal_mul_syntax begin no_notation cardinal_mul (infixl "\<otimes>" 65) end
-unbundle hotg_cardinal_mul_syntax
+open_bundle hotg_cardinal_mul_syntax begin notation cardinal_mul (infixl "\<otimes>" 65) end
 
 lemma cardinal_mul_eq_cardinality_pair: "X \<otimes> Y = |X \<times> Y|"
   unfolding cardinal_mul_def ..

HOTG/Equipollence/HOTG_Equipollence_Base.thy

@@ -15,9 +15,7 @@ We show that equipollence is an equivalence relation.\<close>
 definition "equipollent (X :: set) (Y :: set) \<equiv>
   \<exists>(f :: set \<Rightarrow> set) (g :: set \<Rightarrow> set). bijection_on X Y f g"
 
-bundle hotg_equipollent_syntax begin notation equipollent (infixl "\<approx>" 50) end
-bundle no_hotg_equipollent_syntax begin no_notation equipollent (infixl "\<approx>" 50) end
-unbundle hotg_equipollent_syntax
+open_bundle hotg_equipollent_syntax begin notation equipollent (infixl "\<approx>" 50) end
 
 lemma equipollentI [intro]:
   assumes "bijection_on X Y (f :: set \<Rightarrow> set) (g :: set \<Rightarrow> set)"

HOTG/Functions/HOTG_Clean_Functions.thy

@@ -10,7 +10,7 @@ theory HOTG_Clean_Functions
     Transport.Binary_Relations_Clean_Functions
 begin
 
-unbundle no_HOL_ascii_syntax
+unbundle no HOL_ascii_syntax
 
 definition "crel_dep_mono_wrt_set A B :: (set \<Rightarrow> set \<Rightarrow> bool) \<Rightarrow> bool \<equiv> (x : mem_of A) \<rightarrow>\<^sub>c mem_of (B x)"
 adhoc_overloading crel_dep_mono_wrt crel_dep_mono_wrt_set

HOTG/Functions/HOTG_Functions_Base.thy

@@ -6,7 +6,7 @@ theory HOTG_Functions_Base
     Transport.Binary_Relations_Function_Base
 begin
 
-unbundle no_HOL_ascii_syntax
+unbundle no HOL_ascii_syntax
 
 definition "rel_dep_mono_wrt_set A B :: (set \<Rightarrow> set \<Rightarrow> bool) \<Rightarrow> bool \<equiv> (x : mem_of A) \<rightarrow> mem_of (B x)"
 adhoc_overloading rel_dep_mono_wrt rel_dep_mono_wrt_set

HOTG/Functions/HOTG_Functions_Evaluation.thy

@@ -7,7 +7,7 @@ theory HOTG_Functions_Evaluation
     Transport.Binary_Relations_Function_Evaluation
 begin
 
-unbundle no_HOL_ascii_syntax
+unbundle no HOL_ascii_syntax
 
 subsubsection \<open>Evaluation\<close>
 

HOTG/Functions/HOTG_Functions_Lambda.thy

@@ -8,7 +8,7 @@ theory HOTG_Functions_Lambda
     ML_Unification.Unification_Attributes
 begin
 
-unbundle no_HOL_ascii_syntax
+unbundle no HOL_ascii_syntax
 
 definition "rel_lambda_set A :: (set \<Rightarrow> 'a) \<Rightarrow> set \<Rightarrow> 'a \<Rightarrow> bool \<equiv> rel_lambda (mem_of A)"
 adhoc_overloading rel_lambda rel_lambda_set

HOTG/Functions/HOTG_Functions_Power.thy

@@ -7,9 +7,7 @@ begin
 definition fun_pow :: "('a \<Rightarrow> 'a) \<Rightarrow> set \<Rightarrow> ('a \<Rightarrow> 'a)" where
   "fun_pow f = omega_rec id ((\<circ>) f)"
 
-bundle hotg_fun_pow_syntax begin notation fun_pow ("(_)\<^bsup>(_)\<^esup>" [1000]) end
-bundle no_hotg_fun_pow_syntax begin no_notation fun_pow ("(_)\<^bsup>(_)\<^esup>" [1000]) end
-unbundle hotg_fun_pow_syntax
+open_bundle hotg_fun_pow_syntax begin notation fun_pow ("(_)\<^bsup>(_)\<^esup>" [1000]) end
 
 lemma fun_pow_zero_eq_id [simp]: "f\<^bsup>0\<^esup> = id"
   unfolding fun_pow_def omega_rec_zero by auto

HOTG/Functions/HOTG_Functions_Restrict.thy

@@ -5,10 +5,10 @@ theory HOTG_Functions_Restrict
     Transport.Functions_Restrict
 begin
 
-unbundle no_HOL_ascii_syntax
+unbundle no HOL_ascii_syntax
 
 context
-  includes fun_restrict_syntax no_rel_restrict_syntax
+  includes fun_restrict_syntax and no rel_restrict_syntax
 begin
 
 definition "fun_restrict_set f A \<equiv> f\<restriction>\<^bsub>mem_of A\<^esub>"

HOTG/HOTG_Axioms.thy

@@ -31,28 +31,18 @@ in first-order logic. Moreover, @{thm replacement} takes a meta-level function \
 
 text \<open>Let us define some expected notation.\<close>
 
-bundle hotg_mem_syntax begin notation mem (infixl "\<in>" 50) end
-bundle no_hotg_mem_syntax begin no_notation mem (infixl "\<in>" 50) end
+open_bundle hotg_mem_syntax begin notation mem (infixl \<open>\<in>\<close> 50) end
 
-bundle hotg_emptyset_zero_syntax begin notation emptyset ("\<emptyset>") end
-bundle no_hotg_emptyset_zero_syntax begin no_notation emptyset ("\<emptyset>") end
+bundle hotg_emptyset_zero_syntax begin notation emptyset (\<open>\<emptyset>\<close>) end
+bundle hotg_emptyset_braces_syntax begin notation emptyset (\<open>{}\<close>) end
 
-bundle hotg_emptyset_braces_syntax begin notation emptyset ("{}") end
-bundle no_hotg_emptyset_braces_syntax begin no_notation emptyset ("{}") end
-
-bundle hotg_emptyset_syntax
-begin
-  unbundle hotg_emptyset_zero_syntax hotg_emptyset_braces_syntax
-end
-bundle no_hotg_emptyset_syntax
+open_bundle hotg_emptyset_syntax
 begin
-  unbundle no_hotg_emptyset_zero_syntax no_hotg_emptyset_braces_syntax
+  unbundle hotg_emptyset_zero_syntax
+    and hotg_emptyset_braces_syntax
 end
 
-bundle hotg_union_syntax begin notation union ("\<Union>_" [90] 90) end
-bundle no_hotg_union_syntax begin no_notation union ("\<Union>_" [90] 90) end
-
-unbundle hotg_mem_syntax hotg_emptyset_syntax hotg_union_syntax
+open_bundle hotg_union_syntax begin notation union ("\<Union>_" [90] 90) end
 
 definition "mem_of A x \<equiv> x \<in> A"
 lemma mem_of_eq: "mem_of = (\<lambda>A x. x \<in> A)" unfolding mem_of_def by simp
@@ -69,21 +59,14 @@ lemma mem_of_eq_mem_uhint [uhint]:
 
 abbreviation "not_mem x y \<equiv> \<not>(x \<in> y)"
 
-bundle hotg_not_mem_syntax begin notation not_mem (infixl "\<notin>" 50) end
-bundle no_hotg_not_mem_syntax begin no_notation not_mem (infixl "\<notin>" 50) end
-
-unbundle hotg_not_mem_syntax
-
+open_bundle hotg_not_mem_syntax begin notation not_mem (infixl "\<notin>" 50) end
 
 text \<open>Based on the membership relation, we can define the subset relation.\<close>
 definition subset :: \<open>set \<Rightarrow> set \<Rightarrow> bool\<close>
   where "subset A B \<equiv> \<forall>x. x \<in> A \<longrightarrow> x \<in> B"
 
 text \<open>Again, we define some notation.\<close>
-bundle hotg_subset_syntax begin notation subset (infixl "\<subseteq>" 50) end
-bundle no_hotg_subset_syntax begin no_notation subset (infixl "\<subseteq>" 50) end
-
-unbundle hotg_subset_syntax
+open_bundle hotg_subset_syntax begin notation subset (infixl "\<subseteq>" 50) end
 
 text \<open>The axiom of extensionality and powerset.\<close>
 axiomatization
@@ -119,23 +102,13 @@ where
   univ_min: "\<lbrakk>X \<in> U; mem_trans_closed U; ZF_closed U\<rbrakk> \<Longrightarrow> univ X \<subseteq> U"
 
 (* Bundles to switch basic hotg notations on and off *)
-bundle hotg_basic_syntax
-begin
-  unbundle
-    hotg_mem_syntax
-    hotg_not_mem_syntax
-    hotg_emptyset_syntax
-    hotg_union_syntax
-    hotg_subset_syntax
-end
-bundle no_hotg_basic_syntax
+open_bundle hotg_basic_syntax
 begin
-  unbundle
-    no_hotg_mem_syntax
-    no_hotg_not_mem_syntax
-    no_hotg_emptyset_syntax
-    no_hotg_union_syntax
-    no_hotg_subset_syntax
+  unbundle hotg_mem_syntax
+    and hotg_not_mem_syntax
+    and hotg_emptyset_syntax
+    and hotg_union_syntax
+    and hotg_subset_syntax
 end
 
 end

HOTG/HOTG_Comprehension.thy

@@ -7,21 +7,16 @@ theory HOTG_Comprehension
     HOTG_Finite_Sets
 begin
 
-unbundle no_HOL_ascii_syntax
+unbundle no HOL_ascii_syntax
 
 definition collect :: \<open>set \<Rightarrow> (set \<Rightarrow> bool) \<Rightarrow> set\<close>
   where "collect A P \<equiv> \<Union>{if P x then {x} else {} | x \<in> A}"
 
-bundle hotg_collect_syntax
+open_bundle hotg_collect_syntax
 begin
 syntax "_collect" :: \<open>idt \<Rightarrow> set \<Rightarrow> (set \<Rightarrow> bool) \<Rightarrow> set\<close> ("(1{_ \<in> _ |/ _})")
 end
-bundle no_hotg_collect_syntax
-begin
-no_syntax "_collect" :: \<open>idt \<Rightarrow> set \<Rightarrow> (set \<Rightarrow> bool) \<Rightarrow> set\<close> ("(1{_ \<in> _ |/ _})")
-end
-unbundle hotg_collect_syntax
-
+syntax_consts "_collect" \<rightleftharpoons> collect
 translations
   "{x \<in> A | P}" \<rightleftharpoons> "CONST collect A (\<lambda>x. P)"
 

HOTG/HOTG_Coproduct.thy

@@ -5,7 +5,7 @@ theory HOTG_Coproduct
     HOTG_Functions_Base
 begin
 
-unbundle no_HOL_ascii_syntax
+unbundle no HOL_ascii_syntax
 
 definition "inl a = \<langle>{}, a\<rangle>"
 definition "inr b = \<langle>{{}}, b\<rangle>"
@@ -26,9 +26,7 @@ lemma coprod_rec_eq:
 
 consts coprod :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 
-bundle coprod_syntax begin notation coprod (infixr "\<Coprod>" 70) end
-bundle no_coprod_syntax begin no_notation coprod (infixr "\<Coprod>" 70) end
-unbundle coprod_syntax
+open_bundle coprod_syntax begin notation coprod (infixr "\<Coprod>" 70) end
 
 definition "set_coprod_pred (A :: set \<Rightarrow> bool) (B :: set \<Rightarrow> bool) \<equiv>
   has_inverse_on A inl \<squnion> has_inverse_on B inr"

HOTG/HOTG_Finite_Sets.thy

@@ -6,17 +6,13 @@ theory HOTG_Finite_Sets
   imports HOTG_Unordered_Pairs
 begin
 
-bundle hotg_finite_sets_syntax
+unbundle no HOL_ascii_syntax
+
+open_bundle hotg_finite_sets_syntax
 begin
 syntax "_finset" :: \<open>args \<Rightarrow> set\<close> ("{(_)}")
 end
-bundle no_hotg_finite_sets_syntax
-begin
-no_syntax "_finset" :: \<open>args \<Rightarrow> set\<close> ("{(_)}")
-end
-unbundle hotg_finite_sets_syntax
-unbundle no_HOL_ascii_syntax
-
+syntax_consts "_finset" \<rightleftharpoons> insert
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"