src/HOL/MetisExamples/Message.thy

   | Fst:         "{|X,Y|}   \<in> parts H ==> X \<in> parts H"
   | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
 
-ML{*AtpThread.problem_name := "Message__parts_mono"*}
+ML{*AtpWrapper.problem_name := "Message__parts_mono"*}
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct) 
 apply (metis Inj set_mp)
 apply (metis Fst)

 by auto
 
 
 subsubsection{*Inverse of keys *}
 
-ML{*AtpThread.problem_name := "Message__invKey_eq"*}
+ML{*AtpWrapper.problem_name := "Message__invKey_eq"*}
 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
 by (metis invKey)
 
 
 subsection{*keysFor operator*}

 lemma parts_insert: "parts (insert X H) = parts {X} \<union> parts H"
 apply (subst insert_is_Un [of _ H])
 apply (simp only: parts_Un)
 done
 
-ML{*AtpThread.problem_name := "Message__parts_insert_two"*}
+ML{*AtpWrapper.problem_name := "Message__parts_insert_two"*}
 lemma parts_insert2:
      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
 
 

 by (erule parts.induct, blast+)
 
 lemma parts_idem [simp]: "parts (parts H) = parts H"
 by blast
 
-ML{*AtpThread.problem_name := "Message__parts_subset_iff"*}
+ML{*AtpWrapper.problem_name := "Message__parts_subset_iff"*}
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
 apply (rule iffI) 
 apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
 apply (metis parts_idem parts_mono)
 done
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
 by (blast dest: parts_mono); 
 
 
-ML{*AtpThread.problem_name := "Message__parts_cut"*}
+ML{*AtpWrapper.problem_name := "Message__parts_cut"*}
 lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
 by (metis Un_subset_iff insert_subset parts_increasing parts_trans) 
 
 
 

 apply auto
 apply (erule parts.induct, auto)
 done
 
 
-ML{*AtpThread.problem_name := "Message__msg_Nonce_supply"*}
+ML{*AtpWrapper.problem_name := "Message__msg_Nonce_supply"*}
 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
 apply (induct_tac "msg") 
 apply (simp_all add: parts_insert2)
 apply (metis Suc_n_not_le_n)
 apply (metis le_trans linorder_linear)

 lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
 
 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
 
 
-ML{*AtpThread.problem_name := "Message__parts_analz"*}
+ML{*AtpWrapper.problem_name := "Message__parts_analz"*}
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 apply (rule equalityI)
 apply (metis analz_subset_parts parts_subset_iff)
 apply (metis analz_increasing parts_mono)
 done

 
 lemma analz_trans: "[| X\<in> analz G;  G \<subseteq> analz H |] ==> X\<in> analz H"
 by (drule analz_mono, blast)
 
 
-ML{*AtpThread.problem_name := "Message__analz_cut"*}
+ML{*AtpWrapper.problem_name := "Message__analz_cut"*}
     declare analz_trans[intro]
 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
 (*TOO SLOW
 by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
 ??*)

 by (blast intro: analz_cut analz_insertI)
 
 
 text{*A congruence rule for "analz" *}
 
-ML{*AtpThread.problem_name := "Message__analz_subset_cong"*}
+ML{*AtpWrapper.problem_name := "Message__analz_subset_cong"*}
 lemma analz_subset_cong:
      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
 apply simp
 apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono)

   separate parts, building a compound message using elements of each.*}
 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
 
 
-ML{*AtpThread.problem_name := "Message__synth_insert"*}
+ML{*AtpWrapper.problem_name := "Message__synth_insert"*}
  
 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
 by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
 
 subsubsection{*Idempotence and transitivity *}

 done
 
 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
 by (drule synth_mono, blast)
 
-ML{*AtpThread.problem_name := "Message__synth_cut"*}
+ML{*AtpWrapper.problem_name := "Message__synth_cut"*}
 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
 (*TOO SLOW
 by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
 *)
 by (erule synth_trans, blast)

 by (unfold keysFor_def, blast)
 
 
 subsubsection{*Combinations of parts, analz and synth *}
 
-ML{*AtpThread.problem_name := "Message__parts_synth"*}
+ML{*AtpWrapper.problem_name := "Message__parts_synth"*}
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule parts.induct)
 apply (metis UnCI)

 done
 
 
 
 
-ML{*AtpThread.problem_name := "Message__analz_analz_Un"*}
+ML{*AtpWrapper.problem_name := "Message__analz_analz_Un"*}
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
 apply (rule equalityI);
 apply (metis analz_idem analz_subset_cong order_eq_refl)
 apply (metis analz_increasing analz_subset_cong order_eq_refl)
 done
 
-ML{*AtpThread.problem_name := "Message__analz_synth_Un"*}
+ML{*AtpWrapper.problem_name := "Message__analz_synth_Un"*}
     declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
 apply (rule equalityI)
 apply (rule subsetI)
 apply (erule analz.induct)

 apply (blast intro: analz.Decrypt)
 apply blast
 done
 
 
-ML{*AtpThread.problem_name := "Message__analz_synth"*}
+ML{*AtpWrapper.problem_name := "Message__analz_synth"*}
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
 proof (neg_clausify)
 assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
 have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
   by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)

 qed
 
 
 subsubsection{*For reasoning about the Fake rule in traces *}
 
-ML{*AtpThread.problem_name := "Message__parts_insert_subset_Un"*}
+ML{*AtpWrapper.problem_name := "Message__parts_insert_subset_Un"*}
 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
 proof (neg_clausify)
 assume 0: "X \<in> G"
 assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"
 have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"

   by (metis 5 UnCI)
 show "False"
   by (metis 6 0)
 qed
 
-ML{*AtpThread.problem_name := "Message__Fake_parts_insert"*}
+ML{*AtpWrapper.problem_name := "Message__Fake_parts_insert"*}
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>  
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
 proof (neg_clausify)
 assume 0: "X \<in> synth (analz H)"

 lemma Fake_parts_insert_in_Un:
      "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
       ==> Z \<in>  synth (analz H) \<union> parts H";
 by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
 
-ML{*AtpThread.problem_name := "Message__Fake_analz_insert"*}
+ML{*AtpWrapper.problem_name := "Message__Fake_analz_insert"*}
     declare analz_mono [intro] synth_mono [intro] 
 lemma Fake_analz_insert:
      "X\<in> synth (analz G) ==>  
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un analz_mono analz_synth_Un equalityE insert_absorb order_le_less xt1(12))
 
-ML{*AtpThread.problem_name := "Message__Fake_analz_insert_simpler"*}
+ML{*AtpWrapper.problem_name := "Message__Fake_analz_insert_simpler"*}
 (*simpler problems?  BUT METIS CAN'T PROVE
 lemma Fake_analz_insert_simpler:
      "X\<in> synth (analz G) ==>  
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 apply (rule subsetI)