src/HOL/Auth/Message.ML
changeset 2516 4d68fbe6378b
parent 2484 596a5b5a68ff
child 2559 06b6a499f8ae
equal deleted inserted replaced
2515:6ff9bd353121 2516:4d68fbe6378b
    14 
    14 
    15 fun expand_case_tac P i =
    15 fun expand_case_tac P i =
    16     res_inst_tac [("P",P)] expand_case i THEN
    16     res_inst_tac [("P",P)] expand_case i THEN
    17     Simp_tac (i+1) THEN 
    17     Simp_tac (i+1) THEN 
    18     Simp_tac i;
    18     Simp_tac i;
    19 
       
    20 
       
    21 
       
    22 (*GOALS.ML??*)
       
    23 fun prlim n = (goals_limit:=n; pr());
       
    24 
       
    25 (*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
       
    26 goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
       
    27 by (fast_tac (!claset addEs [equalityE]) 1);
       
    28 val subset_range_iff = result();
       
    29 
    19 
    30 
    20 
    31 open Message;
    21 open Message;
    32 
    22 
    33 AddIffs (msg.inject);
    23 AddIffs (msg.inject);
    42 qed "invKey_eq";
    32 qed "invKey_eq";
    43 
    33 
    44 Addsimps [invKey, invKey_eq];
    34 Addsimps [invKey, invKey_eq];
    45 
    35 
    46 
    36 
    47 (**** Freeness laws for HPair ****)
       
    48 
       
    49 goalw thy [HPair_def] "Agent A ~= HPair X Y";
       
    50 by (Simp_tac 1);
       
    51 qed "Agent_neq_HPair";
       
    52 
       
    53 goalw thy [HPair_def] "Nonce N ~= HPair X Y";
       
    54 by (Simp_tac 1);
       
    55 qed "Nonce_neq_HPair";
       
    56 
       
    57 goalw thy [HPair_def] "Key K ~= HPair X Y";
       
    58 by (Simp_tac 1);
       
    59 qed "Key_neq_HPair";
       
    60 
       
    61 goalw thy [HPair_def] "Hash Z ~= HPair X Y";
       
    62 by (Simp_tac 1);
       
    63 qed "Hash_neq_HPair";
       
    64 
       
    65 goalw thy [HPair_def] "Crypt K X' ~= HPair X Y";
       
    66 by (Simp_tac 1);
       
    67 qed "Crypt_neq_HPair";
       
    68 
       
    69 val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
       
    70 		  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
       
    71 
       
    72 AddIffs HPair_neqs;
       
    73 AddIffs (HPair_neqs RL [not_sym]);
       
    74 
       
    75 goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)";
       
    76 by (Simp_tac 1);
       
    77 qed "HPair_eq";
       
    78 
       
    79 goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)";
       
    80 by (Simp_tac 1);
       
    81 qed "MPair_eq_HPair";
       
    82 
       
    83 goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
       
    84 by (Auto_tac());
       
    85 qed "HPair_eq_MPair";
       
    86 
       
    87 AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
       
    88 
       
    89 
       
    90 (**** keysFor operator ****)
    37 (**** keysFor operator ****)
    91 
    38 
    92 goalw thy [keysFor_def] "keysFor {} = {}";
    39 goalw thy [keysFor_def] "keysFor {} = {}";
    93 by (Fast_tac 1);
    40 by (Fast_tac 1);
    94 qed "keysFor_empty";
    41 qed "keysFor_empty";
   131 by (Auto_tac());
    78 by (Auto_tac());
   132 qed "keysFor_insert_Crypt";
    79 qed "keysFor_insert_Crypt";
   133 
    80 
   134 Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    81 Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
   135           keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
    82           keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
   136 	  keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
    83           keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
   137 
    84 
   138 goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
    85 goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
   139 by (Fast_tac 1);
    86 by (Fast_tac 1);
   140 qed "Crypt_imp_invKey_keysFor";
    87 qed "Crypt_imp_invKey_keysFor";
   141 
    88 
   280 
   227 
   281 (** Rewrite rules for pulling out atomic messages **)
   228 (** Rewrite rules for pulling out atomic messages **)
   282 
   229 
   283 fun parts_tac i =
   230 fun parts_tac i =
   284   EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
   231   EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
   285 	 etac parts.induct i,
   232          etac parts.induct i,
   286 	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
   233          REPEAT (fast_tac (!claset addss (!simpset)) i)];
   287 
   234 
   288 goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   235 goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   289 by (parts_tac 1);
   236 by (parts_tac 1);
   290 qed "parts_insert_Agent";
   237 qed "parts_insert_Agent";
   291 
   238 
   408 
   355 
   409 (** Rewrite rules for pulling out atomic messages **)
   356 (** Rewrite rules for pulling out atomic messages **)
   410 
   357 
   411 fun analz_tac i =
   358 fun analz_tac i =
   412   EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
   359   EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
   413 	 etac analz.induct i,
   360          etac analz.induct i,
   414 	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
   361          REPEAT (fast_tac (!claset addss (!simpset)) i)];
   415 
   362 
   416 goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   363 goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   417 by (analz_tac 1);
   364 by (analz_tac 1);
   418 qed "analz_insert_Agent";
   365 qed "analz_insert_Agent";
   419 
   366 
   486 by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
   433 by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
   487                                                analz_insert_Decrypt])));
   434                                                analz_insert_Decrypt])));
   488 qed "analz_Crypt_if";
   435 qed "analz_Crypt_if";
   489 
   436 
   490 Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
   437 Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
   491 	  analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
   438           analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
   492 
   439 
   493 (*This rule supposes "for the sake of argument" that we have the key.*)
   440 (*This rule supposes "for the sake of argument" that we have the key.*)
   494 goal thy  "analz (insert (Crypt K X) H) <=  \
   441 goal thy  "analz (insert (Crypt K X) H) <=  \
   495 \          insert (Crypt K X) (analz (insert X H))";
   442 \          insert (Crypt K X) (analz (insert X H))";
   496 by (rtac subsetI 1);
   443 by (rtac subsetI 1);
   585 
   532 
   586 (*Can only produce a nonce or key if it is already known,
   533 (*Can only produce a nonce or key if it is already known,
   587   but can synth a pair or encryption from its components...*)
   534   but can synth a pair or encryption from its components...*)
   588 val mk_cases = synth.mk_cases msg.simps;
   535 val mk_cases = synth.mk_cases msg.simps;
   589 
   536 
   590 (*NO Agent_synth, as any Agent name can be synthd*)
   537 (*NO Agent_synth, as any Agent name can be synthesized*)
   591 val Nonce_synth = mk_cases "Nonce n : synth H";
   538 val Nonce_synth = mk_cases "Nonce n : synth H";
   592 val Key_synth   = mk_cases "Key K : synth H";
   539 val Key_synth   = mk_cases "Key K : synth H";
   593 val Hash_synth  = mk_cases "Hash X : synth H";
   540 val Hash_synth  = mk_cases "Hash X : synth H";
   594 val MPair_synth = mk_cases "{|X,Y|} : synth H";
   541 val MPair_synth = mk_cases "{|X,Y|} : synth H";
   595 val Crypt_synth = mk_cases "Crypt K X : synth H";
   542 val Crypt_synth = mk_cases "Crypt K X : synth H";
   750                       addSEs [impOfSubs analz_mono]) 2);
   697                       addSEs [impOfSubs analz_mono]) 2);
   751 by (Full_simp_tac 1);
   698 by (Full_simp_tac 1);
   752 by (Fast_tac 1);
   699 by (Fast_tac 1);
   753 qed "Fake_analz_insert";
   700 qed "Fake_analz_insert";
   754 
   701 
   755 (*Needed????????????????*)
       
   756 goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
       
   757 \              analz (insert X H) <= synth (analz H) Un analz H";
       
   758 by (rtac subsetI 1);
       
   759 by (subgoal_tac "x : analz (synth (analz H))" 1);
       
   760 by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
       
   761                       addSEs [impOfSubs analz_mono]) 2);
       
   762 by (Full_simp_tac 1);
       
   763 by (Fast_tac 1);
       
   764 qed "Fake_analz_insert_old";
       
   765 
       
   766 goal thy "(X: analz H & X: parts H) = (X: analz H)";
   702 goal thy "(X: analz H & X: parts H) = (X: analz H)";
   767 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
   703 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
   768 val analz_conj_parts = result();
   704 val analz_conj_parts = result();
   769 
   705 
   770 goal thy "(X: analz H | X: parts H) = (X: parts H)";
   706 goal thy "(X: analz H | X: parts H) = (X: parts H)";
   786 \              ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
   722 \              ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
   787 by (Fast_tac 1);
   723 by (Fast_tac 1);
   788 qed "Crypt_synth_analz";
   724 qed "Crypt_synth_analz";
   789 
   725 
   790 
   726 
   791 goal thy "!!K. Key K ~: analz H \
   727 goal thy "!!K. X ~: synth (analz H) \
   792 \   ==> (Hash{|Key K,X|} : synth (analz H)) = (Hash{|Key K,X|} : analz H)";
   728 \   ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
   793 by (Fast_tac 1);
   729 by (Fast_tac 1);
   794 qed "Hash_synth_analz";
   730 qed "Hash_synth_analz";
   795 Addsimps [Hash_synth_analz];
   731 Addsimps [Hash_synth_analz];
   796 
   732 
   797 
   733 
   798 (**** HPair: a combination of Hash and MPair ****)
   734 (**** HPair: a combination of Hash and MPair ****)
   799 
   735 
   800 (*** Freeness ***)
   736 (*** Freeness ***)
   801 
   737 
   802 goalw thy [HPair_def] "Agent A ~= HPair X Y";
   738 goalw thy [HPair_def] "Agent A ~= Hash[X] Y";
   803 by (Simp_tac 1);
   739 by (Simp_tac 1);
   804 qed "Agent_neq_HPair";
   740 qed "Agent_neq_HPair";
   805 
   741 
   806 goalw thy [HPair_def] "Nonce N ~= HPair X Y";
   742 goalw thy [HPair_def] "Nonce N ~= Hash[X] Y";
   807 by (Simp_tac 1);
   743 by (Simp_tac 1);
   808 qed "Nonce_neq_HPair";
   744 qed "Nonce_neq_HPair";
   809 
   745 
   810 goalw thy [HPair_def] "Key K ~= HPair X Y";
   746 goalw thy [HPair_def] "Key K ~= Hash[X] Y";
   811 by (Simp_tac 1);
   747 by (Simp_tac 1);
   812 qed "Key_neq_HPair";
   748 qed "Key_neq_HPair";
   813 
   749 
   814 goalw thy [HPair_def] "Hash Z ~= HPair X Y";
   750 goalw thy [HPair_def] "Hash Z ~= Hash[X] Y";
   815 by (Simp_tac 1);
   751 by (Simp_tac 1);
   816 qed "Hash_neq_HPair";
   752 qed "Hash_neq_HPair";
   817 
   753 
   818 goalw thy [HPair_def] "Crypt K X' ~= HPair X Y";
   754 goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y";
   819 by (Simp_tac 1);
   755 by (Simp_tac 1);
   820 qed "Crypt_neq_HPair";
   756 qed "Crypt_neq_HPair";
   821 
   757 
   822 val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
   758 val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
   823 		  Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
   759                   Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
   824 
   760 
   825 AddIffs HPair_neqs;
   761 AddIffs HPair_neqs;
   826 AddIffs (HPair_neqs RL [not_sym]);
   762 AddIffs (HPair_neqs RL [not_sym]);
   827 
   763 
   828 goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)";
   764 goalw thy [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
   829 by (Simp_tac 1);
   765 by (Simp_tac 1);
   830 qed "HPair_eq";
   766 qed "HPair_eq";
   831 
   767 
   832 goalw thy [HPair_def] "({|X',Y'|} = HPair X Y) = (X' = Hash{|X,Y|} & Y'=Y)";
   768 goalw thy [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
   833 by (Simp_tac 1);
   769 by (Simp_tac 1);
   834 qed "MPair_eq_HPair";
   770 qed "MPair_eq_HPair";
   835 
   771 
   836 goalw thy [HPair_def] "(HPair X Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   772 goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   837 by (Auto_tac());
   773 by (Auto_tac());
   838 qed "HPair_eq_MPair";
   774 qed "HPair_eq_MPair";
   839 
   775 
   840 AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
   776 AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
   841 
   777 
   842 
   778 
   843 (*** Specialized laws, proved in terms of those for Hash and MPair ***)
   779 (*** Specialized laws, proved in terms of those for Hash and MPair ***)
   844 
   780 
   845 goalw thy [HPair_def] "keysFor (insert (HPair X Y) H) = keysFor H";
   781 goalw thy [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
   846 by (Simp_tac 1);
   782 by (Simp_tac 1);
   847 qed "keysFor_insert_HPair";
   783 qed "keysFor_insert_HPair";
   848 
   784 
   849 goalw thy [HPair_def]
   785 goalw thy [HPair_def]
   850     "parts (insert (HPair X Y) H) = \
   786     "parts (insert (Hash[X] Y) H) = \
   851 \    insert (HPair X Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
   787 \    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
   852 by (Simp_tac 1);
   788 by (Simp_tac 1);
   853 qed "parts_insert_HPair";
   789 qed "parts_insert_HPair";
   854 
   790 
   855 goalw thy [HPair_def]
   791 goalw thy [HPair_def]
   856     "analz (insert (HPair X Y) H) = \
   792     "analz (insert (Hash[X] Y) H) = \
   857 \    insert (HPair X Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
   793 \    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
   858 by (Simp_tac 1);
   794 by (Simp_tac 1);
   859 qed "analz_insert_HPair";
   795 qed "analz_insert_HPair";
   860 
   796 
   861 goalw thy [HPair_def] "!!H. X ~: synth (analz H) \
   797 goalw thy [HPair_def] "!!H. X ~: synth (analz H) \
   862 \   ==> (HPair X Y : synth (analz H)) = \
   798 \   ==> (Hash[X] Y : synth (analz H)) = \
   863 \       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
   799 \       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
   864 by (Simp_tac 1);
   800 by (Simp_tac 1);
   865 by (Fast_tac 1);
   801 by (Fast_tac 1);
   866 qed "HPair_synth_analz";
   802 qed "HPair_synth_analz";
   867 
   803 
   868 Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 
   804 Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 
   869 	  HPair_synth_analz, HPair_synth_analz];
   805           HPair_synth_analz, HPair_synth_analz];
   870 
   806 
   871 
   807 
   872 (*We do NOT want Crypt... messages broken up in protocols!!*)
   808 (*We do NOT want Crypt... messages broken up in protocols!!*)
   873 Delrules partsEs;
   809 Delrules partsEs;
   874 
   810 
   879 fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
   815 fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
   880                           insert_commute;
   816                           insert_commute;
   881 
   817 
   882 val pushKeys = map (insComm thy "Key ?K") 
   818 val pushKeys = map (insComm thy "Key ?K") 
   883                    ["Agent ?C", "Nonce ?N", "Hash ?X", 
   819                    ["Agent ?C", "Nonce ?N", "Hash ?X", 
   884 		    "MPair ?X ?Y", "Crypt ?X ?K'"];
   820                     "MPair ?X ?Y", "Crypt ?X ?K'"];
   885 
   821 
   886 val pushCrypts = map (insComm thy "Crypt ?X ?K") 
   822 val pushCrypts = map (insComm thy "Crypt ?X ?K") 
   887                      ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
   823                      ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
   888 
   824 
   889 (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   825 (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   896     match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
   832     match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
   897     ORELSE' etac FalseE;
   833     ORELSE' etac FalseE;
   898 
   834 
   899 val Fake_insert_tac = 
   835 val Fake_insert_tac = 
   900     dresolve_tac [impOfSubs Fake_analz_insert,
   836     dresolve_tac [impOfSubs Fake_analz_insert,
   901 		  impOfSubs Fake_parts_insert] THEN'
   837                   impOfSubs Fake_parts_insert] THEN'
   902     eresolve_tac [asm_rl, synth.Inj];
   838     eresolve_tac [asm_rl, synth.Inj];
   903 
   839 
   904 (*Analysis of Fake cases and of messages that forward unknown parts.
   840 (*Analysis of Fake cases and of messages that forward unknown parts.
   905   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   841   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   906   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   842   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   914        (*...allowing further simplifications*)
   850        (*...allowing further simplifications*)
   915        simp_tac (!simpset setloop split_tac [expand_if]) 1,
   851        simp_tac (!simpset setloop split_tac [expand_if]) 1,
   916        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
   852        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
   917        DEPTH_SOLVE 
   853        DEPTH_SOLVE 
   918          (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
   854          (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
   919 	  THEN
   855           THEN
   920 	  IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
   856           IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
   921 						 impOfSubs analz_subset_parts]) 2 1))
   857                                                  impOfSubs analz_subset_parts]) 2 1))
   922        ]) i);
   858        ]) i);
   923 
   859 
   924 (** Useful in many uniqueness proofs **)
   860 (** Useful in many uniqueness proofs **)
   925 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
   861 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
   926                      assume_tac (i+1);
   862                      assume_tac (i+1);
   927 
   863 
   928 (*Apply the EX-ALL quantifification to prove uniqueness theorems in 
   864 (*Apply the EX-ALL quantifification to prove uniqueness theorems in 
   929   their standard form*)
   865   their standard form*)
   930 fun prove_unique_tac lemma = 
   866 fun prove_unique_tac lemma = 
   931   EVERY' [dtac lemma,
   867   EVERY' [dtac lemma,
   932 	  REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
   868           REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
   933 	  (*Duplicate the assumption*)
   869           (*Duplicate the assumption*)
   934 	  forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
   870           forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
   935 	  fast_tac (!claset addSDs [spec])];
   871           fast_tac (!claset addSDs [spec])];
   936 
   872 
   937 
   873 
   938 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   874 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   939 goal Set.thy "A Un (B Un A) = B Un A";
   875 goal Set.thy "A Un (B Un A) = B Un A";
   940 by (Fast_tac 1);
   876 by (Fast_tac 1);