nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:6cdba30c6d66
+:91c374abde06
 use "quotient_info.ML"
 declare [[map list = (map, LIST_REL)]]
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, FUN_REL)]]
+lemmas [quotient_thm] =
+FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
 end
 handle _ => no_tac)
 *}
 ML {*
-fun quotient_tac ctxt quot_thms =
+fun quotient_tac ctxt =
 REPEAT_ALL_NEW (FIRST'
-[rtac @{thm FUN_QUOTIENT},
+[resolve_tac (quotient_rules_get ctxt),
-resolve_tac quot_thms,
-rtac @{thm IDENTITY_QUOTIENT},
-rtac @{thm LIST_QUOTIENT},
 (* For functional identity quotients, (op = ---> op =) *)
 (* TODO: think about the other way around, if we need to shorten the relation *)
 CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
 *}
 (Abs a) => snd (Term.dest_abs a)
 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))  *}
 ML {*
-fun inj_repabs_tac ctxt quot_thms rel_refl trans2 =
+fun inj_repabs_tac ctxt 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> *)
 NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [
 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
 NDT ctxt "8" (rtac @{thm refl}),
 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
 (* observe ---> *)
 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt
-THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
+THEN' (RANGE [SOLVES' (quotient_tac ctxt)]))),
 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
-(RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+(RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
 (* merge with previous tactic *)
 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
 (* global simplification *)
 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
 *}
 ML {*
-fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 =
+fun all_inj_repabs_tac ctxt rel_refl trans2 =
-REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2)
+REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 section {* Cleaning of the theorem *}
 (* TODO: This is slow *)
 ML {*
-fun allex_prs_tac ctxt quot =
+fun allex_prs_tac ctxt =
-(EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)
+(EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt)
 *}
 ML {*
 fun make_inst lhs t =
 let
 in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
 (* It proves the QUOTIENT assumptions by calling quotient_tac *)
 ML {*
-fun solve_quotient_assum i quot_thms ctxt thm =
+fun solve_quotient_assum i ctxt thm =
 let
 val tac =
 (compose_tac (false, thm, i)) THEN_ALL_NEW
-(quotient_tac ctxt quot_thms);
+(quotient_tac ctxt);
 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 =
+fun lambda_allex_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_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 te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi]
+val te = @{thm eq_reflection} OF [solve_quotient_assum 2 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
 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];
+val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 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)) =>
 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];
+val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 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_allex_prs_conv quot =
+val lambda_allex_prs_conv =
-More_Conv.top_conv (lambda_allex_prs_simple_conv quot)
+More_Conv.top_conv lambda_allex_prs_simple_conv
 *}
 ML {*
-fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt)
+fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
 *}
 (*
 Cleaning the theorem consists of 6 kinds of rewrites.
 The first two need to be done before fun_map is unfolded
 The second one is an EqSubst (slow).
 The rest are a simp_tac and are fast.
 *)
 ML {*
-fun clean_tac lthy quot =
+fun clean_tac lthy =
 let
 val thy = ProofContext.theory_of lthy;
+val quotients = quotient_rules_get lthy
 val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
-val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients
 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
-val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients
 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 *)
 (* \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f *)
-NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy),
+NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
 (* NewConst  ---->  (rep ---> abs) oldConst *)
 (* Abs (Rep x)  ---->  x                    *)
 (* id_simps; fun_map.simps                  *)
 NDT lthy "c" (TRY o simp_tac simp_ctxt),
 *}
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv quot =
+fun lift_tac lthy rthm rel_eqv =
 ObjectLogic.full_atomize_tac
 THEN' gen_frees_tac lthy
 THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
 let
 val rthm' = atomize_thm rthm
 in
 EVERY1
 [rtac rule,
 RANGE [rtac rthm',
 regularize_tac lthy rel_eqv,
-rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2,
+rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2,
-clean_tac lthy quot]]
+clean_tac lthy]]
 end) lthy
 *}
 end

changeset 506	91c374abde06
parent 505	6cdba30c6d66
child 507	f7569f994195
child 508	fac6069d8e80