equal
deleted
inserted
replaced
87 |
87 |
88 subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close> |
88 subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close> |
89 |
89 |
90 definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" |
90 definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" |
91 where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}" |
91 where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}" |
92 \<comment> \<open>For @{const wfrec} declarations where the first n parameters |
92 \<comment> \<open>For \<^const>\<open>wfrec\<close> declarations where the first n parameters |
93 stay unchanged in the recursive call.\<close> |
93 stay unchanged in the recursive call.\<close> |
94 |
94 |
95 lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R" |
95 lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R" |
96 by (simp add: same_fst_def) |
96 by (simp add: same_fst_def) |
97 |
97 |