# HG changeset patch # User haftmann # Date 1285831867 -7200 # Node ID 9e59b4c11039d9dd38c8e0e256065eb3969f5ada # Parent 51451d73c3d4cc7f49dfbc599056752ada3e43e7 updated files to recent changes diff -r 51451d73c3d4 -r 9e59b4c11039 doc-src/TutorialI/Datatype/Nested.thy --- a/doc-src/TutorialI/Datatype/Nested.thy Thu Sep 30 08:50:45 2010 +0200 +++ b/doc-src/TutorialI/Datatype/Nested.thy Thu Sep 30 09:31:07 2010 +0200 @@ -111,14 +111,13 @@ (* Exercise 2: *) -consts trev :: "('v,'f) term \ ('v,'f) term" - trevs:: "('v,'f) term list \ ('v,'f) term list" -primrec -"trev (Var v) = Var v" -"trev (App f ts) = App f (trevs ts)" - -"trevs [] = []" -"trevs (t#ts) = (trevs ts) @ [(trev t)]" +primrec trev :: "('v,'f) term \ ('v,'f) term" + and trevs:: "('v,'f) term list \ ('v,'f) term list" +where + "trev (Var v) = Var v" +| "trev (App f ts) = App f (trevs ts)" +| "trevs [] = []" +| "trevs (t#ts) = (trevs ts) @ [(trev t)]" lemma [simp]: "\ ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)" apply (induct_tac xs, auto) diff -r 51451d73c3d4 -r 9e59b4c11039 doc-src/TutorialI/Inductive/Advanced.thy --- a/doc-src/TutorialI/Inductive/Advanced.thy Thu Sep 30 08:50:45 2010 +0200 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Thu Sep 30 09:31:07 2010 +0200 @@ -1,4 +1,3 @@ -(* ID: $Id$ *) (*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*) text {* @@ -360,11 +359,12 @@ (*<*) text{*the following declaration isn't actually used*} -consts integer_arity :: "integer_op \ nat" primrec -"integer_arity (Number n) = 0" -"integer_arity UnaryMinus = 1" -"integer_arity Plus = 2" + integer_arity :: "integer_op \ nat" +where + "integer_arity (Number n) = 0" +| "integer_arity UnaryMinus = 1" +| "integer_arity Plus = 2" text{* the rest isn't used: too complicated. OK for an exercise though.*} diff -r 51451d73c3d4 -r 9e59b4c11039 doc-src/TutorialI/Protocol/Event.thy --- a/doc-src/TutorialI/Protocol/Event.thy Thu Sep 30 08:50:45 2010 +0200 +++ b/doc-src/TutorialI/Protocol/Event.thy Thu Sep 30 09:31:07 2010 +0200 @@ -23,24 +23,15 @@ consts bad :: "agent set" -- {* compromised agents *} - knows :: "agent => event list => msg set" text{*The constant "spies" is retained for compatibility's sake*} -abbreviation (input) - spies :: "event list => msg set" where - "spies == knows Spy" - -text{*Spy has access to his own key for spoof messages, but Server is secure*} -specification (bad) - Spy_in_bad [iff]: "Spy \ bad" - Server_not_bad [iff]: "Server \ bad" - by (rule exI [of _ "{Spy}"], simp) - primrec + knows :: "agent => event list => msg set" +where knows_Nil: "knows A [] = initState A" - knows_Cons: +| knows_Cons: "knows A (ev # evs) = (if A = Spy then (case ev of @@ -57,20 +48,29 @@ | Notes A' X => if A'=A then insert X (knows A evs) else knows A evs))" +abbreviation (input) + spies :: "event list => msg set" where + "spies == knows Spy" + +text{*Spy has access to his own key for spoof messages, but Server is secure*} +specification (bad) + Spy_in_bad [iff]: "Spy \ bad" + Server_not_bad [iff]: "Server \ bad" + by (rule exI [of _ "{Spy}"], simp) + (* Case A=Spy on the Gets event enforces the fact that if a message is received then it must have been sent, therefore the oops case must use Notes *) -consts +primrec (*Set of items that might be visible to somebody: complement of the set of fresh items*) used :: "event list => msg set" - -primrec +where used_Nil: "used [] = (UN B. parts (initState B))" - used_Cons: "used (ev # evs) = +| used_Cons: "used (ev # evs) = (case ev of Says A B X => parts {X} \ used evs | Gets A X => used evs diff -r 51451d73c3d4 -r 9e59b4c11039 doc-src/TutorialI/Protocol/Public.thy --- a/doc-src/TutorialI/Protocol/Public.thy Thu Sep 30 08:50:45 2010 +0200 +++ b/doc-src/TutorialI/Protocol/Public.thy Thu Sep 30 09:31:07 2010 +0200 @@ -22,14 +22,19 @@ abbreviation priK :: "agent \ key" where "priK x \ invKey(pubK x)" (*<*) -primrec +overloading initState \ initState +begin + +primrec initState where (*Agents know their private key and all public keys*) initState_Server: "initState Server = insert (Key (priK Server)) (Key ` range pubK)" - initState_Friend: "initState (Friend i) = +| initState_Friend: "initState (Friend i) = insert (Key (priK (Friend i))) (Key ` range pubK)" - initState_Spy: "initState Spy = +| initState_Spy: "initState Spy = (Key`invKey`pubK`bad) Un (Key ` range pubK)" + +end (*>*) text {* diff -r 51451d73c3d4 -r 9e59b4c11039 doc-src/TutorialI/Sets/Examples.thy --- a/doc-src/TutorialI/Sets/Examples.thy Thu Sep 30 08:50:45 2010 +0200 +++ b/doc-src/TutorialI/Sets/Examples.thy Thu Sep 30 09:31:07 2010 +0200 @@ -95,8 +95,8 @@ text{* set extensionality -@{thm[display] set_ext[no_vars]} -\rulename{set_ext} +@{thm[display] set_eqI[no_vars]} +\rulename{set_eqI} @{thm[display] equalityI[no_vars]} \rulename{equalityI} diff -r 51451d73c3d4 -r 9e59b4c11039 doc-src/TutorialI/Sets/Functions.thy --- a/doc-src/TutorialI/Sets/Functions.thy Thu Sep 30 08:50:45 2010 +0200 +++ b/doc-src/TutorialI/Sets/Functions.thy Thu Sep 30 09:31:07 2010 +0200 @@ -66,20 +66,18 @@ \rulename{o_inv_distrib} *} - - text{* small sample proof @{thm[display] ext[no_vars]} \rulename{ext} -@{thm[display] expand_fun_eq[no_vars]} -\rulename{expand_fun_eq} +@{thm[display] fun_eq_iff[no_vars]} +\rulename{fun_eq_iff} *} lemma "inj f \ (f o g = f o h) = (g = h)"; - apply (simp add: expand_fun_eq inj_on_def) + apply (simp add: fun_eq_iff inj_on_def) apply (auto) done