nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:1f2c8be84be7
+:2f0ad33f0241
 14) simplifying (= ===> =) for simpler respectfullness
 *)
 ML {*
-fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+fun instantiate_tac thm =
+Subgoal.FOCUS (fn {concl, ...} =>
 let
 val pat = Drule.strip_imp_concl (cprop_of thm)
 val insts = Thm.match (pat, concl)
 in
 rtac (Drule.instantiate insts thm) 1
 (* For functional identity quotients, (op = ---> op =) *)
 (* TODO: think about the other way around, if we need to shorten the relation *)
 CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])
 *}
-ML {*
+lemma FUN_REL_I:
-fun LAMBDA_RES_TAC ctxt i st =
+assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
-(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+shows "(R1 ===> R2) f g"
-(_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
+using a by (simp add: FUN_REL.simps)
-(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ML {*
-| _ => fn _ => no_tac) i st
+val LAMBDA_RES_TAC =
+SUBGOAL (fn (goal, i) =>
+case goal of
+(_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i
+| _ => no_tac)
 *}
 ML {*
 fun WEAK_LAMBDA_RES_TAC ctxt i st =
 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
 (FIRST' [
 resolve_tac trans2,
-LAMBDA_RES_TAC ctxt,
+LAMBDA_RES_TAC,
 rtac @{thm RES_FORALL_RSP},
 ball_rsp_tac ctxt,
 rtac @{thm RES_EXISTS_RSP},
 bex_rsp_tac ctxt,
 resolve_tac rsp_thms,
 atac,
 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
 WEAK_LAMBDA_RES_TAC ctxt,
 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
 ])
+fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 (*
 To prove that the regularised theorem implies the abs/rep injected,
 we try:
 1) theorems 'trans2' from the appropriate QUOT_TYPE
-2) remove lambdas from both sides (LAMBDA_RES_TAC)
+2) remove lambdas from both sides: LAMBDA_RES_TAC
 3) remove Ball/Bex from the right hand side
 4) use user-supplied RSP theorems
 5) remove rep_abs from the right side
 6) reflexivity of equality
 7) split applications of lifted type (apply_rsp)
 8) split applications of non-lifted type (cong_tac)
 9) apply extentionality
-10) reflexivity of the relation
+A) reflexivity of the relation
-11) assumption
+B) assumption
 (Lambdas under respects may have left us some assumptions)
-12) proving obvious higher order equalities by simplifying fun_rel
+C) proving obvious higher order equalities by simplifying fun_rel
 (not sure if it is still needed?)
-13) unfolding lambda on one side
+D) unfolding lambda on one side
-14) simplifying (= ===> =) for simpler respectfulness
+E) simplifying (= ===> =) for simpler respectfulness
 *)
 ML {*
 fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
-REPEAT_ALL_NEW (FIRST' [
+(FIRST' [
 (K (print_tac "start")) THEN' (K no_tac),
+(* "cong" rule of the of the relation    *)
+(* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *)
 DT ctxt "1" (resolve_tac trans2),
-DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+DT ctxt "2" (LAMBDA_RES_TAC),
+(* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
 DT ctxt "4" (ball_rsp_tac ctxt),
 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
 DT ctxt "6" (bex_rsp_tac ctxt),
+(* respectfulness of ops *)
 DT ctxt "7" (resolve_tac rsp_thms),
+(* reflexivity of operators arising from Cong_tac *)
 DT ctxt "8" (rtac @{thm refl}),
+(* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
+(* observe ---> *)
 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
+(* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP   provided type of t needs lifting *)
 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
+(* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+(* = (\<lambda>x\<dots>) (\<lambda>x\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
 DT ctxt "C" (rtac @{thm ext}),
+(* reflexivity of the basic relations *)
 DT ctxt "D" (resolve_tac rel_refl),
+(* resolving with R x y assumptions *)
 DT ctxt "E" (atac),
 DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
 DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
 ])
-*}
+fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
+*}
+ML {*
+fun get_inj_repabs_tac ctxt rel lhs rhs =
+let
+val _ = tracing "input"
+val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel)
+val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs)
+val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs)
+in
+case (rel, lhs, rhs) of
+(_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *)
+=> rtac @{thm REP_ABS_RSP(1)}
+| (_, Const (@{const_name "Ball"}, _) $ _,
+Const (@{const_name "Ball"}, _) $ _)
+=> rtac @{thm RES_FORALL_RSP}
+| _ => K no_tac
+end
+*}
+ML {*
+fun inj_repabs_tac ctxt =
+SUBGOAL (fn (goal, i) =>
+(case (HOLogic.dest_Trueprop goal) of
+(rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs
+| _ => K no_tac) i)
+*}
 section {* Cleaning of the theorem *}
 ML {*
 fun applic_prs lthy absrep (rty, qty) =

changeset 423	2f0ad33f0241
parent 420	dcfe009c98aa
child 424	ab6ddf2ec00c