equal
deleted
inserted
replaced
65 qed |
65 qed |
66 |
66 |
67 |
67 |
68 (** merges **) |
68 (** merges **) |
69 |
69 |
70 lemma length_merges [rule_format, simp]: |
70 lemma length_merges [simp]: "size(merges f ps ss) = size ss" |
71 "\<forall>ss. size(merges f ps ss) = size ss" |
71 by (induct ps arbitrary: ss) auto |
72 by (induct_tac ps, auto) |
|
73 |
72 |
74 |
73 |
75 lemma (in Semilat) merges_preserves_type_lemma: |
74 lemma (in Semilat) merges_preserves_type_lemma: |
76 shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A) |
75 shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A) |
77 \<longrightarrow> merges f ps xs \<in> list n A" |
76 \<longrightarrow> merges f ps xs \<in> list n A" |