non-inductive fold1Set proofs
authorpaulson
Thu Feb 10 16:03:18 2005 +0100 (2005-02-10)
changeset 155211ffd04343ac9
parent 15520 0ed33cd8f238
child 15522 ec0fd05b2f2c
non-inductive fold1Set proofs
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Feb 10 13:01:46 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Feb 10 16:03:18 2005 +0100
     1.3 @@ -1699,17 +1699,16 @@
     1.4  
     1.5  text{*First, some lemmas about @{term foldSet}.*}
     1.6  
     1.7 -
     1.8  lemma (in ACf) foldSet_insert_swap:
     1.9  assumes fold: "(A,y) \<in> foldSet f id b"
    1.10 -shows "\<lbrakk> z \<notin> A; b \<notin> A; z \<noteq> b \<rbrakk> \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
    1.11 +shows "b \<notin> A \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
    1.12  using fold
    1.13  proof (induct rule: foldSet.induct)
    1.14    case emptyI thus ?case by (force simp add: fold_insert_aux commute)
    1.15  next
    1.16    case (insertI A x y)
    1.17      have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
    1.18 -      using insertI by force
    1.19 +      using insertI by force  --{*how does @{term id} get unfolded?*}
    1.20      thus ?case by (simp add: insert_commute AC)
    1.21  qed
    1.22  
    1.23 @@ -1721,23 +1720,20 @@
    1.24    case emptyI thus ?case by simp
    1.25  next
    1.26    case (insertI A x y)
    1.27 -  show ?case
    1.28 -  proof -
    1.29 -    have a: "a \<in> insert x A" and b: "b \<notin> insert x A" .
    1.30 -    from a have "a = x \<or> a \<in> A" by simp
    1.31 -    thus "(insert b (insert x A - {a}), id x \<cdot> y) \<in> foldSet f id a"
    1.32 -    proof
    1.33 -      assume "a = x"
    1.34 -      with insertI b show ?thesis by simp (blast intro: foldSet_insert_swap)
    1.35 -    next
    1.36 -      assume ainA: "a \<in> A"
    1.37 -      hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
    1.38 -	using insertI b by (force simp:id_def)
    1.39 -      moreover
    1.40 -      have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
    1.41 -	using ainA insertI by blast
    1.42 -      ultimately show ?thesis by simp
    1.43 -    qed
    1.44 +  have "a = x \<or> a \<in> A" using insertI by simp
    1.45 +  thus ?case
    1.46 +  proof
    1.47 +    assume "a = x"
    1.48 +    with insertI show ?thesis
    1.49 +      by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
    1.50 +  next
    1.51 +    assume ainA: "a \<in> A"
    1.52 +    hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
    1.53 +      using insertI by (force simp: id_def)
    1.54 +    moreover
    1.55 +    have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
    1.56 +      using ainA insertI by blast
    1.57 +    ultimately show ?thesis by (simp add: id_def)
    1.58    qed
    1.59  qed
    1.60  
    1.61 @@ -1756,24 +1752,47 @@
    1.62  apply (auto dest: foldSet_permute_diff [where a=a]) 
    1.63  done
    1.64  
    1.65 -lemma (in ACf) fold1_insert:
    1.66 -  "finite A ==> x \<notin> A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
    1.67 -apply (induct A rule: finite_induct, force)
    1.68 -apply (simp only: insert_commute, simp) 
    1.69 -apply (erule conjE) 
    1.70 -apply (simp add: fold1_eq_fold) 
    1.71 -apply (subst fold1_eq_fold, auto) 
    1.72 +lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
    1.73 +apply safe
    1.74 +apply simp 
    1.75 +apply (drule_tac x=x in spec)
    1.76 +apply (drule_tac x="A-{x}" in spec, auto) 
    1.77  done
    1.78  
    1.79 +lemma (in ACf) fold1_insert:
    1.80 +  assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
    1.81 +  shows "fold1 f (insert x A) = f x (fold1 f A)"
    1.82 +proof -
    1.83 +  from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
    1.84 +    by (auto simp add: nonempty_iff)
    1.85 +  with A show ?thesis
    1.86 +    by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
    1.87 +qed
    1.88 +
    1.89  lemma (in ACIf) fold1_insert_idem [simp]:
    1.90 -  "finite A ==> A \<noteq> {} \<Longrightarrow> fold1 f (insert x A) = f x (fold1 f A)"
    1.91 -apply (induct A rule: finite_induct, force)
    1.92 -apply (case_tac "xa=x") 
    1.93 - prefer 2 apply (simp add: insert_commute fold1_eq_fold fold_insert_idem) 
    1.94 -apply (case_tac "F={}") 
    1.95 -apply (simp add: idem) 
    1.96 -apply (simp add: fold1_insert assoc [symmetric] idem) 
    1.97 -done
    1.98 +  assumes nonempty: "A \<noteq> {}" and A: "finite A" 
    1.99 +  shows "fold1 f (insert x A) = f x (fold1 f A)"
   1.100 +proof -
   1.101 +  from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
   1.102 +    by (auto simp add: nonempty_iff)
   1.103 +  show ?thesis
   1.104 +  proof cases
   1.105 +    assume "a = x"
   1.106 +    thus ?thesis 
   1.107 +    proof cases
   1.108 +      assume "A' = {}"
   1.109 +      with prems show ?thesis by (simp add: idem) 
   1.110 +    next
   1.111 +      assume "A' \<noteq> {}"
   1.112 +      with prems show ?thesis
   1.113 +	by (simp add: fold1_insert assoc [symmetric] idem) 
   1.114 +    qed
   1.115 +  next
   1.116 +    assume "a \<noteq> x"
   1.117 +    with prems show ?thesis
   1.118 +      by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
   1.119 +  qed
   1.120 +qed
   1.121  
   1.122  
   1.123  text{* Now the recursion rules for definitions: *}