--- 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 \<Rightarrow> 'a \<Rightarrow> bool"
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
- assumes equiv: "equivp R"
+ assumes equivp: "equivp R"
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
and rep_inverse: "\<And>x. Abs (Rep x) = x"
and abs_inverse: "\<And>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) \<equiv> (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 = \<lambda>x. if x \<in> p then m x else undefined
-*)
definition
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> '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)