equal
deleted
inserted
replaced
168 |
168 |
169 |
169 |
170 (* lifting of constants *) |
170 (* lifting of constants *) |
171 use "quotient_def.ML" |
171 use "quotient_def.ML" |
172 |
172 |
|
173 section {* Bounded abstraction *} |
|
174 |
173 definition |
175 definition |
174 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
176 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
175 where |
177 where |
176 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
178 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
|
179 |
|
180 section {* Simset setup *} |
|
181 |
|
182 (* since HOL_basic_ss is too "big", we need to set up *) |
|
183 (* our own minimal simpset *) |
|
184 ML {* |
|
185 fun mk_minimal_ss ctxt = |
|
186 Simplifier.context ctxt empty_ss |
|
187 setsubgoaler asm_simp_tac |
|
188 setmksimps (mksimps []) |
|
189 *} |
177 |
190 |
178 section {* atomize *} |
191 section {* atomize *} |
179 |
192 |
180 lemma atomize_eqv[atomize]: |
193 lemma atomize_eqv[atomize]: |
181 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
194 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
688 val thy = ProofContext.theory_of ctxt |
701 val thy = ProofContext.theory_of ctxt |
689 val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc)) |
702 val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc)) |
690 val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc)) |
703 val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc)) |
691 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc)) |
704 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc)) |
692 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc)) |
705 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc)) |
693 val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] |
706 val simp_ctxt = (mk_minimal_ss ctxt) addsimprocs [simproc1, simproc2, simproc3, simproc4] |
694 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
707 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
695 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
708 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
696 in |
709 in |
697 ObjectLogic.full_atomize_tac THEN' |
710 ObjectLogic.full_atomize_tac THEN' |
698 simp_tac simp_ctxt THEN' |
711 simp_tac simp_ctxt THEN' |
1148 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1161 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1149 (* FIXME: shouldn't the definitions already be varified? *) |
1162 (* FIXME: shouldn't the definitions already be varified? *) |
1150 val thms1 = @{thms all_prs ex_prs} @ defs |
1163 val thms1 = @{thms all_prs ex_prs} @ defs |
1151 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1164 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1152 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1165 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1153 fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
1166 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1154 (* FIXME: use of someting smaller than HOL_basic_ss *) |
|
1155 in |
1167 in |
1156 EVERY' [lambda_prs_tac lthy, |
1168 EVERY' [lambda_prs_tac lthy, |
1157 simp_tac (simps thms1), |
1169 simp_tac (simps thms1), |
1158 simp_tac (simps thms2), |
1170 simp_tac (simps thms2), |
1159 TRY o rtac refl] |
1171 TRY o rtac refl] |