A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
#
# IsaMakefile for Tutorial
#
## targets
default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \
HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \
HOL-Protocol HOL-Documents styles
images:
test:
all: default
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
OPTIONS = -m brackets -i true -d "" -D document
USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL
REALUSEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL-Complex
## HOL
HOL:
@cd $(SRC)/HOL; $(ISATOOL) make HOL
HOL-Complex:
@cd $(SRC)/HOL; $(ISATOOL) make HOL-Complex
styles:
@rm -f isabelle.sty
@rm -f isabellesym.sty
@rm -f pdfsetup.sty
@$(ISATOOL) latex -o sty >/dev/null
@rm -f pdfsetup.sty
@rm -f */document/isabelle.sty
@rm -f */document/isabellesym.sty
@rm -f */document/pdfsetup.sty
@rm -f */document/session.tex
## HOL-Ifexpr
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
$(USEDIR) Ifexpr
@rm -f tutorial.dvi
## HOL-ToyList
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
$(USEDIR) ToyList2
@rm -f tutorial.dvi
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
$(USEDIR) ToyList
@rm -f tutorial.dvi
## HOL-CodeGen
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy
$(USEDIR) CodeGen
@rm -f tutorial.dvi
## HOL-Datatype
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
Datatype/Nested.thy Datatype/unfoldnested.thy \
Datatype/Fundata.thy
$(USEDIR) Datatype
@rm -f tutorial.dvi
## HOL-Trie
HOL-Trie: HOL $(LOG)/HOL-Trie.gz
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
$(USEDIR) Trie
@rm -f tutorial.dvi
## HOL-Recdef
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \
Recdef/simplification.thy Recdef/Induction.thy \
Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy
$(USEDIR) Recdef
@rm -f tutorial.dvi
## HOL-Advanced
HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \
Advanced/Partial.thy
$(USEDIR) Advanced
@rm -f tutorial.dvi
## HOL-Rules
HOL-Rules: HOL $(LOG)/HOL-Rules.gz
$(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \
Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \
Rules/Tacticals.thy Rules/ROOT.ML
@$(USEDIR) Rules
@rm -f tutorial.dvi
## HOL-Sets
HOL-Sets: HOL $(LOG)/HOL-Sets.gz
$(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
@$(USEDIR) Sets
@rm -f tutorial.dvi
## HOL-CTL
HOL-CTL: HOL $(LOG)/HOL-CTL.gz
$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
$(USEDIR) CTL
@rm -f tutorial.dvi
## HOL-Inductive
HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz
$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \
Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \
Inductive/Advanced.thy
$(USEDIR) Inductive
@rm -f tutorial.dvi
## HOL-Types
HOL-Complex-Types: HOL-Complex $(LOG)/HOL-Complex-Types.gz
$(LOG)/HOL-Complex-Types.gz: $(OUT)/HOL-Complex Types/ROOT.ML \
Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
Types/Overloading.thy Types/Axioms.thy
$(REALUSEDIR) Types
@rm -f tutorial.dvi
## HOL-Misc
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \
Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
$(USEDIR) Misc
@rm -f tutorial.dvi
## HOL-Protocol
HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz
$(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML \
Protocol/Message.thy Protocol/Message_lemmas.ML \
Protocol/Event.thy Protocol/Event_lemmas.ML \
Protocol/Public.thy Protocol/Public_lemmas.ML \
Protocol/NS_Public.thy
$(USEDIR) Protocol
@rm -f tutorial.dvi
## HOL-Documents
HOL-Documents: HOL $(LOG)/HOL-Documents.gz
$(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML
$(USEDIR) Documents
@rm -f tutorial.dvi
## clean
clean:
@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex