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
+ − 14
locale QUOT_TYPE =
+ − 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
+ − 93
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
+ − 94
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
+ − 95
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
(* Auxiliary data for the quotient package *)
597
+ − 97
use "quotient_info.ML"
+ − 98
+ − 99
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
+ − 100
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
lemmas [quot_thm] = fun_quotient
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
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
+ − 103
lemmas [quot_equiv] = identity_equivp
597
+ − 104
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
+ − 105
(* 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
+ − 106
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
+ − 107
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
+ − 108
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
+ − 109
id_def[THEN eq_reflection, symmetric]
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]
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
+ − 111
o_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
+ − 112
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
+ − 113
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
(* 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
+ − 115
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
+ − 116
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
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
+ − 118
(* Definition of the quotient types *)
725
+ − 119
use "quotient_typ.ML"
597
+ − 120
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
+ − 121
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
(* Definitions for quotient constants *)
597
+ − 123
use "quotient_def.ML"
+ − 124
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
+ − 125
(* Tactics for proving the lifted theorems *)
759
+ − 126
758
+ − 127
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
+ − 128
"equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
758
+ − 129
by (simp add: equivp_reflp)
597
+ − 130
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
+ − 131
(* 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
+ − 132
(* about the lifted theorem in a tactic. *)
758
+ − 133
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
+ − 134
"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
+ − 135
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
+ − 136
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
+ − 137
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
+ − 138
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
+ − 139
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
+ − 140
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
+ − 141
by (simp_all add: Quot_True_def ext)
751
+ − 142
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
+ − 143
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
+ − 144
by (simp add: Quot_True_def)
751
+ − 145
758
+ − 146
use "quotient_tacs.ML"
751
+ − 147
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
+ − 148
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
(* 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
+ − 150
(* 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
+ − 151
(*
597
+ − 152
lemma atomize_eqv[atomize]:
+ − 153
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+ − 154
proof
+ − 155
assume "A \<equiv> B"
+ − 156
then show "Trueprop A \<equiv> Trueprop B" by unfold
+ − 157
next
+ − 158
assume *: "Trueprop A \<equiv> Trueprop B"
+ − 159
have "A = B"
+ − 160
proof (cases A)
+ − 161
case True
+ − 162
have "A" by fact
+ − 163
then show "A = B" using * by simp
+ − 164
next
+ − 165
case False
+ − 166
have "\<not>A" by fact
+ − 167
then show "A = B" using * by auto
+ − 168
qed
+ − 169
then show "A \<equiv> B" by (rule eq_reflection)
+ − 170
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
+ − 171
*)
597
+ − 172
689
+ − 173
section {* Methods / Interface *}
+ − 174
632
+ − 175
ML {*
+ − 176
fun mk_method1 tac thm ctxt =
+ − 177
SIMPLE_METHOD (HEADGOAL (tac ctxt thm))
+ − 178
+ − 179
fun mk_method2 tac ctxt =
+ − 180
SIMPLE_METHOD (HEADGOAL (tac ctxt))
+ − 181
*}
+ − 182
+ − 183
method_setup lifting =
758
+ − 184
{* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *}
632
+ − 185
{* Lifting of theorems to quotient types. *}
+ − 186
+ − 187
method_setup lifting_setup =
758
+ − 188
{* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
632
+ − 189
{* Sets up the three goals for the lifting procedure. *}
+ − 190
+ − 191
method_setup regularize =
758
+ − 192
{* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
632
+ − 193
{* Proves automatically the regularization goals from the lifting procedure. *}
+ − 194
+ − 195
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
+ − 196
{* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
632
+ − 197
{* Proves automatically the rep/abs injection goals from the lifting procedure. *}
+ − 198
+ − 199
method_setup cleaning =
758
+ − 200
{* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
632
+ − 201
{* Proves automatically the cleaning goals from the lifting procedure. *}
+ − 202
597
+ − 203
end
+ − 204