Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
split_weak_cong, nat_case_weak_cong, nat_rec_weak_cong. Used in llist.ML
to make simplifications faster.
HOL/gfp: re-ordered premises to put mono(f) early (first or right after
A==gfp(f) in the def_ rules). Renamed some variables in rules, A to X and
h to A. Renamed coinduct to weak_coinduct, coinduct2 to coinduct.
Strengthened coinduct as suggested by j. Frost, to have the premise X <= f(X
Un gfp(f)).
HOL/llist: used stronger coinduct rule to strengthen LList_coinduct,
LList_equalityI, llist_equalityI, llist_fun_equalityI and to delete the "2"
form of those rules. Proved List_Fun_LList_I, LListD_Fun_diag_I and
llistD_Fun_range_I to help use the new coinduction rules; most proofs
involving them required small changes. Proved prod_fun_range_eq_diag as
lemma for llist_equalityI.
HOL: Higher-Order Logic
This directory contains the Standard ML sources of the Isabelle system for
Higher-Order Logic. Important files include
ROOT.ML -- loads all source files. Enter an ML image containing Pure
Isabelle and type: use "ROOT.ML";
Makefile -- compiles the files under Poly/ML or SML of New Jersey
ex -- subdirectory containing examples. To execute them, enter an ML image
containing HOL and type: use "ex/ROOT.ML";
Useful references on Higher-Order Logic:
P. B. Andrews,
An Introduction to Mathematical Logic and Type Theory
(Academic Press, 1986).
J. Lambek and P. J. Scott,
Introduction to Higher Order Categorical Logic (CUP, 1986)