QuotMain.thy
changeset 582 a082e2d138ab
parent 578 070161f1996a
child 583 7414f6cb5398
--- 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)