Mutually-recursive non-freely generated dataytypes in Isabelle/HOL. Implemented as the animation of a meta-theory about the initial model of Horn clauses.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Examples
OtherExamples
manual-instantiations
quotient-ex
.hgtags
Equiv_Relation2.thy
Makefile
NonFree.thy
NonFreeAnimation.thy
NonFreeInput.thy
Other_README
Preliminaries.thy
README
ROOT.ML
SetoidIsotrans.thy
SimpViaMetaRec.thy
commit-tags
input.ML
isar-keywords-nonfreedata.el

README

This archive contains the code for the nonfree datatype package and examples.

The package works with Isabelle2013.

Some proofs use the Z3 SMT solver. To activate it you have to set
    Z3_NON_COMMERCIAL="yes"
in the environment or in "$ISABELLE_HOME_USER/etc/settings" (see also
contrib/z3* subdirectory of your Isabelle installation). This implies
that you should not use Z3 for commercial purposes.  In case you are
interested in commercial use of our package please let us know.

If you use ProofGeneral to process the examples you have to copy
isar-keywords-nonfreedata.el into Isabelle2013/etc/ 
and then start Isabelle with:
    isabelle emacs -k nonfreedata FSets_Bags.thy

The examples from the paper (including the appendix) are located in theories
with suggestive names.    


The package depends on the infrastructure for algorithmic rule systems and
forward rules in ../metarec/ which is also contained in the archive.