src/HOL/Library/While_Combinator.thy
changeset 10774 4de3a0d3ae28
parent 10673 337c00fd385b
child 10984 8f49dcbec859
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Wed Jan 03 21:23:50 2001 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Wed Jan 03 21:24:29 2001 +0100
     1.3 @@ -29,20 +29,17 @@
     1.4        else if b s then while_aux (b, c, c s)
     1.5        else s)"
     1.6  
     1.7 +recdef_tc while_aux_tc: while_aux
     1.8 +  apply (rule wf_same_fst)
     1.9 +  apply (rule wf_same_fst)
    1.10 +  apply (simp add: wf_iff_no_infinite_down_chain)
    1.11 +  apply blast
    1.12 +  done
    1.13 +
    1.14  constdefs
    1.15    while :: "('a => bool) => ('a => 'a) => 'a => 'a"
    1.16    "while b c s == while_aux (b, c, s)"
    1.17  
    1.18 -ML_setup {*
    1.19 -  goalw_cterm [] (cterm_of (sign_of (the_context ()))
    1.20 -    (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
    1.21 -  br wf_same_fst 1;
    1.22 -  br wf_same_fst 1;
    1.23 -  by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
    1.24 -  by (Blast_tac 1);
    1.25 -  qed "while_aux_tc";
    1.26 -*} (* FIXME cannot access recdef tcs in Isar yet! *)
    1.27 -
    1.28  lemma while_aux_unfold:
    1.29    "while_aux (b, c, s) =
    1.30      (if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))