diff -r 4fcbbb5b3b58 -r f78aa16daae5 QuotMain.thy --- 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: "(\x. x) \ 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 \ 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 \ bool) to (int 'b quo \ 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 \ bool) to (int 'b quo \ 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] *}