isabelle: TFL/rules.sig@96e28b16861c (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
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	48	val SUBS : thm list -> thm -> thm
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3379 diff changeset	49	val simpl_conv : simpset -> thm list -> cterm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	50
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	51	(* 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	52	val term_ref : term list ref
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	53	val thm_ref : thm list ref
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	54	val mss_ref : meta_simpset list ref
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	55	val tracing :bool ref
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3379 diff changeset	56	val CONTEXT_REWRITE_RULE : simpset * term * term * thm * thm list
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3379 diff changeset	57	-> thm -> thm * term list
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	58	val RIGHT_ASSOC : thm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	59
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	60	val prove : cterm * tactic -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	61	end;

author	paulson
	Fri, 17 Oct 1997 11:00:50 +0200
changeset 3913	96e28b16861c
parent 3405	2cccd0e3e9ea
child 6498	1ebbe18fe236
permissions	-rw-r--r--