内核对象与定理

EN | 中文

内核对象与定理

proof_kernel.hproof_kernel.h 是证明块的词汇表。[[cst::proof]][[cst::proof]] 函数并不以语法形式书写分离逻辑公式，而是把它们构造为 HOL 对象；逻辑内置的每一个对象——连接词、堆命题常量、C 类型、内核自带的定理——都通过本头文件声明的访问器进入 C 代码。

这里的东西只有三类。不透明句柄类型（termterm、thmthm、typetype，以及与之配套的列表与配对类型）是其余各头文件共同流通的货币。常量访问器——返回 termterm 或 typetype 的函数——命名证明用来组装待证目标的语法片段。定理访问器——返回 thmthm 的函数——命名内核已经证明的规则，也就是证明所引用的对象。这里不执行任何推理：应用定理的规则在 hol_prover_client.hhol_prover_client.h 中，消耗其结果的引擎调用在 symexec.hsymexec.h 中。

本页是按头文件顺序编排、以名称为索引的目录。它说明声明了什么、以什么名称声明，以及在头文件有记录时给出访问器所返回的确切 HOL 陈述。它不解释逻辑本身。概念层面的讲解 ——把规则按作用分组、把基本定律与其推论分开、把公理标注为公理——见证明规则页；许多定理所涉及的谓词见带类型的内存谓词页。

如何阅读一个条目

每个条目先原样给出头文件中的 C 声明，随后是头文件注释为该访问器记录的 HOL 陈述—— 可能是定理的陈述、常量的类型，也可能是一句说明该访问器返回定义的注记。种类徽标把 theoremtheorem 与 term-constterm-const、typetype、macromacro 区分开来，第二个 derivedderived 徽标则标出头文件标注了 @derived@derived 的条目。右侧的灰色标记是该条目在仓库内置头文件副本中的源位置，因此任何条目都可以对照它的来源文件核查。

每个条目同时也是一个以自身命名的锚点：hsep_assochsep_assoc 的访问器位于本页的 #api-hsep_assoc#api-hsep_assoc 片段处，因此可以按名称链接到某一条规则。

不透明类型

每一个逻辑对象都存在于证明器之中，而不在 C 进程里。C 侧持有的是句柄：指向头文件只声明、从不定义的结构体的指针。这是刻意的设计——证明代码无法检查、分配或伪造一个 termterm，只能把它交回内核，LCF 规范正是这样跨越语言边界继续成立的（见基于 LCF 架构的证明）。


typedef struct hol_term term;
typedef struct hol_theorem thm;
typedef struct hol_type type;
typedef struct hol_conversion conv;
typedef struct hol_term_pair term_pair;
typedef struct hol_thm_pair thm_pair;
typedef struct hol_type_pair type_pair;
typedef struct hol_instantiation instantiation;
typedef struct new_datatype_definition_results indtype;
typedef struct new_inductive_definition_results inddef;


typedef struct hol_term term;
typedef struct hol_theorem thm;
typedef struct hol_type type;
typedef struct hol_conversion conv;
typedef struct hol_term_pair term_pair;
typedef struct hol_thm_pair thm_pair;
typedef struct hol_type_pair type_pair;
typedef struct hol_instantiation instantiation;
typedef struct new_datatype_definition_results indtype;
typedef struct new_inductive_definition_results inddef;

termterm 是 HOL 项——公式、表达式或 hprophprop。thmthm 是定理：内核已经证明的相继式，也是 C 代码唯一无法自行构造、只能经推理规则得到的类型。typetype 是 HOL 类型，如 :hprop:hprop 或 :ctype:ctype。convconv 是变换，即从项映到等式定理的重写函数；变换组合子见 HOL API：变换与求解器页。

最后三个是结果，而非语法。instantiationinstantiation 是把一个项与另一个项匹配所产生、并由实例化规则消耗的替换。indtypeindtype 与 inddefinddef 封装 new_datatype_definitionnew_datatype_definition 和 new_inductive_definitionnew_inductive_definition 的返回结果——新定义的数据类型或归纳关系所对应的归纳定理、递归定理与分情况定理——因此它们是带若干定理字段的结构体，而不是单个句柄。

配对与列表是批量操作的参数类型。一个 term_pairterm_pair 是替换的一个分量；六个列表别名是对 hol_prover_client.hhol_prover_client.h 所声明的向量类型的重命名：


typedef hol_term_list term_list;
typedef hol_theorem_list thm_list;
typedef hol_type_list type_list;
typedef hol_term_pair_list term_pair_list;
typedef hol_thm_pair_list thm_pair_list;
typedef hol_type_pair_list type_pair_list;


typedef hol_term_list term_list;
typedef hol_theorem_list thm_list;
typedef hol_type_list type_list;
typedef hol_term_pair_list term_pair_list;
typedef hol_thm_pair_list thm_pair_list;
typedef hol_type_pair_list type_pair_list;

proof_runtime.hproof_runtime.h 的 TERM_LISTTERM_LIST 与 THM_LISTTHM_LIST 构造子所生成的正是这些类型（见符号执行与运行时 API页）。由于它们是 typedef 而不是声明，这里直接原样引用，而没有作为条目列出：本节以下的全部内容都由头文件中的宏声明与函数声明生成。

访问器宏

本页每一个访问器背后都站着这三个宏。目录之所以整齐划一，原因就在这里：每个常量、每条定理都在首次使用时按名称从证明器取回，且只取一次。

LazyInitmacroproof_kernel.h:24


#define LazyInit(type, name, f, ...) \
  inline type get_##name() {         \
    static bool initialized = false; \
    static type __##name;            \
    if (!initialized) {              \
      initialized = true;            \
      __##name = f(__VA_ARGS__);     \
    }                                \
    return __##name;                 \
  }


#define LazyInit(type, name, f, ...) \
  inline type get_##name() {         \
    static bool initialized = false; \
    static type __##name;            \
    if (!initialized) {              \
      initialized = true;            \
      __##name = f(__VA_ARGS__);     \
    }                                \
    return __##name;                 \
  }

LazyInitTheoremmacroproof_kernel.h:35


#define LazyInitTheorem(name) LazyInit(thm, name, get_theorem_by_name, #name)


#define LazyInitTheorem(name) LazyInit(thm, name, get_theorem_by_name, #name)

__DeclareTheoremmacroproof_kernel.h:37


#define __DeclareTheorem(name) thm get_##name()


#define __DeclareTheorem(name) thm get_##name()

LazyInit(type, name, f, ...)LazyInit(type, name, f, ...) 把 get_<name>()get_<name>() 定义为一个内联函数，其中保存两个函数局部静态变量：一个标志位和缓存下来的对象。首次调用会求值 f(__VA_ARGS__)f(__VA_ARGS__)——一次到证明器的远程过程调用——并保存结果；此后每次调用都直接返回缓存的句柄，不再触碰连接。 LazyInitTheorem(name)LazyInitTheorem(name) 是用于定理的特化：它展开为 LazyInit(thm, name, get_theorem_by_name, #name)LazyInit(thm, name, get_theorem_by_name, #name)，于是取回操作就是在证明器的定理数据库中按定理自身的名称查找，其中 #name#name 把宏参数字符串化。

__DeclareTheorem(name)__DeclareTheorem(name) 是与之对应的声明宏。它展开为 thm get_##name()thm get_##name()，因此头文件中的一行


__DeclareTheorem(hsep_assoc);


__DeclareTheorem(hsep_assoc);

声明的是 thm get_hsep_assoc();thm get_hsep_assoc();，而实现侧用 LazyInitTheorem(hsep_assoc)LazyInitTheorem(hsep_assoc) 提供函数体。整套约定就是这样：内核中名为 TT 的定理，在 C 侧通过 get_T()get_T() 获得。头文件的最后一行执行 #undef __DeclareTheorem#undef __DeclareTheorem，因此该宏对用户代码不可见——它的存在只是为了把头文件写得紧凑。

逻辑连接词

四个访问器以项的形式返回 HOL Light 的布尔连接词。它们是普通的 HOL 常量，并非 C* 新增的东西；证明代码在构造交给判定过程的纯附加条件，或者拆解蕴含形式的待证目标时会用到它们。

get_conj_opterm-constproof_kernel.h:44


term get_conj_op();


term get_conj_op();


/\ : bool->bool->bool


/\ : bool->bool->bool

get_disj_opterm-constproof_kernel.h:47


term get_disj_op();


term get_disj_op();


\/ : bool->bool->bool


\/ : bool->bool->bool

get_iff_opterm-constproof_kernel.h:50


term get_iff_op();


term get_iff_op();


<=> : bool->bool->bool


<=> : bool->bool->bool

get_imp_opterm-constproof_kernel.h:53


term get_imp_op();


term get_imp_op();


==> : bool->bool->bool


==> : bool->bool->bool

返回的是常量本身，而不是应用式：get_conj_op()get_conj_op() 是类型为 bool->bool->boolbool->bool->bool 的运算符 /\/\ ，需要用 HOL API：类型与项页中的项构造子来施加。

堆命题常量

分离逻辑的词汇表。get_hprop_type()get_hprop_type() 返回堆命题的类型 :hprop:hprop；其余访问器返回构造堆命题的各个常量。每个常量的含义见内存模型与断言页；这里给出的是访问器，以及每个常量所带的类型。

get_hprop_typetypeproof_kernel.h:56


type get_hprop_type();


type get_hprop_type();


:hprop


:hprop

get_hfactterm-constproof_kernel.h:59


term get_hfact();


term get_hfact();


fact : bool->hprop


fact : bool->hprop

get_hentailterm-constproof_kernel.h:62


term get_hentail();


term get_hentail();


|-- : hprop->hprop->hprop


|-- : hprop->hprop->hprop

get_hequalterm-constproof_kernel.h:65


term get_hequal();


term get_hequal();


-|- : hprop->hprop->hprop


-|- : hprop->hprop->hprop

get_hconjterm-constproof_kernel.h:68


term get_hconj();


term get_hconj();


** : hprop->hprop->hprop


** : hprop->hprop->hprop

get_hempterm-constproof_kernel.h:71


term get_hemp();


term get_hemp();


emp : hprop


emp : hprop

get_htrueterm-constproof_kernel.h:74


term get_htrue();


term get_htrue();


true : hprop


true : hprop

get_hfalseterm-constproof_kernel.h:77


term get_hfalse();


term get_hfalse();


false : hprop


false : hprop

get_hwandterm-constproof_kernel.h:80


term get_hwand();


term get_hwand();


-* : hprop->hprop->hprop


-* : hprop->hprop->hprop

get_himplterm-constproof_kernel.h:83


term get_himpl();


term get_himpl();


--> : hprop->hprop->hprop


--> : hprop->hprop->hprop

get_horterm-constproof_kernel.h:86


term get_hor();


term get_hor();


|| : hprop->hprop->hprop


|| : hprop->hprop->hprop

get_handterm-constproof_kernel.h:89


term get_hand();


term get_hand();


&& : hprop->hprop->hprop


&& : hprop->hprop->hprop

get_hforallterm-constproof_kernel.h:92


term get_hforall();


term get_hforall();


forall : (A->hprop)->hprop


forall : (A->hprop)->hprop

get_hexiststerm-constproof_kernel.h:95


term get_hexists();


term get_hexists();


exists : (A->hprop)->hprop


exists : (A->hprop)->hprop

get_hpureterm-constproof_kernel.h:98


term get_hpure();


term get_hpure();


pure : bool->hprop


pure : bool->hprop

get_true_termterm-constproof_kernel.h:101


term get_true_term();


term get_true_term();


T : bool


T : bool

get_false_termterm-constproof_kernel.h:104


term get_false_term();


term get_false_term();


F : bool


F : bool

有两处命名细节值得记住。get_hconjget_hconj 返回的是分离合取 **** ，而不是加性合取 ——加性合取 &&&& 对应的是 get_handget_hand。另外，get_hentailget_hentail 与 get_hequalget_hequal 返回 |--|-- 和 -|--|- ，即堆命题之间的蕴含与蕴含等价；头文件中 get_hequalget_hequal 的注释以单引号而非反引号开头，那是头文件里的笔误，并不代表另一个常量。

最后两个根本不是堆命题：get_true_term()get_true_term() 与 get_false_term()get_false_term() 返回布尔常量 TT 和 FF 。它们出现在这里，是因为证明最常用它们来填写纯附加条件——如 pure(T)pure(T)、fact(F)fact(F)——而头文件也正是在此处声明它们的。

C 类型、结构体与字段

逻辑把 C 类型建模为归纳类型 :ctype:ctype 的一个元素，而 data_atdata_at、sizeofsizeof、min_ofmin_of 与 max_ofmax_of 都以它为索引。这些访问器返回该类型及其九个内置构造子，另加用于结构体名与字段名的两个类型。

get_ctype_typetypeproof_kernel.h:343


type get_ctype_type();


type get_ctype_type();


:ctype


:ctype

get_Tcharterm-constproof_kernel.h:346


term get_Tchar();


term get_Tchar();


Tchar : ctype


Tchar : ctype

get_Tucharterm-constproof_kernel.h:349


term get_Tuchar();


term get_Tuchar();


Tuchar : ctype


Tuchar : ctype

get_Tshortterm-constproof_kernel.h:352


term get_Tshort();


term get_Tshort();


Tshort : ctype


Tshort : ctype

get_Tushortterm-constproof_kernel.h:355


term get_Tushort();


term get_Tushort();


Tushort : ctype


Tushort : ctype

get_Tintterm-constproof_kernel.h:358


term get_Tint();


term get_Tint();


Tint : ctype


Tint : ctype

get_Tuintterm-constproof_kernel.h:361


term get_Tuint();


term get_Tuint();


Tuint : ctype


Tuint : ctype

get_Tint64term-constproof_kernel.h:364


term get_Tint64();


term get_Tint64();


Tint64 : ctype


Tint64 : ctype

get_Tuint64term-constproof_kernel.h:367


term get_Tuint64();


term get_Tuint64();


Tuint64 : ctype


Tuint64 : ctype

get_Tptrterm-constproof_kernel.h:370


term get_Tptr();


term get_Tptr();


Tptr : ctype


Tptr : ctype

get_struct_name_typetypeproof_kernel.h:571


type get_struct_name_type();


type get_struct_name_type();


:struct_name


:struct_name

get_field_typetypeproof_kernel.h:574


type get_field_type();


type get_field_type();


:field


:field

整套命名方案就是 TT 前缀这一条：TintTint 是逻辑对 C 的 intint 的称呼，TucharTuchar 对应 unsigned charunsigned char，TptrTptr 对应任意指向类型的指针。接受 struct_namestruct_name 的构造子 TstructTstruct 没有访问器：结构体类型是通过施加它来构造的，而结构体的名称是一个用 cst_add_type_to_headercst_add_type_to_header 注册的 :struct_name:struct_name 常量（见内核头文件页）。get_struct_name_type()get_struct_name_type() 与 get_field_type()get_field_type() 返回这些常量所属的两个类型；头文件把它们声明在最末尾，这里之所以把它们归入本节，是因为它们属于 C 类型词汇，而不属于定理目录。 C* 的扩展页作了完整介绍，包括 field_addrfield_addr 与以 FF 为前缀的字段常量。

定理访问器

头文件的其余部分是定理库：141 个访问器，每个返回一条内核已经证明的定理，每个都在首次使用时按名称从证明器的数据库取回。下面就是这份目录，按头文件顺序排列。

引用其中一条，是证明块做得最多的事：取得 thmthm，再把它交给 hol_prover_client.hhol_prover_client.h 中的推理规则或蕴含求解器。每条规则用来做什么——哪些是分离代数的基本定律，哪些是它们的推论，哪些是 C* 内存模型增设的公理——是证明规则页与带类型的内存谓词页的主题。下面采用的是头文件的顺序，它与那两页所用的概念顺序接近，但并不相同。

HOL 基础

六条通用的 HOL Light 定理，加上关于真与假的两条平凡定理，在这里重新导出，这样证明代码就不必用字符串去查找它们。get_true_thm()get_true_thm() 与 get_false_thm()get_false_thm() 是直接声明的，没有经过 __DeclareTheorem__DeclareTheorem，因此它们的条目名带有 get_get_ 前缀。

get_true_thmtheoremproof_kernel.h:107


thm get_true_thm();


thm get_true_thm();


|- T


|- T

get_false_thmtheoremproof_kernel.h:110


thm get_false_thm();


thm get_false_thm();


|- !t. F ==> t


|- !t. F ==> t

ABS_SIMPtheoremproof_kernel.h:113


thm get_ABS_SIMP();


thm get_ABS_SIMP();


!t1 t2. (\x. t1) t2 = t1


!t1 t2. (\x. t1) t2 = t1

EXCLUDED_MIDDLEtheoremproof_kernel.h:116


thm get_EXCLUDED_MIDDLE();


thm get_EXCLUDED_MIDDLE();


!t. t \/ ~t


!t. t \/ ~t

list_CASEStheoremproof_kernel.h:119


thm get_list_CASES();


thm get_list_CASES();


!l. l = [] \/ (?h t. l = CONS h t)


!l. l = [] \/ (?h t. l = CONS h t)

list_INDUCTtheoremproof_kernel.h:122


thm get_list_INDUCT();


thm get_list_INDUCT();


!P. P [] /\ (!a0 a1. P a1 ==> P (CONS a0 a1)) ==> (!x. P x)


!P. P [] /\ (!a0 a1. P a1 ==> P (CONS a0 a1)) ==> (!x. P x)

num_CASEStheoremproof_kernel.h:125


thm get_num_CASES();


thm get_num_CASES();


!m. m = 0 \/ (?n. m = SUC n)


!m. m = 0 \/ (?n. m = SUC n)

num_INDUCTIONtheoremproof_kernel.h:128


thm get_num_INDUCTION();


thm get_num_INDUCTION();


!P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)


!P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n)

list_INDUCTlist_INDUCT 与 num_INDUCTIONnum_INDUCTION 是关于循环或链式结构的证明会用到的两条归纳原理； list_CASESlist_CASES 与 num_CASESnum_CASES 是与之对应的分情况分析定理。ABS_SIMPABS_SIMP 是等式形式的 beta 归约，EXCLUDED_MIDDLEEXCLUDED_MIDDLE 则使这套逻辑成为经典逻辑。

蕴含与分离合取

骨干部分。蕴含 |--|-- 具有自反性与传递性，并在 -|--|- 意义下具有反对称性；分离合取 **** 满足结合律与交换律，以 empemp 为单位元； -*-* 是它的右伴随；而蕴含对 **** 的任一侧都构成合同关系。

hentail_refltheoremproof_kernel.h:131


thm get_hentail_refl();


thm get_hentail_refl();


!hp. hp |-- hp


!hp. hp |-- hp

hentail_transtheoremproof_kernel.h:134


thm get_hentail_trans();


thm get_hentail_trans();


!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp2 |-- hp3) ==> (hp1 |-- hp3)


!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp2 |-- hp3) ==> (hp1 |-- hp3)

hentail_antisymtheoremproof_kernel.h:137


thm get_hentail_antisym();


thm get_hentail_antisym();


!hp1 hp2. (hp1 |-- hp2) ==> (hp2 |-- hp1) ==> (hp1 -|- hp2)


!hp1 hp2. (hp1 |-- hp2) ==> (hp2 |-- hp1) ==> (hp1 -|- hp2)

hsep_assoctheoremproof_kernel.h:140


thm get_hsep_assoc();


thm get_hsep_assoc();


!hp1 hp2 hp3. (hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)


!hp1 hp2 hp3. (hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)

hsep_commtheoremproof_kernel.h:143


thm get_hsep_comm();


thm get_hsep_comm();


!hp1 hp2. hp1 ** hp2 -|- hp2 ** hp1


!hp1 hp2. hp1 ** hp2 -|- hp2 ** hp1

hsep_hemp_lefttheoremproof_kernel.h:146


thm get_hsep_hemp_left();


thm get_hsep_hemp_left();


!hp. emp ** hp -|- hp


!hp. emp ** hp -|- hp

hsep_hemp_righttheoremproof_kernel.h:149


thm get_hsep_hemp_right();


thm get_hsep_hemp_right();


!hp. hp ** emp -|- hp


!hp. hp ** emp -|- hp

hwand_hsep_adjointtheoremproof_kernel.h:152


thm get_hwand_hsep_adjoint();


thm get_hwand_hsep_adjoint();


!hp1 hp2 hp3. (hp1 ** hp2 |-- hp3) <=> (hp1 |-- hp2 -* hp3)


!hp1 hp2 hp3. (hp1 ** hp2 |-- hp3) <=> (hp1 |-- hp2 -* hp3)

hsep_cancel_lefttheoremproof_kernel.h:155


thm get_hsep_cancel_left();


thm get_hsep_cancel_left();


!hp2 hp2' hp1. (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1 ** hp2')


!hp2 hp2' hp1. (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1 ** hp2')

hsep_cancel_righttheoremproof_kernel.h:158


thm get_hsep_cancel_right();


thm get_hsep_cancel_right();


!hp1 hp1' hp2. (hp1 |-- hp1') ==> (hp1 ** hp2 |-- hp1' ** hp2)


!hp1 hp1' hp2. (hp1 |-- hp1') ==> (hp1 ** hp2 |-- hp1' ** hp2)

hsep_monotonetheoremproof_kernel.h:161


thm get_hsep_monotone();


thm get_hsep_monotone();


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1' ** hp2')


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1' ** hp2')

hsep_cancel_lefthsep_cancel_left 就是本套发展中的框架规则：由 hp2 |-- hp2'hp2 |-- hp2' 得出 hp1 ** hp2 |-- hp1 ** hp2'hp1 ** hp2 |-- hp1 ** hp2'，hp1hp1 原封不动。hsep_cancel_righthsep_cancel_right 在另一侧作框架， hsep_monotonehsep_monotone 则同时在两侧作框架。

真、假与加性连接词

作为堆命题的 truetrue 与 falsefalse 、它们与 purepure 和 factfact 的关系、它们在 **** 之下的吸收行为，以及加性合取 &&&& 、析取 |||| 与蕴含 -->--> 的引入与消去规则。

htrue_deftheoremproof_kernel.h:164


thm get_htrue_def();


thm get_htrue_def();


true -|- pure(T)


true -|- pure(T)

hfalse_deftheoremproof_kernel.h:167


thm get_hfalse_def();


thm get_hfalse_def();


false -|- pure(F)


false -|- pure(F)

htrue_introtheoremproof_kernel.h:170


thm get_htrue_intro();


thm get_htrue_intro();


!hp. hp |-- true


!hp. hp |-- true

htrue_hemptheoremproof_kernel.h:173


thm get_htrue_hemp();


thm get_htrue_hemp();


fact(T) -|- emp


fact(T) -|- emp

hfalse_elimtheoremproof_kernel.h:176


thm get_hfalse_elim();


thm get_hfalse_elim();


!hp. false |-- hp


!hp. false |-- hp

hfact_false_elimtheoremproof_kernel.h:179


thm get_hfact_false_elim();


thm get_hfact_false_elim();


!hp. fact(F) |-- hp


!hp. fact(F) |-- hp

htrue_elim_lefttheoremproof_kernel.h:182


thm get_htrue_elim_left();


thm get_htrue_elim_left();


!hp. fact(T) ** hp -|- hp


!hp. fact(T) ** hp -|- hp

htrue_elim_righttheoremproof_kernel.h:185


thm get_htrue_elim_right();


thm get_htrue_elim_right();


!hp. hp ** fact(T) -|- hp


!hp. hp ** fact(T) -|- hp

hfalse_absorb_lefttheoremproof_kernel.h:188


thm get_hfalse_absorb_left();


thm get_hfalse_absorb_left();


!hp. fact(F) ** hp -|- fact(F)


!hp. fact(F) ** hp -|- fact(F)

hfalse_absorb_righttheoremproof_kernel.h:191


thm get_hfalse_absorb_right();


thm get_hfalse_absorb_right();


!hp. hp ** fact(F) -|- fact(F)


!hp. hp ** fact(F) -|- fact(F)

hand_introtheoremproof_kernel.h:194


thm get_hand_intro();


thm get_hand_intro();


!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp1 |-- hp3) ==> (hp1 |-- hp2 && hp3)


!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp1 |-- hp3) ==> (hp1 |-- hp2 && hp3)

hand_elim1theoremproof_kernel.h:197


thm get_hand_elim1();


thm get_hand_elim1();


!hp1 hp2. (hp1 && hp2 |-- hp1)


!hp1 hp2. (hp1 && hp2 |-- hp1)

hand_elim2theoremproof_kernel.h:200


thm get_hand_elim2();


thm get_hand_elim2();


!hp1 hp2. (hp1 && hp2 |-- hp2)


!hp1 hp2. (hp1 && hp2 |-- hp2)

hor_intro1theoremproof_kernel.h:203


thm get_hor_intro1();


thm get_hor_intro1();


!hp1 hp2. (hp1 |-- hp1 || hp2)


!hp1 hp2. (hp1 |-- hp1 || hp2)

hor_intro2theoremproof_kernel.h:206


thm get_hor_intro2();


thm get_hor_intro2();


!hp1 hp2. (hp2 |-- hp1 || hp2)


!hp1 hp2. (hp2 |-- hp1 || hp2)

hor_elimtheoremproof_kernel.h:209


thm get_hor_elim();


thm get_hor_elim();


!hp1 hp2 hp3. (hp1 |-- hp3) ==> (hp2 |-- hp3) ==> (hp1 || hp2 |-- hp3)


!hp1 hp2 hp3. (hp1 |-- hp3) ==> (hp2 |-- hp3) ==> (hp1 || hp2 |-- hp3)

himpl_hand_adjointtheoremproof_kernel.h:212


thm get_himpl_hand_adjoint();


thm get_himpl_hand_adjoint();


!hp1 hp2 hp3. (hp1 && hp2 |-- hp3) <=> (hp1 |-- hp2 --> hp3)


!hp1 hp2 hp3. (hp1 && hp2 |-- hp3) <=> (hp1 |-- hp2 --> hp3)

注意 htrue_hemphtrue_hemp 所记录的不对称：fact(T)fact(T) 等价于 empemp，而不等价于 truetrue。factfact 携带“堆为空”这一断言，purepure 则不携带。这一区别正是布尔值需要两种嵌入的原因，也是下面的纯事实规则分成两族的原因。

量词规则

堆命题量词 existsexists 与 forallforall 的引入与消去规则；它们是作用在返回 hprophprop 的函数之上的 HOL 绑定子。

hexists_introtheoremproof_kernel.h:215


thm get_hexists_intro();


thm get_hexists_intro();


!(x : A) hp hpA. (hp |-- hpA x) ==> (hp |-- (exists x : A. hpA x))


!(x : A) hp hpA. (hp |-- hpA x) ==> (hp |-- (exists x : A. hpA x))

hexists_elimtheoremproof_kernel.h:218


thm get_hexists_elim();


thm get_hexists_elim();


!hp hpA. (!x : A. hpA x |-- hp) ==> ((exists y : A. hpA y) |-- hp)


!hp hpA. (!x : A. hpA x |-- hp) ==> ((exists y : A. hpA y) |-- hp)

hforall_introtheoremproof_kernel.h:221


thm get_hforall_intro();


thm get_hforall_intro();


!hp hpA. (!x : A. hp |-- hpA x) ==> (hp |-- (forall x : A. hpA x))


!hp hpA. (!x : A. hp |-- hpA x) ==> (hp |-- (forall x : A. hpA x))

hforall_elimtheoremproof_kernel.h:224


thm get_hforall_elim();


thm get_hforall_elim();


!hp hpA (x : A). (hpA x |-- hp) ==> ((forall x : A. hpA x) |-- hp)


!hp hpA (x : A). (hpA x |-- hp) ==> ((forall x : A. hpA x) |-- hp)

纯事实

把纯布尔断言移入、移出堆命题的规则，以及头文件在此处声明的 &&&& 的结合律与交换律。

hpure_introtheoremproof_kernel.h:227


thm get_hpure_intro();


thm get_hpure_intro();


!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- pure(p) && hp2)


!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- pure(p) && hp2)

hpure_elimtheoremproof_kernel.h:230


thm get_hpure_elim();


thm get_hpure_elim();


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (pure(p) && hp1 |-- hp2)


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (pure(p) && hp1 |-- hp2)

hand_assoctheoremproof_kernel.h:233


thm get_hand_assoc();


thm get_hand_assoc();


!hp1 hp2 hp3. (hp1 && hp2) && hp3 -|- hp1 && (hp2 && hp3)


!hp1 hp2 hp3. (hp1 && hp2) && hp3 -|- hp1 && (hp2 && hp3)

hand_commtheoremproof_kernel.h:236


thm get_hand_comm();


thm get_hand_comm();


!hp1 hp2. hp1 && hp2 -|- hp2 && hp1


!hp1 hp2. hp1 && hp2 -|- hp2 && hp1

hsep_hpure_lefttheoremproof_kernel.h:239


thm get_hsep_hpure_left();


thm get_hsep_hpure_left();


!p hp1 hp2. (pure(p) && hp1) ** hp2 -|- pure(p) && (hp1 ** hp2)


!p hp1 hp2. (pure(p) && hp1) ** hp2 -|- pure(p) && (hp1 ** hp2)

hsep_hpure_righttheoremproof_kernel.h:242


thm get_hsep_hpure_right();


thm get_hsep_hpure_right();


!p hp1 hp2. hp1 ** (pure(p) && hp2) -|- pure(p) && (hp1 ** hp2)


!p hp1 hp2. hp1 ** (pure(p) && hp2) -|- pure(p) && (hp1 ** hp2)

hfact_deftheoremproof_kernel.h:245


thm get_hfact_def();


thm get_hfact_def();


!p hp. fact(p) -|- (pure(p) && emp)


!p hp. fact(p) -|- (pure(p) && emp)

hfact_hpuretheoremproof_kernel.h:248


thm get_hfact_hpure();


thm get_hfact_hpure();


!p hp. fact(p) ** hp -|- pure(p) && hp


!p hp. fact(p) ** hp -|- pure(p) && hp

hfact_introtheoremproof_kernel.h:251


thm get_hfact_intro();


thm get_hfact_intro();


!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- fact(p) ** hp2)


!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- fact(p) ** hp2)

hfact_elimtheoremproof_kernel.h:254


thm get_hfact_elim();


thm get_hfact_elim();


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- hp2)


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- hp2)

hfact_duptheoremproof_kernel.h:257


thm get_hfact_dup();


thm get_hfact_dup();


!p. fact(p) |-- fact(p) ** fact(p)


!p. fact(p) |-- fact(p) ** fact(p)

hsep_hfact_lefttheoremproof_kernel.h:260


thm get_hsep_hfact_left();


thm get_hsep_hfact_left();


!p hp1 hp2. (fact(p) ** hp1) ** hp2 -|- fact(p) ** (hp1 ** hp2)


!p hp1 hp2. (fact(p) ** hp1) ** hp2 -|- fact(p) ** (hp1 ** hp2)

hsep_hfact_righttheoremproof_kernel.h:263


thm get_hsep_hfact_right();


thm get_hsep_hfact_right();


!p hp1 hp2. hp1 ** (fact(p) ** hp2) -|- fact(p) ** (hp1 ** hp2)


!p hp1 hp2. hp1 ** (fact(p) ** hp2) -|- fact(p) ** (hp1 ** hp2)

hfact_defhfact_def 确定了两种嵌入之间的关系——fact(p)fact(p) 就是 pure(p) && emppure(p) && emp——而 hfact_hpurehfact_hpure 是实践中反复使用的形式：fact(p) ** hpfact(p) ** hp 与 pure(p) && hppure(p) && hp 是同一个命题。 hfact_duphfact_dup 是复制规则，它之所以健全，是因为纯事实不拥有任何资源。

在量词上的分配

**** 与 &&&& 如何与左侧或右侧的量词交互。存在量词的情形是等价；全称量词的情形只在一个方向上成立蕴含，这正是意料之中的不对称——被量化的分离弱于被分离的量化。

hsep_hexists_lefttheoremproof_kernel.h:266


thm get_hsep_hexists_left();


thm get_hsep_hexists_left();


!hpA hp. (exists x : A. hpA x) ** hp -|- exists x : A. (hpA x ** hp)


!hpA hp. (exists x : A. hpA x) ** hp -|- exists x : A. (hpA x ** hp)

hsep_hexists_righttheoremproof_kernel.h:269


thm get_hsep_hexists_right();


thm get_hsep_hexists_right();


!hp hpA. hp ** (exists x : A. hpA x) -|- exists x : A. (hp ** hpA x)


!hp hpA. hp ** (exists x : A. hpA x) -|- exists x : A. (hp ** hpA x)

hsep_hforall_lefttheoremproof_kernel.h:272


thm get_hsep_hforall_left();


thm get_hsep_hforall_left();


!hpA hp. (forall x : A. hpA x) ** hp |-- forall x : A. (hpA x ** hp)


!hpA hp. (forall x : A. hpA x) ** hp |-- forall x : A. (hpA x ** hp)

hsep_hforall_righttheoremproof_kernel.h:275


thm get_hsep_hforall_right();


thm get_hsep_hforall_right();


!hp hpA. hp ** (forall x : A. hpA x) |-- forall x : A. (hp ** hpA x)


!hp hpA. hp ** (forall x : A. hpA x) |-- forall x : A. (hp ** hpA x)

hand_hexists_lefttheoremproof_kernel.h:278


thm get_hand_hexists_left();


thm get_hand_hexists_left();


!hpA hp. (exists x : A. hpA x) && hp -|- exists x : A. (hpA x && hp)


!hpA hp. (exists x : A. hpA x) && hp -|- exists x : A. (hpA x && hp)

hand_hexists_righttheoremproof_kernel.h:281


thm get_hand_hexists_right();


thm get_hand_hexists_right();


!hp hpA. hp && (exists x : A. hpA x) -|- exists x : A. (hp && hpA x)


!hp hpA. hp && (exists x : A. hpA x) -|- exists x : A. (hp && hpA x)

hand_hforall_lefttheoremproof_kernel.h:284


thm get_hand_hforall_left();


thm get_hand_hforall_left();


!hpA hp. (forall x : A. hpA x) && hp |-- forall x : A. (hpA x && hp)


!hpA hp. (forall x : A. hpA x) && hp |-- forall x : A. (hpA x && hp)

hand_hforall_righttheoremproof_kernel.h:287


thm get_hand_hforall_right();


thm get_hand_hforall_right();


!hp hpA. hp && (forall x : A. hpA x) |-- forall x : A. (hp && hpA x)


!hp hpA. hp && (forall x : A. hpA x) |-- forall x : A. (hp && hpA x)

单调性

蕴含对量词与加性连接词的合同性，补全上文由 hsep_cancel_lefthsep_cancel_left 开启的这一组规则。

hexists_monotonetheoremproof_kernel.h:291


thm get_hexists_monotone();


thm get_hexists_monotone();


!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((exists x:A. hpA x) |-- (exists x:A. hpA' x))


!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((exists x:A. hpA x) |-- (exists x:A. hpA' x))

hforall_monotonetheoremproof_kernel.h:294


thm get_hforall_monotone();


thm get_hforall_monotone();


!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((forall x:A. hpA x) |-- (forall x:A. hpA' x))


!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((forall x:A. hpA x) |-- (forall x:A. hpA' x))

hand_monotonetheoremproof_kernel.h:297


thm get_hand_monotone();


thm get_hand_monotone();


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 && hp2 |-- hp1' && hp2')


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 && hp2 |-- hp1' && hp2')

hor_monotonetheoremproof_kernel.h:300


thm get_hor_monotone();


thm get_hor_monotone();


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 || hp2 |-- hp1' || hp2')


!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 || hp2 |-- hp1' || hp2')

派生规则

有十个访问器带 derivedderived 徽标，来自头文件中的 @derived@derived 标注。这个标注记录的是内核自身发展过程中的层次：这些引理是由上面的规则证得的，而不属于分离代数赖以构建的核心规则集。它与信任程度无关。带标注与不带标注的访问器同样返回证明器已经证明的定理，证明引用它们的方式也完全相同。

它们之所以存在，是因为手工重排断言时反复出现这些形态：把 factfact 交换到堆命题的另一侧，把三元 **** 的第二个合取项提到最前，或者把一条等价按当前需要的方向转成蕴含。

hsep_hfalse_lefttheoremderivedproof_kernel.h:304


thm get_hsep_hfalse_left();


thm get_hsep_hfalse_left();


!hp. false ** hp |-- false


!hp. false ** hp |-- false

hsep_hfact_commtheoremderivedproof_kernel.h:308


thm get_hsep_hfact_comm();


thm get_hsep_hfact_comm();


!hp p. hp ** fact(p) -|- fact(p) ** hp


!hp p. hp ** fact(p) -|- fact(p) ** hp

hfact_hpure_righttheoremderivedproof_kernel.h:312


thm get_hfact_hpure_right();


thm get_hfact_hpure_right();


!p hp1 hp2. hp1 ** (pure(p) && hp2) -|- pure(p) && (hp1 ** hp2)


!p hp1 hp2. hp1 ** (pure(p) && hp2) -|- pure(p) && (hp1 ** hp2)

头文件中 hfact_hpure_righthfact_hpure_right 的注释是错的

上面显示的陈述其实是 hsep_hpure_righthsep_hpure_right 的陈述，那是本页更早处收录的另一条定理。内核以 hfact_hpure_righthfact_hpure_right 这个名称实际证明的（见 cst_seplogic.mlcst_seplogic.ml）是


!p hp. hp && pure(p) -|- fact(p) ** hp


!p hp. hp && pure(p) -|- fact(p) ** hp

——它是 hfact_hpurehfact_hpure 的镜像，把右侧加性合取中的纯事实换成左侧的分离合取。这是 proof_kernel.hproof_kernel.h 上游的文档缺陷，而不是访问器本身的偏差：get_hfact_hpure_right()get_hfact_hpure_right() 返回的正是刚才给出的定理。证明规则页列出了正确的陈述。

hsep_comm_left_parttheoremderivedproof_kernel.h:316


thm get_hsep_comm_left_part();


thm get_hsep_comm_left_part();


!hp hp1 hp2. hp1 ** hp ** hp2 -|- hp ** hp1 ** hp2


!hp hp1 hp2. hp1 ** hp ** hp2 -|- hp ** hp1 ** hp2

hentail_sym_lefttheoremderivedproof_kernel.h:320


thm get_hentail_sym_left();


thm get_hentail_sym_left();


!hp1 hp2. (hp1 -|- hp2) ==> (hp1 |-- hp2)


!hp1 hp2. (hp1 -|- hp2) ==> (hp1 |-- hp2)

hsep_cancel_left_eqtheoremderivedproof_kernel.h:324


thm get_hsep_cancel_left_eq();


thm get_hsep_cancel_left_eq();


!hp1 hp2 hp2'. (hp2 -|- hp2') ==> (hp1 ** hp2 -|- hp1 ** hp2')


!hp1 hp2 hp2'. (hp2 -|- hp2') ==> (hp1 ** hp2 -|- hp1 ** hp2')

hfact_elim_duptheoremderivedproof_kernel.h:328


thm get_hfact_elim_dup();


thm get_hfact_elim_dup();


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- fact(p) ** hp2)


!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- fact(p) ** hp2)

hpure_add_hfacttheoremderivedproof_kernel.h:332


thm get_hpure_add_hfact();


thm get_hpure_add_hfact();


!p hp. (hp |-- pure(p)) ==> (hp |-- fact(p) ** hp)


!p hp. (hp |-- pure(p)) ==> (hp |-- fact(p) ** hp)

hsep_actheoremderivedproof_kernel.h:336


thm get_hsep_ac();


thm get_hsep_ac();


(hp1 ** hp2 -|- hp2 ** hp1) && ((hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)) && (hp1 ** (hp2 ** hp3) -|- hp2 ** (hp1 ** hp3))


(hp1 ** hp2 -|- hp2 ** hp1) && ((hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)) && (hp1 ** (hp2 ** hp3) -|- hp2 ** (hp1 ** hp3))

heq_symtheoremderivedproof_kernel.h:340


thm get_heq_sym();


thm get_heq_sym();


!hp1 hp2. (hp1 -|- hp2) <=> (hp2 -|- hp1)


!hp1 hp2. (hp1 -|- hp2) <=> (hp2 -|- hp1)

hsep_achsep_ac 把结合律—交换律规范化所需的三种嵌套 **** 重排打包在一起，因此它的陈述是一个合取式，而不是单条等价。

C 类型、sizeof 与取值范围

四个访问器与 :ctype:ctype 索引有关：定义 sizeofsizeof、min_ofmin_of 与 max_ofmax_of 的递归方程，外加内核直接导出的那一条推论。

sizeof_deftheoremproof_kernel.h:373


thm get_sizeof_def();


thm get_sizeof_def();


the definition of `sizeof : ctype->int


the definition of `sizeof : ctype->int

sizeof_ge_0theoremproof_kernel.h:376


thm get_sizeof_ge_0();


thm get_sizeof_ge_0();


!ty. sizeof ty >= &0


!ty. sizeof ty >= &0

min_of_deftheoremproof_kernel.h:379


thm get_min_of_def();


thm get_min_of_def();


the definition of `min_of : ctype->int


the definition of `min_of : ctype->int

max_of_deftheoremproof_kernel.h:382


thm get_max_of_def();


thm get_max_of_def();


the definition of `max_of : ctype->int


the definition of `max_of : ctype->int

注释若写作 the definition of ff，表示访问器返回的是定义定理——每个构造子一条方程所组成的合取式——这正是重写步骤把 sizeof Tintsizeof Tint 计算成一个数值字面量所需要的。 sizeof_ge_0sizeof_ge_0 表达的是任何 C 类型的大小都不为负这一事实，凡是需要给数组地址 x + i * sizeof(ty)x + i * sizeof(ty) 定界的地方都会用到它。

带类型的存储单元与数组定义

关于 data_atdata_at 与 undef_data_atundef_data_at 的四条规则——它们是单个带类型存储单元的内存谓词 ——随后是数组谓词的六条定义性定理。

data_at_to_undef_data_attheoremproof_kernel.h:385


thm get_data_at_to_undef_data_at();


thm get_data_at_to_undef_data_at();


!x ty v. data_at x ty v |-- undef_data_at x ty


!x ty v. data_at x ty v |-- undef_data_at x ty

data_at_rangetheoremproof_kernel.h:388


thm get_data_at_range();


thm get_data_at_range();


!x ty v. data_at x ty v |-- data_at x ty v ** fact(min_of(ty) <= v && v <= max_of(ty))


!x ty v. data_at x ty v |-- data_at x ty v ** fact(min_of(ty) <= v && v <= max_of(ty))

data_at_duptheoremproof_kernel.h:391


thm get_data_at_dup();


thm get_data_at_dup();


!x ty v1 v2. data_at x ty v1 ** data_at x ty v2 |-- false


!x ty v1 v2. data_at x ty v1 ** data_at x ty v2 |-- false

undef_data_at_duptheoremproof_kernel.h:394


thm get_undef_data_at_dup();


thm get_undef_data_at_dup();


!x ty. undef_data_at x ty ** undef_data_at x ty |-- false


!x ty. undef_data_at x ty ** undef_data_at x ty |-- false

array_at_rec_deftheoremproof_kernel.h:397


thm get_array_at_rec_def();


thm get_array_at_rec_def();


the definition of `array_at_rec : addr->ctype->int->int->(int)list->hprop


the definition of `array_at_rec : addr->ctype->int->int->(int)list->hprop

array_at_missing_i_rec_deftheoremproof_kernel.h:400


thm get_array_at_missing_i_rec_def();


thm get_array_at_missing_i_rec_def();


the definition of `array_at_missing_i_rec : addr->ctype->int->int->int->(int)list->hprop


the definition of `array_at_missing_i_rec : addr->ctype->int->int->int->(int)list->hprop

array_at_deftheoremproof_kernel.h:403


thm get_array_at_def();


thm get_array_at_def();


the definition of `array_at : addr->ctype->int->(int)list->hprop


the definition of `array_at : addr->ctype->int->(int)list->hprop

undef_array_at_rec_deftheoremproof_kernel.h:406


thm get_undef_array_at_rec_def();


thm get_undef_array_at_rec_def();


the definition of `undef_array_at_rec : addr->ctype->int->int->num->hprop


the definition of `undef_array_at_rec : addr->ctype->int->int->num->hprop

undef_array_at_missing_i_rec_deftheoremproof_kernel.h:409


thm get_undef_array_at_missing_i_rec_def();


thm get_undef_array_at_missing_i_rec_def();


the definition of `undef_array_at_missing_i_rec : addr->ctype->int->int->int->num->hprop


the definition of `undef_array_at_missing_i_rec : addr->ctype->int->int->int->num->hprop

undef_array_at_deftheoremproof_kernel.h:412


thm get_undef_array_at_def();


thm get_undef_array_at_def();


the definition of `undef_array_at : addr->ctype->int->hprop


the definition of `undef_array_at : addr->ctype->int->hprop

data_at_rangedata_at_range 正是类型索引发挥作用的地方：存入的值总是位于 min_of(ty)min_of(ty) 与 max_of(ty)max_of(ty) 之间，这条规则把该事实以纯事实的形式提供出来，而不消耗那个单元。 data_at_dupdata_at_dup 与 undef_data_at_dupundef_data_at_dup 是使所有权具有排他性的反复制事实——对同一地址的两份声明蕴含 falsefalse。

带 _def_def 的条目返回的是定义，其注释给出的是被定义谓词的签名，而不是方程。带 _rec_rec 的变体接受显式的索引范围 lolo、hihi；不带后缀的 array_atarray_at 是在它们之上构建的、以长度为索引的形式；带 missing_imissing_i 的变体描述的是切出了索引 ii 处单元的数组，也就是一次切分之后剩下的东西。

列表操作

数组内容是 HOL 列表，因此内核导出了陈述数组规则所用的列表词汇。LENGTHLENGTH、MEMMEM、 APPENDAPPEND、REVERSEREVERSE 与 REPLICATEREPLICATE 是 HOL Light 自带的；以 II 为前缀的操作—— ilengthilength、inthinth、ifirstnifirstn、iskipniskipn、ireplicateireplicate、replace_inthreplace_inth、sublistsublist——是 C* 的整数索引对应物，引入它们是为了让列表下标与 C 的整数运算处在同一个类型之中。

LENGTHtheoremproof_kernel.h:415


thm get_LENGTH();


thm get_LENGTH();


LENGTH [] = 0 /\ (!h t. LENGTH (CONS h t) = SUC (LENGTH t))


LENGTH [] = 0 /\ (!h t. LENGTH (CONS h t) = SUC (LENGTH t))

ILENGTH_DEFtheoremproof_kernel.h:418


thm get_ILENGTH_DEF();


thm get_ILENGTH_DEF();


the definition of `ilength : (A)list->int


the definition of `ilength : (A)list->int

NTH_DEFtheoremproof_kernel.h:421


thm get_NTH_DEF();


thm get_NTH_DEF();


the definition of `NTH : num->(A)list->A


the definition of `NTH : num->(A)list->A

INTH_DEFtheoremproof_kernel.h:424


thm get_INTH_DEF();


thm get_INTH_DEF();


the definition of `inth : int->(A)list->A


the definition of `inth : int->(A)list->A

REPLACE_NTH_DEFtheoremproof_kernel.h:427


thm get_REPLACE_NTH_DEF();


thm get_REPLACE_NTH_DEF();


the definition of `REPLACE_NTH : num->A->(A)list->(A)list


the definition of `REPLACE_NTH : num->A->(A)list->(A)list

REPLACE_INTH_DEFtheoremproof_kernel.h:430


thm get_REPLACE_INTH_DEF();


thm get_REPLACE_INTH_DEF();


the definition of `replace_inth : int->A->(A)list->(A)list


the definition of `replace_inth : int->A->(A)list->(A)list

FIRSTN_DEFtheoremproof_kernel.h:433


thm get_FIRSTN_DEF();


thm get_FIRSTN_DEF();


the definition of `FIRSTN : num->(A)list->(A)list


the definition of `FIRSTN : num->(A)list->(A)list

IFIRSTN_DEFtheoremproof_kernel.h:436


thm get_IFIRSTN_DEF();


thm get_IFIRSTN_DEF();


the definition of `ifirstn : int->(A)list->(A)list


the definition of `ifirstn : int->(A)list->(A)list

SKIPN_DEFtheoremproof_kernel.h:439


thm get_SKIPN_DEF();


thm get_SKIPN_DEF();


the definition of `SKIPN : num->(A)list->(A)list


the definition of `SKIPN : num->(A)list->(A)list

ISKIPN_DEFtheoremproof_kernel.h:442


thm get_ISKIPN_DEF();


thm get_ISKIPN_DEF();


the definition of `iskipn : int->(A)list->(A)list


the definition of `iskipn : int->(A)list->(A)list

REPLICATEtheoremproof_kernel.h:445


thm get_REPLICATE();


thm get_REPLICATE();


REPLICATE 0 x = [] /\ REPLICATE (SUC n) x = CONS x (REPLICATE n x)


REPLICATE 0 x = [] /\ REPLICATE (SUC n) x = CONS x (REPLICATE n x)

IREPLICATE_DEFtheoremproof_kernel.h:448


thm get_IREPLICATE_DEF();


thm get_IREPLICATE_DEF();


the definition of `ireplicate : int->A->(A)list


the definition of `ireplicate : int->A->(A)list

SUBLIST_DEFtheoremproof_kernel.h:451


thm get_SUBLIST_DEF();


thm get_SUBLIST_DEF();


the definition of `sublist : int->int->(A)list->(A)list


the definition of `sublist : int->int->(A)list->(A)list

MEMtheoremproof_kernel.h:454


thm get_MEM();


thm get_MEM();


(MEM x [] <=> F) /\ (MEM x (CONS h t) <=> x = h \/ MEM x t)


(MEM x [] <=> F) /\ (MEM x (CONS h t) <=> x = h \/ MEM x t)

APPENDtheoremproof_kernel.h:457


thm get_APPEND();


thm get_APPEND();


(!l. APPEND [] l = l) /\ (!h t l. APPEND (CONS h t) l = CONS h (APPEND t l))


(!l. APPEND [] l = l) /\ (!h t l. APPEND (CONS h t) l = CONS h (APPEND t l))

REVERSEtheoremproof_kernel.h:460


thm get_REVERSE();


thm get_REVERSE();


REVERSE [] = [] /\ REVERSE (CONS x l) = APPEND (REVERSE l) [x]


REVERSE [] = [] /\ REVERSE (CONS x l) = APPEND (REVERSE l) [x]

ILENGTH_NONNEGtheoremproof_kernel.h:463


thm get_ILENGTH_NONNEG();


thm get_ILENGTH_NONNEG();


!l:(A)list. &0 <= ilength l


!l:(A)list. &0 <= ilength l

ILENGTH_APPENDtheoremproof_kernel.h:466


thm get_ILENGTH_APPEND();


thm get_ILENGTH_APPEND();


!l1:(A)list l2:(A)list. ilength(l1 ++ l2) == ilength(l1) + ilength(l2)


!l1:(A)list l2:(A)list. ilength(l1 ++ l2) == ilength(l1) + ilength(l2)

ISKIPN_SPLIT_FIRSTtheoremproof_kernel.h:469


thm get_ISKIPN_SPLIT_FIRST();


thm get_ISKIPN_SPLIT_FIRST();


!i:int l:(A)list. &0 <= i && i < ilength l ==> iskipn i l == (inth i l) :: (iskipn (i + &1) l)


!i:int l:(A)list. &0 <= i && i < ilength l ==> iskipn i l == (inth i l) :: (iskipn (i + &1) l)

ISKIPN_ILENGTHtheoremproof_kernel.h:472


thm get_ISKIPN_ILENGTH();


thm get_ISKIPN_ILENGTH();


!l:(A)list. iskipn (ilength l) l == []


!l:(A)list. iskipn (ilength l) l == []

ILENGTH_IREPLICATEtheoremproof_kernel.h:475


thm get_ILENGTH_IREPLICATE();


thm get_ILENGTH_IREPLICATE();


!n:int v:A. ilength(ireplicate n v) == n


!n:int v:A. ilength(ireplicate n v) == n

IREPLICATE_APPENDtheoremproof_kernel.h:478


thm get_IREPLICATE_APPEND();


thm get_IREPLICATE_APPEND();


!l:(A)list v:A. (ireplicate n v) ++ [v] == ireplicate (n + &1) v


!l:(A)list v:A. (ireplicate n v) ++ [v] == ireplicate (n + &1) v

最后六条是数组推理反复需要的、关于这些操作的已证事实：ilengthilength 非负且对拼接可加，从非空后缀的前端跳过一个元素的行为符合预期，跳过全部长度后得到空列表，以及填充未初始化数组时用到的两条关于 ireplicateireplicate 的事实。

array_at 规则族

使数组推理成为可能的三十条规则：长度与范围事实，从数组中切分出一个单元再合并回去，在头部或尾部操作，重设索引范围的基址，把数组一分为二，以及空数组的情形——每条都有已初始化的 array_atarray_at 形式，并在有意义时配有 undef_array_atundef_array_at 的镜像形式。

array_at_rec_lengththeoremproof_kernel.h:481


thm get_array_at_rec_length();


thm get_array_at_rec_length();


!x ty lo hi l. array_at_rec x ty lo hi l |-- array_at_rec x ty lo hi l ** fact(ilength(l) == hi - lo)


!x ty lo hi l. array_at_rec x ty lo hi l |-- array_at_rec x ty lo hi l ** fact(ilength(l) == hi - lo)

array_at_lengththeoremproof_kernel.h:484


thm get_array_at_length();


thm get_array_at_length();


!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(ilength(l) == n)


!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(ilength(l) == n)

array_at_rangetheoremproof_kernel.h:487


thm get_array_at_range();


thm get_array_at_range();


!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(!i. &0 <= i ==> i < n ==> (min_of(ty) <= inth i l && inth i l <= max_of(ty)))


!x ty n l. array_at x ty n l |-- array_at x ty n l ** fact(!i. &0 <= i ==> i < n ==> (min_of(ty) <= inth i l && inth i l <= max_of(ty)))

array_at_rec_splittheoremproof_kernel.h:490


thm get_array_at_rec_split();


thm get_array_at_rec_split();


!x ty lo n m l. (lo <= n) ==> (n < m) ==> (array_at_rec x ty lo m l |-- data_at (x + n * sizeof(ty)) ty (inth (n - lo) l) ** array_at_missing_i_rec x ty n lo m l)


!x ty lo n m l. (lo <= n) ==> (n < m) ==> (array_at_rec x ty lo m l |-- data_at (x + n * sizeof(ty)) ty (inth (n - lo) l) ** array_at_missing_i_rec x ty n lo m l)

array_at_splittheoremproof_kernel.h:493


thm get_array_at_split();


thm get_array_at_split();


!x ty n m l. (&0 <= n) ==> (n < m) ==> (array_at x ty m l |-- data_at (x + n * sizeof(ty)) ty (inth n l) ** array_at_missing_i_rec x ty n (&0) m l)


!x ty n m l. (&0 <= n) ==> (n < m) ==> (array_at x ty m l |-- data_at (x + n * sizeof(ty)) ty (inth n l) ** array_at_missing_i_rec x ty n (&0) m l)

array_at_rec_mergetheoremproof_kernel.h:496


thm get_array_at_rec_merge();


thm get_array_at_rec_merge();


!x ty lo n m a l. (lo <= n) ==> (n < m) ==> (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n lo m l |-- array_at_rec x ty lo m (replace_inth (n - lo) a l))


!x ty lo n m a l. (lo <= n) ==> (n < m) ==> (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n lo m l |-- array_at_rec x ty lo m (replace_inth (n - lo) a l))

array_at_mergetheoremproof_kernel.h:499


thm get_array_at_merge();


thm get_array_at_merge();


!x ty n m a l. (&0 <= n) ==> (n < m) ==> (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n (&0) m l |-- array_at x ty m (replace_inth n a l))


!x ty n m a l. (&0 <= n) ==> (n < m) ==> (data_at (x + n * sizeof(ty)) ty a ** array_at_missing_i_rec x ty n (&0) m l |-- array_at x ty m (replace_inth n a l))

array_at_rec_headtheoremproof_kernel.h:502


thm get_array_at_rec_head();


thm get_array_at_rec_head();


!x ty lo hi l. (lo < hi) ==> (array_at_rec x ty lo hi l |-- data_at (x + lo * sizeof(ty)) ty (inth (&0) l) ** array_at_rec x ty (lo + &1) hi (sublist (&1) (hi - lo) l))


!x ty lo hi l. (lo < hi) ==> (array_at_rec x ty lo hi l |-- data_at (x + lo * sizeof(ty)) ty (inth (&0) l) ** array_at_rec x ty (lo + &1) hi (sublist (&1) (hi - lo) l))

array_at_rec_head_mergetheoremproof_kernel.h:505


thm get_array_at_rec_head_merge();


thm get_array_at_rec_head_merge();


!x ty lo hi a l. (lo < hi) ==> (data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l |-- array_at_rec x ty lo hi (a :: l))


!x ty lo hi a l. (lo < hi) ==> (data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l |-- array_at_rec x ty lo hi (a :: l))

array_at_array_rec_constheoremproof_kernel.h:508


thm get_array_at_array_rec_cons();


thm get_array_at_array_rec_cons();


!x ty lo hi a l. (lo < hi) ==> (array_at_rec x ty lo hi (a :: l) |-- data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l)


!x ty lo hi a l. (lo < hi) ==> (array_at_rec x ty lo hi (a :: l) |-- data_at (x + lo * sizeof(ty)) ty a ** array_at_rec x ty (lo + &1) hi l)

array_at_rec_tail_mergetheoremproof_kernel.h:511


thm get_array_at_rec_tail_merge();


thm get_array_at_rec_tail_merge();


!x ty lo hi a l. (lo <= hi) ==> (data_at (x + hi * sizeof(ty)) ty a ** array_at_rec x ty lo hi l |-- array_at_rec x ty lo (hi + &1) (l ++ [a]))


!x ty lo hi a l. (lo <= hi) ==> (data_at (x + hi * sizeof(ty)) ty a ** array_at_rec x ty lo hi l |-- array_at_rec x ty lo (hi + &1) (l ++ [a]))

array_at_rec_basetheoremproof_kernel.h:514


thm get_array_at_rec_base();


thm get_array_at_rec_base();


!x ty m k n l. array_at_rec x ty (m + k) n l -|- array_at_rec (x + k * sizeof(ty)) ty m (n - k) l


!x ty m k n l. array_at_rec x ty (m + k) n l -|- array_at_rec (x + k * sizeof(ty)) ty m (n - k) l

array_at_rec_divide_auxtheoremproof_kernel.h:517


thm get_array_at_rec_divide_aux();


thm get_array_at_rec_divide_aux();


!x ty lo m n l. (lo <= m) ==> (m <= n) ==> (ilength(l) == n - lo) ==> (array_at_rec x ty lo n l -|- array_at_rec x ty lo m (sublist (&0) (m - lo) l) ** array_at_rec x ty m n (sublist (m - lo) (n - lo) l))


!x ty lo m n l. (lo <= m) ==> (m <= n) ==> (ilength(l) == n - lo) ==> (array_at_rec x ty lo n l -|- array_at_rec x ty lo m (sublist (&0) (m - lo) l) ** array_at_rec x ty m n (sublist (m - lo) (n - lo) l))

array_at_rec_dividetheoremproof_kernel.h:520


thm get_array_at_rec_divide();


thm get_array_at_rec_divide();


!x ty m n l. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at_rec x ty (&0) n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))


!x ty m n l. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at_rec x ty (&0) n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))

array_at_dividetheoremproof_kernel.h:523


thm get_array_at_divide();


thm get_array_at_divide();


!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at x ty n l -|- array_at x ty m (sublist (&0) m l) ** array_at (x + m * sizeof(ty)) ty (n - m) (sublist m n l))


!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at x ty n l -|- array_at x ty m (sublist (&0) m l) ** array_at (x + m * sizeof(ty)) ty (n - m) (sublist m n l))

array_at_divide2theoremproof_kernel.h:526


thm get_array_at_divide2();


thm get_array_at_divide2();


!x ty n m l1 l2. (ilength(l1) == n) ==> (ilength(l2) == m) ==> (array_at x ty (n + m) (l1 ++ l2) -|- array_at x ty n l1 ** array_at (x + n * sizeof(ty)) ty m l2)


!x ty n m l1 l2. (ilength(l1) == n) ==> (ilength(l2) == m) ==> (array_at x ty (n + m) (l1 ++ l2) -|- array_at x ty n l1 ** array_at (x + n * sizeof(ty)) ty m l2)

array_at_divide_rectheoremproof_kernel.h:529


thm get_array_at_divide_rec();


thm get_array_at_divide_rec();


!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at x ty n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))


!x ty n l m. (&0 <= m) ==> (m <= n) ==> (ilength(l) == n) ==> (array_at x ty n l -|- array_at_rec x ty (&0) m (sublist (&0) m l) ** array_at_rec x ty m n (sublist m n l))

undef_array_at_rec_basetheoremproof_kernel.h:532


thm get_undef_array_at_rec_base();


thm get_undef_array_at_rec_base();


!x ty m k n len. undef_array_at_rec x ty (m + k) n len -|- undef_array_at_rec (x + k * sizeof(ty)) ty m (n - k) len


!x ty m k n len. undef_array_at_rec x ty (m + k) n len -|- undef_array_at_rec (x + k * sizeof(ty)) ty m (n - k) len

undef_array_at_dividetheoremproof_kernel.h:535


thm get_undef_array_at_divide();


thm get_undef_array_at_divide();


!x ty n m. (&0 <= m) ==> (m <= n) ==> (undef_array_at x ty n -|- undef_array_at x ty m ** undef_array_at (x + m * sizeof(ty)) ty (n - m))


!x ty n m. (&0 <= m) ==> (m <= n) ==> (undef_array_at x ty n -|- undef_array_at x ty m ** undef_array_at (x + m * sizeof(ty)) ty (n - m))

undef_Tuchar_array_at_splittheoremproof_kernel.h:538


thm get_undef_Tuchar_array_at_split();


thm get_undef_Tuchar_array_at_split();


!x ty n. n >= sizeof(ty) ==> (undef_array_at x Tuchar n -|- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) Tuchar (n - sizeof(ty)))


!x ty n. n >= sizeof(ty) ==> (undef_array_at x Tuchar n -|- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) Tuchar (n - sizeof(ty)))

array_at_split_firsttheoremproof_kernel.h:541


thm get_array_at_split_first();


thm get_array_at_split_first();


!x ty n v l. (n >= &1) ==> (array_at x ty n (v :: l) |-- data_at x ty v ** array_at (x + sizeof(ty)) ty (n - &1) l)


!x ty n v l. (n >= &1) ==> (array_at x ty n (v :: l) |-- data_at x ty v ** array_at (x + sizeof(ty)) ty (n - &1) l)

array_at_merge_firsttheoremproof_kernel.h:544


thm get_array_at_merge_first();


thm get_array_at_merge_first();


!x ty n v l. data_at x ty v ** array_at (x + sizeof(ty)) ty n l |-- array_at x ty (n + &1) (v :: l)


!x ty n v l. data_at x ty v ** array_at (x + sizeof(ty)) ty n l |-- array_at x ty (n + &1) (v :: l)

array_at_split_lasttheoremproof_kernel.h:547


thm get_array_at_split_last();


thm get_array_at_split_last();


!x ty n v l. (n >= &1) ==> (array_at x ty n (l ++ [v]) |-- array_at x ty (n - &1) l ** data_at (x + (n - &1) * sizeof(ty)) ty v)


!x ty n v l. (n >= &1) ==> (array_at x ty n (l ++ [v]) |-- array_at x ty (n - &1) l ** data_at (x + (n - &1) * sizeof(ty)) ty v)

array_at_merge_lasttheoremproof_kernel.h:550


thm get_array_at_merge_last();


thm get_array_at_merge_last();


!x ty n v l. array_at x ty n l ** data_at (x + n * sizeof(ty)) ty v |-- array_at x ty (n + &1) (l ++ [v])


!x ty n v l. array_at x ty n l ** data_at (x + n * sizeof(ty)) ty v |-- array_at x ty (n + &1) (l ++ [v])

undef_array_at_split_firsttheoremproof_kernel.h:553


thm get_undef_array_at_split_first();


thm get_undef_array_at_split_first();


!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty (n - &1))


!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty (n - &1))

undef_array_at_merge_firsttheoremproof_kernel.h:556


thm get_undef_array_at_merge_first();


thm get_undef_array_at_merge_first();


!x ty n. undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty n |-- undef_array_at x ty (n + &1)


!x ty n. undef_data_at x ty ** undef_array_at (x + sizeof(ty)) ty n |-- undef_array_at x ty (n + &1)

undef_array_at_split_lasttheoremproof_kernel.h:559


thm get_undef_array_at_split_last();


thm get_undef_array_at_split_last();


!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_array_at x ty (n - &1) ** undef_data_at (x + (n - &1) * sizeof(ty)) ty)


!x ty n. (n >= &1) ==> (undef_array_at x ty n |-- undef_array_at x ty (n - &1) ** undef_data_at (x + (n - &1) * sizeof(ty)) ty)

undef_array_at_merge_lasttheoremproof_kernel.h:562


thm get_undef_array_at_merge_last();


thm get_undef_array_at_merge_last();


!x ty n. undef_array_at x ty n ** undef_data_at (x + n * sizeof(ty)) ty |-- undef_array_at x ty (n + &1)


!x ty n. undef_array_at x ty n ** undef_data_at (x + n * sizeof(ty)) ty |-- undef_array_at x ty (n + &1)

array_at_zerotheoremproof_kernel.h:565


thm get_array_at_zero();


thm get_array_at_zero();


!x ty n l. (n == &0) ==> (l == []) ==> (array_at x ty n l -|- emp)


!x ty n l. (n == &0) ==> (l == []) ==> (array_at x ty n l -|- emp)

undef_array_at_zerotheoremproof_kernel.h:568


thm get_undef_array_at_zero();


thm get_undef_array_at_zero();


!x ty n. (n == &0) ==> (undef_array_at x ty n -|- emp)


!x ty n. (n == &0) ==> (undef_array_at x ty n -|- emp)

有一条寻址约定贯穿其中每一条规则：以 xx 为基址、元素类型为 tyty 的数组，其第 ii 个元素位于 x + i * sizeof(ty)x + i * sizeof(ty)。带类型的内存谓词页按作用对同一批规则重新分组，并逐条讲解循环不变式真正需要的那些。

小结

proof_kernel.hproof_kernel.h 声明了十个不透明句柄类型与六个列表别名、三个实现访问器约定的宏、三十三个面向逻辑内置项与内置类型的访问器，以及一百四十一个定理访问器。内核中名为 TT 的定理在 C 侧就是 get_T()get_T()；对象只从证明器取回一次，并在此后的整个运行过程中缓存。

这就是证明代码与逻辑内置词汇之间的全部接口。证明拿到这里获得的对象之后所做的一切 ——匹配、实例化、重写、卸除——属于证明器 API，而引擎对这些结果所做的一切属于符号执行 API。