--- a/IntEx.thy Sun Dec 06 02:41:35 2009 +0100
+++ b/IntEx.thy Sun Dec 06 04:03:08 2009 +0100
@@ -147,15 +147,37 @@
apply(rule refl)
done
-abbreviation
- "Abs \<equiv> ABS_my_int"
-abbreviation
- "Rep \<equiv> REP_my_int"
-abbreviation
- "Resp \<equiv> Respects"
-thm apply_rsp rep_abs_rsp lambda_prs
-ML {* map (Pattern.pattern o bare_concl o prop_of) @{thms apply_rsp rep_abs_rsp lambda_prs} *}
+(*
+lemma yy:
+ "(REP_my_int ---> id)
+ (\<lambda>x. Ball (Respects op \<approx>)
+ ((ABS_my_int ---> id)
+ ((REP_my_int ---> id)
+ (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
+ ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
+ (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)) \<approx>
+ (ABS_my_int ---> ABS_my_int ---> REP_my_int)
+ ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
+ (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)))))) =
+(\<lambda>x. Ball (Respects op \<approx>)
+ ((ABS_my_int ---> id)
+ ((REP_my_int ---> id)
+ (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
+ ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
+ (REP_my_int (ABS_my_int b)) \<approx>
+ (ABS_my_int ---> ABS_my_int ---> REP_my_int)
+ ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
+ (REP_my_int (ABS_my_int b))))))"
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [lambda_prs2 @{theory}]) 1*})
+
+apply(rule lambda_prs)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(simp add: id_simps)
+apply(tactic {* quotient_tac @{context} 1 *})
+done
+*)
+
lemma "PLUS a b = PLUS a b"
--- a/QuotMain.thy Sun Dec 06 02:41:35 2009 +0100
+++ b/QuotMain.thy Sun Dec 06 04:03:08 2009 +0100
@@ -1051,27 +1051,28 @@
in (f, Abs ("x", T, mk_abs 0 g)) end;
*}
-thm lambda_prs
-
ML {*
fun lambda_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
- ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
- let
- val (ty_b, ty_a) = dest_fun_type (fastype_of r1);
- val (ty_c, ty_d) = dest_fun_type (fastype_of a2);
- val thy = ProofContext.theory_of ctxt;
- val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
- val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
- val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs};
- val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
- val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
- val tl = Thm.lhs_of ts;
- val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
- val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
- in
- Conv.rewr_conv ti ctrm
- end
+ ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+ val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+ val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+ val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+ val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
+ val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
+ val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+ val tl = Thm.lhs_of ts
+ val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
+ val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+ (*val _ = tracing "lambda_prs"
+ val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
+ val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
+ in
+ Conv.rewr_conv ti ctrm
+ end
| _ => Conv.all_conv ctrm
*}
@@ -1083,29 +1084,27 @@
*}
(*
- Cleaning the theorem consists of 6 kinds of rewrites.
+ Cleaning the theorem consists of three rewriting steps.
The first two need to be done before fun_map is unfolded
- - lambda_prs:
+ 1) lambda_prs:
(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f
- - all_prs (and the same for exists: ex_prs)
- \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f
+ Implemented as conversion since it is not a pattern.
- - Rewriting with definitions from the argument defs
- NewConst ----> (rep ---> abs) oldConst
+ 2) all_prs (the same for exists):
+ Ball (Respects R) ((abs ---> id) f) ----> All f
- - Quotient_rel_rep:
- Rel (Rep x) (Rep y) ----> x = y
+ Rewriting with definitions from the argument defs
+ (rep ---> abs) oldConst ----> newconst
- - ABS_REP
- Abs (Rep x) ----> x
+ 3) Quotient_rel_rep:
+ Rel (Rep x) (Rep y) ----> x = y
- - id_simps; fun_map.simps
+ Quotient_abs_rep:
+ Abs (Rep x) ----> x
- The first one is implemented as a conversion (fast).
- The second one is an EqSubst (slow).
- The rest are a simp_tac and are fast.
+ id_simps; fun_map.simps
*)
ML {*
@@ -1113,28 +1112,17 @@
let
val thy = ProofContext.theory_of lthy;
val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+ (* FIXME: shouldn't the definitions already be varified? *)
val thms1 = @{thms all_prs ex_prs} @ defs
val thms2 = @{thms eq_reflection[OF fun_map.simps]}
@ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
- fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver
- (* FIXME: use of someting smaller than HOL_basic_ss *)
+ fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
+ (* FIXME: use of someting smaller than HOL_basic_ss *)
in
- EVERY' [
- (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *)
- NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
-
- (* Ball (Respects R) ((abs ---> id) f) ----> All f *)
- NDT lthy "b" (simp_tac (simp_ctxt thms1)),
-
- (* NewConst -----> (rep ---> abs) oldConst *)
- (* abs (rep x) -----> x *)
- (* R (Rep x) (Rep y) -----> x = y *)
- (* id_simps; fun_map.simps *)
- NDT lthy "c" (simp_tac (simp_ctxt thms2)),
-
- (* final step *)
- NDT lthy "d" (TRY o rtac refl)
- ]
+ EVERY' [lambda_prs_tac lthy,
+ simp_tac (simps thms1),
+ simp_tac (simps thms2),
+ TRY o rtac refl]
end
*}