equal
deleted
inserted
replaced
43 subsection{*Well-Founded Recursion*} |
43 subsection{*Well-Founded Recursion*} |
44 |
44 |
45 text{*cut*} |
45 text{*cut*} |
46 |
46 |
47 lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))" |
47 lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))" |
48 by (simp add: ext_iff cut_def) |
48 by (simp add: fun_eq_iff cut_def) |
49 |
49 |
50 lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" |
50 lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" |
51 by (simp add: cut_def) |
51 by (simp add: cut_def) |
52 |
52 |
53 text{*Inductive characterization of wfrec combinator; for details see: |
53 text{*Inductive characterization of wfrec combinator; for details see: |