--- a/src/HOL/Library/While_Combinator.thy Wed Jan 03 21:23:50 2001 +0100
+++ b/src/HOL/Library/While_Combinator.thy Wed Jan 03 21:24:29 2001 +0100
@@ -29,20 +29,17 @@
else if b s then while_aux (b, c, c s)
else s)"
+recdef_tc while_aux_tc: while_aux
+ apply (rule wf_same_fst)
+ apply (rule wf_same_fst)
+ apply (simp add: wf_iff_no_infinite_down_chain)
+ apply blast
+ done
+
constdefs
while :: "('a => bool) => ('a => 'a) => 'a => 'a"
"while b c s == while_aux (b, c, s)"
-ML_setup {*
- goalw_cterm [] (cterm_of (sign_of (the_context ()))
- (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
- br wf_same_fst 1;
- br wf_same_fst 1;
- by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
- by (Blast_tac 1);
- qed "while_aux_tc";
-*} (* FIXME cannot access recdef tcs in Isar yet! *)
-
lemma while_aux_unfold:
"while_aux (b, c, s) =
(if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))