isabelle: TFL/rules.sig@084abf3d0eff (annotated)

3302 404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	1	(* Title: TFL/rules
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
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	6	Emulation of HOL inference rules for TFL
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 Rules_sig =
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	10	sig
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	11	(* structure USyntax : USyntax_sig *)
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	12	val dest_thm : thm -> term list * term
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	13
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	14	(* Inference rules *)
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	15	val REFL :cterm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	16	val ASSUME :cterm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	17	val MP :thm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	18	val MATCH_MP :thm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	19	val CONJUNCT1 :thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	20	val CONJUNCT2 :thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	21	val CONJUNCTS :thm -> thm list
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	22	val DISCH :cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	23	val UNDISCH :thm -> thm
3353 9112a2efb9a3 Removal of module Mask and datatype binding with its constructor \|-> paulson parents: 3302 diff changeset	24	val INST_TYPE :(typ*typ)list -> thm -> thm
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	25	val SPEC :cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	26	val ISPEC :cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	27	val ISPECL :cterm list -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	28	val GEN :cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	29	val GENL :cterm list -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	30	val LIST_CONJ :thm list -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	31
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	32	val SYM : thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	33	val DISCH_ALL : thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	34	val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	35	val SPEC_ALL : thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	36	val GEN_ALL : thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	37	val IMP_TRANS : thm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	38	val PROVE_HYP : thm -> thm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	39
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	40	val CHOOSE : cterm * thm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	41	val EXISTS : cterm * cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	42	val EXISTL : cterm list -> thm -> thm
3353 9112a2efb9a3 Removal of module Mask and datatype binding with its constructor \|-> paulson parents: 3302 diff changeset	43	val IT_EXISTS : (cterm*cterm) list -> thm -> 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: 2112 diff changeset	45	val EVEN_ORS : thm list -> thm list
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	46	val DISJ_CASESL : thm -> thm list -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	47
7250 a4bd83b25d23 new version from Konrad with "lazy" (deferred) definitons paulson parents: 6498 diff changeset	48	val list_beta_conv : cterm -> cterm list -> thm
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	49	val SUBS : thm list -> thm -> thm
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3379 diff changeset	50	val simpl_conv : simpset -> thm list -> cterm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	51
7262 a05dc63ca29b from Konrad: support for schematic definitions paulson parents: 7260 diff changeset	52	val rbeta : thm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	53	(* For debugging my isabelle solver in the conditional rewriter *)
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	54	val term_ref : term list ref
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	55	val thm_ref : thm list ref
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	56	val mss_ref : meta_simpset list ref
6498 1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3405 diff changeset	57	val tracing : bool ref
1ebbe18fe236 Now for recdefs that omit the WF relation; paulson parents: 3405 diff changeset	58	val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3379 diff changeset	59	-> thm -> thm * term list
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	60	val RIGHT_ASSOC : thm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	61
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	62	val prove : cterm * tactic -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	63	end;

author	paulson
	Wed, 28 Jun 2000 10:37:52 +0200
changeset 9158	084abf3d0eff
parent 7262	a05dc63ca29b
permissions	-rw-r--r--