64551
|
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
|
69296
|
7 |
keywords "lemmas_with"::thy_decl
|
64551
|
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 |
|
69295
|
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 |
|
64551
|
60 |
end
|
69295
|
61 |
|
69296
|
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 |
|
69295
|
90 |
end
|
69296
|
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 :} -- 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
|