(* Title: ETTS/ETTS.thy Author: Mihails Milehins Copyright 2021 (C) Mihails Milehins Extension of Types-To-Sets. *) section‹Isar commands and default settings for the ETTS› theory ETTS imports (*order is important*) "ETTS_Tools/ETTS_Tools" "Conditional_Transfer_Rule.CTR" "HOL-Types_To_Sets.Types_To_Sets" "HOL-Eisbach.Eisbach" keywords "tts_register_sbts" :: thy_goal_stmt and "tts_find_sbts" :: diag and "tts_theorem" "tts_lemma" "tts_corollary" "tts_proposition" :: thy_goal_stmt and "tts_lemmas" :: thy_defn and "tts_context" :: thy_decl_block and "tts" and "to" and "sbterms" and "substituting" and "given" and "applying" and "rewriting" and "eliminating" and "through" begin subsection‹Prerequisites› subsubsection‹Transfer for local typedef› text‹ The following content was ported from the content of the session ‹Types_To_Sets› in the main library of Isabelle/HOL with minor amendments. › context fixes Rep Abs A T assumes type: "type_definition Rep Abs A" assumes T_def: "T ≡ (λ(x::'a) (y::'b). x = Rep y)" begin lemma type_definition_Domainp': "is_equality a ⟹ Transfer.Rel a (Domainp T) (λx. x ∈ A)" proof - interpret type_definition Rep Abs A by (rule type) show "is_equality a ⟹ Transfer.Rel a (Domainp T) (λx. x ∈ A)" unfolding is_equality_def Transfer.Rel_def by (elim ssubst, unfold Domainp_iff[abs_def] T_def fun_eq_iff) (metis Abs_inverse Rep) qed lemma type_definition_Domainp: "Domainp T = (λx. x ∈ A)" proof - interpret type_definition Rep Abs A by (rule type) show ?thesis unfolding Domainp_iff[abs_def] T_def fun_eq_iff by (metis Abs_inverse Rep) qed lemma type_definition_Rangep: "Rangep T = (λx. True)" proof - interpret type_definition Rep Abs A by (rule type) show ?thesis unfolding T_def by auto qed lemma shows rep_in_S[simp]: "Rep x ∈ A" and rep_inverse[simp]: "Abs (Rep x) = x" and Abs_inverse[simp]: "y ∈ A ⟹ Rep (Abs y) = y" using type unfolding type_definition_def by auto end lemmas [transfer_rule] = ―‹prefer right-total rules› right_total_All_transfer right_total_UNIV_transfer right_total_Ex_transfer subsubsection‹Auxiliary› lemma ex_type_definition: fixes A :: "['a, 'b] ⇒ bool" assumes "right_total A" and "bi_unique A" shows "∃(Rep::'b ⇒ 'a) (Abs::'a ⇒ 'b). type_definition Rep Abs (Collect (Domainp A)) ∧ (∀b b'. A b b' = (b = Rep b'))" proof(unfold type_definition_def, intro exI conjI; intro allI) define Rep :: "'b ⇒ 'a" where Rep: "Rep = (λb'. (SOME b. A b b'))" define Abs :: "'a ⇒ 'b" where Abs: "Abs = (λb. (SOME b'. A b b'))" have Rep_b: "A (Rep b') b'" for b' unfolding Rep by (metis assms(1) right_totalE verit_sko_ex') have Abs_a: "b ∈ Collect (Domainp A) ⟹ A b (Abs b)" for b unfolding Abs by (simp add: assms(1) Domainp_iff someI_ex) show "Rep x ∈ Collect (Domainp A)" for x by (auto intro: Rep_b) show "Abs (Rep x) = x" for x using assms(2) by (auto dest: bi_uniqueDr intro: Abs_a Rep_b) show "y ∈ Collect (Domainp A) ⟶ Rep (Abs y) = y" for y using assms(2) by (auto dest: bi_uniqueDl intro: Abs_a Rep_b) show "A b b' = (b = Rep b')" for b b' using assms(2) by (meson Rep_b bi_uniqueDl) qed lemma ex_eq: "∃x. x = t" by simp subsection‹Import› ML_file‹ETTS_Tactics.ML› ML_file‹ETTS_Utilities.ML› ML_file‹ETTS_RI.ML› ML_file‹ETTS_Substitution.ML› ML_file‹ETTS_Context.ML› ML_file‹ETTS_Algorithm.ML› ML_file‹ETTS_Active.ML› ML_file‹ETTS_Lemma.ML› ML_file‹ETTS_Lemmas.ML› subsection‹Commands and attributes› ML ‹ (* Adopted (with amendments) from the theory Pure.thy *) ETTS_Lemma.tts_lemma \<^command_keyword>‹tts_theorem› "tts theorem"; ETTS_Lemma.tts_lemma \<^command_keyword>‹tts_lemma› "tts lemma"; ETTS_Lemma.tts_lemma \<^command_keyword>‹tts_corollary› "tts corollary"; ETTS_Lemma.tts_lemma \<^command_keyword>‹tts_proposition› "tts proposition"; › subsection‹Default settings› subsubsection‹\<^text>‹tts_implicit›› named_theorems tts_implicit subsubsection‹\<^text>‹tts_transfer_rule›› lemmas [transfer_rule] = right_total_UNIV_transfer right_total_Collect_transfer right_total_Inter_transfer right_total_Compl_transfer finite_transfer image_transfer end