src/HOL/Library/Old_Recdef.thy
 changeset 58184 db1381d811ab parent 56248 67dc9549fa15 child 58825 2065f49da190
equal 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`