Theory Types_To_Sets_Extension.ETTS
section‹Isar commands and default settings for the ETTS›
theory ETTS
imports
"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] =
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 ‹
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