# HG changeset patch # User wenzelm # Date 1386861455 -3600 # Node ID fc384e0a7f51240ed38b0cadb3ad0e66f585c041 # Parent b92694e756b807567888c4eb83b336a0c0b16b9d tuned whitespace; diff -r b92694e756b8 -r fc384e0a7f51 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu Dec 12 14:35:31 2013 +0100 +++ b/src/Pure/raw_simplifier.ML Thu Dec 12 16:17:35 2013 +0100 @@ -946,30 +946,33 @@ val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); val prop' = Thm.prop_of thm'; val unconditional = (Logic.count_prems prop' = 0); - val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop') + val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop'); in if perm andalso not (termless (rhs', lhs')) - then (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name); - trace_thm ctxt (fn () => "Term does not become smaller:") thm'; NONE) - else (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name); - if unconditional - then - (trace_thm ctxt (fn () => "Rewriting:") thm'; + then + (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name); + trace_thm ctxt (fn () => "Term does not become smaller:") thm'; + NONE) + else + (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name); + if unconditional + then + (trace_thm ctxt (fn () => "Rewriting:") thm'; + let + val lr = Logic.dest_equals prop; + val SOME thm'' = check_conv ctxt false eta_thm thm'; + in SOME (thm'', uncond_skel (congs, lr)) end) + else + (trace_thm ctxt (fn () => "Trying to rewrite:") thm'; + if simp_depth ctxt > Config.get ctxt simp_depth_limit + then let - val lr = Logic.dest_equals prop; - val SOME thm'' = check_conv ctxt false eta_thm thm'; - in SOME (thm'', uncond_skel (congs, lr)) end) - else - (trace_thm ctxt (fn () => "Trying to rewrite:") thm'; - if simp_depth ctxt > Config.get ctxt simp_depth_limit - then - let - val s = "simp_depth_limit exceeded - giving up"; - val _ = trace ctxt false (fn () => s); - val _ = Context_Position.if_visible ctxt warning s; - in NONE end - else - case prover ctxt thm' of + val s = "simp_depth_limit exceeded - giving up"; + val _ = trace ctxt false (fn () => s); + val _ = Context_Position.if_visible ctxt warning s; + in NONE end + else + (case prover ctxt thm' of NONE => (trace_thm ctxt (fn () => "FAILED") thm'; NONE) | SOME thm2 => (case check_conv ctxt true eta_thm thm2 of @@ -978,13 +981,13 @@ let val concl = Logic.strip_imp_concl prop; val lr = Logic.dest_equals concl; - in SOME (thm2', cond_skel (congs, lr)) end))) + in SOME (thm2', cond_skel (congs, lr)) end)))) end; fun rews [] = NONE | rews (rrule :: rrules) = let val opt = rew rrule handle Pattern.MATCH => NONE - in case opt of NONE => rews rrules | some => some end; + in (case opt of NONE => rews rrules | some => some) end; fun sort_rrules rrs = let @@ -1003,7 +1006,7 @@ | proc_rews (Proc {name, proc, lhs, ...} :: ps) = if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then (debug_term ctxt false (fn () => "Trying procedure " ^ quote name ^ " on:") eta_t; - case proc ctxt eta_t' of + (case proc ctxt eta_t' of NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps) | SOME raw_thm => (trace_thm ctxt (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:") @@ -1011,7 +1014,7 @@ (case rews (mk_procrule ctxt raw_thm) of NONE => (trace_cterm ctxt true (fn () => "IGNORED result of simproc " ^ quote name ^ " -- does not match") t; proc_rews ps) - | some => some))) + | some => some)))) else proc_rews ps; in (case eta_t of @@ -1052,7 +1055,7 @@ fun transitive1 NONE NONE = NONE | transitive1 (SOME thm1) NONE = SOME thm1 | transitive1 NONE (SOME thm2) = SOME thm2 - | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2) + | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2); fun transitive2 thm = transitive1 (SOME thm); fun transitive3 thm = transitive1 thm o SOME; @@ -1060,25 +1063,25 @@ fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) = let fun botc skel ctxt t = - if is_Var skel then NONE - else - (case subc skel ctxt t of - some as SOME thm1 => - (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of - SOME (thm2, skel2) => - transitive2 (Thm.transitive thm1 thm2) - (botc skel2 ctxt (Thm.rhs_of thm2)) - | NONE => some) - | NONE => - (case rewritec (prover, maxidx) ctxt t of - SOME (thm2, skel2) => transitive2 thm2 + if is_Var skel then NONE + else + (case subc skel ctxt t of + some as SOME thm1 => + (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of + SOME (thm2, skel2) => + transitive2 (Thm.transitive thm1 thm2) (botc skel2 ctxt (Thm.rhs_of thm2)) - | NONE => NONE)) + | NONE => some) + | NONE => + (case rewritec (prover, maxidx) ctxt t of + SOME (thm2, skel2) => transitive2 thm2 + (botc skel2 ctxt (Thm.rhs_of thm2)) + | NONE => NONE)) and try_botc ctxt t = - (case botc skel0 ctxt t of - SOME trec1 => trec1 - | NONE => (Thm.reflexive t)) + (case botc skel0 ctxt t of + SOME trec1 => trec1 + | NONE => Thm.reflexive t) and subc skel ctxt t0 = let val Simpset ({bounds, ...}, {congs, ...}) = simpset_of ctxt in @@ -1094,64 +1097,70 @@ quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ())) else (); val ctxt' = add_bound ((b', T), a) ctxt; - val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; + val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0); in (case botc skel' ctxt' t' of SOME thm => SOME (Thm.abstract_rule a v thm) | NONE => NONE) end - | t $ _ => (case t of + | t $ _ => + (case t of Const ("==>", _) $ _ => impc t0 ctxt | Abs _ => let val thm = Thm.beta_conversion false t0 - in case subc skel0 ctxt (Thm.rhs_of thm) of - NONE => SOME thm - | SOME thm' => SOME (Thm.transitive thm thm') + in + (case subc skel0 ctxt (Thm.rhs_of thm) of + NONE => SOME thm + | SOME thm' => SOME (Thm.transitive thm thm')) end | _ => let fun appc () = let - val (tskel, uskel) = case skel of + val (tskel, uskel) = + (case skel of tskel $ uskel => (tskel, uskel) - | _ => (skel0, skel0); - val (ct, cu) = Thm.dest_comb t0 + | _ => (skel0, skel0)); + val (ct, cu) = Thm.dest_comb t0; in - (case botc tskel ctxt ct of - SOME thm1 => - (case botc uskel ctxt cu of + (case botc tskel ctxt ct of + SOME thm1 => + (case botc uskel ctxt cu of SOME thm2 => SOME (Thm.combination thm1 thm2) | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu))) - | NONE => - (case botc uskel ctxt cu of + | NONE => + (case botc uskel ctxt cu of SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1) | NONE => NONE)) end - val (h, ts) = strip_comb t - in case cong_name h of - SOME a => - (case AList.lookup (op =) (fst congs) a of - NONE => appc () - | SOME cong => + val (h, ts) = strip_comb t; + in + (case cong_name h of + SOME a => + (case AList.lookup (op =) (fst congs) a of + NONE => appc () + | SOME cong => (*post processing: some partial applications h t1 ... tj, j <= length ts, may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) - (let - val thm = congc (prover ctxt) ctxt maxidx cong t0; - val t = the_default t0 (Option.map Thm.rhs_of thm); - val (cl, cr) = Thm.dest_comb t - val dVar = Var(("", 0), dummyT) - val skel = - list_comb (h, replicate (length ts) dVar) - in case botc skel ctxt cl of - NONE => thm - | SOME thm' => transitive3 thm - (Thm.combination thm' (Thm.reflexive cr)) - end handle Pattern.MATCH => appc ())) - | _ => appc () + (let + val thm = congc (prover ctxt) ctxt maxidx cong t0; + val t = the_default t0 (Option.map Thm.rhs_of thm); + val (cl, cr) = Thm.dest_comb t + val dVar = Var(("", 0), dummyT) + val skel = + list_comb (h, replicate (length ts) dVar) + in + (case botc skel ctxt cl of + NONE => thm + | SOME thm' => + transitive3 thm (Thm.combination thm' (Thm.reflexive cr))) + end handle Pattern.MATCH => appc ())) + | _ => appc ()) end) | _ => NONE) end and impc ct ctxt = - if mutsimp then mut_impc0 [] ct [] [] ctxt else nonmut_impc ct ctxt + if mutsimp then mut_impc0 [] ct [] [] ctxt + else nonmut_impc ct ctxt and rules_of_prem ctxt prem = if maxidx_of_term (term_of prem) <> ~1 @@ -1171,16 +1180,18 @@ val eq' = Thm.implies_elim (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) (Thm.implies_intr prem eq) - in if not r then eq' else - let - val (prem', concl) = Thm.dest_implies lhs; - val (prem'', _) = Thm.dest_implies rhs - in Thm.transitive (Thm.transitive - (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) - Drule.swap_prems_eq) eq') - (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) - Drule.swap_prems_eq) - end + in + if not r then eq' + else + let + val (prem', concl) = Thm.dest_implies lhs; + val (prem'', _) = Thm.dest_implies rhs + in Thm.transitive (Thm.transitive + (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) + Drule.swap_prems_eq) eq') + (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) + Drule.swap_prems_eq) + end end and rebuild [] _ _ _ _ eq = eq @@ -1218,27 +1229,29 @@ | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) prems' rrss' asms' eqns ctxt changed k = - case (if k = 0 then NONE else botc skel0 (add_rrules + (case (if k = 0 then NONE else botc skel0 (add_rrules (rev rrss' @ rrss, rev asms' @ asms) ctxt) prem) of NONE => mut_impc prems concl rrss asms (prem :: prems') (rrs :: rrss') (asm :: asms') (NONE :: eqns) ctxt changed (if k = 0 then 0 else k - 1) - | SOME eqn => + | SOME eqn => let val prem' = Thm.rhs_of eqn; val tprems = map term_of prems; val i = 1 + fold Integer.max (map (fn p => find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1; val (rrs', asm') = rules_of_prem ctxt prem'; - in mut_impc prems concl rrss asms (prem' :: prems') - (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true) - (take i prems) - (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies - (drop i prems, concl))))) :: eqns) - ctxt (length prems') ~1 - end + in + mut_impc prems concl rrss asms (prem' :: prems') + (rrs' :: rrss') (asm' :: asms') + (SOME (fold_rev (disch true) + (take i prems) + (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies + (drop i prems, concl))))) :: eqns) + ctxt (length prems') ~1 + end) - (*legacy code - only for backwards compatibility*) + (*legacy code -- only for backwards compatibility*) and nonmut_impc ct ctxt = let val (prem, conc) = Thm.dest_implies ct; @@ -1260,9 +1273,9 @@ | SOME thm1' => SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2')) end) - end + end; - in try_botc end; + in try_botc end; (* Meta-rewriting: rewrites t to u and returns the theorem t==u *)