src/HOL/Library/While_Combinator.thy
changeset 11284 981ea92a86dd
parent 11047 10c51288b00d
child 11549 e7265e70fd7c
equal deleted inserted replaced
11283:358f82c4550d 11284:981ea92a86dd
    44   "while_aux (b, c, s) =
    44   "while_aux (b, c, s) =
    45     (if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))
    45     (if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))
    46       then arbitrary
    46       then arbitrary
    47       else if b s then while_aux (b, c, c s)
    47       else if b s then while_aux (b, c, c s)
    48       else s)"
    48       else s)"
       
    49 thm while_aux.simps
    49   apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])
    50   apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])
    50    apply (simp add: same_fst_def)
       
    51   apply (rule refl)
    51   apply (rule refl)
    52   done
    52   done
    53 
    53 
    54 text {*
    54 text {*
    55  The recursion equation for @{term while}: directly executable!
    55  The recursion equation for @{term while}: directly executable!