src/HOL/Types_To_Sets/Examples/Prerequisites.thy
author wenzelm
Thu Mar 14 16:35:58 2019 +0100 (5 weeks ago)
changeset 69912 dd55d2c926d9
parent 69597 ff784d5a5bfb
permissions -rw-r--r--
tuned whitespace;
wenzelm@64551
     1
(*  Title:      HOL/Types_To_Sets/Examples/Prerequisites.thy
wenzelm@64551
     2
    Author:     Ondřej Kunčar, TU München
wenzelm@64551
     3
*)
wenzelm@64551
     4
wenzelm@64551
     5
theory Prerequisites
wenzelm@64551
     6
  imports Main
wenzelm@69912
     7
  keywords "lemmas_with" :: thy_decl
wenzelm@64551
     8
begin
wenzelm@64551
     9
wenzelm@64551
    10
context
wenzelm@64551
    11
  fixes Rep Abs A T
wenzelm@64551
    12
  assumes type: "type_definition Rep Abs A"
wenzelm@64551
    13
  assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
wenzelm@64551
    14
begin
wenzelm@64551
    15
wenzelm@64551
    16
lemma type_definition_Domainp: "Domainp T = (\<lambda>x. x \<in> A)"
wenzelm@64551
    17
proof -
wenzelm@64551
    18
  interpret type_definition Rep Abs A by(rule type)
wenzelm@64551
    19
  show ?thesis
wenzelm@64551
    20
    unfolding Domainp_iff[abs_def] T_def fun_eq_iff
wenzelm@64551
    21
    by (metis Abs_inverse Rep)
wenzelm@64551
    22
qed
wenzelm@64551
    23
wenzelm@64551
    24
end
wenzelm@64551
    25
immler@69295
    26
subsection \<open>setting up transfer for local typedef\<close>
immler@69295
    27
immler@69295
    28
lemmas [transfer_rule] = \<comment> \<open>prefer right-total rules\<close>
immler@69295
    29
  right_total_All_transfer
immler@69295
    30
  right_total_UNIV_transfer
immler@69295
    31
  right_total_Ex_transfer
immler@69295
    32
immler@69295
    33
locale local_typedef = fixes S ::"'b set" and s::"'s itself"
immler@69295
    34
  assumes Ex_type_definition_S: "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S"
immler@69295
    35
begin
immler@69295
    36
immler@69295
    37
definition "rep = fst (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
immler@69295
    38
definition "Abs = snd (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
immler@69295
    39
immler@69295
    40
lemma type_definition_S: "type_definition rep Abs S"
immler@69295
    41
  unfolding Abs_def rep_def split_beta'
immler@69295
    42
  by (rule someI_ex) (use Ex_type_definition_S in auto)
immler@69295
    43
immler@69295
    44
lemma rep_in_S[simp]: "rep x \<in> S"
immler@69295
    45
  and rep_inverse[simp]: "Abs (rep x) = x"
immler@69295
    46
  and Abs_inverse[simp]: "y \<in> S \<Longrightarrow> rep (Abs y) = y"
immler@69295
    47
  using type_definition_S
immler@69295
    48
  unfolding type_definition_def by auto
immler@69295
    49
immler@69295
    50
definition cr_S where "cr_S \<equiv> \<lambda>s b. s = rep b"
immler@69295
    51
lemmas Domainp_cr_S = type_definition_Domainp[OF type_definition_S cr_S_def, transfer_domain_rule]
immler@69295
    52
lemmas right_total_cr_S = typedef_right_total[OF type_definition_S cr_S_def, transfer_rule]
immler@69295
    53
  and bi_unique_cr_S = typedef_bi_unique[OF type_definition_S cr_S_def, transfer_rule]
immler@69295
    54
  and left_unique_cr_S = typedef_left_unique[OF type_definition_S cr_S_def, transfer_rule]
immler@69295
    55
  and right_unique_cr_S = typedef_right_unique[OF type_definition_S cr_S_def, transfer_rule]
immler@69295
    56
immler@69295
    57
lemma cr_S_rep[intro, simp]: "cr_S (rep a) a" by (simp add: cr_S_def)
immler@69295
    58
lemma cr_S_Abs[intro, simp]: "a\<in>S \<Longrightarrow> cr_S a (Abs a)" by (simp add: cr_S_def)
immler@69295
    59
wenzelm@64551
    60
end
immler@69295
    61
immler@69296
    62
subsection \<open>some \<close>
immler@69296
    63
immler@69296
    64
subsection \<open>Tool support\<close>
immler@69296
    65
immler@69296
    66
lemmas subset_iff' = subset_iff[folded Ball_def]
immler@69296
    67
immler@69296
    68
ML \<open>
immler@69296
    69
structure More_Simplifier =
immler@69296
    70
struct
immler@69296
    71
immler@69296
    72
fun asm_full_var_simplify ctxt thm =
immler@69296
    73
  let
immler@69296
    74
    val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
immler@69296
    75
  in
immler@69296
    76
    Simplifier.asm_full_simplify ctxt' thm'
immler@69296
    77
    |> singleton (Variable.export ctxt' ctxt)
immler@69296
    78
    |> Drule.zero_var_indexes
immler@69296
    79
  end
immler@69296
    80
immler@69296
    81
fun var_simplify_only ctxt ths thm =
immler@69296
    82
  asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm
immler@69296
    83
immler@69296
    84
val var_simplified = Attrib.thms >>
immler@69296
    85
  (fn ths => Thm.rule_attribute ths
immler@69296
    86
    (fn context => var_simplify_only (Context.proof_of context) ths))
immler@69296
    87
immler@69296
    88
val _ = Theory.setup (Attrib.setup \<^binding>\<open>var_simplified\<close> var_simplified "simplified rule (with vars)")
immler@69296
    89
immler@69295
    90
end
immler@69296
    91
\<close>
immler@69296
    92
immler@69296
    93
ML \<open>
immler@69296
    94
val _ = Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas_with\<close> "note theorems with (the same) attributes"
wenzelm@69597
    95
    (Parse.attribs --| \<^keyword>\<open>:\<close> -- Parse_Spec.name_facts -- Parse.for_fixes
immler@69296
    96
     >> (fn (((attrs),facts), fixes) =>
immler@69296
    97
      #2 oo Specification.theorems_cmd Thm.theoremK
immler@69296
    98
        (map (apsnd (map (apsnd (fn xs => attrs@xs)))) facts) fixes))
immler@69296
    99
\<close>
immler@69296
   100
immler@69296
   101
end