1(*  Title:      HOL/Types_To_Sets/Examples/Prerequisites.thy
2    Author:     Ond��ej Kun��ar, TU M��nchen
3*)
4
5theory Prerequisites
6  imports Main
7  keywords "lemmas_with" :: thy_decl
8begin
9
10context
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)"
14begin
15
16lemma type_definition_Domainp: "Domainp T = (\<lambda>x. x \<in> A)"
17proof -
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)
22qed
23
24end
25
26subsection \<open>setting up transfer for local typedef\<close>
27
28lemmas [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
33locale 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"
35begin
36
37definition "rep = fst (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
38definition "Abs = snd (SOME (Rep::'s \<Rightarrow> 'b, Abs). type_definition Rep Abs S)"
39
40lemma 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
44lemma 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
50definition cr_S where "cr_S \<equiv> \<lambda>s b. s = rep b"
51lemmas Domainp_cr_S = type_definition_Domainp[OF type_definition_S cr_S_def, transfer_domain_rule]
52lemmas 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
57lemma cr_S_rep[intro, simp]: "cr_S (rep a) a" by (simp add: cr_S_def)
58lemma cr_S_Abs[intro, simp]: "a\<in>S \<Longrightarrow> cr_S a (Abs a)" by (simp add: cr_S_def)
59
60end
61
62subsection \<open>some \<close>
63
64subsection \<open>Tool support\<close>
65
66lemmas subset_iff' = subset_iff[folded Ball_def]
67
68ML \<open>
69structure More_Simplifier =
70struct
71
72fun 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
81fun var_simplify_only ctxt ths thm =
82  asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm
83
84val var_simplified = Attrib.thms >>
85  (fn ths => Thm.rule_attribute ths
86    (fn context => var_simplify_only (Context.proof_of context) ths))
87
88val _ = Theory.setup (Attrib.setup \<^binding>\<open>var_simplified\<close> var_simplified "simplified rule (with vars)")
89
90end
91\<close>
92
93ML \<open>
94val _ = 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
101end
102