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

author | haftmann |

Mon, 24 May 2010 13:48:56 +0200 | |

changeset 37106 | d56e0b30ce5a |

parent 37105 | e464f84f3680 |

child 37107 | 1535aa1c943a |

induction and case rules

--- a/src/HOL/Library/Dlist.thy Mon May 24 10:48:32 2010 +0200 +++ b/src/HOL/Library/Dlist.thy Mon May 24 13:48:56 2010 +0200 @@ -107,6 +107,49 @@ by simp +section {* Induction principle and case distinction *} + +lemma dlist_induct [case_names empty insert, induct type: dlist]: + assumes empty: "P empty" + assumes insrt: "\<And>x dxs. \<not> member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (insert x dxs)" + shows "P dxs" +proof (cases dxs) + case (Abs_dlist xs) + then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id) + from `distinct xs` have "P (Dlist xs)" + proof (induct xs rule: distinct_induct) + case Nil from empty show ?case by (simp add: empty_def) + next + case (insert x xs) + then have "\<not> member (Dlist xs) x" and "P (Dlist xs)" + by (simp_all add: member_def mem_iff) + with insrt have "P (insert x (Dlist xs))" . + with insert show ?case by (simp add: insert_def distinct_remdups_id) + qed + with dxs show "P dxs" by simp +qed + +lemma dlist_case [case_names empty insert, cases type: dlist]: + assumes empty: "dxs = empty \<Longrightarrow> P" + assumes insert: "\<And>x dys. \<not> member dys x \<Longrightarrow> dxs = insert x dys \<Longrightarrow> P" + shows P +proof (cases dxs) + case (Abs_dlist xs) + then have dxs: "dxs = Dlist xs" and distinct: "distinct xs" + by (simp_all add: Dlist_def distinct_remdups_id) + show P proof (cases xs) + case Nil with dxs have "dxs = empty" by (simp add: empty_def) + with empty show P . + next + case (Cons x xs) + with dxs distinct have "\<not> member (Dlist xs) x" + and "dxs = insert x (Dlist xs)" + by (simp_all add: member_def mem_iff insert_def distinct_remdups_id) + with insert show P . + qed +qed + + section {* Implementation of sets by distinct lists -- canonical! *} definition Set :: "'a dlist \<Rightarrow> 'a fset" where