summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 11 Feb 2001 16:34:20 +0100 | |

changeset 11097 | c1be9f2dff4c |

parent 11096 | bedfd42db838 |

child 11098 | a3299b153741 |

more robust selection of calculational rules;

NEWS | file | annotate | diff | comparison | revisions | |

src/Pure/Isar/calculation.ML | file | annotate | diff | comparison | revisions |

--- a/NEWS Sun Feb 11 16:31:54 2001 +0100 +++ b/NEWS Sun Feb 11 16:34:20 2001 +0100 @@ -90,6 +90,8 @@ * Pure: ?thesis / ?this / "..." now work for pure meta-level statements as well; +* Pure: more robust selection of calculational rules; + * Pure: the builtin notion of 'finished' goal now includes the ==-refl rule (as well as the assumption rule);

--- a/src/Pure/Isar/calculation.ML Sun Feb 11 16:31:54 2001 +0100 +++ b/src/Pure/Isar/calculation.ML Sun Feb 11 16:34:20 2001 +0100 @@ -123,26 +123,23 @@ fun calculate final opt_rules print state = let - val facts = Proof.the_facts (Proof.assert_forward state); - val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm; val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl); - fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms')); + fun projection ths th = Library.exists (Library.curry eq_prop th) ths; - fun combine thms = - let - val ths = thms @ facts; - val rs = get_local_rules state; - val rules = - (case ths of [] => NetRules.rules rs - | th :: _ => NetRules.may_unify rs (strip_assums_concl th)); - val ruleq = Seq.of_list (if_none opt_rules [] @ rules); - in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end; + fun combine ths = + (case opt_rules of Some rules => rules + | None => + (case ths of [] => NetRules.rules (get_local_rules state) + | th :: _ => NetRules.may_unify (get_local_rules state) (strip_assums_concl th))) + |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat + |> Seq.filter (not o projection ths); + val facts = Proof.the_facts (Proof.assert_forward state); val (initial, calculations) = (case get_calculation state of None => (true, Seq.single facts) - | Some thms => (false, Seq.filter (differ thms) (combine thms))) + | Some calc => (false, Seq.map single (combine (calc @ facts)))); in err_if state (initial andalso final) "No calculation yet"; err_if state (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";