More indenting, bracket removing and comment restructuring.
--- a/Quot/quotient_tacs.ML Tue Jan 12 16:44:33 2010 +0100
+++ b/Quot/quotient_tacs.ML Tue Jan 12 17:46:35 2010 +0100
@@ -1,13 +1,13 @@
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
+ 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 =
@@ -70,7 +70,8 @@
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
@@ -87,7 +88,7 @@
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
@@ -131,27 +132,22 @@
| _ => NONE
end
-(* 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-equalities, which need to be *)
-(* instantiated with the followig theorem *)
-(* to avoid loops: *)
-(* thm eq_imp_rel *)
-(* *)
-(* 5. then simplification like 0 *)
-(* *)
-(* finally jump back to 1 *)
+(*
+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)
+
+2. monos
+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
+
+5. then simplification like 0
+
+finally jump back to 1 *)
fun regularize_tac ctxt =
let
val thy = ProofContext.theory_of ctxt
@@ -384,7 +380,7 @@
FIRST' [
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)],
@@ -392,13 +388,13 @@
(* 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]
@@ -513,16 +509,16 @@
(* 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)
+ 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]
+ TRY o rtac refl]
end
@@ -543,18 +539,18 @@
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)
+ 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 **)
@@ -570,11 +566,11 @@
- 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;
- C = D|] ==> D"
+val lifting_procedure_thm =
+ @{lemma "[|A;
+ A --> B;
+ Quot_True D ==> B = C;
+ C = D|] ==> D"
by (simp add: Quot_True_def)}
fun lift_match_error ctxt str rtrm qtrm =
--- a/Quot/quotient_term.ML Tue Jan 12 16:44:33 2010 +0100
+++ b/Quot/quotient_term.ML Tue Jan 12 17:46:35 2010 +0100
@@ -1,20 +1,20 @@
signature QUOTIENT_TERM =
sig
- exception LIFT_MATCH of string
-
- datatype flag = absF | repF
-
- val absrep_fun: flag -> Proof.context -> (typ * typ) -> term
- val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term
+ exception LIFT_MATCH of string
+
+ datatype flag = absF | repF
+
+ val absrep_fun: flag -> Proof.context -> typ * typ -> term
+ val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
- val equiv_relation: Proof.context -> (typ * typ) -> term
- val equiv_relation_chk: Proof.context -> (typ * typ) -> term
+ val equiv_relation: Proof.context -> typ * typ -> term
+ val equiv_relation_chk: Proof.context -> typ * typ -> term
- val regularize_trm: Proof.context -> (term * term) -> term
- val regularize_trm_chk: Proof.context -> (term * term) -> term
-
- val inj_repabs_trm: Proof.context -> (term * term) -> term
- val inj_repabs_trm_chk: Proof.context -> (term * term) -> term
+ val regularize_trm: Proof.context -> term * term -> term
+ val regularize_trm_chk: Proof.context -> term * term -> term
+
+ val inj_repabs_trm: Proof.context -> term * term -> term
+ val inj_repabs_trm_chk: Proof.context -> term * term -> term
end;
structure Quotient_Term: QUOTIENT_TERM =
@@ -55,7 +55,7 @@
fun get_mapfun ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exc = LIFT_MATCH ("No map function for type " ^ (quote s) ^ " found.")
+ val exc = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exc
in
Const (mapfun, dummyT)
@@ -88,7 +88,7 @@
fun get_rty_qty ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.")
+ val exc = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
val qdata = (quotdata_lookup thy s) handle NotFound => raise exc
in
(#rtyp qdata, #qtyp qdata)
@@ -163,7 +163,7 @@
The matching is necessary for types like
- ('a * 'a) list / 'a bar *)
+ ('a * 'a) list / 'a bar *)
fun absrep_fun flag ctxt (rty, qty) =
if rty = qty
then mk_identity rty
@@ -267,7 +267,7 @@
end
(* builds the aggregate equivalence relation
- that will be the argument of Respects *)
+ that will be the argument of Respects *)
fun equiv_relation ctxt (rty, qty) =
if rty = qty
then HOLogic.eq_const rty
@@ -307,17 +307,17 @@
(*** Regularization ***)
(* Regularizing an rtrm means:
-
- - Quantifiers over types that need lifting are replaced
+
+ - Quantifiers over types that need lifting are replaced
by bounded quantifiers, for example:
All P ----> All (Respects R) P
where the aggregate relation R is given by the rty and qty;
-
+
- Abstractions over types that need lifting are replaced
by bounded abstractions, for example:
-
+
%x. P ----> Ball (Respects R) %x. P
- Equalities over types that need lifting are replaced by
@@ -325,14 +325,14 @@
A = B ----> R A B
- or
+ or
A = B ----> (R ===> R) A B
-
+
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)
@@ -348,16 +348,12 @@
| _ => f (trm1, trm2)
(* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)
+fun qnt_typ ty = domain_type (domain_type ty)
-(* produces a regularized version of rtrm *)
-(* *)
-(* - the result might contain dummyTs *)
-(* *)
-(* - for regularisation we do not need any *)
-(* special treatment of bound variables *)
-
+(* produces a regularized version of rtrm
+ - the result might contain dummyTs
+ - for regularisation we do not need to treat bound variables specially *)
fun regularize_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
(Abs (x, ty, t), Abs (_, ty', t')) =>
--- a/Quot/quotient_typ.ML Tue Jan 12 16:44:33 2010 +0100
+++ b/Quot/quotient_typ.ML Tue Jan 12 17:46:35 2010 +0100
@@ -218,7 +218,7 @@
val warns = map_check_aux rty []
in
if null warns then ()
- else warning ("No map function defined for " ^ (commas warns) ^
+ else warning ("No map function defined for " ^ commas warns ^
". This will cause problems later on.")
end
@@ -227,16 +227,16 @@
(*** interface and syntax setup ***)
-(* the ML-interface takes a list of 5-tuples consisting of
-
- - the name of the quotient type
- - its free type variables (first argument)
- - its mixfix annotation
- - the type to be quotient
- - the relation according to which the type is quotient
-
- it opens a proof-state in which one has to show that the
- relations are equivalence relations
+(* the ML-interface takes a list of 5-tuples consisting of:
+
+ - the name of the quotient type
+ - its free type variables (first argument)
+ - its mixfix annotation
+ - the type to be quotient
+ - the relation according to which the type is quotient
+
+ it opens a proof-state in which one has to show that the
+ relations are equivalence relations
*)
fun quotient_type quot_list lthy =