ProofManagement Module

Namespace: HOL
Assembly: nholz.dll

Functions and values

Function or value Description

InstTmLstThmFnForward lbl jf xs t2

Full Usage: InstTmLstThmFnForward lbl jf xs t2

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
xs : (term * term) list
t2 : Proof Tree
Returns: Proof Tree

ThmLstFnForward lbl jf xs

Full Usage: ThmLstFnForward lbl jf xs

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
xs : Proof Tree list
Returns: Proof Tree

TmLstThmFnForward lbl jf xs t2

Full Usage: TmLstThmFnForward lbl jf xs t2

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
xs : term list
t2 : Proof Tree
Returns: Proof Tree

TmThmThmFnForward lbl jf t1 t2 t3

Full Usage: TmThmThmFnForward lbl jf t1 t2 t3

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
t1 : term
t2 : Proof Tree
t3 : Proof Tree
Returns: Proof Tree

add_asm_rule_bk ind loc

Full Usage: add_asm_rule_bk ind loc

Parameters:
Returns: Proof Location
ind : int
loc : Proof Location
Returns: Proof Location

add_asm_rule_fd

Full Usage: add_asm_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

assume_rule_bk loc

Full Usage: assume_rule_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

assume_rule_fd t

Full Usage: assume_rule_fd t

Parameters:
Returns: Proof Tree
t : term
Returns: Proof Tree

by thm lbl loc

Full Usage: by thm lbl loc

Parameters:
Returns: Proof Location
thm : thm
lbl : string
loc : Proof Location
Returns: Proof Location

choose_rule_bk ind1 ind2 pind (ys, xs) loc

Full Usage: choose_rule_bk ind1 ind2 pind (ys, xs) loc

Parameters:
    ind1 : int list
    ind2 : int list
    pind : int
    ys : string
    xs : string
    loc : (Exp * string * InfRule) Location

Returns: (Exp * string * InfRule) Location
ind1 : int list
ind2 : int list
pind : int
ys : string
xs : string
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

choose_rule_fd

Full Usage: choose_rule_fd

Returns: term -> Proof Tree -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree -> Proof Tree

conj_rule_bk ind1 ind2 loc

Full Usage: conj_rule_bk ind1 ind2 loc

Parameters:
Returns: (Exp * string * InfRule) Location
ind1 : int list
ind2 : int list
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

conj_rule_fd

Full Usage: conj_rule_fd

Returns: Proof Tree -> Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree -> Proof Tree

conjunct1_rule_bk t2 loc

Full Usage: conjunct1_rule_bk t2 loc

Parameters:
Returns: Proof Location
t2 : string
loc : Proof Location
Returns: Proof Location

conjunct1_rule_fd

Full Usage: conjunct1_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

conjunct2_rule_bk t1 loc

Full Usage: conjunct2_rule_bk t1 loc

Parameters:
Returns: Proof Location
t1 : string
loc : Proof Location
Returns: Proof Location

conjunct2_rule_fd

Full Usage: conjunct2_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

contr_rule_bk loc

Full Usage: contr_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

contr_rule_fd

Full Usage: contr_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

deduct_antisym_rule_bk ind1 ind2 loc

Full Usage: deduct_antisym_rule_bk ind1 ind2 loc

Parameters:
Returns: (Exp * string * InfRule) Location
ind1 : int list
ind2 : int list
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

deduct_antisym_rule_fd t1 t2

Full Usage: deduct_antisym_rule_fd t1 t2

Parameters:
Returns: Proof Tree
t1 : Proof Tree
t2 : Proof Tree
Returns: Proof Tree

deduct_contrapos_rule_bk ind loc

Full Usage: deduct_contrapos_rule_bk ind loc

Parameters:
Returns: (Exp * string * InfRule) Location
ind : int
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

deduct_contrapos_rule_fd

Full Usage: deduct_contrapos_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

disch_rule_bk loc

Full Usage: disch_rule_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

disch_rule_fd

Full Usage: disch_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

disj1_rule_bk loc

Full Usage: disj1_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

disj1_rule_fd

Full Usage: disj1_rule_fd

Returns: Proof Tree -> term -> Proof Tree
Returns: Proof Tree -> term -> Proof Tree

disj2_rule_bk loc

Full Usage: disj2_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

disj2_rule_fd

Full Usage: disj2_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

disj_cases_rule_bk ind1 ind2 ind3 disj1 disj2 loc

Full Usage: disj_cases_rule_bk ind1 ind2 ind3 disj1 disj2 loc

Parameters:
    ind1 : int list
    ind2 : int list
    ind3 : int list
    disj1 : string
    disj2 : string
    loc : (Exp * string * InfRule) Location

Returns: (Exp * string * InfRule) Location
ind1 : int list
ind2 : int list
ind3 : int list
disj1 : string
disj2 : string
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

disj_cases_rule_fd

Full Usage: disj_cases_rule_fd

Returns: Proof Tree -> Proof Tree -> Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree -> Proof Tree -> Proof Tree

eq_mp_rule_bk ind1 ind2 t2 loc

Full Usage: eq_mp_rule_bk ind1 ind2 t2 loc

Parameters:
    ind1 : int list
    ind2 : int list
    t2 : string
    loc : Proof Location

Returns: Proof Location
ind1 : int list
ind2 : int list
t2 : string
loc : Proof Location
Returns: Proof Location

eq_mp_rule_fd t1 t2

Full Usage: eq_mp_rule_fd t1 t2

Parameters:
Returns: Proof Tree
t1 : Proof Tree
t2 : Proof Tree
Returns: Proof Tree

eqf_elim_rule_bk loc

Full Usage: eqf_elim_rule_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

eqf_elim_rule_fd

Full Usage: eqf_elim_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

eqf_intro_rule_bk loc

Full Usage: eqf_intro_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

eqf_intro_rule_fd

Full Usage: eqf_intro_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

eqt_intro_rule_bk loc

Full Usage: eqt_intro_rule_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

eqt_intro_rule_fd

Full Usage: eqt_intro_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

eta_conv_bk loc

Full Usage: eta_conv_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

eta_conv_fd t

Full Usage: eta_conv_fd t

Parameters:
Returns: Proof Tree
t : term
Returns: Proof Tree

exists_rule_bk ts loc

Full Usage: exists_rule_bk ts loc

Parameters:
Returns: Proof Location
ts : string
loc : Proof Location
Returns: Proof Location

exists_rule_fd

Full Usage: exists_rule_fd

Returns: term -> term -> Proof Tree -> Proof Tree
Returns: term -> term -> Proof Tree -> Proof Tree

findExp x loc

Full Usage: findExp x loc

Parameters:
Returns: Proof Location option
x : Exp
loc : Proof Location
Returns: Proof Location option

focus_goal loc

Full Usage: focus_goal loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

gen_rule_bk loc

Full Usage: gen_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

gen_rule_fd

Full Usage: gen_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

instTermlst_fd xs

Full Usage: instTermlst_fd xs

Parameters:
Returns: (Exp * string * InfRule) Tree
xs : (term * term) list
Returns: (Exp * string * InfRule) Tree

instTyLstThmFnForward lbl jf xs t2

Full Usage: instTyLstThmFnForward lbl jf xs t2

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
xs : (hol_type * hol_type) list
t2 : Proof Tree
Returns: Proof Tree

instTyLst_fd t

Full Usage: instTyLst_fd t

Parameters:
Returns: (Exp * string * InfRule) Tree
t : (hol_type * hol_type) list
Returns: (Exp * string * InfRule) Tree

inst_rule_bk theta loc

Full Usage: inst_rule_bk theta loc

Parameters:
Returns: (Exp * string * InfRule) Location
theta : (term * term) list
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

inst_rule_fd

Full Usage: inst_rule_fd

Returns: (term * term) list -> Proof Tree -> Proof Tree
Returns: (term * term) list -> Proof Tree -> Proof Tree

inst_type_rule_fd xs

Full Usage: inst_type_rule_fd xs

Parameters:
Returns: Proof Tree -> Proof Tree
xs : (hol_type * hol_type) list
Returns: Proof Tree -> Proof Tree

list_gen_rule_bk loc

Full Usage: list_gen_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

list_gen_rule_fd

Full Usage: list_gen_rule_fd

Returns: term list -> Proof Tree -> Proof Tree
Returns: term list -> Proof Tree -> Proof Tree

list_spec_rule_bk txs loc

Full Usage: list_spec_rule_bk txs loc

Parameters:
Returns: (Exp * string * InfRule) Location
txs : (string * string) list
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

list_spec_rule_fd

Full Usage: list_spec_rule_fd

Returns: term list -> Proof Tree -> Proof Tree
Returns: term list -> Proof Tree -> Proof Tree

list_trans_rule_fd

Full Usage: list_trans_rule_fd

Returns: Proof Tree list -> Proof Tree
Returns: Proof Tree list -> Proof Tree

mk_abs_rule_bk loc

Full Usage: mk_abs_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

mk_abs_rule_fd

Full Usage: mk_abs_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

mk_bin_rule_bk ind1 ind2 loc

Full Usage: mk_bin_rule_bk ind1 ind2 loc

Parameters:
Returns: (Exp * string * InfRule) Location
ind1 : int list
ind2 : int list
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

mk_bin_rule_fd

Full Usage: mk_bin_rule_fd

Returns: term -> Proof Tree -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree -> Proof Tree

mk_comb1_rule_bk loc

Full Usage: mk_comb1_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

mk_comb1_rule_fd

Full Usage: mk_comb1_rule_fd

Returns: Proof Tree -> term -> Proof Tree
Returns: Proof Tree -> term -> Proof Tree

mk_comb2_rule_bk loc

Full Usage: mk_comb2_rule_bk loc

Parameters:
Returns: (Exp * string * InfRule) Location
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

mk_comb2_rule_fd

Full Usage: mk_comb2_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

mp_rule_bk ind1 ind2 t2 loc

Full Usage: mp_rule_bk ind1 ind2 t2 loc

Parameters:
    ind1 : int list
    ind2 : int list
    t2 : string
    loc : Proof Location

Returns: Proof Location
ind1 : int list
ind2 : int list
t2 : string
loc : Proof Location
Returns: Proof Location

mp_rule_fd t1 t2

Full Usage: mp_rule_fd t1 t2

Parameters:
Returns: Proof Tree
t1 : Proof Tree
t2 : Proof Tree
Returns: Proof Tree

not_elim_rule_bk loc

Full Usage: not_elim_rule_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

not_elim_rule_fd

Full Usage: not_elim_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

not_intro_rule_bk loc

Full Usage: not_intro_rule_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

not_intro_rule_fd

Full Usage: not_intro_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

prove loc

Full Usage: prove loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

prove' loc

Full Usage: prove' loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

refl_conv_bk loc

Full Usage: refl_conv_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

refl_conv_fd t

Full Usage: refl_conv_fd t

Parameters:
Returns: Proof Tree
t : term
Returns: Proof Tree

select exp loc

Full Usage: select exp loc

Parameters:
Returns: Proof Location
exp : Exp
loc : Proof Location
Returns: Proof Location

select_rule_bk t1 loc

Full Usage: select_rule_bk t1 loc

Parameters:
Returns: Proof Location
t1 : string
loc : Proof Location
Returns: Proof Location

select_rule_fd

Full Usage: select_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

spec_rule_bk (ts, xs) newT loc

Full Usage: spec_rule_bk (ts, xs) newT loc

Parameters:
Returns: (Exp * string * InfRule) Location
ts : string
xs : string
newT : string
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

spec_rule_fd

Full Usage: spec_rule_fd

Returns: term -> Proof Tree -> Proof Tree
Returns: term -> Proof Tree -> Proof Tree

start_proof (xs, s)

Full Usage: start_proof (xs, s)

Parameters:
    xs : string list
    s : string

Returns: Proof Location
xs : string list
s : string
Returns: Proof Location

sym_rule_bk loc

Full Usage: sym_rule_bk loc

Parameters:
Returns: Proof Location
loc : Proof Location
Returns: Proof Location

sym_rule_fd

Full Usage: sym_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree

term_fd t

Full Usage: term_fd t

Parameters:
Returns: (Exp * string * InfRule) Tree
t : term
Returns: (Exp * string * InfRule) Tree

termlst_fd xs

Full Usage: termlst_fd xs

Parameters:
Returns: (Exp * string * InfRule) Tree
xs : term list
Returns: (Exp * string * InfRule) Tree

thmFnForward lbl jf t

Full Usage: thmFnForward lbl jf t

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
t : Proof Tree
Returns: Proof Tree

thmThmFnForward lbl jf t1 t2

Full Usage: thmThmFnForward lbl jf t1 t2

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
t1 : Proof Tree
t2 : Proof Tree
Returns: Proof Tree

thmThmThmFnForward lbl jf t1 t2 t3

Full Usage: thmThmThmFnForward lbl jf t1 t2 t3

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
t1 : Proof Tree
t2 : Proof Tree
t3 : Proof Tree
Returns: Proof Tree

thmTmFnForward lbl jf tr1 t

Full Usage: thmTmFnForward lbl jf tr1 t

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
tr1 : Proof Tree
t : term
Returns: Proof Tree

thm_fd lbl th

Full Usage: thm_fd lbl th

Parameters:
    lbl : string
    th : thm

Returns: Proof Tree
lbl : string
th : thm
Returns: Proof Tree

tmFnForward lbl jf t

Full Usage: tmFnForward lbl jf t

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
t : term
Returns: Proof Tree

tmThm2ThmFnForward lbl jf t1 t2 t3

Full Usage: tmThm2ThmFnForward lbl jf t1 t2 t3

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
t1 : term
t2 : Proof Tree
t3 : Proof Tree
Returns: Proof Tree

tmThmFnForward lbl jf t t2

Full Usage: tmThmFnForward lbl jf t t2

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
t : term
t2 : Proof Tree
Returns: Proof Tree

tmTmThmFnForward lbl jf t1 t2 t3

Full Usage: tmTmThmFnForward lbl jf t1 t2 t3

Parameters:
Returns: Proof Tree
lbl : string
jf : InfRule
t1 : term
t2 : term
t3 : Proof Tree
Returns: Proof Tree

trans_rule_bk t' loc

Full Usage: trans_rule_bk t' loc

Parameters:
Returns: (Exp * string * InfRule) Location
t' : string
loc : (Exp * string * InfRule) Location
Returns: (Exp * string * InfRule) Location

trans_rule_fd

Full Usage: trans_rule_fd

Returns: Proof Tree -> Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree -> Proof Tree

undisch_rule_bk ind loc

Full Usage: undisch_rule_bk ind loc

Parameters:
Returns: Proof Location
ind : int
loc : Proof Location
Returns: Proof Location

undisch_rule_fd

Full Usage: undisch_rule_fd

Returns: Proof Tree -> Proof Tree
Returns: Proof Tree -> Proof Tree