equal
deleted
inserted
replaced
36 lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric] |
36 lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric] |
37 |
37 |
38 |
38 |
39 lemma (in Semilat) nth_merges: |
39 lemma (in Semilat) nth_merges: |
40 "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow> |
40 "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow> |
41 (merges f ps ss)!p = map snd (filter (\<lambda>(p',t'). p'=p) ps) ++_f ss!p" |
41 (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p" |
42 (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps") |
42 (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps") |
43 proof (induct ps) |
43 proof (induct ps) |
44 show "\<And>ss. ?P ss []" by simp |
44 show "\<And>ss. ?P ss []" by simp |
45 |
45 |
46 fix ss p' ps' |
46 fix ss p' ps' |