isabelle: TFL/rules.sig@4e4ee8a101be (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 *)
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	12	type 'a binding
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	13
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	14	val dest_thm : thm -> term list * term
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	15
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	16	(* Inference rules *)
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	17	val REFL :cterm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	18	val ASSUME :cterm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	19	val MP :thm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	20	val MATCH_MP :thm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	21	val CONJUNCT1 :thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	22	val CONJUNCT2 :thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	23	val CONJUNCTS :thm -> thm list
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	24	val DISCH :cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	25	val UNDISCH :thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	26	val INST_TYPE :typ binding list -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	27	val SPEC :cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	28	val ISPEC :cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	29	val ISPECL :cterm list -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	30	val GEN :cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	31	val GENL :cterm list -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	32	val LIST_CONJ :thm list -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	33
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	34	val SYM : thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	35	val DISCH_ALL : thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	36	val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	37	val SPEC_ALL : thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	38	val GEN_ALL : thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	39	val IMP_TRANS : thm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	40	val PROVE_HYP : thm -> thm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	41
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	42	val CHOOSE : cterm * thm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	43	val EXISTS : cterm * cterm -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	44	val EXISTL : cterm list -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	45	val IT_EXISTS : cterm binding list -> thm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	46
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	47	val EVEN_ORS : thm list -> thm list
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	48	val DISJ_CASESL : thm -> thm list -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	49
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	50	val SUBS : thm list -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	51	val simplify : thm list -> thm -> thm
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	52	val simpl_conv : thm list -> cterm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	53
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	54	(* For debugging my isabelle solver in the conditional rewriter *)
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	55	(*
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	56	val term_ref : term list ref
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	57	val thm_ref : thm list ref
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	58	val mss_ref : meta_simpset list ref
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	59	val tracing :bool ref
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	60	*)
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	61	val CONTEXT_REWRITE_RULE : term * term
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	62	-> {thms:thm list,congs: thm list, th:thm}
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	63	-> thm * term list
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	64	val RIGHT_ASSOC : thm -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	65
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 2112 diff changeset	66	val prove : cterm * tactic -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	67	end;

author	slotosch
	Sun, 25 May 1997 16:57:19 +0200
changeset 3325	4e4ee8a101be
parent 3302	404fe31fd8d2
child 3353	9112a2efb9a3
permissions	-rw-r--r--