(* Author: Joshua Schneider, ETH Zurich *) subsection ‹Idiomatic terms -- Properties and operations› theory Idiomatic_Terms imports Combinators begin text ‹This theory proves the correctness of the normalisation algorithm for arbitrary applicative functors. We generalise the normal form using a framework for bracket abstraction algorithms. Both approaches justify lifting certain classes of equations. We model this as implications of term equivalences, where unlifting of idiomatic terms is expressed syntactically.› subsubsection ‹Basic definitions› datatype 'a itrm = Opaque 'a | Pure dB | IAp "'a itrm" "'a itrm" (infixl "⋄" 150) primrec opaque :: "'a itrm ⇒ 'a list" where "opaque (Opaque x) = [x]" | "opaque (Pure _) = []" | "opaque (f ⋄ x) = opaque f @ opaque x" abbreviation "iorder x ≡ length (opaque x)" inductive itrm_cong :: "('a itrm ⇒ 'a itrm ⇒ bool) ⇒ 'a itrm ⇒ 'a itrm ⇒ bool" for R where into_itrm_cong: "R x y ⟹ itrm_cong R x y" | pure_cong[intro]: "x ↔ y ⟹ itrm_cong R (Pure x) (Pure y)" | ap_cong: "itrm_cong R f f' ⟹ itrm_cong R x x' ⟹ itrm_cong R (f ⋄ x) (f' ⋄ x')" | itrm_refl[iff]: "itrm_cong R x x" | itrm_sym[sym]: "itrm_cong R x y ⟹ itrm_cong R y x" | itrm_trans[trans]: "itrm_cong R x y ⟹ itrm_cong R y z ⟹ itrm_cong R x z" lemma ap_congL[intro]: "itrm_cong R f f' ⟹ itrm_cong R (f ⋄ x) (f' ⋄ x)" by (blast intro: ap_cong) lemma ap_congR[intro]: "itrm_cong R x x' ⟹ itrm_cong R (f ⋄ x) (f ⋄ x')" by (blast intro: ap_cong) text ‹Idiomatic terms are \emph{similar} iff they have the same structure, and all contained lambda terms are equivalent.› abbreviation similar :: "'a itrm ⇒ 'a itrm ⇒ bool" (infixl "≅" 50) where "x ≅ y ≡ itrm_cong (λ_ _. False) x y" lemma pure_similarE: assumes "Pure x' ≅ y" obtains y' where "y = Pure y'" and "x' ↔ y'" proof - define x :: "'a itrm" where "x = Pure x'" from assms have "x ≅ y" unfolding x_def . then have "(∀x''. x = Pure x'' ⟶ (∃y'. y = Pure y' ∧ x'' ↔ y')) ∧ (∀x''. y = Pure x'' ⟶ (∃y'. x = Pure y' ∧ x'' ↔ y'))" proof (induction) case pure_cong thus ?case by (auto intro: term_sym) next case itrm_trans thus ?case by (fastforce intro: term_trans) qed simp_all with that show thesis unfolding x_def by blast qed lemma opaque_similarE: assumes "Opaque x' ≅ y" obtains y' where "y = Opaque y'" and "x' = y'" proof - define x :: "'a itrm" where "x = Opaque x'" from assms have "x ≅ y" unfolding x_def . then have "(∀x''. x = Opaque x'' ⟶ (∃y'. y = Opaque y' ∧ x'' = y')) ∧ (∀x''. y = Opaque x'' ⟶ (∃y'. x = Opaque y' ∧ x'' = y'))" by induction fast+ with that show thesis unfolding x_def by blast qed lemma ap_similarE: assumes "x1 ⋄ x2 ≅ y" obtains y1 y2 where "y = y1 ⋄ y2" and "x1 ≅ y1" and "x2 ≅ y2" proof - from assms have "(∀x1' x2'. x1 ⋄ x2 = x1' ⋄ x2' ⟶ (∃y1 y2. y = y1 ⋄ y2 ∧ x1' ≅ y1 ∧ x2' ≅ y2)) ∧ (∀x1' x2'. y = x1' ⋄ x2' ⟶ (∃y1 y2. x1 ⋄ x2 = y1 ⋄ y2 ∧ x1' ≅ y1 ∧ x2' ≅ y2))" proof (induction) case ap_cong thus ?case by (blast intro: itrm_sym) next case trans: itrm_trans thus ?case by (fastforce intro: itrm_trans) qed simp_all with that show thesis by blast qed text ‹The following relations define semantic equivalence of idiomatic terms. We consider equivalences that hold universally in all idioms, as well as arbitrary specialisations using additional laws.› inductive idiom_rule :: "'a itrm ⇒ 'a itrm ⇒ bool" where idiom_id: "idiom_rule (Pure ℐ ⋄ x) x" | idiom_comp: "idiom_rule (Pure ℬ ⋄ g ⋄ f ⋄ x) (g ⋄ (f ⋄ x))" | idiom_hom: "idiom_rule (Pure f ⋄ Pure x) (Pure (f ° x))" | idiom_xchng: "idiom_rule (f ⋄ Pure x) (Pure (𝒯 ° x) ⋄ f)" abbreviation itrm_equiv :: "'a itrm ⇒ 'a itrm ⇒ bool" (infixl "≃" 50) where "x ≃ y ≡ itrm_cong idiom_rule x y" lemma idiom_rule_into_equiv: "idiom_rule x y ⟹ x ≃ y" .. lemmas itrm_id = idiom_id[THEN idiom_rule_into_equiv] lemmas itrm_comp = idiom_comp[THEN idiom_rule_into_equiv] lemmas itrm_hom = idiom_hom[THEN idiom_rule_into_equiv] lemmas itrm_xchng = idiom_xchng[THEN idiom_rule_into_equiv] lemma similar_into_equiv: "x ≅ y ⟹ x ≃ y" by (induction pred: itrm_cong) (auto intro: ap_cong itrm_sym itrm_trans) lemma opaque_equiv: "x ≃ y ⟹ opaque x = opaque y" proof (induction pred: itrm_cong) case (into_itrm_cong x y) thus ?case by induction auto qed simp_all lemma iorder_equiv: "x ≃ y ⟹ iorder x = iorder y" by (auto dest: opaque_equiv) locale special_idiom = fixes extra_rule :: "'a itrm ⇒ 'a itrm ⇒ bool" begin definition "idiom_ext_rule = sup idiom_rule extra_rule" abbreviation itrm_ext_equiv :: "'a itrm ⇒ 'a itrm ⇒ bool" (infixl "≃⇧^{+}" 50) where "x ≃⇧^{+}y ≡ itrm_cong idiom_ext_rule x y" lemma equiv_into_ext_equiv: "x ≃ y ⟹ x ≃⇧^{+}y" unfolding idiom_ext_rule_def by (induction pred: itrm_cong) (auto intro: into_itrm_cong ap_cong itrm_sym itrm_trans) lemmas itrm_ext_id = itrm_id[THEN equiv_into_ext_equiv] lemmas itrm_ext_comp = itrm_comp[THEN equiv_into_ext_equiv] lemmas itrm_ext_hom = itrm_hom[THEN equiv_into_ext_equiv] lemmas itrm_ext_xchng = itrm_xchng[THEN equiv_into_ext_equiv] end subsubsection ‹Syntactic unlifting› paragraph ‹With generalisation of variables› primrec unlift' :: "nat ⇒ 'a itrm ⇒ nat ⇒ dB" where "unlift' n (Opaque _) i = Var i" | "unlift' n (Pure x) i = liftn n x 0" | "unlift' n (f ⋄ x) i = unlift' n f (i + iorder x) ° unlift' n x i" abbreviation "unlift x ≡ (Abs^^iorder x) (unlift' (iorder x) x 0)" lemma funpow_Suc_inside: "(f ^^ Suc n) x = (f ^^ n) (f x)" using funpow_Suc_right unfolding comp_def by metis lemma absn_cong[intro]: "s ↔ t ⟹ (Abs^^n) s ↔ (Abs^^n) t" by (induction n) auto lemma free_unlift: "free (unlift' n x i) j ⟹ j ≥ n ∨ (j ≥ i ∧ j < i + iorder x)" proof (induction x arbitrary: i) case (Opaque x) thus ?case by simp next case (Pure x) thus ?case using free_liftn by simp next case (IAp x y) thus ?case by fastforce qed lemma unlift_subst: "j ≤ i ∧ j ≤ n ⟹ (unlift' (Suc n) t (Suc i))[s/j] = unlift' n t i" proof (induction t arbitrary: i) case (Opaque x) thus ?case by simp next case (Pure x) thus ?case using subst_liftn by simp next case (IAp x y) hence "j ≤ i + iorder y" by simp with IAp show ?case by auto qed lemma unlift'_equiv: "x ≃ y ⟹ unlift' n x i ↔ unlift' n y i" proof (induction arbitrary: n i pred: itrm_cong) case (into_itrm_cong x y) thus ?case proof induction case (idiom_id x) show ?case using I_equiv[symmetric] by simp next case (idiom_comp g f x) let ?G = "unlift' n g (i + iorder f + iorder x)" let ?F = "unlift' n f (i + iorder x)" let ?X = "unlift' n x i" have "unlift' n (g ⋄ (f ⋄ x)) i = ?G ° (?F ° ?X)" by (simp add: add.assoc) moreover have "unlift' n (Pure ℬ ⋄ g ⋄ f ⋄ x) i = ℬ ° ?G ° ?F ° ?X" by (simp add: add.commute add.left_commute) moreover have "?G ° (?F ° ?X) ↔ ℬ ° ?G ° ?F ° ?X" using B_equiv[symmetric] . ultimately show ?case by simp next case (idiom_hom f x) show ?case by auto next case (idiom_xchng f x) let ?F = "unlift' n f i" let ?X = "liftn n x 0" have "unlift' n (f ⋄ Pure x) i = ?F ° ?X" by simp moreover have "unlift' n (Pure (𝒯 ° x) ⋄ f) i = 𝒯 ° ?X ° ?F" by simp moreover have "?F ° ?X ↔ 𝒯 ° ?X ° ?F" using T_equiv[symmetric] . ultimately show ?case by simp qed next case pure_cong thus ?case by (auto intro: equiv_liftn) next case (ap_cong f f' x x') from ‹x ≃ x'› have iorder_eq: "iorder x = iorder x'" by (rule iorder_equiv) have "unlift' n (f ⋄ x) i = unlift' n f (i + iorder x) ° unlift' n x i" by simp moreover have "unlift' n (f' ⋄ x') i = unlift' n f' (i + iorder x) ° unlift' n x' i" using iorder_eq by simp ultimately show ?case using ap_cong.IH by (auto intro: equiv_app) next case itrm_refl thus ?case by simp next case itrm_sym thus ?case using term_sym by simp next case itrm_trans thus ?case using term_trans by blast qed lemma unlift_equiv: "x ≃ y ⟹ unlift x ↔ unlift y" proof - assume "x ≃ y" then have "unlift' (iorder y) x 0 ↔ unlift' (iorder y) y 0" by (rule unlift'_equiv) moreover from ‹x ≃ y› have "iorder x = iorder y" by (rule iorder_equiv) ultimately show ?thesis by auto qed paragraph ‹Preserving variables› primrec unlift_vars :: "nat ⇒ nat itrm ⇒ dB" where "unlift_vars n (Opaque i) = Var i" | "unlift_vars n (Pure x) = liftn n x 0" | "unlift_vars n (x ⋄ y) = unlift_vars n x ° unlift_vars n y" lemma all_pure_unlift_vars: "opaque x = [] ⟹ x ≃ Pure (unlift_vars 0 x)" proof (induction x) case (Opaque x) then show ?case by simp next case (Pure x) then show ?case by simp next case (IAp x y) then have no_opaque: "opaque x = []" "opaque y = []" by simp+ then have unlift_ap: "unlift_vars 0 (x ⋄ y) = unlift_vars 0 x ° unlift_vars 0 y" by simp from no_opaque IAp.IH have "x ⋄ y ≃ Pure (unlift_vars 0 x) ⋄ Pure (unlift_vars 0 y)" by (blast intro: ap_cong) also have "... ≃ Pure (unlift_vars 0 x ° unlift_vars 0 y)" by (rule itrm_hom) also have "... = Pure (unlift_vars 0 (x ⋄ y))" by (simp only: unlift_ap) finally show ?case . qed subsubsection ‹Canonical forms› inductive_set CF :: "'a itrm set" where pure_cf[iff]: "Pure x ∈ CF" | ap_cf[intro]: "f ∈ CF ⟹ f ⋄ Opaque x ∈ CF" primrec CF_pure :: "'a itrm ⇒ dB" where "CF_pure (Opaque _) = undefined" | "CF_pure (Pure x) = x" | "CF_pure (x ⋄ _) = CF_pure x" lemma ap_cfD1[dest]: "f ⋄ x ∈ CF ⟹ f ∈ CF" by (rule CF.cases) auto lemma ap_cfD2[dest]: "f ⋄ x ∈ CF ⟹ ∃x'. x = Opaque x'" by (rule CF.cases) auto lemma opaque_not_cf[simp]: "Opaque x ∈ CF ⟹ False" by (rule CF.cases) auto lemma cf_unlift: assumes "x ∈ CF" shows "CF_pure x ↔ unlift x" using assms proof (induction set: CF) case (pure_cf x) show ?case by simp next case (ap_cf f x) let ?n = "iorder f + 1" have "unlift (f ⋄ Opaque x) = (Abs^^?n) (unlift' ?n f 1 ° Var 0)" by simp also have "... = (Abs^^iorder f) (Abs (unlift' ?n f 1 ° Var 0))" using funpow_Suc_inside by simp also have "... ↔ unlift f" proof - have "¬ free (unlift' ?n f 1) 0" using free_unlift by fastforce hence "Abs (unlift' ?n f 1 ° Var 0) →⇩_{η}(unlift' ?n f 1)[Var 0/0]" .. also have "... = unlift' (iorder f) f 0" using unlift_subst by (metis One_nat_def Suc_eq_plus1 le0) finally show ?thesis by (simp add: r_into_rtranclp absn_cong eta_into_equiv) qed finally show ?case using ap_cf.IH by (auto intro: term_sym term_trans) qed lemma cf_similarI: assumes "x ∈ CF" "y ∈ CF" and "opaque x = opaque y" and "CF_pure x ↔ CF_pure y" shows "x ≅ y" using assms proof (induction arbitrary: y) case (pure_cf x) hence "opaque y = []" by auto with ‹y ∈ CF› obtain y' where "y = Pure y'" by cases auto with pure_cf.prems show ?case by auto next case (ap_cf f x) from ‹opaque (f ⋄ Opaque x) = opaque y› obtain y1 y2 where "opaque y = y1 @ y2" and "opaque f = y1" and "[x] = y2" by fastforce from ‹[x] = y2› obtain y' where "y2 = [y']" and "x = y'" by auto with ‹y ∈ CF› and ‹opaque y = y1 @ y2› obtain g where "opaque g = y1" and y_split: "y = g ⋄ Opaque y'" "g ∈ CF" by cases auto with ap_cf.prems ‹opaque f = y1› have "opaque f = opaque g" "CF_pure f ↔ CF_pure g" by auto with ap_cf.IH ‹g ∈ CF› have "f ≅ g" by simp with ap_cf.prems y_split ‹x = y'› show ?case by (auto intro: ap_cong) qed lemma cf_similarD: assumes in_cf: "x ∈ CF" "y ∈ CF" and similar: "x ≅ y" shows "CF_pure x ↔ CF_pure y ∧ opaque x = opaque y" using assms by (blast intro!: similar_into_equiv opaque_equiv cf_unlift unlift_equiv intro: term_trans term_sym) text ‹Equivalent idiomatic terms in canonical form are similar. This justifies speaking of a normal form.› lemma cf_unique: assumes in_cf: "x ∈ CF" "y ∈ CF" and equiv: "x ≃ y" shows "x ≅ y" using in_cf proof (rule cf_similarI) from equiv show "opaque x = opaque y" by (rule opaque_equiv) next from equiv have "unlift x ↔ unlift y" by (rule unlift_equiv) thus "CF_pure x ↔ CF_pure y" using cf_unlift[OF in_cf(1)] cf_unlift[OF in_cf(2)] by (auto intro: term_sym term_trans) qed subsubsection ‹Normalisation of idiomatic terms› primrec norm_pn :: "dB ⇒ 'a itrm ⇒ 'a itrm" where "norm_pn f (Opaque x) = undefined" | "norm_pn f (Pure x) = Pure (f ° x)" | "norm_pn f (n ⋄ x) = norm_pn (ℬ ° f) n ⋄ x" primrec norm_nn :: "'a itrm ⇒ 'a itrm ⇒ 'a itrm" where "norm_nn n (Opaque x) = undefined" | "norm_nn n (Pure x) = norm_pn (𝒯 ° x) n" | "norm_nn n (n' ⋄ x) = norm_nn (norm_pn ℬ n) n' ⋄ x" primrec norm :: "'a itrm ⇒ 'a itrm" where "norm (Opaque x) = Pure ℐ ⋄ Opaque x" | "norm (Pure x) = Pure x" | "norm (f ⋄ x) = norm_nn (norm f) (norm x)" lemma norm_pn_in_cf: assumes "x ∈ CF" shows "norm_pn f x ∈ CF" using assms by (induction x arbitrary: f) auto lemma norm_nn_in_cf: assumes "n ∈ CF" "n' ∈ CF" shows "norm_nn n n' ∈ CF" using assms(2,1) by (induction n' arbitrary: n) (auto intro: norm_pn_in_cf) lemma norm_in_cf: "norm x ∈ CF" by (induction x) (auto intro: norm_nn_in_cf) lemma norm_pn_equiv: assumes "x ∈ CF" shows "norm_pn f x ≃ Pure f ⋄ x" using assms proof (induction x arbitrary: f) case (pure_cf x) have "Pure (f ° x) ≃ Pure f ⋄ Pure x" using itrm_hom[symmetric] . then show ?case by simp next case (ap_cf n x) from ap_cf.IH have "norm_pn (ℬ ° f) n ≃ Pure (ℬ ° f) ⋄ n" . then have "norm_pn (ℬ ° f) n ⋄ Opaque x ≃ Pure (ℬ ° f) ⋄ n ⋄ Opaque x" .. also have "... ≃ Pure ℬ ⋄ Pure f ⋄ n ⋄ Opaque x" using itrm_hom[symmetric] by blast also have "... ≃ Pure f ⋄ (n ⋄ Opaque x)" using itrm_comp . finally show ?case by simp qed lemma norm_nn_equiv: assumes "n ∈ CF" "n' ∈ CF" shows "norm_nn n n' ≃ n ⋄ n'" using assms(2,1) proof (induction n' arbitrary: n) case (pure_cf x) then have "norm_pn (𝒯 ° x) n ≃ Pure (𝒯 ° x) ⋄ n" by (rule norm_pn_equiv) also have "... ≃ n ⋄ Pure x" using itrm_xchng[symmetric] . finally show ?case by simp next case (ap_cf n' x) have "norm_nn (norm_pn ℬ n) n' ⋄ Opaque x ≃ Pure ℬ ⋄ n ⋄ n' ⋄ Opaque x" proof from ‹n ∈ CF› have "norm_pn ℬ n ∈ CF" by (rule norm_pn_in_cf) with ap_cf.IH have "norm_nn (norm_pn ℬ n) n' ≃ norm_pn ℬ n ⋄ n'" . also have "... ≃ Pure ℬ ⋄ n ⋄ n'" using norm_pn_equiv ‹n ∈ CF› by blast finally show "norm_nn (norm_pn ℬ n) n' ≃ Pure ℬ ⋄ n ⋄ n'" . qed also have "... ≃ n ⋄ (n' ⋄ Opaque x)" using itrm_comp . finally show ?case by simp qed lemma norm_equiv: "norm x ≃ x" proof (induction) case (Opaque x) have "Pure ℐ ⋄ Opaque x ≃ Opaque x" using itrm_id . then show ?case by simp next case (Pure x) show ?case by simp next case (IAp f x) have "norm f ∈ CF" and "norm x ∈ CF" by (rule norm_in_cf)+ then have "norm_nn (norm f) (norm x) ≃ norm f ⋄ norm x" by (rule norm_nn_equiv) also have "... ≃ f ⋄ x" using IAp.IH .. finally show ?case by simp qed lemma normal_form: obtains n where "n ≃ x" and "n ∈ CF" using norm_equiv norm_in_cf .. subsubsection ‹Lifting with normal forms› lemma nf_unlift: assumes equiv: "n ≃ x" and cf: "n ∈ CF" shows "CF_pure n ↔ unlift x" proof - from cf have "CF_pure n ↔ unlift n" by (rule cf_unlift) also from equiv have "unlift n ↔ unlift x" by (rule unlift_equiv) finally show ?thesis . qed theorem nf_lifting: assumes opaque: "opaque x = opaque y" and base_eq: "unlift x ↔ unlift y" shows "x ≃ y" proof - obtain n where nf_x: "n ≃ x" "n ∈ CF" by (rule normal_form) obtain n' where nf_y: "n' ≃ y" "n' ∈ CF" by (rule normal_form) from nf_x have "CF_pure n ↔ unlift x" by (rule nf_unlift) also note base_eq also from nf_y have "unlift y ↔ CF_pure n'" by (rule nf_unlift[THEN term_sym]) finally have pure_eq: "CF_pure n ↔ CF_pure n'" . from nf_x(1) have "opaque n = opaque x" by (rule opaque_equiv) also note opaque also from nf_y(1) have "opaque y = opaque n'" by (rule opaque_equiv[THEN sym]) finally have opaque_eq: "opaque n = opaque n'" . from nf_x(1) have "x ≃ n" .. also have "n ≃ n'" using nf_x nf_y pure_eq opaque_eq by (blast intro: similar_into_equiv cf_similarI) also from nf_y(1) have "n' ≃ y" . finally show "x ≃ y" . qed subsubsection ‹Bracket abstraction, twice› paragraph ‹Preliminaries: Sequential application of variables› definition frees :: "dB ⇒ nat set" where [simp]: "frees t = {i. free t i}" definition var_dist :: "nat list ⇒ dB ⇒ dB" where "var_dist = fold (λi t. t ° Var i)" lemma var_dist_Nil[simp]: "var_dist [] t = t" unfolding var_dist_def by simp lemma var_dist_Cons[simp]: "var_dist (v # vs) t = var_dist vs (t ° Var v)" unfolding var_dist_def by simp lemma var_dist_append1: "var_dist (vs @ [v]) t = var_dist vs t ° Var v" unfolding var_dist_def by simp lemma var_dist_frees: "frees (var_dist vs t) = frees t ∪ set vs" by (induction vs arbitrary: t) auto lemma var_dist_subst_lt: "∀v∈set vs. i < v ⟹ (var_dist vs s)[t/i] = var_dist (map (λv. v - 1) vs) (s[t/i])" by (induction vs arbitrary: s) simp_all lemma var_dist_subst_gt: "∀v∈set vs. v < i ⟹ (var_dist vs s)[t/i] = var_dist vs (s[t/i])" by (induction vs arbitrary: s) simp_all definition vsubst :: "nat ⇒ nat ⇒ nat ⇒ nat" where "vsubst u v w = (if u < w then u else if u = w then v else u - 1)" lemma vsubst_subst[simp]: "(Var u)[Var v/w] = Var (vsubst u v w)" unfolding vsubst_def by simp lemma vsubst_subst_lt[simp]: "u < w ⟹ vsubst u v w = u" unfolding vsubst_def by simp lemma var_dist_subst_Var: "(var_dist vs s)[Var i/j] = var_dist (map (λv. vsubst v i j) vs) (s[Var i/j])" by (induction vs arbitrary: s) simp_all lemma var_dist_cong: "s ↔ t ⟹ var_dist vs s ↔ var_dist vs t" by (induction vs arbitrary: s t) auto paragraph ‹Preliminaries: Eta reductions with permuted variables› lemma absn_subst: "((Abs^^n) s)[t/k] = (Abs^^n) (s[liftn n t 0/k+n])" by (induction n arbitrary: t k) (simp_all add: liftn_lift_swap) lemma absn_beta_equiv: "(Abs^^Suc n) s ° t ↔ (Abs^^n) (s[liftn n t 0/n])" proof - have "(Abs^^Suc n) s ° t = Abs ((Abs^^n) s) ° t" by simp also have "... ↔ ((Abs^^n) s)[t/0]" by (rule beta_into_equiv) (rule beta.beta) also have "... = (Abs^^n) (s[liftn n t 0/n])" by (simp add: absn_subst) finally show ?thesis . qed lemma absn_dist_eta: "(Abs^^n) (var_dist (rev [0..<n]) (liftn n t 0)) ↔ t" proof (induction n) case 0 show ?case by simp next case (Suc n) let ?dist_range = "λa k. var_dist (rev [a..<k]) (liftn k t 0)" have append: "rev [0..<Suc n] = rev [1..<Suc n] @ [0]" by (simp add: upt_rec) have dist_last: "?dist_range 0 (Suc n) = ?dist_range 1 (Suc n) ° Var 0" unfolding append var_dist_append1 .. have "¬ free (?dist_range 1 (Suc n)) 0" proof - have "frees (?dist_range 1 (Suc n)) = frees (liftn (Suc n) t 0) ∪ {1..n}" unfolding var_dist_frees by fastforce then have "0 ∉ frees (?dist_range 1 (Suc n))" by simp then show ?thesis by simp qed then have "Abs (?dist_range 0 (Suc n)) →⇩_{η}(?dist_range 1 (Suc n))[Var 0/0]" unfolding dist_last by (rule eta) also have "... = var_dist (rev [0..<n]) ((liftn (Suc n) t 0)[Var 0/0])" proof - have "∀v∈set (rev [1..<Suc n]). 0 < v" by auto moreover have "rev [0..<n] = map (λv. v - 1) (rev [1..<Suc n])" by (induction n) simp_all ultimately show ?thesis by (simp only: var_dist_subst_lt) qed also have "... = ?dist_range 0 n" using subst_liftn[of 0 n 0 t "Var 0"] by simp finally have "Abs (?dist_range 0 (Suc n)) ↔ ?dist_range 0 n" .. then have "(Abs^^Suc n) (?dist_range 0 (Suc n)) ↔ (Abs^^n) (?dist_range 0 n)" unfolding funpow_Suc_inside by (rule absn_cong) also from Suc.IH have "... ↔ t" . finally show ?case . qed primrec strip_context :: "nat ⇒ dB ⇒ nat ⇒ dB" where "strip_context n (Var i) k = (if i < k then Var i else Var (i - n))" | "strip_context n (Abs t) k = Abs (strip_context n t (Suc k))" | "strip_context n (s ° t) k = strip_context n s k ° strip_context n t k" lemma strip_context_liftn: "strip_context n (liftn (m + n) t k) k = liftn m t k" by (induction t arbitrary: k) simp_all lemma liftn_strip_context: assumes "∀i∈frees t. i < k ∨ k + n ≤ i" shows "liftn n (strip_context n t k) k = t" using assms proof (induction t arbitrary: k) case (Abs t) have "∀i∈frees t. i < Suc k ∨ Suc k + n ≤ i" proof fix i assume free: "i ∈ frees t" show "i < Suc k ∨ Suc k + n ≤ i" proof (cases "i > 0") assume "i > 0" with free Abs.prems have "i-1 < k ∨ k + n ≤ i-1" by simp then show ?thesis by arith qed simp qed with Abs.IH show ?case by simp qed auto lemma absn_dist_eta_free: assumes "∀i∈frees t. n ≤ i" shows "(Abs^^n) (var_dist (rev [0..<n]) t) ↔ strip_context n t 0" (is "?lhs t ↔ ?rhs") proof - have "?lhs (liftn n ?rhs 0) ↔ ?rhs" by (rule absn_dist_eta) moreover have "liftn n ?rhs 0 = t" using assms by (auto intro: liftn_strip_context) ultimately show ?thesis by simp qed definition perm_vars :: "nat ⇒ nat list ⇒ bool" where "perm_vars n vs ⟷ distinct vs ∧ set vs = {0..<n}" lemma perm_vars_distinct: "perm_vars n vs ⟹ distinct vs" unfolding perm_vars_def by simp lemma perm_vars_length: "perm_vars n vs ⟹ length vs = n" unfolding perm_vars_def using distinct_card by force lemma perm_vars_lt: "perm_vars n vs ⟹ ∀i∈set vs. i < n" unfolding perm_vars_def by simp lemma perm_vars_nth_lt: "perm_vars n vs ⟹ i < n ⟹ vs ! i < n" using perm_vars_length perm_vars_lt by simp lemma perm_vars_inj_on_nth: assumes "perm_vars n vs" shows "inj_on (nth vs) {0..<n}" proof (rule inj_onI) fix i j assume "i ∈ {0..<n}" and "j ∈ {0..<n}" with assms have "i < length vs" and "j < length vs" using perm_vars_length by simp+ moreover from assms have "distinct vs" by (rule perm_vars_distinct) moreover assume "vs ! i = vs ! j" ultimately show "i = j" using nth_eq_iff_index_eq by blast qed abbreviation perm_vars_inv :: "nat ⇒ nat list ⇒ nat ⇒ nat" where "perm_vars_inv n vs i ≡ the_inv_into {0..<n} ((!) vs) i" lemma perm_vars_inv_nth: assumes "perm_vars n vs" and "i < n" shows "perm_vars_inv n vs (vs ! i) = i" using assms by (auto intro: the_inv_into_f_f perm_vars_inj_on_nth) lemma dist_perm_eta: assumes perm_vars: "perm_vars n vs" obtains vs' where "⋀t. ∀i∈frees t. n ≤ i ⟹ (Abs^^n) (var_dist vs' ((Abs^^n) (var_dist vs (liftn n t 0)))) ↔ strip_context n t 0" proof - define vsubsts where "vsubsts n vs' vs = map (λv. if v < n - length vs' then v else if v < n then vs' ! (n - v - 1) + (n - length vs') else v - length vs') vs" for n vs' vs let ?app_vars = "λt n vs' vs. var_dist vs' ((Abs^^n) (var_dist vs (liftn n t 0)))" { fix t :: dB and vs' :: "nat list" assume partial: "length vs' ≤ n" let ?m = "n - length vs'" have "?app_vars t n vs' vs ↔ (Abs^^?m) (var_dist (vsubsts n vs' vs) (liftn ?m t 0))" using partial proof (induction vs' arbitrary: vs n) case Nil then have "vsubsts n [] vs = vs" unfolding vsubsts_def by (auto intro: map_idI) then show ?case by simp next case (Cons v vs') define n' where "n' = n - 1" have Suc_n': "Suc n' = n" unfolding n'_def using Cons.prems by simp have vs'_length: "length vs' ≤ n'" unfolding n'_def using Cons.prems by simp let ?m' = "n' - length vs'" have m'_conv: "?m' = n - length (v # vs')" unfolding n'_def by simp have "?app_vars t n (v # vs') vs = ?app_vars t (Suc n') (v # vs') vs" unfolding Suc_n' .. also have "... ↔ var_dist vs' ((Abs^^Suc n') (var_dist vs (liftn (Suc n') t 0)) ° Var v)" unfolding var_dist_Cons .. also have "... ↔ ?app_vars t n' vs' (vsubsts n [v] vs)" proof (rule var_dist_cong) have "map (λvv. vsubst vv (v + n') n') vs = vsubsts n [v] vs" unfolding Suc_n'[symmetric] vsubsts_def vsubst_def by (auto cong: if_cong) then have "(var_dist vs (liftn (Suc n') t 0))[liftn n' (Var v) 0/n'] = var_dist (vsubsts n [v] vs) (liftn n' t 0)" using var_dist_subst_Var subst_liftn by simp then show "(Abs^^Suc n') (var_dist vs (liftn (Suc n') t 0)) ° Var v ↔ (Abs^^n') (var_dist (vsubsts n [v] vs) (liftn n' t 0))" by (fastforce intro: absn_beta_equiv[THEN term_trans]) qed also have "... ↔ (Abs^^?m') (var_dist (vsubsts n' vs' (vsubsts n [v] vs)) (liftn ?m' t 0))" using vs'_length Cons.IH by blast also have "... = (Abs^^?m') (var_dist (vsubsts n (v # vs') vs) (liftn ?m' t 0))" proof - have "vsubsts n' vs' (vsubsts (Suc n') [v] vs) = vsubsts (Suc n') (v # vs') vs" unfolding vsubsts_def using vs'_length [[linarith_split_limit=10]] by auto then show ?thesis unfolding Suc_n' by simp qed finally show ?case unfolding m'_conv . qed } note partial_appd = this define vs' where "vs' = map (λi. n - perm_vars_inv n vs (n - i - 1) - 1) [0..<n]" from perm_vars have vs_length: "length vs = n" by (rule perm_vars_length) have vs'_length: "length vs' = n" unfolding vs'_def by simp have "map (λv. vs' ! (n - v - 1)) vs = rev [0..<n]" proof - have "length vs = length (rev [0..<n])" unfolding vs_length by simp then have "list_all2 (λv v'. vs' ! (n - v - 1) = v') vs (rev [0..<n])" proof fix i assume "i < length vs" then have "i < n" unfolding vs_length . then have "vs ! i < n" using perm_vars perm_vars_nth_lt by simp with ‹i < n› have "vs' ! (n - vs ! i - 1) = n - perm_vars_inv n vs (vs ! i) - 1" unfolding vs'_def by simp also from ‹i < n› have "... = n - i - 1" using perm_vars perm_vars_inv_nth by simp also from ‹i < n› have "... = rev [0..<n] ! i" by (simp add: rev_nth) finally show "vs' ! (n - vs ! i - 1) = rev [0..<n] ! i" . qed then show ?thesis unfolding list.rel_eq[symmetric] using list.rel_map by auto qed then have vs'_vs: "vsubsts n vs' vs = rev [0..<n]" unfolding vsubsts_def vs'_length using perm_vars perm_vars_lt by (auto intro: map_ext[THEN trans]) let ?appd_vars = "λt n. var_dist (rev [0..<n]) t" { fix t assume not_free: "∀i∈frees t. n ≤ i" have "?app_vars t n vs' vs ↔ ?appd_vars t n" for t using partial_appd[of vs'] vs'_length vs'_vs by simp then have "(Abs^^n) (?app_vars t n vs' vs) ↔ (Abs^^n) (?appd_vars t n)" by (rule absn_cong) also have "... ↔ strip_context n t 0" using not_free by (rule absn_dist_eta_free) finally have "(Abs^^n) (?app_vars t n vs' vs) ↔ strip_context n t 0" . } with that show ?thesis . qed lemma liftn_absn: "liftn n ((Abs^^m) t) k = (Abs^^m) (liftn n t (k + m))" by (induction m arbitrary: k) auto lemma liftn_var_dist_lt: "∀i∈set vs. i < k ⟹ liftn n (var_dist vs t) k = var_dist vs (liftn n t k)" by (induction vs arbitrary: t) auto lemma liftn_context_conv: "k ≤ k' ⟹ ∀i∈frees t. i < k ∨ k' ≤ i ⟹ liftn n t k = liftn n t k'" proof (induction t arbitrary: k k') case (Abs t) have "∀i∈frees t. i < Suc k ∨ Suc k' ≤ i" proof fix i assume "i ∈ frees t" show "i < Suc k ∨ Suc k' ≤ i" proof (cases "i = 0") assume "i = 0" then show ?thesis by simp next assume "i ≠ 0" from Abs.prems(2) have "∀i. free t (Suc i) ⟶ i < k ∨ k' ≤ i" by auto then have "∀i. 0 < i ∧ free t i ⟶ i - 1 < k ∨ k' ≤ i - 1" by simp then have "∀i. 0 < i ∧ free t i ⟶ i < Suc k ∨ Suc k' ≤ i" by auto with ‹i ≠ 0› ‹i ∈ frees t› show ?thesis by simp qed qed with Abs.IH Abs.prems(1) show ?case by auto qed auto lemma liftn_liftn0: "∀i∈frees t. k ≤ i ⟹ liftn n t k = liftn n t 0" using liftn_context_conv by auto lemma dist_perm_eta_equiv: assumes perm_vars: "perm_vars n vs" and not_free: "∀i∈frees s. n ≤ i" "∀i∈frees t. n ≤ i" and perm_equiv: "(Abs^^n) (var_dist vs s) ↔ (Abs^^n) (var_dist vs t)" shows "strip_context n s 0 ↔ strip_context n t 0" proof - from perm_vars have vs_lt_n: "∀i∈set vs. i < n" using perm_vars_lt by simp obtain vs' where etas: "⋀t. ∀i∈frees t. n ≤ i ⟹ (Abs^^n) (var_dist vs' ((Abs^^n) (var_dist vs (liftn n t 0)))) ↔ strip_context n t 0" using perm_vars dist_perm_eta by blast have "strip_context n s 0 ↔ (Abs^^n) (var_dist vs' ((Abs^^n) (var_dist vs (liftn n s 0))))" using etas[THEN term_sym] not_free(1) . also have "... ↔ (Abs^^n) (var_dist vs' ((Abs^^n) (var_dist vs (liftn n t 0))))" proof (rule absn_cong, rule var_dist_cong) have "(Abs^^n) (var_dist vs (liftn n s 0)) = (Abs^^n) (var_dist vs (liftn n s n))" using not_free(1) liftn_liftn0[of s n] by simp also have "... = (Abs^^n) (liftn n (var_dist vs s) n)" using vs_lt_n liftn_var_dist_lt by simp also have "... = liftn n ((Abs^^n) (var_dist vs s)) 0" using liftn_absn by simp also have "... ↔ liftn n ((Abs^^n) (var_dist vs t)) 0" using perm_equiv by (rule equiv_liftn) also have "... = (Abs^^n) (liftn n (var_dist vs t) n)" using liftn_absn by simp also have "... = (Abs^^n) (var_dist vs (liftn n t n))" using vs_lt_n liftn_var_dist_lt by simp also have "... = (Abs^^n) (var_dist vs (liftn n t 0))" using not_free(2) liftn_liftn0[of t n] by simp finally show "(Abs^^n) (var_dist vs (liftn n s 0)) ↔ ..." . qed also have "... ↔ strip_context n t 0" using etas not_free(2) . finally show ?thesis . qed paragraph ‹General notion of bracket abstraction for lambda terms› definition foldr_option :: "('a ⇒ 'b ⇒ 'b option) ⇒ 'a list ⇒ 'b ⇒ 'b option" where "foldr_option f xs e = foldr (λa b. Option.bind b (f a)) xs (Some e)" lemma bind_eq_SomeE: assumes "Option.bind x f = Some y" obtains x' where "x = Some x'" and "f x' = Some y" using assms by (auto iff: bind_eq_Some_conv) lemma foldr_option_Nil[simp]: "foldr_option f [] e = Some e" unfolding foldr_option_def by simp lemma foldr_option_Cons_SomeE: assumes "foldr_option f (x#xs) e = Some y" obtains y' where "foldr_option f xs e = Some y'" and "f x y' = Some y" using assms unfolding foldr_option_def by (auto elim: bind_eq_SomeE) locale bracket_abstraction = fixes term_bracket :: "nat ⇒ dB ⇒ dB option" assumes bracket_app: "term_bracket i s = Some s' ⟹ s' ° Var i ↔ s" assumes bracket_frees: "term_bracket i s = Some s' ⟹ frees s' = frees s - {i}" begin definition term_brackets :: "nat list ⇒ dB ⇒ dB option" where "term_brackets = foldr_option term_bracket" lemma term_brackets_Nil[simp]: "term_brackets [] t = Some t" unfolding term_brackets_def by simp lemma term_brackets_Cons_SomeE: assumes "term_brackets (v#vs) t = Some t'" obtains s' where "term_brackets vs t = Some s'" and "term_bracket v s' = Some t'" using assms unfolding term_brackets_def by (elim foldr_option_Cons_SomeE) lemma term_brackets_ConsI: assumes "term_brackets vs t = Some t'" and "term_bracket v t' = Some t''" shows "term_brackets (v#vs) t = Some t''" using assms unfolding term_brackets_def foldr_option_def by simp lemma term_brackets_dist: assumes "term_brackets vs t = Some t'" shows "var_dist vs t' ↔ t" proof - from assms have "∀t''. t' ↔ t'' ⟶ var_dist vs t'' ↔ t" proof (induction vs arbitrary: t') case Nil then show ?case by (simp add: term_sym) next case (Cons v vs) from Cons.prems obtain u where inner: "term_brackets vs t = Some u" and step: "term_bracket v u = Some t'" by (auto elim: term_brackets_Cons_SomeE) from step have red1: "t' ° Var v ↔ u" by (rule bracket_app) show ?case proof rule+ fix t'' assume "t' ↔ t''" with red1 have red: "t'' ° Var v ↔ u" using term_sym term_trans by blast have "var_dist (v # vs) t'' = var_dist vs (t'' ° Var v)" by simp also have "... ↔ t" using Cons.IH[OF inner] red[symmetric] by blast finally show "var_dist (v # vs) t'' ↔ t" . qed qed then show ?thesis by blast qed end (* locale bracket_abstraction *) paragraph ‹Bracket abstraction for idiomatic terms› text ‹We consider idiomatic terms with explicitly assigned variables.› lemma strip_unlift_vars: assumes "opaque x = []" shows "strip_context n (unlift_vars n x) 0 = unlift_vars 0 x" using assms by (induction x) (simp_all add: strip_context_liftn[where m=0, simplified]) lemma unlift_vars_frees: "∀i∈frees (unlift_vars n x). i ∈ set (opaque x) ∨ n ≤ i" by (induction x) (auto simp add: free_liftn) locale itrm_abstraction = special_idiom extra_rule for extra_rule :: "nat itrm ⇒ _" + fixes itrm_bracket :: "nat ⇒ nat itrm ⇒ nat itrm option" assumes itrm_bracket_ap: "itrm_bracket i x = Some x' ⟹ x' ⋄ Opaque i ≃⇧^{+}x" assumes itrm_bracket_opaque: "itrm_bracket i x = Some x' ⟹ set (opaque x') = set (opaque x) - {i}" begin definition "itrm_brackets = foldr_option itrm_bracket" lemma itrm_brackets_Nil[simp]: "itrm_brackets [] x = Some x" unfolding itrm_brackets_def by simp lemma itrm_brackets_Cons_SomeE: assumes "itrm_brackets (v#vs) x = Some x'" obtains y' where "itrm_brackets vs x = Some y'" and "itrm_bracket v y' = Some x'" using assms unfolding itrm_brackets_def by (elim foldr_option_Cons_SomeE) definition "opaque_dist = fold (λi y. y ⋄ Opaque i)" lemma opaque_dist_cong: "x ≃⇧^{+}y ⟹ opaque_dist vs x ≃⇧^{+}opaque_dist vs y" unfolding opaque_dist_def by (induction vs arbitrary: x y) (simp_all add: ap_congL) lemma itrm_brackets_dist: assumes defined: "itrm_brackets vs x = Some x'" shows "opaque_dist vs x' ≃⇧^{+}x" proof - define x'' where "x'' = x'" have "x' ≃⇧^{+}x''" unfolding x''_def .. with defined show "opaque_dist vs x'' ≃⇧^{+}x" unfolding opaque_dist_def proof (induction vs arbitrary: x' x'') case Nil then show ?case unfolding itrm_brackets_def by (simp add: itrm_sym) next case (Cons v vs) from Cons.prems(1) obtain y' where defined': "itrm_brackets vs x = Some y'" and "itrm_bracket v y' = Some x'" by (rule itrm_brackets_Cons_SomeE) then have "x' ⋄ Opaque v ≃⇧^{+}y'" by (elim itrm_bracket_ap) then have "x'' ⋄ Opaque v ≃⇧^{+}y'" using Cons.prems(2) by (blast intro: itrm_sym itrm_trans) note this[symmetric] with defined' have "fold (λi y. y ⋄ Opaque i) vs (x'' ⋄ Opaque v) ≃⇧^{+}x" using Cons.IH by blast then show ?case by simp qed qed lemma itrm_brackets_opaque: assumes "itrm_brackets vs x = Some x'" shows "set (opaque x') = set (opaque x) - set vs" using assms proof (induction vs arbitrary: x') case Nil then show ?case unfolding itrm_brackets_def by simp next case (Cons v vs) then show ?case by (auto elim: itrm_brackets_Cons_SomeE dest!: itrm_bracket_opaque) qed lemma itrm_brackets_all: assumes all_opaque: "set (opaque x) ⊆ set vs" and defined: "itrm_brackets vs x = Some x'" shows "opaque x' = []" proof - from defined have "set (opaque x') = set (opaque x) - set vs" by (rule itrm_brackets_opaque) with all_opaque have "set (opaque x') = {}" by simp then show ?thesis by simp qed lemma itrm_brackets_all_unlift_vars: assumes all_opaque: "set (opaque x) ⊆ set vs" and defined: "itrm_brackets vs x = Some x'" shows "x' ≃⇧^{+}Pure (unlift_vars 0 x')" proof (rule equiv_into_ext_equiv) from assms have "opaque x' = []" by (rule itrm_brackets_all) then show "x' ≃ Pure (unlift_vars 0 x')" by (rule all_pure_unlift_vars) qed end (* locale itrm_abstraction *) subsubsection ‹Lifting with bracket abstraction› locale lifted_bracket = bracket_abstraction + itrm_abstraction + assumes bracket_compat: "set (opaque x) ⊆ {0..<n} ⟹ i < n ⟹ term_bracket i (unlift_vars n x) = map_option (unlift_vars n) (itrm_bracket i x)" begin lemma brackets_unlift_vars_swap: assumes all_opaque: "set (opaque x) ⊆ {0..<n}" and vs_bound: "set vs ⊆ {0..<n}" and defined: "itrm_brackets vs x = Some x'" shows "term_brackets vs (unlift_vars n x) = Some (unlift_vars n x')" using vs_bound defined proof (induction vs arbitrary: x') case Nil then show ?case by simp next case (Cons v vs) then obtain y' where ivs: "itrm_brackets vs x = Some y'" and iv: "itrm_bracket v y' = Some x'" by (elim itrm_brackets_Cons_SomeE) with Cons have "term_brackets vs (unlift_vars n x) = Some (unlift_vars n y')" by auto moreover { have "Some (unlift_vars n x') = map_option (unlift_vars n) (itrm_bracket v y')" unfolding iv by simp moreover have "set (opaque y') ⊆ {0..<n}" using all_opaque ivs by (auto dest: itrm_brackets_opaque) moreover have "v < n" using Cons.prems by simp ultimately have "term_bracket v (unlift_vars n y') = Some (unlift_vars n x')" using bracket_compat by auto } ultimately show ?case by (rule term_brackets_ConsI) qed theorem bracket_lifting: assumes all_vars: "set (opaque x) ∪ set (opaque y) ⊆ {0..<n}" and perm_vars: "perm_vars n vs" and defined: "itrm_brackets vs x = Some x'" "itrm_brackets vs y = Some y'" and base_eq: "(Abs^^n) (unlift_vars n x) ↔ (Abs^^n) (unlift_vars n y)" shows "x ≃⇧^{+}y" proof - from perm_vars have set_vs: "set vs = {0..<n}" unfolding perm_vars_def by simp have x_swap: "term_brackets vs (unlift_vars n x) = Some (unlift_vars n x')" using all_vars set_vs defined(1) by (auto intro: brackets_unlift_vars_swap) have y_swap: "term_brackets vs (unlift_vars n y) = Some (unlift_vars n y')" using all_vars set_vs defined(2) by (auto intro: brackets_unlift_vars_swap) from all_vars have "set (opaque x) ⊆ set vs" unfolding set_vs by simp then have complete_x: "opaque x' = []" using defined(1) itrm_brackets_all by blast then have ux_frees: "∀i∈frees (unlift_vars n x'). n ≤ i" using unlift_vars_frees by fastforce from all_vars have "set (opaque y) ⊆ set vs" unfolding set_vs by simp then have complete_y: "opaque y' = []" using defined(2) itrm_brackets_all by blast then have uy_frees: "∀i∈frees (unlift_vars n y'). n ≤ i" using unlift_vars_frees by fastforce have "x ≃⇧^{+}opaque_dist vs x'" using defined(1) by (rule itrm_brackets_dist[symmetric]) also have "... ≃⇧^{+}opaque_dist vs (Pure (unlift_vars 0 x'))" using all_vars set_vs defined(1) by (auto intro: opaque_dist_cong itrm_brackets_all_unlift_vars) also have "... ≃⇧^{+}opaque_dist vs (Pure (unlift_vars 0 y'))" proof (rule opaque_dist_cong, rule pure_cong) have "(Abs^^n) (var_dist vs (unlift_vars n x')) ↔ (Abs^^n) (unlift_vars n x)" using x_swap term_brackets_dist by auto also have "... ↔ (Abs^^n) (unlift_vars n y)" using base_eq . also have "... ↔ (Abs^^n) (var_dist vs (unlift_vars n y'))" using y_swap term_brackets_dist[THEN term_sym] by auto finally have "strip_context n (unlift_vars n x') 0 ↔ strip_context n (unlift_vars n y') 0" using perm_vars ux_frees uy_frees by (intro dist_perm_eta_equiv) then show "unlift_vars 0 x' ↔ unlift_vars 0 y'" using strip_unlift_vars complete_x complete_y by simp qed also have "... ≃⇧^{+}opaque_dist vs y'" proof (rule opaque_dist_cong) show "Pure (unlift_vars 0 y') ≃⇧^{+}y'" using all_vars set_vs defined(2) itrm_brackets_all_unlift_vars[THEN itrm_sym] by blast qed also have "... ≃⇧^{+}y" using defined(2) by (rule itrm_brackets_dist) finally show ?thesis . qed end (* locale lifted_bracket *) end