nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:243a5ceaa088
+:17ca92ab4660
 ball_reg_eqv_range and bex_reg_eqv_range
 Since the left-hand-side contains a non-pattern '?P (f ?x)'
 we rely on unification/instantiation to check whether the
 theorem applies and return NONE if it doesn't.
 *)
 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
 let
 val thy = ProofContext.theory_of ctxt
 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
 end
 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_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
 calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 | _ => NONE
 end
 4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
 to avoid loops
 5. then simplification like 0
 finally jump back to 1
 *)
 fun regularize_tac ctxt =
 let
 val thy = ProofContext.theory_of ctxt
 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
 val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
 val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (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 bex1_bexeq_reg},
 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 assumptions, 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
 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)
 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)))
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 (* We apply apply_rsp only in case if the type needs lifting.
 This 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)
 end
 | _ => no_tac
 end)
 (* Instantiates and applies 'equals_rsp'. Since the theorem is
 complex we rely on instantiation to tell us if it applies
 *)
 fun equals_rsp_tac R ctxt =
 let
 val thy = ProofContext.theory_of ctxt
 in
 end
 | _ => no_tac)
 (* Injection means to prove that the regularised theorem implies
 the abs/rep injected one.
 The deterministic part:
 - remove lambdas from both sides
 - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
 - prove equality of relations using equals_rsp
 - use user-supplied RSP theorems
 - solve 'relation of relations' goals using quot_rel_rsp
 - remove rep_abs from the right side
 (Lambdas under respects may have left us some assumptions)
 Then in order:
 - split applications of lifted type (apply_rsp)
 - split applications of non-lifted type (cong_tac)
 - apply extentionality
 - assumption
 | (_ $
 (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 *)
 => 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 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_def[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
 (* 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 an 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
 (* Cleaning consists of:
 1. unfolding of ---> in front of everything, except
 bound variables (this prevents lambda_prs from
 becoming stuck)
 2. simplification with lambda_prs
 3. simplification with:
 - Quotient_abs_rep Quotient_rel_rep
 babs_prs all_prs ex_prs ex1_prs
 - id_simps and preservation lemmas and
 - symmetric versions of the definitions
 (that is definitions of quotient constants
 are folded)
 4. test for refl
 *)
 fun clean_tac lthy =
 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
 - 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 2nd records the lifted theorem
 *)
 val lifting_procedure_thm =
 @{lemma  "[|A;
 A --> B;
 Quot_True D ==> B = C;
 fun lift_match_error ctxt msg 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 "[" "]" msg, "The quotient theorem", qtrm_str,
 "", "does not match with original theorem", rtrm_str]
 in
 error msg
 end
 (* Automatic Proofs *)
 val msg1 = "The regularize proof failed."
 val msg2 = cat_lines ["The 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 = "The cleaning proof failed."
 fun lift_tac ctxt rthms =
 let
 fun mk_tac rthm =
 procedure_tac ctxt rthm
 THEN' RANGE_WARN
 [(regularize_tac ctxt, msg1),
 (all_injection_tac ctxt, msg2),
 (clean_tac ctxt, msg3)]
 in
 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
 THEN' RANGE (map mk_tac rthms)
 end
 (* An Attribute which automatically constructs the qthm *)
 fun lifted_attrib_aux context thm =

changeset 1128	17ca92ab4660
parent 1120	42b623872781
child 1137	36d596cb63a2