src/HOL/Library/Dlist.thy
changeset 37106 d56e0b30ce5a
parent 37029 d754fb55a20f
child 37473 013f78aed840
     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