759
+ − 1
(* Title: ??/QuotMain.thy
+ − 2
Author: Cezary Kaliszyk and Christian Urban
+ − 3
*)
+ − 4
597
+ − 5
theory QuotMain
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 6
imports QuotScript Prove
597
+ − 7
uses ("quotient_info.ML")
725
+ − 8
("quotient_typ.ML")
597
+ − 9
("quotient_def.ML")
758
+ − 10
("quotient_term.ML")
+ − 11
("quotient_tacs.ML")
597
+ − 12
begin
+ − 13
781
+ − 14
locale Quot_Type =
597
+ − 15
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ − 16
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ − 17
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ − 18
assumes equivp: "equivp R"
+ − 19
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ − 20
and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ − 21
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ − 22
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+ − 23
begin
+ − 24
+ − 25
definition
719
+ − 26
abs::"'a \<Rightarrow> 'b"
597
+ − 27
where
719
+ − 28
"abs x \<equiv> Abs (R x)"
597
+ − 29
+ − 30
definition
719
+ − 31
rep::"'b \<Rightarrow> 'a"
597
+ − 32
where
719
+ − 33
"rep a = Eps (Rep a)"
597
+ − 34
+ − 35
lemma lem9:
+ − 36
shows "R (Eps (R x)) = R x"
+ − 37
proof -
+ − 38
have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
+ − 39
then have "R x (Eps (R x))" by (rule someI)
+ − 40
then show "R (Eps (R x)) = R x"
+ − 41
using equivp unfolding equivp_def by simp
+ − 42
qed
+ − 43
+ − 44
theorem thm10:
719
+ − 45
shows "abs (rep a) \<equiv> a"
597
+ − 46
apply (rule eq_reflection)
719
+ − 47
unfolding abs_def rep_def
597
+ − 48
proof -
+ − 49
from rep_prop
+ − 50
obtain x where eq: "Rep a = R x" by auto
+ − 51
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+ − 52
also have "\<dots> = Abs (R x)" using lem9 by simp
+ − 53
also have "\<dots> = Abs (Rep a)" using eq by simp
+ − 54
also have "\<dots> = a" using rep_inverse by simp
+ − 55
finally
+ − 56
show "Abs (R (Eps (Rep a))) = a" by simp
+ − 57
qed
+ − 58
719
+ − 59
lemma rep_refl:
+ − 60
shows "R (rep a) (rep a)"
+ − 61
unfolding rep_def
597
+ − 62
by (simp add: equivp[simplified equivp_def])
+ − 63
+ − 64
lemma lem7:
+ − 65
shows "(R x = R y) = (Abs (R x) = Abs (R y))"
+ − 66
apply(rule iffI)
+ − 67
apply(simp)
+ − 68
apply(drule rep_inject[THEN iffD2])
+ − 69
apply(simp add: abs_inverse)
+ − 70
done
+ − 71
+ − 72
theorem thm11:
719
+ − 73
shows "R r r' = (abs r = abs r')"
+ − 74
unfolding abs_def
597
+ − 75
by (simp only: equivp[simplified equivp_def] lem7)
+ − 76
719
+ − 77
lemma rep_abs_rsp:
+ − 78
shows "R f (rep (abs g)) = R f g"
+ − 79
and "R (rep (abs g)) f = R g f"
597
+ − 80
by (simp_all add: thm10 thm11)
+ − 81
+ − 82
lemma Quotient:
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 83
shows "Quotient R abs rep"
597
+ − 84
apply(unfold Quotient_def)
+ − 85
apply(simp add: thm10)
719
+ − 86
apply(simp add: rep_refl)
597
+ − 87
apply(subst thm11[symmetric])
+ − 88
apply(simp add: equivp[simplified equivp_def])
+ − 89
done
+ − 90
+ − 91
end
+ − 92
789
+ − 93
term Quot_Type.abs
597
+ − 94
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
section {* ML setup *}
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 96
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 97
(* Auxiliary data for the quotient package *)
597
+ − 98
use "quotient_info.ML"
+ − 99
+ − 100
declare [[map "fun" = (fun_map, fun_rel)]]
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
lemmas [quot_thm] = fun_quotient
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 103
lemmas [quot_respect] = quot_rel_rsp
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 104
lemmas [quot_equiv] = identity_equivp
597
+ − 105
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 106
(* Lemmas about simplifying id's. *)
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 107
lemmas [id_simps] =
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 108
fun_map_id[THEN eq_reflection]
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 109
id_apply[THEN eq_reflection]
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 110
id_o[THEN eq_reflection]
854
5961edda27d7
absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 111
id_def[symmetric, THEN eq_reflection]
825
+ − 112
o_id[THEN eq_reflection]
+ − 113
eq_comp_r
774
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 114
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 115
(* The translation functions for the lifting process. *)
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 116
use "quotient_term.ML"
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 117
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 118
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 119
(* Definition of the quotient types *)
725
+ − 120
use "quotient_typ.ML"
597
+ − 121
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 122
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 123
(* Definitions for quotient constants *)
597
+ − 124
use "quotient_def.ML"
+ − 125
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 126
(* Tactics for proving the lifted theorems *)
759
+ − 127
758
+ − 128
lemma eq_imp_rel:
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 129
"equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
758
+ − 130
by (simp add: equivp_reflp)
597
+ − 131
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 132
(* An auxiliar constant for recording some information *)
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 133
(* about the lifted theorem in a tactic. *)
758
+ − 134
definition
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 135
"Quot_True x \<equiv> True"
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 136
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 137
lemma
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 138
shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 140
and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 141
and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142
by (simp_all add: Quot_True_def ext)
751
+ − 143
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
by (simp add: Quot_True_def)
751
+ − 146
758
+ − 147
use "quotient_tacs.ML"
751
+ − 148
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 149
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
(* Atomize infrastructure *)
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 151
(* FIXME/TODO: is this really needed? *)
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
(*
597
+ − 153
lemma atomize_eqv[atomize]:
+ − 154
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+ − 155
proof
+ − 156
assume "A \<equiv> B"
+ − 157
then show "Trueprop A \<equiv> Trueprop B" by unfold
+ − 158
next
+ − 159
assume *: "Trueprop A \<equiv> Trueprop B"
+ − 160
have "A = B"
+ − 161
proof (cases A)
+ − 162
case True
+ − 163
have "A" by fact
+ − 164
then show "A = B" using * by simp
+ − 165
next
+ − 166
case False
+ − 167
have "\<not>A" by fact
+ − 168
then show "A = B" using * by auto
+ − 169
qed
+ − 170
then show "A \<equiv> B" by (rule eq_reflection)
+ − 171
qed
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 172
*)
597
+ − 173
689
+ − 174
section {* Methods / Interface *}
+ − 175
632
+ − 176
ML {*
+ − 177
fun mk_method1 tac thm ctxt =
+ − 178
SIMPLE_METHOD (HEADGOAL (tac ctxt thm))
+ − 179
+ − 180
fun mk_method2 tac ctxt =
+ − 181
SIMPLE_METHOD (HEADGOAL (tac ctxt))
+ − 182
*}
+ − 183
+ − 184
method_setup lifting =
758
+ − 185
{* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *}
632
+ − 186
{* Lifting of theorems to quotient types. *}
+ − 187
+ − 188
method_setup lifting_setup =
758
+ − 189
{* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
632
+ − 190
{* Sets up the three goals for the lifting procedure. *}
+ − 191
+ − 192
method_setup regularize =
758
+ − 193
{* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
632
+ − 194
{* Proves automatically the regularization goals from the lifting procedure. *}
+ − 195
+ − 196
method_setup injection =
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 197
{* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
632
+ − 198
{* Proves automatically the rep/abs injection goals from the lifting procedure. *}
+ − 199
+ − 200
method_setup cleaning =
758
+ − 201
{* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
632
+ − 202
{* Proves automatically the cleaning goals from the lifting procedure. *}
+ − 203
597
+ − 204
end
+ − 205