nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:c6a9b4e4d548
+:40bb0c4718a6
 use "quotient.ML"
 (* lifting of constants *)
 use "quotient_def.ML"
-text {* FIXME: auxiliary function *}
-ML {*
-val no_vars = Thm.rule_attribute (fn context => fn th =>
-let
-val ctxt = Variable.set_body false (Context.proof_of context);
-val ((_, [th']), _) = Variable.import true [th] ctxt;
-in th' end);
-*}
 section {* ATOMIZE *}
 lemma atomize_eqv[atomize]:
 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
 else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
 | _ => trm
 *}
+(* For polymorphic types we need to find the type of the Relation term. *)
+(* TODO: we assume that the relation is a Constant. Is this always true? *)
 ML {*
 fun my_reg_inst lthy rel rty trm =
 case rel of
 Const (n, _) => Syntax.check_term lthy
 (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"};*}
+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 t2 = Syntax.check_term @{context} t;
 Toplevel.program (fn () => cterm_of @{theory} t2)
 *}*)
 lemma implication_twice:
 "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 by auto
-(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+(*lemma equality_twice:
+"a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
 by auto*)
 ML {*
 fun regularize thm rty rel rel_eqv rel_refl lthy =
 let
 val goal = build_regularize_goal thm rty rel lthy;
 fun tac ctxt =
 (ObjectLogic.full_atomize_tac) THEN'
 REPEAT_ALL_NEW (FIRST' [
 rtac rel_refl,
 atac,
 rtac @{thm universal_twice},
 (rtac @{thm impI} THEN' atac),
 rtac @{thm implication_twice},
-(*rtac @{thm equality_twice},*)
+EqSubst.eqsubst_tac ctxt [0]
-EqSubst.eqsubst_tac ctxt [0]
+[(@{thm equiv_res_forall} OF [rel_eqv]),
-[(@{thm equiv_res_forall} OF [rel_eqv]),
+(@{thm equiv_res_exists} OF [rel_eqv])],
-(@{thm equiv_res_exists} OF [rel_eqv])],
+(rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
-(rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+(rtac @{thm RIGHT_RES_FORALL_REGULAR})
-(rtac @{thm RIGHT_RES_FORALL_REGULAR})
+]);
-]);
+val cthm = Goal.prove lthy [] [] goal
-val cthm = Goal.prove lthy [] [] goal
+(fn {context, ...} => tac context 1);
-(fn {context,...} => tac context 1);
 in
 cthm OF [thm]
 end
 *}
 section {* RepAbs injection *}
+(*
+Injecting RepAbs means:
+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.
+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
+2) remove lambdas from both sides (LAMBDA_RES_TAC)
+3) remove Ball/Bex
+4) use RSP theorems
+5) remove rep_abs from right side
+6) reflexivity
+7) split applications of lifted type (apply_rsp)
+8) split applications of non-lifted type (cong_tac)
+9) apply extentionality
+10) relation reflexive
+11) assumption
+12) proving obvious higher order equalities by simplifying fun_rel
+(not sure if 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)
 in
 if (Sign.typ_instance thy (ty, rty))
 then (get_const flag (ty, (exchange_ty lthy rty qty ty)))
 else (case ty of
 TFree _ => (mk_identity ty, (ty, ty))
 | Type (_, []) => (mk_identity ty, (ty, ty))
 | Type ("fun" , [ty1, ty2]) =>
-get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2]
+get_fun_fun [get_fun_noexchange (negF flag) (rty, qty) lthy ty1,
+get_fun_noexchange flag (rty, qty) lthy ty2]
 | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys)
 | _ => raise ERROR ("no type variables"))
 end
 fun get_fun_noex flag (rty, qty) lthy ty =
 fst (get_fun_noexchange flag (rty, qty) lthy ty)
 | SOME th => cprem_of th 1
 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
 in
-@{thm Pure.equal_elim_rule1} OF [rt,thm]
+@{thm Pure.equal_elim_rule1} OF [rt, thm]
 end
 *}
 ML {*
 fun repeat_eqsubst_thm ctxt thms thm =
 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
 handle _ => thm
 *}
 ML {*
-fun build_repabs_term lthy thm constructors rty qty =
+fun build_repabs_term lthy thm consts rty qty =
 let
 val rty = Logic.varifyT rty;
 val qty = Logic.varifyT qty;
 fun mk_abs tm =
 fun mk_repabs tm =
 let
 val ty = fastype_of tm
 in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end
-fun is_constructor (Const (x, _)) = member (op =) constructors x
+fun is_lifted_const (Const (x, _)) = member (op =) consts x
-| is_constructor _ = false;
+| is_lifted_const _ = false;
 fun build_aux lthy tm =
 case tm of
 Abs (a as (_, vty, _)) =>
-let
-val (vs, t) = Term.dest_abs a;
-val v = Free(vs, vty);
-val t' = lambda v (build_aux lthy t)
-in
-if (not (needs_lift rty (fastype_of tm))) then t'
-else mk_repabs (
-if not (needs_lift rty vty) then t'
-else
 let
-val v' = mk_repabs v;
+val (vs, t) = Term.dest_abs a;
-val t1 = Envir.beta_norm (t' $ v')
+val v = Free(vs, vty);
+val t' = lambda v (build_aux lthy t)
 in
-lambda v t1
+if (not (needs_lift rty (fastype_of tm))) then t'
+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 *)
+val t1 = Envir.beta_norm (t' $ v')
+in
+lambda v t1
+end)
 end
-)
+| x =>
-end
+case Term.strip_comb tm of
-| x =>
+(Const(@{const_name Respects}, _), _) => tm
-let
+| (opp, tms0) =>
-val (opp, tms0) = Term.strip_comb tm
+let
 val tms = map (build_aux lthy) tms0
 val ty = fastype_of tm
 in
-if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
+if (is_lifted_const opp andalso needs_lift rty ty) then
-then (list_comb (opp, (hd tms0) :: (tl tms)))
+mk_repabs (list_comb (opp, tms))
-else if (is_constructor opp andalso needs_lift rty ty) then
+else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
-mk_repabs (list_comb (opp,tms))
+mk_repabs (list_comb (opp, tms))
-else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
+else if tms = [] then opp
-mk_repabs(list_comb(opp,tms))
+else list_comb(opp, tms)
-else if tms = [] then opp
+end
-else list_comb(opp, tms)
-end
 in
 repeat_eqsubst_prop lthy @{thms id_def_sym}
 (build_aux lthy (Thm.prop_of thm))
 end
 *}
 fun quotient_tac quot_thm =
 REPEAT_ALL_NEW (FIRST' [
 rtac @{thm FUN_QUOTIENT},
 rtac quot_thm,
 rtac @{thm IDENTITY_QUOTIENT},
-(fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN rtac @{thm IDENTITY_QUOTIENT} i)
+(
+fn i => CHANGED (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I}) i) THEN
+rtac @{thm IDENTITY_QUOTIENT} i
+)
 ])
 *}
 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
 *}
 ML {*
 fun WEAK_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})
-| (_ $ (_ $ (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
 *}
 end
 handle _ => no_tac)
 *}
 ML {*
-val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
 let
-val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl
+val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
+(Const (@{const_name Ball}, _) $ _)) = term_of concl
 in
 ((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
 handle _ => no_tac
 )
 *}
 ML {*
-val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
 let
-val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl
+val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
+(Const (@{const_name Bex}, _) $ _)) = term_of concl
 in
 ((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
 *}
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
 (FIRST' [
-(*    rtac @{thm FUN_QUOTIENT},
-rtac quot_thm,
-rtac @{thm IDENTITY_QUOTIENT},*)
 rtac trans_thm,
 LAMBDA_RES_TAC ctxt,
-res_forall_rsp_tac ctxt,
+ball_rsp_tac ctxt,
-res_exists_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])),
 (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i))
 ])
 *}
 ML {*
-fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =
 let
-val rt = build_repabs_term lthy thm constructors rty qty;
+val rt = build_repabs_term lthy thm consts rty qty;
 val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
 in
 |> repeat_eqsubst_thm lthy @{thms FUN_MAP_I id_apply prod_fun_id map_id}
 *}
 text {* expects atomized definition *}
 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;
 val g = simp_ids lthy f
 in
 (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
 end
 handle _ => [simp_ids lthy thm]
 *}
 ML {*
 fun add_lower_defs lthy def =
 let
 map Thm.varifyT defs_all
 end
 *}
 ML {*
 fun findabs_all rty tm =
 case tm of
 Abs(_, T, b) =>
 let
 val b' = subst_bound ((Free ("x", T)), b);
 val tys = findabs_all rty b'
 val ty = fastype_of tm
 in if needs_lift rty ty then (ty :: tys) else tys
 end
 | 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))
 | (f $ a) => (findaps_all rty f @ findaps_all rty a)
-| Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else [])
+| Free (_, (T as (Type ("fun", (_ :: _))))) =>
-| _ => [];
+(if needs_lift rty T then [T] else [])
-fun findaps rty tm = distinct (op =) (findaps_all rty tm)
+| _ => [];
+fun findaps rty tm = distinct (op =) (findaps_all rty tm)
 *}
 ML {*
 fun make_simp_prs_thm lthy quot_thm thm typ =
 let
 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
 end
 *}
 ML {*
 fun findallex_all rty qty tm =
 case tm of
 Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
 let
 val (tya, tye) = findallex_all rty qty s
 in if needs_lift rty T then
 ((T :: tya), tye)
 else (tya, tye) end
 | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>
 let
 val (tya, tye) = findallex_all rty qty s
 in if needs_lift rty T then
 (tya, (T :: tye))
 else (tya, tye) end
 | Abs(_, T, b) =>
 findallex_all rty qty (subst_bound ((Free ("x", T)), b))
 | f $ a =>
 let
 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);
 val (au, eu) = (distinct (op =) ad, distinct (op =) ed);
 val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)
 in
 (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)
 end
 *}
 ML {*
 fun make_allex_prs_thm lthy quot_thm thm typ =
 let
 val tac =
 (compose_tac (false, lpi, 1)) THEN_ALL_NEW
 (quotient_tac quot_thm);
 val gc = Drule.strip_imp_concl (cprop_of lpi);
 val t = Goal.prove_internal [] gc (fn _ => tac 1)
-val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t;
+val t_noid = MetaSimplifier.rewrite_rule
+[@{thm eq_reflection} OF @{thms id_apply}] t;
 val t_sym = @{thm "HOL.sym"} OF [t_noid];
 val t_eq = @{thm "eq_reflection"} OF [t_sym]
 in
 t_eq
 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_new repF (rty, qty) lthy ty) $ tm) end;
 fun mk_abs tm =
 let
 val ty = fastype_of tm
 in Syntax.check_term lthy ((get_fun_new 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 = (Simplifier.context lthy' 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 matches (ty1, ty2) =
 Type.raw_instance (ty1, Logic.varifyT ty2);
 end
 *}
 ML {*
 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
 let
 val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
 val (_, lthy2) = note (name, lifted_thm) lthy;
 in
 lthy2
-end;
+end
 *}
 end

changeset 301	40bb0c4718a6
parent 300	c6a9b4e4d548
child 302	a840c232e04e