src/HOL/Library/Old_Recdef.thy
changeset 58184 db1381d811ab
parent 56248 67dc9549fa15
child 58825 2065f49da190
equal deleted inserted replaced
58183:285fbec02fb0 58184:db1381d811ab
    17 lemma tfl_wf_induct: "ALL R. wf R -->  
    17 lemma tfl_wf_induct: "ALL R. wf R -->  
    18        (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
    18        (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
    19 apply clarify
    19 apply clarify
    20 apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
    20 apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
    21 done
    21 done
       
    22 
       
    23 lemma tfl_cut_def: "cut f r x \<equiv> (\<lambda>y. if (y,x) \<in> r then f y else undefined)"
       
    24   unfolding cut_def .
    22 
    25 
    23 lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
    26 lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
    24 apply clarify
    27 apply clarify
    25 apply (rule cut_apply, assumption)
    28 apply (rule cut_apply, assumption)
    26 done
    29 done