--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotMainNew.thy Sun Nov 29 19:48:55 2009 +0100
@@ -0,0 +1,1273 @@
+theory QuotMain
+imports QuotScript QuotList Prove
+uses ("quotient_info.ML")
+ ("quotient.ML")
+ ("quotient_def.ML")
+begin
+
+locale QUOT_TYPE =
+ fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ assumes equiv: "EQUIV R"
+ and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+begin
+
+definition
+ ABS::"'a \<Rightarrow> 'b"
+where
+ "ABS x \<equiv> Abs (R x)"
+
+definition
+ REP::"'b \<Rightarrow> 'a"
+where
+ "REP a = Eps (Rep a)"
+
+lemma lem9:
+ shows "R (Eps (R x)) = R x"
+proof -
+ have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
+ then have "R x (Eps (R x))" by (rule someI)
+ then show "R (Eps (R x)) = R x"
+ using equiv unfolding EQUIV_def by simp
+qed
+
+theorem thm10:
+ shows "ABS (REP a) \<equiv> a"
+ apply (rule eq_reflection)
+ unfolding ABS_def REP_def
+proof -
+ from rep_prop
+ obtain x where eq: "Rep a = R x" by auto
+ have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+ also have "\<dots> = Abs (R x)" using lem9 by simp
+ also have "\<dots> = Abs (Rep a)" using eq by simp
+ also have "\<dots> = a" using rep_inverse by simp
+ finally
+ show "Abs (R (Eps (Rep a))) = a" by simp
+qed
+
+lemma REP_refl:
+ shows "R (REP a) (REP a)"
+unfolding REP_def
+by (simp add: equiv[simplified EQUIV_def])
+
+lemma lem7:
+ shows "(R x = R y) = (Abs (R x) = Abs (R y))"
+apply(rule iffI)
+apply(simp)
+apply(drule rep_inject[THEN iffD2])
+apply(simp add: abs_inverse)
+done
+
+theorem thm11:
+ shows "R r r' = (ABS r = ABS r')"
+unfolding ABS_def
+by (simp only: equiv[simplified EQUIV_def] lem7)
+
+
+lemma REP_ABS_rsp:
+ shows "R f (REP (ABS g)) = R f g"
+ and "R (REP (ABS g)) f = R g f"
+by (simp_all add: thm10 thm11)
+
+lemma QUOTIENT:
+ "QUOTIENT R ABS REP"
+apply(unfold QUOTIENT_def)
+apply(simp add: thm10)
+apply(simp add: REP_refl)
+apply(subst thm11[symmetric])
+apply(simp add: equiv[simplified EQUIV_def])
+done
+
+lemma R_trans:
+ assumes ab: "R a b"
+ and bc: "R b c"
+ shows "R a c"
+proof -
+ have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ moreover have ab: "R a b" by fact
+ moreover have bc: "R b c" by fact
+ ultimately show "R a c" unfolding TRANS_def by blast
+qed
+
+lemma R_sym:
+ assumes ab: "R a b"
+ shows "R b a"
+proof -
+ have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ then show "R b a" using ab unfolding SYM_def by blast
+qed
+
+lemma R_trans2:
+ assumes ac: "R a c"
+ and bd: "R b d"
+ shows "R a b = R c d"
+using ac bd
+by (blast intro: R_trans R_sym)
+
+lemma REPS_same:
+ shows "R (REP a) (REP b) \<equiv> (a = b)"
+proof -
+ have "R (REP a) (REP b) = (a = b)"
+ proof
+ assume as: "R (REP a) (REP b)"
+ from rep_prop
+ obtain x y
+ where eqs: "Rep a = R x" "Rep b = R y" by blast
+ from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
+ then have "R x (Eps (R y))" using lem9 by simp
+ then have "R (Eps (R y)) x" using R_sym by blast
+ then have "R y x" using lem9 by simp
+ then have "R x y" using R_sym by blast
+ then have "ABS x = ABS y" using thm11 by simp
+ then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
+ then show "a = b" using rep_inverse by simp
+ next
+ assume ab: "a = b"
+ have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
+ then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
+ qed
+ then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
+qed
+
+end
+
+lemma equiv_trans2:
+ assumes e: "EQUIV R"
+ and ac: "R a c"
+ and bd: "R b d"
+ shows "R a b = R c d"
+using ac bd e
+unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def
+by (blast)
+
+section {* type definition for the quotient type *}
+
+(* the auxiliary data for the quotient types *)
+use "quotient_info.ML"
+
+declare [[map list = (map, LIST_REL)]]
+declare [[map * = (prod_fun, prod_rel)]]
+declare [[map "fun" = (fun_map, FUN_REL)]]
+
+ML {* maps_lookup @{theory} "List.list" *}
+ML {* maps_lookup @{theory} "*" *}
+ML {* maps_lookup @{theory} "fun" *}
+
+
+(* definition of the quotient types *)
+(* FIXME: should be called quotient_typ.ML *)
+use "quotient.ML"
+
+
+(* lifting of constants *)
+use "quotient_def.ML"
+
+(* TODO: Consider defining it with an "if"; sth like:
+ Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+*)
+definition
+ Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+ "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+
+section {* ATOMIZE *}
+
+lemma atomize_eqv[atomize]:
+ shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+proof
+ assume "A \<equiv> B"
+ then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+ assume *: "Trueprop A \<equiv> Trueprop B"
+ have "A = B"
+ proof (cases A)
+ case True
+ have "A" by fact
+ then show "A = B" using * by simp
+ next
+ case False
+ have "\<not>A" by fact
+ then show "A = B" using * by auto
+ qed
+ then show "A \<equiv> B" by (rule eq_reflection)
+qed
+
+ML {*
+fun atomize_thm thm =
+let
+ val thm' = Thm.freezeT (forall_intr_vars thm)
+ val thm'' = ObjectLogic.atomize (cprop_of thm')
+in
+ @{thm equal_elim_rule1} OF [thm'', thm']
+end
+*}
+
+section {* infrastructure about id *}
+
+lemma prod_fun_id: "prod_fun id id \<equiv> id"
+ by (rule eq_reflection) (simp add: prod_fun_def)
+
+lemma map_id: "map id \<equiv> id"
+ apply (rule eq_reflection)
+ apply (rule ext)
+ apply (rule_tac list="x" in list.induct)
+ apply (simp_all)
+ done
+
+lemmas id_simps =
+ FUN_MAP_I[THEN eq_reflection]
+ id_apply[THEN eq_reflection]
+ id_def[THEN eq_reflection,symmetric]
+ prod_fun_id map_id
+
+ML {*
+fun simp_ids thm =
+ MetaSimplifier.rewrite_rule @{thms id_simps} thm
+*}
+
+section {* Debugging infrastructure for testing tactics *}
+
+ML {*
+fun my_print_tac ctxt s i thm =
+let
+ val prem_str = nth (prems_of thm) (i - 1)
+ |> Syntax.string_of_term ctxt
+ handle Subscript => "no subgoal"
+ val _ = tracing (s ^ "\n" ^ prem_str)
+in
+ Seq.single thm
+end *}
+
+
+ML {*
+fun DT ctxt s tac i thm =
+let
+ val before_goal = nth (prems_of thm) (i - 1)
+ |> Syntax.string_of_term ctxt
+ val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
+ |> cat_lines
+in
+ EVERY [tac i, my_print_tac ctxt before_msg i] thm
+end
+
+fun NDT ctxt s tac thm = tac thm
+*}
+
+
+section {* Infrastructure about definitions *}
+
+(* Does the same as 'subst' in a given theorem *)
+ML {*
+fun eqsubst_thm ctxt thms thm =
+ let
+ val goalstate = Goal.init (Thm.cprop_of thm)
+ val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+ NONE => error "eqsubst_thm"
+ | SOME th => cprem_of th 1
+ val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+ val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
+ val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
+ val rt = Goal.prove_internal [] cgoal (fn _ => tac);
+ in
+ @{thm equal_elim_rule1} OF [rt, thm]
+ end
+*}
+
+(* 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;
+ val g = simp_ids f
+ in
+ (simp_ids thm) :: (add_lower_defs_aux lthy g)
+ end
+ handle _ => [simp_ids thm]
+*}
+
+ML {*
+fun add_lower_defs lthy def =
+ let
+ val def_pre_sym = symmetric def
+ val def_atom = atomize_thm def_pre_sym
+ val defs_all = add_lower_defs_aux lthy def_atom
+ in
+ map Thm.varifyT defs_all
+ end
+*}
+
+section {* Infrastructure for collecting theorems for starting the lifting *}
+
+ML {*
+fun lookup_quot_data lthy qty =
+ let
+ val qty_name = fst (dest_Type qty)
+ val SOME quotdata = quotdata_lookup lthy qty_name
+ (* cu: Changed the lookup\<dots>not sure whether this works *)
+ (* 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 = @{thm EQUIV_REFL} OF [rel_eqv]
+ in
+ (rty, rel, rel_refl, rel_eqv)
+ end
+*}
+
+ML {*
+fun lookup_quot_thms lthy qty_name =
+ let
+ val thy = ProofContext.theory_of lthy;
+ val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
+ val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
+ val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
+ val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
+ in
+ (trans2, reps_same, absrep, quot)
+ end
+*}
+
+ML {*
+fun lookup_quot_consts defs =
+ let
+ fun dest_term (a $ b) = (a, b);
+ val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
+ in
+ map (fst o dest_Const o snd o dest_term) def_terms
+ end
+*}
+
+section {* Infrastructure for special quotient identity *}
+
+definition
+ "qid TYPE('a) TYPE('b) x \<equiv> x"
+
+ML {*
+fun get_typ_aux (Type ("itself", [T])) = T
+fun get_typ (Const ("TYPE", T)) = get_typ_aux T
+fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) =
+ (get_typ ty1, get_typ ty2)
+
+fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true
+ | is_qid _ = false
+
+
+fun mk_itself ty = Type ("itself", [ty])
+fun mk_TYPE ty = Const ("TYPE", mk_itself ty)
+fun mk_qid (rty, qty, trm) =
+ Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT)
+ $ mk_TYPE rty $ mk_TYPE qty $ trm
+*}
+
+ML {*
+fun insertion_aux rtrm qtrm =
+ case (rtrm, qtrm) of
+ (Abs (x, ty, t), Abs (x', ty', t')) =>
+ let
+ val (y, s) = Term.dest_abs (x, ty, t)
+ val (_, s') = Term.dest_abs (x', ty', t')
+ val yvar = Free (y, ty)
+ val result = Term.lambda_name (y, yvar) (insertion_aux s s')
+ in
+ if ty = ty'
+ then result
+ else mk_qid (ty, ty', result)
+ end
+ | (t1 $ t2, t1' $ t2') =>
+ let
+ val rty = fastype_of rtrm
+ val qty = fastype_of qtrm
+ val subtrm1 = insertion_aux t1 t1'
+ val subtrm2 = insertion_aux t2 t2'
+ in
+ if rty = qty
+ then subtrm1 $ subtrm2
+ else mk_qid (rty, qty, subtrm1 $ subtrm2)
+ end
+ | (Free (_, ty), Free (_, ty')) =>
+ if ty = ty'
+ then rtrm
+ else mk_qid (ty, ty', rtrm)
+ | (Const (s, ty), Const (s', ty')) =>
+ if s = s' andalso ty = ty'
+ then rtrm
+ else mk_qid (ty, ty', rtrm)
+ | (_, _) => raise (LIFT_MATCH "insertion")
+*}
+
+section {* Regularization *}
+
+(*
+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
+
+ the relation R is given by the rty and qty;
+
+ - abstractions over a type that needs lifting are replaced
+ by bounded abstractions:
+ \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
+
+ - equalities over the type being lifted are replaced by
+ corresponding relations:
+ A = B \<Longrightarrow> A \<approx> B
+
+ 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
+ if rty = qty
+ then HOLogic.eq_const rty
+ else
+ case (rty, qty) of
+ (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then let
+ val SOME map_info = maps_lookup thy s
+ val args = map (mk_resp_arg lthy) (tys ~~ tys')
+ in
+ list_comb (Const (#relfun map_info, dummyT), args)
+ end
+ else let
+ val SOME qinfo = quotdata_lookup_thy thy s'
+ (* FIXME: check in this case that the rty and qty *)
+ (* FIXME: correspond to each other *)
+ val (s, _) = dest_Const (#rel qinfo)
+ (* FIXME: the relation should only be the string *)
+ (* FIXME: and the type needs to be calculated as below; *)
+ (* FIXME: maybe one should actually have a term *)
+ (* FIXME: and one needs to force it to have this type *)
+ in
+ Const (s, rty --> rty --> @{typ bool})
+ end
+ | _ => HOLogic.eq_const dummyT
+ (* FIXME: check that the types correspond to each other? *)
+end
+*}
+
+ML {*
+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 *)
+(* variables do not have to be treated specially *)
+
+fun apply_subt f trm =
+ case trm of
+ (Abs (x, T, t)) => Abs (x, T, f t)
+ | _ => f trm
+
+(* the major type of All and Ex quantifiers *)
+fun qnt_typ ty = domain_type (domain_type ty)
+*}
+
+ML {*
+(* produces a regularized version of trm *)
+(* - the result is still not completely typed *)
+(* - does not need any special treatment of *)
+(* bound variables *)
+
+fun regularize_trm lthy trm =
+ case trm of
+ (Const (@{const_name "qid"},_) $ rty' $ qty' $ Abs (x, ty, t)) =>
+ let
+ val rty = get_typ rty'
+ val qty = get_typ qty'
+ val subtrm = regularize_trm lthy t
+ in
+ mk_qid (rty, qty, mk_babs $ (mk_resp $ mk_resp_arg lthy (rty, qty)) $ subtrm)
+ end
+ | (Const (@{const_name "qid"},_) $ rty' $ qty' $ (Const (@{const_name "All"}, ty) $ t)) =>
+ let
+ val subtrm = apply_subt (regularize_trm lthy) t
+ in
+ if ty = ty'
+ then Const (@{const_name "All"}, ty) $ subtrm
+ else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+ end
+ | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+ let
+ val subtrm = apply_subt (regularize_trm lthy) t t'
+ in
+ if ty = ty'
+ then Const (@{const_name "Ex"}, ty) $ subtrm
+ else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+ end
+ (* FIXME: Should = only be replaced, when fully applied? *)
+ (* Then there must be a 2nd argument *)
+ | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
+ let
+ val subtrm = regularize_trm lthy t t'
+ in
+ if ty = ty'
+ then Const (@{const_name "op ="}, ty) $ subtrm
+ else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
+ end
+ | (t1 $ t2, t1' $ t2') =>
+ (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
+ | (Free (x, ty), Free (x', ty')) =>
+ (* this case cannot arrise as we start with two fully atomized terms *)
+ raise (LIFT_MATCH "regularize (frees)")
+ | (Bound i, Bound i') =>
+ if i = i'
+ then rtrm
+ else raise (LIFT_MATCH "regularize (bounds)")
+ | (Const (s, ty), Const (s', ty')) =>
+ if s = s' andalso ty = ty'
+ then rtrm
+ else rtrm (* FIXME: check correspondence according to definitions *)
+ | (rt, qt) =>
+ raise (LIFT_MATCH "regularize (default)")
+*}
+
+(*
+FIXME / TODO: needs to be adapted
+
+To prove that the raw theorem implies the regularised one,
+we try in order:
+
+ - Reflexivity of the relation
+ - Assumption
+ - Elimnating quantifiers on both sides of toplevel implication
+ - Simplifying implications on both sides of toplevel implication
+ - Ball (Respects ?E) ?P = All ?P
+ - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+
+*)
+
+(* FIXME: they should be in in the new Isabelle *)
+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
+
+(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
+ML {*
+fun equiv_tac rel_eqvs =
+ REPEAT_ALL_NEW (FIRST'
+ [resolve_tac rel_eqvs,
+ rtac @{thm IDENTITY_EQUIV},
+ rtac @{thm LIST_EQUIV}])
+*}
+
+ML {*
+fun ball_reg_eqv_simproc rel_eqvs ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val thy = ProofContext.theory_of ctxt
+ in
+ case redex of
+ (ogl as ((Const (@{const_name "Ball"}, _)) $
+ ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
+ (let
+ val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+ val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
+ val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
+ val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
+(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
+ in
+ SOME thm
+ end
+ handle _ => NONE
+ )
+ | _ => NONE
+ end
+*}
+
+ML {*
+fun bex_reg_eqv_simproc rel_eqvs ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val thy = ProofContext.theory_of ctxt
+ in
+ case redex of
+ (ogl as ((Const (@{const_name "Bex"}, _)) $
+ ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
+ (let
+ val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
+ val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
+ val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
+ val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
+(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
+ in
+ SOME thm
+ end
+ handle _ => NONE
+ )
+ | _ => NONE
+ 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 ball_reg_eqv_range_simproc rel_eqvs ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val thy = ProofContext.theory_of ctxt
+ in
+ case redex of
+ (ogl as ((Const (@{const_name "Ball"}, _)) $
+ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
+ (let
+ val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
+ val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
+ val _ = tracing (Syntax.string_of_term ctxt glc);
+ val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
+ val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
+ val R1c = cterm_of thy R1;
+ val thmi = Drule.instantiate' [] [SOME R1c] thm;
+(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
+ val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
+ val _ = tracing "AAA";
+ val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
+ val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
+ in
+ SOME thm2
+ end
+ handle _ => NONE
+
+ )
+ | _ => NONE
+ end
+*}
+
+ML {*
+fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
+ let
+ val ctxt = Simplifier.the_context ss
+ val thy = ProofContext.theory_of ctxt
+ in
+ case redex of
+ (ogl as ((Const (@{const_name "Bex"}, _)) $
+ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
+ (let
+ val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
+ val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
+ val _ = tracing (Syntax.string_of_term ctxt glc);
+ val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
+ val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
+ val R1c = cterm_of thy R1;
+ val thmi = Drule.instantiate' [] [SOME R1c] thm;
+(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
+ val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
+ val _ = tracing "AAA";
+ val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
+ val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
+ in
+ SOME thm2
+ end
+ handle _ => NONE
+
+ )
+ | _ => NONE
+ end
+*}
+
+lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
+by (simp add: EQUIV_REFL)
+
+ML {*
+fun regularize_tac ctxt rel_eqvs =
+ let
+ val pat1 = [@{term "Ball (Respects R) P"}];
+ val pat2 = [@{term "Bex (Respects R) P"}];
+ val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+ val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
+ val thy = ProofContext.theory_of ctxt
+ val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))
+ val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs))
+ val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))
+ val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))
+ val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
+ (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *)
+ val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs
+ in
+ ObjectLogic.full_atomize_tac THEN'
+ simp_tac simp_ctxt THEN'
+ REPEAT_ALL_NEW (FIRST' [
+ rtac @{thm ball_reg_right},
+ rtac @{thm bex_reg_left},
+ resolve_tac (Inductive.get_monos ctxt),
+ rtac @{thm ball_all_comm},
+ rtac @{thm bex_ex_comm},
+ resolve_tac eq_eqvs,
+ simp_tac simp_ctxt
+ ])
+ end
+*}
+
+section {* Injections of REP and ABSes *}
+
+(*
+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. 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.
+*)
+
+ML {*
+fun mk_repabs lthy (T, T') trm =
+ Quotient_Def.get_fun repF lthy (T, T')
+ $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
+*}
+
+ML {*
+(* bound variables need to be treated properly, *)
+(* as the type of subterms need to be calculated *)
+
+fun inj_repabs_trm lthy (rtrm, qtrm) =
+let
+ val rty = fastype_of rtrm
+ val qty = fastype_of qtrm
+in
+ case (rtrm, qtrm) of
+ (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+ Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+ | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+ Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+ | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
+ Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+ | (Abs (x, T, t), Abs (x', T', t')) =>
+ let
+ val (y, s) = Term.dest_abs (x, T, t)
+ val (_, s') = Term.dest_abs (x', T', t')
+ val yvar = Free (y, T)
+ val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
+ in
+ if rty = qty
+ then result
+ else mk_repabs lthy (rty, qty) result
+ end
+ | _ =>
+ (* FIXME / TODO: this is a case that needs to be looked at *)
+ (* - variables get a rep-abs insde and outside an application *)
+ (* - constants only get a rep-abs on the outside of the application *)
+ (* - applications get a rep-abs insde and outside an application *)
+ let
+ val (rhead, rargs) = strip_comb rtrm
+ val (qhead, qargs) = strip_comb qtrm
+ val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
+ in
+ if rty = qty
+ then
+ case (rhead, qhead) of
+ (Free (_, T), Free (_, T')) =>
+ if T = T' then list_comb (rhead, rargs')
+ else list_comb (mk_repabs lthy (T, T') rhead, rargs')
+ | _ => list_comb (rhead, rargs')
+ else
+ case (rhead, qhead, length rargs') of
+ (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead
+ | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead
+ | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs'))
+ | (Free (x, T), Free (x', T'), _) =>
+ mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
+ | (Abs _, Abs _, _ ) =>
+ mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs'))
+ | _ => raise (LIFT_MATCH "injection")
+ end
+end
+*}
+
+section {* RepAbs Injection Tactic *}
+
+ML {*
+fun stripped_term_of ct =
+ ct |> term_of |> HOLogic.dest_Trueprop
+*}
+
+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 quotient_tac quot_thms =
+ REPEAT_ALL_NEW (FIRST'
+ [rtac @{thm FUN_QUOTIENT},
+ resolve_tac quot_thms,
+ rtac @{thm IDENTITY_QUOTIENT},
+ (* For functional identity quotients, (op = ---> op =) *)
+ (* TODO: think about the other way around, if we need to shorten the relation *)
+ CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])
+*}
+
+lemma FUN_REL_I:
+ assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ shows "(R1 ===> R2) f g"
+using a by (simp add: FUN_REL.simps)
+
+ML {*
+val lambda_res_tac =
+ Subgoal.FOCUS (fn {concl, ...} =>
+ case (stripped_term_of concl) of
+ (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1
+ | _ => no_tac)
+*}
+
+ML {*
+val weak_lambda_res_tac =
+ Subgoal.FOCUS (fn {concl, ...} =>
+ case (stripped_term_of concl) of
+ (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1
+ | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1
+ | _ => no_tac)
+*}
+
+ML {*
+val ball_rsp_tac =
+ Subgoal.FOCUS (fn {concl, ...} =>
+ case (stripped_term_of concl) of
+ (_ $ (Const (@{const_name Ball}, _) $ _)
+ $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1
+ |_ => no_tac)
+*}
+
+ML {*
+val bex_rsp_tac =
+ Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+ case (stripped_term_of concl) of
+ (_ $ (Const (@{const_name Bex}, _) $ _)
+ $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1
+ | _ => no_tac)
+*}
+
+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, ...} =>
+ case (stripped_term_of concl) of
+ (_ $ (f $ _) $ (_ $ _)) =>
+ let
+ val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+ val insts = Thm.match (pat, concl)
+ in
+ if needs_lift rty (fastype_of f)
+ then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+ else no_tac
+ end
+ | _ => no_tac)
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+(*
+To prove that the regularised theorem implies the abs/rep injected,
+we 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
+ A) reflexivity of the relation
+ B) assumption
+ (Lambdas under respects may have left us some assumptions)
+ C) proving obvious higher order equalities by simplifying fun_rel
+ (not sure if it is still needed?)
+ D) unfolding lambda on one side
+ E) simplifying (= ===> =) for simpler respectfulness
+
+*)
+
+ML {*
+fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
+ (FIRST' [
+ (* "cong" rule of the of the relation / transitivity*)
+ (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
+ NDT ctxt "1" (resolve_tac trans2),
+
+ (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+ NDT ctxt "2" (lambda_res_tac ctxt),
+
+ (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+
+ (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
+ NDT ctxt "4" (ball_rsp_tac ctxt),
+
+ (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+
+ (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
+ NDT ctxt "6" (bex_rsp_tac ctxt),
+
+ (* respectfulness of constants *)
+ NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
+
+ (* reflexivity of operators arising from Cong_tac *)
+ NDT ctxt "8" (rtac @{thm refl}),
+
+ (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
+ (* observe ---> *)
+ NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
+ THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
+
+ (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *)
+ NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
+ (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
+
+ (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
+ (* merge with previous tactic *)
+ NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+
+ (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+ NDT ctxt "C" (rtac @{thm ext}),
+
+ (* reflexivity of the basic relations *)
+ (* R \<dots> \<dots> *)
+ NDT ctxt "D" (resolve_tac rel_refl),
+
+ (* resolving with R x y assumptions *)
+ NDT ctxt "E" (atac),
+
+ (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*)
+
+ (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+ (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+ (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*)
+
+ (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
+ (* global simplification *)
+ NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+*}
+
+ML {*
+fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
+ REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)
+*}
+
+
+section {* Cleaning of the theorem *}
+
+ML {*
+fun applic_prs lthy absrep (rty, qty) =
+ let
+ fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
+ fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
+ val (raty, rgty) = Term.strip_type rty;
+ val (qaty, qgty) = Term.strip_type qty;
+ val vs = map (fn _ => "x") qaty;
+ val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+ val f = Free (fname, qaty ---> qgty);
+ val args = map Free (vfs ~~ qaty);
+ val rhs = list_comb(f, args);
+ val largs = map2 mk_rep (raty ~~ qaty) args;
+ val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
+ val llhs = Syntax.check_term lthy lhs;
+ val eq = Logic.mk_equals (llhs, rhs);
+ val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+ val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);
+ val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+ val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
+ in
+ singleton (ProofContext.export lthy' lthy) t_id
+ end
+*}
+
+ML {*
+fun find_aps_all rtm qtm =
+ case (rtm, qtm) of
+ (Abs(_, T1, s1), Abs(_, T2, s2)) =>
+ find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
+ | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
+ let
+ val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+ in
+ if T1 = T2 then sub else (T1, T2) :: sub
+ end
+ | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
+ | _ => [];
+
+fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
+*}
+
+ML {*
+fun allex_prs_tac lthy quot =
+ (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
+ THEN' (quotient_tac quot)
+*}
+
+(* Rewrites the term with LAMBDA_PRS thm.
+
+Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
+ with: f
+
+It proves the QUOTIENT assumptions by calling quotient_tac
+ *)
+ML {*
+fun make_inst lhs t =
+ let
+ val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ val _ $ (Abs (_, _, g)) = t;
+ fun mk_abs i t =
+ if incr_boundvars i u aconv t then Bound i
+ else (case t of
+ t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+ | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')
+ | Bound j => if i = j then error "make_inst" else t
+ | _ => t);
+ in (f, Abs ("x", T, mk_abs 0 g)) end;
+
+fun lambda_prs_conv1 ctxt quot_thms 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_thms);
+ 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 @{thms id_simps} te
+ val tl = Thm.lhs_of ts;
+ val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
+ val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
+(* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+ in
+ Conv.rewr_conv ti ctrm
+ end
+*}
+
+(* 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 aps =
+ let
+ val lower = flat (map (add_lower_defs lthy) defs)
+ val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
+ val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+ val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
+ val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
+ val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower)
+ val aps_thms = map (applic_prs lthy absrep) aps
+ in
+ EVERY' [lambda_prs_tac lthy quot,
+ TRY o simp_tac simp_ctxt,
+ TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
+ TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
+ TRY o rtac refl]
+ end
+*}
+
+section {* Genralisation of free variables in a goal *}
+
+ML {*
+fun inst_spec ctrm =
+ Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
+
+fun inst_spec_tac ctrms =
+ EVERY' (map (dtac o inst_spec) ctrms)
+
+fun all_list xs trm =
+ fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
+
+fun apply_under_Trueprop f =
+ HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
+
+fun gen_frees_tac ctxt =
+ SUBGOAL (fn (concl, i) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val vrs = Term.add_frees concl []
+ val cvrs = map (cterm_of thy o Free) vrs
+ val concl' = apply_under_Trueprop (all_list vrs) concl
+ val goal = Logic.mk_implies (concl', concl)
+ val rule = Goal.prove ctxt [] [] goal
+ (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
+ in
+ rtac rule i
+ end)
+*}
+
+section {* General outline of the lifting procedure *}
+
+(* - A is the original raw theorem *)
+(* - B is the regularized theorem *)
+(* - C is the rep/abs injected version of B *)
+(* - D is the lifted theorem *)
+(* *)
+(* - b is the regularization step *)
+(* - c is the rep/abs injection step *)
+(* - d is the cleaning part *)
+
+lemma lifting_procedure:
+ assumes a: "A"
+ and b: "A \<Longrightarrow> B"
+ and c: "B = C"
+ and d: "C = D"
+ shows "D"
+ using a b c d
+ by simp
+
+ML {*
+fun lift_match_error ctxt fun_str rtrm qtrm =
+let
+ val rtrm_str = Syntax.string_of_term ctxt rtrm
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
+ val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str,
+ "and the lifted theorem\n", rtrm_str, "do not match"]
+in
+ error (space_implode " " msg)
+end
+*}
+
+ML {*
+fun procedure_inst ctxt rtrm qtrm =
+let
+ val thy = ProofContext.theory_of ctxt
+ val rtrm' = HOLogic.dest_Trueprop rtrm
+ val qtrm' = HOLogic.dest_Trueprop qtrm
+ val reg_goal =
+ Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
+ handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
+ val inj_goal =
+ Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
+ handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
+in
+ Drule.instantiate' []
+ [SOME (cterm_of thy rtrm'),
+ SOME (cterm_of thy reg_goal),
+ SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
+end
+*}
+
+(* Left for debugging *)
+ML {*
+fun procedure_tac lthy rthm =
+ ObjectLogic.full_atomize_tac
+ THEN' gen_frees_tac lthy
+ THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+ let
+ val rthm' = atomize_thm rthm
+ val rule = procedure_inst context (prop_of rthm') (term_of concl)
+ in
+ EVERY1 [rtac rule, rtac rthm']
+ end) lthy
+*}
+
+ML {*
+(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
+fun lift_tac lthy rthm rel_eqv rty quot defs =
+ ObjectLogic.full_atomize_tac
+ THEN' gen_frees_tac lthy
+ THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+ 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)
+ val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
+ val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
+ in
+ EVERY1
+ [rtac rule,
+ RANGE [rtac rthm',
+ regularize_tac lthy rel_eqv,
+ all_inj_repabs_tac lthy rty quot rel_refl trans2,
+ clean_tac lthy quot defs aps]]
+ end) lthy
+*}
+
+end
+
+