src/HOL/Metis_Examples/Message.thy
 changeset 36911 0e2818493775 parent 36580 d23a3a4d1849 child 39260 f94c53d9b8fb
equal 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"`
`   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))"`