--- a/src/HOLCF/Fix.ML Fri Jan 31 15:54:00 1997 +0100
+++ b/src/HOLCF/Fix.ML Fri Jan 31 16:39:27 1997 +0100
@@ -499,6 +499,14 @@
(atac 1)
]);
+qed_goal "def_fix_ind" Fix.thy "[| f == fix`F; adm(P); \
+\ P(UU);!!x. P(x) ==> P(F`x)|] ==> P f" (fn prems => [
+ (cut_facts_tac prems 1),
+ (asm_simp_tac HOL_ss 1),
+ (etac fix_ind 1),
+ (atac 1),
+ (eresolve_tac prems 1)]);
+
(* ------------------------------------------------------------------------ *)
(* computational induction for weak admissible formulae *)
(* ------------------------------------------------------------------------ *)
@@ -515,6 +523,13 @@
(etac spec 1)
]);
+qed_goal "def_wfix_ind" Fix.thy "[| f == fix`F; admw(P); \
+\ !n. P(iterate n F UU) |] ==> P f" (fn prems => [
+ (cut_facts_tac prems 1),
+ (asm_simp_tac HOL_ss 1),
+ (etac wfix_ind 1),
+ (atac 1)]);
+
(* ------------------------------------------------------------------------ *)
(* for chain-finite (easy) types every formula is admissible *)
(* ------------------------------------------------------------------------ *)