nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:a95f6bb081cf
+:d6acae26d027
 signature QUOTIENT_TACS =
 sig
 val regularize_tac: Proof.context -> int -> tactic
-val all_inj_repabs_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 lift_tac: Proof.context -> thm -> int -> tactic
 val quotient_tac: Proof.context -> int -> tactic
 end;
 structure Quotient_Tacs: QUOTIENT_TACS =
 struct
 in
 @{thm equal_elim_rule1} OF [thm'', thm']
 end
+(*********************)
 (* Regularize Tactic *)
+(*********************)
+(* solvers for equivp and quotient assumptions *)
 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
+(* 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_assm ctxt thm =
+case Seq.pull (quotient_tac ctxt 1 thm) of
+SOME (t, _) => t
+| _ => error "solve_quotient_assm failed. Maybe a quotient_thm is missing"
 fun prep_trm thy (x, (T, t)) =
 (cterm_of thy (Var (x, T)), cterm_of thy t)
 fun prep_ty thy (x, (S, ty)) =
 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 end
 (* calculates the instantiations for te lemmas *)
 (* ball_reg_eqv_range and bex_reg_eqv_range    *)
-fun calculate_instance ctxt ball_bex_thm redex R1 R2 =
+fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
 let
 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
 val thy = ProofContext.theory_of ctxt
 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
 val trm_inst1 = map (SOME o cterm_of thy) [R2, R1]
 (* FIXME/TODO: What is the place where the exception is raised,  *)
 (* FIXME/TODO: and which exception is it?                        *)
 (* FIXME/TODO: Can one not find out from the types of R1 or R2,  *)
 (* FIXME/TODO: or from their form, when NONE should be returned? *)
 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[THEN eq_reflection]} redex 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_instance ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
+calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} 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_assm ctxt thm =
-case Seq.pull (quotient_tac ctxt 1 thm) of
-SOME (t, _) => t
-| _ => error "solve_quotient_assm 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          *)
+(* 4. then rel-equalities, which need to be        *)
-(*    instantiated to avoid loops)                 *)
+(*    instantiated with the followig theorem       *)
+(*    to avoid loops:                              *)
 (*    thm eq_imp_rel                               *)
 (*                                                 *)
 (* 5. then simplification like 0                   *)
 (*                                                 *)
 (* finally jump back to 1                          *)
 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' [
+REPEAT_ALL_NEW (CHANGED o FIRST'
-resolve_tac @{thms ball_reg_right bex_reg_left},
+[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 *)
+(* 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
+(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) =>
+(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}
+val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_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}, _) $ _) =>
+(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
 | 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.      *)
-(* which 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 *)
 val apply_rsp_tac =
 Subgoal.FOCUS (fn {concl, asms, context,...} =>
 let
 val bare_concl = HOLogic.dest_Trueprop (term_of concl)
 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' *)
+(* Are they raised by instantiate'? *)
 handle THM _  => K no_tac
 | TYPE _ => K no_tac
 | TERM _ => K no_tac
 D) unfolding lambda on one side
 E) simplifying (= ===> =) for simpler respectfulness
 *)
-fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
+fun injection_match_tac 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
 ORELSE' rep_abs_rsp_tac ctxt
 | _ => K no_tac
 ) i)
-fun inj_repabs_step_tac ctxt rel_refl =
+fun injection_step_tac ctxt rel_refl =
 FIRST' [
-inj_repabs_tac_match ctxt,
+injection_match_tac ctxt,
-(* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
+(* 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 *)
 (* reflexivity of the basic relations *)
 (* R ... ... *)
 resolve_tac rel_refl]
-fun inj_repabs_tac ctxt =
+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? *)
-THEN' inj_repabs_step_tac ctxt rel_refl
+THEN' injection_step_tac ctxt rel_refl
 end
-fun all_inj_repabs_tac ctxt =
+fun all_injection_tac ctxt =
-REPEAT_ALL_NEW (inj_repabs_tac ctxt)
+REPEAT_ALL_NEW (injection_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 $ _) =>
 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_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;  *)
 (*    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                                   *)
+(*    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                                    *)
+(* 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)
 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 =
 (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 *)
+(* the Quot_True premise in 2 records the lifted theorem *)
 val lifting_procedure =
 @{lemma  "[|A;
 A --> B;
-QUOT_TRUE D ==> B = C;
+Quot_True D ==> B = C;
 C = D|] ==> D"
-by (simp add: QUOT_TRUE_def)}
+by (simp add: Quot_True_def)}
-fun lift_match_error ctxt fun_str rtrm qtrm =
+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 "[" "]" fun_str, "The quotient theorem", qtrm_str,
+val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str,
 "", "does not match with original theorem", rtrm_str]
 in
 error msg
 end
 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
+handle (LIFT_MATCH str) => lift_match_error ctxt str 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
+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,
 fun lift_tac ctxt rthm =
 procedure_tac ctxt rthm
 THEN' RANGE_WARN
 [(regularize_tac ctxt, msg1),
-(all_inj_repabs_tac ctxt, msg2),
+(all_injection_tac ctxt, msg2),
 (clean_tac ctxt, msg3)]
 end; (* structure *)

changeset 773	d6acae26d027
parent 772	a95f6bb081cf
child 774	b4ffb8826105