nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:3a4da8a63840
+:6793659d38d6
 ML {*
 fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 =
 (FIRST' [
 (* "cong" rule of the of the relation / transitivity*)
 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-DT ctxt "1" (resolve_tac trans2),
+NDT ctxt "1" (resolve_tac trans2),
 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
 NDT ctxt "2" (lambda_rsp_tac),
 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 ML {*
 fun allex_prs_tac ctxt quot =
 (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)
 *}
-(* Rewrites the term with LAMBDA_PRS thm.
-Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
-with: f
-It proves the QUOTIENT assumptions by calling quotient_tac
-*)
 ML {*
 fun make_inst lhs t =
 let
 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
 val _ $ (Abs (_, _, g)) = t;
 | Bound j => if i = j then error "make_inst" else t
 | _ => t);
 in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
-ML {*
+(* It proves the QUOTIENT assumptions by calling quotient_tac *)
-fun lambda_prs_simple_conv quot_thms ctxt ctrm =
+ML {*
-case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
+fun solve_quotient_assum i quot_thms ctxt thm =
+let
+val tac =
+(compose_tac (false, thm, i)) THEN_ALL_NEW
+(quotient_tac ctxt quot_thms);
+val gc = Drule.strip_imp_concl (cprop_of thm);
+in
+Goal.prove_internal [] gc (fn _ => tac 1)
+end
+handle _ => error "solve_quotient_assum"
+*}
+ML {*
+fun lambda_allex_prs_simple_conv quot_thms ctxt ctrm =
+case (term_of ctrm) of
+((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
 let
 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
 val thy = ProofContext.theory_of ctxt;
 val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_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 tac =
+val te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi]
-(compose_tac (false, lpi, 2)) THEN_ALL_NEW
-(quotient_tac ctxt quot_thms);
-val gc = Drule.strip_imp_concl (cprop_of lpi);
-val t = Goal.prove_internal [] gc (fn _ => tac 1)
-val te = @{thm eq_reflection} OF [t]
 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 _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+in
+Conv.rewr_conv ti ctrm
+end
+| (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $
+(((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
+let
+val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf);
+val thy = ProofContext.theory_of ctxt;
+val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
+val tyinst = [SOME cty_a, SOME cty_b];
+val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
+val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
+val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
+in
+Conv.rewr_conv ti ctrm
+end
+| (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $
+(((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
+let
+val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf);
+val thy = ProofContext.theory_of ctxt;
+val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
+val tyinst = [SOME cty_a, SOME cty_b];
+val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
+val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
+val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
 in
 Conv.rewr_conv ti ctrm
 end
 | _ => Conv.all_conv ctrm
 *}
 (* quot stands for the QUOTIENT theorems: *)
 (* could be potentially all of them       *)
 ML {*
-fun lambda_prs_conv quot =
+fun lambda_allex_prs_conv quot =
-More_Conv.top_conv (lambda_prs_simple_conv quot)
+More_Conv.top_conv (lambda_allex_prs_simple_conv quot)
 *}
 ML {*
-fun lambda_prs_tac quot ctxt = CONVERSION (lambda_prs_conv quot ctxt)
+fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt)
 *}
 (*
 Cleaning the theorem consists of 6 kinds of rewrites.
 The first two need to be done before fun_map is unfolded
 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.
 *)
-thm all_prs ex_prs
 ML {*
 fun clean_tac lthy quot defs =
 let
 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
 in
 EVERY' [
 (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f *)
-DT lthy "a" (TRY o lambda_prs_tac quot lthy),
 (* \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f *)
-DT lthy "b" (TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot)),
+NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy),
 (* NewConst  ---->  (rep ---> abs) oldConst *)
 (* Abs (Rep x)  ---->  x                    *)
 (* id_simps; fun_map.simps                  *)
-DT lthy "c" (TRY o simp_tac simp_ctxt),
+NDT lthy "c" (TRY o simp_tac simp_ctxt),
 (* final step *)
-DT lthy "d" (TRY o rtac refl)
+NDT lthy "d" (TRY o rtac refl)
 ]
 end
 *}
 section {* Genralisation of free variables in a goal *}

changeset 492	6793659d38d6
parent 491	3a4da8a63840
child 493	672b94510e7d