72 theorem thm11: |
72 theorem thm11: |
73 shows "R r r' = (abs r = abs r')" |
73 shows "R r r' = (abs r = abs r')" |
74 unfolding abs_def |
74 unfolding abs_def |
75 by (simp only: equivp[simplified equivp_def] lem7) |
75 by (simp only: equivp[simplified equivp_def] lem7) |
76 |
76 |
77 |
|
78 lemma rep_abs_rsp: |
77 lemma rep_abs_rsp: |
79 shows "R f (rep (abs g)) = R f g" |
78 shows "R f (rep (abs g)) = R f g" |
80 and "R (rep (abs g)) f = R g f" |
79 and "R (rep (abs g)) f = R g f" |
81 by (simp_all add: thm10 thm11) |
80 by (simp_all add: thm10 thm11) |
82 |
81 |
83 lemma Quotient: |
82 lemma Quotient: |
84 "Quotient R abs rep" |
83 shows "Quotient R abs rep" |
85 apply(unfold Quotient_def) |
84 apply(unfold Quotient_def) |
86 apply(simp add: thm10) |
85 apply(simp add: thm10) |
87 apply(simp add: rep_refl) |
86 apply(simp add: rep_refl) |
88 apply(subst thm11[symmetric]) |
87 apply(subst thm11[symmetric]) |
89 apply(simp add: equivp[simplified equivp_def]) |
88 apply(simp add: equivp[simplified equivp_def]) |
90 done |
89 done |
91 |
90 |
92 end |
91 end |
93 |
92 |
94 section {* type definition for the quotient type *} |
93 |
95 |
94 section {* ML setup *} |
96 (* auxiliary data for the quotient package *) |
95 |
|
96 (* Auxiliary data for the quotient package *) |
97 use "quotient_info.ML" |
97 use "quotient_info.ML" |
98 |
98 |
99 declare [[map "fun" = (fun_map, fun_rel)]] |
99 declare [[map "fun" = (fun_map, fun_rel)]] |
100 |
100 |
101 lemmas [quot_thm] = fun_quotient |
101 lemmas [quot_thm] = fun_quotient |
102 lemmas [quot_respect] = quot_rel_rsp |
102 lemmas [quot_respect] = quot_rel_rsp |
103 |
|
104 (* fun_map is not here since equivp is not true *) |
|
105 lemmas [quot_equiv] = identity_equivp |
103 lemmas [quot_equiv] = identity_equivp |
106 |
104 |
107 (* definition of the quotient types *) |
105 (* Lemmas about simplifying id's. *) |
|
106 lemmas [id_simps] = |
|
107 fun_map_id[THEN eq_reflection] |
|
108 id_apply[THEN eq_reflection] |
|
109 id_def[THEN eq_reflection, symmetric] |
|
110 id_o[THEN eq_reflection] |
|
111 o_id[THEN eq_reflection] |
|
112 |
|
113 (* Definition of the quotient types *) |
108 use "quotient_typ.ML" |
114 use "quotient_typ.ML" |
109 |
115 |
110 (* lifting of constants *) |
116 |
|
117 (* Definitions for quotient constants *) |
111 use "quotient_def.ML" |
118 use "quotient_def.ML" |
112 |
119 |
113 (* the translation functions for the lifting process *) |
120 |
|
121 (* The translation functions for the lifting process. *) |
114 use "quotient_term.ML" |
122 use "quotient_term.ML" |
115 |
123 |
116 (* tactics for proving the theorems *) |
124 |
|
125 (* Tactics for proving the lifted theorems *) |
117 |
126 |
118 lemma eq_imp_rel: |
127 lemma eq_imp_rel: |
119 "equivp R ==> a = b \<longrightarrow> R a b" |
128 "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
120 by (simp add: equivp_reflp) |
129 by (simp add: equivp_reflp) |
121 |
130 |
122 (* an auxiliar constant that records some information *) |
131 (* An auxiliar constant for recording some information *) |
123 (* about the lifted theorem *) |
132 (* about the lifted theorem in a tactic. *) |
124 definition |
133 definition |
125 "QUOT_TRUE x \<equiv> True" |
134 "Quot_True x \<equiv> True" |
126 |
135 |
127 lemma quot_true_dests: |
136 lemma |
128 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
137 shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" |
129 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
138 and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P" |
130 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
139 and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))" |
131 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
140 and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)" |
132 by (simp_all add: QUOT_TRUE_def ext) |
141 by (simp_all add: Quot_True_def ext) |
133 |
142 |
134 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
143 lemma QT_imp: "Quot_True a \<equiv> Quot_True b" |
135 by (simp add: QUOT_TRUE_def) |
144 by (simp add: Quot_True_def) |
136 |
|
137 lemma regularize_to_injection: |
|
138 shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
|
139 by(auto simp add: QUOT_TRUE_def) |
|
140 |
145 |
141 use "quotient_tacs.ML" |
146 use "quotient_tacs.ML" |
142 |
147 |
143 (* atomize infrastructure *) |
148 |
|
149 (* Atomize infrastructure *) |
|
150 (* FIXME/TODO: is this really needed? *) |
|
151 (* |
144 lemma atomize_eqv[atomize]: |
152 lemma atomize_eqv[atomize]: |
145 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
153 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
146 proof |
154 proof |
147 assume "A \<equiv> B" |
155 assume "A \<equiv> B" |
148 then show "Trueprop A \<equiv> Trueprop B" by unfold |
156 then show "Trueprop A \<equiv> Trueprop B" by unfold |
191 method_setup regularize = |
191 method_setup regularize = |
192 {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} |
192 {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} |
193 {* Proves automatically the regularization goals from the lifting procedure. *} |
193 {* Proves automatically the regularization goals from the lifting procedure. *} |
194 |
194 |
195 method_setup injection = |
195 method_setup injection = |
196 {* Scan.succeed (mk_method2 Quotient_Tacs.all_inj_repabs_tac) *} |
196 {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *} |
197 {* Proves automatically the rep/abs injection goals from the lifting procedure. *} |
197 {* Proves automatically the rep/abs injection goals from the lifting procedure. *} |
198 |
198 |
199 method_setup cleaning = |
199 method_setup cleaning = |
200 {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} |
200 {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} |
201 {* Proves automatically the cleaning goals from the lifting procedure. *} |
201 {* Proves automatically the cleaning goals from the lifting procedure. *} |