Adapted to new inductive definition package.
authorberghofe
Wed Feb 07 17:28:09 2007 +0100 (2007-02-07)
changeset 2226296ba62dff413
parent 22261 9e185f78e7d4
child 22263 990a638e6f69
Adapted to new inductive definition package.
src/HOL/Accessible_Part.thy
src/HOL/Finite_Set.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Accessible_Part.thy	Wed Feb 07 17:26:49 2007 +0100
     1.2 +++ b/src/HOL/Accessible_Part.thy	Wed Feb 07 17:28:09 2007 +0100
     1.3 @@ -17,22 +17,22 @@
     1.4   relation; see also \cite{paulin-tlca}.
     1.5  *}
     1.6  
     1.7 -consts
     1.8 -  acc :: "('a \<times> 'a) set => 'a set"
     1.9 -inductive "acc r"
    1.10 -  intros
    1.11 -    accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r"
    1.12 +inductive2
    1.13 +  acc :: "('a => 'a => bool) => 'a => bool"
    1.14 +  for r :: "'a => 'a => bool"
    1.15 +  where
    1.16 +    accI: "(!!y. r y x ==> acc r y) ==> acc r x"
    1.17  
    1.18  abbreviation
    1.19 -  termi :: "('a \<times> 'a) set => 'a set" where
    1.20 -  "termi r == acc (r\<inverse>)"
    1.21 +  termi :: "('a => 'a => bool) => 'a => bool" where
    1.22 +  "termi r == acc (r\<inverse>\<inverse>)"
    1.23  
    1.24  
    1.25  subsection {* Induction rules *}
    1.26  
    1.27  theorem acc_induct:
    1.28 -  assumes major: "a \<in> acc r"
    1.29 -  assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
    1.30 +  assumes major: "acc r a"
    1.31 +  assumes hyp: "!!x. acc r x ==> \<forall>y. r y x --> P y ==> P x"
    1.32    shows "P a"
    1.33    apply (rule major [THEN acc.induct])
    1.34    apply (rule hyp)
    1.35 @@ -43,35 +43,55 @@
    1.36  
    1.37  theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]
    1.38  
    1.39 -theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r"
    1.40 -  apply (erule acc.elims)
    1.41 +theorem acc_downward: "acc r b ==> r a b ==> acc r a"
    1.42 +  apply (erule acc.cases)
    1.43    apply fast
    1.44    done
    1.45  
    1.46 -lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r --> b \<in> acc r"
    1.47 -  apply (erule rtrancl_induct)
    1.48 +lemma not_acc_down:
    1.49 +  assumes na: "\<not> acc R x"
    1.50 +  obtains z where "R z x" and "\<not> acc R z"
    1.51 +proof -
    1.52 +  assume a: "\<And>z. \<lbrakk>R z x; \<not> acc R z\<rbrakk> \<Longrightarrow> thesis"
    1.53 +
    1.54 +  show thesis
    1.55 +  proof (cases "\<forall>z. R z x \<longrightarrow> acc R z")
    1.56 +    case True
    1.57 +    hence "\<And>z. R z x \<Longrightarrow> acc R z" by auto
    1.58 +    hence "acc R x"
    1.59 +      by (rule accI)
    1.60 +    with na show thesis ..
    1.61 +  next
    1.62 +    case False then obtain z where "R z x" and "\<not> acc R z"
    1.63 +      by auto
    1.64 +    with a show thesis .
    1.65 +  qed
    1.66 +qed
    1.67 +
    1.68 +lemma acc_downwards_aux: "r\<^sup>*\<^sup>* b a ==> acc r a --> acc r b"
    1.69 +  apply (erule rtrancl_induct')
    1.70     apply blast
    1.71    apply (blast dest: acc_downward)
    1.72    done
    1.73  
    1.74 -theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r"
    1.75 +theorem acc_downwards: "acc r a ==> r\<^sup>*\<^sup>* b a ==> acc r b"
    1.76    apply (blast dest: acc_downwards_aux)
    1.77    done
    1.78  
    1.79 -theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r"
    1.80 -  apply (rule wfUNIVI)
    1.81 +theorem acc_wfI: "\<forall>x. acc r x ==> wfP r"
    1.82 +  apply (rule wfPUNIVI)
    1.83    apply (induct_tac P x rule: acc_induct)
    1.84     apply blast
    1.85    apply blast
    1.86    done
    1.87  
    1.88 -theorem acc_wfD: "wf r ==> x \<in> acc r"
    1.89 -  apply (erule wf_induct)
    1.90 +theorem acc_wfD: "wfP r ==> acc r x"
    1.91 +  apply (erule wfP_induct_rule)
    1.92    apply (rule accI)
    1.93    apply blast
    1.94    done
    1.95  
    1.96 -theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)"
    1.97 +theorem wf_acc_iff: "wfP r = (\<forall>x. acc r x)"
    1.98    apply (blast intro: acc_wfI dest: acc_wfD)
    1.99    done
   1.100  
   1.101 @@ -79,16 +99,16 @@
   1.102  text {* Smaller relations have bigger accessible parts: *}
   1.103  
   1.104  lemma acc_subset:
   1.105 -  assumes sub: "R1 \<subseteq> R2"
   1.106 -  shows "acc R2 \<subseteq> acc R1"
   1.107 +  assumes sub: "R1 \<le> R2"
   1.108 +  shows "acc R2 \<le> acc R1"
   1.109  proof
   1.110 -  fix x assume "x \<in> acc R2"
   1.111 -  then show "x \<in> acc R1"
   1.112 +  fix x assume "acc R2 x"
   1.113 +  then show "acc R1 x"
   1.114    proof (induct x)
   1.115      fix x
   1.116 -    assume ih: "\<And>y. (y, x) \<in> R2 \<Longrightarrow> y \<in> acc R1"
   1.117 -    with sub show "x \<in> acc R1"
   1.118 -      by (blast intro:accI)
   1.119 +    assume ih: "\<And>y. R2 y x \<Longrightarrow> acc R1 y"
   1.120 +    with sub show "acc R1 x"
   1.121 +      by (blast intro: accI)
   1.122    qed
   1.123  qed
   1.124  
   1.125 @@ -97,19 +117,19 @@
   1.126    subsets of the accessible part. *}
   1.127  
   1.128  lemma acc_subset_induct:
   1.129 -  assumes subset: "D \<subseteq> acc R"
   1.130 -    and dcl: "\<And>x z. \<lbrakk>x \<in> D; (z, x)\<in>R\<rbrakk> \<Longrightarrow> z \<in> D"
   1.131 -    and "x \<in> D"
   1.132 -    and istep: "\<And>x. \<lbrakk>x \<in> D; (\<And>z. (z, x)\<in>R \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   1.133 +  assumes subset: "D \<le> acc R"
   1.134 +    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
   1.135 +    and "D x"
   1.136 +    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   1.137    shows "P x"
   1.138  proof -
   1.139 -  from `x \<in> D` and subset 
   1.140 -  have "x \<in> acc R" ..
   1.141 -  then show "P x" using `x \<in> D`
   1.142 +  from subset and `D x`
   1.143 +  have "acc R x" ..
   1.144 +  then show "P x" using `D x`
   1.145    proof (induct x)
   1.146      fix x
   1.147 -    assume "x \<in> D"
   1.148 -      and "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<in> D \<Longrightarrow> P y"
   1.149 +    assume "D x"
   1.150 +      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
   1.151      with dcl and istep show "P x" by blast
   1.152    qed
   1.153  qed
     2.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 07 17:26:49 2007 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Wed Feb 07 17:28:09 2007 +0100
     2.3 @@ -12,14 +12,10 @@
     2.4  
     2.5  subsection {* Definition and basic properties *}
     2.6  
     2.7 -consts Finites :: "'a set set"
     2.8 -abbreviation
     2.9 -  "finite A == A : Finites"
    2.10 -
    2.11 -inductive Finites
    2.12 -  intros
    2.13 -    emptyI [simp, intro!]: "{} : Finites"
    2.14 -    insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
    2.15 +inductive2 finite :: "'a set => bool"
    2.16 +  where
    2.17 +    emptyI [simp, intro!]: "finite {}"
    2.18 +  | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
    2.19  
    2.20  axclass finite \<subseteq> type
    2.21    finite: "finite UNIV"
    2.22 @@ -32,7 +28,7 @@
    2.23    thus ?thesis by blast
    2.24  qed
    2.25  
    2.26 -lemma finite_induct [case_names empty insert, induct set: Finites]:
    2.27 +lemma finite_induct [case_names empty insert, induct set: finite]:
    2.28    "finite F ==>
    2.29      P {} ==> (!!x F. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F"
    2.30    -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
    2.31 @@ -146,7 +142,7 @@
    2.32  
    2.33  lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
    2.34    -- {* The union of two finite sets is finite. *}
    2.35 -  by (induct set: Finites) simp_all
    2.36 +  by (induct set: finite) simp_all
    2.37  
    2.38  lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
    2.39    -- {* Every subset of a finite set is finite. *}
    2.40 @@ -244,7 +240,7 @@
    2.41  
    2.42  lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
    2.43    -- {* The image of a finite set is finite. *}
    2.44 -  by (induct set: Finites) simp_all
    2.45 +  by (induct set: finite) simp_all
    2.46  
    2.47  lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
    2.48    apply (frule finite_imageI)
    2.49 @@ -286,7 +282,7 @@
    2.50  lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
    2.51    -- {* The inverse image of a finite set under an injective function
    2.52           is finite. *}
    2.53 -  apply (induct set: Finites)
    2.54 +  apply (induct set: finite)
    2.55     apply simp_all
    2.56    apply (subst vimage_insert)
    2.57    apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
    2.58 @@ -296,7 +292,7 @@
    2.59  text {* The finite UNION of finite sets *}
    2.60  
    2.61  lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
    2.62 -  by (induct set: Finites) simp_all
    2.63 +  by (induct set: finite) simp_all
    2.64  
    2.65  text {*
    2.66    Strengthen RHS to
    2.67 @@ -398,7 +394,7 @@
    2.68  
    2.69  lemma finite_Field: "finite r ==> finite (Field r)"
    2.70    -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
    2.71 -  apply (induct set: Finites)
    2.72 +  apply (induct set: finite)
    2.73     apply (auto simp add: Field_def Domain_insert Range_insert)
    2.74    done
    2.75  
    2.76 @@ -427,38 +423,39 @@
    2.77  se the definitions of sums and products over finite sets.
    2.78  *}
    2.79  
    2.80 -consts
    2.81 -  foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \<times> 'a) set"
    2.82 -
    2.83 -inductive "foldSet f g z"
    2.84 -intros
    2.85 -emptyI [intro]: "({}, z) : foldSet f g z"
    2.86 -insertI [intro]:
    2.87 -     "\<lbrakk> x \<notin> A; (A, y) : foldSet f g z \<rbrakk>
    2.88 -      \<Longrightarrow> (insert x A, f (g x) y) : foldSet f g z"
    2.89 -
    2.90 -inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z"
    2.91 +inductive2
    2.92 +  foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool"
    2.93 +  for f ::  "'a => 'a => 'a"
    2.94 +  and g :: "'b => 'a"
    2.95 +  and z :: 'a
    2.96 +where
    2.97 +  emptyI [intro]: "foldSet f g z {} z"
    2.98 +| insertI [intro]:
    2.99 +     "\<lbrakk> x \<notin> A; foldSet f g z A y \<rbrakk>
   2.100 +      \<Longrightarrow> foldSet f g z (insert x A) (f (g x) y)"
   2.101 +
   2.102 +inductive_cases2 empty_foldSetE [elim!]: "foldSet f g z {} x"
   2.103  
   2.104  constdefs
   2.105    fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
   2.106 -  "fold f g z A == THE x. (A, x) : foldSet f g z"
   2.107 +  "fold f g z A == THE x. foldSet f g z A x"
   2.108  
   2.109  text{*A tempting alternative for the definiens is
   2.110 -@{term "if finite A then THE x. (A, x) : foldSet f g e else e"}.
   2.111 +@{term "if finite A then THE x. foldSet f g e A x else e"}.
   2.112  It allows the removal of finiteness assumptions from the theorems
   2.113  @{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}.
   2.114  The proofs become ugly, with @{text rule_format}. It is not worth the effort.*}
   2.115  
   2.116  
   2.117  lemma Diff1_foldSet:
   2.118 -  "(A - {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z"
   2.119 +  "foldSet f g z (A - {x}) y ==> x: A ==> foldSet f g z A (f (g x) y)"
   2.120  by (erule insert_Diff [THEN subst], rule foldSet.intros, auto)
   2.121  
   2.122 -lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A"
   2.123 +lemma foldSet_imp_finite: "foldSet f g z A x==> finite A"
   2.124    by (induct set: foldSet) auto
   2.125  
   2.126 -lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g z"
   2.127 -  by (induct set: Finites) auto
   2.128 +lemma finite_imp_foldSet: "finite A ==> EX x. foldSet f g z A x"
   2.129 +  by (induct set: finite) auto
   2.130  
   2.131  
   2.132  subsubsection {* Commutative monoids *}
   2.133 @@ -554,33 +551,31 @@
   2.134  
   2.135  lemma (in ACf) foldSet_determ_aux:
   2.136    "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; inj_on h {i. i<n}; 
   2.137 -                (A,x) : foldSet f g z; (A,x') : foldSet f g z \<rbrakk>
   2.138 +                foldSet f g z A x; foldSet f g z A x' \<rbrakk>
   2.139     \<Longrightarrow> x' = x"
   2.140  proof (induct n rule: less_induct)
   2.141    case (less n)
   2.142      have IH: "!!m h A x x'. 
   2.143                 \<lbrakk>m<n; A = h ` {i. i<m}; inj_on h {i. i<m}; 
   2.144 -                (A,x) \<in> foldSet f g z; (A, x') \<in> foldSet f g z\<rbrakk> \<Longrightarrow> x' = x" .
   2.145 -    have Afoldx: "(A,x) \<in> foldSet f g z" and Afoldx': "(A,x') \<in> foldSet f g z"
   2.146 +                foldSet f g z A x; foldSet f g z A x'\<rbrakk> \<Longrightarrow> x' = x" .
   2.147 +    have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'"
   2.148       and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" .
   2.149      show ?case
   2.150      proof (rule foldSet.cases [OF Afoldx])
   2.151 -      assume "(A, x) = ({}, z)"
   2.152 +      assume "A = {}" and "x = z"
   2.153        with Afoldx' show "x' = x" by blast
   2.154      next
   2.155        fix B b u
   2.156 -      assume "(A,x) = (insert b B, g b \<cdot> u)" and notinB: "b \<notin> B"
   2.157 -         and Bu: "(B,u) \<in> foldSet f g z"
   2.158 -      hence AbB: "A = insert b B" and x: "x = g b \<cdot> u" by auto
   2.159 +      assume AbB: "A = insert b B" and x: "x = g b \<cdot> u"
   2.160 +         and notinB: "b \<notin> B" and Bu: "foldSet f g z B u"
   2.161        show "x'=x" 
   2.162        proof (rule foldSet.cases [OF Afoldx'])
   2.163 -        assume "(A, x') = ({}, z)"
   2.164 +        assume "A = {}" and "x' = z"
   2.165          with AbB show "x' = x" by blast
   2.166        next
   2.167  	fix C c v
   2.168 -	assume "(A,x') = (insert c C, g c \<cdot> v)" and notinC: "c \<notin> C"
   2.169 -	   and Cv: "(C,v) \<in> foldSet f g z"
   2.170 -	hence AcC: "A = insert c C" and x': "x' = g c \<cdot> v" by auto
   2.171 +	assume AcC: "A = insert c C" and x': "x' = g c \<cdot> v"
   2.172 +           and notinC: "c \<notin> C" and Cv: "foldSet f g z C v"
   2.173  	from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
   2.174          from insert_inj_onE [OF Beq notinB injh]
   2.175          obtain hB mB where inj_onB: "inj_on hB {i. i < mB}" 
   2.176 @@ -604,15 +599,15 @@
   2.177  	    using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
   2.178  	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
   2.179  	  with AbB have "finite ?D" by simp
   2.180 -	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
   2.181 +	  then obtain d where Dfoldd: "foldSet f g z ?D d"
   2.182  	    using finite_imp_foldSet by iprover
   2.183  	  moreover have cinB: "c \<in> B" using B by auto
   2.184 -	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
   2.185 +	  ultimately have "foldSet f g z B (g c \<cdot> d)"
   2.186  	    by(rule Diff1_foldSet)
   2.187  	  hence "g c \<cdot> d = u" by (rule IH [OF lessB Beq inj_onB Bu]) 
   2.188            moreover have "g b \<cdot> d = v"
   2.189  	  proof (rule IH[OF lessC Ceq inj_onC Cv])
   2.190 -	    show "(C, g b \<cdot> d) \<in> foldSet f g z" using C notinB Dfoldd
   2.191 +	    show "foldSet f g z C (g b \<cdot> d)" using C notinB Dfoldd
   2.192  	      by fastsimp
   2.193  	  qed
   2.194  	  ultimately show ?thesis using x x' by (auto simp: AC)
   2.195 @@ -623,12 +618,12 @@
   2.196  
   2.197  
   2.198  lemma (in ACf) foldSet_determ:
   2.199 -  "(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x"
   2.200 +  "foldSet f g z A x ==> foldSet f g z A y ==> y = x"
   2.201  apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) 
   2.202  apply (blast intro: foldSet_determ_aux [rule_format])
   2.203  done
   2.204  
   2.205 -lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y"
   2.206 +lemma (in ACf) fold_equality: "foldSet f g z A y ==> fold f g z A = y"
   2.207    by (unfold fold_def) (blast intro: foldSet_determ)
   2.208  
   2.209  text{* The base case for @{text fold}: *}
   2.210 @@ -637,8 +632,8 @@
   2.211    by (unfold fold_def) blast
   2.212  
   2.213  lemma (in ACf) fold_insert_aux: "x \<notin> A ==>
   2.214 -    ((insert x A, v) : foldSet f g z) =
   2.215 -    (EX y. (A, y) : foldSet f g z & v = f (g x) y)"
   2.216 +    (foldSet f g z (insert x A) v) =
   2.217 +    (EX y. foldSet f g z A y & v = f (g x) y)"
   2.218    apply auto
   2.219    apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE])
   2.220     apply (fastsimp dest: foldSet_imp_finite)
   2.221 @@ -700,7 +695,7 @@
   2.222  
   2.223  lemma (in ACf) fold_commute:
   2.224    "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
   2.225 -  apply (induct set: Finites)
   2.226 +  apply (induct set: finite)
   2.227     apply simp
   2.228    apply (simp add: left_commute [of x])
   2.229    done
   2.230 @@ -708,7 +703,7 @@
   2.231  lemma (in ACf) fold_nest_Un_Int:
   2.232    "finite A ==> finite B
   2.233      ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)"
   2.234 -  apply (induct set: Finites)
   2.235 +  apply (induct set: finite)
   2.236     apply simp
   2.237    apply (simp add: fold_commute Int_insert_left insert_absorb)
   2.238    done
   2.239 @@ -730,7 +725,7 @@
   2.240    "finite A ==> finite B ==>
   2.241      fold f g e A \<cdot> fold f g e B =
   2.242      fold f g e (A Un B) \<cdot> fold f g e (A Int B)"
   2.243 -  apply (induct set: Finites, simp)
   2.244 +  apply (induct set: finite, simp)
   2.245    apply (simp add: AC insert_absorb Int_insert_left)
   2.246    done
   2.247  
   2.248 @@ -744,7 +739,7 @@
   2.249       ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {} \<rbrakk>
   2.250     \<Longrightarrow> fold f g e (UNION I A) =
   2.251         fold f (%i. fold f g e (A i)) e I"
   2.252 -  apply (induct set: Finites, simp, atomize)
   2.253 +  apply (induct set: finite, simp, atomize)
   2.254    apply (subgoal_tac "ALL i:F. x \<noteq> i")
   2.255     prefer 2 apply blast
   2.256    apply (subgoal_tac "A x Int UNION F A = {}")
   2.257 @@ -762,7 +757,7 @@
   2.258  	"finite A ==> 
   2.259  	 (!!x y. h (g x y) = f x (h y)) ==>
   2.260           h (fold g j w A) = fold f j (h w) A"
   2.261 -  by (induct set: Finites) simp_all
   2.262 +  by (induct set: finite) simp_all
   2.263  
   2.264  lemma (in ACf) fold_cong:
   2.265    "finite A \<Longrightarrow> (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A"
   2.266 @@ -954,7 +949,7 @@
   2.267  
   2.268  lemma setsum_eq_0_iff [simp]:
   2.269      "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   2.270 -  by (induct set: Finites) auto
   2.271 +  by (induct set: finite) auto
   2.272  
   2.273  lemma setsum_Un_nat: "finite A ==> finite B ==>
   2.274      (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   2.275 @@ -1064,7 +1059,7 @@
   2.276  lemma setsum_negf:
   2.277    "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   2.278  proof (cases "finite A")
   2.279 -  case True thus ?thesis by (induct set: Finites) auto
   2.280 +  case True thus ?thesis by (induct set: finite) auto
   2.281  next
   2.282    case False thus ?thesis by (simp add: setsum_def)
   2.283  qed
   2.284 @@ -1398,18 +1393,18 @@
   2.285  
   2.286  lemma setprod_eq_1_iff [simp]:
   2.287      "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
   2.288 -  by (induct set: Finites) auto
   2.289 +  by (induct set: finite) auto
   2.290  
   2.291  lemma setprod_zero:
   2.292       "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
   2.293 -  apply (induct set: Finites, force, clarsimp)
   2.294 +  apply (induct set: finite, force, clarsimp)
   2.295    apply (erule disjE, auto)
   2.296    done
   2.297  
   2.298  lemma setprod_nonneg [rule_format]:
   2.299       "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A"
   2.300    apply (case_tac "finite A")
   2.301 -  apply (induct set: Finites, force, clarsimp)
   2.302 +  apply (induct set: finite, force, clarsimp)
   2.303    apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
   2.304    apply (rule mult_mono, assumption+)
   2.305    apply (auto simp add: setprod_def)
   2.306 @@ -1418,7 +1413,7 @@
   2.307  lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x)
   2.308       --> 0 < setprod f A"
   2.309    apply (case_tac "finite A")
   2.310 -  apply (induct set: Finites, force, clarsimp)
   2.311 +  apply (induct set: finite, force, clarsimp)
   2.312    apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
   2.313    apply (rule mult_strict_mono, assumption+)
   2.314    apply (auto simp add: setprod_def)
   2.315 @@ -1546,7 +1541,7 @@
   2.316  by (simp add: card_def setsum_mono2)
   2.317  
   2.318  lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
   2.319 -  apply (induct set: Finites, simp, clarify)
   2.320 +  apply (induct set: finite, simp, clarify)
   2.321    apply (subgoal_tac "finite A & A - {x} <= F")
   2.322     prefer 2 apply (blast intro: finite_subset, atomize)
   2.323    apply (drule_tac x = "A - {x}" in spec)
   2.324 @@ -1698,7 +1693,7 @@
   2.325    done
   2.326  
   2.327  lemma card_image_le: "finite A ==> card (f ` A) <= card A"
   2.328 -  apply (induct set: Finites)
   2.329 +  apply (induct set: finite)
   2.330     apply simp
   2.331    apply (simp add: le_SucI finite_imageI card_insert_if)
   2.332    done
   2.333 @@ -1763,7 +1758,7 @@
   2.334  subsubsection {* Cardinality of the Powerset *}
   2.335  
   2.336  lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A"  (* FIXME numeral 2 (!?) *)
   2.337 -  apply (induct set: Finites)
   2.338 +  apply (induct set: finite)
   2.339     apply (simp_all add: Pow_insert)
   2.340    apply (subst card_Un_disjoint, blast)
   2.341      apply (blast intro: finite_imageI, blast)
   2.342 @@ -1783,7 +1778,7 @@
   2.343    k dvd card (Union C)"
   2.344  apply(frule finite_UnionD)
   2.345  apply(rotate_tac -1)
   2.346 -  apply (induct set: Finites, simp_all, clarify)
   2.347 +  apply (induct set: finite, simp_all, clarify)
   2.348    apply (subst card_Un_disjoint)
   2.349    apply (auto simp add: dvd_add disjoint_eq_subset_Compl)
   2.350    done
   2.351 @@ -1793,36 +1788,35 @@
   2.352  
   2.353  text{* Does not require start value. *}
   2.354  
   2.355 -consts
   2.356 -  fold1Set :: "('a => 'a => 'a) => ('a set \<times> 'a) set"
   2.357 -
   2.358 -inductive "fold1Set f"
   2.359 -intros
   2.360 +inductive2
   2.361 +  fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
   2.362 +  for f :: "'a => 'a => 'a"
   2.363 +where
   2.364    fold1Set_insertI [intro]:
   2.365 -   "\<lbrakk> (A,x) \<in> foldSet f id a; a \<notin> A \<rbrakk> \<Longrightarrow> (insert a A, x) \<in> fold1Set f"
   2.366 +   "\<lbrakk> foldSet f id a A x; a \<notin> A \<rbrakk> \<Longrightarrow> fold1Set f (insert a A) x"
   2.367  
   2.368  constdefs
   2.369    fold1 :: "('a => 'a => 'a) => 'a set => 'a"
   2.370 -  "fold1 f A == THE x. (A, x) : fold1Set f"
   2.371 +  "fold1 f A == THE x. fold1Set f A x"
   2.372  
   2.373  lemma fold1Set_nonempty:
   2.374 - "(A, x) : fold1Set f \<Longrightarrow> A \<noteq> {}"
   2.375 + "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
   2.376  by(erule fold1Set.cases, simp_all) 
   2.377  
   2.378  
   2.379 -inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f"
   2.380 -
   2.381 -inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f"
   2.382 -
   2.383 -
   2.384 -lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)"
   2.385 +inductive_cases2 empty_fold1SetE [elim!]: "fold1Set f {} x"
   2.386 +
   2.387 +inductive_cases2 insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
   2.388 +
   2.389 +
   2.390 +lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"
   2.391    by (blast intro: foldSet.intros elim: foldSet.cases)
   2.392  
   2.393  lemma fold1_singleton[simp]: "fold1 f {a} = a"
   2.394    by (unfold fold1_def) blast
   2.395  
   2.396  lemma finite_nonempty_imp_fold1Set:
   2.397 -  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. (A, x) : fold1Set f"
   2.398 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> EX x. fold1Set f A x"
   2.399  apply (induct A rule: finite_induct)
   2.400  apply (auto dest: finite_imp_foldSet [of _ f id])  
   2.401  done
   2.402 @@ -1830,26 +1824,26 @@
   2.403  text{*First, some lemmas about @{term foldSet}.*}
   2.404  
   2.405  lemma (in ACf) foldSet_insert_swap:
   2.406 -assumes fold: "(A,y) \<in> foldSet f id b"
   2.407 -shows "b \<notin> A \<Longrightarrow> (insert b A, z \<cdot> y) \<in> foldSet f id z"
   2.408 +assumes fold: "foldSet f id b A y"
   2.409 +shows "b \<notin> A \<Longrightarrow> foldSet f id z (insert b A) (z \<cdot> y)"
   2.410  using fold
   2.411  proof (induct rule: foldSet.induct)
   2.412    case emptyI thus ?case by (force simp add: fold_insert_aux commute)
   2.413  next
   2.414 -  case (insertI A x y)
   2.415 -    have "(insert x (insert b A), x \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z"
   2.416 +  case (insertI x A y)
   2.417 +    have "foldSet f (\<lambda>u. u) z (insert x (insert b A)) (x \<cdot> (z \<cdot> y))"
   2.418        using insertI by force  --{*how does @{term id} get unfolded?*}
   2.419      thus ?case by (simp add: insert_commute AC)
   2.420  qed
   2.421  
   2.422  lemma (in ACf) foldSet_permute_diff:
   2.423 -assumes fold: "(A,x) \<in> foldSet f id b"
   2.424 -shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> foldSet f id a"
   2.425 +assumes fold: "foldSet f id b A x"
   2.426 +shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> foldSet f id a (insert b (A-{a})) x"
   2.427  using fold
   2.428  proof (induct rule: foldSet.induct)
   2.429    case emptyI thus ?case by simp
   2.430  next
   2.431 -  case (insertI A x y)
   2.432 +  case (insertI x A y)
   2.433    have "a = x \<or> a \<in> A" using insertI by simp
   2.434    thus ?case
   2.435    proof
   2.436 @@ -1858,7 +1852,7 @@
   2.437        by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) 
   2.438    next
   2.439      assume ainA: "a \<in> A"
   2.440 -    hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> foldSet f id a"
   2.441 +    hence "foldSet f id a (insert x (insert b (A - {a}))) (x \<cdot> y)"
   2.442        using insertI by (force simp: id_def)
   2.443      moreover
   2.444      have "insert x (insert b (A - {a})) = insert b (insert x A - {a})"
   2.445 @@ -1875,7 +1869,7 @@
   2.446  apply (rule sym, clarify)
   2.447  apply (case_tac "Aa=A")
   2.448   apply (best intro: the_equality foldSet_determ)  
   2.449 -apply (subgoal_tac "(A,x) \<in> foldSet f id a") 
   2.450 +apply (subgoal_tac "foldSet f id a A x")
   2.451   apply (best intro: the_equality foldSet_determ)  
   2.452  apply (subgoal_tac "insert aa (Aa - {a}) = A") 
   2.453   prefer 2 apply (blast elim: equalityE) 
   2.454 @@ -1943,18 +1937,18 @@
   2.455  text{*Not actually used!!*}
   2.456  
   2.457  lemma (in ACf) foldSet_permute:
   2.458 -  "[|(insert a A, x) \<in> foldSet f id b; a \<notin> A; b \<notin> A|]
   2.459 -   ==> (insert b A, x) \<in> foldSet f id a"
   2.460 +  "[|foldSet f id b (insert a A) x; a \<notin> A; b \<notin> A|]
   2.461 +   ==> foldSet f id a (insert b A) x"
   2.462  apply (case_tac "a=b") 
   2.463  apply (auto dest: foldSet_permute_diff) 
   2.464  done
   2.465  
   2.466  lemma (in ACf) fold1Set_determ:
   2.467 -  "(A, x) \<in> fold1Set f ==> (A, y) \<in> fold1Set f ==> y = x"
   2.468 +  "fold1Set f A x ==> fold1Set f A y ==> y = x"
   2.469  proof (clarify elim!: fold1Set.cases)
   2.470    fix A x B y a b
   2.471 -  assume Ax: "(A, x) \<in> foldSet f id a"
   2.472 -  assume By: "(B, y) \<in> foldSet f id b"
   2.473 +  assume Ax: "foldSet f id a A x"
   2.474 +  assume By: "foldSet f id b B y"
   2.475    assume anotA:  "a \<notin> A"
   2.476    assume bnotB:  "b \<notin> B"
   2.477    assume eq: "insert a A = insert b B"
   2.478 @@ -1970,16 +1964,16 @@
   2.479       and aB: "a \<in> B" and bA: "b \<in> A"
   2.480        using eq anotA bnotB diff by (blast elim!:equalityE)+
   2.481      with aB bnotB By
   2.482 -    have "(insert b ?D, y) \<in> foldSet f id a" 
   2.483 +    have "foldSet f id a (insert b ?D) y" 
   2.484        by (auto intro: foldSet_permute simp add: insert_absorb)
   2.485      moreover
   2.486 -    have "(insert b ?D, x) \<in> foldSet f id a"
   2.487 +    have "foldSet f id a (insert b ?D) x"
   2.488        by (simp add: A [symmetric] Ax) 
   2.489      ultimately show ?thesis by (blast intro: foldSet_determ) 
   2.490    qed
   2.491  qed
   2.492  
   2.493 -lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y"
   2.494 +lemma (in ACf) fold1Set_equality: "fold1Set f A y ==> fold1 f A = y"
   2.495    by (unfold fold1_def) (blast intro: fold1Set_determ)
   2.496  
   2.497  declare
     3.1 --- a/src/HOL/List.thy	Wed Feb 07 17:26:49 2007 +0100
     3.2 +++ b/src/HOL/List.thy	Wed Feb 07 17:28:09 2007 +0100
     3.3 @@ -2200,40 +2200,71 @@
     3.4  
     3.5  subsubsection {* @{text lists}: the list-forming operator over sets *}
     3.6  
     3.7 -consts lists :: "'a set => 'a list set"
     3.8 -inductive "lists A"
     3.9 - intros
    3.10 -  Nil [intro!]: "[]: lists A"
    3.11 -  Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
    3.12 -
    3.13 -inductive_cases listsE [elim!]: "x#l : lists A"
    3.14 -
    3.15 -lemma lists_mono [mono]: "A \<subseteq> B ==> lists A \<subseteq> lists B"
    3.16 -by (unfold lists.defs) (blast intro!: lfp_mono)
    3.17 -
    3.18 -lemma lists_IntI:
    3.19 -  assumes l: "l: lists A" shows "l: lists B ==> l: lists (A Int B)" using l
    3.20 +inductive2
    3.21 +  listsp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    3.22 +  for A :: "'a \<Rightarrow> bool"
    3.23 +where
    3.24 +    Nil [intro!]: "listsp A []"
    3.25 +  | Cons [intro!]: "[| A a; listsp A l |] ==> listsp A (a # l)"
    3.26 +
    3.27 +constdefs
    3.28 +  lists :: "'a set => 'a list set"
    3.29 +  "lists A == Collect (listsp (member A))"
    3.30 +
    3.31 +lemma listsp_lists_eq [pred_set_conv]: "listsp (member A) = member (lists A)"
    3.32 +  by (simp add: lists_def)
    3.33 +
    3.34 +lemmas lists_intros [intro!] = listsp.intros [to_set]
    3.35 +
    3.36 +lemmas lists_induct [consumes 1, case_names Nil Cons, induct set: lists] =
    3.37 +  listsp.induct [to_set]
    3.38 +
    3.39 +inductive_cases2 listspE [elim!]: "listsp A (x # l)"
    3.40 +
    3.41 +lemmas listsE [elim!] = listspE [to_set]
    3.42 +
    3.43 +lemma listsp_mono [mono2]: "A \<le> B ==> listsp A \<le> listsp B"
    3.44 +  by (clarify, erule listsp.induct, blast+)
    3.45 +
    3.46 +lemmas lists_mono [mono] = listsp_mono [to_set]
    3.47 +
    3.48 +lemma listsp_meetI:
    3.49 +  assumes l: "listsp A l" shows "listsp B l ==> listsp (meet A B) l" using l
    3.50    by induct blast+
    3.51  
    3.52 -lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B"
    3.53 -proof (rule mono_Int [THEN equalityI])
    3.54 -  show "mono lists" by (simp add: mono_def lists_mono)
    3.55 -  show "lists A \<inter> lists B \<subseteq> lists (A \<inter> B)" by (blast intro: lists_IntI)
    3.56 +lemmas lists_IntI = listsp_meetI [to_set]
    3.57 +
    3.58 +lemma listsp_meet_eq [simp]: "listsp (meet A B) = meet (listsp A) (listsp B)"
    3.59 +proof (rule mono_meet [where f=listsp, THEN order_antisym])
    3.60 +  show "mono listsp" by (simp add: mono_def listsp_mono)
    3.61 +  show "meet (listsp A) (listsp B) \<le> listsp (meet A B)" by (blast intro: listsp_meetI)
    3.62  qed
    3.63  
    3.64 -lemma append_in_lists_conv [iff]:
    3.65 -     "(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)"
    3.66 +lemmas listsp_conj_eq [simp] = listsp_meet_eq [simplified meet_fun_eq meet_bool_eq]
    3.67 +
    3.68 +lemmas lists_Int_eq [simp] = listsp_meet_eq [to_set]
    3.69 +
    3.70 +lemma append_in_listsp_conv [iff]:
    3.71 +     "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
    3.72  by (induct xs) auto
    3.73  
    3.74 -lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)"
    3.75 --- {* eliminate @{text lists} in favour of @{text set} *}
    3.76 +lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
    3.77 +
    3.78 +lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
    3.79 +-- {* eliminate @{text listsp} in favour of @{text set} *}
    3.80  by (induct xs) auto
    3.81  
    3.82 -lemma in_listsD [dest!]: "xs \<in> lists A ==> \<forall>x\<in>set xs. x \<in> A"
    3.83 -by (rule in_lists_conv_set [THEN iffD1])
    3.84 -
    3.85 -lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A"
    3.86 -by (rule in_lists_conv_set [THEN iffD2])
    3.87 +lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
    3.88 +
    3.89 +lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
    3.90 +by (rule in_listsp_conv_set [THEN iffD1])
    3.91 +
    3.92 +lemmas in_listsD [dest!] = in_listspD [to_set]
    3.93 +
    3.94 +lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
    3.95 +by (rule in_listsp_conv_set [THEN iffD2])
    3.96 +
    3.97 +lemmas in_listsI [intro!] = in_listspI [to_set]
    3.98  
    3.99  lemma lists_UNIV [simp]: "lists UNIV = UNIV"
   3.100  by auto
   3.101 @@ -2242,13 +2273,12 @@
   3.102  
   3.103  subsubsection{* Inductive definition for membership *}
   3.104  
   3.105 -consts ListMem :: "('a \<times> 'a list)set"
   3.106 -inductive ListMem
   3.107 -intros
   3.108 - elem:  "(x,x#xs) \<in> ListMem"
   3.109 - insert:  "(x,xs) \<in> ListMem \<Longrightarrow> (x,y#xs) \<in> ListMem"
   3.110 -
   3.111 -lemma ListMem_iff: "((x,xs) \<in> ListMem) = (x \<in> set xs)"
   3.112 +inductive2 ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
   3.113 +where
   3.114 +    elem:  "ListMem x (x # xs)"
   3.115 +  | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
   3.116 +
   3.117 +lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
   3.118  apply (rule iffI)
   3.119   apply (induct set: ListMem)
   3.120    apply auto
   3.121 @@ -2495,60 +2525,73 @@
   3.122  
   3.123  subsubsection{*Lifting a Relation on List Elements to the Lists*}
   3.124  
   3.125 -consts  listrel :: "('a * 'a)set => ('a list * 'a list)set"
   3.126 -
   3.127 -inductive "listrel(r)"
   3.128 - intros
   3.129 -   Nil:  "([],[]) \<in> listrel r"
   3.130 -   Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
   3.131 -
   3.132 -inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
   3.133 -inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
   3.134 -inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
   3.135 -inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
   3.136 +inductive2
   3.137 +  list_all2' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"
   3.138 +  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   3.139 +where
   3.140 +    Nil:  "list_all2' r [] []"
   3.141 +  | Cons: "[| r x y; list_all2' r xs ys |] ==> list_all2' r (x#xs) (y#ys)"
   3.142 +
   3.143 +constdefs
   3.144 +  listrel :: "('a * 'b) set => ('a list * 'b list) set"
   3.145 +  "listrel r == Collect2 (list_all2' (member2 r))"
   3.146 +
   3.147 +lemma list_all2_listrel_eq [pred_set_conv]:
   3.148 +  "list_all2' (member2 r) = member2 (listrel r)"
   3.149 +  by (simp add: listrel_def)
   3.150 +
   3.151 +lemmas listrel_induct [consumes 1, case_names Nil Cons, induct set: listrel] =
   3.152 +  list_all2'.induct [to_set]
   3.153 +
   3.154 +lemmas listrel_intros = list_all2'.intros [to_set]
   3.155 +
   3.156 +inductive_cases2 listrel_Nil1 [to_set, elim!]: "list_all2' r [] xs"
   3.157 +inductive_cases2 listrel_Nil2 [to_set, elim!]: "list_all2' r xs []"
   3.158 +inductive_cases2 listrel_Cons1 [to_set, elim!]: "list_all2' r  (y#ys) xs"
   3.159 +inductive_cases2 listrel_Cons2 [to_set, elim!]: "list_all2' r xs (y#ys)"
   3.160  
   3.161  
   3.162  lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
   3.163  apply clarify  
   3.164 -apply (erule listrel.induct)
   3.165 -apply (blast intro: listrel.intros)+
   3.166 +apply (erule listrel_induct)
   3.167 +apply (blast intro: listrel_intros)+
   3.168  done
   3.169  
   3.170  lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
   3.171  apply clarify 
   3.172 -apply (erule listrel.induct, auto) 
   3.173 +apply (erule listrel_induct, auto) 
   3.174  done
   3.175  
   3.176  lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)" 
   3.177  apply (simp add: refl_def listrel_subset Ball_def)
   3.178  apply (rule allI) 
   3.179  apply (induct_tac x) 
   3.180 -apply (auto intro: listrel.intros)
   3.181 +apply (auto intro: listrel_intros)
   3.182  done
   3.183  
   3.184  lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
   3.185  apply (auto simp add: sym_def)
   3.186 -apply (erule listrel.induct) 
   3.187 -apply (blast intro: listrel.intros)+
   3.188 +apply (erule listrel_induct) 
   3.189 +apply (blast intro: listrel_intros)+
   3.190  done
   3.191  
   3.192  lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
   3.193  apply (simp add: trans_def)
   3.194  apply (intro allI) 
   3.195  apply (rule impI) 
   3.196 -apply (erule listrel.induct) 
   3.197 -apply (blast intro: listrel.intros)+
   3.198 +apply (erule listrel_induct) 
   3.199 +apply (blast intro: listrel_intros)+
   3.200  done
   3.201  
   3.202  theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
   3.203  by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) 
   3.204  
   3.205  lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
   3.206 -by (blast intro: listrel.intros)
   3.207 +by (blast intro: listrel_intros)
   3.208  
   3.209  lemma listrel_Cons:
   3.210       "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
   3.211 -by (auto simp add: set_Cons_def intro: listrel.intros) 
   3.212 +by (auto simp add: set_Cons_def intro: listrel_intros) 
   3.213  
   3.214  
   3.215  subsection{*Miscellany*}
     4.1 --- a/src/HOL/Nat.thy	Wed Feb 07 17:26:49 2007 +0100
     4.2 +++ b/src/HOL/Nat.thy	Wed Feb 07 17:28:09 2007 +0100
     4.3 @@ -30,20 +30,18 @@
     4.4  
     4.5  text {* Type definition *}
     4.6  
     4.7 -consts
     4.8 -  Nat :: "ind set"
     4.9 -
    4.10 -inductive Nat
    4.11 -intros
    4.12 -  Zero_RepI: "Zero_Rep : Nat"
    4.13 -  Suc_RepI: "i : Nat ==> Suc_Rep i : Nat"
    4.14 +inductive2 Nat :: "ind \<Rightarrow> bool"
    4.15 +where
    4.16 +    Zero_RepI: "Nat Zero_Rep"
    4.17 +  | Suc_RepI: "Nat i ==> Nat (Suc_Rep i)"
    4.18  
    4.19  global
    4.20  
    4.21  typedef (open Nat)
    4.22 -  nat = Nat
    4.23 +  nat = "Collect Nat"
    4.24  proof
    4.25 -  show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
    4.26 +  from Nat.Zero_RepI
    4.27 +  show "Zero_Rep : Collect Nat" ..
    4.28  qed
    4.29  
    4.30  text {* Abstract constants and syntax *}
    4.31 @@ -61,22 +59,25 @@
    4.32  instance nat :: "{ord, zero, one}"
    4.33    Zero_nat_def: "0 == Abs_Nat Zero_Rep"
    4.34    One_nat_def [simp]: "1 == Suc 0"
    4.35 -  less_def: "m < n == (m, n) : trancl pred_nat"
    4.36 +  less_def: "m < n == (m, n) : pred_nat^+"
    4.37    le_def: "m \<le> (n::nat) == ~ (n < m)" ..
    4.38  
    4.39  text {* Induction *}
    4.40  
    4.41 +lemmas Rep_Nat' = Rep_Nat [simplified mem_Collect_eq]
    4.42 +lemmas Abs_Nat_inverse' = Abs_Nat_inverse [simplified mem_Collect_eq]
    4.43 +
    4.44  theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
    4.45    apply (unfold Zero_nat_def Suc_def)
    4.46    apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    4.47 -  apply (erule Rep_Nat [THEN Nat.induct])
    4.48 -  apply (iprover elim: Abs_Nat_inverse [THEN subst])
    4.49 +  apply (erule Rep_Nat' [THEN Nat.induct])
    4.50 +  apply (iprover elim: Abs_Nat_inverse' [THEN subst])
    4.51    done
    4.52  
    4.53  text {* Distinctness of constructors *}
    4.54  
    4.55  lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
    4.56 -  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI
    4.57 +  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat' Suc_RepI Zero_RepI
    4.58                  Suc_Rep_not_Zero_Rep) 
    4.59  
    4.60  lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
    4.61 @@ -91,7 +92,7 @@
    4.62  text {* Injectiveness of @{term Suc} *}
    4.63  
    4.64  lemma inj_Suc[simp]: "inj_on Suc N"
    4.65 -  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI 
    4.66 +  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat' Suc_RepI 
    4.67                  inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) 
    4.68  
    4.69  lemma Suc_inject: "Suc x = Suc y ==> x = y"
     5.1 --- a/src/HOL/Transitive_Closure.thy	Wed Feb 07 17:26:49 2007 +0100
     5.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Feb 07 17:28:09 2007 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  header {* Reflexive and Transitive closure of a relation *}
     5.5  
     5.6  theory Transitive_Closure
     5.7 -imports Inductive
     5.8 +imports Predicate
     5.9  uses "~~/src/Provers/trancl.ML"
    5.10  begin
    5.11  
    5.12 @@ -20,56 +20,85 @@
    5.13    operands to be atomic.
    5.14  *}
    5.15  
    5.16 -consts
    5.17 -  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^*)" [1000] 999)
    5.18 -
    5.19 -inductive "r^*"
    5.20 -  intros
    5.21 -    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*"
    5.22 -    rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
    5.23 +inductive2
    5.24 +  rtrancl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"   ("(_^**)" [1000] 1000)
    5.25 +  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    5.26 +where
    5.27 +    rtrancl_refl [intro!, Pure.intro!, simp]: "r^** a a"
    5.28 +  | rtrancl_into_rtrancl [Pure.intro]: "r^** a b ==> r b c ==> r^** a c"
    5.29  
    5.30 -consts
    5.31 -  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    5.32 +inductive2
    5.33 +  trancl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(_^++)" [1000] 1000)
    5.34 +  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    5.35 +where
    5.36 +    r_into_trancl [intro, Pure.intro]: "r a b ==> r^++ a b"
    5.37 +  | trancl_into_trancl [Pure.intro]: "r^++ a b ==> r b c ==> r^++ a c"
    5.38  
    5.39 -inductive "r^+"
    5.40 -  intros
    5.41 -    r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
    5.42 -    trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+"
    5.43 +constdefs
    5.44 +  rtrancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^*)" [1000] 999)
    5.45 +  "r^* == Collect2 (member2 r)^**"
    5.46 +
    5.47 +  trancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    5.48 +  "r^+ == Collect2 (member2 r)^++"
    5.49  
    5.50  abbreviation
    5.51 -  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
    5.52 +  reflcl :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
    5.53 +  "r^== == join r op ="
    5.54 +
    5.55 +abbreviation
    5.56 +  reflcl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
    5.57    "r^= == r \<union> Id"
    5.58  
    5.59  notation (xsymbols)
    5.60 -  rtrancl  ("(_\<^sup>*)" [1000] 999) and
    5.61 -  trancl  ("(_\<^sup>+)" [1000] 999) and
    5.62 -  reflcl  ("(_\<^sup>=)" [1000] 999)
    5.63 +  rtrancl  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
    5.64 +  trancl  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
    5.65 +  reflcl  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
    5.66 +  rtrancl_set  ("(_\<^sup>*)" [1000] 999) and
    5.67 +  trancl_set  ("(_\<^sup>+)" [1000] 999) and
    5.68 +  reflcl_set  ("(_\<^sup>=)" [1000] 999)
    5.69  
    5.70  notation (HTML output)
    5.71 -  rtrancl  ("(_\<^sup>*)" [1000] 999) and
    5.72 -  trancl  ("(_\<^sup>+)" [1000] 999) and
    5.73 -  reflcl  ("(_\<^sup>=)" [1000] 999)
    5.74 +  rtrancl  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
    5.75 +  trancl  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
    5.76 +  reflcl  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
    5.77 +  rtrancl_set  ("(_\<^sup>*)" [1000] 999) and
    5.78 +  trancl_set  ("(_\<^sup>+)" [1000] 999) and
    5.79 +  reflcl_set  ("(_\<^sup>=)" [1000] 999)
    5.80  
    5.81  
    5.82  subsection {* Reflexive-transitive closure *}
    5.83  
    5.84 +lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)"
    5.85 +  by (simp add: rtrancl_set_def)
    5.86 +
    5.87 +lemma reflcl_set_eq [pred_set_conv]: "(join (member2 r) op =) = member2 (r Un Id)"
    5.88 +  by (simp add: expand_fun_eq)
    5.89 +
    5.90 +lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set]
    5.91 +lemmas rtrancl_into_rtrancl [Pure.intro] = rtrancl_into_rtrancl [to_set]
    5.92 +
    5.93  lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
    5.94    -- {* @{text rtrancl} of @{text r} contains @{text r} *}
    5.95    apply (simp only: split_tupled_all)
    5.96    apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])
    5.97    done
    5.98  
    5.99 -lemma rtrancl_mono: "r \<subseteq> s ==> r^* \<subseteq> s^*"
   5.100 +lemma r_into_rtrancl' [intro]: "r x y ==> r^** x y"
   5.101 +  -- {* @{text rtrancl} of @{text r} contains @{text r} *}
   5.102 +  by (erule rtrancl.rtrancl_refl [THEN rtrancl.rtrancl_into_rtrancl])
   5.103 +
   5.104 +lemma rtrancl_mono': "r \<le> s ==> r^** \<le> s^**"
   5.105    -- {* monotonicity of @{text rtrancl} *}
   5.106 -  apply (rule subsetI)
   5.107 -  apply (simp only: split_tupled_all)
   5.108 +  apply (rule predicate2I)
   5.109    apply (erule rtrancl.induct)
   5.110 -   apply (rule_tac [2] rtrancl_into_rtrancl, blast+)
   5.111 +   apply (rule_tac [2] rtrancl.rtrancl_into_rtrancl, blast+)
   5.112    done
   5.113  
   5.114 -theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
   5.115 -  assumes a: "(a, b) : r^*"
   5.116 -    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z"
   5.117 +lemmas rtrancl_mono = rtrancl_mono' [to_set]
   5.118 +
   5.119 +theorem rtrancl_induct' [consumes 1, induct set: rtrancl]:
   5.120 +  assumes a: "r^** a b"
   5.121 +    and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z"
   5.122    shows "P b"
   5.123  proof -
   5.124    from a have "a = a --> P b"
   5.125 @@ -77,6 +106,12 @@
   5.126    thus ?thesis by iprover
   5.127  qed
   5.128  
   5.129 +lemmas rtrancl_induct [consumes 1, induct set: rtrancl_set] = rtrancl_induct' [to_set]
   5.130 +
   5.131 +lemmas rtrancl_induct2' =
   5.132 +  rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule,
   5.133 +                 consumes 1, case_names refl step]
   5.134 +
   5.135  lemmas rtrancl_induct2 =
   5.136    rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
   5.137                   consumes 1, case_names refl step]
   5.138 @@ -95,6 +130,12 @@
   5.139  
   5.140  lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
   5.141  
   5.142 +lemma rtrancl_trans':
   5.143 +  assumes xy: "r^** x y"
   5.144 +  and yz: "r^** y z"
   5.145 +  shows "r^** x z" using yz xy
   5.146 +  by induct iprover+
   5.147 +
   5.148  lemma rtranclE:
   5.149    assumes major: "(a::'a,b) : r^*"
   5.150      and cases: "(a = b) ==> P"
   5.151 @@ -114,21 +155,25 @@
   5.152    apply (erule rtrancl_induct, auto) 
   5.153    done
   5.154  
   5.155 -lemma converse_rtrancl_into_rtrancl:
   5.156 -  "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
   5.157 -  by (rule rtrancl_trans) iprover+
   5.158 +lemma converse_rtrancl_into_rtrancl':
   5.159 +  "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c"
   5.160 +  by (rule rtrancl_trans') iprover+
   5.161 +
   5.162 +lemmas converse_rtrancl_into_rtrancl = converse_rtrancl_into_rtrancl' [to_set]
   5.163  
   5.164  text {*
   5.165    \medskip More @{term "r^*"} equations and inclusions.
   5.166  *}
   5.167  
   5.168 -lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
   5.169 -  apply auto
   5.170 -  apply (erule rtrancl_induct)
   5.171 -   apply (rule rtrancl_refl)
   5.172 -  apply (blast intro: rtrancl_trans)
   5.173 +lemma rtrancl_idemp' [simp]: "(r^**)^** = r^**"
   5.174 +  apply (auto intro!: order_antisym)
   5.175 +  apply (erule rtrancl_induct')
   5.176 +   apply (rule rtrancl.rtrancl_refl)
   5.177 +  apply (blast intro: rtrancl_trans')
   5.178    done
   5.179  
   5.180 +lemmas rtrancl_idemp [simp] = rtrancl_idemp' [to_set]
   5.181 +
   5.182  lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"
   5.183    apply (rule set_ext)
   5.184    apply (simp only: split_tupled_all)
   5.185 @@ -138,16 +183,22 @@
   5.186  lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*"
   5.187  by (drule rtrancl_mono, simp)
   5.188  
   5.189 -lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*"
   5.190 -  apply (drule rtrancl_mono)
   5.191 -  apply (drule rtrancl_mono, simp)
   5.192 +lemma rtrancl_subset': "R \<le> S ==> S \<le> R^** ==> S^** = R^**"
   5.193 +  apply (drule rtrancl_mono')
   5.194 +  apply (drule rtrancl_mono', simp)
   5.195    done
   5.196  
   5.197 -lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*"
   5.198 -  by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD])
   5.199 +lemmas rtrancl_subset = rtrancl_subset' [to_set]
   5.200 +
   5.201 +lemma rtrancl_Un_rtrancl': "(join (R^**) (S^**))^** = (join R S)^**"
   5.202 +  by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D])
   5.203  
   5.204 -lemma rtrancl_reflcl [simp]: "(R^=)^* = R^*"
   5.205 -  by (blast intro!: rtrancl_subset intro: r_into_rtrancl)
   5.206 +lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set]
   5.207 +
   5.208 +lemma rtrancl_reflcl' [simp]: "(R^==)^** = R^**"
   5.209 +  by (blast intro!: rtrancl_subset')
   5.210 +
   5.211 +lemmas rtrancl_reflcl [simp] = rtrancl_reflcl' [to_set]
   5.212  
   5.213  lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"
   5.214    apply (rule sym)
   5.215 @@ -157,58 +208,75 @@
   5.216    apply (blast intro!: r_into_rtrancl)
   5.217    done
   5.218  
   5.219 -theorem rtrancl_converseD:
   5.220 -  assumes r: "(x, y) \<in> (r^-1)^*"
   5.221 -  shows "(y, x) \<in> r^*"
   5.222 +lemma rtrancl_r_diff_Id': "(meet r op ~=)^** = r^**"
   5.223 +  apply (rule sym)
   5.224 +  apply (rule rtrancl_subset')
   5.225 +  apply blast+
   5.226 +  done
   5.227 +
   5.228 +theorem rtrancl_converseD':
   5.229 +  assumes r: "(r^--1)^** x y"
   5.230 +  shows "r^** y x"
   5.231  proof -
   5.232    from r show ?thesis
   5.233 -    by induct (iprover intro: rtrancl_trans dest!: converseD)+
   5.234 +    by induct (iprover intro: rtrancl_trans' dest!: conversepD)+
   5.235  qed
   5.236  
   5.237 -theorem rtrancl_converseI:
   5.238 -  assumes r: "(y, x) \<in> r^*"
   5.239 -  shows "(x, y) \<in> (r^-1)^*"
   5.240 +lemmas rtrancl_converseD = rtrancl_converseD' [to_set]
   5.241 +
   5.242 +theorem rtrancl_converseI':
   5.243 +  assumes r: "r^** y x"
   5.244 +  shows "(r^--1)^** x y"
   5.245  proof -
   5.246    from r show ?thesis
   5.247 -    by induct (iprover intro: rtrancl_trans converseI)+
   5.248 +    by induct (iprover intro: rtrancl_trans' conversepI)+
   5.249  qed
   5.250  
   5.251 +lemmas rtrancl_converseI = rtrancl_converseI' [to_set]
   5.252 +
   5.253  lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   5.254    by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
   5.255  
   5.256  lemma sym_rtrancl: "sym r ==> sym (r^*)"
   5.257    by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])
   5.258  
   5.259 -theorem converse_rtrancl_induct[consumes 1]:
   5.260 -  assumes major: "(a, b) : r^*"
   5.261 -    and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
   5.262 +theorem converse_rtrancl_induct'[consumes 1]:
   5.263 +  assumes major: "r^** a b"
   5.264 +    and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y"
   5.265    shows "P a"
   5.266  proof -
   5.267 -  from rtrancl_converseI [OF major]
   5.268 +  from rtrancl_converseI' [OF major]
   5.269    show ?thesis
   5.270 -    by induct (iprover intro: cases dest!: converseD rtrancl_converseD)+
   5.271 +    by induct (iprover intro: cases dest!: conversepD rtrancl_converseD')+
   5.272  qed
   5.273  
   5.274 +lemmas converse_rtrancl_induct[consumes 1] = converse_rtrancl_induct' [to_set]
   5.275 +
   5.276 +lemmas converse_rtrancl_induct2' =
   5.277 +  converse_rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule,
   5.278 +                 consumes 1, case_names refl step]
   5.279 +
   5.280  lemmas converse_rtrancl_induct2 =
   5.281    converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
   5.282                   consumes 1, case_names refl step]
   5.283  
   5.284 -lemma converse_rtranclE:
   5.285 -  assumes major: "(x,z):r^*"
   5.286 +lemma converse_rtranclE':
   5.287 +  assumes major: "r^** x z"
   5.288      and cases: "x=z ==> P"
   5.289 -      "!!y. [| (x,y):r; (y,z):r^* |] ==> P"
   5.290 +      "!!y. [| r x y; r^** y z |] ==> P"
   5.291    shows P
   5.292 -  apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
   5.293 -   apply (rule_tac [2] major [THEN converse_rtrancl_induct])
   5.294 +  apply (subgoal_tac "x = z | (EX y. r x y & r^** y z)")
   5.295 +   apply (rule_tac [2] major [THEN converse_rtrancl_induct'])
   5.296      prefer 2 apply iprover
   5.297     prefer 2 apply iprover
   5.298    apply (erule asm_rl exE disjE conjE cases)+
   5.299    done
   5.300  
   5.301 -ML_setup {*
   5.302 -  bind_thm ("converse_rtranclE2", split_rule
   5.303 -    (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] (thm "converse_rtranclE")));
   5.304 -*}
   5.305 +lemmas converse_rtranclE = converse_rtranclE' [to_set]
   5.306 +
   5.307 +lemmas converse_rtranclE2' = converse_rtranclE' [of _ "(xa,xb)" "(za,zb)", split_rule]
   5.308 +
   5.309 +lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule]
   5.310  
   5.311  lemma r_comp_rtrancl_eq: "r O r^* = r^* O r"
   5.312    by (blast elim: rtranclE converse_rtranclE
   5.313 @@ -220,8 +288,14 @@
   5.314  
   5.315  subsection {* Transitive closure *}
   5.316  
   5.317 +lemma trancl_set_eq [pred_set_conv]: "(member2 r)^++ = member2 (r^+)"
   5.318 +  by (simp add: trancl_set_def)
   5.319 +
   5.320 +lemmas r_into_trancl [intro, Pure.intro] = r_into_trancl [to_set]
   5.321 +lemmas trancl_into_trancl [Pure.intro] = trancl_into_trancl [to_set]
   5.322 +
   5.323  lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
   5.324 -  apply (simp only: split_tupled_all)
   5.325 +  apply (simp add: split_tupled_all trancl_set_def)
   5.326    apply (erule trancl.induct)
   5.327    apply (iprover dest: subsetD)+
   5.328    done
   5.329 @@ -233,24 +307,30 @@
   5.330    \medskip Conversions between @{text trancl} and @{text rtrancl}.
   5.331  *}
   5.332  
   5.333 -lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*"
   5.334 +lemma trancl_into_rtrancl': "r^++ a b ==> r^** a b"
   5.335    by (erule trancl.induct) iprover+
   5.336  
   5.337 -lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*"
   5.338 -  shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r
   5.339 +lemmas trancl_into_rtrancl = trancl_into_rtrancl' [to_set]
   5.340 +
   5.341 +lemma rtrancl_into_trancl1': assumes r: "r^** a b"
   5.342 +  shows "!!c. r b c ==> r^++ a c" using r
   5.343    by induct iprover+
   5.344  
   5.345 -lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
   5.346 +lemmas rtrancl_into_trancl1 = rtrancl_into_trancl1' [to_set]
   5.347 +
   5.348 +lemma rtrancl_into_trancl2': "[| r a b; r^** b c |] ==> r^++ a c"
   5.349    -- {* intro rule from @{text r} and @{text rtrancl} *}
   5.350 -  apply (erule rtranclE, iprover)
   5.351 -  apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
   5.352 -   apply (assumption | rule r_into_rtrancl)+
   5.353 +  apply (erule rtrancl.cases, iprover)
   5.354 +  apply (rule rtrancl_trans' [THEN rtrancl_into_trancl1'])
   5.355 +   apply (simp | rule r_into_rtrancl')+
   5.356    done
   5.357  
   5.358 -lemma trancl_induct [consumes 1, induct set: trancl]:
   5.359 -  assumes a: "(a,b) : r^+"
   5.360 -  and cases: "!!y. (a, y) : r ==> P y"
   5.361 -    "!!y z. (a,y) : r^+ ==> (y, z) : r ==> P y ==> P z"
   5.362 +lemmas rtrancl_into_trancl2 = rtrancl_into_trancl2' [to_set]
   5.363 +
   5.364 +lemma trancl_induct' [consumes 1, induct set: trancl]:
   5.365 +  assumes a: "r^++ a b"
   5.366 +  and cases: "!!y. r a y ==> P y"
   5.367 +    "!!y z. r^++ a y ==> r y z ==> P y ==> P z"
   5.368    shows "P b"
   5.369    -- {* Nice induction rule for @{text trancl} *}
   5.370  proof -
   5.371 @@ -259,19 +339,32 @@
   5.372    thus ?thesis by iprover
   5.373  qed
   5.374  
   5.375 +lemmas trancl_induct [consumes 1, induct set: trancl_set] = trancl_induct' [to_set]
   5.376 +
   5.377 +lemmas trancl_induct2' =
   5.378 +  trancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule,
   5.379 +                 consumes 1, case_names base step]
   5.380 +
   5.381  lemmas trancl_induct2 =
   5.382    trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
   5.383                   consumes 1, case_names base step]
   5.384  
   5.385 -lemma trancl_trans_induct:
   5.386 -  assumes major: "(x,y) : r^+"
   5.387 -    and cases: "!!x y. (x,y) : r ==> P x y"
   5.388 -      "!!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z"
   5.389 +lemma trancl_trans_induct':
   5.390 +  assumes major: "r^++ x y"
   5.391 +    and cases: "!!x y. r x y ==> P x y"
   5.392 +      "!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z"
   5.393    shows "P x y"
   5.394    -- {* Another induction rule for trancl, incorporating transitivity *}
   5.395 -  by (iprover intro: r_into_trancl major [THEN trancl_induct] cases)
   5.396 +  by (iprover intro: major [THEN trancl_induct'] cases)
   5.397 +
   5.398 +lemmas trancl_trans_induct = trancl_trans_induct' [to_set]
   5.399  
   5.400 -inductive_cases tranclE: "(a, b) : r^+"
   5.401 +lemma tranclE:
   5.402 +  assumes H: "(a, b) : r^+"
   5.403 +  and cases: "(a, b) : r ==> P" "\<And>c. (a, c) : r^+ ==> (c, b) : r ==> P"
   5.404 +  shows P
   5.405 +  using H [simplified trancl_set_def, simplified]
   5.406 +  by cases (auto intro: cases [simplified trancl_set_def, simplified])
   5.407  
   5.408  lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
   5.409    apply (rule subsetI)
   5.410 @@ -293,6 +386,12 @@
   5.411  
   5.412  lemmas trancl_trans = trans_trancl [THEN transD, standard]
   5.413  
   5.414 +lemma trancl_trans':
   5.415 +  assumes xy: "r^++ x y"
   5.416 +  and yz: "r^++ y z"
   5.417 +  shows "r^++ x z" using yz xy
   5.418 +  by induct iprover+
   5.419 +
   5.420  lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r"
   5.421  apply(auto)
   5.422  apply(erule trancl_induct)
   5.423 @@ -301,12 +400,16 @@
   5.424  apply(blast)
   5.425  done
   5.426  
   5.427 -lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
   5.428 -  shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
   5.429 -  by induct (iprover intro: trancl_trans)+
   5.430 +lemma rtrancl_trancl_trancl': assumes r: "r^** x y"
   5.431 +  shows "!!z. r^++ y z ==> r^++ x z" using r
   5.432 +  by induct (iprover intro: trancl_trans')+
   5.433  
   5.434 -lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
   5.435 -  by (erule transD [OF trans_trancl r_into_trancl])
   5.436 +lemmas rtrancl_trancl_trancl = rtrancl_trancl_trancl' [to_set]
   5.437 +
   5.438 +lemma trancl_into_trancl2': "r a b ==> r^++ b c ==> r^++ a c"
   5.439 +  by (erule trancl_trans' [OF trancl.r_into_trancl])
   5.440 +
   5.441 +lemmas trancl_into_trancl2 = trancl_into_trancl2' [to_set]
   5.442  
   5.443  lemma trancl_insert:
   5.444    "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"
   5.445 @@ -321,41 +424,51 @@
   5.446      [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   5.447    done
   5.448  
   5.449 -lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+"
   5.450 -  apply (drule converseD)
   5.451 -  apply (erule trancl.induct)
   5.452 -  apply (iprover intro: converseI trancl_trans)+
   5.453 +lemma trancl_converseI': "(r^++)^--1 x y ==> (r^--1)^++ x y"
   5.454 +  apply (drule conversepD)
   5.455 +  apply (erule trancl_induct')
   5.456 +  apply (iprover intro: conversepI trancl_trans')+
   5.457    done
   5.458  
   5.459 -lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   5.460 -  apply (rule converseI)
   5.461 -  apply (erule trancl.induct)
   5.462 -  apply (iprover dest: converseD intro: trancl_trans)+
   5.463 +lemmas trancl_converseI = trancl_converseI' [to_set]
   5.464 +
   5.465 +lemma trancl_converseD': "(r^--1)^++ x y ==> (r^++)^--1 x y"
   5.466 +  apply (rule conversepI)
   5.467 +  apply (erule trancl_induct')
   5.468 +  apply (iprover dest: conversepD intro: trancl_trans')+
   5.469    done
   5.470  
   5.471 -lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
   5.472 -  by (fastsimp simp add: split_tupled_all
   5.473 -    intro!: trancl_converseI trancl_converseD)
   5.474 +lemmas trancl_converseD = trancl_converseD' [to_set]
   5.475 +
   5.476 +lemma trancl_converse': "(r^--1)^++ = (r^++)^--1"
   5.477 +  by (fastsimp simp add: expand_fun_eq
   5.478 +    intro!: trancl_converseI' dest!: trancl_converseD')
   5.479 +
   5.480 +lemmas trancl_converse = trancl_converse' [to_set]
   5.481  
   5.482  lemma sym_trancl: "sym r ==> sym (r^+)"
   5.483    by (simp only: sym_conv_converse_eq trancl_converse [symmetric])
   5.484  
   5.485 -lemma converse_trancl_induct:
   5.486 -  assumes major: "(a,b) : r^+"
   5.487 -    and cases: "!!y. (y,b) : r ==> P(y)"
   5.488 -      "!!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y)"
   5.489 +lemma converse_trancl_induct':
   5.490 +  assumes major: "r^++ a b"
   5.491 +    and cases: "!!y. r y b ==> P(y)"
   5.492 +      "!!y z.[| r y z;  r^++ z b;  P(z) |] ==> P(y)"
   5.493    shows "P a"
   5.494 -  apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
   5.495 +  apply (rule trancl_induct' [OF trancl_converseI', OF conversepI, OF major])
   5.496     apply (rule cases)
   5.497 -   apply (erule converseD)
   5.498 -  apply (blast intro: prems dest!: trancl_converseD)
   5.499 +   apply (erule conversepD)
   5.500 +  apply (blast intro: prems dest!: trancl_converseD' conversepD)
   5.501    done
   5.502  
   5.503 -lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
   5.504 -  apply (erule converse_trancl_induct, auto)
   5.505 -  apply (blast intro: rtrancl_trans)
   5.506 +lemmas converse_trancl_induct = converse_trancl_induct' [to_set]
   5.507 +
   5.508 +lemma tranclD': "R^++ x y ==> EX z. R x z \<and> R^** z y"
   5.509 +  apply (erule converse_trancl_induct', auto)
   5.510 +  apply (blast intro: rtrancl_trans')
   5.511    done
   5.512  
   5.513 +lemmas tranclD = tranclD' [to_set]
   5.514 +
   5.515  lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
   5.516    by (blast elim: tranclE dest: trancl_into_rtrancl)
   5.517  
   5.518 @@ -373,12 +486,14 @@
   5.519    apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+
   5.520    done
   5.521  
   5.522 -lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
   5.523 -  apply safe
   5.524 -   apply (erule trancl_into_rtrancl)
   5.525 -  apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
   5.526 +lemma reflcl_trancl' [simp]: "(r^++)^== = r^**"
   5.527 +  apply (safe intro!: order_antisym)
   5.528 +   apply (erule trancl_into_rtrancl')
   5.529 +  apply (blast elim: rtrancl.cases dest: rtrancl_into_trancl1')
   5.530    done
   5.531  
   5.532 +lemmas reflcl_trancl [simp] = reflcl_trancl' [to_set]
   5.533 +
   5.534  lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
   5.535    apply safe
   5.536     apply (drule trancl_into_rtrancl, simp)
   5.537 @@ -394,8 +509,10 @@
   5.538  lemma rtrancl_empty [simp]: "{}^* = Id"
   5.539    by (rule subst [OF reflcl_trancl]) simp
   5.540  
   5.541 -lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+"
   5.542 -  by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
   5.543 +lemma rtranclD': "R^** a b ==> a = b \<or> a \<noteq> b \<and> R^++ a b"
   5.544 +  by (force simp add: reflcl_trancl' [symmetric] simp del: reflcl_trancl')
   5.545 +
   5.546 +lemmas rtranclD = rtranclD' [to_set]
   5.547  
   5.548  lemma rtrancl_eq_or_trancl:
   5.549    "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)"
   5.550 @@ -450,24 +567,32 @@
   5.551    apply (fast intro: r_r_into_trancl trancl_trans)
   5.552    done
   5.553  
   5.554 -lemma trancl_rtrancl_trancl:
   5.555 -    "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r\<^sup>* ==> (a, c) \<in> r\<^sup>+"
   5.556 -  apply (drule tranclD)
   5.557 +lemma trancl_rtrancl_trancl':
   5.558 +    "r\<^sup>+\<^sup>+ a b ==> r\<^sup>*\<^sup>* b c ==> r\<^sup>+\<^sup>+ a c"
   5.559 +  apply (drule tranclD')
   5.560    apply (erule exE, erule conjE)
   5.561 -  apply (drule rtrancl_trans, assumption)
   5.562 -  apply (drule rtrancl_into_trancl2, assumption, assumption)
   5.563 +  apply (drule rtrancl_trans', assumption)
   5.564 +  apply (drule rtrancl_into_trancl2', assumption, assumption)
   5.565    done
   5.566  
   5.567 +lemmas trancl_rtrancl_trancl = trancl_rtrancl_trancl' [to_set]
   5.568 +
   5.569  lemmas transitive_closure_trans [trans] =
   5.570    r_r_into_trancl trancl_trans rtrancl_trans
   5.571    trancl_into_trancl trancl_into_trancl2
   5.572    rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
   5.573    rtrancl_trancl_trancl trancl_rtrancl_trancl
   5.574  
   5.575 +lemmas transitive_closure_trans' [trans] =
   5.576 +  trancl_trans' rtrancl_trans'
   5.577 +  trancl.trancl_into_trancl trancl_into_trancl2'
   5.578 +  rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl'
   5.579 +  rtrancl_trancl_trancl' trancl_rtrancl_trancl'
   5.580 +
   5.581  declare trancl_into_rtrancl [elim]
   5.582  
   5.583 -declare rtranclE [cases set: rtrancl]
   5.584 -declare tranclE [cases set: trancl]
   5.585 +declare rtranclE [cases set: rtrancl_set]
   5.586 +declare tranclE [cases set: trancl_set]
   5.587  
   5.588  
   5.589  
   5.590 @@ -490,8 +615,8 @@
   5.591  
   5.592    fun decomp (Trueprop $ t) =
   5.593      let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
   5.594 -        let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
   5.595 -              | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
   5.596 +        let fun decr (Const ("Transitive_Closure.rtrancl_set", _ ) $ r) = (r,"r*")
   5.597 +              | decr (Const ("Transitive_Closure.trancl_set", _ ) $ r)  = (r,"r+")
   5.598                | decr r = (r,"r");
   5.599              val (rel,r) = decr rel;
   5.600          in SOME (a,b,rel,r) end
   5.601 @@ -500,9 +625,34 @@
   5.602  
   5.603    end);
   5.604  
   5.605 +structure Tranclp_Tac = Trancl_Tac_Fun (
   5.606 +  struct
   5.607 +    val r_into_trancl = thm "trancl.r_into_trancl";
   5.608 +    val trancl_trans  = thm "trancl_trans'";
   5.609 +    val rtrancl_refl = thm "rtrancl.rtrancl_refl";
   5.610 +    val r_into_rtrancl = thm "r_into_rtrancl'";
   5.611 +    val trancl_into_rtrancl = thm "trancl_into_rtrancl'";
   5.612 +    val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl'";
   5.613 +    val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl'";
   5.614 +    val rtrancl_trans = thm "rtrancl_trans'";
   5.615 +
   5.616 +  fun decomp (Trueprop $ t) =
   5.617 +    let fun dec (rel $ a $ b) =
   5.618 +        let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
   5.619 +              | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
   5.620 +              | decr r = (r,"r");
   5.621 +            val (rel,r) = decr rel;
   5.622 +        in SOME (a, b, Envir.beta_eta_contract rel, r) end
   5.623 +      | dec _ =  NONE
   5.624 +    in dec t end;
   5.625 +
   5.626 +  end);
   5.627 +
   5.628  change_simpset (fn ss => ss
   5.629    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
   5.630 -  addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)));
   5.631 +  addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
   5.632 +  addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
   5.633 +  addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)));
   5.634  
   5.635  *}
   5.636  
   5.637 @@ -514,5 +664,11 @@
   5.638  method_setup rtrancl =
   5.639    {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
   5.640    {* simple transitivity reasoner *}
   5.641 +method_setup tranclp =
   5.642 +  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
   5.643 +  {* simple transitivity reasoner (predicate version) *}
   5.644 +method_setup rtranclp =
   5.645 +  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
   5.646 +  {* simple transitivity reasoner (predicate version) *}
   5.647  
   5.648  end