--- 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 *)