equal
deleted
inserted
replaced
|
1 (* Title: ??/QuotMain.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 *) |
|
4 |
1 theory QuotMain |
5 theory QuotMain |
2 imports QuotScript Prove |
6 imports QuotScript Prove |
3 uses ("quotient_info.ML") |
7 uses ("quotient_info.ML") |
4 ("quotient_typ.ML") |
8 ("quotient_typ.ML") |
5 ("quotient_def.ML") |
9 ("quotient_def.ML") |
87 |
91 |
88 end |
92 end |
89 |
93 |
90 section {* type definition for the quotient type *} |
94 section {* type definition for the quotient type *} |
91 |
95 |
92 (* the auxiliary data for the quotient types *) |
96 (* auxiliary data for the quotient package *) |
93 use "quotient_info.ML" |
97 use "quotient_info.ML" |
94 |
98 |
95 ML {* print_mapsinfo @{context} *} |
|
96 |
|
97 declare [[map "fun" = (fun_map, fun_rel)]] |
99 declare [[map "fun" = (fun_map, fun_rel)]] |
98 |
100 |
99 lemmas [quot_thm] = fun_quotient |
101 lemmas [quot_thm] = fun_quotient |
100 |
|
101 lemmas [quot_respect] = quot_rel_rsp |
102 lemmas [quot_respect] = quot_rel_rsp |
102 |
103 |
103 (* fun_map is not here since equivp is not true *) |
104 (* fun_map is not here since equivp is not true *) |
104 lemmas [quot_equiv] = identity_equivp |
105 lemmas [quot_equiv] = identity_equivp |
105 |
106 |
107 use "quotient_typ.ML" |
108 use "quotient_typ.ML" |
108 |
109 |
109 (* lifting of constants *) |
110 (* lifting of constants *) |
110 use "quotient_def.ML" |
111 use "quotient_def.ML" |
111 |
112 |
112 (* the translation functions *) |
113 (* the translation functions for the lifting process *) |
113 use "quotient_term.ML" |
114 use "quotient_term.ML" |
114 |
115 |
115 (* tactics *) |
116 (* tactics for proving the theorems *) |
|
117 |
116 lemma eq_imp_rel: |
118 lemma eq_imp_rel: |
117 "equivp R ==> a = b --> R a b" |
119 "equivp R ==> a = b \<longrightarrow> R a b" |
118 by (simp add: equivp_reflp) |
120 by (simp add: equivp_reflp) |
119 |
121 |
|
122 (* an auxiliar constant that records some information *) |
|
123 (* about the lifted theorem *) |
120 definition |
124 definition |
121 "QUOT_TRUE x \<equiv> True" |
125 "QUOT_TRUE x \<equiv> True" |
122 |
126 |
123 lemma quot_true_dests: |
127 lemma quot_true_dests: |
124 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
128 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
128 by (simp_all add: QUOT_TRUE_def ext) |
132 by (simp_all add: QUOT_TRUE_def ext) |
129 |
133 |
130 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
134 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
131 by (simp add: QUOT_TRUE_def) |
135 by (simp add: QUOT_TRUE_def) |
132 |
136 |
133 lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
137 lemma regularize_to_injection: |
134 by(auto simp add: QUOT_TRUE_def) |
138 shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
|
139 by(auto simp add: QUOT_TRUE_def) |
135 |
140 |
136 use "quotient_tacs.ML" |
141 use "quotient_tacs.ML" |
137 |
142 |
138 section {* Atomize Infrastructure *} |
143 (* atomize infrastructure *) |
139 |
|
140 lemma atomize_eqv[atomize]: |
144 lemma atomize_eqv[atomize]: |
141 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
145 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
142 proof |
146 proof |
143 assume "A \<equiv> B" |
147 assume "A \<equiv> B" |
144 then show "Trueprop A \<equiv> Trueprop B" by unfold |
148 then show "Trueprop A \<equiv> Trueprop B" by unfold |
155 then show "A = B" using * by auto |
159 then show "A = B" using * by auto |
156 qed |
160 qed |
157 then show "A \<equiv> B" by (rule eq_reflection) |
161 then show "A \<equiv> B" by (rule eq_reflection) |
158 qed |
162 qed |
159 |
163 |
160 section {* Infrastructure about id *} |
164 (* lemmas about simplifying id *) |
161 |
|
162 lemmas [id_simps] = |
165 lemmas [id_simps] = |
163 fun_map_id[THEN eq_reflection] |
166 fun_map_id[THEN eq_reflection] |
164 id_apply[THEN eq_reflection] |
167 id_apply[THEN eq_reflection] |
165 id_def[THEN eq_reflection,symmetric] |
168 id_def[THEN eq_reflection, symmetric] |
166 |
169 |
167 section {* Methods / Interface *} |
170 section {* Methods / Interface *} |
168 |
171 |
169 ML {* |
172 ML {* |
170 fun mk_method1 tac thm ctxt = |
173 fun mk_method1 tac thm ctxt = |