nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:070161f1996a
+:a082e2d138ab
 uses ("quotient_info.ML")
 ("quotient.ML")
 ("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)"
 and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
 begin
 "REP a = Eps (Rep a)"
 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:
 shows "ABS (REP a) \<equiv> a"
 apply  (rule eq_reflection)
 qed
 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))"
 apply(rule iffI)
 apply(simp)
 done
 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:
 shows "R f (REP (ABS g)) = R f g"
 and   "R (REP (ABS g)) f = R g f"
 "Quotient R ABS REP"
 apply(unfold Quotient_def)
 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:
 assumes ab: "R a b"
 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
 qed
 lemma R_sym:
 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
 lemma R_trans2:
 assumes ac: "R a c"
 then have "ABS x = ABS y" using thm11 by simp
 then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
 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
 qed
 fun_quotient list_quotient
 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" *}
 (* 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
 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 handle Subscript => "no subgoal"
 val _ = tracing (s ^ "\n" ^ prem_str)
 in
 Seq.single thm
 end *}
 ML {*
 fun DT ctxt s tac i thm =
 let
 val before_goal = nth (prems_of thm) (i - 1)
 - Ball (Respects ?E) ?P = All ?P
 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 *)
-(* FIXME: OPTION_equivp, PAIR_equivp, ... *)
+ML {*
-ML {*
+fun equiv_tac ctxt =
-fun equiv_tac rel_eqvs =
 REPEAT_ALL_NEW (FIRST'
-[resolve_tac rel_eqvs,
+[resolve_tac (equiv_rules_get ctxt)])
-rtac @{thm identity_equivp},
+*}
-rtac @{thm list_equivp}])
-*}
+ML {*
+fun ball_reg_eqv_simproc ss redex =
-thm ball_reg_eqv
-ML {*
-fun ball_reg_eqv_simproc rel_eqvs ss redex =
 let
 val ctxt = Simplifier.the_context ss
 val thy = ProofContext.theory_of ctxt
 in
 case redex of
 (ogl as ((Const (@{const_name "Ball"}, _)) $
 ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
 (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
 SOME thm
 end
 | _ => NONE
 end
 *}
 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
 in
 case redex of
 (ogl as ((Const (@{const_name "Bex"}, _)) $
 ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
 (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
 SOME thm
 end
 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 end
 *}
 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
 in
 case redex of
 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
 (let
 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;
 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*)
 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
 thm ball_reg_eqv_range
 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
 in
 case redex of
 ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
 (let
 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;
 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 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 simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
-val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs))
+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 rel_eqvs))
+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 rel_eqvs))
+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'
 REPEAT_ALL_NEW (FIRST' [
 rtac @{thm ball_reg_right},
 *}
 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)
 *}

changeset 582	a082e2d138ab
parent 578	070161f1996a
child 583	7414f6cb5398