summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 27 Sep 2018 07:18:34 +0200 | |

changeset 69075 | 6e1b569ccce1 |

parent 69074 | 787f3db8e313 |

child 69076 | 90cce2f79e77 |

simpler def

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Wed Sep 26 22:38:16 2018 +0200 +++ b/src/HOL/List.thy Thu Sep 27 07:18:34 2018 +0200 @@ -258,10 +258,13 @@ hide_const (open) n_lists -fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where +function splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where "splice [] ys = ys" | -"splice xs [] = xs" | -"splice (x#xs) (y#ys) = x # y # splice xs ys" +"splice (x#xs) ys = x # splice ys xs" +by pat_completeness auto + +termination +by(relation "measure(\<lambda>(xs,ys). size xs + size ys)") auto function shuffle where "shuffle [] ys = {ys}" @@ -4522,18 +4525,18 @@ subsubsection \<open>@{const splice}\<close> -lemma splice_Nil2 [simp, code]: "splice xs [] = xs" +lemma splice_Nil2 [simp]: "splice xs [] = xs" by (cases xs) simp_all -declare splice.simps(1,3)[code] -declare splice.simps(2)[simp del] - lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys" by (induct xs ys rule: splice.induct) auto subsubsection \<open>@{const shuffle}\<close> +lemma shuffle_commutes: "shuffle xs ys = shuffle ys xs" +by (induction xs ys rule: shuffle.induct) (simp_all add: Un_commute) + lemma Nil_in_shuffle[simp]: "[] \<in> shuffle xs ys \<longleftrightarrow> xs = [] \<and> ys = []" by (induct xs ys rule: shuffle.induct) auto @@ -4552,7 +4555,7 @@ by (induct xs ys rule: shuffle.induct) auto lemma splice_in_shuffle [simp, intro]: "splice xs ys \<in> shuffle xs ys" - by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffle_iff) +by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffle_iff shuffle_commutes) lemma Nil_in_shuffleI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffle xs ys" by simp @@ -4585,9 +4588,6 @@ qed simp_all qed simp_all -lemma shuffle_commutes: "shuffle xs ys = shuffle ys xs" - by (induction xs ys rule: shuffle.induct) (simp_all add: Un_commute) - lemma Cons_shuffle_subset1: "(#) x ` shuffle xs ys \<subseteq> shuffle (x # xs) ys" by (cases ys) auto