explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
authorwenzelm
Tue Dec 29 16:20:39 2009 +0100 (2009-12-29)
changeset 34205f69cd974bc4e
parent 34204 fd76bc33b89b
child 34206 c29264a16ad8
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
src/HOL/Extraction/ROOT.ML
src/HOL/IsaMakefile
src/HOL/Lambda/ROOT.ML
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/Extraction/ROOT.ML	Mon Dec 28 23:34:36 2009 +0100
     1.2 +++ b/src/HOL/Extraction/ROOT.ML	Tue Dec 29 16:20:39 2009 +0100
     1.3 @@ -1,11 +1,6 @@
     1.4 -(*  Title:      HOL/Extraction/ROOT.ML
     1.5 -
     1.6 -Examples for program extraction in Higher-Order Logic.
     1.7 -*)
     1.8 +(* Examples for program extraction in Higher-Order Logic *)
     1.9  
    1.10 -if HOL_proofs < 2 then
    1.11 -  warning "HOL proof terms required for running extraction examples"
    1.12 -else
    1.13 -  (Proofterm.proofs := 2;
    1.14 -   no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"];
    1.15 -   use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"]);
    1.16 +Proofterm.proofs := 2;
    1.17 +
    1.18 +no_document use_thys ["Efficient_Nat", "~~/src/HOL/Old_Number_Theory/Factorization"];
    1.19 +use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
     2.1 --- a/src/HOL/IsaMakefile	Mon Dec 28 23:34:36 2009 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Tue Dec 29 16:20:39 2009 +0100
     2.3 @@ -17,6 +17,7 @@
     2.4    HOL-NSA \
     2.5    HOL-Nominal \
     2.6    HOL-Plain \
     2.7 +  HOL-Proofs \
     2.8    HOL-SMT \
     2.9    HOL-Word \
    2.10    HOL4 \
    2.11 @@ -30,7 +31,6 @@
    2.12    HOL-Bali \
    2.13    HOL-Boogie-Examples \
    2.14    HOL-Decision_Procs \
    2.15 -  HOL-Extraction \
    2.16    HOL-Hahn_Banach \
    2.17    HOL-Hoare \
    2.18    HOL-Hoare_Parallel \
    2.19 @@ -41,7 +41,6 @@
    2.20    HOL-Import \
    2.21    HOL-Induct \
    2.22    HOL-Isar_Examples \
    2.23 -  HOL-Lambda \
    2.24    HOL-Lattice \
    2.25    HOL-Matrix \
    2.26    HOL-Metis_Examples \
    2.27 @@ -55,6 +54,8 @@
    2.28    HOL-Old_Number_Theory \
    2.29    HOL-Probability \
    2.30    HOL-Prolog \
    2.31 +  HOL-Proofs-Extraction \
    2.32 +  HOL-Proofs-Lambda \
    2.33    HOL-SET_Protocol \
    2.34    HOL-SMT-Examples \
    2.35    HOL-Statespace \
    2.36 @@ -69,8 +70,6 @@
    2.37    HOL-ZF
    2.38      # ^ this is the sort position
    2.39  
    2.40 -proofterms: HOL HOL-Extraction HOL-Lambda
    2.41 -
    2.42  all: test images
    2.43  
    2.44  
    2.45 @@ -91,6 +90,8 @@
    2.46  
    2.47  HOL-Main: Pure $(OUT)/HOL-Main
    2.48  
    2.49 +HOL-Proofs: Pure $(OUT)/HOL-Proofs
    2.50 +
    2.51  Pure:
    2.52  	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    2.53  
    2.54 @@ -324,7 +325,7 @@
    2.55  $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
    2.56  	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
    2.57  
    2.58 -$(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
    2.59 +HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
    2.60    Archimedean_Field.thy \
    2.61    Complex.thy \
    2.62    Complex_Main.thy \
    2.63 @@ -357,7 +358,13 @@
    2.64    Tools/Qelim/ferrante_rackoff.ML \
    2.65    Tools/Qelim/langford_data.ML \
    2.66    Tools/Qelim/langford.ML
    2.67 -	@$(ISABELLE_TOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    2.68 +
    2.69 +$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
    2.70 +	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
    2.71 +
    2.72 +$(OUT)/HOL-Proofs: ROOT.ML $(HOL_DEPENDENCIES)
    2.73 +	@$(ISABELLE_TOOL) usedir -b -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
    2.74 +
    2.75  
    2.76  
    2.77  ## HOL-Library
    2.78 @@ -800,17 +807,17 @@
    2.79  	@$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
    2.80  
    2.81  
    2.82 -## HOL-Lambda
    2.83 +## HOL-Proofs-Lambda
    2.84  
    2.85 -HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
    2.86 +HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
    2.87  
    2.88 -$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.thy Lambda/Eta.thy	\
    2.89 -  Lambda/InductTermi.thy Lambda/Lambda.thy Lambda/ListApplication.thy	\
    2.90 -  Lambda/ListBeta.thy Lambda/ListOrder.thy Lambda/NormalForm.thy	\
    2.91 -  Lambda/ParRed.thy Lambda/Standardization.thy Lambda/StrongNorm.thy	\
    2.92 -  Lambda/Type.thy Lambda/WeakNorm.thy Lambda/ROOT.ML			\
    2.93 -  Lambda/document/root.bib Lambda/document/root.tex
    2.94 -	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
    2.95 +$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs Lambda/Commutation.thy	\
    2.96 +  Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy		\
    2.97 +  Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy	\
    2.98 +  Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy	\
    2.99 +  Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy		\
   2.100 +  Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
   2.101 +	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL-Proofs Lambda
   2.102  
   2.103  
   2.104  ## HOL-Prolog
   2.105 @@ -893,17 +900,17 @@
   2.106  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
   2.107  
   2.108  
   2.109 -## HOL-Extraction
   2.110 +## HOL-Proofs-Extraction
   2.111  
   2.112 -HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
   2.113 +HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
   2.114  
   2.115 -$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy	\
   2.116 -  Extraction/Euclid.thy Extraction/Greatest_Common_Divisor.thy	\
   2.117 -  Extraction/Higman.thy Extraction/Pigeonhole.thy		\
   2.118 -  Extraction/QuotRem.thy Extraction/ROOT.ML Extraction/Util.thy	\
   2.119 -  Extraction/Warshall.thy Extraction/document/root.tex		\
   2.120 -  Extraction/document/root.bib
   2.121 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Extraction
   2.122 +$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs			\
   2.123 +  Library/Efficient_Nat.thy Extraction/Euclid.thy			\
   2.124 +  Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy		\
   2.125 +  Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML	\
   2.126 +  Extraction/Util.thy Extraction/Warshall.thy				\
   2.127 +  Extraction/document/root.tex Extraction/document/root.bib
   2.128 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Proofs Extraction
   2.129  
   2.130  
   2.131  ## HOL-IOA
   2.132 @@ -1417,18 +1424,17 @@
   2.133  	@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz			\
   2.134  		$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz			\
   2.135  		$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz	\
   2.136 -		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Extraction.gz	\
   2.137 -		$(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-Hoare.gz		\
   2.138 -		$(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-IMP.gz		\
   2.139 -		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz			\
   2.140 +		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Hahn_Banach.gz	\
   2.141 +		$(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare_Parallel.gz	\
   2.142 +		$(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz	\
   2.143  		$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz	\
   2.144  		$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz	\
   2.145 -		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Lattice			\
   2.146 -		$(LOG)/HOL-Lattice.gz $(LOG)/HOL-Lex.gz			\
   2.147 -		$(LOG)/HOL-Library.gz $(LOG)/HOL-Main.gz		\
   2.148 -		$(LOG)/HOL-Matrix $(LOG)/HOL-Matrix.gz			\
   2.149 -		$(LOG)/HOL-Metis_Examples.gz $(LOG)/HOL-MicroJava.gz	\
   2.150 -		$(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-Modelcheck.gz	\
   2.151 +		$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz		\
   2.152 +		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz			\
   2.153 +		$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix			\
   2.154 +		$(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz	\
   2.155 +		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz		\
   2.156 +		$(LOG)/HOL-Modelcheck.gz				\
   2.157  		$(LOG)/HOL-Multivariate_Analysis.gz			\
   2.158  		$(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz		\
   2.159  		$(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz	\
   2.160 @@ -1436,8 +1442,9 @@
   2.161  		$(LOG)/HOL-Number_Theory.gz				\
   2.162  		$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz	\
   2.163  		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
   2.164 -		$(LOG)/HOL-SET_Protocol.gz $(LOG)/HOL-SMT-Examples.gz	\
   2.165 -		$(LOG)/HOL-SMT.gz					\
   2.166 +		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz	\
   2.167 +		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
   2.168 +		$(LOG)/HOL-SMT-Examples.gz $(LOG)/HOL-SMT.gz		\
   2.169  		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
   2.170  		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
   2.171  		$(LOG)/HOL-W0.gz $(LOG)/HOL-Word-Examples.gz		\
   2.172 @@ -1447,5 +1454,5 @@
   2.173  		$(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base		\
   2.174  		$(OUT)/HOL-Boogie $(OUT)/HOL-Main			\
   2.175  		$(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA		\
   2.176 -		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain $(OUT)/HOL-SMT	\
   2.177 -		$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA
   2.178 +		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain $(OUT)/HOL-Proofs	\
   2.179 +		$(OUT)/HOL-SMT $(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA
     3.1 --- a/src/HOL/Lambda/ROOT.ML	Mon Dec 28 23:34:36 2009 +0100
     3.2 +++ b/src/HOL/Lambda/ROOT.ML	Tue Dec 29 16:20:39 2009 +0100
     3.3 @@ -1,14 +1,5 @@
     3.4 -(*  Title:      HOL/Lambda/ROOT.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Tobias Nipkow
     3.7 -    Copyright   1998 TUM
     3.8 -*)
     3.9 -
    3.10  Syntax.ambiguity_level := 100;
    3.11  Proofterm.proofs := 2;
    3.12  
    3.13  no_document use_thys ["Code_Integer"];
    3.14 -use_thys ["Eta", "StrongNorm", "Standardization"];
    3.15 -if HOL_proofs < 2 then
    3.16 -  warning "HOL proof terms required for running theory WeakNorm"
    3.17 -else use_thys ["WeakNorm"];
    3.18 +use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];
     4.1 --- a/src/HOL/ROOT.ML	Mon Dec 28 23:34:36 2009 +0100
     4.2 +++ b/src/HOL/ROOT.ML	Tue Dec 29 16:20:39 2009 +0100
     4.3 @@ -1,5 +1,3 @@
     4.4  (* Classical Higher-order Logic -- batteries included *)
     4.5  
     4.6  use_thys ["Complex_Main"];
     4.7 -
     4.8 -val HOL_proofs = ! Proofterm.proofs;