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 *)
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 98
597
+ − 99
use "quotient_info.ML"
+ − 100
+ − 101
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
+ − 102
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 103
lemmas [quot_thm] = fun_quotient
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 104
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
+ − 105
lemmas [quot_equiv] = identity_equivp
597
+ − 106
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
+ − 107
(* 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
+ − 108
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
+ − 109
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
+ − 110
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
+ − 111
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
+ − 112
id_def[symmetric, THEN eq_reflection]
825
+ − 113
o_id[THEN eq_reflection]
+ − 114
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
+ − 115
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
(* 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
+ − 117
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
+ − 118
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 119
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
+ − 120
(* Definition of the quotient types *)
725
+ − 121
use "quotient_typ.ML"
597
+ − 122
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
+ − 123
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
+ − 124
(* Definitions for quotient constants *)
597
+ − 125
use "quotient_def.ML"
+ − 126
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
+ − 127
(* Tactics for proving the lifted theorems *)
759
+ − 128
758
+ − 129
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
+ − 130
"equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
758
+ − 131
by (simp add: equivp_reflp)
597
+ − 132
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
+ − 133
(* 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
+ − 134
(* about the lifted theorem in a tactic. *)
758
+ − 135
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
+ − 136
"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
+ − 137
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
+ − 138
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
+ − 139
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
+ − 140
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
+ − 141
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
+ − 142
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
+ − 143
by (simp_all add: Quot_True_def ext)
751
+ − 144
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
+ − 145
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
+ − 146
by (simp add: Quot_True_def)
751
+ − 147
758
+ − 148
use "quotient_tacs.ML"
751
+ − 149
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
+ − 150
689
+ − 151
section {* Methods / Interface *}
+ − 152
632
+ − 153
ML {*
+ − 154
fun mk_method1 tac thm ctxt =
+ − 155
SIMPLE_METHOD (HEADGOAL (tac ctxt thm))
+ − 156
+ − 157
fun mk_method2 tac ctxt =
+ − 158
SIMPLE_METHOD (HEADGOAL (tac ctxt))
+ − 159
*}
+ − 160
+ − 161
method_setup lifting =
758
+ − 162
{* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *}
632
+ − 163
{* Lifting of theorems to quotient types. *}
+ − 164
+ − 165
method_setup lifting_setup =
758
+ − 166
{* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
632
+ − 167
{* Sets up the three goals for the lifting procedure. *}
+ − 168
+ − 169
method_setup regularize =
758
+ − 170
{* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
632
+ − 171
{* Proves automatically the regularization goals from the lifting procedure. *}
+ − 172
+ − 173
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
+ − 174
{* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
632
+ − 175
{* Proves automatically the rep/abs injection goals from the lifting procedure. *}
+ − 176
+ − 177
method_setup cleaning =
758
+ − 178
{* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
632
+ − 179
{* Proves automatically the cleaning goals from the lifting procedure. *}
+ − 180
597
+ − 181
end
+ − 182