isabelle: TFL/tfl.sig@1056cbbaeb29 (annotated)

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
8622 870a58dd0ddd the simplification rules returned from TFL are now paired with the row they nipkow parents: 6498 diff changeset	18	type pattern
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	19
3391 5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const paulson parents: 3333 diff changeset	20	val mk_functional : theory -> term list
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	21	-> {functional:term,
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	22	pats: pattern list}
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	23
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	24	val wfrec_definition0 : theory -> string -> term -> term -> theory
3191 14bd6e5985f1 TFL now integrated with HOL (more work needed) paulson parents: 2112 diff changeset	25
6498 1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	26	val post_definition : thm list -> theory * (thm * pattern list)
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	27	-> {theory : theory,
8622 870a58dd0ddd the simplification rules returned from TFL are now paired with the row they nipkow parents: 6498 diff changeset	28	rules : thm,
870a58dd0ddd the simplification rules returned from TFL are now paired with the row they nipkow parents: 6498 diff changeset	29	rows : int list,
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	30	TCs : term list list,
8622 870a58dd0ddd the simplification rules returned from TFL are now paired with the row they nipkow parents: 6498 diff changeset	31	full_pats_TCs : (term * term list) list}
3191 14bd6e5985f1 TFL now integrated with HOL (more work needed) paulson parents: 2112 diff changeset	32
6498 1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	33	val wfrec_eqns : theory -> xstring
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	34	-> thm list (* congruence rules *)
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	35	-> term list
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	36	-> {WFR : term, SV : term list,
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	37	proto_def : term,
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	38	extracta :(thm * term list) list,
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	39	pats : pattern list}
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	40
6498 1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	41	val lazyR_def : theory -> xstring
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	42	-> thm list (* congruence rules *)
3391 5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const paulson parents: 3333 diff changeset	43	-> term list
6498 1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	44	-> {theory : theory,
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	45	rules : thm,
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	46	R : term,
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	47	SV : term list,
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	48	full_pats_TCs : (term * term list) list,
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	49	patterns : pattern list}
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	50
6498 1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	51	val mk_induction : theory
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	52	-> {fconst:term,
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	53	R : term,
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	54	SV : term list,
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	55	pat_TCs_list : (term * term list) list}
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3459 diff changeset	56	-> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	57
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	58	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	59	-> theory
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	60	-> {rules:thm, induction:thm, TCs:term list list}
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	61	-> {rules:thm, induction:thm, nested_tcs:thm list}
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	62	end;

author	oheimb
	Fri, 02 Jun 2000 17:46:32 +0200
changeset 9020	1056cbbaeb29
parent 8622	870a58dd0ddd
child 9640	8c6cf4f01644
permissions	-rw-r--r--