# HG changeset patch # User huffman # Date 1267591421 28800 # Node ID 743e8ca36b18bc8314b3bebda5ca539155141d93 # Parent 60647586b1732f09bfb1d7240c71ec4e545fdc05# Parent 99b3fce7e475fcc94f2604962cd803c7f3b0ee92 merged diff -r 60647586b173 -r 743e8ca36b18 doc-src/TutorialI/Protocol/NS_Public.thy --- 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) \Nonce NA, Agent A\)"} may be extended by an event of the form @{term [display,indent=5] "Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\)"} -where @{text NB} is a fresh nonce: @{term "Nonce NB \ used evs2"}. +where @{text NB} is a fresh nonce: @{term "Nonce NB \ 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 diff -r 60647586b173 -r 743e8ca36b18 doc-src/TutorialI/Protocol/document/NS_Public.tex --- 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 diff -r 60647586b173 -r 743e8ca36b18 src/HOL/IsaMakefile --- 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 diff -r 60647586b173 -r 743e8ca36b18 src/HOL/List.thy --- 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 diff -r 60647586b173 -r 743e8ca36b18 src/HOL/ZF/HOLZF.thy --- 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) diff -r 60647586b173 -r 743e8ca36b18 src/HOL/ZF/Helper.thy --- 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 \ (!! x. P x \ Q x) \ 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 \ range f & z \ (f ` x)) = (z \ f ` x)" - by auto - -lemma f_x_in_range_f: "f x \ range f" - by (blast intro: image_eqI) - -lemma comp_inj: "inj f \ inj g \ 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 diff -r 60647586b173 -r 743e8ca36b18 src/HOL/ZF/Zet.thy --- 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 \ 'a zet \ 'a zet" where diff -r 60647586b173 -r 743e8ca36b18 src/Tools/nbe.ML --- 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 *)