--- a/QuotMain.thy Wed Nov 25 14:25:29 2009 +0100
+++ b/QuotMain.thy Wed Nov 25 15:20:10 2009 +0100
@@ -201,32 +201,7 @@
ML {* atomize_thm @{thm list.induct} *}
-section {* RepAbs injection *}
-(*
-
-To prove that the old theorem implies the new one, we first
-atomize it and then try:
-
- 1) theorems 'trans2' from the appropriate QUOT_TYPE
- 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
-11) assumption
- (Lambdas under respects may have left us some assumptions)
-12) proving obvious higher order equalities by simplifying fun_rel
- (not sure if it is still needed?)
-13) unfolding lambda on one side
-14) simplifying (= ===> =) for simpler respectfullness
-
-*)
-
-
+section {* infrastructure about id *}
(* Need to have a meta-equality *)
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
@@ -234,21 +209,6 @@
(* TODO: can be also obtained with: *)
ML {* symmetric (eq_reflection OF @{thms id_def}) *}
-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)
-*}
-
-ML {*
-fun CHANGED' tac = (fn i => CHANGED (tac i))
-*}
-
lemma prod_fun_id: "prod_fun id id \<equiv> id"
by (rule eq_reflection) (simp add: prod_fun_def)
@@ -260,124 +220,11 @@
done
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 =) *)
- CHANGED' (
- (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
- )))
- ])
-*}
-
-ML {*
-fun LAMBDA_RES_TAC ctxt i st =
- (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
- (_ $ (_ $ (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
-*}
-
-ML {*
-fun WEAK_LAMBDA_RES_TAC ctxt i st =
- (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
- (_ $ (_ $ _ $ (Abs(_, _, _)))) =>
- (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
- (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
- | (_ $ (_ $ (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
-*}
-
-ML {* (* Legacy *)
-fun needs_lift (rty as Type (rty_s, _)) ty =
- case ty of
- Type (s, tys) =>
- (s = rty_s) orelse (exists (needs_lift rty) tys)
- | _ => false
-
-*}
-
-ML {*
-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
- val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
- (Const (@{const_name Ball}, _) $ _)) = term_of concl
- in
- ((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)
-*}
-
-ML {*
-val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
- let
- val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
- (Const (@{const_name Bex}, _) $ _)) = term_of concl
- in
- ((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)
-*}
-
-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' [
- rtac trans_thm,
- LAMBDA_RES_TAC ctxt,
- ball_rsp_tac ctxt,
- 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)])),
- (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})),
- WEAK_LAMBDA_RES_TAC ctxt,
- CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
- ])
-*}
-
-section {* Cleaning the goal *}
-
-
-ML {*
fun simp_ids lthy thm =
MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
*}
-text {* Does the same as 'subst' in a given prop or theorem *}
+section {* Does the same as 'subst' in a given theorem *}
ML {*
fun eqsubst_thm ctxt thms thm =
@@ -395,6 +242,8 @@
end
*}
+section {* Infrastructure about definitions *}
+
text {* expects atomized definition *}
ML {*
fun add_lower_defs_aux lthy thm =
@@ -419,140 +268,7 @@
end
*}
-ML {*
-fun findaps_all rty tm =
- case tm of
- Abs(_, T, b) =>
- findaps_all rty (subst_bound ((Free ("x", T)), b))
- | (f $ a) => (findaps_all rty f @ findaps_all rty a)
- | Free (_, (T as (Type ("fun", (_ :: _))))) =>
- (if needs_lift rty T then [T] else [])
- | _ => [];
-fun findaps rty tm = distinct (op =) (findaps_all rty tm)
-*}
-
-
-
-(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
-ML {*
-fun exchange_ty lthy rty qty ty =
- let
- val thy = ProofContext.theory_of lthy
- in
- if Sign.typ_instance thy (ty, rty) then
- let
- val inst = Sign.typ_match thy (rty, ty) Vartab.empty
- in
- Envir.subst_type inst qty
- end
- else
- let
- val (s, tys) = dest_Type ty
- in
- Type (s, map (exchange_ty lthy rty qty) tys)
- end
- end
- handle TYPE _ => ty (* for dest_Type *)
-*}
-
-
-ML {*
-fun find_matching_types rty ty =
- if Type.raw_instance (Logic.varifyT ty, rty)
- then [ty]
- else
- let val (s, tys) = dest_Type ty in
- flat (map (find_matching_types rty) tys)
- end
- handle TYPE _ => []
-*}
-
-ML {*
-fun negF absF = repF
- | negF repF = absF
-
-fun get_fun flag qenv lthy ty =
-let
-
- fun get_fun_aux s fs =
- (case (maps_lookup (ProofContext.theory_of lthy) s) of
- SOME info => list_comb (Const (#mapfun info, dummyT), fs)
- | NONE => error ("no map association for type " ^ s))
-
- fun get_const flag qty =
- let
- val thy = ProofContext.theory_of lthy
- val qty_name = Long_Name.base_name (fst (dest_Type qty))
- in
- case flag of
- absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
- | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
- end
-
- fun mk_identity ty = Abs ("", ty, Bound 0)
-
-in
- if (AList.defined (op=) qenv ty)
- then (get_const flag ty)
- else (case ty of
- TFree _ => mk_identity ty
- | Type (_, []) => mk_identity ty
- | Type ("fun" , [ty1, ty2]) =>
- let
- val fs_ty1 = get_fun (negF flag) qenv lthy ty1
- val fs_ty2 = get_fun flag qenv lthy ty2
- in
- get_fun_aux "fun" [fs_ty1, fs_ty2]
- end
- | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
- | _ => error ("no type variables allowed"))
-end
-*}
-
-ML {*
-fun get_fun_OLD flag (rty, qty) lthy ty =
- let
- val tys = find_matching_types rty ty;
- val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
- val xchg_ty = exchange_ty lthy rty qty ty
- in
- get_fun flag qenv lthy xchg_ty
- end
-*}
-
-ML {*
-fun applic_prs lthy rty qty absrep ty =
- let
- val rty = Logic.varifyT rty;
- val qty = Logic.varifyT qty;
- fun absty ty =
- exchange_ty lthy rty qty ty
- fun mk_rep tm =
- let
- val ty = exchange_ty lthy qty rty (fastype_of tm)
- in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
- fun mk_abs tm =
- let
- val ty = fastype_of tm
- in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
- val (l, ltl) = Term.strip_type ty;
- val nl = map absty l;
- val vs = map (fn _ => "x") l;
- val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
- val args = map Free (vfs ~~ nl);
- val lhs = list_comb((Free (fname, nl ---> ltl)), args);
- val rargs = map mk_rep args;
- val f = Free (fname, nl ---> ltl);
- val rhs = mk_abs (list_comb((mk_rep f), rargs));
- val eq = Logic.mk_equals (rhs, lhs);
- val ceq = cterm_of (ProofContext.theory_of lthy') eq;
- val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});
- val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
- val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
- in
- singleton (ProofContext.export lthy' lthy) t_id
- end
-*}
+section {* infrastructure about collecting theorems for calling lifting *}
ML {*
fun lookup_quot_data lthy qty =
@@ -947,6 +663,402 @@
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
+ 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
+11) assumption
+ (Lambdas under respects may have left us some assumptions)
+12) proving obvious higher order equalities by simplifying fun_rel
+ (not sure if it is still needed?)
+13) unfolding lambda on one side
+14) simplifying (= ===> =) for simpler respectfullness
+
+*)
+
+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)
+*}
+
+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 =) *)
+ CHANGED' (
+ (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
+ )))
+ ])
+*}
+
+ML {*
+fun LAMBDA_RES_TAC ctxt i st =
+ (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ (_ $ (_ $ (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
+*}
+
+ML {*
+fun WEAK_LAMBDA_RES_TAC ctxt i st =
+ (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+ (_ $ (_ $ _ $ (Abs(_, _, _)))) =>
+ (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+ (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+ | (_ $ (_ $ (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
+*}
+
+ML {* (* Legacy *)
+fun needs_lift (rty as Type (rty_s, _)) ty =
+ case ty of
+ Type (s, tys) =>
+ (s = rty_s) orelse (exists (needs_lift rty) tys)
+ | _ => false
+
+*}
+
+ML {*
+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
+ val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
+ (Const (@{const_name Ball}, _) $ _)) = term_of concl
+ in
+ ((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)
+*}
+
+ML {*
+val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+ let
+ val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
+ (Const (@{const_name Bex}, _) $ _)) = term_of concl
+ in
+ ((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)
+*}
+
+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' [
+ rtac trans_thm,
+ LAMBDA_RES_TAC ctxt,
+ ball_rsp_tac ctxt,
+ 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)])),
+ (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})),
+ WEAK_LAMBDA_RES_TAC ctxt,
+ CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
+ ])
+*}
+
+
+(****************************************)
+(* cleaning of the theorem *)
+(****************************************)
+
+
+
+(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
+ML {*
+fun exchange_ty lthy rty qty ty =
+ let
+ val thy = ProofContext.theory_of lthy
+ in
+ if Sign.typ_instance thy (ty, rty) then
+ let
+ val inst = Sign.typ_match thy (rty, ty) Vartab.empty
+ in
+ Envir.subst_type inst qty
+ end
+ else
+ let
+ val (s, tys) = dest_Type ty
+ in
+ Type (s, map (exchange_ty lthy rty qty) tys)
+ end
+ end
+ handle TYPE _ => ty (* for dest_Type *)
+*}
+
+
+ML {*
+fun find_matching_types rty ty =
+ if Type.raw_instance (Logic.varifyT ty, rty)
+ then [ty]
+ else
+ let val (s, tys) = dest_Type ty in
+ flat (map (find_matching_types rty) tys)
+ end
+ handle TYPE _ => []
+*}
+
+ML {*
+fun negF absF = repF
+ | negF repF = absF
+
+fun get_fun flag qenv lthy ty =
+let
+
+ fun get_fun_aux s fs =
+ (case (maps_lookup (ProofContext.theory_of lthy) s) of
+ SOME info => list_comb (Const (#mapfun info, dummyT), fs)
+ | NONE => error ("no map association for type " ^ s))
+
+ fun get_const flag qty =
+ let
+ val thy = ProofContext.theory_of lthy
+ val qty_name = Long_Name.base_name (fst (dest_Type qty))
+ in
+ case flag of
+ absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
+ | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
+ end
+
+ fun mk_identity ty = Abs ("", ty, Bound 0)
+
+in
+ if (AList.defined (op=) qenv ty)
+ then (get_const flag ty)
+ else (case ty of
+ TFree _ => mk_identity ty
+ | Type (_, []) => mk_identity ty
+ | Type ("fun" , [ty1, ty2]) =>
+ let
+ val fs_ty1 = get_fun (negF flag) qenv lthy ty1
+ val fs_ty2 = get_fun flag qenv lthy ty2
+ in
+ get_fun_aux "fun" [fs_ty1, fs_ty2]
+ end
+ | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
+ | _ => error ("no type variables allowed"))
+end
+*}
+
+ML {*
+fun get_fun_OLD flag (rty, qty) lthy ty =
+ let
+ val tys = find_matching_types rty ty;
+ val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
+ val xchg_ty = exchange_ty lthy rty qty ty
+ in
+ get_fun flag qenv lthy xchg_ty
+ end
+*}
+
+ML {*
+fun applic_prs lthy rty qty absrep ty =
+ let
+ val rty = Logic.varifyT rty;
+ val qty = Logic.varifyT qty;
+ fun absty ty =
+ exchange_ty lthy rty qty ty
+ fun mk_rep tm =
+ let
+ val ty = exchange_ty lthy qty rty (fastype_of tm)
+ in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
+ fun mk_abs tm =
+ let
+ val ty = fastype_of tm
+ in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
+ val (l, ltl) = Term.strip_type ty;
+ val nl = map absty l;
+ val vs = map (fn _ => "x") l;
+ val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+ val args = map Free (vfs ~~ nl);
+ val lhs = list_comb((Free (fname, nl ---> ltl)), args);
+ val rargs = map mk_rep args;
+ val f = Free (fname, nl ---> ltl);
+ val rhs = mk_abs (list_comb((mk_rep f), rargs));
+ val eq = Logic.mk_equals (rhs, lhs);
+ val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+ val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});
+ val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+ val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
+ in
+ singleton (ProofContext.export lthy' lthy) t_id
+ end
+*}
+
+
+ML {*
+fun findaps_all rty tm =
+ case tm of
+ Abs(_, T, b) =>
+ findaps_all rty (subst_bound ((Free ("x", T)), b))
+ | (f $ a) => (findaps_all rty f @ findaps_all rty a)
+ | Free (_, (T as (Type ("fun", (_ :: _))))) =>
+ (if needs_lift rty T then [T] else [])
+ | _ => [];
+fun findaps rty tm = distinct (op =) (findaps_all rty tm)
+*}
+
+
+ML {*
+(* FIXME: allex_prs and lambda_prs can be one function *)
+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)) =
+ (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+*}
+
+ML {*
+fun matching_prs thy pat trm =
+let
+ val univ = Unify.matchers thy [(pat, trm)]
+ val SOME (env, _) = Seq.pull univ
+ val tenv = Vartab.dest (Envir.term_env env)
+ val tyenv = Vartab.dest (Envir.type_env env)
+in
+ (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+end
+*}
+
+ML {*
+fun lambda_prs_conv1 ctxt quot 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 =
+ (compose_tac (false, lpi, 2)) THEN_ALL_NEW
+ (quotient_tac quot);
+ 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 [@{thm eq_reflection} OF @{thms id_apply}] te
+ val tl = Thm.lhs_of ts
+(* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
+(* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)
+ val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
+ val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
+(* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+ in
+ Conv.rewr_conv ti ctrm
+ end
+(* TODO: We can add a proper error message... *)
+ handle Bind => Conv.all_conv ctrm
+
+*}
+
+(* quot stands for the QUOTIENT theorems: *)
+(* could be potentially all of them *)
+ML {*
+fun lambda_prs_conv ctxt quot ctrm =
+ case (term_of ctrm) of
+ (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
+ (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
+ then_conv (lambda_prs_conv1 ctxt quot)) ctrm
+ | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
+ | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
+ | _ => Conv.all_conv ctrm
+*}
+
+ML {*
+fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
+ CONVERSION
+ (Conv.params_conv ~1 (fn ctxt =>
+ (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
+ Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
+*}
+
+ML {*
+fun clean_tac lthy quot defs reps_same =
+ let
+ val lower = flat (map (add_lower_defs lthy) defs)
+ in
+ EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
+ lambda_prs_tac lthy quot,
+ (* TODO: cleaning according to app_prs *)
+ 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 *)
@@ -1047,119 +1159,12 @@
end) ctxt
*}
-
-
-ML {*
-(* FIXME: allex_prs and lambda_prs can be one function *)
-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)) =
- (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
-*}
-
-ML {*
-fun matching_prs thy pat trm =
-let
- val univ = Unify.matchers thy [(pat, trm)]
- val SOME (env, _) = Seq.pull univ
- val tenv = Vartab.dest (Envir.term_env env)
- val tyenv = Vartab.dest (Envir.type_env env)
-in
- (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
-end
-*}
-
-ML {*
-fun lambda_prs_conv1 ctxt quot 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 =
- (compose_tac (false, lpi, 2)) THEN_ALL_NEW
- (quotient_tac quot);
- 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 [@{thm eq_reflection} OF @{thms id_apply}] te
- val tl = Thm.lhs_of ts
-(* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
-(* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)
- val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
- val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
-(* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
- in
- Conv.rewr_conv ti ctrm
- end
-(* TODO: We can add a proper error message... *)
- handle Bind => Conv.all_conv ctrm
-
-*}
-ML {*
-fun lambda_prs_conv ctxt quot ctrm =
- case (term_of ctrm) of
- (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) =>
- (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
- then_conv (lambda_prs_conv1 ctxt quot)) ctrm
- | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
- | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
- | _ => Conv.all_conv ctrm
-*}
-
-ML {*
-fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
- CONVERSION
- (Conv.params_conv ~1 (fn ctxt =>
- (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
- Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
-*}
-
-ML {*
- fun TRY' tac = fn i => TRY (tac i)
-*}
-
-ML {*
-fun clean_tac lthy quot defs reps_same =
- let
- val lower = flat (map (add_lower_defs lthy) defs)
- in
- TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
- TRY' (lambda_prs_tac lthy quot) THEN'
- TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
- simp_tac (HOL_ss addsimps [reps_same])
- end
-*}
-
ML {*
fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs =
- (procedure_tac thm lthy) THEN'
- (regularize_tac lthy rel_eqv rel_refl) THEN'
- (REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms)) THEN'
- (clean_tac lthy quot defs reps_same)
+ procedure_tac thm lthy THEN'
+ RANGE [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]
*}