equal
deleted
inserted
replaced
349 done |
349 done |
350 |
350 |
351 subsection{*Injectivity of @{term FnCall}*} |
351 subsection{*Injectivity of @{term FnCall}*} |
352 |
352 |
353 definition |
353 definition |
354 fun :: "exp \<Rightarrow> nat" |
354 "fun" :: "exp \<Rightarrow> nat" |
355 "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})" |
355 "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})" |
356 |
356 |
357 lemma fun_respects: "(%U. {freefun U}) respects exprel" |
357 lemma fun_respects: "(%U. {freefun U}) respects exprel" |
358 by (simp add: congruent_def exprel_imp_eq_freefun) |
358 by (simp add: congruent_def exprel_imp_eq_freefun) |
359 |
359 |