TFL/rules.sig
changeset 3245 241838c01caf
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
equal deleted inserted replaced
3244:71b760618f30 3245:241838c01caf
     1 signature Rules_sig =
     1 signature Rules_sig =
     2 sig
     2 sig
     3 (*  structure USyntax : USyntax_sig *)
     3 (*  structure USyntax : USyntax_sig *)
     4   type Type
       
     5   type Preterm
       
     6   type Term
       
     7   type Thm
       
     8   type Tactic
       
     9   type 'a binding
     4   type 'a binding
    10 
     5 
    11   val dest_thm : Thm -> Preterm list * Preterm
     6   val dest_thm : thm -> term list * term
    12 
     7 
    13   (* Inference rules *)
     8   (* Inference rules *)
    14   val REFL      :Term -> Thm
     9   val REFL      :cterm -> thm
    15   val ASSUME    :Term -> Thm
    10   val ASSUME    :cterm -> thm
    16   val MP        :Thm -> Thm -> Thm
    11   val MP        :thm -> thm -> thm
    17   val MATCH_MP  :Thm -> Thm -> Thm
    12   val MATCH_MP  :thm -> thm -> thm
    18   val CONJUNCT1 :Thm -> Thm
    13   val CONJUNCT1 :thm -> thm
    19   val CONJUNCT2 :Thm -> Thm
    14   val CONJUNCT2 :thm -> thm
    20   val CONJUNCTS :Thm -> Thm list
    15   val CONJUNCTS :thm -> thm list
    21   val DISCH     :Term -> Thm -> Thm
    16   val DISCH     :cterm -> thm -> thm
    22   val UNDISCH   :Thm  -> Thm
    17   val UNDISCH   :thm  -> thm
    23   val INST_TYPE :Type binding list -> Thm -> Thm
    18   val INST_TYPE :typ binding list -> thm -> thm
    24   val SPEC      :Term -> Thm -> Thm
    19   val SPEC      :cterm -> thm -> thm
    25   val ISPEC     :Term -> Thm -> Thm
    20   val ISPEC     :cterm -> thm -> thm
    26   val ISPECL    :Term list -> Thm -> Thm
    21   val ISPECL    :cterm list -> thm -> thm
    27   val GEN       :Term -> Thm -> Thm
    22   val GEN       :cterm -> thm -> thm
    28   val GENL      :Term list -> Thm -> Thm
    23   val GENL      :cterm list -> thm -> thm
    29   val BETA_RULE :Thm -> Thm
    24   val LIST_CONJ :thm list -> thm
    30   val LIST_CONJ :Thm list -> Thm
       
    31 
    25 
    32   val SYM : Thm -> Thm
    26   val SYM : thm -> thm
    33   val DISCH_ALL : Thm -> Thm
    27   val DISCH_ALL : thm -> thm
    34   val FILTER_DISCH_ALL : (Preterm -> bool) -> Thm -> Thm
    28   val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
    35   val SPEC_ALL  : Thm -> Thm
    29   val SPEC_ALL  : thm -> thm
    36   val GEN_ALL   : Thm -> Thm
    30   val GEN_ALL   : thm -> thm
    37   val IMP_TRANS : Thm -> Thm -> Thm
    31   val IMP_TRANS : thm -> thm -> thm
    38   val PROVE_HYP : Thm -> Thm -> Thm
    32   val PROVE_HYP : thm -> thm -> thm
    39 
    33 
    40   val CHOOSE : Term * Thm -> Thm -> Thm
    34   val CHOOSE : cterm * thm -> thm -> thm
    41   val EXISTS : Term * Term -> Thm -> Thm
    35   val EXISTS : cterm * cterm -> thm -> thm
    42   val EXISTL : Term list -> Thm -> Thm
    36   val EXISTL : cterm list -> thm -> thm
    43   val IT_EXISTS : Term binding list -> Thm -> Thm
    37   val IT_EXISTS : cterm binding list -> thm -> thm
    44 
    38 
    45   val EVEN_ORS : Thm list -> Thm list
    39   val EVEN_ORS : thm list -> thm list
    46   val DISJ_CASESL : Thm -> Thm list -> Thm
    40   val DISJ_CASESL : thm -> thm list -> thm
    47 
    41 
    48   val SUBS : Thm list -> Thm -> Thm
    42   val SUBS : thm list -> thm -> thm
    49   val simplify : Thm list -> Thm -> Thm
    43   val simplify : thm list -> thm -> thm
    50   val simpl_conv : Thm list -> Term -> Thm
    44   val simpl_conv : thm list -> cterm -> thm
    51 
    45 
    52 (* For debugging my isabelle solver in the conditional rewriter *)
    46 (* For debugging my isabelle solver in the conditional rewriter *)
    53 (*
    47 (*
    54   val term_ref : Preterm list ref
    48   val term_ref : term list ref
    55   val thm_ref : Thm list ref
    49   val thm_ref : thm list ref
    56   val mss_ref : meta_simpset list ref
    50   val mss_ref : meta_simpset list ref
    57   val tracing :bool ref
    51   val tracing :bool ref
    58 *)
    52 *)
    59   val CONTEXT_REWRITE_RULE : Preterm * Preterm
    53   val CONTEXT_REWRITE_RULE : term * term
    60                              -> {thms:Thm list,congs: Thm list, th:Thm} 
    54                              -> {thms:thm list,congs: thm list, th:thm} 
    61                              -> Thm * Preterm list
    55                              -> thm * term list
    62   val RIGHT_ASSOC : Thm -> Thm 
    56   val RIGHT_ASSOC : thm -> thm 
    63 
    57 
    64   val prove : Term * Tactic -> Thm
    58   val prove : cterm * tactic -> thm
    65 end;
    59 end;