dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
authorhaftmann
Mon Oct 25 13:34:58 2010 +0200 (2010-10-25)
changeset 401221d8ad2ff3e01
parent 40121 e7a80c6752c9
child 40123 cfed65476db7
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
src/HOL/Library/Dlist.thy
src/HOL/Library/Permutation.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Dlist.thy	Mon Oct 25 13:34:57 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Oct 25 13:34:58 2010 +0200
     1.3 @@ -143,11 +143,11 @@
     1.4    proof (induct xs)
     1.5      case Nil from empty show ?case by (simp add: empty_def)
     1.6    next
     1.7 -    case (insert x xs)
     1.8 +    case (Cons x xs)
     1.9      then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
    1.10        by (simp_all add: member_def List.member_def)
    1.11      with insrt have "P (insert x (Dlist xs))" .
    1.12 -    with insert show ?case by (simp add: insert_def distinct_remdups_id)
    1.13 +    with Cons show ?case by (simp add: insert_def distinct_remdups_id)
    1.14    qed
    1.15    with dxs show "P dxs" by simp
    1.16  qed
     2.1 --- a/src/HOL/Library/Permutation.thy	Mon Oct 25 13:34:57 2010 +0200
     2.2 +++ b/src/HOL/Library/Permutation.thy	Mon Oct 25 13:34:58 2010 +0200
     2.3 @@ -168,7 +168,7 @@
     2.4      apply simp
     2.5      apply (subgoal_tac "a#list <~~> a#ysa@zs")
     2.6       apply (metis Cons_eq_appendI perm_append_Cons trans)
     2.7 -    apply (metis Cons Cons_eq_appendI distinct_simps(2)
     2.8 +    apply (metis Cons Cons_eq_appendI distinct.simps(2)
     2.9        distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
    2.10     apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
    2.11      apply (fastsimp simp add: insert_ident)
     3.1 --- a/src/HOL/List.thy	Mon Oct 25 13:34:57 2010 +0200
     3.2 +++ b/src/HOL/List.thy	Mon Oct 25 13:34:58 2010 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* The datatype of finite lists *}
     3.5  
     3.6  theory List
     3.7 -imports Plain Quotient Presburger Code_Numeral Recdef
     3.8 +imports Plain Presburger Recdef Code_Numeral Quotient
     3.9  uses ("Tools/list_code.ML")
    3.10  begin
    3.11  
    3.12 @@ -174,15 +174,10 @@
    3.13      "removeAll x [] = []"
    3.14    | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
    3.15  
    3.16 -inductive
    3.17 +primrec
    3.18    distinct :: "'a list \<Rightarrow> bool" where
    3.19 -    Nil: "distinct []"
    3.20 -  | insert: "x \<notin> set xs \<Longrightarrow> distinct xs \<Longrightarrow> distinct (x # xs)"
    3.21 -
    3.22 -lemma distinct_simps [simp, code]:
    3.23 -  "distinct [] \<longleftrightarrow> True"
    3.24 -  "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
    3.25 -  by (auto intro: distinct.intros elim: distinct.cases)
    3.26 +    "distinct [] \<longleftrightarrow> True"
    3.27 +  | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
    3.28  
    3.29  primrec
    3.30    remdups :: "'a list \<Rightarrow> 'a list" where
    3.31 @@ -786,9 +781,8 @@
    3.32  by (induct xs) auto
    3.33  
    3.34  lemma map_cong [fundef_cong, recdef_cong]:
    3.35 -"xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
    3.36 --- {* a congruence rule for @{text map} *}
    3.37 -by simp
    3.38 +  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys"
    3.39 +  by simp
    3.40  
    3.41  lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
    3.42  by (cases xs) auto
    3.43 @@ -990,14 +984,14 @@
    3.44    "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
    3.45    by (auto dest!: split_list_first)
    3.46  
    3.47 -lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
    3.48 -proof (induct xs rule:rev_induct)
    3.49 +lemma split_list_last: "x \<in> set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
    3.50 +proof (induct xs rule: rev_induct)
    3.51    case Nil thus ?case by simp
    3.52  next
    3.53    case (snoc a xs)
    3.54    show ?case
    3.55    proof cases
    3.56 -    assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
    3.57 +    assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE)
    3.58    next
    3.59      assume "x \<noteq> a" thus ?case using snoc by fastsimp
    3.60    qed
    3.61 @@ -1030,8 +1024,7 @@
    3.62    show ?case
    3.63    proof cases
    3.64      assume "P x"
    3.65 -    thus ?thesis by simp
    3.66 -      (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
    3.67 +    thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
    3.68    next
    3.69      assume "\<not> P x"
    3.70      hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp