Minor cleanup of headers and some speedup of the HOL4 import.
authorskalberg
Sat Apr 17 23:53:35 2004 +0200 (2004-04-17)
changeset 146201be590fd2422
parent 14619 8876ad83b1fb
child 14621 bd78bdbc85a9
Minor cleanup of headers and some speedup of the HOL4 import.
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
src/HOL/Import/Generate-HOL/GenHOL4Real.thy
src/HOL/Import/Generate-HOL/GenHOL4Vec.thy
src/HOL/Import/Generate-HOL/GenHOL4Word32.thy
src/HOL/Import/Generate-HOL/ROOT.ML
src/HOL/Import/HOL/README
src/HOL/Import/HOL/ROOT.ML
src/HOL/Import/HOL/real.imp
src/HOL/Import/HOL/realax.imp
src/HOL/Import/HOL4Compat.thy
src/HOL/Import/HOL4Setup.thy
src/HOL/Import/HOL4Syntax.thy
src/HOL/Import/MakeEqual.thy
src/HOL/Import/ROOT.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_package.ML
src/HOL/Import/import_syntax.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Import/shuffler.ML
src/HOL/Tools/specification_package.ML
     1.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Apr 17 20:04:23 2004 +0200
     1.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Sat Apr 17 23:53:35 2004 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  Title:      HOL/Import/Generate-HOL/GenHOL4Base.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     1.7 +*)
     1.8 +
     1.9  theory GenHOL4Base = HOL4Compat + HOL4Syntax:;
    1.10  
    1.11  import_segment "hol4";
     2.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sat Apr 17 20:04:23 2004 +0200
     2.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Sat Apr 17 23:53:35 2004 +0200
     2.3 @@ -1,3 +1,8 @@
     2.4 +(*  Title:      HOL/Import/Generate-HOL/GenHOL4Prob.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     2.7 +*)
     2.8 +
     2.9  theory GenHOL4Prob = GenHOL4Real:
    2.10  
    2.11  import_segment "hol4";
     3.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Sat Apr 17 20:04:23 2004 +0200
     3.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Sat Apr 17 23:53:35 2004 +0200
     3.3 @@ -1,3 +1,8 @@
     3.4 +(*  Title:      HOL/Import/Generate-HOL/GenHOL4Real.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     3.7 +*)
     3.8 +
     3.9  theory GenHOL4Real = GenHOL4Base:
    3.10  
    3.11  import_segment "hol4";
     4.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sat Apr 17 20:04:23 2004 +0200
     4.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Sat Apr 17 23:53:35 2004 +0200
     4.3 @@ -1,3 +1,8 @@
     4.4 +(*  Title:      HOL/Import/Generate-HOL/GenHOL4Vec.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     4.7 +*)
     4.8 +
     4.9  theory GenHOL4Vec = GenHOL4Base:
    4.10  
    4.11  import_segment "hol4";
     5.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sat Apr 17 20:04:23 2004 +0200
     5.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Sat Apr 17 23:53:35 2004 +0200
     5.3 @@ -1,3 +1,8 @@
     5.4 +(*  Title:      HOL/Import/Generate-HOL/GenHOL4Word32.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     5.7 +*)
     5.8 +
     5.9  theory GenHOL4Word32 = GenHOL4Base:;
    5.10  
    5.11  import_segment "hol4";
     6.1 --- a/src/HOL/Import/Generate-HOL/ROOT.ML	Sat Apr 17 20:04:23 2004 +0200
     6.2 +++ b/src/HOL/Import/Generate-HOL/ROOT.ML	Sat Apr 17 23:53:35 2004 +0200
     6.3 @@ -1,3 +1,8 @@
     6.4 +(*  Title:      HOL/Import/Generate-HOL/ROOT.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     6.7 +*)
     6.8 +
     6.9  with_path ".." use_thy "HOL4Compat";
    6.10  with_path ".." use_thy "HOL4Syntax";
    6.11  use_thy "GenHOL4Prob";
     7.1 --- a/src/HOL/Import/HOL/README	Sat Apr 17 20:04:23 2004 +0200
     7.2 +++ b/src/HOL/Import/HOL/README	Sat Apr 17 23:53:35 2004 +0200
     7.3 @@ -1,3 +1,20 @@
     7.4 +(*  Title:      HOL/Import/HOL/README
     7.5 +    ID:         $Id$
     7.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     7.7 +*)
     7.8 +
     7.9  All the files in this directory (except this README, HOL4.thy, and
    7.10  ROOT.ML) are automatically generated.  Edit the files in
    7.11 -../Generate-HOL, if something needs to be changed.
    7.12 +../Generate-HOL and run "isatool make HOL-Complex-Generate-HOL" in
    7.13 +~~/src/HOL, if something needs to be changed.
    7.14 +
    7.15 +To build the logic in this directory, simply do a "isatool make
    7.16 +HOL-Import-HOL" in ~~/src/HOL.
    7.17 +
    7.18 +Note that the quick_and_dirty flag is on as default for this
    7.19 +directory, which means that the original HOL4 proofs are not consulted
    7.20 +at all.  If a real replay of the HOL4 proofs is desired, get and
    7.21 +unpack the HOL4 proof objects to somewhere on your harddisk, and set
    7.22 +the variable PROOF_DIRS to the directory where the directory "hol4"
    7.23 +is.  Now edit the ROOT.ML file to unset the quick_and_dirty flag and
    7.24 +do "isatool make HOL-Import-HOL" in ~~/src/HOL.
     8.1 --- a/src/HOL/Import/HOL/ROOT.ML	Sat Apr 17 20:04:23 2004 +0200
     8.2 +++ b/src/HOL/Import/HOL/ROOT.ML	Sat Apr 17 23:53:35 2004 +0200
     8.3 @@ -1,3 +1,8 @@
     8.4 +(*  Title:      HOL/Import/HOL/ROOT.ML
     8.5 +    ID:         $Id$
     8.6 +    Author:     Sebastian Skalberg (TU Muenchen)
     8.7 +*)
     8.8 +
     8.9  with_path ".." use_thy "HOL4Compat";
    8.10  with_path ".." use_thy "HOL4Syntax";
    8.11  setmp quick_and_dirty true use_thy "HOL4Prob";
     9.1 --- a/src/HOL/Import/HOL/real.imp	Sat Apr 17 20:04:23 2004 +0200
     9.2 +++ b/src/HOL/Import/HOL/real.imp	Sat Apr 17 23:53:35 2004 +0200
     9.3 @@ -77,13 +77,13 @@
     9.4    "REAL_SUB_RZERO" > "Ring_and_Field.diff_0_right"
     9.5    "REAL_SUB_RNEG" > "Ring_and_Field.diff_minus_eq_add"
     9.6    "REAL_SUB_REFL" > "Ring_and_Field.diff_self"
     9.7 -  "REAL_SUB_RDISTRIB" > "Ring_and_Field.left_diff_distrib"
     9.8 +  "REAL_SUB_RDISTRIB" > "Ring_and_Field.ring_eq_simps_6"
     9.9    "REAL_SUB_NEG2" > "HOL4Real.real.REAL_SUB_NEG2"
    9.10    "REAL_SUB_LZERO" > "Ring_and_Field.diff_0"
    9.11    "REAL_SUB_LT" > "RealDef.real_0_less_diff_iff"
    9.12    "REAL_SUB_LNEG" > "HOL4Real.real.REAL_SUB_LNEG"
    9.13    "REAL_SUB_LE" > "RealDef.real_0_le_diff_iff"
    9.14 -  "REAL_SUB_LDISTRIB" > "Ring_and_Field.right_diff_distrib"
    9.15 +  "REAL_SUB_LDISTRIB" > "Ring_and_Field.ring_eq_simps_7"
    9.16    "REAL_SUB_INV2" > "HOL4Real.real.REAL_SUB_INV2"
    9.17    "REAL_SUB_ADD2" > "Ring_and_Field.add_minus_self_left"
    9.18    "REAL_SUB_ADD" > "Ring_and_Field.minus_add_self"
    9.19 @@ -91,7 +91,7 @@
    9.20    "REAL_SUB_0" > "Ring_and_Field.eq_iff_diff_eq_0"
    9.21    "REAL_RNEG_UNIQ" > "RealDef.real_add_eq_0_iff"
    9.22    "REAL_RINV_UNIQ" > "RealDef.real_inverse_unique"
    9.23 -  "REAL_RDISTRIB" > "Ring_and_Field.ring_distrib_2"
    9.24 +  "REAL_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
    9.25    "REAL_POW_POW" > "Power.power_mult"
    9.26    "REAL_POW_MONO_LT" > "Power.power_strict_increasing"
    9.27    "REAL_POW_LT2" > "HOL4Real.real.REAL_POW_LT2"
    9.28 @@ -129,7 +129,7 @@
    9.29    "REAL_NEG_ADD" > "Ring_and_Field.minus_add_distrib"
    9.30    "REAL_NEG_0" > "Ring_and_Field.minus_zero"
    9.31    "REAL_NEGNEG" > "Ring_and_Field.minus_minus"
    9.32 -  "REAL_MUL_SYM" > "Ring_and_Field.mult_ac_2"
    9.33 +  "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2"
    9.34    "REAL_MUL_RZERO" > "Ring_and_Field.mult_zero_right"
    9.35    "REAL_MUL_RNEG" > "Ring_and_Field.minus_mult_right"
    9.36    "REAL_MUL_RINV" > "Ring_and_Field.right_inverse"
    9.37 @@ -243,7 +243,7 @@
    9.38    "REAL_LET_ADD" > "HOL4Real.real.REAL_LET_ADD"
    9.39    "REAL_LE1_POW2" > "HOL4Real.real.REAL_LE1_POW2"
    9.40    "REAL_LE" > "RealDef.real_of_nat_le_iff"
    9.41 -  "REAL_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
    9.42 +  "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
    9.43    "REAL_INV_POS" > "Ring_and_Field.positive_imp_inverse_positive"
    9.44    "REAL_INV_NZ" > "Ring_and_Field.nonzero_imp_inverse_nonzero"
    9.45    "REAL_INV_MUL" > "HOL4Real.real.REAL_INV_MUL"
    9.46 @@ -257,8 +257,8 @@
    9.47    "REAL_INJ" > "RealDef.real_of_nat_inject"
    9.48    "REAL_HALF_DOUBLE" > "RComplete.real_sum_of_halves"
    9.49    "REAL_FACT_NZ" > "HOL4Real.real.REAL_FACT_NZ"
    9.50 -  "REAL_EQ_SUB_RADD" > "Ring_and_Field.compare_rls_10"
    9.51 -  "REAL_EQ_SUB_LADD" > "Ring_and_Field.compare_rls_11"
    9.52 +  "REAL_EQ_SUB_RADD" > "Ring_and_Field.ring_eq_simps_15"
    9.53 +  "REAL_EQ_SUB_LADD" > "Ring_and_Field.ring_eq_simps_16"
    9.54    "REAL_EQ_RMUL_IMP" > "Ring_and_Field.field_mult_cancel_right_lemma"
    9.55    "REAL_EQ_RMUL" > "Ring_and_Field.field_mult_cancel_right"
    9.56    "REAL_EQ_RDIV_EQ" > "HOL4Real.real.REAL_EQ_RDIV_EQ"
    9.57 @@ -283,17 +283,17 @@
    9.58    "REAL_DIFFSQ" > "HOL4Real.real.REAL_DIFFSQ"
    9.59    "REAL_ARCH_LEAST" > "HOL4Real.real.REAL_ARCH_LEAST"
    9.60    "REAL_ARCH" > "RComplete.reals_Archimedean3"
    9.61 -  "REAL_ADD_SYM" > "Ring_and_Field.add_ac_2"
    9.62 +  "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
    9.63    "REAL_ADD_SUB2" > "HOL4Real.real.REAL_ADD_SUB2"
    9.64    "REAL_ADD_SUB" > "Ring_and_Field.add_minus_self_right"
    9.65    "REAL_ADD_RINV" > "Ring_and_Field.right_minus"
    9.66    "REAL_ADD_RID_UNIQ" > "HOL4Real.real.REAL_ADD_RID_UNIQ"
    9.67    "REAL_ADD_RID" > "Ring_and_Field.add_0_right"
    9.68 -  "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_distrib_2"
    9.69 +  "REAL_ADD_RDISTRIB" > "Ring_and_Field.ring_eq_simps_4"
    9.70    "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
    9.71    "REAL_ADD_LID_UNIQ" > "HOL4Real.real.REAL_ADD_LID_UNIQ"
    9.72    "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0"
    9.73 -  "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
    9.74 +  "REAL_ADD_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
    9.75    "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
    9.76    "REAL_ADD2_SUB2" > "HOL4Real.real.REAL_ADD2_SUB2"
    9.77    "REAL_ADD" > "RealDef.real_of_nat_add"
    10.1 --- a/src/HOL/Import/HOL/realax.imp	Sat Apr 17 20:04:23 2004 +0200
    10.2 +++ b/src/HOL/Import/HOL/realax.imp	Sat Apr 17 23:53:35 2004 +0200
    10.3 @@ -91,7 +91,7 @@
    10.4    "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC"
    10.5    "TREAL_10" > "HOL4Real.realax.TREAL_10"
    10.6    "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
    10.7 -  "REAL_MUL_SYM" > "Ring_and_Field.mult_ac_2"
    10.8 +  "REAL_MUL_SYM" > "Ring_and_Field.ring_eq_simps_2"
    10.9    "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
   10.10    "REAL_MUL_LID" > "Ring_and_Field.almost_semiring.mult_1"
   10.11    "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
   10.12 @@ -100,9 +100,9 @@
   10.13    "REAL_LT_REFL" > "HOL.order_less_irrefl"
   10.14    "REAL_LT_MUL" > "Ring_and_Field.mult_pos"
   10.15    "REAL_LT_IADD" > "Ring_and_Field.add_strict_left_mono"
   10.16 -  "REAL_LDISTRIB" > "Ring_and_Field.ring_distrib_1"
   10.17 +  "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
   10.18    "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"
   10.19 -  "REAL_ADD_SYM" > "Ring_and_Field.add_ac_2"
   10.20 +  "REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
   10.21    "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
   10.22    "REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0"
   10.23    "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
    11.1 --- a/src/HOL/Import/HOL4Compat.thy	Sat Apr 17 20:04:23 2004 +0200
    11.2 +++ b/src/HOL/Import/HOL4Compat.thy	Sat Apr 17 23:53:35 2004 +0200
    11.3 @@ -1,3 +1,8 @@
    11.4 +(*  Title:      HOL/Import/HOL4Compat.thy
    11.5 +    ID:         $Id$
    11.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    11.7 +*)
    11.8 +
    11.9  theory HOL4Compat = HOL4Setup + Divides + Primes + Real:
   11.10  
   11.11  lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
    12.1 --- a/src/HOL/Import/HOL4Setup.thy	Sat Apr 17 20:04:23 2004 +0200
    12.2 +++ b/src/HOL/Import/HOL4Setup.thy	Sat Apr 17 23:53:35 2004 +0200
    12.3 @@ -1,3 +1,8 @@
    12.4 +(*  Title:      HOL/Import/HOL4Setup.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    12.7 +*)
    12.8 +
    12.9  theory HOL4Setup = MakeEqual
   12.10    files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"):
   12.11  
    13.1 --- a/src/HOL/Import/HOL4Syntax.thy	Sat Apr 17 20:04:23 2004 +0200
    13.2 +++ b/src/HOL/Import/HOL4Syntax.thy	Sat Apr 17 23:53:35 2004 +0200
    13.3 @@ -1,3 +1,8 @@
    13.4 +(*  Title:      HOL/Import/HOL4Syntax.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    13.7 +*)
    13.8 +
    13.9  theory HOL4Syntax = HOL4Setup
   13.10    files "import_syntax.ML":
   13.11  
    14.1 --- a/src/HOL/Import/MakeEqual.thy	Sat Apr 17 20:04:23 2004 +0200
    14.2 +++ b/src/HOL/Import/MakeEqual.thy	Sat Apr 17 23:53:35 2004 +0200
    14.3 @@ -1,3 +1,8 @@
    14.4 +(*  Title:      HOL/Import/MakeEqual.thy
    14.5 +    ID:         $Id$
    14.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    14.7 +*)
    14.8 +
    14.9  theory MakeEqual = Main
   14.10    files "shuffler.ML":
   14.11  
    15.1 --- a/src/HOL/Import/ROOT.ML	Sat Apr 17 20:04:23 2004 +0200
    15.2 +++ b/src/HOL/Import/ROOT.ML	Sat Apr 17 23:53:35 2004 +0200
    15.3 @@ -1,2 +1,7 @@
    15.4 +(*  Title:      HOL/Import/ROOT.ML
    15.5 +    ID:         $Id$
    15.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    15.7 +*)
    15.8 +
    15.9  use_thy "HOL4Compat";
   15.10  use_thy "HOL4Syntax";
    16.1 --- a/src/HOL/Import/hol4rews.ML	Sat Apr 17 20:04:23 2004 +0200
    16.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Apr 17 23:53:35 2004 +0200
    16.3 @@ -1,3 +1,8 @@
    16.4 +(*  Title:      HOL/Import/hol4rews.ML
    16.5 +    ID:         $Id$
    16.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    16.7 +*)
    16.8 +
    16.9  structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);
   16.10  
   16.11  type holthm = (term * term) list * thm
   16.12 @@ -24,7 +29,7 @@
   16.13  
   16.14  structure ImportSegmentArgs: THEORY_DATA_ARGS =
   16.15  struct
   16.16 -val name = "HOL4/import"
   16.17 +val name = "HOL4/import_segment"
   16.18  type T = string
   16.19  val empty = ""
   16.20  val copy = I
    17.1 --- a/src/HOL/Import/import_package.ML	Sat Apr 17 20:04:23 2004 +0200
    17.2 +++ b/src/HOL/Import/import_package.ML	Sat Apr 17 23:53:35 2004 +0200
    17.3 @@ -1,3 +1,8 @@
    17.4 +(*  Title:      HOL/Import/import_package.ML
    17.5 +    ID:         $Id$
    17.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    17.7 +*)
    17.8 +
    17.9  signature IMPORT_PACKAGE =
   17.10  sig
   17.11      val import_meth: Args.src -> Proof.context -> Proof.method
   17.12 @@ -5,6 +10,20 @@
   17.13      val debug      : bool ref
   17.14  end
   17.15  
   17.16 +structure ImportDataArgs: THEORY_DATA_ARGS =
   17.17 +struct
   17.18 +val name = "HOL4/import_data"
   17.19 +type T = ProofKernel.thm option array option
   17.20 +val empty = None
   17.21 +val copy = I
   17.22 +val prep_ext = I
   17.23 +fun merge _ = None
   17.24 +fun print sg import_segment =
   17.25 +    Pretty.writeln (Pretty.str ("Pretty printing of importer data not implemented"))
   17.26 +end
   17.27 +
   17.28 +structure ImportData = TheoryDataFun(ImportDataArgs)
   17.29 +
   17.30  structure ImportPackage :> IMPORT_PACKAGE =
   17.31  struct
   17.32  
   17.33 @@ -24,7 +43,9 @@
   17.34  	    val sg = sign_of_thm th
   17.35  	    val prem = hd (prems_of th)
   17.36  	    val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
   17.37 -	    val int_thms = fst (Replay.setup_int_thms thyname thy)
   17.38 +	    val int_thms = case ImportData.get thy of
   17.39 +			       None => fst (Replay.setup_int_thms thyname thy)
   17.40 +			     | Some a => a
   17.41  	    val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
   17.42  	    val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
   17.43  	    val thm = snd (ProofKernel.to_isa_thm hol4thm)
   17.44 @@ -57,5 +78,5 @@
   17.45  			  Method.SIMPLE_METHOD (import_tac arg thy)
   17.46  		      end)
   17.47  
   17.48 -val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem")]
   17.49 +val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init]
   17.50  end
    18.1 --- a/src/HOL/Import/import_syntax.ML	Sat Apr 17 20:04:23 2004 +0200
    18.2 +++ b/src/HOL/Import/import_syntax.ML	Sat Apr 17 23:53:35 2004 +0200
    18.3 @@ -1,3 +1,8 @@
    18.4 +(*  Title:      HOL/Import/import_syntax.ML
    18.5 +    ID:         $Id$
    18.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    18.7 +*)
    18.8 +
    18.9  signature HOL4_IMPORT_SYNTAX =
   18.10  sig
   18.11      type token = OuterSyntax.token
   18.12 @@ -150,14 +155,26 @@
   18.13  	apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
   18.14      end
   18.15  
   18.16 +fun create_int_thms thyname thy =
   18.17 +    case ImportData.get thy of
   18.18 +	None => ImportData.put (Some (fst (Replay.setup_int_thms thyname thy))) thy
   18.19 +      | Some _ => error "Import data not closed - forgotten an end_setup, mayhap?"
   18.20 +
   18.21 +fun clear_int_thms thy =
   18.22 +    case ImportData.get thy of
   18.23 +	None => error "Import data already cleared - forgotten a setup_theory?"
   18.24 +      | Some _ => ImportData.put None thy
   18.25 +
   18.26  val setup_theory = P.name
   18.27  		       >>
   18.28  		       (fn thyname =>
   18.29  			fn thy =>
   18.30 -			   case HOL4DefThy.get thy of
   18.31 -			       NoImport => thy |> import_thy thyname
   18.32 -			     | Generating _ => error "Currently generating a theory!"
   18.33 -			     | Replaying _ => thy |> clear_import_thy |> import_thy thyname)
   18.34 +			   (case HOL4DefThy.get thy of
   18.35 +				NoImport => thy
   18.36 +			      | Generating _ => error "Currently generating a theory!"
   18.37 +			      | Replaying _ => thy |> clear_import_thy)
   18.38 +			       |> import_thy thyname
   18.39 +			       |> create_int_thms thyname)
   18.40  
   18.41  fun end_setup toks =
   18.42      Scan.succeed
   18.43 @@ -168,6 +185,7 @@
   18.44  	    in
   18.45  		thy |> set_segment thyname segname
   18.46  		    |> clear_import_thy
   18.47 +		    |> clear_int_thms
   18.48  		    |> Theory.parent_path
   18.49  	    end) toks
   18.50  
    19.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Apr 17 20:04:23 2004 +0200
    19.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Apr 17 23:53:35 2004 +0200
    19.3 @@ -1,3 +1,8 @@
    19.4 +(*  Title:      HOL/Import/proof_kernel.ML
    19.5 +    ID:         $Id$
    19.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    19.7 +*)
    19.8 +
    19.9  signature ProofKernel =
   19.10  sig
   19.11      type hol_type
   19.12 @@ -47,7 +52,7 @@
   19.13  
   19.14      exception PK of string * string
   19.15  
   19.16 -    val get_proof_dir: string -> theory -> string
   19.17 +    val get_proof_dir: string -> theory -> string option
   19.18      val debug : bool ref
   19.19      val disk_info_of : proof -> (string * string) option
   19.20      val set_disk_info_of : proof -> string -> string -> unit
   19.21 @@ -165,16 +170,10 @@
   19.22  
   19.23  (* Compatibility. *)
   19.24  
   19.25 -fun quote s = "\"" ^ s ^ "\""
   19.26 -
   19.27 -fun alphanum str = case String.explode str of
   19.28 -		       first::rest => Char.isAlpha first andalso forall (fn c => Char.isAlphaNum c orelse c = #"_") rest
   19.29 -		     | _ => error "ProofKernel.alphanum: Empty constname??"
   19.30 -
   19.31 -fun mk_syn c = if alphanum c then NoSyn else Syntax.literal c
   19.32 +fun mk_syn c = if Symbol.is_identifier c then NoSyn else Syntax.literal c
   19.33  
   19.34  val keywords = ["open"]
   19.35 -fun quotename c = if alphanum c andalso not (c mem keywords) then c else quote c
   19.36 +fun quotename c = if Symbol.is_identifier c andalso not (c mem keywords) then c else quote c
   19.37  
   19.38  fun smart_string_of_cterm ct =
   19.39      let
   19.40 @@ -321,6 +320,7 @@
   19.41  	    || scan_string "quot;" #"\""
   19.42  	    || scan_string "gt;" #">"
   19.43  	    || scan_string "lt;" #"<"
   19.44 +            || scan_string "apos;" #"'"
   19.45  in
   19.46  fun scan_nonquote toks =
   19.47      case LazySeq.getItem toks of
   19.48 @@ -566,29 +566,29 @@
   19.49  	    case get_segment2 thyname thy of
   19.50  		Some seg => seg
   19.51  	      | None => get_import_segment thy
   19.52 -	val defpath = [(getenv "ISABELLE_HOME_USER") ^ "/proofs"]
   19.53 -	val path =
   19.54 -	    case getenv "PROOF_DIRS" of
   19.55 -		"" => defpath
   19.56 -	      | path => (space_explode ":" path) @ defpath
   19.57 -	fun find [] = error ("Unable to find import segment " ^ import_segment)
   19.58 -	  | find (p::ps) = (let
   19.59 -				val dir = p ^ "/" ^ import_segment
   19.60 -			    in
   19.61 -				if OS.FileSys.isDir dir
   19.62 -				then dir
   19.63 -				else find ps
   19.64 -			    end) handle OS.SysErr _ => find ps
   19.65 +	val defpath = [OS.Path.joinDirFile {dir=getenv "ISABELLE_HOME_USER",file="proofs"}]
   19.66 +	val path = space_explode ":" (getenv "PROOF_DIRS") @ defpath
   19.67 +	fun find [] = None
   19.68 +	  | find (p::ps) =
   19.69 +	    (let
   19.70 +		 val dir = OS.Path.joinDirFile {dir = p,file=import_segment}
   19.71 +	     in
   19.72 +		 if OS.FileSys.isDir dir
   19.73 +		 then Some dir
   19.74 +		 else find ps
   19.75 +	     end) handle OS.SysErr _ => find ps
   19.76      in
   19.77 -	find path ^ "/" ^ thyname
   19.78 +	apsome (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
   19.79      end
   19.80  			   
   19.81  fun proof_file_name thyname thmname thy =
   19.82      let
   19.83 -	val path = get_proof_dir thyname thy
   19.84 +	val path = case get_proof_dir thyname thy of
   19.85 +		       Some p => p
   19.86 +		     | None => error "Cannot find proof files"
   19.87  	val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
   19.88      in
   19.89 -	String.concat[path,"/",thmname,".prf"]
   19.90 +	OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = thmname, ext = SOME "prf"}}
   19.91      end
   19.92  	
   19.93  fun xml_to_proof thyname types terms prf thy =
    20.1 --- a/src/HOL/Import/replay.ML	Sat Apr 17 20:04:23 2004 +0200
    20.2 +++ b/src/HOL/Import/replay.ML	Sat Apr 17 23:53:35 2004 +0200
    20.3 @@ -1,3 +1,8 @@
    20.4 +(*  Title:      HOL/Import/replay.ML
    20.5 +    ID:         $Id$
    20.6 +    Author:     Sebastian Skalberg (TU Muenchen)
    20.7 +*)
    20.8 +
    20.9  structure Replay =
   20.10  struct
   20.11  
   20.12 @@ -268,7 +273,11 @@
   20.13  
   20.14  fun setup_int_thms thyname thy =
   20.15      let
   20.16 -	val is = TextIO.openIn(P.get_proof_dir thyname thy ^"/facts.lst")
   20.17 +	val fname =
   20.18 +	    case P.get_proof_dir thyname thy of
   20.19 +		Some p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
   20.20 +	      | None => error "Cannot find proof files"
   20.21 +	val is = TextIO.openIn fname
   20.22  	val (num_int_thms,facts) =
   20.23  	    let
   20.24  		fun get_facts facts =
    21.1 --- a/src/HOL/Import/shuffler.ML	Sat Apr 17 20:04:23 2004 +0200
    21.2 +++ b/src/HOL/Import/shuffler.ML	Sat Apr 17 23:53:35 2004 +0200
    21.3 @@ -1,7 +1,6 @@
    21.4 -(*  Title:      Provers/shuffler.ML
    21.5 +(*  Title:      HOL/Import/shuffler.ML
    21.6      ID:         $Id$
    21.7      Author:     Sebastian Skalberg, TU Muenchen
    21.8 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    21.9  
   21.10  Package for proving two terms equal by normalizing (hence the
   21.11  "shuffler" name).  Uses the simplifier for the normalization.
    22.1 --- a/src/HOL/Tools/specification_package.ML	Sat Apr 17 20:04:23 2004 +0200
    22.2 +++ b/src/HOL/Tools/specification_package.ML	Sat Apr 17 23:53:35 2004 +0200
    22.3 @@ -1,7 +1,6 @@
    22.4  (*  Title:      HOL/Tools/specification_package.ML
    22.5      ID:         $Id$
    22.6      Author:     Sebastian Skalberg, TU Muenchen
    22.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    22.8  
    22.9  Package for defining constants by specification.
   22.10  *)