--- a/doc-src/TutorialI/Protocol/NS_Public.thy Tue Mar 02 20:36:07 2010 -0800
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy Tue Mar 02 20:43:41 2010 -0800
@@ -76,7 +76,7 @@
@{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"}
may be extended by an event of the form
@{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"}
-where @{text NB} is a fresh nonce: @{term "Nonce NB \<in> used evs2"}.
+where @{text NB} is a fresh nonce: @{term "Nonce NB \<notin> used evs2"}.
Writing the sender as @{text A'} indicates that @{text B} does not
know who sent the message. Calling the trace variable @{text evs2} rather
than simply @{text evs} helps us know where we are in a proof after many
--- a/doc-src/TutorialI/Protocol/document/NS_Public.tex Tue Mar 02 20:36:07 2010 -0800
+++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex Tue Mar 02 20:43:41 2010 -0800
@@ -84,7 +84,7 @@
\begin{isabelle}%
\ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}%
\end{isabelle}
-where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}.
+where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}}.
Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not
know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather
than simply \isa{evs} helps us know where we are in a proof after many
--- a/src/HOL/IsaMakefile Tue Mar 02 20:36:07 2010 -0800
+++ b/src/HOL/IsaMakefile Tue Mar 02 20:43:41 2010 -0800
@@ -756,7 +756,7 @@
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
-$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy \
+$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
--- a/src/HOL/List.thy Tue Mar 02 20:36:07 2010 -0800
+++ b/src/HOL/List.thy Tue Mar 02 20:43:41 2010 -0800
@@ -761,13 +761,13 @@
by(induct ys, auto simp add: Cons_eq_map_conv)
lemma map_eq_imp_length_eq:
- assumes "map f xs = map f ys"
+ assumes "map f xs = map g ys"
shows "length xs = length ys"
using assms proof (induct ys arbitrary: xs)
case Nil then show ?case by simp
next
case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
- from Cons xs have "map f zs = map f ys" by simp
+ from Cons xs have "map f zs = map g ys" by simp
moreover with Cons have "length zs = length ys" by blast
with xs show ?case by simp
qed
--- a/src/HOL/ZF/HOLZF.thy Tue Mar 02 20:36:07 2010 -0800
+++ b/src/HOL/ZF/HOLZF.thy Tue Mar 02 20:43:41 2010 -0800
@@ -6,7 +6,7 @@
*)
theory HOLZF
-imports Helper
+imports Main
begin
typedecl ZF
@@ -298,7 +298,7 @@
apply (rule_tac x="Fst z" in exI)
apply (simp add: isOpair_def)
apply (auto simp add: Fst Snd Opair)
- apply (rule theI2')
+ apply (rule the1I2)
apply auto
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair x ya" and y="Opair x yb" in PFun_inj)
@@ -306,7 +306,7 @@
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair x y" and y="Opair x ya" in PFun_inj)
apply (auto simp add: Fst Snd)
- apply (rule theI2')
+ apply (rule the1I2)
apply (auto simp add: Fun_total)
apply (drule Fun_implies_PFun)
apply (drule_tac x="Opair a x" and y="Opair a y" in PFun_inj)
--- a/src/HOL/ZF/Helper.thy Tue Mar 02 20:36:07 2010 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: HOL/ZF/Helper.thy
- ID: $Id$
- Author: Steven Obua
-
- Some helpful lemmas that probably will end up elsewhere.
-*)
-
-theory Helper
-imports Main
-begin
-
-lemma theI2' : "?! x. P x \<Longrightarrow> (!! x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (THE x. P x)"
- apply auto
- apply (subgoal_tac "P (THE x. P x)")
- apply blast
- apply (rule theI)
- apply auto
- done
-
-lemma in_range_superfluous: "(z \<in> range f & z \<in> (f ` x)) = (z \<in> f ` x)"
- by auto
-
-lemma f_x_in_range_f: "f x \<in> range f"
- by (blast intro: image_eqI)
-
-lemma comp_inj: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (g o f)"
- by (blast intro: comp_inj_on subset_inj_on)
-
-lemma comp_image_eq: "(g o f) ` x = g ` f ` x"
- by auto
-
-end
\ No newline at end of file
--- a/src/HOL/ZF/Zet.thy Tue Mar 02 20:36:07 2010 -0800
+++ b/src/HOL/ZF/Zet.thy Tue Mar 02 20:43:41 2010 -0800
@@ -35,7 +35,7 @@
apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
apply (simp add: explode_Repl_eq)
apply (subgoal_tac "explode z = f ` A")
- apply (simp_all add: comp_image_eq)
+ apply (simp_all add: image_compose)
done
lemma zet_image_mem:
@@ -56,7 +56,7 @@
apply (auto simp add: subset injf)
done
show ?thesis
- apply (simp add: zet_def' comp_image_eq[symmetric])
+ apply (simp add: zet_def' image_compose[symmetric])
apply (rule exI[where x="?w"])
apply (simp add: injw image_zet_rep Azet)
done
@@ -108,7 +108,7 @@
lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
apply (simp add: zimage_def)
apply (subst Abs_zet_inverse)
- apply (simp_all add: comp_image_eq zet_image_mem Rep_zet)
+ apply (simp_all add: image_compose zet_image_mem Rep_zet)
done
definition zunion :: "'a zet \<Rightarrow> 'a zet \<Rightarrow> 'a zet" where
--- a/src/Tools/nbe.ML Tue Mar 02 20:36:07 2010 -0800
+++ b/src/Tools/nbe.ML Tue Mar 02 20:43:41 2010 -0800
@@ -235,7 +235,7 @@
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
fun nbe_bound v = "v_" ^ v;
fun nbe_bound_optional NONE = "_"
- | nbe_bound_optional (SOME v) = nbe_bound v;
+ | nbe_bound_optional (SOME v) = nbe_bound v;
fun nbe_default v = "w_" ^ v;
(*note: these three are the "turning spots" where proper argument order is established!*)
@@ -434,7 +434,7 @@
#-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
end;
-fun ensure_stmts ctxt naming program =
+fun ensure_stmts ctxt program =
let
fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
then (gr, (maxidx, idx_tab))
@@ -443,7 +443,6 @@
Graph.imm_succs program name)) names);
in
fold_rev add_stmts (Graph.strong_conn program)
- #> pair naming
end;
@@ -513,18 +512,18 @@
structure Nbe_Functions = Code_Data
(
- type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table));
- val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));
+ type T = (Univ option * int) Graph.T * (int * string Inttab.table);
+ val empty = (Graph.empty, (0, Inttab.empty));
);
(* compilation, evaluation and reification *)
-fun compile_eval thy naming program vs_t deps =
+fun compile_eval thy program vs_t deps =
let
val ctxt = ProofContext.init thy;
- val (_, (gr, (_, idx_tab))) =
- Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
+ val (gr, (_, idx_tab)) =
+ Nbe_Functions.change thy (ensure_stmts ctxt program);
in
vs_t
|> eval_term ctxt gr deps
@@ -534,7 +533,7 @@
(* evaluation with type reconstruction *)
-fun normalize thy naming program ((vs0, (vs, ty)), t) deps =
+fun normalize thy program ((vs0, (vs, ty)), t) deps =
let
val ty' = typ_of_itype program vs0 ty;
fun type_infer t =
@@ -546,7 +545,7 @@
^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
in
- compile_eval thy naming program (vs, t) deps
+ compile_eval thy program (vs, t) deps
|> traced (fn t => "Normalized:\n" ^ string_of_term t)
|> type_infer
|> traced (fn t => "Types inferred:\n" ^ string_of_term t)
@@ -565,11 +564,11 @@
in Thm.mk_binop eq lhs rhs end;
val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_t, deps, ct) =>
- mk_equals thy ct (normalize thy naming program vsp_ty_t deps))));
+ (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
+ mk_equals thy ct (normalize thy program vsp_ty_t deps))));
-fun norm_oracle thy naming program vsp_ty_t deps ct =
- raw_norm_oracle (thy, naming, program, vsp_ty_t, deps, ct);
+fun norm_oracle thy program vsp_ty_t deps ct =
+ raw_norm_oracle (thy, program, vsp_ty_t, deps, ct);
fun no_frees_conv conv ct =
let
@@ -597,9 +596,9 @@
val norm_conv = no_frees_conv (fn ct =>
let
val thy = Thm.theory_of_cterm ct;
- in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (norm_oracle thy)) ct end);
+ in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (K (norm_oracle thy))) ct end);
-fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (normalize thy)));
+fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (K (normalize thy))));
(* evaluation command *)