IsaPlanner Developer News

Lucas Dixon - 13 Sep 2007

Many small fixes, including fixed bug in InstEnv: we now certify terms at the right time and instantiate any new given terms.
moved to subversion.

Lucas Dixon - 17 June 2007

Lucas Dixon - 12 March 2007

added quickqueck technique, and contextual infor for counter-examples.
added techinque combining safe, auto and quickcheck for automating simple problems.
added dbg/auto_counter_example.ML for batch mode use of auto+quickcheck.
fixed small bugs in dtacs
added unsafe apply tactic tool for proof plans (does not respect meta-vars) in order to allow auto to be applied using assumptions. Will have to figure out later how to do this properly.

Lucas Dixon - 11 March 2007

restructured - dtacs now in rtechn directory
dtacs are now for operations of the proof plan, not just for isabelle operations. They represent atomic techniques.
atomic techniques now largely rewritten.
gtacs for goalname based tactics written. These combone operations of the proof plan. They include names for results derived in a forward manner as well as goal names derived backwards. Gives great flexibility for combination.

Lucas Dixon - 10 March 2007

Lucas Dixon - 13 Feb 2007

Prf variable table merge bug fixed/hidden: we don't expect variable tables to have correct upto-date types. See the ToDo list.
Subst bug killed: it was accidentally throwing away binders under the subst.

Lucas Dixon - 8 Feb 2007

Lucas Dixon - 16 Jan 2007

many small fixes and additions including top level api for using theorems in proof plan, basic techniques to apply these, fixes to printing of proof plans.
Basic Lemma conjecturing functionality added - we now make conjectures and use them. Still need to add all the search space pruning tricks.

Moa Johansson - 11 November 2006

Properly integrated splitting if-statements and rippling. This is now done directly after an if-statement has be introduced by rippling.
Made a change in how the induction technique decides which goals are base/step cases, previously everything that has an assumption after induction was assumed to be step-cases. This meant that we couldn't do induction on goals with previous assumption. Fixed by checking if we have new assumptions after induction.
Also changed the base-case technique to let it use assumptions to simplify the base-case (won't work with ordinary simp anymore as assumptions are stored separate from conclusion in the new environment, and you don't get a theorem with the associated assumptions out when applying a dtac). (Although I just noticed this doesn't work properly - strange bug make IsaPlanner refuse to use assumption to simplify base-case in some situation...will investigate)

Lucas Dixon - 8 November 2006

Substitution in the underlying proof environment is now supported and many bugs have been fixed.

Moa Johansson - 1 November 2006

Change the wrule database so it no longer allows rewriting 'True' or 'False' to something like 'even(0)' (obviously this was only an issue for bf-rippling).
Fixed lots of bugs in case-splitting for if-statements and integrated it with rippling. Will play around with when exactlycase-splitting is applied.

Lucas Dixon - 26 October 2006

Many changes in the last few weeks: Updated internal proof representation; rewrote pretty printing for internal proof representation, provided a notion of compound proof method native to the internal proof representation; explicit lifting of things internally; added some and all statements for goals in the reasoning techniques; rewrote contextual information for rippling.

Moa Johansson - 17 October 2006

Committed new code for case-splits of if-statements. There is now a reasoning technique that tries to prove the condition of an if-statement (by applying an assumtion) to decide which branch to go down. If we can't decide it introduces a case-split. Next to do is integrating this with rippling.

Moa Johansson - 6 October 2006

Made Best-First Rippling typecheck again (excluding conjecturing). Appears to work, but not tested on that many things yet.

Lucas Dixon - 18 September 2006

Fixed bug in InstEnv unification that was incorrectly putting all instantiations into the pattern environment. This resultied in adding an extra argument to unification: the variables used by the target as well as the variables of both pattern and target.

Lucas Dixon - 13 September 2006

Lucas Dixon - 11 September 2006

Assumptions now give back vars that were under meta level quantifiers as fresh vars.
Embedding now requires vars in the target to match against some var in the skeleton.

Lucas Dixon - 5 September 2006

Rewrote trace structure the add_then and add_refine functions now take an int*rst, and add them correctly to the trace even when it is empty.
Bugfix: changed dtac rtechn functions to name what they do and set the continuation to empty. Previously they didn't do this. May still need more looking at.

Moa Johansson - 5 September 2006

Changed the type of RTechnEnv.map_then. It now takes a function goalname -> reasoning-technique. This makes writing techniques that work on exactly one goal more elegant.
Fixed bug: In rippling, when updating the reasoning state was given the wrong name (of the previous state) because it was given the wrong goalname.
Fixed bug with RTechnEnv.and_then. If the first list was empty, the second technique was never applied.

Lucas Dixon - 4 September 2006

added function to add elements to param tables
added function to get theorem of an assumption as needed for rippling skeletons (params are varified and meta vars are fixed), updated start rippling, still more to do.

Lucas Dixon - 3 September 2006

Reorganised things: moved all rippling code into one place: rtechn/rippling. For the idea behind this, see the CodeOrganisation page.
Refactored prf and aprf, removing the goal.ML file which previously wrapped terms. I also changed the name of name-collections from NTab to NCol, to make it easily distinguishable from name-tables.

Lucas Dixon - 31 August 2006

Fixed bug in term renaming: we no longer get dummy renamings for non-renamed terms.
Fixed bug in subst dtac: it was very confused, we now instantiate the term before we give it to low level rewriting. We were using the dthm, we are now using the rule which has the meta level equality, rather than the dthm, which is usually only object level.
Fixed bug in variable renaming when computing instantiations in rule nets: we had forgotten to rename vars that didn't appear in the pattern. We now pass hold a rule's variables with the rule.

Lucas Dixon - 30 August 2006

Rewrote aterms to fix a bug where they produced no annotations for embeddings. This also simplified the code.

Lucas Dixon - 29 August 2006

Rewrote the induction techniques
Re-organised the mini-isaplanner loading files
Added the ability to apply dtacs to fixed goals (free variables instead of meta-level params)
Changed IsaPlanner default to apply to fixed versions of the goals - this will be problematic when meta-variables exist: strange unifiers will be found. Some thought and care is needed here. A new version of unification which respects the idea of local constants is needed.
Added an signature and cleaned up argument order for function in RstPP(holds some utility functions for reasoning states)
Created this wiki
created a debug file for testing reasoning techniques at the ML level.
cleaned up induction tools, we now have induction dtac separated from the technique. It should now be making all non-induction variables into sinks.