TFL/tfl.sig
author paulson
Thu, 05 Jun 1997 13:27:28 +0200
changeset 3405 2cccd0e3e9ea
parent 3391 5e45dd3b64e9
child 3459 112cbb8301dc
permissions -rw-r--r--
Numerous simplifications and removal of HOL-isms Addition of the "simpset" feature (replacing references to \!simpset)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3302
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     1
(*  Title:      TFL/tfl
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     2
    ID:         $Id$
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     4
    Copyright   1997  University of Cambridge
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     5
3391
5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents: 3333
diff changeset
     6
Main module
3302
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     7
*)
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3245
diff changeset
     8
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     9
signature TFL_sig =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    10
sig
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    11
   datatype pattern = GIVEN of term * int
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    12
                    | OMITTED of term * int
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
3391
5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents: 3333
diff changeset
    14
   val mk_functional : theory -> term list
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    15
                       -> {functional:term,
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
                           pats: pattern list}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    18
   val wfrec_definition0 : theory -> string -> term -> term -> theory
3191
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
    19
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    20
   val post_definition : simpset -> theory * (thm * pattern list)
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    21
				 -> {theory : theory,
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    22
				     rules  : thm, 
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    23
				       TCs  : term list list,
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    24
			     full_pats_TCs  : (term * term list) list, 
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    25
				  patterns  : pattern list}
3191
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
    26
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    27
(*CURRENTLY UNUSED
3391
5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents: 3333
diff changeset
    28
   val wfrec_eqns : theory -> term list
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    29
                     -> {WFR : term, 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    30
                         proto_def : term,
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    31
                         extracta :(thm * term list) list,
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
                         pats  : pattern list}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    33
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    34
   val lazyR_def : theory
3391
5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents: 3333
diff changeset
    35
                   -> term list
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    36
                   -> {theory:theory,
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    37
                       rules :thm,
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    38
                           R :term,
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    39
                       full_pats_TCs :(term * term list) list, 
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    40
                       patterns: pattern list}
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    41
---------------------*)
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    42
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    43
   val mk_induction : theory -> term -> term -> (term * term list) list -> thm
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    44
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    45
   val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    46
                     -> theory 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    47
                      -> {rules:thm, induction:thm, TCs:term list list}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    48
                       -> {rules:thm, induction:thm, nested_tcs:thm list}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    49
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    50
   structure Context
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    51
     : sig
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    52
         val read : unit -> thm list
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    53
         val write : thm list -> unit
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    54
       end
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    55
end;