src/HOL/Metis_Examples/Message.thy
changeset 36911 0e2818493775
parent 36580 d23a3a4d1849
child 39260 f94c53d9b8fb
equal deleted inserted replaced
36910:dd5a31098f85 36911:0e2818493775
     7 theory Message
     7 theory Message
     8 imports Main
     8 imports Main
     9 begin
     9 begin
    10 
    10 
    11 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
    11 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
    12 by (metis Un_ac(2) Un_ac(3))
    12 by (metis Un_commute Un_left_absorb)
    13 
    13 
    14 types 
    14 types 
    15   key = nat
    15   key = nat
    16 
    16 
    17 consts
    17 consts
   679 apply blast
   679 apply blast
   680 done
   680 done
   681 
   681 
   682 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   682 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   683 proof -
   683 proof -
   684   have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)"
   684   have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)" by (metis Un_commute analz_synth_Un)
   685     by (metis Un_commute analz_synth_Un)
   685   hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> {})" by (metis Un_empty_right)
   686   hence "\<forall>x\<^isub>3 x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> UNION {} x\<^isub>3)"
   686   hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)" by (metis Un_empty_right)
   687     by (metis UN_extend_simps(3))
   687   hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)" by (metis Un_commute)
   688   hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)"
       
   689     by (metis UN_extend_simps(3))
       
   690   hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)"
       
   691     by (metis Un_commute)
       
   692   thus "analz (synth H) = analz H \<union> synth H" by metis
   688   thus "analz (synth H) = analz H \<union> synth H" by metis
   693 qed
   689 qed
   694 
   690 
   695 
   691 
   696 subsubsection{*For reasoning about the Fake rule in traces *}
   692 subsubsection{*For reasoning about the Fake rule in traces *}
   697 
   693 
   698 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   694 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
   699 proof -
   695 proof -
   700   assume "X \<in> G"
   696   assume "X \<in> G"
   701   hence "\<forall>u. X \<in> G \<union> u" by (metis Un_iff)
   697   hence "G X" by (metis mem_def)
   702   hence "X \<in> G \<union> H \<and> H \<subseteq> G \<union> H"
   698   hence "\<forall>x\<^isub>1. G \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 X" by (metis predicate1D)
   703     by (metis Un_upper2)
   699   hence "\<forall>x\<^isub>1. (G \<union> x\<^isub>1) X" by (metis Un_upper1)
   704   hence "insert X H \<subseteq> G \<union> H" by (metis insert_subset)
   700   hence "\<forall>x\<^isub>1. X \<in> G \<union> x\<^isub>1" by (metis mem_def)
   705   hence "parts (insert X H) \<subseteq> parts (G \<union> H)"
   701   hence "insert X H \<subseteq> G \<union> H" by (metis Un_upper2 insert_subset)
   706     by (metis parts_mono)
   702   hence "parts (insert X H) \<subseteq> parts (G \<union> H)" by (metis parts_mono)
   707   thus "parts (insert X H) \<subseteq> parts G \<union> parts H"
   703   thus "parts (insert X H) \<subseteq> parts G \<union> parts H" by (metis parts_Un)
   708     by (metis parts_Un)
       
   709 qed
   704 qed
   710 
   705 
   711 lemma Fake_parts_insert:
   706 lemma Fake_parts_insert:
   712      "X \<in> synth (analz H) ==>  
   707      "X \<in> synth (analz H) ==>  
   713       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   708       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
   714 (*sledgehammer*)
       
   715 proof -
   709 proof -
   716   assume A1: "X \<in> synth (analz H)"
   710   assume A1: "X \<in> synth (analz H)"
   717   have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"
   711   have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"
   718     by (metis analz_idem analz_synth)
   712     by (metis analz_idem analz_synth)
   719   have F2: "\<forall>x\<^isub>1. parts x\<^isub>1 \<union> synth (analz x\<^isub>1) = parts (synth (analz x\<^isub>1))"
   713   have F2: "\<forall>x\<^isub>1. parts x\<^isub>1 \<union> synth (analz x\<^isub>1) = parts (synth (analz x\<^isub>1))"