nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:a840c232e04e
+:991b0e53f9dc
 Regularizing a theorem 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
 - Abstractions over a type that needs lifting are replaced
-by bounded abstactions:
+by bounded abstractions:
 \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
 - Equalities over the type being lifted are replaced by
 appropriate relations:
 A = B     \<Longrightarrow>     A \<approx> B
 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
 val ty_out = ty --> ty --> @{typ bool};
 val tys_out = tys_rel ---> ty_out;
 in
 (case (maps_lookup (ProofContext.theory_of lthy) s) of
-SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
+SOME (info) => list_comb (Const (#relfun info, tys_out),
+map (fn ty => tyRel ty rty rel lthy) tys)
 | NONE  => HOLogic.eq_const ty
 )
 end
 | _ => HOLogic.eq_const ty)
 *}
 (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)
 *}
 (*
 ML {*
-text {*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow> bool"};*}
 val r = Free ("R", dummyT);
-val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
+val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
 val t2 = Syntax.check_term @{context} t;
-Toplevel.program (fn () => cterm_of @{theory} t2)
+cterm_of @{theory} t2
-*}*)
+*}
+*)
 text {* Assumes that the given theorem is atomized *}
 ML {*
 fun build_regularize_goal thm rty rel lthy =
 Logic.mk_implies
 ((prop_of thm),
 (my_reg_inst lthy rel rty (prop_of thm)))
 *}
 lemma universal_twice:
-"(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
+assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
-by auto
+shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
+using * by auto
-lemma implication_twice:
-"(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+lemma implication_twice:
-by auto
+assumes a: "c \<longrightarrow> a"
+assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
-(*lemma equality_twice:
+shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-"a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+using a b by auto
-by auto*)
 ML {*
 fun regularize thm rty rel rel_eqv rel_refl lthy =
 let
 val goal = build_regularize_goal thm rty rel lthy;
 (rtac @{thm impI} THEN' atac),
 rtac @{thm implication_twice},
 EqSubst.eqsubst_tac ctxt [0]
 [(@{thm equiv_res_forall} OF [rel_eqv]),
 (@{thm equiv_res_exists} OF [rel_eqv])],
+(* For a = b \<longrightarrow> a \<approx> b *)
 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
 (rtac @{thm RIGHT_RES_FORALL_REGULAR})
 ]);
 val cthm = Goal.prove lthy [] [] goal
 (fn {context, ...} => tac context 1);
 *}
 section {* RepAbs injection *}
 (*
-Injecting RepAbs means:
+RepAbs injection is done in the following phases:
+1) build_repabs_term inserts rep-abs pairs in the term
+2) we prove the equality between the original theorem and this one
+3) we use Pure.equal_elim_rule1 to get the new theorem.
+build_repabs_term does:
 For abstractions:
 * If the type of the abstraction doesn't need lifting we recurse.
 * If it does we add RepAbs around the whole term and check if the
 variable needs lifting.
 * If it doesn't then we recurse
 * If it does we recurse and put 'RepAbs' around all occurences
-of the variable in the obtained subterm.
+of the variable in the obtained subterm. This in combination
+with the RepAbs above will let us change the type of the
+abstraction with rewriting.
 For applications:
 * If the term is 'Respects' applied to anything we leave it unchanged
 * If the term needs lifting and the head is a constant that we know
 how to lift, we put a RepAbs and recurse
 * If the term needs lifting and the head is a free applied to subterms
 (if it is not applied we treated it in Abs branch) then we
 put RepAbs and recurse
 * Otherwise just recurse.
-The injection is done in the following phases:
-1) build_repabs_term inserts rep-abs pairs in the term
-2) we prove the equality between the original theorem and this one
-3) we use Pure.equal_elim_rule1 to get the new theorem.
 To prove that the old theorem implies the new one, we first
 atomize it and then try:
-1) theorems 'trans2' from the QUOT_TYPE
+1) theorems 'trans2' from the appropriate QUOT_TYPE
 2) remove lambdas from both sides (LAMBDA_RES_TAC)
-3) remove Ball/Bex
+3) remove Ball/Bex from the right hand side
-4) use RSP theorems
+4) use user-supplied RSP theorems
-5) remove rep_abs from right side
+5) remove rep_abs from the right side
-6) reflexivity
+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) relation reflexive
+10) reflexivity of the relation
 11) assumption
+(Lambdas under respects may have left us some assumptions)
 12) proving obvious higher order equalities by simplifying fun_rel
-(not sure if still needed?)
+(not sure if it is still needed?)
 13) unfolding lambda on one side
 14) simplifying (= ===> =) for simpler respectfullness
 *)
 (* Needed 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}) *}
 ML {*
 fun build_repabs_term lthy thm consts rty qty =
 let
+(* TODO: The rty and qty stored in the quotient_info should
+be varified, so this will soon not be needed *)
 val rty = Logic.varifyT rty;
 val qty = Logic.varifyT qty;
 fun mk_abs tm =
 let
 else mk_repabs (
 if not (needs_lift rty vty) then t'
 else
 let
 val v' = mk_repabs v;
-(* TODO: I believe this is not needed any more *)
+(* TODO: I believe 'beta' is not needed any more *)
-val t1 = Envir.beta_norm (t' $ v')
+val t1 = (* Envir.beta_norm *) (t' $ v')
 in
 lambda v t1
 end)
 end
 | x =>
 repeat_eqsubst_prop lthy @{thms id_def_sym}
 (build_aux lthy (Thm.prop_of thm))
 end
 *}
-text {* Assumes that it is given a regularized theorem *}
+text {* Builds provable goals for regularized theorems *}
 ML {*
 fun build_repabs_goal ctxt thm cons rty qty =
 Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
 *}
 ML {*
 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
 end
-handle _ => no_tac
+handle _ => no_tac)
-)
+*}
+ML {*
+fun CHANGED' tac = (fn i => CHANGED (tac i))
 *}
 ML {*
 fun quotient_tac quot_thm =
 REPEAT_ALL_NEW (FIRST' [
 rtac @{thm FUN_QUOTIENT},
 rtac quot_thm,
 rtac @{thm IDENTITY_QUOTIENT},
-(
+(* For functional identity quotients, (op = ---> op =) *)
-fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN
+CHANGED' (
-rtac @{thm IDENTITY_QUOTIENT} i
+(simp_tac (HOL_ss addsimps @{thms FUN_MAP_I})) THEN'
+rtac @{thm IDENTITY_QUOTIENT}
 )
 ])
 *}
 ML {*
 fun LAMBDA_RES_TAC ctxt i st =
 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-(_ $ (_ $ (Abs(_, _, _))$(Abs(_, _, _)))) =>
+(_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
 | _ => fn _ => no_tac) i st
 *}
 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
 let
 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
 val insts = Thm.match (pat, concl)
 in
 if needs_lift rty (type_of f) then
 rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
 else no_tac
 end
 handle _ => no_tac)
 *}
 ML {*
 val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
 let
 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
 end
-handle _ => no_tac
+handle _ => no_tac)
-)
 *}
 ML {*
 val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
 let
 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
 end
-handle _ => no_tac
+handle _ => no_tac)
-)
+*}
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 *}
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
 (FIRST' [
 ball_rsp_tac ctxt,
 bex_rsp_tac ctxt,
 FIRST' (map rtac rsp_thms),
 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
 rtac refl,
-(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, 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})),
-(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-THEN_ALL_NEW (fn _ => no_tac)
-),
 WEAK_LAMBDA_RES_TAC ctxt,
-(fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i))
+CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
 ])
 *}
 ML {*
 fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =
 *}
 section {* Cleaning the goal *}
 lemma prod_fun_id: "prod_fun id id = id"
-apply (simp add: prod_fun_def)
+by (simp add: prod_fun_def)
-done
 lemma map_id: "map id x = x"
-apply (induct x)
+by (induct x) (simp_all)
-apply (simp_all add: map.simps)
-done
 ML {*
 fun simp_ids lthy thm =
 thm
 |> MetaSimplifier.rewrite_rule @{thms id_def_sym}
 in
 map Thm.varifyT defs_all
 end
 *}
+(* TODO: Check if it behaves properly with varifyed rty *)
 ML {*
 fun findabs_all rty tm =
 case tm of
 Abs(_, T, b) =>
 let
 | f $ a => (findabs_all rty f) @ (findabs_all rty a)
 | _ => [];
 fun findabs rty tm = distinct (op =) (findabs_all rty tm)
 *}
 ML {*
 fun findaps_all rty tm =
 case tm of
 Abs(_, T, b) =>
 findaps_all rty (subst_bound ((Free ("x", T)), b))
 (if needs_lift rty T then [T] else [])
 | _ => [];
 fun findaps rty tm = distinct (op =) (findaps_all rty tm)
 *}
+(* Currently useful only for LAMBDA_PRS *)
 ML {*
 fun make_simp_prs_thm lthy quot_thm thm typ =
 let
 val (_, [lty, rty]) = dest_Type typ;
 val thy = ProofContext.theory_of lthy;
 val (a1, e1) = findallex_all rty qty f;
 val (a2, e2) = findallex_all rty qty a;
 in (a1 @ a2, e1 @ e2) end
 | _ => ([], []);
 *}
 ML {*
 fun findallex lthy rty qty tm =
 let
 val (a, e) = findallex_all rty qty tm;
 val (ad, ed) = (map domain_type a, map domain_type e);
 singleton (ProofContext.export lthy' lthy) t_id
 end
 *}
 ML {*
-fun matches (ty1, ty2) =
-Type.raw_instance (ty1, Logic.varifyT ty2);
 fun lookup_quot_data lthy qty =
 let
+fun matches (ty1, ty2) =
+Type.raw_instance (ty1, Logic.varifyT ty2);
 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+(* TODO: Should no longer be needed *)
 val rty = Logic.unvarifyT (#rtyp quotdata)
 val rel = #rel quotdata
 val rel_eqv = #equiv_thm quotdata
 val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]
 val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]

changeset 303	991b0e53f9dc
parent 302	a840c232e04e
child 307	9aa3aba71ecc