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 =