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.
open Ord;
val [prem] = goalw Ord.thy [mono_def]
"[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
by (REPEAT (ares_tac [allI, impI, prem] 1));
val monoI = result();
val [major,minor] = goalw Ord.thy [mono_def]
"[| mono(f); A <= B |] ==> f(A) <= f(B)";
by (rtac (major RS spec RS spec RS mp) 1);
by (rtac minor 1);
val monoD = result();