nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:0ce025c02ef3
+:bb012513fb39
 in
 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 end
 (* Calculates the instantiations for the lemmas:
 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. *)
+theorem applies and return NONE if it doesn't.
+*)
 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]
 in
-(case try (Drule.instantiate' typ_inst1 trm_inst1) ball_bex_thm of
+case try (Drule.instantiate' typ_inst1 trm_inst1) ball_bex_thm of
 NONE => NONE
 | SOME thm' =>
 (case try (get_match_inst thy (get_lhs thm')) redex of
 NONE => NONE
 | SOME inst2 => try (Drule.instantiate inst2) thm')
-)
 end
 fun ball_bex_range_simproc ss redex =
 let
 val ctxt = Simplifier.the_context ss
 calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 | _ => NONE
 end
-(*
+(* Regularize works as follows:
-0. preliminary simplification step according to
-ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
+0. preliminary simplification step according to
+ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
-1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
+1. eliminating simple Ball/Bex instances (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 (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 'eq_imp_rel'
+to avoid loops
-5. then simplification like 0
+5. then simplification like 0
-finally jump back to 1 *)
+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"}
 (*** Injection Tactic ***)
 (* 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
 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. *)
+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)
 end
 | _ => no_tac
 end)
 (* Instantiates and applies 'equals_rsp'. Since the theorem is
-complex we rely on instantiation to tell us if it applies *)
+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
 case try (cterm_of thy) R of (* There can be loose bounds in R *)
 | NONE => no_tac
 end
 | _ => no_tac)
-(*
-To prove that the regularised theorem implies the abs/rep injected,
+(* Injection means to prove that the regularised theorem implies
-we try:
+the abs/rep injected one.
 The deterministic part:
--) remove lambdas from both sides
+- remove lambdas from both sides
--) prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
+- prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
--) prove Ball/Bex relations unfolding fun_rel_id
+- prove Ball/Bex relations unfolding fun_rel_id
--) reflexivity of equality
+- reflexivity of equality
--) prove equality of relations using equals_rsp
+- prove equality of relations using equals_rsp
--) use user-supplied RSP theorems
+- use user-supplied RSP theorems
--) solve 'relation of relations' goals using quot_rel_rsp
+- solve 'relation of relations' goals using quot_rel_rsp
--) remove rep_abs from the right side
+- 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)
+Then in order:
--) split applications of non-lifted type (cong_tac)
+- split applications of lifted type (apply_rsp)
--) apply extentionality
+- split applications of non-lifted type (cong_tac)
--) assumption
+- apply extentionality
--) reflexivity of the relation
+- assumption
-*)
+- reflexivity of the relation
+*)
 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
 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 *)
 fun fun_map_simple_conv xs ctrm =
 case (term_of ctrm) of
 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
 (* 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 *)
+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
 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 (* Cleaning consists of:
-1. folding of definitions and preservation lemmas;
-and simplification with babs_prs all_prs ex_prs
+1. folding of definitions and preservation lemmas;
+and simplification with babs_prs all_prs ex_prs
-2. unfolding of ---> in front of everything, except
-bound variables
+2. unfolding of ---> in front of everything, except
-(this prevents lambda_prs from becoming stuck)
+bound variables
+(this prevents lambda_prs from becoming stuck)
-3. simplification with lambda_prs
+3. simplification with lambda_prs
-4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
+4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
-5. test for refl *)
+5. test for refl
+*)
 fun clean_tac 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)
 end
 (** 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 =
 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 2nd records the lifted theorem *)
+the Quot_True premise in 2nd records the lifted theorem
+*)
 val lifting_procedure_thm =
 @{lemma  "[|A;
 A --> B;
 Quot_True D ==> B = C;
 C = D|] ==> D"

changeset 858	bb012513fb39
parent 857	0ce025c02ef3
child 860	e18c691335db