nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:4771198ecfd8
+:d676974e3c89
 fun atomize_thm thm =
 let
 val thm' = Thm.freezeT (forall_intr_vars thm)
 val thm'' = ObjectLogic.atomize (cprop_of thm')
 in
-@{thm Pure.equal_elim_rule1} OF [thm'', thm']
+@{thm equal_elim_rule1} OF [thm'', thm']
 end
 *}
-ML {* atomize_thm @{thm list.induct} *}
 section {* infrastructure about id *}
 (* Need to have a meta-equality *)
 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
 by (simp add: id_def)
 (* TODO: can be also obtained with: *)
 ML {* symmetric (eq_reflection OF @{thms id_def}) *}
 lemma prod_fun_id: "prod_fun id id \<equiv> id"
 by (rule eq_reflection) (simp add: prod_fun_def)
 end
 *}
 section {*  Infrastructure about definitions *}
-text {* expects atomized definition *}
+(* expects atomized definitions *)
 ML {*
 fun add_lower_defs_aux lthy thm =
 let
 val e1 = @{thm fun_cong} OF [thm];
 val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
 in
 map Thm.varifyT defs_all
 end
 *}
-section {* infrastructure about collecting theorems for calling lifting *}
+section {* Infrastructure for collecting theorems for calling lifting *}
 ML {*
 fun lookup_quot_data lthy qty =
 let
 val qty_name = fst (dest_Type qty)
 in
 map (fst o dest_Const o snd o dest_term) def_terms
 end
 *}
 section {* Regularization *}
-ML {*
 (*
 Regularizing an rtrm means:
 - quantifiers over a type that needs lifting are replaced by
 bounded quantifiers, for example:
 \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P
 example with more complicated types of A, B:
 A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
 *)
+ML {*
 (* builds the relation that is the argument of respects *)
 fun mk_resp_arg lthy (rty, qty) =
 let
 val thy = ProofContext.theory_of lthy
 in
 val mk_babs = Const (@{const_name "Babs"}, dummyT)
 val mk_ball = Const (@{const_name "Ball"}, dummyT)
 val mk_bex  = Const (@{const_name "Bex"}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 *}
 ML {*
 (* - applies f to the subterm of an abstraction,   *)
 (*   otherwise to the given term,                  *)
 (* - used by REGULARIZE, therefore abstracted      *)
 else rtrm (* FIXME: check correspondence according to definitions *)
 | (rt, qt) =>
 raise (LIFT_MATCH "regularize (default)")
 *}
-ML {*
-fun mk_REGULARIZE_goal lthy rtrm qtrm =
-Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))
-*}
 (*
 To prove that the raw theorem implies the regularised one,
 we try in order:
 - Reflexivity of the relation
 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
 ]);
 *}
-lemma move_forall: "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
+lemma move_forall:
+"(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
 by auto
-lemma move_exists: "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
+lemma move_exists:
+"((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
 by auto
-lemma [mono]: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
+lemma [mono]:
+"(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
 by blast
 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
 by auto
 | _ => raise (LIFT_MATCH "injection")
 end
 end
 *}
-ML {*
+section {* RepAbs Injection Tactic *}
-fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =
-Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
-*}
-section {* RepAbs injection tactic *}
 (*
 To prove that the regularised theorem implies the abs/rep injected, we first
 atomize it and then try:
 1) theorems 'trans2' from the appropriate QUOT_TYPE
 ball_rsp_tac ctxt,
 rtac @{thm RES_EXISTS_RSP},
 bex_rsp_tac ctxt,
 FIRST' (map rtac rsp_thms),
 rtac refl,
-(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
+(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
-(APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
+(RANGE [SOLVES' (quotient_tac quot_thm)])),
+(APPLY_RSP_TAC rty ctxt THEN'
+(RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
 Cong_Tac.cong_tac @{thm cong},
 rtac @{thm ext},
 rtac reflex_thm,
 atac,
 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
 fun allex_prs_tac lthy quot =
 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
 THEN' (quotient_tac quot);
 *}
-ML {*
-let
-val parser = Args.context -- Scan.lift Args.name_source
-fun term_pat (ctxt, str) =
-str |> ProofContext.read_term_pattern ctxt
-|> ML_Syntax.print_term
-|> ML_Syntax.atomic
-in
-ML_Antiquote.inline "term_pat" (parser >> term_pat)
-end
-*}
 ML {*
 fun prep_trm thy (x, (T, t)) =
 (cterm_of thy (Var (x, T)), cterm_of thy t)
 fun prep_ty thy (x, (S, ty)) =
 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
 simp_tac (HOL_ss addsimps [reps_same])]
 end
 *}
-(* Genralisation of free variables in a goal *)
+section {* Genralisation of free variables in a goal *}
 ML {*
 fun inst_spec ctrm =
 let
 val cty = ctyp_of_term ctrm
 let
 val rthm' = atomize_thm rthm
 val rule = procedure_inst context (prop_of rthm') (term_of concl)
 val aps = find_aps (prop_of rthm') (term_of concl)
 in
-rtac rule THEN' RANGE [
+rtac rule THEN'
-rtac rthm',
+RANGE [rtac rthm',
 regularize_tac lthy [rel_eqv] rel_refl,
 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
-clean_tac lthy quot defs reps_same absrep aps
+clean_tac lthy quot defs reps_same absrep aps]
-]
 end 1) lthy
 *}
 end

changeset 404	d676974e3c89
parent 403	4771198ecfd8
child 405	8bc7428745ad