# HG changeset patch # User berghofe # Date 1170865689 -3600 # Node ID 96ba62dff41378695ccc06cd616f1b5f5fd55f45 # Parent 9e185f78e7d42d0430ac86dc6e4eae53bce94e9e Adapted to new inductive definition package. diff -r 9e185f78e7d4 -r 96ba62dff413 src/HOL/Accessible_Part.thy --- a/src/HOL/Accessible_Part.thy Wed Feb 07 17:26:49 2007 +0100 +++ b/src/HOL/Accessible_Part.thy Wed Feb 07 17:28:09 2007 +0100 @@ -17,22 +17,22 @@ relation; see also \cite{paulin-tlca}. *} -consts - acc :: "('a \ 'a) set => 'a set" -inductive "acc r" - intros - accI: "(!!y. (y, x) \ r ==> y \ acc r) ==> x \ acc r" +inductive2 + acc :: "('a => 'a => bool) => 'a => bool" + for r :: "'a => 'a => bool" + where + accI: "(!!y. r y x ==> acc r y) ==> acc r x" abbreviation - termi :: "('a \ 'a) set => 'a set" where - "termi r == acc (r\)" + termi :: "('a => 'a => bool) => 'a => bool" where + "termi r == acc (r\\)" subsection {* Induction rules *} theorem acc_induct: - assumes major: "a \ acc r" - assumes hyp: "!!x. x \ acc r ==> \y. (y, x) \ r --> P y ==> P x" + assumes major: "acc r a" + assumes hyp: "!!x. acc r x ==> \y. r y x --> P y ==> P x" shows "P a" apply (rule major [THEN acc.induct]) apply (rule hyp) @@ -43,35 +43,55 @@ theorems acc_induct_rule = acc_induct [rule_format, induct set: acc] -theorem acc_downward: "b \ acc r ==> (a, b) \ r ==> a \ acc r" - apply (erule acc.elims) +theorem acc_downward: "acc r b ==> r a b ==> acc r a" + apply (erule acc.cases) apply fast done -lemma acc_downwards_aux: "(b, a) \ r\<^sup>* ==> a \ acc r --> b \ acc r" - apply (erule rtrancl_induct) +lemma not_acc_down: + assumes na: "\ acc R x" + obtains z where "R z x" and "\ acc R z" +proof - + assume a: "\z. \R z x; \ acc R z\ \ thesis" + + show thesis + proof (cases "\z. R z x \ acc R z") + case True + hence "\z. R z x \ acc R z" by auto + hence "acc R x" + by (rule accI) + with na show thesis .. + next + case False then obtain z where "R z x" and "\ acc R z" + by auto + with a show thesis . + qed +qed + +lemma acc_downwards_aux: "r\<^sup>*\<^sup>* b a ==> acc r a --> acc r b" + apply (erule rtrancl_induct') apply blast apply (blast dest: acc_downward) done -theorem acc_downwards: "a \ acc r ==> (b, a) \ r\<^sup>* ==> b \ acc r" +theorem acc_downwards: "acc r a ==> r\<^sup>*\<^sup>* b a ==> acc r b" apply (blast dest: acc_downwards_aux) done -theorem acc_wfI: "\x. x \ acc r ==> wf r" - apply (rule wfUNIVI) +theorem acc_wfI: "\x. acc r x ==> wfP r" + apply (rule wfPUNIVI) apply (induct_tac P x rule: acc_induct) apply blast apply blast done -theorem acc_wfD: "wf r ==> x \ acc r" - apply (erule wf_induct) +theorem acc_wfD: "wfP r ==> acc r x" + apply (erule wfP_induct_rule) apply (rule accI) apply blast done -theorem wf_acc_iff: "wf r = (\x. x \ acc r)" +theorem wf_acc_iff: "wfP r = (\x. acc r x)" apply (blast intro: acc_wfI dest: acc_wfD) done @@ -79,16 +99,16 @@ text {* Smaller relations have bigger accessible parts: *} lemma acc_subset: - assumes sub: "R1 \ R2" - shows "acc R2 \ acc R1" + assumes sub: "R1 \ R2" + shows "acc R2 \ acc R1" proof - fix x assume "x \ acc R2" - then show "x \ acc R1" + fix x assume "acc R2 x" + then show "acc R1 x" proof (induct x) fix x - assume ih: "\y. (y, x) \ R2 \ y \ acc R1" - with sub show "x \ acc R1" - by (blast intro:accI) + assume ih: "\y. R2 y x \ acc R1 y" + with sub show "acc R1 x" + by (blast intro: accI) qed qed @@ -97,19 +117,19 @@ subsets of the accessible part. *} lemma acc_subset_induct: - assumes subset: "D \ acc R" - and dcl: "\x z. \x \ D; (z, x)\R\ \ z \ D" - and "x \ D" - and istep: "\x. \x \ D; (\z. (z, x)\R \ P z)\ \ P x" + assumes subset: "D \ acc R" + and dcl: "\x z. \D x; R z x\ \ D z" + and "D x" + and istep: "\x. \D x; (\z. R z x \ P z)\ \ P x" shows "P x" proof - - from `x \ D` and subset - have "x \ acc R" .. - then show "P x" using `x \ D` + from subset and `D x` + have "acc R x" .. + then show "P x" using `D x` proof (induct x) fix x - assume "x \ D" - and "\y. (y, x) \ R \ y \ D \ P y" + assume "D x" + and "\y. R y x \ D y \ P y" with dcl and istep show "P x" by blast qed qed diff -r 9e185f78e7d4 -r 96ba62dff413 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Feb 07 17:26:49 2007 +0100 +++ b/src/HOL/Finite_Set.thy Wed Feb 07 17:28:09 2007 +0100 @@ -12,14 +12,10 @@ subsection {* Definition and basic properties *} -consts Finites :: "'a set set" -abbreviation - "finite A == A : Finites" - -inductive Finites - intros - emptyI [simp, intro!]: "{} : Finites" - insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" +inductive2 finite :: "'a set => bool" + where + emptyI [simp, intro!]: "finite {}" + | insertI [simp, intro!]: "finite A ==> finite (insert a A)" axclass finite \ type finite: "finite UNIV" @@ -32,7 +28,7 @@ thus ?thesis by blast qed -lemma finite_induct [case_names empty insert, induct set: Finites]: +lemma finite_induct [case_names empty insert, induct set: finite]: "finite F ==> P {} ==> (!!x F. finite F ==> x \ F ==> P F ==> P (insert x F)) ==> P F" -- {* Discharging @{text "x \ F"} entails extra work. *} @@ -146,7 +142,7 @@ lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)" -- {* The union of two finite sets is finite. *} - by (induct set: Finites) simp_all + by (induct set: finite) simp_all lemma finite_subset: "A \ B ==> finite B ==> finite A" -- {* Every subset of a finite set is finite. *} @@ -244,7 +240,7 @@ lemma finite_imageI[simp]: "finite F ==> finite (h ` F)" -- {* The image of a finite set is finite. *} - by (induct set: Finites) simp_all + by (induct set: finite) simp_all lemma finite_surj: "finite A ==> B <= f ` A ==> finite B" apply (frule finite_imageI) @@ -286,7 +282,7 @@ lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)" -- {* The inverse image of a finite set under an injective function is finite. *} - apply (induct set: Finites) + apply (induct set: finite) apply simp_all apply (subst vimage_insert) apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) @@ -296,7 +292,7 @@ text {* The finite UNION of finite sets *} lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)" - by (induct set: Finites) simp_all + by (induct set: finite) simp_all text {* Strengthen RHS to @@ -398,7 +394,7 @@ lemma finite_Field: "finite r ==> finite (Field r)" -- {* A finite relation has a finite field (@{text "= domain \ range"}. *} - apply (induct set: Finites) + apply (induct set: finite) apply (auto simp add: Field_def Domain_insert Range_insert) done @@ -427,38 +423,39 @@ se the definitions of sums and products over finite sets. *} -consts - foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => ('b set \ 'a) set" - -inductive "foldSet f g z" -intros -emptyI [intro]: "({}, z) : foldSet f g z" -insertI [intro]: - "\ x \ A; (A, y) : foldSet f g z \ - \ (insert x A, f (g x) y) : foldSet f g z" - -inductive_cases empty_foldSetE [elim!]: "({}, x) : foldSet f g z" +inductive2 + foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool" + for f :: "'a => 'a => 'a" + and g :: "'b => 'a" + and z :: 'a +where + emptyI [intro]: "foldSet f g z {} z" +| insertI [intro]: + "\ x \ A; foldSet f g z A y \ + \ foldSet f g z (insert x A) (f (g x) y)" + +inductive_cases2 empty_foldSetE [elim!]: "foldSet f g z {} x" constdefs fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a" - "fold f g z A == THE x. (A, x) : foldSet f g z" + "fold f g z A == THE x. foldSet f g z A x" text{*A tempting alternative for the definiens is -@{term "if finite A then THE x. (A, x) : foldSet f g e else e"}. +@{term "if finite A then THE x. foldSet f g e A x else e"}. It allows the removal of finiteness assumptions from the theorems @{text fold_commute}, @{text fold_reindex} and @{text fold_distrib}. The proofs become ugly, with @{text rule_format}. It is not worth the effort.*} lemma Diff1_foldSet: - "(A - {x}, y) : foldSet f g z ==> x: A ==> (A, f (g x) y) : foldSet f g z" + "foldSet f g z (A - {x}) y ==> x: A ==> foldSet f g z A (f (g x) y)" by (erule insert_Diff [THEN subst], rule foldSet.intros, auto) -lemma foldSet_imp_finite: "(A, x) : foldSet f g z ==> finite A" +lemma foldSet_imp_finite: "foldSet f g z A x==> finite A" by (induct set: foldSet) auto -lemma finite_imp_foldSet: "finite A ==> EX x. (A, x) : foldSet f g z" - by (induct set: Finites) auto +lemma finite_imp_foldSet: "finite A ==> EX x. foldSet f g z A x" + by (induct set: finite) auto subsubsection {* Commutative monoids *} @@ -554,33 +551,31 @@ lemma (in ACf) foldSet_determ_aux: "!!A x x' h. \ A = h`{i::nat. i + foldSet f g z A x; foldSet f g z A x' \ \ x' = x" proof (induct n rule: less_induct) case (less n) have IH: "!!m h A x x'. \m foldSet f g z; (A, x') \ foldSet f g z\ \ x' = x" . - have Afoldx: "(A,x) \ foldSet f g z" and Afoldx': "(A,x') \ foldSet f g z" + foldSet f g z A x; foldSet f g z A x'\ \ x' = x" . + have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'" and A: "A = h`{i. i u)" and notinB: "b \ B" - and Bu: "(B,u) \ foldSet f g z" - hence AbB: "A = insert b B" and x: "x = g b \ u" by auto + assume AbB: "A = insert b B" and x: "x = g b \ u" + and notinB: "b \ B" and Bu: "foldSet f g z B u" show "x'=x" proof (rule foldSet.cases [OF Afoldx']) - assume "(A, x') = ({}, z)" + assume "A = {}" and "x' = z" with AbB show "x' = x" by blast next fix C c v - assume "(A,x') = (insert c C, g c \ v)" and notinC: "c \ C" - and Cv: "(C,v) \ foldSet f g z" - hence AcC: "A = insert c C" and x': "x' = g c \ v" by auto + assume AcC: "A = insert c C" and x': "x' = g c \ v" + and notinC: "c \ C" and Cv: "foldSet f g z C v" from A AbB have Beq: "insert b B = h`{i. i foldSet f g z" + then obtain d where Dfoldd: "foldSet f g z ?D d" using finite_imp_foldSet by iprover moreover have cinB: "c \ B" using B by auto - ultimately have "(B,g c \ d) \ foldSet f g z" + ultimately have "foldSet f g z B (g c \ d)" by(rule Diff1_foldSet) hence "g c \ d = u" by (rule IH [OF lessB Beq inj_onB Bu]) moreover have "g b \ d = v" proof (rule IH[OF lessC Ceq inj_onC Cv]) - show "(C, g b \ d) \ foldSet f g z" using C notinB Dfoldd + show "foldSet f g z C (g b \ d)" using C notinB Dfoldd by fastsimp qed ultimately show ?thesis using x x' by (auto simp: AC) @@ -623,12 +618,12 @@ lemma (in ACf) foldSet_determ: - "(A,x) : foldSet f g z ==> (A,y) : foldSet f g z ==> y = x" + "foldSet f g z A x ==> foldSet f g z A y ==> y = x" apply (frule foldSet_imp_finite [THEN finite_imp_nat_seg_image_inj_on]) apply (blast intro: foldSet_determ_aux [rule_format]) done -lemma (in ACf) fold_equality: "(A, y) : foldSet f g z ==> fold f g z A = y" +lemma (in ACf) fold_equality: "foldSet f g z A y ==> fold f g z A = y" by (unfold fold_def) (blast intro: foldSet_determ) text{* The base case for @{text fold}: *} @@ -637,8 +632,8 @@ by (unfold fold_def) blast lemma (in ACf) fold_insert_aux: "x \ A ==> - ((insert x A, v) : foldSet f g z) = - (EX y. (A, y) : foldSet f g z & v = f (g x) y)" + (foldSet f g z (insert x A) v) = + (EX y. foldSet f g z A y & v = f (g x) y)" apply auto apply (rule_tac A1 = A and f1 = f in finite_imp_foldSet [THEN exE]) apply (fastsimp dest: foldSet_imp_finite) @@ -700,7 +695,7 @@ lemma (in ACf) fold_commute: "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)" - apply (induct set: Finites) + apply (induct set: finite) apply simp apply (simp add: left_commute [of x]) done @@ -708,7 +703,7 @@ lemma (in ACf) fold_nest_Un_Int: "finite A ==> finite B ==> fold f g (fold f g z B) A = fold f g (fold f g z (A Int B)) (A Un B)" - apply (induct set: Finites) + apply (induct set: finite) apply simp apply (simp add: fold_commute Int_insert_left insert_absorb) done @@ -730,7 +725,7 @@ "finite A ==> finite B ==> fold f g e A \ fold f g e B = fold f g e (A Un B) \ fold f g e (A Int B)" - apply (induct set: Finites, simp) + apply (induct set: finite, simp) apply (simp add: AC insert_absorb Int_insert_left) done @@ -744,7 +739,7 @@ ALL i:I. ALL j:I. i \ j --> A i Int A j = {} \ \ fold f g e (UNION I A) = fold f (%i. fold f g e (A i)) e I" - apply (induct set: Finites, simp, atomize) + apply (induct set: finite, simp, atomize) apply (subgoal_tac "ALL i:F. x \ i") prefer 2 apply blast apply (subgoal_tac "A x Int UNION F A = {}") @@ -762,7 +757,7 @@ "finite A ==> (!!x y. h (g x y) = f x (h y)) ==> h (fold g j w A) = fold f j (h w) A" - by (induct set: Finites) simp_all + by (induct set: finite) simp_all lemma (in ACf) fold_cong: "finite A \ (!!x. x:A ==> g x = h x) ==> fold f g z A = fold f h z A" @@ -954,7 +949,7 @@ lemma setsum_eq_0_iff [simp]: "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" - by (induct set: Finites) auto + by (induct set: finite) auto lemma setsum_Un_nat: "finite A ==> finite B ==> (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" @@ -1064,7 +1059,7 @@ lemma setsum_negf: "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A" proof (cases "finite A") - case True thus ?thesis by (induct set: Finites) auto + case True thus ?thesis by (induct set: finite) auto next case False thus ?thesis by (simp add: setsum_def) qed @@ -1398,18 +1393,18 @@ lemma setprod_eq_1_iff [simp]: "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" - by (induct set: Finites) auto + by (induct set: finite) auto lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" - apply (induct set: Finites, force, clarsimp) + apply (induct set: finite, force, clarsimp) apply (erule disjE, auto) done lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_idom) \ f x) --> 0 \ setprod f A" apply (case_tac "finite A") - apply (induct set: Finites, force, clarsimp) + apply (induct set: finite, force, clarsimp) apply (subgoal_tac "0 * 0 \ f x * setprod f F", force) apply (rule mult_mono, assumption+) apply (auto simp add: setprod_def) @@ -1418,7 +1413,7 @@ lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) --> 0 < setprod f A" apply (case_tac "finite A") - apply (induct set: Finites, force, clarsimp) + apply (induct set: finite, force, clarsimp) apply (subgoal_tac "0 * 0 < f x * setprod f F", force) apply (rule mult_strict_mono, assumption+) apply (auto simp add: setprod_def) @@ -1546,7 +1541,7 @@ by (simp add: card_def setsum_mono2) lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)" - apply (induct set: Finites, simp, clarify) + apply (induct set: finite, simp, clarify) apply (subgoal_tac "finite A & A - {x} <= F") prefer 2 apply (blast intro: finite_subset, atomize) apply (drule_tac x = "A - {x}" in spec) @@ -1698,7 +1693,7 @@ done lemma card_image_le: "finite A ==> card (f ` A) <= card A" - apply (induct set: Finites) + apply (induct set: finite) apply simp apply (simp add: le_SucI finite_imageI card_insert_if) done @@ -1763,7 +1758,7 @@ subsubsection {* Cardinality of the Powerset *} lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *) - apply (induct set: Finites) + apply (induct set: finite) apply (simp_all add: Pow_insert) apply (subst card_Un_disjoint, blast) apply (blast intro: finite_imageI, blast) @@ -1783,7 +1778,7 @@ k dvd card (Union C)" apply(frule finite_UnionD) apply(rotate_tac -1) - apply (induct set: Finites, simp_all, clarify) + apply (induct set: finite, simp_all, clarify) apply (subst card_Un_disjoint) apply (auto simp add: dvd_add disjoint_eq_subset_Compl) done @@ -1793,36 +1788,35 @@ text{* Does not require start value. *} -consts - fold1Set :: "('a => 'a => 'a) => ('a set \ 'a) set" - -inductive "fold1Set f" -intros +inductive2 + fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool" + for f :: "'a => 'a => 'a" +where fold1Set_insertI [intro]: - "\ (A,x) \ foldSet f id a; a \ A \ \ (insert a A, x) \ fold1Set f" + "\ foldSet f id a A x; a \ A \ \ fold1Set f (insert a A) x" constdefs fold1 :: "('a => 'a => 'a) => 'a set => 'a" - "fold1 f A == THE x. (A, x) : fold1Set f" + "fold1 f A == THE x. fold1Set f A x" lemma fold1Set_nonempty: - "(A, x) : fold1Set f \ A \ {}" + "fold1Set f A x \ A \ {}" by(erule fold1Set.cases, simp_all) -inductive_cases empty_fold1SetE [elim!]: "({}, x) : fold1Set f" - -inductive_cases insert_fold1SetE [elim!]: "(insert a X, x) : fold1Set f" - - -lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)" +inductive_cases2 empty_fold1SetE [elim!]: "fold1Set f {} x" + +inductive_cases2 insert_fold1SetE [elim!]: "fold1Set f (insert a X) x" + + +lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)" by (blast intro: foldSet.intros elim: foldSet.cases) lemma fold1_singleton[simp]: "fold1 f {a} = a" by (unfold fold1_def) blast lemma finite_nonempty_imp_fold1Set: - "\ finite A; A \ {} \ \ EX x. (A, x) : fold1Set f" + "\ finite A; A \ {} \ \ EX x. fold1Set f A x" apply (induct A rule: finite_induct) apply (auto dest: finite_imp_foldSet [of _ f id]) done @@ -1830,26 +1824,26 @@ text{*First, some lemmas about @{term foldSet}.*} lemma (in ACf) foldSet_insert_swap: -assumes fold: "(A,y) \ foldSet f id b" -shows "b \ A \ (insert b A, z \ y) \ foldSet f id z" +assumes fold: "foldSet f id b A y" +shows "b \ A \ foldSet f id z (insert b A) (z \ y)" using fold proof (induct rule: foldSet.induct) case emptyI thus ?case by (force simp add: fold_insert_aux commute) next - case (insertI A x y) - have "(insert x (insert b A), x \ (z \ y)) \ foldSet f (\u. u) z" + case (insertI x A y) + have "foldSet f (\u. u) z (insert x (insert b A)) (x \ (z \ y))" using insertI by force --{*how does @{term id} get unfolded?*} thus ?case by (simp add: insert_commute AC) qed lemma (in ACf) foldSet_permute_diff: -assumes fold: "(A,x) \ foldSet f id b" -shows "!!a. \a \ A; b \ A\ \ (insert b (A-{a}), x) \ foldSet f id a" +assumes fold: "foldSet f id b A x" +shows "!!a. \a \ A; b \ A\ \ foldSet f id a (insert b (A-{a})) x" using fold proof (induct rule: foldSet.induct) case emptyI thus ?case by simp next - case (insertI A x y) + case (insertI x A y) have "a = x \ a \ A" using insertI by simp thus ?case proof @@ -1858,7 +1852,7 @@ by (simp add: id_def [symmetric], blast intro: foldSet_insert_swap) next assume ainA: "a \ A" - hence "(insert x (insert b (A - {a})), x \ y) \ foldSet f id a" + hence "foldSet f id a (insert x (insert b (A - {a}))) (x \ y)" using insertI by (force simp: id_def) moreover have "insert x (insert b (A - {a})) = insert b (insert x A - {a})" @@ -1875,7 +1869,7 @@ apply (rule sym, clarify) apply (case_tac "Aa=A") apply (best intro: the_equality foldSet_determ) -apply (subgoal_tac "(A,x) \ foldSet f id a") +apply (subgoal_tac "foldSet f id a A x") apply (best intro: the_equality foldSet_determ) apply (subgoal_tac "insert aa (Aa - {a}) = A") prefer 2 apply (blast elim: equalityE) @@ -1943,18 +1937,18 @@ text{*Not actually used!!*} lemma (in ACf) foldSet_permute: - "[|(insert a A, x) \ foldSet f id b; a \ A; b \ A|] - ==> (insert b A, x) \ foldSet f id a" + "[|foldSet f id b (insert a A) x; a \ A; b \ A|] + ==> foldSet f id a (insert b A) x" apply (case_tac "a=b") apply (auto dest: foldSet_permute_diff) done lemma (in ACf) fold1Set_determ: - "(A, x) \ fold1Set f ==> (A, y) \ fold1Set f ==> y = x" + "fold1Set f A x ==> fold1Set f A y ==> y = x" proof (clarify elim!: fold1Set.cases) fix A x B y a b - assume Ax: "(A, x) \ foldSet f id a" - assume By: "(B, y) \ foldSet f id b" + assume Ax: "foldSet f id a A x" + assume By: "foldSet f id b B y" assume anotA: "a \ A" assume bnotB: "b \ B" assume eq: "insert a A = insert b B" @@ -1970,16 +1964,16 @@ and aB: "a \ B" and bA: "b \ A" using eq anotA bnotB diff by (blast elim!:equalityE)+ with aB bnotB By - have "(insert b ?D, y) \ foldSet f id a" + have "foldSet f id a (insert b ?D) y" by (auto intro: foldSet_permute simp add: insert_absorb) moreover - have "(insert b ?D, x) \ foldSet f id a" + have "foldSet f id a (insert b ?D) x" by (simp add: A [symmetric] Ax) ultimately show ?thesis by (blast intro: foldSet_determ) qed qed -lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y" +lemma (in ACf) fold1Set_equality: "fold1Set f A y ==> fold1 f A = y" by (unfold fold1_def) (blast intro: fold1Set_determ) declare diff -r 9e185f78e7d4 -r 96ba62dff413 src/HOL/List.thy --- a/src/HOL/List.thy Wed Feb 07 17:26:49 2007 +0100 +++ b/src/HOL/List.thy Wed Feb 07 17:28:09 2007 +0100 @@ -2200,40 +2200,71 @@ subsubsection {* @{text lists}: the list-forming operator over sets *} -consts lists :: "'a set => 'a list set" -inductive "lists A" - intros - Nil [intro!]: "[]: lists A" - Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A" - -inductive_cases listsE [elim!]: "x#l : lists A" - -lemma lists_mono [mono]: "A \ B ==> lists A \ lists B" -by (unfold lists.defs) (blast intro!: lfp_mono) - -lemma lists_IntI: - assumes l: "l: lists A" shows "l: lists B ==> l: lists (A Int B)" using l +inductive2 + listsp :: "('a \ bool) \ 'a list \ bool" + for A :: "'a \ bool" +where + Nil [intro!]: "listsp A []" + | Cons [intro!]: "[| A a; listsp A l |] ==> listsp A (a # l)" + +constdefs + lists :: "'a set => 'a list set" + "lists A == Collect (listsp (member A))" + +lemma listsp_lists_eq [pred_set_conv]: "listsp (member A) = member (lists A)" + by (simp add: lists_def) + +lemmas lists_intros [intro!] = listsp.intros [to_set] + +lemmas lists_induct [consumes 1, case_names Nil Cons, induct set: lists] = + listsp.induct [to_set] + +inductive_cases2 listspE [elim!]: "listsp A (x # l)" + +lemmas listsE [elim!] = listspE [to_set] + +lemma listsp_mono [mono2]: "A \ B ==> listsp A \ listsp B" + by (clarify, erule listsp.induct, blast+) + +lemmas lists_mono [mono] = listsp_mono [to_set] + +lemma listsp_meetI: + assumes l: "listsp A l" shows "listsp B l ==> listsp (meet A B) l" using l by induct blast+ -lemma lists_Int_eq [simp]: "lists (A \ B) = lists A \ lists B" -proof (rule mono_Int [THEN equalityI]) - show "mono lists" by (simp add: mono_def lists_mono) - show "lists A \ lists B \ lists (A \ B)" by (blast intro: lists_IntI) +lemmas lists_IntI = listsp_meetI [to_set] + +lemma listsp_meet_eq [simp]: "listsp (meet A B) = meet (listsp A) (listsp B)" +proof (rule mono_meet [where f=listsp, THEN order_antisym]) + show "mono listsp" by (simp add: mono_def listsp_mono) + show "meet (listsp A) (listsp B) \ listsp (meet A B)" by (blast intro: listsp_meetI) qed -lemma append_in_lists_conv [iff]: - "(xs @ ys : lists A) = (xs : lists A \ ys : lists A)" +lemmas listsp_conj_eq [simp] = listsp_meet_eq [simplified meet_fun_eq meet_bool_eq] + +lemmas lists_Int_eq [simp] = listsp_meet_eq [to_set] + +lemma append_in_listsp_conv [iff]: + "(listsp A (xs @ ys)) = (listsp A xs \ listsp A ys)" by (induct xs) auto -lemma in_lists_conv_set: "(xs : lists A) = (\x \ set xs. x : A)" --- {* eliminate @{text lists} in favour of @{text set} *} +lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set] + +lemma in_listsp_conv_set: "(listsp A xs) = (\x \ set xs. A x)" +-- {* eliminate @{text listsp} in favour of @{text set} *} by (induct xs) auto -lemma in_listsD [dest!]: "xs \ lists A ==> \x\set xs. x \ A" -by (rule in_lists_conv_set [THEN iffD1]) - -lemma in_listsI [intro!]: "\x\set xs. x \ A ==> xs \ lists A" -by (rule in_lists_conv_set [THEN iffD2]) +lemmas in_lists_conv_set = in_listsp_conv_set [to_set] + +lemma in_listspD [dest!]: "listsp A xs ==> \x\set xs. A x" +by (rule in_listsp_conv_set [THEN iffD1]) + +lemmas in_listsD [dest!] = in_listspD [to_set] + +lemma in_listspI [intro!]: "\x\set xs. A x ==> listsp A xs" +by (rule in_listsp_conv_set [THEN iffD2]) + +lemmas in_listsI [intro!] = in_listspI [to_set] lemma lists_UNIV [simp]: "lists UNIV = UNIV" by auto @@ -2242,13 +2273,12 @@ subsubsection{* Inductive definition for membership *} -consts ListMem :: "('a \ 'a list)set" -inductive ListMem -intros - elem: "(x,x#xs) \ ListMem" - insert: "(x,xs) \ ListMem \ (x,y#xs) \ ListMem" - -lemma ListMem_iff: "((x,xs) \ ListMem) = (x \ set xs)" +inductive2 ListMem :: "'a \ 'a list \ bool" +where + elem: "ListMem x (x # xs)" + | insert: "ListMem x xs \ ListMem x (y # xs)" + +lemma ListMem_iff: "(ListMem x xs) = (x \ set xs)" apply (rule iffI) apply (induct set: ListMem) apply auto @@ -2495,60 +2525,73 @@ subsubsection{*Lifting a Relation on List Elements to the Lists*} -consts listrel :: "('a * 'a)set => ('a list * 'a list)set" - -inductive "listrel(r)" - intros - Nil: "([],[]) \ listrel r" - Cons: "[| (x,y) \ r; (xs,ys) \ listrel r |] ==> (x#xs, y#ys) \ listrel r" - -inductive_cases listrel_Nil1 [elim!]: "([],xs) \ listrel r" -inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \ listrel r" -inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \ listrel r" -inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \ listrel r" +inductive2 + list_all2' :: "('a \ 'b \ bool) \ 'a list \ 'b list \ bool" + for r :: "'a \ 'b \ bool" +where + Nil: "list_all2' r [] []" + | Cons: "[| r x y; list_all2' r xs ys |] ==> list_all2' r (x#xs) (y#ys)" + +constdefs + listrel :: "('a * 'b) set => ('a list * 'b list) set" + "listrel r == Collect2 (list_all2' (member2 r))" + +lemma list_all2_listrel_eq [pred_set_conv]: + "list_all2' (member2 r) = member2 (listrel r)" + by (simp add: listrel_def) + +lemmas listrel_induct [consumes 1, case_names Nil Cons, induct set: listrel] = + list_all2'.induct [to_set] + +lemmas listrel_intros = list_all2'.intros [to_set] + +inductive_cases2 listrel_Nil1 [to_set, elim!]: "list_all2' r [] xs" +inductive_cases2 listrel_Nil2 [to_set, elim!]: "list_all2' r xs []" +inductive_cases2 listrel_Cons1 [to_set, elim!]: "list_all2' r (y#ys) xs" +inductive_cases2 listrel_Cons2 [to_set, elim!]: "list_all2' r xs (y#ys)" lemma listrel_mono: "r \ s \ listrel r \ listrel s" apply clarify -apply (erule listrel.induct) -apply (blast intro: listrel.intros)+ +apply (erule listrel_induct) +apply (blast intro: listrel_intros)+ done lemma listrel_subset: "r \ A \ A \ listrel r \ lists A \ lists A" apply clarify -apply (erule listrel.induct, auto) +apply (erule listrel_induct, auto) done lemma listrel_refl: "refl A r \ refl (lists A) (listrel r)" apply (simp add: refl_def listrel_subset Ball_def) apply (rule allI) apply (induct_tac x) -apply (auto intro: listrel.intros) +apply (auto intro: listrel_intros) done lemma listrel_sym: "sym r \ sym (listrel r)" apply (auto simp add: sym_def) -apply (erule listrel.induct) -apply (blast intro: listrel.intros)+ +apply (erule listrel_induct) +apply (blast intro: listrel_intros)+ done lemma listrel_trans: "trans r \ trans (listrel r)" apply (simp add: trans_def) apply (intro allI) apply (rule impI) -apply (erule listrel.induct) -apply (blast intro: listrel.intros)+ +apply (erule listrel_induct) +apply (blast intro: listrel_intros)+ done theorem equiv_listrel: "equiv A r \ equiv (lists A) (listrel r)" by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}" -by (blast intro: listrel.intros) +by (blast intro: listrel_intros) lemma listrel_Cons: "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"; -by (auto simp add: set_Cons_def intro: listrel.intros) +by (auto simp add: set_Cons_def intro: listrel_intros) subsection{*Miscellany*} diff -r 9e185f78e7d4 -r 96ba62dff413 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Feb 07 17:26:49 2007 +0100 +++ b/src/HOL/Nat.thy Wed Feb 07 17:28:09 2007 +0100 @@ -30,20 +30,18 @@ text {* Type definition *} -consts - Nat :: "ind set" - -inductive Nat -intros - Zero_RepI: "Zero_Rep : Nat" - Suc_RepI: "i : Nat ==> Suc_Rep i : Nat" +inductive2 Nat :: "ind \ bool" +where + Zero_RepI: "Nat Zero_Rep" + | Suc_RepI: "Nat i ==> Nat (Suc_Rep i)" global typedef (open Nat) - nat = Nat + nat = "Collect Nat" proof - show "Zero_Rep : Nat" by (rule Nat.Zero_RepI) + from Nat.Zero_RepI + show "Zero_Rep : Collect Nat" .. qed text {* Abstract constants and syntax *} @@ -61,22 +59,25 @@ instance nat :: "{ord, zero, one}" Zero_nat_def: "0 == Abs_Nat Zero_Rep" One_nat_def [simp]: "1 == Suc 0" - less_def: "m < n == (m, n) : trancl pred_nat" + less_def: "m < n == (m, n) : pred_nat^+" le_def: "m \ (n::nat) == ~ (n < m)" .. text {* Induction *} +lemmas Rep_Nat' = Rep_Nat [simplified mem_Collect_eq] +lemmas Abs_Nat_inverse' = Abs_Nat_inverse [simplified mem_Collect_eq] + theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" apply (unfold Zero_nat_def Suc_def) apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} - apply (erule Rep_Nat [THEN Nat.induct]) - apply (iprover elim: Abs_Nat_inverse [THEN subst]) + apply (erule Rep_Nat' [THEN Nat.induct]) + apply (iprover elim: Abs_Nat_inverse' [THEN subst]) done text {* Distinctness of constructors *} lemma Suc_not_Zero [iff]: "Suc m \ 0" - by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI + by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat' Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep) lemma Zero_not_Suc [iff]: "0 \ Suc m" @@ -91,7 +92,7 @@ text {* Injectiveness of @{term Suc} *} lemma inj_Suc[simp]: "inj_on Suc N" - by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI + by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat' Suc_RepI inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) lemma Suc_inject: "Suc x = Suc y ==> x = y" diff -r 9e185f78e7d4 -r 96ba62dff413 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Feb 07 17:26:49 2007 +0100 +++ b/src/HOL/Transitive_Closure.thy Wed Feb 07 17:28:09 2007 +0100 @@ -7,7 +7,7 @@ header {* Reflexive and Transitive closure of a relation *} theory Transitive_Closure -imports Inductive +imports Predicate uses "~~/src/Provers/trancl.ML" begin @@ -20,56 +20,85 @@ operands to be atomic. *} -consts - rtrancl :: "('a \ 'a) set => ('a \ 'a) set" ("(_^*)" [1000] 999) - -inductive "r^*" - intros - rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*" - rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*" +inductive2 + rtrancl :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" ("(_^**)" [1000] 1000) + for r :: "'a \ 'a \ bool" +where + rtrancl_refl [intro!, Pure.intro!, simp]: "r^** a a" + | rtrancl_into_rtrancl [Pure.intro]: "r^** a b ==> r b c ==> r^** a c" -consts - trancl :: "('a \ 'a) set => ('a \ 'a) set" ("(_^+)" [1000] 999) +inductive2 + trancl :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" ("(_^++)" [1000] 1000) + for r :: "'a \ 'a \ bool" +where + r_into_trancl [intro, Pure.intro]: "r a b ==> r^++ a b" + | trancl_into_trancl [Pure.intro]: "r^++ a b ==> r b c ==> r^++ a c" -inductive "r^+" - intros - r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" - trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+" +constdefs + rtrancl_set :: "('a \ 'a) set => ('a \ 'a) set" ("(_^*)" [1000] 999) + "r^* == Collect2 (member2 r)^**" + + trancl_set :: "('a \ 'a) set => ('a \ 'a) set" ("(_^+)" [1000] 999) + "r^+ == Collect2 (member2 r)^++" abbreviation - reflcl :: "('a \ 'a) set => ('a \ 'a) set" ("(_^=)" [1000] 999) where + reflcl :: "('a => 'a => bool) => 'a => 'a => bool" ("(_^==)" [1000] 1000) where + "r^== == join r op =" + +abbreviation + reflcl_set :: "('a \ 'a) set => ('a \ 'a) set" ("(_^=)" [1000] 999) where "r^= == r \ Id" notation (xsymbols) - rtrancl ("(_\<^sup>*)" [1000] 999) and - trancl ("(_\<^sup>+)" [1000] 999) and - reflcl ("(_\<^sup>=)" [1000] 999) + rtrancl ("(_\<^sup>*\<^sup>*)" [1000] 1000) and + trancl ("(_\<^sup>+\<^sup>+)" [1000] 1000) and + reflcl ("(_\<^sup>=\<^sup>=)" [1000] 1000) and + rtrancl_set ("(_\<^sup>*)" [1000] 999) and + trancl_set ("(_\<^sup>+)" [1000] 999) and + reflcl_set ("(_\<^sup>=)" [1000] 999) notation (HTML output) - rtrancl ("(_\<^sup>*)" [1000] 999) and - trancl ("(_\<^sup>+)" [1000] 999) and - reflcl ("(_\<^sup>=)" [1000] 999) + rtrancl ("(_\<^sup>*\<^sup>*)" [1000] 1000) and + trancl ("(_\<^sup>+\<^sup>+)" [1000] 1000) and + reflcl ("(_\<^sup>=\<^sup>=)" [1000] 1000) and + rtrancl_set ("(_\<^sup>*)" [1000] 999) and + trancl_set ("(_\<^sup>+)" [1000] 999) and + reflcl_set ("(_\<^sup>=)" [1000] 999) subsection {* Reflexive-transitive closure *} +lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)" + by (simp add: rtrancl_set_def) + +lemma reflcl_set_eq [pred_set_conv]: "(join (member2 r) op =) = member2 (r Un Id)" + by (simp add: expand_fun_eq) + +lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set] +lemmas rtrancl_into_rtrancl [Pure.intro] = rtrancl_into_rtrancl [to_set] + lemma r_into_rtrancl [intro]: "!!p. p \ r ==> p \ r^*" -- {* @{text rtrancl} of @{text r} contains @{text r} *} apply (simp only: split_tupled_all) apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) done -lemma rtrancl_mono: "r \ s ==> r^* \ s^*" +lemma r_into_rtrancl' [intro]: "r x y ==> r^** x y" + -- {* @{text rtrancl} of @{text r} contains @{text r} *} + by (erule rtrancl.rtrancl_refl [THEN rtrancl.rtrancl_into_rtrancl]) + +lemma rtrancl_mono': "r \ s ==> r^** \ s^**" -- {* monotonicity of @{text rtrancl} *} - apply (rule subsetI) - apply (simp only: split_tupled_all) + apply (rule predicate2I) apply (erule rtrancl.induct) - apply (rule_tac [2] rtrancl_into_rtrancl, blast+) + apply (rule_tac [2] rtrancl.rtrancl_into_rtrancl, blast+) done -theorem rtrancl_induct [consumes 1, induct set: rtrancl]: - assumes a: "(a, b) : r^*" - and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z" +lemmas rtrancl_mono = rtrancl_mono' [to_set] + +theorem rtrancl_induct' [consumes 1, induct set: rtrancl]: + assumes a: "r^** a b" + and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z" shows "P b" proof - from a have "a = a --> P b" @@ -77,6 +106,12 @@ thus ?thesis by iprover qed +lemmas rtrancl_induct [consumes 1, induct set: rtrancl_set] = rtrancl_induct' [to_set] + +lemmas rtrancl_induct2' = + rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, + consumes 1, case_names refl step] + lemmas rtrancl_induct2 = rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), consumes 1, case_names refl step] @@ -95,6 +130,12 @@ lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard] +lemma rtrancl_trans': + assumes xy: "r^** x y" + and yz: "r^** y z" + shows "r^** x z" using yz xy + by induct iprover+ + lemma rtranclE: assumes major: "(a::'a,b) : r^*" and cases: "(a = b) ==> P" @@ -114,21 +155,25 @@ apply (erule rtrancl_induct, auto) done -lemma converse_rtrancl_into_rtrancl: - "(a, b) \ r \ (b, c) \ r\<^sup>* \ (a, c) \ r\<^sup>*" - by (rule rtrancl_trans) iprover+ +lemma converse_rtrancl_into_rtrancl': + "r a b \ r\<^sup>*\<^sup>* b c \ r\<^sup>*\<^sup>* a c" + by (rule rtrancl_trans') iprover+ + +lemmas converse_rtrancl_into_rtrancl = converse_rtrancl_into_rtrancl' [to_set] text {* \medskip More @{term "r^*"} equations and inclusions. *} -lemma rtrancl_idemp [simp]: "(r^*)^* = r^*" - apply auto - apply (erule rtrancl_induct) - apply (rule rtrancl_refl) - apply (blast intro: rtrancl_trans) +lemma rtrancl_idemp' [simp]: "(r^**)^** = r^**" + apply (auto intro!: order_antisym) + apply (erule rtrancl_induct') + apply (rule rtrancl.rtrancl_refl) + apply (blast intro: rtrancl_trans') done +lemmas rtrancl_idemp [simp] = rtrancl_idemp' [to_set] + lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*" apply (rule set_ext) apply (simp only: split_tupled_all) @@ -138,16 +183,22 @@ lemma rtrancl_subset_rtrancl: "r \ s^* ==> r^* \ s^*" by (drule rtrancl_mono, simp) -lemma rtrancl_subset: "R \ S ==> S \ R^* ==> S^* = R^*" - apply (drule rtrancl_mono) - apply (drule rtrancl_mono, simp) +lemma rtrancl_subset': "R \ S ==> S \ R^** ==> S^** = R^**" + apply (drule rtrancl_mono') + apply (drule rtrancl_mono', simp) done -lemma rtrancl_Un_rtrancl: "(R^* \ S^*)^* = (R \ S)^*" - by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD]) +lemmas rtrancl_subset = rtrancl_subset' [to_set] + +lemma rtrancl_Un_rtrancl': "(join (R^**) (S^**))^** = (join R S)^**" + by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D]) -lemma rtrancl_reflcl [simp]: "(R^=)^* = R^*" - by (blast intro!: rtrancl_subset intro: r_into_rtrancl) +lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set] + +lemma rtrancl_reflcl' [simp]: "(R^==)^** = R^**" + by (blast intro!: rtrancl_subset') + +lemmas rtrancl_reflcl [simp] = rtrancl_reflcl' [to_set] lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*" apply (rule sym) @@ -157,58 +208,75 @@ apply (blast intro!: r_into_rtrancl) done -theorem rtrancl_converseD: - assumes r: "(x, y) \ (r^-1)^*" - shows "(y, x) \ r^*" +lemma rtrancl_r_diff_Id': "(meet r op ~=)^** = r^**" + apply (rule sym) + apply (rule rtrancl_subset') + apply blast+ + done + +theorem rtrancl_converseD': + assumes r: "(r^--1)^** x y" + shows "r^** y x" proof - from r show ?thesis - by induct (iprover intro: rtrancl_trans dest!: converseD)+ + by induct (iprover intro: rtrancl_trans' dest!: conversepD)+ qed -theorem rtrancl_converseI: - assumes r: "(y, x) \ r^*" - shows "(x, y) \ (r^-1)^*" +lemmas rtrancl_converseD = rtrancl_converseD' [to_set] + +theorem rtrancl_converseI': + assumes r: "r^** y x" + shows "(r^--1)^** x y" proof - from r show ?thesis - by induct (iprover intro: rtrancl_trans converseI)+ + by induct (iprover intro: rtrancl_trans' conversepI)+ qed +lemmas rtrancl_converseI = rtrancl_converseI' [to_set] + lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) lemma sym_rtrancl: "sym r ==> sym (r^*)" by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) -theorem converse_rtrancl_induct[consumes 1]: - assumes major: "(a, b) : r^*" - and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y" +theorem converse_rtrancl_induct'[consumes 1]: + assumes major: "r^** a b" + and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y" shows "P a" proof - - from rtrancl_converseI [OF major] + from rtrancl_converseI' [OF major] show ?thesis - by induct (iprover intro: cases dest!: converseD rtrancl_converseD)+ + by induct (iprover intro: cases dest!: conversepD rtrancl_converseD')+ qed +lemmas converse_rtrancl_induct[consumes 1] = converse_rtrancl_induct' [to_set] + +lemmas converse_rtrancl_induct2' = + converse_rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, + consumes 1, case_names refl step] + lemmas converse_rtrancl_induct2 = converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), consumes 1, case_names refl step] -lemma converse_rtranclE: - assumes major: "(x,z):r^*" +lemma converse_rtranclE': + assumes major: "r^** x z" and cases: "x=z ==> P" - "!!y. [| (x,y):r; (y,z):r^* |] ==> P" + "!!y. [| r x y; r^** y z |] ==> P" shows P - apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)") - apply (rule_tac [2] major [THEN converse_rtrancl_induct]) + apply (subgoal_tac "x = z | (EX y. r x y & r^** y z)") + apply (rule_tac [2] major [THEN converse_rtrancl_induct']) prefer 2 apply iprover prefer 2 apply iprover apply (erule asm_rl exE disjE conjE cases)+ done -ML_setup {* - bind_thm ("converse_rtranclE2", split_rule - (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] (thm "converse_rtranclE"))); -*} +lemmas converse_rtranclE = converse_rtranclE' [to_set] + +lemmas converse_rtranclE2' = converse_rtranclE' [of _ "(xa,xb)" "(za,zb)", split_rule] + +lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] lemma r_comp_rtrancl_eq: "r O r^* = r^* O r" by (blast elim: rtranclE converse_rtranclE @@ -220,8 +288,14 @@ subsection {* Transitive closure *} +lemma trancl_set_eq [pred_set_conv]: "(member2 r)^++ = member2 (r^+)" + by (simp add: trancl_set_def) + +lemmas r_into_trancl [intro, Pure.intro] = r_into_trancl [to_set] +lemmas trancl_into_trancl [Pure.intro] = trancl_into_trancl [to_set] + lemma trancl_mono: "!!p. p \ r^+ ==> r \ s ==> p \ s^+" - apply (simp only: split_tupled_all) + apply (simp add: split_tupled_all trancl_set_def) apply (erule trancl.induct) apply (iprover dest: subsetD)+ done @@ -233,24 +307,30 @@ \medskip Conversions between @{text trancl} and @{text rtrancl}. *} -lemma trancl_into_rtrancl: "(a, b) \ r^+ ==> (a, b) \ r^*" +lemma trancl_into_rtrancl': "r^++ a b ==> r^** a b" by (erule trancl.induct) iprover+ -lemma rtrancl_into_trancl1: assumes r: "(a, b) \ r^*" - shows "!!c. (b, c) \ r ==> (a, c) \ r^+" using r +lemmas trancl_into_rtrancl = trancl_into_rtrancl' [to_set] + +lemma rtrancl_into_trancl1': assumes r: "r^** a b" + shows "!!c. r b c ==> r^++ a c" using r by induct iprover+ -lemma rtrancl_into_trancl2: "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+" +lemmas rtrancl_into_trancl1 = rtrancl_into_trancl1' [to_set] + +lemma rtrancl_into_trancl2': "[| r a b; r^** b c |] ==> r^++ a c" -- {* intro rule from @{text r} and @{text rtrancl} *} - apply (erule rtranclE, iprover) - apply (rule rtrancl_trans [THEN rtrancl_into_trancl1]) - apply (assumption | rule r_into_rtrancl)+ + apply (erule rtrancl.cases, iprover) + apply (rule rtrancl_trans' [THEN rtrancl_into_trancl1']) + apply (simp | rule r_into_rtrancl')+ done -lemma trancl_induct [consumes 1, induct set: trancl]: - assumes a: "(a,b) : r^+" - and cases: "!!y. (a, y) : r ==> P y" - "!!y z. (a,y) : r^+ ==> (y, z) : r ==> P y ==> P z" +lemmas rtrancl_into_trancl2 = rtrancl_into_trancl2' [to_set] + +lemma trancl_induct' [consumes 1, induct set: trancl]: + assumes a: "r^++ a b" + and cases: "!!y. r a y ==> P y" + "!!y z. r^++ a y ==> r y z ==> P y ==> P z" shows "P b" -- {* Nice induction rule for @{text trancl} *} proof - @@ -259,19 +339,32 @@ thus ?thesis by iprover qed +lemmas trancl_induct [consumes 1, induct set: trancl_set] = trancl_induct' [to_set] + +lemmas trancl_induct2' = + trancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, + consumes 1, case_names base step] + lemmas trancl_induct2 = trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), consumes 1, case_names base step] -lemma trancl_trans_induct: - assumes major: "(x,y) : r^+" - and cases: "!!x y. (x,y) : r ==> P x y" - "!!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z" +lemma trancl_trans_induct': + assumes major: "r^++ x y" + and cases: "!!x y. r x y ==> P x y" + "!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z" shows "P x y" -- {* Another induction rule for trancl, incorporating transitivity *} - by (iprover intro: r_into_trancl major [THEN trancl_induct] cases) + by (iprover intro: major [THEN trancl_induct'] cases) + +lemmas trancl_trans_induct = trancl_trans_induct' [to_set] -inductive_cases tranclE: "(a, b) : r^+" +lemma tranclE: + assumes H: "(a, b) : r^+" + and cases: "(a, b) : r ==> P" "\c. (a, c) : r^+ ==> (c, b) : r ==> P" + shows P + using H [simplified trancl_set_def, simplified] + by cases (auto intro: cases [simplified trancl_set_def, simplified]) lemma trancl_Int_subset: "[| r \ s; r O (r^+ \ s) \ s|] ==> r^+ \ s" apply (rule subsetI) @@ -293,6 +386,12 @@ lemmas trancl_trans = trans_trancl [THEN transD, standard] +lemma trancl_trans': + assumes xy: "r^++ x y" + and yz: "r^++ y z" + shows "r^++ x z" using yz xy + by induct iprover+ + lemma trancl_id[simp]: "trans r \ r^+ = r" apply(auto) apply(erule trancl_induct) @@ -301,12 +400,16 @@ apply(blast) done -lemma rtrancl_trancl_trancl: assumes r: "(x, y) \ r^*" - shows "!!z. (y, z) \ r^+ ==> (x, z) \ r^+" using r - by induct (iprover intro: trancl_trans)+ +lemma rtrancl_trancl_trancl': assumes r: "r^** x y" + shows "!!z. r^++ y z ==> r^++ x z" using r + by induct (iprover intro: trancl_trans')+ -lemma trancl_into_trancl2: "(a, b) \ r ==> (b, c) \ r^+ ==> (a, c) \ r^+" - by (erule transD [OF trans_trancl r_into_trancl]) +lemmas rtrancl_trancl_trancl = rtrancl_trancl_trancl' [to_set] + +lemma trancl_into_trancl2': "r a b ==> r^++ b c ==> r^++ a c" + by (erule trancl_trans' [OF trancl.r_into_trancl]) + +lemmas trancl_into_trancl2 = trancl_into_trancl2' [to_set] lemma trancl_insert: "(insert (y, x) r)^+ = r^+ \ {(a, b). (a, y) \ r^* \ (x, b) \ r^*}" @@ -321,41 +424,51 @@ [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) done -lemma trancl_converseI: "(x, y) \ (r^+)^-1 ==> (x, y) \ (r^-1)^+" - apply (drule converseD) - apply (erule trancl.induct) - apply (iprover intro: converseI trancl_trans)+ +lemma trancl_converseI': "(r^++)^--1 x y ==> (r^--1)^++ x y" + apply (drule conversepD) + apply (erule trancl_induct') + apply (iprover intro: conversepI trancl_trans')+ done -lemma trancl_converseD: "(x, y) \ (r^-1)^+ ==> (x, y) \ (r^+)^-1" - apply (rule converseI) - apply (erule trancl.induct) - apply (iprover dest: converseD intro: trancl_trans)+ +lemmas trancl_converseI = trancl_converseI' [to_set] + +lemma trancl_converseD': "(r^--1)^++ x y ==> (r^++)^--1 x y" + apply (rule conversepI) + apply (erule trancl_induct') + apply (iprover dest: conversepD intro: trancl_trans')+ done -lemma trancl_converse: "(r^-1)^+ = (r^+)^-1" - by (fastsimp simp add: split_tupled_all - intro!: trancl_converseI trancl_converseD) +lemmas trancl_converseD = trancl_converseD' [to_set] + +lemma trancl_converse': "(r^--1)^++ = (r^++)^--1" + by (fastsimp simp add: expand_fun_eq + intro!: trancl_converseI' dest!: trancl_converseD') + +lemmas trancl_converse = trancl_converse' [to_set] lemma sym_trancl: "sym r ==> sym (r^+)" by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) -lemma converse_trancl_induct: - assumes major: "(a,b) : r^+" - and cases: "!!y. (y,b) : r ==> P(y)" - "!!y z.[| (y,z) : r; (z,b) : r^+; P(z) |] ==> P(y)" +lemma converse_trancl_induct': + assumes major: "r^++ a b" + and cases: "!!y. r y b ==> P(y)" + "!!y z.[| r y z; r^++ z b; P(z) |] ==> P(y)" shows "P a" - apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]]) + apply (rule trancl_induct' [OF trancl_converseI', OF conversepI, OF major]) apply (rule cases) - apply (erule converseD) - apply (blast intro: prems dest!: trancl_converseD) + apply (erule conversepD) + apply (blast intro: prems dest!: trancl_converseD' conversepD) done -lemma tranclD: "(x, y) \ R^+ ==> EX z. (x, z) \ R \ (z, y) \ R^*" - apply (erule converse_trancl_induct, auto) - apply (blast intro: rtrancl_trans) +lemmas converse_trancl_induct = converse_trancl_induct' [to_set] + +lemma tranclD': "R^++ x y ==> EX z. R x z \ R^** z y" + apply (erule converse_trancl_induct', auto) + apply (blast intro: rtrancl_trans') done +lemmas tranclD = tranclD' [to_set] + lemma irrefl_tranclI: "r^-1 \ r^* = {} ==> (x, x) \ r^+" by (blast elim: tranclE dest: trancl_into_rtrancl) @@ -373,12 +486,14 @@ apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ done -lemma reflcl_trancl [simp]: "(r^+)^= = r^*" - apply safe - apply (erule trancl_into_rtrancl) - apply (blast elim: rtranclE dest: rtrancl_into_trancl1) +lemma reflcl_trancl' [simp]: "(r^++)^== = r^**" + apply (safe intro!: order_antisym) + apply (erule trancl_into_rtrancl') + apply (blast elim: rtrancl.cases dest: rtrancl_into_trancl1') done +lemmas reflcl_trancl [simp] = reflcl_trancl' [to_set] + lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" apply safe apply (drule trancl_into_rtrancl, simp) @@ -394,8 +509,10 @@ lemma rtrancl_empty [simp]: "{}^* = Id" by (rule subst [OF reflcl_trancl]) simp -lemma rtranclD: "(a, b) \ R^* ==> a = b \ a \ b \ (a, b) \ R^+" - by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl) +lemma rtranclD': "R^** a b ==> a = b \ a \ b \ R^++ a b" + by (force simp add: reflcl_trancl' [symmetric] simp del: reflcl_trancl') + +lemmas rtranclD = rtranclD' [to_set] lemma rtrancl_eq_or_trancl: "(x,y) \ R\<^sup>* = (x=y \ x\y \ (x,y) \ R\<^sup>+)" @@ -450,24 +567,32 @@ apply (fast intro: r_r_into_trancl trancl_trans) done -lemma trancl_rtrancl_trancl: - "(a, b) \ r\<^sup>+ ==> (b, c) \ r\<^sup>* ==> (a, c) \ r\<^sup>+" - apply (drule tranclD) +lemma trancl_rtrancl_trancl': + "r\<^sup>+\<^sup>+ a b ==> r\<^sup>*\<^sup>* b c ==> r\<^sup>+\<^sup>+ a c" + apply (drule tranclD') apply (erule exE, erule conjE) - apply (drule rtrancl_trans, assumption) - apply (drule rtrancl_into_trancl2, assumption, assumption) + apply (drule rtrancl_trans', assumption) + apply (drule rtrancl_into_trancl2', assumption, assumption) done +lemmas trancl_rtrancl_trancl = trancl_rtrancl_trancl' [to_set] + lemmas transitive_closure_trans [trans] = r_r_into_trancl trancl_trans rtrancl_trans trancl_into_trancl trancl_into_trancl2 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl rtrancl_trancl_trancl trancl_rtrancl_trancl +lemmas transitive_closure_trans' [trans] = + trancl_trans' rtrancl_trans' + trancl.trancl_into_trancl trancl_into_trancl2' + rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl' + rtrancl_trancl_trancl' trancl_rtrancl_trancl' + declare trancl_into_rtrancl [elim] -declare rtranclE [cases set: rtrancl] -declare tranclE [cases set: trancl] +declare rtranclE [cases set: rtrancl_set] +declare tranclE [cases set: trancl_set] @@ -490,8 +615,8 @@ fun decomp (Trueprop $ t) = let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = - let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") - | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") + let fun decr (Const ("Transitive_Closure.rtrancl_set", _ ) $ r) = (r,"r*") + | decr (Const ("Transitive_Closure.trancl_set", _ ) $ r) = (r,"r+") | decr r = (r,"r"); val (rel,r) = decr rel; in SOME (a,b,rel,r) end @@ -500,9 +625,34 @@ end); +structure Tranclp_Tac = Trancl_Tac_Fun ( + struct + val r_into_trancl = thm "trancl.r_into_trancl"; + val trancl_trans = thm "trancl_trans'"; + val rtrancl_refl = thm "rtrancl.rtrancl_refl"; + val r_into_rtrancl = thm "r_into_rtrancl'"; + val trancl_into_rtrancl = thm "trancl_into_rtrancl'"; + val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl'"; + val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl'"; + val rtrancl_trans = thm "rtrancl_trans'"; + + fun decomp (Trueprop $ t) = + let fun dec (rel $ a $ b) = + let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") + | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") + | decr r = (r,"r"); + val (rel,r) = decr rel; + in SOME (a, b, Envir.beta_eta_contract rel, r) end + | dec _ = NONE + in dec t end; + + end); + change_simpset (fn ss => ss addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac)) - addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))); + addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)) + addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac)) + addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac))); *} @@ -514,5 +664,11 @@ method_setup rtrancl = {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *} {* simple transitivity reasoner *} +method_setup tranclp = + {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *} + {* simple transitivity reasoner (predicate version) *} +method_setup rtranclp = + {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *} + {* simple transitivity reasoner (predicate version) *} end