theory QuotMainNew
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 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
| (_ $ _, _ $ _) =>
let
val rty = fastype_of rtrm
val qty = fastype_of qtrm
val (rhead, rargs) = strip_comb rtrm
val (qhead, qargs) = strip_comb qtrm
val rargs' = map insertion_aux (rargs ~~ qargs)
val rhead' = insertion_aux (rhead, qhead)
val result = list_comb (rhead', rargs')
in
if rty = qty
then result
else mk_qid (rty, qty, result)
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'
then rtrm
else mk_qid (ty, ty', rtrm)
| (_, _) => raise (LIFT_MATCH "insertion")
*}
ML {*
fun insertion ctxt rtrm qtrm =
Syntax.check_term ctxt (insertion_aux (rtrm, qtrm))
*}
fun
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
where
"intrel (x, y) (u, v) = (x + v = u + y)"
quotient my_int = "nat \<times> nat" / intrel
apply(unfold EQUIV_def)
apply(auto simp add: mem_def expand_fun_eq)
done
fun
my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
where
"my_plus (x, y) (u, v) = (x + u, y + v)"
quotient_def
PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
where
"PLUS \<equiv> my_plus"
thm PLUS_def
ML {* MetaSimplifier.rewrite_term *}
ML {*
let
val rtrm = @{term "\<forall>a b. my_plus a b \<approx> my_plus b a"}
val qtrm = @{term "\<forall>a b. PLUS a b = PLUS b a"}
val ctxt = @{context}
in
insertion ctxt rtrm qtrm
(*|> Drule.term_rule @{theory} (MetaSimplifier.rewrite_rule [@{thm "qid_def"}])*)
|> Syntax.string_of_term ctxt
|> writeln
end
*}
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
*)
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 {* 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, rtac rthm']
end) lthy
*}
end