author | haftmann |

Mon May 24 13:48:56 2010 +0200 (2010-05-24) | |

changeset 37106 | d56e0b30ce5a |

parent 37105 | e464f84f3680 |

child 37107 | 1535aa1c943a |

induction and case rules

1.1 --- a/src/HOL/Library/Dlist.thy Mon May 24 10:48:32 2010 +0200 1.2 +++ b/src/HOL/Library/Dlist.thy Mon May 24 13:48:56 2010 +0200 1.3 @@ -107,6 +107,49 @@ 1.4 by simp 1.5 1.6 1.7 +section {* Induction principle and case distinction *} 1.8 + 1.9 +lemma dlist_induct [case_names empty insert, induct type: dlist]: 1.10 + assumes empty: "P empty" 1.11 + assumes insrt: "\<And>x dxs. \<not> member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (insert x dxs)" 1.12 + shows "P dxs" 1.13 +proof (cases dxs) 1.14 + case (Abs_dlist xs) 1.15 + then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id) 1.16 + from `distinct xs` have "P (Dlist xs)" 1.17 + proof (induct xs rule: distinct_induct) 1.18 + case Nil from empty show ?case by (simp add: empty_def) 1.19 + next 1.20 + case (insert x xs) 1.21 + then have "\<not> member (Dlist xs) x" and "P (Dlist xs)" 1.22 + by (simp_all add: member_def mem_iff) 1.23 + with insrt have "P (insert x (Dlist xs))" . 1.24 + with insert show ?case by (simp add: insert_def distinct_remdups_id) 1.25 + qed 1.26 + with dxs show "P dxs" by simp 1.27 +qed 1.28 + 1.29 +lemma dlist_case [case_names empty insert, cases type: dlist]: 1.30 + assumes empty: "dxs = empty \<Longrightarrow> P" 1.31 + assumes insert: "\<And>x dys. \<not> member dys x \<Longrightarrow> dxs = insert x dys \<Longrightarrow> P" 1.32 + shows P 1.33 +proof (cases dxs) 1.34 + case (Abs_dlist xs) 1.35 + then have dxs: "dxs = Dlist xs" and distinct: "distinct xs" 1.36 + by (simp_all add: Dlist_def distinct_remdups_id) 1.37 + show P proof (cases xs) 1.38 + case Nil with dxs have "dxs = empty" by (simp add: empty_def) 1.39 + with empty show P . 1.40 + next 1.41 + case (Cons x xs) 1.42 + with dxs distinct have "\<not> member (Dlist xs) x" 1.43 + and "dxs = insert x (Dlist xs)" 1.44 + by (simp_all add: member_def mem_iff insert_def distinct_remdups_id) 1.45 + with insert show P . 1.46 + qed 1.47 +qed 1.48 + 1.49 + 1.50 section {* Implementation of sets by distinct lists -- canonical! *} 1.51 1.52 definition Set :: "'a dlist \<Rightarrow> 'a fset" where