--- a/src/HOL/MetisExamples/Message.thy Tue Oct 14 15:45:46 2008 +0200
+++ b/src/HOL/MetisExamples/Message.thy Tue Oct 14 16:01:36 2008 +0200
@@ -78,7 +78,7 @@
| 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)
@@ -102,7 +102,7 @@
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)
@@ -203,7 +203,7 @@
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)
@@ -240,7 +240,7 @@
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)
@@ -251,7 +251,7 @@
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)
@@ -316,7 +316,7 @@
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)
@@ -368,7 +368,7 @@
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)
@@ -520,7 +520,7 @@
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
@@ -538,7 +538,7 @@
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')"
@@ -616,7 +616,7 @@
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)
@@ -638,7 +638,7 @@
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)
@@ -670,7 +670,7 @@
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)
@@ -685,14 +685,14 @@
-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)
@@ -706,7 +706,7 @@
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"
@@ -729,7 +729,7 @@
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"
@@ -748,7 +748,7 @@
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"
@@ -791,14 +791,14 @@
==> 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) ==>