get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
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+ −
+ −
open Quotient_Info;+ −
open Quotient_Type;+ −
open Quotient_Term;+ −
+ −
+ −
(* 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+ −
simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) + −
THEN' 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_aux 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+ −
+ −
fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)+ −
+ −
(* 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; (* structure *)+ −