nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:017cb46b27bb
+:433f7c17255f
 signature QUOTIENT_TACS =
 sig
 val regularize_tac: Proof.context -> int -> tactic
 val injection_tac: Proof.context -> int -> tactic
 val all_injection_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
 val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
 end;
 structure Quotient_Tacs: QUOTIENT_TACS =
 struct
 open Quotient_Info;
 open Quotient_Term;
-(* various helper fuctions *)
+(** various helper fuctions **)
 (* 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
 in
 @{thm equal_elim_rule1} OF [thm'', thm']
 end
-(*********************)
-(* Regularize Tactic *)
+(*** Regularize Tactic ***)
-(*********************)
+(** solvers for equivp and quotient assumptions **)
-(* solvers for equivp and quotient assumptions *)
 (* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *)
 (* FIXME / TODO: none of te examples break if added                    *)
 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
 (* FIXME / TODO: test whether DETERM makes any runtime-difference *)
 (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *)
 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
+val quotient_solver =
+Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
 fun solve_quotient_assm ctxt thm =
 case Seq.pull (quotient_tac ctxt 1 thm) of
 SOME (t, _) => t
 | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
 fun get_match_inst thy pat trm =
 let
 val univ = Unify.matchers thy [(pat, trm)]
-val SOME (env, _) = Seq.pull univ                   (* raises BIND, if no unifier *)
+val SOME (env, _) = Seq.pull univ             (* raises BIND, if no unifier *)
 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
 calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 | _ => NONE
 end
-(* 0. preliminary simplification step according to *)
+(*
-(*    thm ball_reg_eqv bex_reg_eqv babs_reg_eqv    *)
+0. preliminary simplification step according to
-(*        ball_reg_eqv_range bex_reg_eqv_range     *)
+ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
-(*                                                 *)
-(* 1. eliminating simple Ball/Bex instances        *)
+1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
-(*    thm ball_reg_right bex_reg_left              *)
-(*                                                 *)
+2. monos
-(* 2. monos                                        *)
-(*                                                 *)
+3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
-(* 3. commutation rules for ball and bex           *)
-(*    thm ball_all_comm bex_ex_comm                *)
+4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
-(*                                                 *)
+to avoid loops
-(* 4. then rel-equalities, which need to be        *)
-(*    instantiated with the followig theorem       *)
+5. then simplification like 0
-(*    to avoid loops:                              *)
-(*    thm eq_imp_rel                               *)
+finally jump back to 1 *)
-(*                                                 *)
-(* 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} @ (id_simps_get 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'
 resolve_tac eq_eqvs,
 simp_tac simpset])
 end
-(********************)
-(* Injection Tactic *)
+(*** Injection Tactic ***)
-(********************)
+(* Looks for Quot_True assumtions, and in case its parameter
-(* Looks for Quot_True assumtions, and in case its parameter    *)
+is an application, it returns the function and the 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
 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.       *)
+(* 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        *)
+This is the case if the type of the data in the Quot_True
-(* assumption is different from the corresponding type in the goal. *)
+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}
+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)
 | _ => K no_tac
 end
 (* TODO: Again, can one specify more concretely        *)
 (* TODO: in terms of R when no_tac should be returned? *)
 fun rep_abs_rsp_tac ctxt =
 SUBGOAL (fn (goal, i) =>
-case (bare_concl goal) of
+case (try bare_concl goal) of
-(rel $ _ $ (rep $ (abs $ _))) =>
+SOME (rel $ _ $ (rep $ (abs $ _))) =>
-(let
+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];
+in
-val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
+case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
-in
+SOME t_inst =>
-(rtac inst_thm THEN' quotient_tac ctxt) i
+(case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
-end
+SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
-handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *)
+| NONE => no_tac)
+| NONE => no_tac
+end
 | _ => 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
+The deterministic part:
-2) remove lambdas from both sides: lambda_rsp_tac
+-) remove lambdas from both sides
-3) remove Ball/Bex from the right hand side
+-) prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
-4) use user-supplied RSP theorems
+-) prove Ball/Bex relations unfolding fun_rel_id
-5) remove rep_abs from the right side
+-) reflexivity of equality
-6) reflexivity of equality
+-) prove equality of relations using equals_rsp
-7) split applications of lifted type (apply_rsp)
+-) use user-supplied RSP theorems
-8) split applications of non-lifted type (cong_tac)
+-) solve 'relation of relations' goals using quot_rel_rsp
-9) apply extentionality
+-) remove rep_abs from the right side
-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
+Then in order:
-(not sure if it is still needed?)
+-) split applications of lifted type (apply_rsp)
-D) unfolding lambda on one side
+-) split applications of non-lifted type (cong_tac)
-E) simplifying (= ===> =) for simpler respectfulness
+-) apply extentionality
+-) assumption
+-) reflexivity of the relation
 *)
 fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
 (case (bare_concl goal) of
 fun injection_step_tac ctxt rel_refl =
 FIRST' [
 injection_match_tac 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 injection_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? *)
+injection_step_tac ctxt rel_refl
-THEN' injection_step_tac ctxt rel_refl
 end
 fun all_injection_tac ctxt =
 REPEAT_ALL_NEW (injection_tac ctxt)
-(***************************)
-(* Cleaning of the Theorem *)
+(** Cleaning of the Theorem **)
-(***************************)
+(* expands all fun_maps, except in front of the bound variables listed in xs *)
-(* expands all fun_maps, except in front of the bound *)
-(* variables listed in xs                             *)
 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 =
 val _ $ (Abs (_, _, g)) = t;
 in
 (f, Abs ("x", T, mk_abs u 0 g))
 end
-(* Simplifies a redex using the 'lambda_prs' theorem.        *)
+(* Simplifies a redex using the 'lambda_prs' theorem.
-(* First instantiates the types and known subterms.          *)
+First instantiates the types and known subterms.
-(* Then solves the quotient assumptions to get Rep2 and Abs1 *)
+Then solves the quotient assumptions to get Rep2 and Abs1
-(* Finally instantiates the function f using make_inst       *)
+Finally instantiates the function f using make_inst
-(* If Rep2 is an identity then the pattern is simpler and    *)
+If Rep2 is an identity then the pattern is simpler and
-(* make_inst_id is used                                      *)
+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
+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[THEN eq_reflection]}
 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
 val (insp, inst) =
 if ty_c = ty_d
 then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)
 else 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) (* TODO: another catch all - can this be improved? *)
 | _ => Conv.all_conv ctrm
 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
-(* 1. folding of definitions and preservation lemmas;  *)
+(* Cleaning consists of:
-(*    and simplification with                          *)
+1. folding of definitions and preservation lemmas;
-(*    thm babs_prs all_prs ex_prs                      *)
+and simplification with babs_prs all_prs ex_prs
-(*                                                     *)
-(* 2. unfolding of ---> in front of everything, except *)
+2. unfolding of ---> in front of everything, except
-(*    bound variables (this prevents lambda_prs from   *)
+bound variables
-(*    becoming stuck)                                  *)
+(this prevents lambda_prs from becoming stuck)
-(*    thm fun_map.simps                                *)
-(*                                                     *)
+3. simplification with lambda_prs
-(* 3. simplification with                              *)
-(*    thm lambda_prs                                   *)
+4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
-(*                                                     *)
-(* 4. simplification with                              *)
+5. test for refl *)
-(*    thm Quotient_abs_rep Quotient_rel_rep id_simps   *)
+fun clean_tac lthy =
-(*                                                     *)
-(* 5. test for refl                                    *)
-fun clean_tac_aux lthy =
 let
 (* FIXME/TODO produce defs with lthy, like prs and ids *)
 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 prs = prs_rules_get lthy
 val ids = id_simps_get lthy
 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs})
 val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids)
 in
 EVERY' [simp_tac ss1,
 fun_map_tac lthy,
 lambda_prs_tac lthy,
 simp_tac ss2,
 TRY o rtac refl]
 end
-fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)
+(** Tactic for Generalising Free Variables in a Goal **)
-(****************************************************)
-(* Tactic for Generalising 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 =
 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 *)
+(** The General Shape of the Lifting Procedure **)
-(**********************************************)
-(* - A is the original raw theorem                         *)
+(* - A is the original raw theorem
-(* - B is the regularized theorem                          *)
+- B is the regularized theorem
-(* - C is the rep/abs injected version of B                *)
+- C is the rep/abs injected version of B
-(* - D is the lifted theorem                               *)
+- D is the lifted theorem
-(*                                                         *)
-(* - 1st prem is the regularization step                   *)
+- 1st prem is the regularization step
-(* - 2nd prem is the rep/abs injection step                *)
+- 2nd prem is the rep/abs injection step
-(* - 3rd prem is the cleaning part                         *)
+- 3rd prem is the cleaning part
-(*                                                         *)
-(* the Quot_True premise in 2nd records the lifted theorem *)
+the Quot_True premise in 2nd records the lifted theorem *)
+val lifting_procedure_thm =
-val lifting_procedure_thm =
+@{lemma  "[|A;
-@{lemma  "[|A;
+A --> B;
-A --> B;
+Quot_True D ==> B = C;
-Quot_True D ==> B = C;
+C = D|] ==> D"
-C = D|] ==> D"
 by (simp add: Quot_True_def)}
 fun lift_match_error ctxt 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 "[" "]" 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 = regularize_trm_chk ctxt (rtrm', qtrm')
 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
 val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
 in
 Drule.instantiate' []
 [SOME (cterm_of thy rtrm'),
 SOME (cterm_of thy reg_goal),
 NONE,

changeset 856	433f7c17255f
parent 853	3fd1365f5729
child 857	0ce025c02ef3