haftmann@37743: (*  Title:      HOL/Tools/Quotient/quotient_tacs.ML
kaliszyk@35222:     Author:     Cezary Kaliszyk and Christian Urban
kaliszyk@35222: 
wenzelm@35788: Tactics for solving goal arising from lifting theorems to quotient
wenzelm@35788: types.
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: signature QUOTIENT_TACS =
kaliszyk@35222: sig
kaliszyk@35222:   val regularize_tac: Proof.context -> int -> tactic
kaliszyk@35222:   val injection_tac: Proof.context -> int -> tactic
kaliszyk@35222:   val all_injection_tac: Proof.context -> int -> tactic
kaliszyk@35222:   val clean_tac: Proof.context -> int -> tactic
wenzelm@41700: 
urbanc@39088:   val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
urbanc@39088:   val descend_tac: Proof.context -> thm list -> int -> tactic
wenzelm@41700: 
urbanc@39088:   val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
urbanc@39088:   val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
urbanc@37593: 
urbanc@38848:   val lifted: Proof.context -> typ list -> thm list -> thm -> thm
kaliszyk@35222:   val lifted_attrib: attribute
kaliszyk@35222: end;
kaliszyk@35222: 
kaliszyk@35222: structure Quotient_Tacs: QUOTIENT_TACS =
kaliszyk@35222: struct
kaliszyk@35222: 
kaliszyk@35222: (** various helper fuctions **)
kaliszyk@35222: 
kaliszyk@35222: (* Since HOL_basic_ss is too "big" for us, we *)
kaliszyk@35222: (* need to set up our own minimal simpset.    *)
kaliszyk@35222: fun mk_minimal_ss ctxt =
kaliszyk@35222:   Simplifier.context ctxt empty_ss
kaliszyk@35222:     setsubgoaler asm_simp_tac
kaliszyk@35222:     setmksimps (mksimps [])
kaliszyk@35222: 
kaliszyk@35222: (* composition of two theorems, used in maps *)
kaliszyk@35222: fun OF1 thm1 thm2 = thm2 RS thm1
kaliszyk@35222: 
kaliszyk@35222: fun atomize_thm thm =
wenzelm@41700:   let
wenzelm@41700:     val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
wenzelm@41700:     val thm'' = Object_Logic.atomize (cprop_of thm')
wenzelm@41700:   in
wenzelm@41700:     @{thm equal_elim_rule1} OF [thm'', thm']
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (*** Regularize Tactic ***)
kaliszyk@35222: 
kaliszyk@35222: (** solvers for equivp and quotient assumptions **)
kaliszyk@35222: 
kaliszyk@35222: fun equiv_tac ctxt =
wenzelm@41707:   REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt))
kaliszyk@35222: 
kaliszyk@35222: fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
wenzelm@44469: val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac
kaliszyk@35222: 
kaliszyk@35222: fun quotient_tac ctxt =
kaliszyk@35222:   (REPEAT_ALL_NEW (FIRST'
kaliszyk@35222:     [rtac @{thm identity_quotient},
wenzelm@41707:      resolve_tac (Quotient_Info.quotient_rules_get ctxt)]))
kaliszyk@35222: 
kaliszyk@35222: fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
wenzelm@44469: val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac
kaliszyk@35222: 
kaliszyk@35222: fun solve_quotient_assm ctxt thm =
kaliszyk@35222:   case Seq.pull (quotient_tac ctxt 1 thm) of
kaliszyk@35222:     SOME (t, _) => t
kaliszyk@35222:   | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: fun prep_trm thy (x, (T, t)) =
kaliszyk@35222:   (cterm_of thy (Var (x, T)), cterm_of thy t)
kaliszyk@35222: 
kaliszyk@35222: fun prep_ty thy (x, (S, ty)) =
kaliszyk@35222:   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
kaliszyk@35222: 
kaliszyk@35222: fun get_match_inst thy pat trm =
wenzelm@41700:   let
wenzelm@41700:     val univ = Unify.matchers thy [(pat, trm)]
wenzelm@41700:     val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
wenzelm@41700:     val tenv = Vartab.dest (Envir.term_env env)
wenzelm@41700:     val tyenv = Vartab.dest (Envir.type_env env)
wenzelm@41700:   in
wenzelm@41700:     (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: (* Calculates the instantiations for the lemmas:
kaliszyk@35222: 
kaliszyk@35222:       ball_reg_eqv_range and bex_reg_eqv_range
kaliszyk@35222: 
kaliszyk@35222:    Since the left-hand-side contains a non-pattern '?P (f ?x)'
kaliszyk@35222:    we rely on unification/instantiation to check whether the
kaliszyk@35222:    theorem applies and return NONE if it doesn't.
kaliszyk@35222: *)
kaliszyk@35222: fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
wenzelm@41700:   let
wenzelm@43232:     val thy = Proof_Context.theory_of ctxt
wenzelm@41700:     fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
wenzelm@41700:     val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
wenzelm@41700:     val trm_inst = map (SOME o cterm_of thy) [R2, R1]
wenzelm@41700:   in
wenzelm@41700:     (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
wenzelm@41700:       NONE => NONE
wenzelm@41700:     | SOME thm' =>
wenzelm@41700:         (case try (get_match_inst thy (get_lhs thm')) redex of
wenzelm@41700:           NONE => NONE
wenzelm@44215:         | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: fun ball_bex_range_simproc ss redex =
wenzelm@41700:   let
wenzelm@41700:     val ctxt = Simplifier.the_context ss
wenzelm@41700:   in
wenzelm@41700:     case redex of
wenzelm@41700:       (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
wenzelm@41700:         (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
wenzelm@41700:           calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
kaliszyk@35222: 
wenzelm@41700:     | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
wenzelm@41700:         (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
wenzelm@41700:           calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
kaliszyk@35222: 
wenzelm@41700:     | _ => NONE
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: (* Regularize works as follows:
kaliszyk@35222: 
kaliszyk@35222:   0. preliminary simplification step according to
kaliszyk@35222:      ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
kaliszyk@35222: 
kaliszyk@35222:   1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
kaliszyk@35222: 
kaliszyk@35222:   2. monos
kaliszyk@35222: 
kaliszyk@35222:   3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
kaliszyk@35222: 
kaliszyk@35222:   4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
kaliszyk@35222:      to avoid loops
kaliszyk@35222: 
kaliszyk@35222:   5. then simplification like 0
kaliszyk@35222: 
kaliszyk@35222:   finally jump back to 1
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@37493: fun reflp_get ctxt =
kaliszyk@37493:   map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
wenzelm@41707:     handle THM _ => NONE) (Quotient_Info.equiv_rules_get ctxt)
kaliszyk@37493: 
kaliszyk@37493: val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
kaliszyk@37493: 
wenzelm@41707: fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules_get ctxt)
kaliszyk@37493: 
kaliszyk@35222: fun regularize_tac ctxt =
wenzelm@41700:   let
wenzelm@43232:     val thy = Proof_Context.theory_of ctxt
wenzelm@41700:     val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
wenzelm@41700:     val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
wenzelm@41700:     val simproc =
wenzelm@41700:       Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
wenzelm@41700:     val simpset =
wenzelm@41700:       mk_minimal_ss ctxt
wenzelm@41700:       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
wenzelm@41700:       addsimprocs [simproc]
wenzelm@41700:       addSolver equiv_solver addSolver quotient_solver
wenzelm@41700:     val eq_eqvs = eq_imp_rel_get ctxt
wenzelm@41700:   in
wenzelm@41700:     simp_tac simpset THEN'
wenzelm@41700:     REPEAT_ALL_NEW (CHANGED o FIRST'
wenzelm@41700:       [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
wenzelm@41700:        resolve_tac (Inductive.get_monos ctxt),
wenzelm@41700:        resolve_tac @{thms ball_all_comm bex_ex_comm},
wenzelm@41700:        resolve_tac eq_eqvs,
wenzelm@41700:        simp_tac simpset])
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (*** Injection Tactic ***)
kaliszyk@35222: 
kaliszyk@35222: (* Looks for Quot_True assumptions, and in case its parameter
kaliszyk@35222:    is an application, it returns the function and the argument.
kaliszyk@35222: *)
kaliszyk@35222: fun find_qt_asm asms =
wenzelm@41700:   let
wenzelm@41700:     fun find_fun trm =
wenzelm@41700:       (case trm of
wenzelm@41700:         (Const (@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
wenzelm@41700:       | _ => false)
wenzelm@41700:   in
wenzelm@41700:      (case find_first find_fun asms of
wenzelm@41700:        SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
wenzelm@41700:      | _ => NONE)
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: fun quot_true_simple_conv ctxt fnctn ctrm =
wenzelm@41700:   case term_of ctrm of
kaliszyk@35222:     (Const (@{const_name Quot_True}, _) $ x) =>
wenzelm@41700:       let
wenzelm@41700:         val fx = fnctn x;
wenzelm@43232:         val thy = Proof_Context.theory_of ctxt;
wenzelm@41700:         val cx = cterm_of thy x;
wenzelm@41700:         val cfx = cterm_of thy fx;
wenzelm@41700:         val cxt = ctyp_of thy (fastype_of x);
wenzelm@41700:         val cfxt = ctyp_of thy (fastype_of fx);
wenzelm@41700:         val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
wenzelm@41700:       in
wenzelm@41700:         Conv.rewr_conv thm ctrm
wenzelm@41700:       end
kaliszyk@35222: 
kaliszyk@35222: fun quot_true_conv ctxt fnctn ctrm =
wenzelm@41700:   (case term_of ctrm of
kaliszyk@35222:     (Const (@{const_name Quot_True}, _) $ _) =>
kaliszyk@35222:       quot_true_simple_conv ctxt fnctn ctrm
kaliszyk@35222:   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
kaliszyk@35222:   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
wenzelm@41700:   | _ => Conv.all_conv ctrm)
kaliszyk@35222: 
kaliszyk@35222: fun quot_true_tac ctxt fnctn =
wenzelm@41700:   CONVERSION
kaliszyk@35222:     ((Conv.params_conv ~1 (fn ctxt =>
wenzelm@41700:         (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
kaliszyk@35222: 
kaliszyk@35222: fun dest_comb (f $ a) = (f, a)
kaliszyk@35222: fun dest_bcomb ((_ $ l) $ r) = (l, r)
kaliszyk@35222: 
kaliszyk@35222: fun unlam t =
wenzelm@41700:   (case t of
wenzelm@41700:     Abs a => snd (Term.dest_abs a)
wenzelm@41700:   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
kaliszyk@35222: 
kaliszyk@35222: val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
kaliszyk@35222: 
kaliszyk@35222: (* We apply apply_rsp only in case if the type needs lifting.
kaliszyk@35222:    This is the case if the type of the data in the Quot_True
kaliszyk@35222:    assumption is different from the corresponding type in the goal.
kaliszyk@35222: *)
kaliszyk@35222: val apply_rsp_tac =
kaliszyk@35222:   Subgoal.FOCUS (fn {concl, asms, context,...} =>
wenzelm@41700:     let
wenzelm@41700:       val bare_concl = HOLogic.dest_Trueprop (term_of concl)
wenzelm@41700:       val qt_asm = find_qt_asm (map term_of asms)
wenzelm@41700:     in
wenzelm@41700:       case (bare_concl, qt_asm) of
wenzelm@41700:         (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
wenzelm@41700:           if fastype_of qt_fun = fastype_of f
wenzelm@41700:           then no_tac
wenzelm@41700:           else
wenzelm@41700:             let
wenzelm@41700:               val ty_x = fastype_of x
wenzelm@41700:               val ty_b = fastype_of qt_arg
wenzelm@41700:               val ty_f = range_type (fastype_of f)
wenzelm@43232:               val thy = Proof_Context.theory_of context
wenzelm@41700:               val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
wenzelm@41700:               val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
wenzelm@41700:               val inst_thm = Drule.instantiate' ty_inst
wenzelm@41700:                 ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
wenzelm@41700:             in
wenzelm@41700:               (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
wenzelm@41700:             end
wenzelm@41700:       | _ => no_tac
wenzelm@41700:     end)
kaliszyk@35222: 
kaliszyk@35222: (* Instantiates and applies 'equals_rsp'. Since the theorem is
kaliszyk@35222:    complex we rely on instantiation to tell us if it applies
kaliszyk@35222: *)
kaliszyk@35222: fun equals_rsp_tac R ctxt =
wenzelm@41700:   let
wenzelm@43232:     val thy = Proof_Context.theory_of ctxt
wenzelm@41700:   in
wenzelm@41700:     case try (cterm_of thy) R of (* There can be loose bounds in R *)
wenzelm@41700:       SOME ctm =>
wenzelm@41700:         let
wenzelm@41700:           val ty = domain_type (fastype_of R)
wenzelm@41700:         in
wenzelm@41700:           case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
wenzelm@41700:               [SOME (cterm_of thy R)]) @{thm equals_rsp} of
wenzelm@41700:             SOME thm => rtac thm THEN' quotient_tac ctxt
wenzelm@41700:           | NONE => K no_tac
wenzelm@41700:         end
wenzelm@41700:     | _ => K no_tac
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: fun rep_abs_rsp_tac ctxt =
kaliszyk@35222:   SUBGOAL (fn (goal, i) =>
wenzelm@41700:     (case try bare_concl goal of
kaliszyk@35843:       SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
kaliszyk@35843:     | SOME (rel $ _ $ (rep $ (abs $ _))) =>
kaliszyk@35222:         let
wenzelm@43232:           val thy = Proof_Context.theory_of ctxt;
wenzelm@41089:           val (ty_a, ty_b) = dest_funT (fastype_of abs);
kaliszyk@35222:           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
kaliszyk@35222:         in
kaliszyk@35222:           case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
kaliszyk@35222:             SOME t_inst =>
kaliszyk@35222:               (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
kaliszyk@35222:                 SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
kaliszyk@35222:               | NONE => no_tac)
kaliszyk@35222:           | NONE => no_tac
kaliszyk@35222:         end
wenzelm@41700:     | _ => no_tac))
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
urbanc@38955: (* Injection means to prove that the regularized theorem implies
kaliszyk@35222:    the abs/rep injected one.
kaliszyk@35222: 
kaliszyk@35222:    The deterministic part:
kaliszyk@35222:     - remove lambdas from both sides
kaliszyk@35222:     - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
urbanc@38541:     - prove Ball/Bex relations using fun_relI
kaliszyk@35222:     - reflexivity of equality
kaliszyk@35222:     - prove equality of relations using equals_rsp
kaliszyk@35222:     - use user-supplied RSP theorems
kaliszyk@35222:     - solve 'relation of relations' goals using quot_rel_rsp
kaliszyk@35222:     - remove rep_abs from the right side
kaliszyk@35222:       (Lambdas under respects may have left us some assumptions)
kaliszyk@35222: 
kaliszyk@35222:    Then in order:
kaliszyk@35222:     - split applications of lifted type (apply_rsp)
kaliszyk@35222:     - split applications of non-lifted type (cong_tac)
kaliszyk@35222:     - apply extentionality
kaliszyk@35222:     - assumption
kaliszyk@35222:     - reflexivity of the relation
kaliszyk@35222: *)
kaliszyk@35222: fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
wenzelm@41700:   (case bare_concl goal of
wenzelm@41700:       (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
wenzelm@41700:     (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
wenzelm@41700:         => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
kaliszyk@35222: 
wenzelm@41700:       (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
wenzelm@41700:   | (Const (@{const_name HOL.eq},_) $
wenzelm@41700:       (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41700:       (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
wenzelm@41700:         => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
kaliszyk@35222: 
wenzelm@41700:       (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
wenzelm@41700:   | (Const (@{const_name fun_rel}, _) $ _ $ _) $
wenzelm@41700:       (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41700:       (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
wenzelm@41700:         => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
kaliszyk@35222: 
wenzelm@41700:       (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
wenzelm@41700:   | Const (@{const_name HOL.eq},_) $
wenzelm@41700:       (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41700:       (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
wenzelm@41700:         => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
kaliszyk@35222: 
wenzelm@41700:       (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
wenzelm@41700:   | (Const (@{const_name fun_rel}, _) $ _ $ _) $
wenzelm@41700:       (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41700:       (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
wenzelm@41700:         => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
kaliszyk@35222: 
wenzelm@41700:   | (Const (@{const_name fun_rel}, _) $ _ $ _) $
wenzelm@41700:       (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
wenzelm@41700:         => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
kaliszyk@35222: 
wenzelm@41700:   | (_ $
wenzelm@41700:       (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
wenzelm@41700:       (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
wenzelm@41700:         => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
kaliszyk@35222: 
wenzelm@41700:   | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
wenzelm@41700:      (rtac @{thm refl} ORELSE'
wenzelm@41700:       (equals_rsp_tac R ctxt THEN' RANGE [
wenzelm@41700:          quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
kaliszyk@35222: 
wenzelm@41700:       (* reflexivity of operators arising from Cong_tac *)
wenzelm@41700:   | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
kaliszyk@35222: 
wenzelm@41700:      (* respectfulness of constants; in particular of a simple relation *)
wenzelm@41700:   | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
wenzelm@41707:       => resolve_tac (Quotient_Info.rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
kaliszyk@35222: 
wenzelm@41700:       (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
wenzelm@41700:       (* observe map_fun *)
wenzelm@41700:   | _ $ _ $ _
wenzelm@41700:       => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
wenzelm@41700:          ORELSE' rep_abs_rsp_tac ctxt
kaliszyk@35222: 
wenzelm@41700:   | _ => K no_tac) i)
kaliszyk@35222: 
kaliszyk@35222: fun injection_step_tac ctxt rel_refl =
wenzelm@41700:   FIRST' [
kaliszyk@35222:     injection_match_tac ctxt,
kaliszyk@35222: 
kaliszyk@35222:     (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
kaliszyk@35222:     apply_rsp_tac ctxt THEN'
kaliszyk@35222:                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
kaliszyk@35222: 
kaliszyk@35222:     (* (op =) (t $ ...) (t' $ ...) ----> Cong   provided type of t does not need lifting *)
kaliszyk@35222:     (* merge with previous tactic *)
kaliszyk@35222:     Cong_Tac.cong_tac @{thm cong} THEN'
kaliszyk@35222:                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
kaliszyk@35222: 
kaliszyk@35222:     (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
kaliszyk@35222:     rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
kaliszyk@35222: 
kaliszyk@35222:     (* resolving with R x y assumptions *)
kaliszyk@35222:     atac,
kaliszyk@35222: 
kaliszyk@35222:     (* reflexivity of the basic relations *)
kaliszyk@35222:     (* R ... ... *)
kaliszyk@35222:     resolve_tac rel_refl]
kaliszyk@35222: 
kaliszyk@35222: fun injection_tac ctxt =
wenzelm@41700:   let
wenzelm@41700:     val rel_refl = reflp_get ctxt
wenzelm@41700:   in
wenzelm@41700:     injection_step_tac ctxt rel_refl
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: fun all_injection_tac ctxt =
kaliszyk@35222:   REPEAT_ALL_NEW (injection_tac ctxt)
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (*** Cleaning of the Theorem ***)
kaliszyk@35222: 
haftmann@40850: (* expands all map_funs, except in front of the (bound) variables listed in xs *)
haftmann@40850: fun map_fun_simple_conv xs ctrm =
wenzelm@41700:   (case term_of ctrm of
haftmann@40850:     ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
kaliszyk@35222:         if member (op=) xs h
kaliszyk@35222:         then Conv.all_conv ctrm
haftmann@40850:         else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
wenzelm@41700:   | _ => Conv.all_conv ctrm)
kaliszyk@35222: 
haftmann@40850: fun map_fun_conv xs ctxt ctrm =
wenzelm@41700:   (case term_of ctrm of
wenzelm@41700:     _ $ _ =>
wenzelm@41700:       (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
wenzelm@41700:         map_fun_simple_conv xs) ctrm
wenzelm@41700:   | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
wenzelm@41700:   | _ => Conv.all_conv ctrm)
kaliszyk@35222: 
haftmann@40850: fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
kaliszyk@35222: 
kaliszyk@35222: (* custom matching functions *)
kaliszyk@35222: fun mk_abs u i t =
wenzelm@41700:   if incr_boundvars i u aconv t then Bound i
wenzelm@41700:   else
wenzelm@41700:     case t of
wenzelm@41700:       t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
wenzelm@41700:     | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
wenzelm@41700:     | Bound j => if i = j then error "make_inst" else t
wenzelm@41700:     | _ => t
kaliszyk@35222: 
kaliszyk@35222: fun make_inst lhs t =
wenzelm@41700:   let
wenzelm@41700:     val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
wenzelm@41700:     val _ $ (Abs (_, _, (_ $ g))) = t;
wenzelm@41700:   in
wenzelm@41700:     (f, Abs ("x", T, mk_abs u 0 g))
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: fun make_inst_id lhs t =
wenzelm@41700:   let
wenzelm@41700:     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
wenzelm@41700:     val _ $ (Abs (_, _, g)) = t;
wenzelm@41700:   in
wenzelm@41700:     (f, Abs ("x", T, mk_abs u 0 g))
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: (* Simplifies a redex using the 'lambda_prs' theorem.
kaliszyk@35222:    First instantiates the types and known subterms.
kaliszyk@35222:    Then solves the quotient assumptions to get Rep2 and Abs1
kaliszyk@35222:    Finally instantiates the function f using make_inst
kaliszyk@35222:    If Rep2 is an identity then the pattern is simpler and
kaliszyk@35222:    make_inst_id is used
kaliszyk@35222: *)
kaliszyk@35222: fun lambda_prs_simple_conv ctxt ctrm =
wenzelm@41700:   (case term_of ctrm of
haftmann@40850:     (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
kaliszyk@35222:       let
wenzelm@43232:         val thy = Proof_Context.theory_of ctxt
wenzelm@41089:         val (ty_b, ty_a) = dest_funT (fastype_of r1)
wenzelm@41089:         val (ty_c, ty_d) = dest_funT (fastype_of a2)
kaliszyk@35222:         val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
kaliszyk@35222:         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
kaliszyk@35222:         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
kaliszyk@35222:         val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
wenzelm@41494:         val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
kaliszyk@35222:         val (insp, inst) =
kaliszyk@35222:           if ty_c = ty_d
kaliszyk@35222:           then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
kaliszyk@35222:           else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm)
wenzelm@44215:         val thm4 = Drule.instantiate_normalize ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3
kaliszyk@35222:       in
kaliszyk@35222:         Conv.rewr_conv thm4 ctrm
kaliszyk@35222:       end
wenzelm@41700:   | _ => Conv.all_conv ctrm)
kaliszyk@35222: 
wenzelm@36938: fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
kaliszyk@35222: fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (* Cleaning consists of:
kaliszyk@35222: 
kaliszyk@35222:   1. unfolding of ---> in front of everything, except
kaliszyk@35222:      bound variables (this prevents lambda_prs from
kaliszyk@35222:      becoming stuck)
kaliszyk@35222: 
kaliszyk@35222:   2. simplification with lambda_prs
kaliszyk@35222: 
kaliszyk@35222:   3. simplification with:
kaliszyk@35222: 
kaliszyk@35222:       - Quotient_abs_rep Quotient_rel_rep
kaliszyk@35222:         babs_prs all_prs ex_prs ex1_prs
kaliszyk@35222: 
kaliszyk@35222:       - id_simps and preservation lemmas and
kaliszyk@35222: 
kaliszyk@35222:       - symmetric versions of the definitions
kaliszyk@35222:         (that is definitions of quotient constants
kaliszyk@35222:          are folded)
kaliszyk@35222: 
kaliszyk@35222:   4. test for refl
kaliszyk@35222: *)
kaliszyk@35222: fun clean_tac lthy =
wenzelm@41700:   let
wenzelm@41707:     val defs = map (Thm.symmetric o #def) (Quotient_Info.qconsts_dest lthy)
wenzelm@41707:     val prs = Quotient_Info.prs_rules_get lthy
wenzelm@41707:     val ids = Quotient_Info.id_simps_get lthy
wenzelm@41700:     val thms =
wenzelm@41700:       @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
kaliszyk@35222: 
wenzelm@41700:     val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
wenzelm@41700:   in
wenzelm@41707:     EVERY' [
wenzelm@41707:       map_fun_tac lthy,
wenzelm@41707:       lambda_prs_tac lthy,
wenzelm@41707:       simp_tac ss,
wenzelm@41707:       TRY o rtac refl]
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: 
urbanc@38955: (* Tactic for Generalising Free Variables in a Goal *)
kaliszyk@35222: 
kaliszyk@35222: fun inst_spec ctrm =
wenzelm@41700:   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
kaliszyk@35222: 
kaliszyk@35222: fun inst_spec_tac ctrms =
kaliszyk@35222:   EVERY' (map (dtac o inst_spec) ctrms)
kaliszyk@35222: 
kaliszyk@35222: fun all_list xs trm =
kaliszyk@35222:   fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
kaliszyk@35222: 
kaliszyk@35222: fun apply_under_Trueprop f =
kaliszyk@35222:   HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
kaliszyk@35222: 
kaliszyk@35222: fun gen_frees_tac ctxt =
kaliszyk@35222:   SUBGOAL (fn (concl, i) =>
kaliszyk@35222:     let
wenzelm@43232:       val thy = Proof_Context.theory_of ctxt
kaliszyk@35222:       val vrs = Term.add_frees concl []
kaliszyk@35222:       val cvrs = map (cterm_of thy o Free) vrs
kaliszyk@35222:       val concl' = apply_under_Trueprop (all_list vrs) concl
kaliszyk@35222:       val goal = Logic.mk_implies (concl', concl)
kaliszyk@35222:       val rule = Goal.prove ctxt [] [] goal
kaliszyk@35222:         (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
kaliszyk@35222:     in
kaliszyk@35222:       rtac rule i
kaliszyk@35222:     end)
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (** The General Shape of the Lifting Procedure **)
kaliszyk@35222: 
kaliszyk@35222: (* - A is the original raw theorem
kaliszyk@35222:    - B is the regularized theorem
kaliszyk@35222:    - C is the rep/abs injected version of B
kaliszyk@35222:    - D is the lifted theorem
kaliszyk@35222: 
kaliszyk@35222:    - 1st prem is the regularization step
kaliszyk@35222:    - 2nd prem is the rep/abs injection step
kaliszyk@35222:    - 3rd prem is the cleaning part
kaliszyk@35222: 
kaliszyk@35222:    the Quot_True premise in 2nd records the lifted theorem
kaliszyk@35222: *)
kaliszyk@35222: val lifting_procedure_thm =
kaliszyk@35222:   @{lemma  "[|A;
kaliszyk@35222:               A --> B;
kaliszyk@35222:               Quot_True D ==> B = C;
kaliszyk@35222:               C = D|] ==> D"
kaliszyk@35222:       by (simp add: Quot_True_def)}
kaliszyk@35222: 
kaliszyk@35222: fun lift_match_error ctxt msg rtrm qtrm =
wenzelm@41700:   let
wenzelm@41700:     val rtrm_str = Syntax.string_of_term ctxt rtrm
wenzelm@41700:     val qtrm_str = Syntax.string_of_term ctxt qtrm
wenzelm@41700:     val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
wenzelm@41700:       "", "does not match with original theorem", rtrm_str]
wenzelm@41700:   in
wenzelm@41700:     error msg
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: fun procedure_inst ctxt rtrm qtrm =
wenzelm@41700:   let
wenzelm@43232:     val thy = Proof_Context.theory_of ctxt
wenzelm@41700:     val rtrm' = HOLogic.dest_Trueprop rtrm
wenzelm@41700:     val qtrm' = HOLogic.dest_Trueprop qtrm
wenzelm@41707:     val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
wenzelm@41707:       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
wenzelm@41707:     val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
wenzelm@41707:       handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
wenzelm@41700:   in
wenzelm@41700:     Drule.instantiate' []
wenzelm@41700:       [SOME (cterm_of thy rtrm'),
wenzelm@41700:        SOME (cterm_of thy reg_goal),
wenzelm@41700:        NONE,
wenzelm@41700:        SOME (cterm_of thy inj_goal)] lifting_procedure_thm
wenzelm@41700:   end
kaliszyk@35222: 
urbanc@37593: 
urbanc@39089: (* Since we use Ball and Bex during the lifting and descending,
kaliszyk@39091:    we cannot deal with lemmas containing them, unless we unfold
kaliszyk@39091:    them by default. *)
urbanc@39089: 
kaliszyk@39091: val default_unfolds = @{thms Ball_def Bex_def}
urbanc@39089: 
urbanc@39089: 
urbanc@37593: (** descending as tactic **)
urbanc@37593: 
urbanc@39088: fun descend_procedure_tac ctxt simps =
wenzelm@41700:   let
wenzelm@41700:     val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
wenzelm@41700:   in
wenzelm@41700:     full_simp_tac ss
wenzelm@41700:     THEN' Object_Logic.full_atomize_tac
wenzelm@41700:     THEN' gen_frees_tac ctxt
wenzelm@41700:     THEN' SUBGOAL (fn (goal, i) =>
wenzelm@41700:       let
wenzelm@41700:         val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
wenzelm@41707:         val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
wenzelm@41700:         val rule = procedure_inst ctxt rtrm  goal
wenzelm@41700:       in
wenzelm@41700:         rtac rule i
wenzelm@41700:       end)
wenzelm@41700:   end
kaliszyk@35222: 
urbanc@39088: fun descend_tac ctxt simps =
wenzelm@41700:   let
wenzelm@41700:     val mk_tac_raw =
wenzelm@41700:       descend_procedure_tac ctxt simps
wenzelm@41700:       THEN' RANGE
wenzelm@41700:         [Object_Logic.rulify_tac THEN' (K all_tac),
wenzelm@41700:          regularize_tac ctxt,
wenzelm@41700:          all_injection_tac ctxt,
wenzelm@41700:          clean_tac ctxt]
wenzelm@41700:   in
wenzelm@41700:     Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
wenzelm@41700:   end
kaliszyk@35222: 
urbanc@37593: 
urbanc@38848: (** lifting as a tactic **)
urbanc@37593: 
urbanc@38955: 
urbanc@37593: (* the tactic leaves three subgoals to be proved *)
urbanc@39088: fun lift_procedure_tac ctxt simps rthm =
wenzelm@41700:   let
wenzelm@41700:     val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
wenzelm@41700:   in
wenzelm@41700:     full_simp_tac ss
wenzelm@41700:     THEN' Object_Logic.full_atomize_tac
wenzelm@41700:     THEN' gen_frees_tac ctxt
wenzelm@41700:     THEN' SUBGOAL (fn (goal, i) =>
wenzelm@41700:       let
wenzelm@41700:         (* full_atomize_tac contracts eta redexes,
wenzelm@41700:            so we do it also in the original theorem *)
wenzelm@41700:         val rthm' =
wenzelm@41700:           rthm |> full_simplify ss
wenzelm@41700:                |> Drule.eta_contraction_rule
wenzelm@41700:                |> Thm.forall_intr_frees
wenzelm@41700:                |> atomize_thm
urbanc@38954: 
wenzelm@41700:         val rule = procedure_inst ctxt (prop_of rthm') goal
wenzelm@41700:       in
wenzelm@41700:         (rtac rule THEN' rtac rthm') i
wenzelm@41700:       end)
wenzelm@41700:   end
kaliszyk@35222: 
wenzelm@41700: fun lift_single_tac ctxt simps rthm =
urbanc@39088:   lift_procedure_tac ctxt simps rthm
urbanc@38848:   THEN' RANGE
urbanc@38848:     [ regularize_tac ctxt,
urbanc@38848:       all_injection_tac ctxt,
urbanc@38848:       clean_tac ctxt ]
urbanc@38848: 
urbanc@39088: fun lift_tac ctxt simps rthms =
wenzelm@41700:   Goal.conjunction_tac
urbanc@39088:   THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
kaliszyk@35222: 
urbanc@37593: 
urbanc@38848: (* automated lifting with pre-simplification of the theorems;
urbanc@38848:    for internal usage *)
urbanc@38848: fun lifted ctxt qtys simps rthm =
wenzelm@41700:   let
wenzelm@41700:     val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
wenzelm@41707:     val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm')
wenzelm@41700:   in
wenzelm@41700:     Goal.prove ctxt' [] [] goal
wenzelm@41700:       (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
wenzelm@43232:     |> singleton (Proof_Context.export ctxt' ctxt)
wenzelm@41700:   end
urbanc@38848: 
urbanc@38848: 
urbanc@38848: (* lifting as an attribute *)
kaliszyk@35222: 
wenzelm@41700: val lifted_attrib = Thm.rule_attribute (fn context =>
urbanc@37593:   let
urbanc@37593:     val ctxt = Context.proof_of context
urbanc@37593:     val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
urbanc@37593:   in
urbanc@38848:     lifted ctxt qtys []
urbanc@37593:   end)
kaliszyk@35222: 
kaliszyk@35222: end; (* structure *)