New headers and other minor changes
authorpaulson
Thu May 22 15:13:16 1997 +0200 (1997-05-22)
changeset 3302404fe31fd8d2
parent 3301 cdcc4d5602b6
child 3303 656b5221a56e
New headers and other minor changes
TFL/dcterm.sml
TFL/mask.sig
TFL/mask.sml
TFL/post.sml
TFL/rules.new.sml
TFL/rules.sig
TFL/sys.sml
TFL/tfl.sig
TFL/thms.sig
TFL/thms.sml
TFL/thry.sig
TFL/thry.sml
TFL/usyntax.sig
TFL/usyntax.sml
TFL/utils.sig
TFL/utils.sml
     1.1 --- a/TFL/dcterm.sml	Thu May 22 15:11:56 1997 +0200
     1.2 +++ b/TFL/dcterm.sml	Thu May 22 15:13:16 1997 +0200
     1.3 @@ -1,3 +1,9 @@
     1.4 +(*  Title:      TFL/dcterm
     1.5 +    ID:         $Id$
     1.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     1.7 +    Copyright   1997  University of Cambridge
     1.8 +*)
     1.9 +
    1.10  (*---------------------------------------------------------------------------
    1.11   * Derived efficient cterm destructors.
    1.12   *---------------------------------------------------------------------------*)
     2.1 --- a/TFL/mask.sig	Thu May 22 15:11:56 1997 +0200
     2.2 +++ b/TFL/mask.sig	Thu May 22 15:13:16 1997 +0200
     2.3 @@ -1,3 +1,9 @@
     2.4 +(*  Title:      TFL/mask
     2.5 +    ID:         $Id$
     2.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     2.7 +    Copyright   1997  University of Cambridge
     2.8 +*)
     2.9 +
    2.10  signature Mask_sig =
    2.11  sig
    2.12   datatype 'a binding = |-> of ('a * 'a)  (* infix 7 |->; *)
     3.1 --- a/TFL/mask.sml	Thu May 22 15:11:56 1997 +0200
     3.2 +++ b/TFL/mask.sml	Thu May 22 15:13:16 1997 +0200
     3.3 @@ -1,3 +1,9 @@
     3.4 +(*  Title:      TFL/mask
     3.5 +    ID:         $Id$
     3.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     3.7 +    Copyright   1997  University of Cambridge
     3.8 +*)
     3.9 +
    3.10  (*---------------------------------------------------------------------------
    3.11   * This structure is intended to shield TFL from any constructors already 
    3.12   * declared in the environment. In the Isabelle port, for example, there
     4.1 --- a/TFL/post.sml	Thu May 22 15:11:56 1997 +0200
     4.2 +++ b/TFL/post.sml	Thu May 22 15:13:16 1997 +0200
     4.3 @@ -1,6 +1,13 @@
     4.4 +(*  Title:      TFL/post
     4.5 +    ID:         $Id$
     4.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     4.7 +    Copyright   1997  University of Cambridge
     4.8 +
     4.9 +Postprocessing of TFL definitions
    4.10 +*)
    4.11 +
    4.12  (*-------------------------------------------------------------------------
    4.13 -there are 3 postprocessors that get applied to the definition:
    4.14 -
    4.15 +Three postprocessors are applied to the definition:
    4.16      - a wellfoundedness prover (WF_TAC)
    4.17      - a simplifier (tries to eliminate the language of termination expressions)
    4.18      - a termination prover
    4.19 @@ -75,7 +82,7 @@
    4.20                                      addss (!simpset)) 1);
    4.21  
    4.22   val simpls = [less_eq RS eq_reflection,
    4.23 -               lex_prod_def, rprod_def, measure_def, inv_image_def];
    4.24 +               lex_prod_def, measure_def, inv_image_def];
    4.25  
    4.26   (*---------------------------------------------------------------------------
    4.27    * Does some standard things with the termination conditions of a definition:
    4.28 @@ -191,14 +198,14 @@
    4.29            |   e                 => print_exn e;
    4.30  
    4.31  
    4.32 -(*lcp: uncurry the predicate of the induction rule*)
    4.33 -fun uncurry_rule rl = Prod_Syntax.split_rule_var
    4.34 +(*lcp: curry the predicate of the induction rule*)
    4.35 +fun curry_rule rl = Prod_Syntax.split_rule_var
    4.36                          (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
    4.37  			 rl);
    4.38  
    4.39  (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
    4.40  val meta_outer = 
    4.41 -    uncurry_rule o standard o 
    4.42 +    curry_rule o standard o 
    4.43      rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]
    4.44  				  ORELSE' etac conjE));
    4.45  
     5.1 --- a/TFL/rules.new.sml	Thu May 22 15:11:56 1997 +0200
     5.2 +++ b/TFL/rules.new.sml	Thu May 22 15:13:16 1997 +0200
     5.3 @@ -1,3 +1,11 @@
     5.4 +(*  Title:      TFL/rules
     5.5 +    ID:         $Id$
     5.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     5.7 +    Copyright   1997  University of Cambridge
     5.8 +
     5.9 +Emulation of HOL inference rules for TFL
    5.10 +*)
    5.11 +
    5.12  structure FastRules : Rules_sig = 
    5.13  struct
    5.14  
     6.1 --- a/TFL/rules.sig	Thu May 22 15:11:56 1997 +0200
     6.2 +++ b/TFL/rules.sig	Thu May 22 15:13:16 1997 +0200
     6.3 @@ -1,3 +1,11 @@
     6.4 +(*  Title:      TFL/rules
     6.5 +    ID:         $Id$
     6.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     6.7 +    Copyright   1997  University of Cambridge
     6.8 +
     6.9 +Emulation of HOL inference rules for TFL
    6.10 +*)
    6.11 +
    6.12  signature Rules_sig =
    6.13  sig
    6.14  (*  structure USyntax : USyntax_sig *)
     7.1 --- a/TFL/sys.sml	Thu May 22 15:11:56 1997 +0200
     7.2 +++ b/TFL/sys.sml	Thu May 22 15:13:16 1997 +0200
     7.3 @@ -1,4 +1,10 @@
     7.4 -(* Compile the TFL system *)
     7.5 +(*  Title:      TFL/mask
     7.6 +    ID:         $Id$
     7.7 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     7.8 +    Copyright   1997  University of Cambridge
     7.9 +
    7.10 +Compile the TFL system
    7.11 +*)
    7.12  
    7.13  (* Portability stuff *)
    7.14  nonfix prefix;
     8.1 --- a/TFL/tfl.sig	Thu May 22 15:11:56 1997 +0200
     8.2 +++ b/TFL/tfl.sig	Thu May 22 15:13:16 1997 +0200
     8.3 @@ -1,3 +1,11 @@
     8.4 +(*  Title:      TFL/tfl
     8.5 +    ID:         $Id$
     8.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     8.7 +    Copyright   1997  University of Cambridge
     8.8 +
     8.9 +Main TFL functor
    8.10 +*)
    8.11 +
    8.12  signature TFL_sig =
    8.13  sig
    8.14     structure Rules: Rules_sig
     9.1 --- a/TFL/thms.sig	Thu May 22 15:11:56 1997 +0200
     9.2 +++ b/TFL/thms.sig	Thu May 22 15:13:16 1997 +0200
     9.3 @@ -1,3 +1,9 @@
     9.4 +(*  Title:      TFL/thms
     9.5 +    ID:         $Id$
     9.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     9.7 +    Copyright   1997  University of Cambridge
     9.8 +*)
     9.9 +
    9.10  signature Thms_sig =
    9.11  sig
    9.12     val WF_INDUCTION_THM:thm
    10.1 --- a/TFL/thms.sml	Thu May 22 15:11:56 1997 +0200
    10.2 +++ b/TFL/thms.sml	Thu May 22 15:13:16 1997 +0200
    10.3 @@ -1,3 +1,9 @@
    10.4 +(*  Title:      TFL/thms
    10.5 +    ID:         $Id$
    10.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
    10.7 +    Copyright   1997  University of Cambridge
    10.8 +*)
    10.9 +
   10.10  structure Thms : Thms_sig =
   10.11  struct
   10.12     val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
    11.1 --- a/TFL/thry.sig	Thu May 22 15:11:56 1997 +0200
    11.2 +++ b/TFL/thry.sig	Thu May 22 15:13:16 1997 +0200
    11.3 @@ -1,3 +1,9 @@
    11.4 +(*  Title:      TFL/thry
    11.5 +    ID:         $Id$
    11.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
    11.7 +    Copyright   1997  University of Cambridge
    11.8 +*)
    11.9 +
   11.10  signature Thry_sig =
   11.11  sig
   11.12    type 'a binding
    12.1 --- a/TFL/thry.sml	Thu May 22 15:11:56 1997 +0200
    12.2 +++ b/TFL/thry.sml	Thu May 22 15:13:16 1997 +0200
    12.3 @@ -1,3 +1,9 @@
    12.4 +(*  Title:      TFL/thry
    12.5 +    ID:         $Id$
    12.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
    12.7 +    Copyright   1997  University of Cambridge
    12.8 +*)
    12.9 +
   12.10  structure Thry : Thry_sig (* LThry_sig *) = 
   12.11  struct
   12.12  
    13.1 --- a/TFL/usyntax.sig	Thu May 22 15:11:56 1997 +0200
    13.2 +++ b/TFL/usyntax.sig	Thu May 22 15:13:16 1997 +0200
    13.3 @@ -1,3 +1,11 @@
    13.4 +(*  Title:      TFL/usyntax
    13.5 +    ID:         $Id$
    13.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
    13.7 +    Copyright   1997  University of Cambridge
    13.8 +
    13.9 +Emulation of HOL's abstract syntax functions
   13.10 +*)
   13.11 +
   13.12  signature USyntax_sig =
   13.13  sig
   13.14    structure Utils : Utils_sig
    14.1 --- a/TFL/usyntax.sml	Thu May 22 15:11:56 1997 +0200
    14.2 +++ b/TFL/usyntax.sml	Thu May 22 15:13:16 1997 +0200
    14.3 @@ -1,3 +1,11 @@
    14.4 +(*  Title:      TFL/usyntax
    14.5 +    ID:         $Id$
    14.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
    14.7 +    Copyright   1997  University of Cambridge
    14.8 +
    14.9 +Emulation of HOL's abstract syntax functions
   14.10 +*)
   14.11 +
   14.12  structure USyntax : USyntax_sig =
   14.13  struct
   14.14  
   14.15 @@ -104,7 +112,6 @@
   14.16  
   14.17  
   14.18  (* Construction routines *)
   14.19 -(* fun mk_var{Name,Ty} = Var((Name,0),Ty); *)
   14.20  fun mk_var{Name,Ty} = Free(Name,Ty);
   14.21  val mk_prim_var = Var;
   14.22  
    15.1 --- a/TFL/utils.sig	Thu May 22 15:11:56 1997 +0200
    15.2 +++ b/TFL/utils.sig	Thu May 22 15:13:16 1997 +0200
    15.3 @@ -1,3 +1,11 @@
    15.4 +(*  Title:      TFL/utils
    15.5 +    ID:         $Id$
    15.6 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
    15.7 +    Copyright   1997  University of Cambridge
    15.8 +
    15.9 +Basic utilities
   15.10 +*)
   15.11 +
   15.12  signature Utils_sig =
   15.13  sig
   15.14    (* General error format and reporting mechanism *)
    16.1 --- a/TFL/utils.sml	Thu May 22 15:11:56 1997 +0200
    16.2 +++ b/TFL/utils.sml	Thu May 22 15:13:16 1997 +0200
    16.3 @@ -1,7 +1,10 @@
    16.4 -(*---------------------------------------------------------------------------
    16.5 - * Some common utilities.
    16.6 - *---------------------------------------------------------------------------*)
    16.7 +(*  Title:      TFL/utils
    16.8 +    ID:         $Id$
    16.9 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
   16.10 +    Copyright   1997  University of Cambridge
   16.11  
   16.12 +Basic utilities
   16.13 +*)
   16.14  
   16.15  structure Utils = 
   16.16  struct