TFL/tfl.sig
author wenzelm
Wed, 30 Jun 1999 12:22:31 +0200
changeset 6857 6e6eb8d92377
parent 6498 1ebbe18fe236
child 8622 870a58dd0ddd
permissions -rw-r--r--
added sync marker;
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
6498
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    11
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    12
   val trace : bool ref
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    13
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    14
   val default_simps : thm list      (*simprules used for deriving rules...*)
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    15
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    16
   val congs : thm list -> thm list  (*fn to make congruent rules*)
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    17
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    18
   datatype pattern = GIVEN of term * int
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    19
                    | OMITTED of term * int
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
3391
5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents: 3333
diff changeset
    21
   val mk_functional : theory -> term list
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    22
                       -> {functional:term,
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
                           pats: pattern list}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    25
   val wfrec_definition0 : theory -> string -> term -> term -> theory
3191
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
    26
6498
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    27
   val post_definition : thm list -> theory * (thm * pattern list)
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    28
				  -> {theory : theory,
3405
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    29
				     rules  : thm, 
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    30
				       TCs  : term list list,
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    31
			     full_pats_TCs  : (term * term list) list, 
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms
paulson
parents: 3391
diff changeset
    32
				  patterns  : pattern list}
3191
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
    33
6498
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    34
   val wfrec_eqns : theory -> xstring
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    35
	             -> thm list (* congruence rules *)
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    36
                     -> term list
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    37
                     -> {WFR : term,  SV : term list,
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    38
                         proto_def : term,
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    39
                         extracta :(thm * term list) list,
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    40
                         pats  : pattern list}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    41
6498
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    42
   val lazyR_def : theory -> xstring
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    43
	           -> thm list (* congruence rules *)
3391
5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents: 3333
diff changeset
    44
                   -> term list
6498
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    45
                   -> {theory : theory,
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    46
                       rules : thm,
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    47
                       R : term, 
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    48
                       SV : term list,
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    49
                       full_pats_TCs : (term * term list) list, 
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    50
                       patterns : pattern list}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    51
6498
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    52
   val mk_induction : theory 
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    53
                       -> {fconst:term,
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    54
                           R : term,
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    55
                           SV : term list,
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    56
                           pat_TCs_list : (term * term list) list}
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3459
diff changeset
    57
                       -> thm
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    58
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    59
   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
    60
                     -> theory 
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    61
                      -> {rules:thm, induction:thm, TCs:term list list}
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    62
                       -> {rules:thm, induction:thm, nested_tcs:thm list}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    63
end;