--- a/Quot/Examples/FSet.thy Wed Dec 16 14:28:48 2009 +0100
+++ b/Quot/Examples/FSet.thy Thu Dec 17 14:58:33 2009 +0100
@@ -359,7 +359,7 @@
apply(regularize)
apply(rule fun_rel_id_asm)
apply(subst babs_simp)
-apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
apply(rule fun_rel_id_asm)
apply(rule impI)
apply(rule mp[OF eq_imp_rel[OF fset_equivp]])
--- a/Quot/Examples/IntEx.thy Wed Dec 16 14:28:48 2009 +0100
+++ b/Quot/Examples/IntEx.thy Thu Dec 17 14:58:33 2009 +0100
@@ -135,13 +135,13 @@
done
lemma "PLUS a = PLUS a"
-apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
+apply(lifting_setup test2)
apply(rule impI)
apply(rule ballI)
apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
apply(simp only: in_respects)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(injection)
+apply(cleaning)
done
lemma test3: "my_plus = my_plus"
@@ -149,7 +149,7 @@
done
lemma "PLUS = PLUS"
-apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
+apply(lifting_setup test3)
apply(rule impI)
apply(rule plus_rsp)
apply(injection)
@@ -158,10 +158,7 @@
lemma "PLUS a b = PLUS b a"
-apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting plus_sym_pre)
done
lemma plus_assoc_pre:
@@ -173,10 +170,7 @@
done
lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
-apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(lifting plus_assoc_pre)
done
lemma int_induct_raw:
@@ -212,10 +206,7 @@
sorry
lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
-apply(lifting_setup ho_tst2)
-apply(regularize)
-apply(injection)
-apply(cleaning)
+apply(lifting ho_tst2)
done
lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
@@ -236,46 +227,6 @@
lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
by simp
-(* test about lifting identity equations *)
-
-ML {*
-(* helper code from QuotMain *)
-val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
-val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"}
-val simproc = Simplifier.simproc_i @{theory} "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
-val simpset = (mk_minimal_ss @{context})
- addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
- addsimprocs [simproc] addSolver equiv_solver
-*}
-
-(* What regularising does *)
-(*========================*)
-
-(* 0. preliminary simplification step *)
-thm ball_reg_eqv bex_reg_eqv (* of no use: babs_reg_eqv *)
- ball_reg_eqv_range bex_reg_eqv_range
-(* 1. first two rtacs *)
-thm ball_reg_right bex_reg_left
-(* 2. monos *)
-(* 3. commutation rules *)
-thm ball_all_comm bex_ex_comm
-(* 4. then rel-equality *)
-thm eq_imp_rel
-(* 5. then simplification like 0 *)
-(* finally jump to 1 *)
-
-
-(* What cleaning does *)
-(*====================*)
-
-(* 1. conversion *)
-thm lambda_prs
-(* 2. simplification with *)
-thm all_prs ex_prs
-(* 3. Simplification with *)
-thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep
-(* 4. Test for refl *)
-
lemma
shows "equivp (op \<approx>)"
and "equivp ((op \<approx>) ===> (op \<approx>))"
@@ -295,11 +246,9 @@
done
lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
+apply(lifting lam_tst3a)
apply(rule impI)
apply(rule lam_tst3a_reg)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *})
done
lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
--- a/Quot/Examples/LamEx.thy Wed Dec 16 14:28:48 2009 +0100
+++ b/Quot/Examples/LamEx.thy Thu Dec 17 14:58:33 2009 +0100
@@ -1,5 +1,5 @@
theory LamEx
-imports Nominal "../QuotList"
+imports Nominal "../QuotMain" "../QuotList"
begin
atom_decl name
@@ -165,46 +165,46 @@
lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
-apply (tactic {* lift_tac @{context} @{thm pi_var_com} 1 *})
+apply (lifting pi_var_com)
done
lemma pi_app: "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
-apply (tactic {* lift_tac @{context} @{thm pi_app_com} 1 *})
+apply (lifting pi_app_com)
done
lemma pi_lam: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
-apply (tactic {* lift_tac @{context} @{thm pi_lam_com} 1 *})
+apply (lifting pi_lam_com)
done
lemma fv_var: "fv (Var (a\<Colon>name)) = {a}"
-apply (tactic {* lift_tac @{context} @{thm rfv_var} 1 *})
+apply (lifting rfv_var)
done
lemma fv_app: "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
-apply (tactic {* lift_tac @{context} @{thm rfv_app} 1 *})
+apply (lifting rfv_app)
done
lemma fv_lam: "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
-apply (tactic {* lift_tac @{context} @{thm rfv_lam} 1 *})
+apply (lifting rfv_lam)
done
lemma a1: "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
-apply (tactic {* lift_tac @{context} @{thm a1} 1 *})
+apply (lifting a1)
done
lemma a2: "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
-apply (tactic {* lift_tac @{context} @{thm a2} 1 *})
+apply (lifting a2)
done
lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
-apply (tactic {* lift_tac @{context} @{thm a3} 1 *})
+apply (lifting a3)
done
lemma alpha_cases: "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
\<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
\<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
-apply (tactic {* lift_tac @{context} @{thm alpha.cases} 1 *})
+apply (lifting alpha.cases)
done
lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
@@ -212,16 +212,16 @@
\<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
\<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
\<Longrightarrow> qxb qx qxa"
-apply (tactic {* lift_tac @{context} @{thm alpha.induct} 1 *})
+apply (lifting alpha.induct)
done
lemma var_inject: "(Var a = Var b) = (a = b)"
-apply (tactic {* lift_tac @{context} @{thm rvar_inject} 1 *})
+apply (lifting rvar_inject)
done
lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
\<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
-apply (tactic {* lift_tac @{context} @{thm rlam.induct} 1 *})
+apply (lifting rlam.induct)
done
lemma var_supp:
--- a/Quot/QuotMain.thy Wed Dec 16 14:28:48 2009 +0100
+++ b/Quot/QuotMain.thy Thu Dec 17 14:58:33 2009 +0100
@@ -3,6 +3,8 @@
uses ("quotient_info.ML")
("quotient_typ.ML")
("quotient_def.ML")
+ ("quotient_term.ML")
+ ("quotient_tacs.ML")
begin
locale QUOT_TYPE =
@@ -107,36 +109,31 @@
(* lifting of constants *)
use "quotient_def.ML"
-section {* Simset setup *}
+(* the translation functions *)
+use "quotient_term.ML"
-(* Since HOL_basic_ss is too "big" for us, *)
-(* we set up our own minimal simpset. *)
-ML {*
-fun mk_minimal_ss ctxt =
- Simplifier.context ctxt empty_ss
- setsubgoaler asm_simp_tac
- setmksimps (mksimps [])
-*}
+(* tactics *)
+lemma eq_imp_rel:
+ "equivp R ==> a = b --> R a b"
+by (simp add: equivp_reflp)
-ML {*
-fun OF1 thm1 thm2 = thm2 RS thm1
-*}
+definition
+ "QUOT_TRUE x \<equiv> True"
-(* various tactic combinators *)
-ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
-*}
+lemma quot_true_dests:
+ shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
+ and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
+ and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"
+ and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
+by (simp_all add: QUOT_TRUE_def ext)
-ML {*
-(* prints warning, if goal is unsolved *)
-fun WARN (tac, msg) i st =
- case Seq.pull ((SOLVES' tac) i st) of
- NONE => (warning msg; Seq.single st)
- | seqcell => Seq.make (fn () => seqcell)
+lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
+by (simp add: QUOT_TRUE_def)
-fun RANGE_WARN xs = RANGE (map WARN xs)
-*}
+lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
+ by(auto simp add: QUOT_TRUE_def)
+use "quotient_tacs.ML"
section {* Atomize Infrastructure *}
@@ -160,16 +157,6 @@
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 *}
lemmas [id_simps] =
@@ -177,902 +164,6 @@
id_apply[THEN eq_reflection]
id_def[THEN eq_reflection,symmetric]
-section {* Computation of the Regularize Goal *}
-
-(*
-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 trm1 trm2 =
- case (trm1, trm2) of
- (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
- | _ => f trm1 trm2
-
-(* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)
-*}
-
-ML {*
-(* produces a regularized version of rtrm *)
-(* - the result is contains dummyT *)
-(* - does not need any special treatment of *)
-(* bound variables *)
-
-fun regularize_trm lthy rtrm qtrm =
- case (rtrm, qtrm) of
- (Abs (x, ty, t), Abs (x', ty', t')) =>
- let
- val subtrm = Abs(x, ty, regularize_trm lthy t t')
- in
- if ty = ty' then subtrm
- else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
- end
-
- | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
- let
- val subtrm = apply_subt (regularize_trm lthy) t 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
-
- | (* equalities need to be replaced by appropriate equivalence relations *)
- (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
- if ty = ty' then rtrm
- else mk_resp_arg lthy (domain_type ty, domain_type ty')
-
- | (* in this case we check whether the given equivalence relation is correct *)
- (rel, Const (@{const_name "op ="}, ty')) =>
- let
- val exc = LIFT_MATCH "regularise (relation mismatch)"
- val rel_ty = (fastype_of rel) handle TERM _ => raise exc
- val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty')
- in
- if rel' = rel then rtrm else raise exc
- end
-
- | (_, Const _) =>
- let
- fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)
- | same_name _ _ = false
- (* TODO/FIXME: This test is not enough. *)
- (* Why? *)
- (* Because constants can have the same name but not be the same
- constant. All overloaded constants have the same name but because
- of different types they do differ.
-
- This code will let one write a theorem where plus on nat is
- matched to plus on int, even if the latter is defined differently.
-
- This would result in hard to understand failures in injection and
- cleaning. *)
- (* cu: if I also test the type, then something else breaks *)
- in
- if same_name rtrm qtrm then rtrm
- else
- let
- val thy = ProofContext.theory_of lthy
- val qtrm_str = Syntax.string_of_term lthy qtrm
- val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
- val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
- val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
- in
- if Pattern.matches thy (rtrm', rtrm)
- then rtrm else raise exc2
- end
- 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 mismatch)")
-
- | _ =>
- let
- val rtrm_str = Syntax.string_of_term lthy rtrm
- val qtrm_str = Syntax.string_of_term lthy qtrm
- in
- raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
- end
-*}
-
-section {* Regularize Tactic *}
-
-ML {*
-fun equiv_tac ctxt =
- REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
-
-fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
-val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
-*}
-
-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 calculate_instance ctxt thm redex R1 R2 =
-let
- val thy = ProofContext.theory_of ctxt
- val goal = Const (@{const_name "equivp"}, dummyT) $ R2
- |> Syntax.check_term ctxt
- |> HOLogic.mk_Trueprop
- val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1)
- val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
- val R1c = cterm_of thy R1
- val thmi = Drule.instantiate' [] [SOME R1c] thm
- val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
- val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)
-in
- SOME thm2
-end
-handle _ => NONE
-(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)
-*}
-
-ML {*
-fun ball_bex_range_simproc ss redex =
-let
- val ctxt = Simplifier.the_context ss
-in
- case redex of
- (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
- (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
- calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
-
- | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
- (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
- calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
- | _ => NONE
-end
-*}
-
-lemma eq_imp_rel:
- shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
-by (simp add: equivp_reflp)
-
-ML {*
-(* test whether DETERM makes any difference *)
-fun quotient_tac ctxt = SOLVES'
- (REPEAT_ALL_NEW (FIRST'
- [rtac @{thm identity_quotient},
- resolve_tac (quotient_rules_get ctxt)]))
-
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
-fun solve_quotient_assum ctxt thm =
- case Seq.pull (quotient_tac ctxt 1 thm) of
- SOME (t, _) => t
- | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing"
-*}
-
-
-(* 0. preliminary simplification step according to *)
-thm ball_reg_eqv bex_reg_eqv babs_reg_eqv
- ball_reg_eqv_range bex_reg_eqv_range
-(* 1. eliminating simple Ball/Bex instances*)
-thm ball_reg_right bex_reg_left
-(* 2. monos *)
-(* 3. commutation rules for ball and bex *)
-thm ball_all_comm bex_ex_comm
-(* 4. then rel-equality (which need to be instantiated to avoid loops) *)
-thm eq_imp_rel
-(* 5. then simplification like 0 *)
-(* finally jump back to 1 *)
-
-ML {*
-fun regularize_tac ctxt =
-let
- val thy = ProofContext.theory_of ctxt
- val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
- val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"}
- val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
- val simpset = (mk_minimal_ss ctxt)
- addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
- addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver
- val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
-in
- simp_tac simpset THEN'
- REPEAT_ALL_NEW (CHANGED o FIRST' [
- resolve_tac @{thms ball_reg_right bex_reg_left},
- resolve_tac (Inductive.get_monos ctxt),
- resolve_tac @{thms ball_all_comm bex_ex_comm},
- resolve_tac eq_eqvs,
- simp_tac simpset])
-end
-*}
-
-section {* Calculation of the Injected Goal *}
-
-(*
-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 *)
-(* in the abstraction case *)
-
-fun inj_repabs_trm lthy (rtrm, qtrm) =
- 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' as (Abs _)) =>
- let
- val rty = fastype_of rtrm
- val qty = fastype_of qtrm
- in
- mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
- end
-
- | (Abs (x, T, t), Abs (x', T', t')) =>
- let
- val rty = fastype_of rtrm
- val qty = fastype_of qtrm
- 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
-
- | (t $ s, t' $ s') =>
- (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
-
- | (Free (_, T), Free (_, T')) =>
- if T = T' then rtrm
- else mk_repabs lthy (T, T') rtrm
-
- | (_, Const (@{const_name "op ="}, _)) => rtrm
-
- | (_, Const (_, T')) =>
- let
- val rty = fastype_of rtrm
- in
- if rty = T' then rtrm
- else mk_repabs lthy (rty, T') rtrm
- end
-
- | _ => raise (LIFT_MATCH "injection")
-*}
-
-section {* Injection Tactic *}
-
-definition
- "QUOT_TRUE x \<equiv> True"
-
-ML {*
-(* looks for QUOT_TRUE assumtions, and in case its argument *)
-(* is an application, it returns the function and the argument *)
-fun find_qt_asm asms =
-let
- fun find_fun trm =
- case trm of
- (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
- | _ => false
-in
- case find_first find_fun asms of
- SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
- | _ => NONE
-end
-*}
-
-text {*
-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_rsp_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
-*}
-
-lemma quot_true_dests:
- shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
- and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
- and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"
- and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
-by (simp_all add: QUOT_TRUE_def ext)
-
-lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
-by (simp add: QUOT_TRUE_def)
-
-lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
- by(auto simp add: QUOT_TRUE_def)
-
-ML {*
-fun quot_true_simple_conv ctxt fnctn ctrm =
- case (term_of ctrm) of
- (Const (@{const_name QUOT_TRUE}, _) $ x) =>
- let
- val fx = fnctn x;
- val thy = ProofContext.theory_of ctxt;
- val cx = cterm_of thy x;
- val cfx = cterm_of thy fx;
- val cxt = ctyp_of thy (fastype_of x);
- val cfxt = ctyp_of thy (fastype_of fx);
- val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
- in
- Conv.rewr_conv thm ctrm
- end
-*}
-
-ML {*
-fun quot_true_conv ctxt fnctn ctrm =
- case (term_of ctrm) of
- (Const (@{const_name QUOT_TRUE}, _) $ _) =>
- quot_true_simple_conv ctxt fnctn ctrm
- | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
- | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
- | _ => Conv.all_conv ctrm
-*}
-
-ML {*
-fun quot_true_tac ctxt fnctn =
- CONVERSION
- ((Conv.params_conv ~1 (fn ctxt =>
- (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
-*}
-
-ML {* fun dest_comb (f $ a) = (f, a) *}
-ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
-(* TODO: Can this be done easier? *)
-ML {*
-fun unlam t =
- case t of
- (Abs a) => snd (Term.dest_abs a)
- | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
-*}
-
-ML {*
-fun dest_fun_type (Type("fun", [T, S])) = (T, S)
- | dest_fun_type _ = error "dest_fun_type"
-*}
-
-ML {*
-val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
-*}
-
-ML {*
-(* we apply apply_rsp only in case if the type needs lifting, *)
-(* which is the case if the type of the data in the QUOT_TRUE *)
-(* assumption is different from the corresponding type in the goal *)
-val apply_rsp_tac =
- Subgoal.FOCUS (fn {concl, asms, context,...} =>
- let
- val bare_concl = HOLogic.dest_Trueprop (term_of concl)
- val qt_asm = find_qt_asm (map term_of asms)
- in
- case (bare_concl, qt_asm) of
- (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
- if (fastype_of qt_fun) = (fastype_of f)
- then no_tac
- else
- let
- val ty_x = fastype_of x
- val ty_b = fastype_of qt_arg
- val ty_f = range_type (fastype_of f)
- val thy = ProofContext.theory_of context
- val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
- val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
- val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
- in
- (rtac inst_thm THEN' quotient_tac context) 1
- end
- | _ => no_tac
- end)
-*}
-
-thm equals_rsp
-
-ML {*
-fun equals_rsp_tac R ctxt =
-let
- val ty = domain_type (fastype_of R);
- val thy = ProofContext.theory_of ctxt
- val thm = Drule.instantiate'
- [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
-in
- rtac thm THEN' quotient_tac ctxt
-end
-(* raised by instantiate' *)
-handle THM _ => K no_tac
- | TYPE _ => K no_tac
- | TERM _ => K no_tac
-*}
-
-ML {*
-fun rep_abs_rsp_tac ctxt =
- SUBGOAL (fn (goal, i) =>
- case (bare_concl goal) of
- (rel $ _ $ (rep $ (abs $ _))) =>
- (let
- val thy = ProofContext.theory_of ctxt;
- val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
- val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
- val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
- val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
- in
- (rtac inst_thm THEN' quotient_tac ctxt) i
- end
- handle THM _ => no_tac | TYPE _ => no_tac)
- | _ => no_tac)
-*}
-
-ML {*
-fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
-(case (bare_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_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 Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
- (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => 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 Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
- (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
- => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
-
-| (_ $
- (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
- (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
- => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
-
-| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
- (rtac @{thm refl} ORELSE'
- (equals_rsp_tac R ctxt THEN' RANGE [
- quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
-
- (* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
-
- (* respectfulness of constants; in particular of a simple relation *)
-| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
- => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
-
- (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
- (* observe ---> *)
-| _ $ _ $ _
- => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
- ORELSE' rep_abs_rsp_tac ctxt
-
-| _ => K no_tac
-) i)
-*}
-
-ML {*
-fun inj_repabs_step_tac ctxt rel_refl =
- (FIRST' [
- inj_repabs_tac_match ctxt,
- (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *)
-
- apply_rsp_tac ctxt THEN'
- RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
-
- (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
- (* merge with previous tactic *)
- Cong_Tac.cong_tac @{thm cong} THEN'
- RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
-
- (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
- rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
-
- (* resolving with R x y assumptions *)
- atac,
-
- (* reflexivity of the basic relations *)
- (* R \<dots> \<dots> *)
- resolve_tac rel_refl])
-*}
-
-ML {*
-fun inj_repabs_tac ctxt =
-let
- val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
-in
- inj_repabs_step_tac ctxt rel_refl
-end
-
-fun all_inj_repabs_tac ctxt =
- REPEAT_ALL_NEW (inj_repabs_tac ctxt)
-*}
-
-section {* Cleaning of the Theorem *}
-
-ML {*
-(* expands all fun_maps, except in front of bound variables *)
-
-fun fun_map_simple_conv xs ctxt ctrm =
- case (term_of ctrm) of
- ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
- if (member (op=) xs h)
- then Conv.all_conv ctrm
- else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm
- | _ => Conv.all_conv ctrm
-
-fun fun_map_conv xs ctxt ctrm =
- case (term_of ctrm) of
- _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
- fun_map_simple_conv xs ctxt) ctrm
- | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
- | _ => Conv.all_conv ctrm
-
-fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
-*}
-
-ML {*
-fun mk_abs u i t =
- if incr_boundvars i u aconv t then Bound i
- else (case t of
- t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2)
- | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
- | Bound j => if i = j then error "make_inst" else t
- | _ => t)
-
-fun make_inst lhs t =
-let
- val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
- val _ $ (Abs (_, _, (_ $ g))) = t;
-in
- (f, Abs ("x", T, mk_abs u 0 g))
-end
-
-fun make_inst_id lhs t =
-let
- val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
- val _ $ (Abs (_, _, g)) = t;
-in
- (f, Abs ("x", T, mk_abs u 0 g))
-end
-*}
-
-ML {*
-(* Simplifies a redex using the 'lambda_prs' theorem. *)
-(* First instantiates the types and known subterms. *)
-(* Then solves the quotient assumptions to get Rep2 and Abs1 *)
-(* Finally instantiates the function f using make_inst *)
-(* If Rep2 is identity then the pattern is simpler and make_inst_id is used *)
-fun lambda_prs_simple_conv ctxt ctrm =
- case (term_of ctrm) of
- (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
- (let
- val thy = ProofContext.theory_of ctxt
- val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
- val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
- val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_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 te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)]
- val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
- val make_inst = if ty_c = ty_d then make_inst_id else make_inst
- val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
- val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
- in
- Conv.rewr_conv ti ctrm
- end
- handle _ => Conv.all_conv ctrm)
- | _ => Conv.all_conv ctrm
-*}
-
-ML {*
-val lambda_prs_conv =
- More_Conv.top_conv lambda_prs_simple_conv
-
-fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
-*}
-
-(* 1. folding of definitions and preservation lemmas; *)
-(* and simplification with *)
-thm babs_prs all_prs ex_prs
-(* 2. unfolding of ---> in front of everything, except *)
-(* bound variables (this prevents lambda_prs from *)
-(* becoming stuck *)
-thm fun_map.simps
-(* 3. simplification with *)
-thm lambda_prs
-(* 4. simplification with *)
-thm Quotient_abs_rep Quotient_rel_rep id_simps
-(* 5. Test for refl *)
-
-ML {*
-fun clean_tac lthy =
- let
- val thy = ProofContext.theory_of lthy;
- val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
- (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
-
- val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
- val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
- fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
- in
- EVERY' [simp_tac (simps thms1),
- fun_map_tac lthy,
- lambda_prs_tac lthy,
- simp_tac (simps thms2),
- TRY o rtac refl]
- end
-*}
-
-section {* Tactic for 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 {* The General Shape 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 *)
-(* *)
-(* - 1st prem is the regularization step *)
-(* - 2nd prem is the rep/abs injection step *)
-(* - 3rd prem is the cleaning part *)
-(* *)
-(* the QUOT_TRUE premise in 2 records the lifted theorem *)
-
-ML {*
-val lifting_procedure =
- @{lemma "\<lbrakk>A;
- A \<longrightarrow> B;
- QUOT_TRUE D \<Longrightarrow> B = C;
- C = D\<rbrakk> \<Longrightarrow> D"
- by (simp add: QUOT_TRUE_def)}
-*}
-
-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 = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str,
- "", "does not match with original theorem", rtrm_str]
-in
- error 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),
- NONE,
- SOME (cterm_of thy inj_goal)] lifting_procedure
-end
-*}
-
-ML {*
-(* the tactic leaves three subgoals to be proved *)
-fun procedure_tac ctxt rthm =
- ObjectLogic.full_atomize_tac
- THEN' gen_frees_tac ctxt
- THEN' CSUBGOAL (fn (goal, i) =>
- let
- val rthm' = atomize_thm rthm
- val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
- in
- (rtac rule THEN' rtac rthm') i
- end)
-*}
-
-section {* Automatic Proofs *}
-
-
-ML {*
-local
-
-val msg1 = "Regularize proof failed."
-val msg2 = cat_lines ["Injection proof failed.",
- "This is probably due to missing respects lemmas.",
- "Try invoking the injection method manually to see",
- "which lemmas are missing."]
-val msg3 = "Cleaning proof failed."
-
-in
-
-fun lift_tac ctxt rthm =
- procedure_tac ctxt rthm
- THEN' RANGE_WARN
- [(regularize_tac ctxt, msg1),
- (all_inj_repabs_tac ctxt, msg2),
- (clean_tac ctxt, msg3)]
-
-end
-*}
-
section {* Methods / Interface *}
ML {*
@@ -1084,23 +175,23 @@
*}
method_setup lifting =
- {* Attrib.thm >> (mk_method1 lift_tac) *}
+ {* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *}
{* Lifting of theorems to quotient types. *}
method_setup lifting_setup =
- {* Attrib.thm >> (mk_method1 procedure_tac) *}
+ {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
{* Sets up the three goals for the lifting procedure. *}
method_setup regularize =
- {* Scan.succeed (mk_method2 regularize_tac) *}
+ {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
{* Proves automatically the regularization goals from the lifting procedure. *}
method_setup injection =
- {* Scan.succeed (mk_method2 all_inj_repabs_tac) *}
+ {* Scan.succeed (mk_method2 Quotient_Tacs.all_inj_repabs_tac) *}
{* Proves automatically the rep/abs injection goals from the lifting procedure. *}
method_setup cleaning =
- {* Scan.succeed (mk_method2 clean_tac) *}
+ {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
{* Proves automatically the cleaning goals from the lifting procedure. *}
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/quotient_tacs.ML Thu Dec 17 14:58:33 2009 +0100
@@ -0,0 +1,619 @@
+signature QUOTIENT_TACS =
+sig
+ val regularize_tac: Proof.context -> int -> tactic
+ val all_inj_repabs_tac: Proof.context -> int -> tactic
+ val clean_tac: Proof.context -> int -> tactic
+ val procedure_tac: Proof.context -> thm -> int -> tactic
+ val lift_tac: Proof.context ->thm -> int -> tactic
+ val quotient_tac: Proof.context -> int -> tactic
+end;
+
+structure Quotient_Tacs: QUOTIENT_TACS =
+struct
+
+(* Since HOL_basic_ss is too "big" for us, *)
+(* we need to set up our own minimal simpset. *)
+fun mk_minimal_ss ctxt =
+ Simplifier.context ctxt empty_ss
+ setsubgoaler asm_simp_tac
+ setmksimps (mksimps [])
+
+
+
+(* various helper functions *)
+fun OF1 thm1 thm2 = thm2 RS thm1
+
+(* makes sure a subgoal is solved *)
+fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
+
+(* prints warning, if goal is unsolved *)
+fun WARN (tac, msg) i st =
+ case Seq.pull ((SOLVES' tac) i st) of
+ NONE => (warning msg; Seq.single st)
+ | seqcell => Seq.make (fn () => seqcell)
+
+fun RANGE_WARN xs = RANGE (map WARN xs)
+
+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
+
+
+
+
+(* Regularize Tactic *)
+
+fun equiv_tac ctxt =
+ REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
+
+fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
+val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
+
+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)
+
+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
+
+fun calculate_instance ctxt thm redex R1 R2 =
+let
+ val thy = ProofContext.theory_of ctxt
+ val goal = Const (@{const_name "equivp"}, dummyT) $ R2
+ |> Syntax.check_term ctxt
+ |> HOLogic.mk_Trueprop
+ val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1)
+ val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
+ val R1c = cterm_of thy R1
+ val thmi = Drule.instantiate' [] [SOME R1c] thm
+ val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
+ val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)
+in
+ SOME thm2
+end
+handle _ => NONE
+(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)
+
+fun ball_bex_range_simproc ss redex =
+let
+ val ctxt = Simplifier.the_context ss
+in
+ case redex of
+ (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
+ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
+
+ | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
+ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
+ | _ => NONE
+end
+
+(* test whether DETERM makes any difference *)
+fun quotient_tac ctxt = SOLVES'
+ (REPEAT_ALL_NEW (FIRST'
+ [rtac @{thm identity_quotient},
+ resolve_tac (quotient_rules_get ctxt)]))
+
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+
+fun solve_quotient_assum ctxt thm =
+ case Seq.pull (quotient_tac ctxt 1 thm) of
+ SOME (t, _) => t
+ | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing"
+
+
+(* 0. preliminary simplification step according to *)
+(* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *)
+(* ball_reg_eqv_range bex_reg_eqv_range *)
+(* *)
+(* 1. eliminating simple Ball/Bex instances *)
+(* thm ball_reg_right bex_reg_left *)
+(* *)
+(* 2. monos *)
+(* 3. commutation rules for ball and bex *)
+(* thm ball_all_comm bex_ex_comm *)
+(* *)
+(* 4. then rel-equality (which need to be *)
+(* instantiated to avoid loops) *)
+(* thm eq_imp_rel *)
+(* *)
+(* 5. then simplification like 0 *)
+(* *)
+(* finally jump back to 1 *)
+
+fun regularize_tac ctxt =
+let
+ val thy = ProofContext.theory_of ctxt
+ val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
+ val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"}
+ val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
+ val simpset = (mk_minimal_ss ctxt)
+ addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
+ addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver
+ val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
+in
+ simp_tac simpset THEN'
+ REPEAT_ALL_NEW (CHANGED o FIRST' [
+ resolve_tac @{thms ball_reg_right bex_reg_left},
+ resolve_tac (Inductive.get_monos ctxt),
+ resolve_tac @{thms ball_all_comm bex_ex_comm},
+ resolve_tac eq_eqvs,
+ simp_tac simpset])
+end
+
+
+
+(* Injection Tactic *)
+
+(* looks for QUOT_TRUE assumtions, and in case its parameter *)
+(* is an application, it returns the function and the argument *)
+fun find_qt_asm asms =
+let
+ fun find_fun trm =
+ case trm of
+ (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
+ | _ => false
+in
+ case find_first find_fun asms of
+ SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+ | _ => NONE
+end
+
+fun quot_true_simple_conv ctxt fnctn ctrm =
+ case (term_of ctrm) of
+ (Const (@{const_name QUOT_TRUE}, _) $ x) =>
+ let
+ val fx = fnctn x;
+ val thy = ProofContext.theory_of ctxt;
+ val cx = cterm_of thy x;
+ val cfx = cterm_of thy fx;
+ val cxt = ctyp_of thy (fastype_of x);
+ val cfxt = ctyp_of thy (fastype_of fx);
+ val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
+ in
+ Conv.rewr_conv thm ctrm
+ end
+
+fun quot_true_conv ctxt fnctn ctrm =
+ case (term_of ctrm) of
+ (Const (@{const_name QUOT_TRUE}, _) $ _) =>
+ quot_true_simple_conv ctxt fnctn ctrm
+ | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
+ | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
+ | _ => Conv.all_conv ctrm
+
+fun quot_true_tac ctxt fnctn =
+ CONVERSION
+ ((Conv.params_conv ~1 (fn ctxt =>
+ (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
+
+fun dest_comb (f $ a) = (f, a)
+fun dest_bcomb ((_ $ l) $ r) = (l, r)
+
+(* TODO: Can this be done easier? *)
+fun unlam t =
+ case t of
+ (Abs a) => snd (Term.dest_abs a)
+ | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
+
+fun dest_fun_type (Type("fun", [T, S])) = (T, S)
+ | dest_fun_type _ = error "dest_fun_type"
+
+val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
+
+
+(* we apply apply_rsp only in case if the type needs lifting, *)
+(* which is the case if the type of the data in the QUOT_TRUE *)
+(* assumption is different from the corresponding type in the goal *)
+val apply_rsp_tac =
+ Subgoal.FOCUS (fn {concl, asms, context,...} =>
+ let
+ val bare_concl = HOLogic.dest_Trueprop (term_of concl)
+ val qt_asm = find_qt_asm (map term_of asms)
+ in
+ case (bare_concl, qt_asm) of
+ (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
+ if (fastype_of qt_fun) = (fastype_of f)
+ then no_tac
+ else
+ let
+ val ty_x = fastype_of x
+ val ty_b = fastype_of qt_arg
+ val ty_f = range_type (fastype_of f)
+ val thy = ProofContext.theory_of context
+ val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
+ val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+ val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
+ in
+ (rtac inst_thm THEN' quotient_tac context) 1
+ end
+ | _ => no_tac
+ end)
+
+fun equals_rsp_tac R ctxt =
+let
+ val ty = domain_type (fastype_of R);
+ val thy = ProofContext.theory_of ctxt
+ val thm = Drule.instantiate'
+ [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
+in
+ rtac thm THEN' quotient_tac ctxt
+end
+(* raised by instantiate' *)
+handle THM _ => K no_tac
+ | TYPE _ => K no_tac
+ | TERM _ => K no_tac
+
+
+fun rep_abs_rsp_tac ctxt =
+ SUBGOAL (fn (goal, i) =>
+ case (bare_concl goal) of
+ (rel $ _ $ (rep $ (abs $ _))) =>
+ (let
+ val thy = ProofContext.theory_of ctxt;
+ val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+ val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+ val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
+ val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
+ in
+ (rtac inst_thm THEN' quotient_tac ctxt) i
+ end
+ handle THM _ => no_tac | TYPE _ => no_tac)
+ | _ => no_tac)
+
+
+(* FIXME /TODO needs to be adapted *)
+(*
+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_rsp_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
+*)
+
+
+fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
+(case (bare_concl goal) of
+ (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
+ (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
+ => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+
+ (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
+| (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...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
+| (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_id} THEN' quot_true_tac ctxt unlam
+
+ (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
+| 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...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
+| (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_id} THEN' quot_true_tac ctxt unlam
+
+| (_ $
+ (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+ (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+ => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+
+| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+ (rtac @{thm refl} ORELSE'
+ (equals_rsp_tac R ctxt THEN' RANGE [
+ quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+
+ (* reflexivity of operators arising from Cong_tac *)
+| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
+
+ (* respectfulness of constants; in particular of a simple relation *)
+| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
+ => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+
+ (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
+ (* observe fun_map *)
+| _ $ _ $ _
+ => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
+ ORELSE' rep_abs_rsp_tac ctxt
+
+| _ => K no_tac
+) i)
+
+fun inj_repabs_step_tac ctxt rel_refl =
+ FIRST' [
+ inj_repabs_tac_match ctxt,
+ (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *)
+
+ apply_rsp_tac ctxt THEN'
+ RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
+
+ (* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *)
+ (* merge with previous tactic *)
+ Cong_Tac.cong_tac @{thm cong} THEN'
+ RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
+
+ (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
+ rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
+
+ (* resolving with R x y assumptions *)
+ atac,
+
+ (* reflexivity of the basic relations *)
+ (* R ... ... *)
+ resolve_tac rel_refl]
+
+fun inj_repabs_tac ctxt =
+let
+ val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
+in
+ inj_repabs_step_tac ctxt rel_refl
+end
+
+fun all_inj_repabs_tac ctxt =
+ REPEAT_ALL_NEW (inj_repabs_tac ctxt)
+
+
+(* Cleaning of the Theorem *)
+
+
+(* expands all fun_maps, except in front of bound variables *)
+fun fun_map_simple_conv xs ctrm =
+ case (term_of ctrm) of
+ ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
+ if (member (op=) xs h)
+ then Conv.all_conv ctrm
+ else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm
+ | _ => Conv.all_conv ctrm
+
+fun fun_map_conv xs ctxt ctrm =
+ case (term_of ctrm) of
+ _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
+ fun_map_simple_conv xs) ctrm
+ | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
+ | _ => Conv.all_conv ctrm
+
+fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
+
+fun mk_abs u i t =
+ if incr_boundvars i u aconv t then Bound i
+ else (case t of
+ t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2)
+ | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
+ | Bound j => if i = j then error "make_inst" else t
+ | _ => t)
+
+fun make_inst lhs t =
+let
+ val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+ val _ $ (Abs (_, _, (_ $ g))) = t;
+in
+ (f, Abs ("x", T, mk_abs u 0 g))
+end
+
+fun make_inst_id lhs t =
+let
+ val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ val _ $ (Abs (_, _, g)) = t;
+in
+ (f, Abs ("x", T, mk_abs u 0 g))
+end
+
+(* Simplifies a redex using the 'lambda_prs' theorem. *)
+(* First instantiates the types and known subterms. *)
+(* Then solves the quotient assumptions to get Rep2 and Abs1 *)
+(* Finally instantiates the function f using make_inst *)
+(* If Rep2 is identity then the pattern is simpler and *)
+(* make_inst_id is used *)
+fun lambda_prs_simple_conv ctxt ctrm =
+ case (term_of ctrm) of
+ (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
+ (let
+ val thy = ProofContext.theory_of ctxt
+ val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+ val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+ val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_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 te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)]
+ val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+ val make_inst = if ty_c = ty_d then make_inst_id else make_inst
+ val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
+ val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+ in
+ Conv.rewr_conv ti ctrm
+ end
+ handle _ => Conv.all_conv ctrm)
+ | _ => Conv.all_conv ctrm
+
+val lambda_prs_conv =
+ More_Conv.top_conv lambda_prs_simple_conv
+
+fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
+
+
+(* 1. folding of definitions and preservation lemmas; *)
+(* and simplification with *)
+(* thm babs_prs all_prs ex_prs *)
+(* *)
+(* 2. unfolding of ---> in front of everything, except *)
+(* bound variables (this prevents lambda_prs from *)
+(* becoming stuck *)
+(* thm fun_map.simps *)
+(* *)
+(* 3. simplification with *)
+(* thm lambda_prs *)
+(* *)
+(* 4. simplification with *)
+(* thm Quotient_abs_rep Quotient_rel_rep id_simps *)
+(* *)
+(* 5. Test for refl *)
+
+fun clean_tac lthy =
+ let
+ val thy = ProofContext.theory_of lthy;
+ val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+ (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
+
+ val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
+ val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
+ fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+ in
+ EVERY' [simp_tac (simps thms1),
+ fun_map_tac lthy,
+ lambda_prs_tac lthy,
+ simp_tac (simps thms2),
+ TRY o rtac refl]
+ end
+
+
+
+(* Tactic for Genralisation of Free Variables in a Goal *)
+
+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)
+
+
+(* The General Shape 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 *)
+(* *)
+(* - 1st prem is the regularization step *)
+(* - 2nd prem is the rep/abs injection step *)
+(* - 3rd prem is the cleaning part *)
+(* *)
+(* the QUOT_TRUE premise in 2 records the lifted theorem *)
+
+val lifting_procedure =
+ @{lemma "[|A;
+ A --> B;
+ QUOT_TRUE D ==> B = C;
+ C = D|] ==> D"
+ by (simp add: QUOT_TRUE_def)}
+
+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 = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str,
+ "", "does not match with original theorem", rtrm_str]
+in
+ error msg
+end
+
+
+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),
+ NONE,
+ SOME (cterm_of thy inj_goal)] lifting_procedure
+end
+
+
+(* the tactic leaves three subgoals to be proved *)
+fun procedure_tac ctxt rthm =
+ ObjectLogic.full_atomize_tac
+ THEN' gen_frees_tac ctxt
+ THEN' CSUBGOAL (fn (goal, i) =>
+ let
+ val rthm' = atomize_thm rthm
+ val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
+ in
+ (rtac rule THEN' rtac rthm') i
+ end)
+
+
+(* Automatic Proofs *)
+
+val msg1 = "Regularize proof failed."
+val msg2 = cat_lines ["Injection proof failed.",
+ "This is probably due to missing respects lemmas.",
+ "Try invoking the injection method manually to see",
+ "which lemmas are missing."]
+val msg3 = "Cleaning proof failed."
+
+fun lift_tac ctxt rthm =
+ procedure_tac ctxt rthm
+ THEN' RANGE_WARN
+ [(regularize_tac ctxt, msg1),
+ (all_inj_repabs_tac ctxt, msg2),
+ (clean_tac ctxt, msg3)]
+
+
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/quotient_term.ML Thu Dec 17 14:58:33 2009 +0100
@@ -0,0 +1,278 @@
+signature QUOTIENT_TERM =
+sig
+ val regularize_trm: Proof.context -> term -> term -> term
+ val inj_repabs_trm: Proof.context -> (term * term) -> term
+end;
+
+structure Quotient_Term: QUOTIENT_TERM =
+struct
+
+(*
+Regularizing an rtrm means:
+
+ - Quantifiers over a type that need lifting are replaced
+ by bounded quantifiers, for example:
+
+ All P ===> All (Respects R) P
+
+ where the relation R is given by the rty and qty;
+
+ - Abstractions over a type that needs lifting are replaced
+ by bounded abstractions:
+
+ %x. P ===> Ball (Respects R) %x. P
+
+ - Equalities over the type being lifted are replaced by
+ corresponding equivalence relations:
+
+ A = B ===> R A B
+
+ or
+
+ A = B ===> (R ===> R) A B
+
+ for more complicated types of A and B
+*)
+
+(* 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
+ (* FIXME dont return an option, raise an exception *)
+ 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
+
+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)
+
+(* - 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 trm1 trm2 =
+ case (trm1, trm2) of
+ (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f t t')
+ | _ => f trm1 trm2
+
+(* the major type of All and Ex quantifiers *)
+fun qnt_typ ty = domain_type (domain_type ty)
+
+
+(* produces a regularized version of rtrm *)
+(* *)
+(* - the result is still contains dummyT *)
+(* *)
+(* - for regularisation we do not need any *)
+(* special treatment of bound variables *)
+
+fun regularize_trm lthy rtrm qtrm =
+ case (rtrm, qtrm) of
+ (Abs (x, ty, t), Abs (_, ty', t')) =>
+ let
+ val subtrm = Abs(x, ty, regularize_trm lthy t t')
+ in
+ if ty = ty' then subtrm
+ else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
+ end
+
+ | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
+ let
+ val subtrm = apply_subt (regularize_trm lthy) t 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
+
+ | (* equalities need to be replaced by appropriate equivalence relations *)
+ (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
+ if ty = ty' then rtrm
+ else mk_resp_arg lthy (domain_type ty, domain_type ty')
+
+ | (* in this case we check whether the given equivalence relation is correct *)
+ (rel, Const (@{const_name "op ="}, ty')) =>
+ let
+ val exc = LIFT_MATCH "regularise (relation mismatch)"
+ val rel_ty = (fastype_of rel) handle TERM _ => raise exc
+ val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty')
+ in
+ if rel' = rel then rtrm else raise exc
+ end
+
+ | (_, Const _) =>
+ let
+ fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)
+ | same_name _ _ = false
+ (* TODO/FIXME: This test is not enough. *)
+ (* Why? *)
+ (* Because constants can have the same name but not be the same
+ constant. All overloaded constants have the same name but because
+ of different types they do differ.
+
+ This code will let one write a theorem where plus on nat is
+ matched to plus on int, even if the latter is defined differently.
+
+ This would result in hard to understand failures in injection and
+ cleaning. *)
+ (* cu: if I also test the type, then something else breaks *)
+ in
+ if same_name rtrm qtrm then rtrm
+ else
+ let
+ val thy = ProofContext.theory_of lthy
+ val qtrm_str = Syntax.string_of_term lthy qtrm
+ val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
+ val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
+ val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
+ in
+ if Pattern.matches thy (rtrm', rtrm)
+ then rtrm else raise exc2
+ end
+ 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 mismatch)")
+
+ | _ =>
+ let
+ val rtrm_str = Syntax.string_of_term lthy rtrm
+ val qtrm_str = Syntax.string_of_term lthy qtrm
+ in
+ raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
+ end
+
+
+
+(*
+Injecting of Rep/Abs means:
+
+ For abstractions
+:
+ * If the type of the abstraction doesn't need lifting we recurse.
+
+ * If it needs lifting then we add Rep/Abs around the whole term and
+ check if the bound variable needs lifting.
+
+ * If it does we recurse and put Rep/Abs around all occurences
+ of the variable in the obtained subterm. This in combination
+ with the Rep/Abs from 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 Rep/Abs 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 Rep/Abs and recurse
+
+ * Otherwise just recurse.
+*)
+
+fun mk_repabs lthy (T, T') trm =
+ Quotient_Def.get_fun repF lthy (T, T')
+ $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
+
+
+(* bound variables need to be treated properly, *)
+(* as the type of subterms needs to be calculated *)
+
+fun inj_repabs_trm lthy (rtrm, qtrm) =
+ 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' as (Abs _)) =>
+ let
+ val rty = fastype_of rtrm
+ val qty = fastype_of qtrm
+ in
+ mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
+ end
+
+ | (Abs (x, T, t), Abs (x', T', t')) =>
+ let
+ val rty = fastype_of rtrm
+ val qty = fastype_of qtrm
+ 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
+
+ | (t $ s, t' $ s') =>
+ (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
+
+ | (Free (_, T), Free (_, T')) =>
+ if T = T' then rtrm
+ else mk_repabs lthy (T, T') rtrm
+
+ | (_, Const (@{const_name "op ="}, _)) => rtrm
+
+ | (_, Const (_, T')) =>
+ let
+ val rty = fastype_of rtrm
+ in
+ if rty = T' then rtrm
+ else mk_repabs lthy (rty, T') rtrm
+ end
+
+ | _ => raise (LIFT_MATCH "injection")
+
+end; (* structure *)
+
+open Quotient_Term;
+
+