diff -r 070161f1996a -r a082e2d138ab QuotMain.thy --- a/QuotMain.thy Sun Dec 06 11:39:34 2009 +0100 +++ b/QuotMain.thy Sun Dec 06 13:41:42 2009 +0100 @@ -5,11 +5,12 @@ ("quotient_def.ML") begin + locale QUOT_TYPE = fixes R :: "'a \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" and Rep :: "'b \ ('a \ bool)" - assumes equiv: "equivp R" + assumes equivp: "equivp R" and rep_prop: "\y. \x. Rep y = R x" and rep_inverse: "\x. Abs (Rep x) = x" and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" @@ -29,10 +30,10 @@ lemma lem9: shows "R (Eps (R x)) = R x" proof - - have a: "R x x" using equiv by (simp add: equivp_reflp_symp_transp reflp_def) + have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) then have "R x (Eps (R x))" by (rule someI) then show "R (Eps (R x)) = R x" - using equiv unfolding equivp_def by simp + using equivp unfolding equivp_def by simp qed theorem thm10: @@ -53,7 +54,7 @@ lemma REP_refl: shows "R (REP a) (REP a)" unfolding REP_def -by (simp add: equiv[simplified equivp_def]) +by (simp add: equivp[simplified equivp_def]) lemma lem7: shows "(R x = R y) = (Abs (R x) = Abs (R y))" @@ -66,7 +67,7 @@ theorem thm11: shows "R r r' = (ABS r = ABS r')" unfolding ABS_def -by (simp only: equiv[simplified equivp_def] lem7) +by (simp only: equivp[simplified equivp_def] lem7) lemma REP_ABS_rsp: @@ -80,7 +81,7 @@ apply(simp add: thm10) apply(simp add: REP_refl) apply(subst thm11[symmetric]) -apply(simp add: equiv[simplified equivp_def]) +apply(simp add: equivp[simplified equivp_def]) done lemma R_trans: @@ -88,7 +89,7 @@ and bc: "R b c" shows "R a c" proof - - have tr: "transp R" using equiv equivp_reflp_symp_transp[of R] by simp + have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp moreover have ab: "R a b" by fact moreover have bc: "R b c" by fact ultimately show "R a c" unfolding transp_def by blast @@ -98,7 +99,7 @@ assumes ab: "R a b" shows "R b a" proof - - have re: "symp R" using equiv equivp_reflp_symp_transp[of R] by simp + have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp then show "R b a" using ab unfolding symp_def by blast qed @@ -128,7 +129,7 @@ then show "a = b" using rep_inverse by simp next assume ab: "a = b" - have "reflp R" using equiv equivp_reflp_symp_transp[of R] by simp + have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto qed then show "R (REP a) (REP b) \ (a = b)" by simp @@ -151,6 +152,11 @@ lemmas [quotient_rsp] = quot_rel_rsp nil_rsp cons_rsp foldl_rsp +(* OPTION, PRODUCTS *) +lemmas [quotient_equiv] = + identity_equivp list_equivp + + ML {* maps_lookup @{theory} "List.list" *} ML {* maps_lookup @{theory} "*" *} ML {* maps_lookup @{theory} "fun" *} @@ -164,9 +170,6 @@ (* lifting of constants *) use "quotient_def.ML" -(* TODO: Consider defining it with an "if"; sth like: - Babs p m = \x. if x \ p then m x else undefined -*) definition Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" where @@ -240,7 +243,6 @@ Seq.single thm end *} - ML {* fun DT ctxt s tac i thm = let @@ -494,19 +496,14 @@ *) -(* FIXME: OPTION_equivp, PAIR_equivp, ... *) ML {* -fun equiv_tac rel_eqvs = +fun equiv_tac ctxt = REPEAT_ALL_NEW (FIRST' - [resolve_tac rel_eqvs, - rtac @{thm identity_equivp}, - rtac @{thm list_equivp}]) + [resolve_tac (equiv_rules_get ctxt)]) *} -thm ball_reg_eqv - ML {* -fun ball_reg_eqv_simproc rel_eqvs ss redex = +fun ball_reg_eqv_simproc ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt @@ -517,7 +514,7 @@ (let val gl = Const (@{const_name "equivp"}, dummyT) $ R; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) in @@ -530,7 +527,7 @@ *} ML {* -fun bex_reg_eqv_simproc rel_eqvs ss redex = +fun bex_reg_eqv_simproc ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt @@ -541,7 +538,7 @@ (let val gl = Const (@{const_name "equivp"}, dummyT) $ R; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]); (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) in @@ -574,7 +571,7 @@ *} ML {* -fun ball_reg_eqv_range_simproc rel_eqvs ss redex = +fun ball_reg_eqv_range_simproc ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt @@ -586,7 +583,7 @@ val gl = Const (@{const_name "equivp"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); (* val _ = tracing (Syntax.string_of_term ctxt glc);*) - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); val R1c = cterm_of thy R1; val thmi = Drule.instantiate' [] [SOME R1c] thm; @@ -608,7 +605,7 @@ thm bex_reg_eqv_range ML {* -fun bex_reg_eqv_range_simproc rel_eqvs ss redex = +fun bex_reg_eqv_range_simproc ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt @@ -620,7 +617,7 @@ val gl = Const (@{const_name "equivp"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); (* val _ = tracing (Syntax.string_of_term ctxt glc); *) - val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); + val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); val R1c = cterm_of thy R1; val thmi = Drule.instantiate' [] [SOME R1c] thm; @@ -642,20 +639,20 @@ by (simp add: equivp_reflp) ML {* -fun regularize_tac ctxt rel_eqvs = +fun regularize_tac ctxt = let val pat1 = [@{term "Ball (Respects R) P"}]; val pat2 = [@{term "Bex (Respects R) P"}]; val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; val thy = ProofContext.theory_of ctxt - val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) - val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) - val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) - val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) + val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc)) + val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc)) + val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc)) + val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc)) val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) - val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs + val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) in ObjectLogic.full_atomize_tac THEN' simp_tac simp_ctxt THEN' @@ -1221,21 +1218,21 @@ ML {* (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) -fun lift_tac ctxt rthm rel_eqv = +fun lift_tac ctxt rthm = ObjectLogic.full_atomize_tac THEN' gen_frees_tac ctxt THEN' CSUBGOAL (fn (gl, i) => let val rthm' = atomize_thm rthm val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv + val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) val quotients = quotient_rules_get ctxt val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} in (rtac rule THEN' RANGE [rtac rthm', - regularize_tac ctxt rel_eqv, + regularize_tac ctxt, rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, clean_tac ctxt]) i end)