--- a/QuotMain.thy Fri Dec 04 15:25:51 2009 +0100
+++ b/QuotMain.thy Fri Dec 04 15:41:09 2009 +0100
@@ -143,7 +143,7 @@
declare [[map list = (map, LIST_REL)]]
declare [[map * = (prod_fun, prod_rel)]]
-declare [[map "fun" = (fun_map, FUN_REL)]]
+declare [[map "fun" = (fun_map, fun_rel)]]
lemmas [quotient_thm] =
FUN_Quotient LIST_Quotient
@@ -540,7 +540,7 @@
in
case redex of
(ogl as ((Const (@{const_name "Ball"}, _)) $
- ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
+ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
(let
val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
@@ -571,7 +571,7 @@
in
case redex of
(ogl as ((Const (@{const_name "Bex"}, _)) $
- ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
+ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
(let
val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
@@ -728,37 +728,11 @@
resolve_tac (quotient_rules_get ctxt)])
*}
-lemma FUN_REL_I:
+lemma fun_rel_id:
assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
shows "(R1 ===> R2) f g"
using a by simp
-ML {*
-val lambda_rsp_tac =
- SUBGOAL (fn (goal, i) =>
- case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
- (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i
- | _ => no_tac)
-*}
-
-ML {*
-val ball_rsp_tac =
- SUBGOAL (fn (goal, i) =>
- case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
- (_ $ (Const (@{const_name Ball}, _) $ _)
- $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i
- |_ => no_tac)
-*}
-
-ML {*
-val bex_rsp_tac =
- SUBGOAL (fn (goal, i) =>
- case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
- (_ $ (Const (@{const_name Bex}, _) $ _)
- $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i
- | _ => no_tac)
-*}
-
definition
"QUOT_TRUE x \<equiv> True"
@@ -936,28 +910,28 @@
fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
(case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
- ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
- => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+ ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+ => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
(* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
| (Const (@{const_name "op ="},_) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
(* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
-| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+ => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
(* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
| Const (@{const_name "op ="},_) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
(* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
-| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+ => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
| Const (@{const_name "op ="},_) $ _ $ _ =>
(* reflexivity of operators arising from Cong_tac *)
rtac @{thm refl} ORELSE'
--- a/QuotMainNew.thy Fri Dec 04 15:25:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,723 +0,0 @@
-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
-
-