# HG changeset patch # User blanchet # Date 1325513746 -3600 # Node ID 86e6e9d42ad7abc1ae823397959cfd2fa441941a # Parent a109eb27f54f123171ce66b0463b17299e9a48e7 ported "Sets" example to "set" type constructor diff -r a109eb27f54f -r 86e6e9d42ad7 src/HOL/Metis_Examples/Sets.thy --- a/src/HOL/Metis_Examples/Sets.thy Mon Jan 02 15:08:40 2012 +0100 +++ b/src/HOL/Metis_Examples/Sets.thy Mon Jan 02 15:15:46 2012 +0100 @@ -24,50 +24,50 @@ sledgehammer_params [isar_proof, isar_shrink_factor = 1] (*multiple versions of this example*) -(* lemma (*equal_union: *) +lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" proof - - have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>1 \ x\<^isub>2" by (metis Un_commute Un_upper2) - have F2a: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) - have F2: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq) + have F1: "\(x\<^isub>2\'b set) x\<^isub>1\'b set. x\<^isub>1 \ x\<^isub>1 \ x\<^isub>2" by (metis Un_commute Un_upper2) + have F2a: "\(x\<^isub>2\'b set) x\<^isub>1\'b set. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) + have F2: "\(x\<^isub>2\'b set) x\<^isub>1\'b set. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq) { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } moreover { assume AA1: "Y \ Z \ X" { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis F1) } moreover { assume AAA1: "Y \ X \ Y \ Z \ X" { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } moreover { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" hence "Y \ Z \ X \ X \ Y \ Z" by (metis Un_subset_iff) hence "Y \ Z \ X \ \ X \ Y \ Z" by (metis F2) - hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1) } + hence "\x\<^isub>1\'a set. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis AA1) } moreover - { assume "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + { assume "\x\<^isub>1\'a set. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis F1) } moreover { assume AAA1: "Y \ X \ Y \ Z \ X" { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } moreover { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" hence "Y \ Z \ X \ X \ Y \ Z" by (metis Un_subset_iff) hence "Y \ Z \ X \ \ X \ Y \ Z" by (metis F2) - hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by blast } + hence "\x\<^isub>1\'a set. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis AAA1) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by blast } moreover { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1) } - ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by metis + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis F1) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by metis qed sledgehammer_params [isar_proof, isar_shrink_factor = 2] @@ -75,36 +75,36 @@ lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" proof - - have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) - { assume AA1: "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + have F1: "\(x\<^isub>2\'b set) x\<^isub>1\'b set. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) + { assume AA1: "\x\<^isub>1\'a set. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" { assume AAA1: "Y \ X \ Y \ Z \ X" { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } moreover { assume "Y \ Z \ X \ X \ Y \ Z" - hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AAA1 Un_subset_iff) } + hence "\x\<^isub>1\'a set. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis AAA1 Un_subset_iff) } moreover { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } moreover { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } moreover { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } moreover { assume AA1: "Y \ X \ Y \ Z \ X" { assume "\ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } moreover { assume "Y \ Z \ X \ X \ Y \ Z" - hence "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } - ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by metis + hence "\x\<^isub>1\'a set. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" by (metis F1 Un_commute Un_upper2) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + ultimately have "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_subset_iff) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by metis qed sledgehammer_params [isar_proof, isar_shrink_factor = 3] @@ -112,16 +112,16 @@ lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" proof - - have F1a: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) - have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq) + have F1a: "\(x\<^isub>2\'b set) x\<^isub>1\'b set. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 = x\<^isub>2 \ x\<^isub>1" by (metis Un_commute subset_Un_eq) + have F1: "\(x\<^isub>2\'b set) x\<^isub>1\'b set. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq) { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } moreover - { assume AA1: "\x\<^isub>1\'a \ bool. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" + { assume AA1: "\x\<^isub>1\'a set. (Z \ x\<^isub>1 \ Y \ x\<^isub>1) \ \ X \ x\<^isub>1" { assume "(Z \ X \ Y \ X) \ Y \ Z \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) } - ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) qed sledgehammer_params [isar_proof, isar_shrink_factor = 4] @@ -129,15 +129,15 @@ lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" proof - - have F1: "\(x\<^isub>2\'b \ bool) x\<^isub>1\'b \ bool. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) + have F1: "\(x\<^isub>2\'b set) x\<^isub>1\'b set. x\<^isub>1 \ x\<^isub>2 \ x\<^isub>2 \ x\<^isub>1 \ x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) { assume "\ Y \ X" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) } moreover { assume AA1: "Y \ X \ Y \ Z \ X" - { assume "\x\<^isub>1\'a \ bool. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } - hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) } - ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a \ bool. Y \ V \ Z \ V \ X \ V))" by (metis Un_subset_iff Un_upper2) + { assume "\x\<^isub>1\'a set. Y \ x\<^isub>1 \ Z \ Y \ Z \ X \ \ X \ x\<^isub>1 \ Z" + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_upper2) } + hence "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) } + ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_subset_iff Un_upper2) qed sledgehammer_params [isar_proof, isar_shrink_factor = 1] @@ -172,8 +172,8 @@ assume "\x \ S. \S \ x" hence "\x\<^isub>1. x\<^isub>1 \ \S \ x\<^isub>1 \ S \ x\<^isub>1 = \S" by (metis set_eq_subset) hence "\x\<^isub>1. x\<^isub>1 \ S \ x\<^isub>1 = \S" by (metis Union_upper) - hence "\x\<^isub>1\('a \ bool) \ bool. \S \ x\<^isub>1 \ S \ x\<^isub>1" by (metis subsetI) - hence "\x\<^isub>1\('a \ bool) \ bool. S \ insert (\S) x\<^isub>1" by (metis insert_iff) + hence "\x\<^isub>1\('a set) set. \S \ x\<^isub>1 \ S \ x\<^isub>1" by (metis subsetI) + hence "\x\<^isub>1\('a set) set. S \ insert (\S) x\<^isub>1" by (metis insert_iff) thus "\z. S \ {z}" by metis qed @@ -194,12 +194,11 @@ "(\C. (0, 0) \ C \ (\x y. (x, y) \ C \ (Suc x, Suc y) \ C) \ (n, m) \ C) \ Q n \ Q m" apply (metis all_not_in_conv) apply (metis all_not_in_conv) - apply (metis mem_def) + apply (metis mem_Collect_eq) apply (metis less_int_def singleton_iff) - apply (metis mem_def) - apply (metis mem_def) + apply (metis mem_Collect_eq) + apply (metis mem_Collect_eq) apply (metis all_not_in_conv) by (metis pair_in_Id_conv) -*) end