Theory ETTS

(* 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