# HG changeset patch # User Cezary Kaliszyk # Date 1263314795 -3600 # Node ID 3fd1365f57295c58b66603a72799dc7fad3d9fea # Parent 67e5da3a356a752f364bda802145a5ba85c8046a More indenting, bracket removing and comment restructuring. diff -r 67e5da3a356a -r 3fd1365f5729 Quot/quotient_tacs.ML --- 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 = diff -r 67e5da3a356a -r 3fd1365f5729 Quot/quotient_term.ML --- 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')) => diff -r 67e5da3a356a -r 3fd1365f5729 Quot/quotient_typ.ML --- 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 =