--- a/Quot/quotient_def.ML Wed Jan 13 09:30:59 2010 +0100
+++ b/Quot/quotient_def.ML Wed Jan 13 09:41:57 2010 +0100
@@ -28,14 +28,14 @@
(* the ML-interface takes
- - the mixfix annotation
- - name and attributes
- - the new constant as term
- - the rhs of the definition as term
+ - the mixfix annotation
+ - name and attributes
+ - the new constant as term
+ - the rhs of the definition as term
- it returns the defined constant and its definition
- theorem; stores the data in the qconsts slot *)
-
+ it returns the defined constant and its definition
+ theorem; stores the data in the qconsts slot
+*)
fun quotient_def mx attr lhs rhs lthy =
let
val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
--- a/Quot/quotient_tacs.ML Wed Jan 13 09:30:59 2010 +0100
+++ b/Quot/quotient_tacs.ML Wed Jan 13 09:41:57 2010 +0100
@@ -97,10 +97,13 @@
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))
@@ -108,13 +111,12 @@
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 =
@@ -133,22 +135,24 @@
| _ => NONE
end
-(*
-0. preliminary simplification step according to
- ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
+(* Regularize works as follows:
-1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
+ 0. preliminary simplification step according to
+ ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
-2. monos
+ 1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
+
+ 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
@@ -175,7 +179,8 @@
(*** 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 =
@@ -231,7 +236,8 @@
(* 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
@@ -259,7 +265,8 @@
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
@@ -298,29 +305,28 @@
| _ => no_tac)
-(*
-To prove that the regularised theorem implies the abs/rep injected,
-we try:
+
+(* 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 Ball/Bex relations unfolding fun_rel_id
- -) reflexivity of equality
- -) 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
- -) reflexivity of the relation
+ The deterministic part:
+ - remove lambdas from both sides
+ - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
+ - prove Ball/Bex relations unfolding fun_rel_id
+ - reflexivity of equality
+ - 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
+ - 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) *)
@@ -412,7 +418,7 @@
-(** 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 =
@@ -462,7 +468,8 @@
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 _) =>
@@ -490,18 +497,20 @@
(* 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
- (this prevents lambda_prs from becoming stuck)
+ 2. unfolding of ---> in front of everything, except
+ 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 *)
@@ -526,7 +535,6 @@
(** Tactic for Generalising Free Variables in a Goal **)
-
fun inst_spec ctrm =
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
@@ -556,17 +564,17 @@
(** 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
+ - 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
+ - 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;
--- a/Quot/quotient_term.ML Wed Jan 13 09:30:59 2010 +0100
+++ b/Quot/quotient_term.ML Wed Jan 13 09:41:57 2010 +0100
@@ -175,7 +175,7 @@
('a * 'a) list / 'a bar
- The test is necessary in order to eliminate superflous
+ The test is necessary in order to eliminate superfluous
identity maps.
*)
@@ -358,7 +358,6 @@
for more complicated types of A and B
*)
-
val mk_babs = Const (@{const_name Babs}, dummyT)
val mk_ball = Const (@{const_name Ball}, dummyT)
val mk_bex = Const (@{const_name Bex}, dummyT)