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