# HG changeset patch # User berghofe # Date 1184145291 -7200 # Node ID a455e69c31cc8a44cd983a03e6ae623239f2acfc # Parent 28df61d931e25669d720afc1521392a2e3679ed0 Adapted to new inductive definition package. diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Algebra/FiniteProduct.thy Wed Jul 11 11:14:51 2007 +0200 @@ -18,13 +18,12 @@ @{text "x \ carrier G"}. We introduce an explicit argument for the domain @{text D}. *} -consts +inductive_set foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" - -inductive "foldSetD D f e" - intros + for D :: "'a set" and f :: "'b => 'a => 'a" and e :: 'a + where emptyI [intro]: "e \ D ==> ({}, e) \ foldSetD D f e" - insertI [intro]: "[| x ~: A; f x y \ D; (A, y) \ foldSetD D f e |] ==> + | insertI [intro]: "[| x ~: A; f x y \ D; (A, y) \ foldSetD D f e |] ==> (insert x A, f x y) \ foldSetD D f e" inductive_cases empty_foldSetDE [elim!]: "({}, x) \ foldSetD D f e" @@ -36,7 +35,7 @@ lemma foldSetD_closed: "[| (A, z) \ foldSetD D f e ; e \ D; !!x y. [| x \ A; y \ D |] ==> f x y \ D |] ==> z \ D"; - by (erule foldSetD.elims) auto + by (erule foldSetD.cases) auto lemma Diff1_foldSetD: "[| (A - {x}, y) \ foldSetD D f e; x \ A; f x y \ D |] ==> @@ -75,7 +74,7 @@ lemma (in LCD) foldSetD_closed [dest]: "(A, z) \ foldSetD D f e ==> z \ D"; - by (erule foldSetD.elims) auto + by (erule foldSetD.cases) auto lemma (in LCD) Diff1_foldSetD: "[| (A - {x}, y) \ foldSetD D f e; x \ A; A \ B |] ==> @@ -117,7 +116,7 @@ apply (erule rev_mp) apply (simp add: less_Suc_eq_le) apply (rule impI) - apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb") + apply (rename_tac xa Aa ya xb Ab yb, case_tac "xa = xb") apply (subgoal_tac "Aa = Ab") prefer 2 apply (blast elim!: equalityE) apply blast diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/CertifiedEmail.thy --- a/src/HOL/Auth/CertifiedEmail.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/CertifiedEmail.thy Wed Jul 11 11:14:51 2007 +0200 @@ -30,24 +30,23 @@ "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}" -consts certified_mail :: "event list set" -inductive "certified_mail" - intros +inductive_set certified_mail :: "event list set" + where -Nil: --{*The empty trace*} + Nil: --{*The empty trace*} "[] \ certified_mail" -Fake: --{*The Spy may say anything he can say. The sender field is correct, +| Fake: --{*The Spy may say anything he can say. The sender field is correct, but agents don't use that information.*} "[| evsf \ certified_mail; X \ synth(analz(spies evsf))|] ==> Says Spy B X # evsf \ certified_mail" -FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent +| FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent equipped with the necessary credentials to serve as an SSL server.*} "[| evsfssl \ certified_mail; X \ synth(analz(spies evsfssl))|] ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \ certified_mail" -CM1: --{*The sender approaches the recipient. The message is a number.*} +| CM1: --{*The sender approaches the recipient. The message is a number.*} "[|evs1 \ certified_mail; Key K \ used evs1; K \ symKeys; @@ -58,7 +57,7 @@ Number cleartext, Nonce q, S2TTP|} # evs1 \ certified_mail" -CM2: --{*The recipient records @{term S2TTP} while transmitting it and her +| CM2: --{*The recipient records @{term S2TTP} while transmitting it and her password to @{term TTP} over an SSL channel.*} "[|evs2 \ certified_mail; Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, @@ -69,7 +68,7 @@ Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2 \ certified_mail" -CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives +| CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives a receipt to the sender. The SSL channel does not authenticate the client (@{term R}), but @{term TTP} accepts the message only if the given password is that of the claimed sender, @{term R}. @@ -84,7 +83,7 @@ Gets S (Crypt (priSK TTP) S2TTP) # Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \ certified_mail" -Reception: +| Reception: "[|evsr \ certified_mail; Says A B X \ set evsr|] ==> Gets B X#evsr \ certified_mail" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/Analz.thy --- a/src/HOL/Auth/Guard/Analz.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/Analz.thy Wed Jul 11 11:14:51 2007 +0200 @@ -18,13 +18,13 @@ subsection{*messages that do not contribute to analz*} -consts pparts :: "msg set => msg set" - -inductive "pparts H" -intros -Inj [intro]: "[| X:H; is_MPair X |] ==> X:pparts H" -Fst [dest]: "[| {|X,Y|}:pparts H; is_MPair X |] ==> X:pparts H" -Snd [dest]: "[| {|X,Y|}:pparts H; is_MPair Y |] ==> Y:pparts H" +inductive_set + pparts :: "msg set => msg set" + for H :: "msg set" +where + Inj [intro]: "[| X:H; is_MPair X |] ==> X:pparts H" +| Fst [dest]: "[| {|X,Y|}:pparts H; is_MPair X |] ==> X:pparts H" +| Snd [dest]: "[| {|X,Y|}:pparts H; is_MPair Y |] ==> Y:pparts H" subsection{*basic facts about @{term pparts}*} @@ -120,13 +120,13 @@ subsection{*messages that contribute to analz*} -consts kparts :: "msg set => msg set" - -inductive "kparts H" -intros -Inj [intro]: "[| X:H; not_MPair X |] ==> X:kparts H" -Fst [intro]: "[| {|X,Y|}:pparts H; not_MPair X |] ==> X:kparts H" -Snd [intro]: "[| {|X,Y|}:pparts H; not_MPair Y |] ==> Y:kparts H" +inductive_set + kparts :: "msg set => msg set" + for H :: "msg set" +where + Inj [intro]: "[| X:H; not_MPair X |] ==> X:kparts H" +| Fst [intro]: "[| {|X,Y|}:pparts H; not_MPair X |] ==> X:kparts H" +| Snd [intro]: "[| {|X,Y|}:pparts H; not_MPair Y |] ==> Y:kparts H" subsection{*basic facts about @{term kparts}*} diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/Guard.thy --- a/src/HOL/Auth/Guard/Guard.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/Guard.thy Wed Jul 11 11:14:51 2007 +0200 @@ -18,14 +18,14 @@ in a sub-message of the form Crypt (invKey K) X with K:Ks ******************************************************************************) -consts guard :: "nat => key set => msg set" - -inductive "guard n Ks" -intros -No_Nonce [intro]: "Nonce n ~:parts {X} ==> X:guard n Ks" -Guard_Nonce [intro]: "invKey K:Ks ==> Crypt K X:guard n Ks" -Crypt [intro]: "X:guard n Ks ==> Crypt K X:guard n Ks" -Pair [intro]: "[| X:guard n Ks; Y:guard n Ks |] ==> {|X,Y|}:guard n Ks" +inductive_set + guard :: "nat => key set => msg set" + for n :: nat and Ks :: "key set" +where + No_Nonce [intro]: "Nonce n ~:parts {X} ==> X:guard n Ks" +| Guard_Nonce [intro]: "invKey K:Ks ==> Crypt K X:guard n Ks" +| Crypt [intro]: "X:guard n Ks ==> Crypt K X:guard n Ks" +| Pair [intro]: "[| X:guard n Ks; Y:guard n Ks |] ==> {|X,Y|}:guard n Ks" subsection{*basic facts about @{term guard}*} @@ -117,7 +117,7 @@ ==> Guard n Ks (analz G)" apply (auto simp: Guard_def) apply (erule analz.induct, auto) -by (ind_cases "Crypt K Xa:guard n Ks", auto) +by (ind_cases "Crypt K Xa:guard n Ks" for K Xa, auto) lemma in_Guard [dest]: "[| X:G; Guard n Ks G |] ==> X:guard n Ks" by (auto simp: Guard_def) diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/GuardK.thy --- a/src/HOL/Auth/Guard/GuardK.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/GuardK.thy Wed Jul 11 11:14:51 2007 +0200 @@ -23,14 +23,14 @@ in a sub-message of the form Crypt (invKey K) X with K:Ks ******************************************************************************) -consts guardK :: "nat => key set => msg set" - -inductive "guardK n Ks" -intros -No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks" -Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks" -Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks" -Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> {|X,Y|}:guardK n Ks" +inductive_set + guardK :: "nat => key set => msg set" + for n :: nat and Ks :: "key set" +where + No_Key [intro]: "Key n ~:parts {X} ==> X:guardK n Ks" +| Guard_Key [intro]: "invKey K:Ks ==> Crypt K X:guardK n Ks" +| Crypt [intro]: "X:guardK n Ks ==> Crypt K X:guardK n Ks" +| Pair [intro]: "[| X:guardK n Ks; Y:guardK n Ks |] ==> {|X,Y|}:guardK n Ks" subsection{*basic facts about @{term guardK}*} @@ -119,7 +119,7 @@ ==> GuardK n Ks (analz G)" apply (auto simp: GuardK_def) apply (erule analz.induct, auto) -by (ind_cases "Crypt K Xa:guardK n Ks", auto) +by (ind_cases "Crypt K Xa:guardK n Ks" for K Xa, auto) lemma in_GuardK [dest]: "[| X:G; GuardK n Ks G |] ==> X:guardK n Ks" by (auto simp: GuardK_def) diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/Guard_NS_Public.thy --- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Wed Jul 11 11:14:51 2007 +0200 @@ -40,22 +40,20 @@ subsection{*definition of the protocol*} -consts nsp :: "event list set" +inductive_set nsp :: "event list set" +where -inductive nsp -intros + Nil: "[]:nsp" -Nil: "[]:nsp" +| Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp" -Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp" - -NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp" +| NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp" -NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==> -ns2 B A NA NB # evs2:nsp" +| NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==> + ns2 B A NA NB # evs2:nsp" -NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==> -ns3 A B NB # evs3:nsp" +| NS3: "!!A B B' NA NB evs3. [| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==> + ns3 A B NB # evs3:nsp" subsection{*declarations for tactics*} @@ -72,7 +70,7 @@ by (auto simp: Gets_correct_def dest: nsp_has_no_Gets) lemma nsp_is_one_step [iff]: "one_step nsp" -by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto) +by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp" for ev evs, auto) lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==> ev:set evs --> (EX A B X. ev=Says A B X)" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/Guard_OtwayRees.thy --- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Wed Jul 11 11:14:51 2007 +0200 @@ -62,25 +62,23 @@ subsection{*definition of the protocol*} -consts or :: "event list set" +inductive_set or :: "event list set" +where -inductive or -intros + Nil: "[]:or" -Nil: "[]:or" +| Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or" -Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or" +| OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or" -OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or" - -OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |] -==> or2 A B NA NB X # evs2:or" +| OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |] + ==> or2 A B NA NB X # evs2:or" -OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |] -==> or3 A B NA NB K # evs3:or" +| OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |] + ==> or3 A B NA NB K # evs3:or" -OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |] -==> or4 A B NA X # evs4:or" +| OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |] + ==> or4 A B NA X # evs4:or" subsection{*declarations for tactics*} @@ -97,7 +95,7 @@ by (auto simp: Gets_correct_def dest: or_has_no_Gets) lemma or_is_one_step [iff]: "one_step or" -by (unfold one_step_def, clarify, ind_cases "ev#evs:or", auto) +by (unfold one_step_def, clarify, ind_cases "ev#evs:or" for ev evs, auto) lemma or_has_only_Says' [rule_format]: "evs:or ==> ev:set evs --> (EX A B X. ev=Says A B X)" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/Guard_Yahalom.thy --- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Jul 11 11:14:51 2007 +0200 @@ -53,25 +53,23 @@ subsection{*definition of the protocol*} -consts ya :: "event list set" +inductive_set ya :: "event list set" +where -inductive ya -intros + Nil: "[]:ya" -Nil: "[]:ya" +| Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya" -Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya" +| YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya" -YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya" - -YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |] -==> ya2 A B NA NB # evs2:ya" +| YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |] + ==> ya2 A B NA NB # evs2:ya" -YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |] -==> ya3 A B NA NB K # evs3:ya" +| YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |] + ==> ya3 A B NA NB K # evs3:ya" -YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |] -==> ya4 A B K NB Y # evs4:ya" +| YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |] + ==> ya4 A B K NB Y # evs4:ya" subsection{*declarations for tactics*} @@ -88,7 +86,7 @@ by (auto simp: Gets_correct_def dest: ya_has_no_Gets) lemma ya_is_one_step [iff]: "one_step ya" -by (unfold one_step_def, clarify, ind_cases "ev#evs:ya", auto) +by (unfold one_step_def, clarify, ind_cases "ev#evs:ya" for ev evs, auto) lemma ya_has_only_Says' [rule_format]: "evs:ya ==> ev:set evs --> (EX A B X. ev=Says A B X)" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/List_Msg.thy --- a/src/HOL/Auth/Guard/List_Msg.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/List_Msg.thy Wed Jul 11 11:14:51 2007 +0200 @@ -137,12 +137,10 @@ nil :: msg where "nil == Number 0" -consts agl :: "msg set" - -inductive agl -intros -Nil[intro]: "nil:agl" -Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl" +inductive_set agl :: "msg set" +where + Nil[intro]: "nil:agl" +| Cons[intro]: "[| A:agent; I:agl |] ==> cons (Agent A) I :agl" subsubsection{*basic facts about agent lists*} diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/P1.thy --- a/src/HOL/Auth/Guard/P1.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/P1.thy Wed Jul 11 11:14:51 2007 +0200 @@ -150,20 +150,18 @@ subsubsection{*protocol*} -consts p1 :: "event list set" +inductive_set p1 :: "event list set" +where -inductive p1 -intros - -Nil: "[]:p1" + Nil: "[]:p1" -Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1" +| Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1" -Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1" +| Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1" -Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; -I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); -Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1" +| Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; + I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); + Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1" subsubsection{*Composition of Traces*} @@ -181,13 +179,13 @@ subsubsection{*Valid Offer Lists*} -consts valid :: "agent => nat => agent => msg set" +inductive_set + valid :: "agent => nat => agent => msg set" + for A :: agent and n :: nat and B :: agent +where + Request [intro]: "cons (anchor A n B) nil:valid A n B" -inductive "valid A n B" -intros -Request [intro]: "cons (anchor A n B) nil:valid A n B" - -Propose [intro]: "L:valid A n B +| Propose [intro]: "L:valid A n B ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" subsubsection{*basic properties of valid*} @@ -284,15 +282,15 @@ apply clarify apply (frule len_not_empty, clarsimp) apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,xa,l'a|}:valid A n B") -apply (ind_cases "{|x,M,l'a|}:valid A n B") +apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a) +apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a) apply (simp add: chain_def) (* i > 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B") +apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na) apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B") +apply (ind_cases "{|x,l'|}:valid A n B" for x l') by (drule_tac x=l' in spec, simp, blast) subsubsection{*insertion resilience: @@ -308,15 +306,15 @@ (* i = 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B", simp) -apply (ind_cases "{|x,M,l'|}:valid A n B", clarsimp) -apply (ind_cases "{|head l',l'|}:valid A n B", simp, simp) +apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp) +apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp) +apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp) (* i > 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B") +apply (ind_cases "{|x,l'|}:valid A n B" for x l') apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B") +apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na) apply (frule len_not_empty, clarsimp) by (drule_tac x=l' in spec, clarsimp) @@ -329,14 +327,14 @@ (* i = 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B") +apply (ind_cases "{|x,l'|}:valid A n B" for x l') apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|M,l'|}:valid A n B") +apply (ind_cases "{|M,l'|}:valid A n B" for l') apply (frule len_not_empty, clarsimp, simp) (* i > 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B") +apply (ind_cases "{|x,l'|}:valid A n B" for x l') apply (frule len_not_empty, clarsimp) by (drule_tac x=l' in spec, clarsimp) @@ -375,7 +373,7 @@ by (auto simp: Gets_correct_def dest: p1_has_no_Gets) lemma p1_is_one_step [iff]: "one_step p1" -by (unfold one_step_def, clarify, ind_cases "ev#evs:p1", auto) +by (unfold one_step_def, clarify, ind_cases "ev#evs:p1" for ev evs, auto) lemma p1_has_only_Says' [rule_format]: "evs:p1 ==> ev:set evs --> (EX A B X. ev=Says A B X)" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/P2.thy --- a/src/HOL/Auth/Guard/P2.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/P2.thy Wed Jul 11 11:14:51 2007 +0200 @@ -130,31 +130,29 @@ subsubsection{*protocol*} -consts p2 :: "event list set" +inductive_set p2 :: "event list set" +where -inductive p2 -intros - -Nil: "[]:p2" + Nil: "[]:p2" -Fake: "[| evsf:p2; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p2" +| Fake: "[| evsf:p2; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p2" -Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2" +| Request: "[| evsr:p2; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p2" -Propose: "[| evsp:p2; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; -I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); -Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p2" +| Propose: "[| evsp:p2; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; + I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); + Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p2" subsubsection{*valid offer lists*} -consts valid :: "agent => nat => agent => msg set" +inductive_set + valid :: "agent => nat => agent => msg set" + for A :: agent and n :: nat and B :: agent +where + Request [intro]: "cons (anchor A n B) nil:valid A n B" -inductive "valid A n B" -intros -Request [intro]: "cons (anchor A n B) nil:valid A n B" - -Propose [intro]: "L:valid A n B -==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" +| Propose [intro]: "L:valid A n B + ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" subsubsection{*basic properties of valid*} @@ -188,15 +186,15 @@ apply clarify apply (frule len_not_empty, clarsimp) apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,xa,l'a|}:valid A n B") -apply (ind_cases "{|x,M,l'a|}:valid A n B") +apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a) +apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a) apply (simp add: chain_def) (* i > 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B") +apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na) apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B") +apply (ind_cases "{|x,l'|}:valid A n B" for x l') by (drule_tac x=l' in spec, simp, blast) subsection{*insertion resilience: @@ -212,15 +210,15 @@ (* i = 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B", simp) -apply (ind_cases "{|x,M,l'|}:valid A n B", clarsimp) -apply (ind_cases "{|head l',l'|}:valid A n B", simp, simp) +apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp) +apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp) +apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp) (* i > 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B") +apply (ind_cases "{|x,l'|}:valid A n B" for x l') apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B") +apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na) apply (frule len_not_empty, clarsimp) by (drule_tac x=l' in spec, clarsimp) @@ -233,14 +231,14 @@ (* i = 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B") +apply (ind_cases "{|x,l'|}:valid A n B" for x l') apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|M,l'|}:valid A n B") +apply (ind_cases "{|M,l'|}:valid A n B" for l') apply (frule len_not_empty, clarsimp, simp) (* i > 0 *) apply clarify apply (frule len_not_empty, clarsimp) -apply (ind_cases "{|x,l'|}:valid A n B") +apply (ind_cases "{|x,l'|}:valid A n B" for x l') apply (frule len_not_empty, clarsimp) by (drule_tac x=l' in spec, clarsimp) @@ -279,7 +277,7 @@ by (auto simp: Gets_correct_def dest: p2_has_no_Gets) lemma p2_is_one_step [iff]: "one_step p2" -by (unfold one_step_def, clarify, ind_cases "ev#evs:p2", auto) +by (unfold one_step_def, clarify, ind_cases "ev#evs:p2" for ev evs, auto) lemma p2_has_only_Says' [rule_format]: "evs:p2 ==> ev:set evs --> (EX A B X. ev=Says A B X)" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Guard/Proto.thy --- a/src/HOL/Auth/Guard/Proto.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Guard/Proto.thy Wed Jul 11 11:14:51 2007 +0200 @@ -106,22 +106,23 @@ "ok evs R s == ((ALL x. x:fst R --> ap s x:set evs) & (ALL n. n:newn R --> Nonce (nonce s n) ~:used evs))" -consts tr :: "proto => event list set" - -inductive "tr p" intros +inductive_set + tr :: "proto => event list set" + for p :: proto +where -Nil [intro]: "[]:tr p" + Nil [intro]: "[]:tr p" -Fake [intro]: "[| evsf:tr p; X:synth (analz (spies evsf)) |] -==> Says Spy B X # evsf:tr p" +| Fake [intro]: "[| evsf:tr p; X:synth (analz (spies evsf)) |] + ==> Says Spy B X # evsf:tr p" -Proto [intro]: "[| evs:tr p; R:p; ok evs R s |] ==> ap' s R # evs:tr p" +| Proto [intro]: "[| evs:tr p; R:p; ok evs R s |] ==> ap' s R # evs:tr p" subsection{*general properties*} lemma one_step_tr [iff]: "one_step (tr p)" apply (unfold one_step_def, clarify) -by (ind_cases "ev # evs:tr p", auto) +by (ind_cases "ev # evs:tr p" for ev evs, auto) constdefs has_only_Says' :: "proto => bool" "has_only_Says' p == ALL R. R:p --> is_Says (snd R)" @@ -379,9 +380,6 @@ Na :: nat "Na == 0" Nb :: nat "Nb == 1" -consts -ns :: proto - abbreviation ns1 :: rule where "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))" @@ -397,10 +395,10 @@ Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})}, Says a b (Crypt (pubK b) (Nonce Nb)))" -inductive ns intros -[iff]: "ns1:ns" -[iff]: "ns2:ns" -[iff]: "ns3:ns" +inductive_set ns :: proto where + [iff]: "ns1:ns" +| [iff]: "ns2:ns" +| [iff]: "ns3:ns" abbreviation (input) ns3a :: event where @@ -428,6 +426,8 @@ lemma inf_is_ord [iff]: "ord ns inf" apply (unfold ord_def inf_def) apply (rule allI)+ +apply (rule impI) +apply (simp add: split_paired_all) by (rule impI, erule ns.cases, simp_all)+ subsection{*general properties*} @@ -435,6 +435,7 @@ lemma ns_has_only_Says' [iff]: "has_only_Says' ns" apply (unfold has_only_Says'_def) apply (rule allI, rule impI) +apply (simp add: split_paired_all) by (erule ns.cases, auto) lemma newn_ns1 [iff]: "newn ns1 = {Na}" @@ -458,6 +459,7 @@ apply (erule fresh_ruleD, simp, simp, simp, simp) apply (rule allI)+ apply (rule impI, rule impI, rule impI) +apply (simp add: split_paired_all) apply (erule ns.cases) (* fresh with NS1 *) apply (rule impI, rule impI, rule impI, rule impI, rule impI, rule impI) @@ -525,6 +527,7 @@ lemma "uniq' ns inf secret" apply (unfold uniq'_def) apply (rule allI)+ +apply (simp add: split_paired_all) apply (rule impI, erule ns.cases) (* R = ns1 *) apply (rule impI, erule ns.cases) @@ -540,7 +543,8 @@ apply (drule Crypt_insert_synth, simp, simp, simp) apply (drule Crypt_insert_synth, simp, simp, simp, simp) (* Proto *) -apply (erule_tac P="ok evsa Ra sa" in rev_mp) +apply (erule_tac P="ok evsa R sa" in rev_mp) +apply (simp add: split_paired_all) apply (erule ns.cases) (* ns1 *) apply (clarify, simp add: secret_def) @@ -563,7 +567,8 @@ apply (drule Crypt_insert_synth, simp, simp, simp) apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp) (* Proto *) -apply (erule_tac P="ok evsa Ra sa" in rev_mp) +apply (erule_tac P="ok evsa R sa" in rev_mp) +apply (simp add: split_paired_all) apply (erule ns.cases) (* ns1 *) apply (clarify, simp add: secret_def) @@ -591,7 +596,8 @@ apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp) apply (drule_tac n="nonce s' Nb" in Crypt_insert_synth, simp, simp, simp, simp) (* Proto *) -apply (erule_tac P="ok evsa Ra sa" in rev_mp) +apply (erule_tac P="ok evsa R sa" in rev_mp) +apply (simp add: split_paired_all) apply (erule ns.cases) (* ns1 *) apply (simp add: secret_def) diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/KerberosIV.thy --- a/src/HOL/Auth/KerberosIV.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/KerberosIV.thy Wed Jul 11 11:14:51 2007 +0200 @@ -110,19 +110,16 @@ Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\ \) \ set evs" -consts - -kerbIV :: "event list set" -inductive "kerbIV" - intros +inductive_set kerbIV :: "event list set" + where Nil: "[] \ kerbIV" - Fake: "\ evsf \ kerbIV; X \ synth (analz (spies evsf)) \ + | Fake: "\ evsf \ kerbIV; X \ synth (analz (spies evsf)) \ \ Says Spy B X # evsf \ kerbIV" (* FROM the initiator *) - K1: "\ evs1 \ kerbIV \ + | K1: "\ evs1 \ kerbIV \ \ Says A Kas \Agent A, Agent Tgs, Number (CT evs1)\ # evs1 \ kerbIV" @@ -133,7 +130,7 @@ (*---------------------------------------------------------------------*) (*FROM Kas *) - K2: "\ evs2 \ kerbIV; Key authK \ used evs2; authK \ symKeys; + | K2: "\ evs2 \ kerbIV; Key authK \ used evs2; authK \ symKeys; Says A' Kas \Agent A, Agent Tgs, Number T1\ \ set evs2 \ \ Says Kas A (Crypt (shrK A) \Key authK, Agent Tgs, Number (CT evs2), @@ -149,7 +146,7 @@ (*---------------------------------------------------------------------*) (* FROM the initiator *) - K3: "\ evs3 \ kerbIV; + | K3: "\ evs3 \ kerbIV; Says A Kas \Agent A, Agent Tgs, Number T1\ \ set evs3; Says Kas' A (Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, authTicket\) \ set evs3; @@ -169,7 +166,7 @@ Theorems that exploit it have the suffix `_u', which stands for updated protocol. *) - K4: "\ evs4 \ kerbIV; Key servK \ used evs4; servK \ symKeys; + | K4: "\ evs4 \ kerbIV; Key servK \ used evs4; servK \ symKeys; B \ Tgs; authK \ symKeys; Says A' Tgs \ (Crypt (shrK Tgs) \Agent A, Agent Tgs, Key authK, @@ -196,7 +193,7 @@ (*---------------------------------------------------------------------*) (* FROM the initiator *) - K5: "\ evs5 \ kerbIV; authK \ symKeys; servK \ symKeys; + | K5: "\ evs5 \ kerbIV; authK \ symKeys; servK \ symKeys; Says A Tgs \authTicket, Crypt authK \Agent A, Number T2\, Agent B\ @@ -213,7 +210,7 @@ (*---------------------------------------------------------------------*) (* FROM the responder*) - K6: "\ evs6 \ kerbIV; + | K6: "\ evs6 \ kerbIV; Says A' B \ (Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\), (Crypt servK \Agent A, Number T3\)\ @@ -228,7 +225,7 @@ (*---------------------------------------------------------------------*) (* Leaking an authK... *) - Oops1: "\ evsO1 \ kerbIV; A \ Spy; + | Oops1: "\ evsO1 \ kerbIV; A \ Spy; Says Kas A (Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, authTicket\) \ set evsO1; @@ -239,7 +236,7 @@ (*---------------------------------------------------------------------*) (*Leaking a servK... *) - Oops2: "\ evsO2 \ kerbIV; A \ Spy; + | Oops2: "\ evsO2 \ kerbIV; A \ Spy; Says Tgs A (Crypt authK \Key servK, Agent B, Number Ts, servTicket\) \ set evsO2; diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/KerberosIV_Gets.thy --- a/src/HOL/Auth/KerberosIV_Gets.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/KerberosIV_Gets.thy Wed Jul 11 11:14:51 2007 +0200 @@ -98,22 +98,19 @@ Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\ \) \ set evs" -consts - -kerbIV_gets :: "event list set" -inductive "kerbIV_gets" - intros +inductive_set "kerbIV_gets" :: "event list set" + where Nil: "[] \ kerbIV_gets" - Fake: "\ evsf \ kerbIV_gets; X \ synth (analz (spies evsf)) \ + | Fake: "\ evsf \ kerbIV_gets; X \ synth (analz (spies evsf)) \ \ Says Spy B X # evsf \ kerbIV_gets" - Reception: "\ evsr \ kerbIV_gets; Says A B X \ set evsr \ + | Reception: "\ evsr \ kerbIV_gets; Says A B X \ set evsr \ \ Gets B X # evsr \ kerbIV_gets" (* FROM the initiator *) - K1: "\ evs1 \ kerbIV_gets \ + | K1: "\ evs1 \ kerbIV_gets \ \ Says A Kas \Agent A, Agent Tgs, Number (CT evs1)\ # evs1 \ kerbIV_gets" @@ -124,7 +121,7 @@ (*---------------------------------------------------------------------*) (*FROM Kas *) - K2: "\ evs2 \ kerbIV_gets; Key authK \ used evs2; authK \ symKeys; + | K2: "\ evs2 \ kerbIV_gets; Key authK \ used evs2; authK \ symKeys; Gets Kas \Agent A, Agent Tgs, Number T1\ \ set evs2 \ \ Says Kas A (Crypt (shrK A) \Key authK, Agent Tgs, Number (CT evs2), @@ -140,7 +137,7 @@ (*---------------------------------------------------------------------*) (* FROM the initiator *) - K3: "\ evs3 \ kerbIV_gets; + | K3: "\ evs3 \ kerbIV_gets; Says A Kas \Agent A, Agent Tgs, Number T1\ \ set evs3; Gets A (Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, authTicket\) \ set evs3; @@ -160,7 +157,7 @@ Theorems that exploit it have the suffix `_u', which stands for updated protocol. *) - K4: "\ evs4 \ kerbIV_gets; Key servK \ used evs4; servK \ symKeys; + | K4: "\ evs4 \ kerbIV_gets; Key servK \ used evs4; servK \ symKeys; B \ Tgs; authK \ symKeys; Gets Tgs \ (Crypt (shrK Tgs) \Agent A, Agent Tgs, Key authK, @@ -187,7 +184,7 @@ (*---------------------------------------------------------------------*) (* FROM the initiator *) - K5: "\ evs5 \ kerbIV_gets; authK \ symKeys; servK \ symKeys; + | K5: "\ evs5 \ kerbIV_gets; authK \ symKeys; servK \ symKeys; Says A Tgs \authTicket, Crypt authK \Agent A, Number T2\, Agent B\ @@ -204,7 +201,7 @@ (*---------------------------------------------------------------------*) (* FROM the responder*) - K6: "\ evs6 \ kerbIV_gets; + | K6: "\ evs6 \ kerbIV_gets; Gets B \ (Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\), (Crypt servK \Agent A, Number T3\)\ @@ -219,7 +216,7 @@ (*---------------------------------------------------------------------*) (* Leaking an authK... *) - Oops1: "\ evsO1 \ kerbIV_gets; A \ Spy; + | Oops1: "\ evsO1 \ kerbIV_gets; A \ Spy; Says Kas A (Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, authTicket\) \ set evsO1; @@ -230,7 +227,7 @@ (*---------------------------------------------------------------------*) (*Leaking a servK... *) - Oops2: "\ evsO2 \ kerbIV_gets; A \ Spy; + | Oops2: "\ evsO2 \ kerbIV_gets; A \ Spy; Says Tgs A (Crypt authK \Key servK, Agent B, Number Ts, servTicket\) \ set evsO2; diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/KerberosV.thy --- a/src/HOL/Auth/KerberosV.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/KerberosV.thy Wed Jul 11 11:14:51 2007 +0200 @@ -100,24 +100,21 @@ Crypt (shrK B) \Agent A, Agent B, Key servK, tt\ \ \ set evs" -consts - -kerbV :: "event list set" -inductive "kerbV" - intros +inductive_set kerbV :: "event list set" + where Nil: "[] \ kerbV" - Fake: "\ evsf \ kerbV; X \ synth (analz (spies evsf)) \ + | Fake: "\ evsf \ kerbV; X \ synth (analz (spies evsf)) \ \ Says Spy B X # evsf \ kerbV" (*Authentication phase*) - KV1: "\ evs1 \ kerbV \ + | KV1: "\ evs1 \ kerbV \ \ Says A Kas \Agent A, Agent Tgs, Number (CT evs1)\ # evs1 \ kerbV" (*Unlike version IV, authTicket is not re-encrypted*) - KV2: "\ evs2 \ kerbV; Key authK \ used evs2; authK \ symKeys; + | KV2: "\ evs2 \ kerbV; Key authK \ used evs2; authK \ symKeys; Says A' Kas \Agent A, Agent Tgs, Number T1\ \ set evs2 \ \ Says Kas A \ Crypt (shrK A) \Key authK, Agent Tgs, Number (CT evs2)\, @@ -126,7 +123,7 @@ (* Authorisation phase *) - KV3: "\ evs3 \ kerbV; A \ Kas; A \ Tgs; + | KV3: "\ evs3 \ kerbV; A \ Kas; A \ Tgs; Says A Kas \Agent A, Agent Tgs, Number T1\ \ set evs3; Says Kas' A \Crypt (shrK A) \Key authK, Agent Tgs, Number Ta\, authTicket\ \ set evs3; @@ -136,7 +133,7 @@ (Crypt authK \Agent A, Number (CT evs3)\), Agent B\ # evs3 \ kerbV" (*Unlike version IV, servTicket is not re-encrypted*) - KV4: "\ evs4 \ kerbV; Key servK \ used evs4; servK \ symKeys; + | KV4: "\ evs4 \ kerbV; Key servK \ used evs4; servK \ symKeys; B \ Tgs; authK \ symKeys; Says A' Tgs \ (Crypt (shrK Tgs) \Agent A, Agent Tgs, Key authK, @@ -154,7 +151,7 @@ (*Service phase*) - KV5: "\ evs5 \ kerbV; authK \ symKeys; servK \ symKeys; + | KV5: "\ evs5 \ kerbV; authK \ symKeys; servK \ symKeys; A \ Kas; A \ Tgs; Says A Tgs \authTicket, Crypt authK \Agent A, Number T2\, @@ -168,7 +165,7 @@ Crypt servK \Agent A, Number (CT evs5)\ \ # evs5 \ kerbV" - KV6: "\ evs6 \ kerbV; B \ Kas; B \ Tgs; + | KV6: "\ evs6 \ kerbV; B \ Kas; B \ Tgs; Says A' B \ (Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\), (Crypt servK \Agent A, Number T3\)\ @@ -182,7 +179,7 @@ (* Leaking an authK... *) - Oops1:"\ evsO1 \ kerbV; A \ Spy; + | Oops1:"\ evsO1 \ kerbV; A \ Spy; Says Kas A \Crypt (shrK A) \Key authK, Agent Tgs, Number Ta\, authTicket\ \ set evsO1; expiredAK Ta evsO1 \ @@ -190,7 +187,7 @@ # evsO1 \ kerbV" (*Leaking a servK... *) - Oops2: "\ evsO2 \ kerbV; A \ Spy; + | Oops2: "\ evsO2 \ kerbV; A \ Spy; Says Tgs A \Crypt authK \Key servK, Agent B, Number Ts\, servTicket\ \ set evsO2; expiredSK Ts evsO2 \ diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Kerberos_BAN.thy --- a/src/HOL/Auth/Kerberos_BAN.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.thy Wed Jul 11 11:14:51 2007 +0200 @@ -71,22 +71,21 @@ ev \ set (tl (dropWhile (% z. z \ ev) evs))" -consts bankerberos :: "event list set" -inductive "bankerberos" - intros +inductive_set bankerberos :: "event list set" + where Nil: "[] \ bankerberos" - Fake: "\ evsf \ bankerberos; X \ synth (analz (spies evsf)) \ + | Fake: "\ evsf \ bankerberos; X \ synth (analz (spies evsf)) \ \ Says Spy B X # evsf \ bankerberos" - BK1: "\ evs1 \ bankerberos \ + | BK1: "\ evs1 \ bankerberos \ \ Says A Server \Agent A, Agent B\ # evs1 \ bankerberos" - BK2: "\ evs2 \ bankerberos; Key K \ used evs2; K \ symKeys; + | BK2: "\ evs2 \ bankerberos; Key K \ used evs2; K \ symKeys; Says A' Server \Agent A, Agent B\ \ set evs2 \ \ Says Server A (Crypt (shrK A) @@ -95,7 +94,7 @@ # evs2 \ bankerberos" - BK3: "\ evs3 \ bankerberos; + | BK3: "\ evs3 \ bankerberos; Says S A (Crypt (shrK A) \Number Tk, Agent B, Key K, Ticket\) \ set evs3; Says A Server \Agent A, Agent B\ \ set evs3; @@ -104,7 +103,7 @@ # evs3 \ bankerberos" - BK4: "\ evs4 \ bankerberos; + | BK4: "\ evs4 \ bankerberos; Says A' B \(Crypt (shrK B) \Number Tk, Agent A, Key K\), (Crypt K \Agent A, Number Ta\) \: set evs4; \ expiredK Tk evs4; \ expiredA Ta evs4 \ @@ -112,7 +111,7 @@ \ bankerberos" (*Old session keys may become compromised*) - Oops: "\ evso \ bankerberos; + | Oops: "\ evso \ bankerberos; Says Server A (Crypt (shrK A) \Number Tk, Agent B, Key K, Ticket\) \ set evso; expiredK Tk evso \ diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Kerberos_BAN_Gets.thy --- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Wed Jul 11 11:14:51 2007 +0200 @@ -63,24 +63,23 @@ ev \ set (tl (dropWhile (% z. z \ ev) evs))" -consts bankerb_gets :: "event list set" -inductive "bankerb_gets" - intros +inductive_set bankerb_gets :: "event list set" + where Nil: "[] \ bankerb_gets" - Fake: "\ evsf \ bankerb_gets; X \ synth (analz (knows Spy evsf)) \ + | Fake: "\ evsf \ bankerb_gets; X \ synth (analz (knows Spy evsf)) \ \ Says Spy B X # evsf \ bankerb_gets" - Reception: "\ evsr\ bankerb_gets; Says A B X \ set evsr \ + | Reception: "\ evsr\ bankerb_gets; Says A B X \ set evsr \ \ Gets B X # evsr \ bankerb_gets" - BK1: "\ evs1 \ bankerb_gets \ + | BK1: "\ evs1 \ bankerb_gets \ \ Says A Server \Agent A, Agent B\ # evs1 \ bankerb_gets" - BK2: "\ evs2 \ bankerb_gets; Key K \ used evs2; K \ symKeys; + | BK2: "\ evs2 \ bankerb_gets; Key K \ used evs2; K \ symKeys; Gets Server \Agent A, Agent B\ \ set evs2 \ \ Says Server A (Crypt (shrK A) @@ -89,7 +88,7 @@ # evs2 \ bankerb_gets" - BK3: "\ evs3 \ bankerb_gets; + | BK3: "\ evs3 \ bankerb_gets; Gets A (Crypt (shrK A) \Number Tk, Agent B, Key K, Ticket\) \ set evs3; Says A Server \Agent A, Agent B\ \ set evs3; @@ -98,7 +97,7 @@ # evs3 \ bankerb_gets" - BK4: "\ evs4 \ bankerb_gets; + | BK4: "\ evs4 \ bankerb_gets; Gets B \(Crypt (shrK B) \Number Tk, Agent A, Key K\), (Crypt K \Agent A, Number Ta\) \: set evs4; \ expiredK Tk evs4; \ expiredA Ta evs4 \ @@ -106,7 +105,7 @@ \ bankerb_gets" (*Old session keys may become compromised*) - Oops: "\ evso \ bankerb_gets; + | Oops: "\ evso \ bankerb_gets; Says Server A (Crypt (shrK A) \Number Tk, Agent B, Key K, Ticket\) \ set evso; expiredK Tk evso \ diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Message.thy Wed Jul 11 11:14:51 2007 +0200 @@ -72,13 +72,14 @@ subsubsection{*Inductive Definition of All Parts" of a Message*} -consts parts :: "msg set => msg set" -inductive "parts H" - intros +inductive_set + parts :: "msg set => msg set" + for H :: "msg set" + where Inj [intro]: "X \ H ==> X \ parts H" - Fst: "{|X,Y|} \ parts H ==> X \ parts H" - Snd: "{|X,Y|} \ parts H ==> Y \ parts H" - Body: "Crypt K X \ parts H ==> X \ parts H" + | Fst: "{|X,Y|} \ parts H ==> X \ parts H" + | Snd: "{|X,Y|} \ parts H ==> Y \ parts H" + | Body: "Crypt K X \ parts H ==> X \ parts H" text{*Monotonicity*} @@ -335,13 +336,14 @@ messages, including keys. A form of downward closure. Pairs can be taken apart; messages decrypted with known keys. *} -consts analz :: "msg set => msg set" -inductive "analz H" - intros +inductive_set + analz :: "msg set => msg set" + for H :: "msg set" + where Inj [intro,simp] : "X \ H ==> X \ analz H" - Fst: "{|X,Y|} \ analz H ==> X \ analz H" - Snd: "{|X,Y|} \ analz H ==> Y \ analz H" - Decrypt [dest]: + | Fst: "{|X,Y|} \ analz H ==> X \ analz H" + | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" + | Decrypt [dest]: "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" @@ -460,14 +462,14 @@ analz (insert (Crypt K X) H) \ insert (Crypt K X) (analz (insert X H))" apply (rule subsetI) -apply (erule_tac xa = x in analz.induct, auto) +apply (erule_tac x = x in analz.induct, auto) done lemma lemma2: "Key (invKey K) \ analz H ==> insert (Crypt K X) (analz (insert X H)) \ analz (insert (Crypt K X) H)" apply auto -apply (erule_tac xa = x in analz.induct, auto) +apply (erule_tac x = x in analz.induct, auto) apply (blast intro: analz_insertI analz.Decrypt) done @@ -579,15 +581,16 @@ encrypted with known keys. Agent names are public domain. Numbers can be guessed, but Nonces cannot be. *} -consts synth :: "msg set => msg set" -inductive "synth H" - intros +inductive_set + synth :: "msg set => msg set" + for H :: "msg set" + where Inj [intro]: "X \ H ==> X \ synth H" - Agent [intro]: "Agent agt \ synth H" - Number [intro]: "Number n \ synth H" - Hash [intro]: "X \ synth H ==> Hash X \ synth H" - MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" - Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" + | Agent [intro]: "Agent agt \ synth H" + | Number [intro]: "Number n \ synth H" + | Hash [intro]: "X \ synth H ==> Hash X \ synth H" + | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" + | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" text{*Monotonicity*} lemma synth_mono: "G\H ==> synth(G) \ synth(H)" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/NS_Public.thy --- a/src/HOL/Auth/NS_Public.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/NS_Public.thy Wed Jul 11 11:14:51 2007 +0200 @@ -11,32 +11,30 @@ theory NS_Public imports Public begin -consts ns_public :: "event list set" - -inductive ns_public - intros +inductive_set ns_public :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ ns_public" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "\evsf \ ns_public; X \ synth (analz (spies evsf))\ + | Fake: "\evsf \ ns_public; X \ synth (analz (spies evsf))\ \ Says Spy B X # evsf \ ns_public" (*Alice initiates a protocol run, sending a nonce to Bob*) - NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) # evs1 \ ns_public" (*Bob responds to Alice's message with a further nonce*) - NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) # evs2 \ ns_public" (*Alice proves her existence by sending NB back to Bob.*) - NS3: "\evs3 \ ns_public; + | NS3: "\evs3 \ ns_public; Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs3\ diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/NS_Public_Bad.thy --- a/src/HOL/Auth/NS_Public_Bad.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.thy Wed Jul 11 11:14:51 2007 +0200 @@ -15,32 +15,30 @@ theory NS_Public_Bad imports Public begin -consts ns_public :: "event list set" - -inductive ns_public - intros +inductive_set ns_public :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ ns_public" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "\evsf \ ns_public; X \ synth (analz (spies evsf))\ + | Fake: "\evsf \ ns_public; X \ synth (analz (spies evsf))\ \ Says Spy B X # evsf \ ns_public" (*Alice initiates a protocol run, sending a nonce to Bob*) - NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) # evs1 \ ns_public" (*Bob responds to Alice's message with a further nonce*) - NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) # evs2 \ ns_public" (*Alice proves her existence by sending NB back to Bob.*) - NS3: "\evs3 \ ns_public; + | NS3: "\evs3 \ ns_public; Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Wed Jul 11 11:14:51 2007 +0200 @@ -25,26 +25,25 @@ X \ parts (spies (takeWhile (% z. z \ Says A B Y) (rev evs)))" -consts ns_shared :: "event list set" -inductive "ns_shared" - intros +inductive_set ns_shared :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ ns_shared" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "\evsf \ ns_shared; X \ synth (analz (spies evsf))\ +| Fake: "\evsf \ ns_shared; X \ synth (analz (spies evsf))\ \ Says Spy B X # evsf \ ns_shared" (*Alice initiates a protocol run, requesting to talk to any B*) - NS1: "\evs1 \ ns_shared; Nonce NA \ used evs1\ +| NS1: "\evs1 \ ns_shared; Nonce NA \ used evs1\ \ Says A Server \Agent A, Agent B, Nonce NA\ # evs1 \ ns_shared" (*Server's response to Alice's message. !! It may respond more than once to A's request !! Server doesn't know who the true sender is, hence the A' in the sender field.*) - NS2: "\evs2 \ ns_shared; Key KAB \ used evs2; KAB \ symKeys; +| NS2: "\evs2 \ ns_shared; Key KAB \ used evs2; KAB \ symKeys; Says A' Server \Agent A, Agent B, Nonce NA\ \ set evs2\ \ Says Server A (Crypt (shrK A) @@ -54,14 +53,14 @@ (*We can't assume S=Server. Agent A "remembers" her nonce. Need A \ Server because we allow messages to self.*) - NS3: "\evs3 \ ns_shared; A \ Server; +| NS3: "\evs3 \ ns_shared; A \ Server; Says S A (Crypt (shrK A) \Nonce NA, Agent B, Key K, X\) \ set evs3; Says A Server \Agent A, Agent B, Nonce NA\ \ set evs3\ \ Says A B X # evs3 \ ns_shared" (*Bob's nonce exchange. He does not know who the message came from, but responds to A because she is mentioned inside.*) - NS4: "\evs4 \ ns_shared; Nonce NB \ used evs4; K \ symKeys; +| NS4: "\evs4 \ ns_shared; Nonce NB \ used evs4; K \ symKeys; Says A' B (Crypt (shrK B) \Key K, Agent A\) \ set evs4\ \ Says B A (Crypt K (Nonce NB)) # evs4 \ ns_shared" @@ -70,7 +69,7 @@ We do NOT send NB-1 or similar as the Spy cannot spoof such things. Letting the Spy add or subtract 1 lets him send all nonces. Instead we distinguish the messages by sending the nonce twice.*) - NS5: "\evs5 \ ns_shared; K \ symKeys; +| NS5: "\evs5 \ ns_shared; K \ symKeys; Says B' A (Crypt K (Nonce NB)) \ set evs5; Says S A (Crypt (shrK A) \Nonce NA, Agent B, Key K, X\) \ set evs5\ @@ -79,7 +78,7 @@ (*This message models possible leaks of session keys. The two Nonces identify the protocol run: the rule insists upon the true senders in order to make them accurate.*) - Oops: "\evso \ ns_shared; Says B A (Crypt K (Nonce NB)) \ set evso; +| Oops: "\evso \ ns_shared; Says B A (Crypt K (Nonce NB)) \ set evso; Says Server A (Crypt (shrK A) \Nonce NA, Agent B, Key K, X\) \ set evso\ \ Notes Spy \Nonce NA, Nonce NB, Key K\ # evso \ ns_shared" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Wed Jul 11 11:14:51 2007 +0200 @@ -14,31 +14,30 @@ This is the original version, which encrypts Nonce NB.*} -consts otway :: "event list set" -inductive "otway" - intros +inductive_set otway :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ otway" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] + | Fake: "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ otway" (*A message that has been sent can be received by the intended recipient.*) - Reception: "[| evsr \ otway; Says A B X \set evsr |] + | Reception: "[| evsr \ otway; Says A B X \set evsr |] ==> Gets B X # evsr \ otway" (*Alice initiates a protocol run*) - OR1: "[| evs1 \ otway; Nonce NA \ used evs1 |] + | OR1: "[| evs1 \ otway; Nonce NA \ used evs1 |] ==> Says A B {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} # evs1 : otway" (*Bob's response to Alice's message. Note that NB is encrypted.*) - OR2: "[| evs2 \ otway; Nonce NB \ used evs2; + | OR2: "[| evs2 \ otway; Nonce NB \ used evs2; Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] ==> Says B Server {|Nonce NA, Agent A, Agent B, X, @@ -49,7 +48,7 @@ (*The Server receives Bob's message and checks that the three NAs match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) - OR3: "[| evs3 \ otway; Key KAB \ used evs3; + | OR3: "[| evs3 \ otway; Key KAB \ used evs3; Gets Server {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, @@ -64,7 +63,7 @@ (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. Need B \ Server because we allow messages to self.*) - OR4: "[| evs4 \ otway; B \ Server; + | OR4: "[| evs4 \ otway; B \ Server; Says B Server {|Nonce NA, Agent A, Agent B, X', Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} @@ -75,7 +74,7 @@ (*This message models possible leaks of session keys. The nonces identify the protocol run.*) - Oops: "[| evso \ otway; + | Oops: "[| evso \ otway; Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} : set evso |] ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/OtwayReesBella.thy --- a/src/HOL/Auth/OtwayReesBella.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/OtwayReesBella.thy Wed Jul 11 11:14:51 2007 +0200 @@ -16,31 +16,30 @@ updated protocol makes no use of the session key to encrypt but informs A that B knows it.*} -consts orb :: "event list set" -inductive "orb" - intros +inductive_set orb :: "event list set" + where Nil: "[]\ orb" - Fake: "\evsa\ orb; X\ synth (analz (knows Spy evsa))\ +| Fake: "\evsa\ orb; X\ synth (analz (knows Spy evsa))\ \ Says Spy B X # evsa \ orb" - Reception: "\evsr\ orb; Says A B X \ set evsr\ +| Reception: "\evsr\ orb; Says A B X \ set evsr\ \ Gets B X # evsr \ orb" - OR1: "\evs1\ orb; Nonce NA \ used evs1\ +| OR1: "\evs1\ orb; Nonce NA \ used evs1\ \ Says A B \Nonce M, Agent A, Agent B, Crypt (shrK A) \Nonce NA, Nonce M, Agent A, Agent B\\ # evs1 \ orb" - OR2: "\evs2\ orb; Nonce NB \ used evs2; +| OR2: "\evs2\ orb; Nonce NB \ used evs2; Gets B \Nonce M, Agent A, Agent B, X\ \ set evs2\ \ Says B Server \Nonce M, Agent A, Agent B, X, Crypt (shrK B) \Nonce NB, Nonce M, Nonce M, Agent A, Agent B\\ # evs2 \ orb" - OR3: "\evs3\ orb; Key KAB \ used evs3; +| OR3: "\evs3\ orb; Key KAB \ used evs3; Gets Server \Nonce M, Agent A, Agent B, Crypt (shrK A) \Nonce NA, Nonce M, Agent A, Agent B\, @@ -53,7 +52,7 @@ (*B can only check that the message he is bouncing is a ciphertext*) (*Sending M back is omitted*) - OR4: "\evs4\ orb; B \ Server; \ p q. X \ \p, q\; +| OR4: "\evs4\ orb; B \ Server; \ p q. X \ \p, q\; Says B Server \Nonce M, Agent A, Agent B, X', Crypt (shrK B) \Nonce NB, Nonce M, Nonce M, Agent A, Agent B\\ \ set evs4; @@ -62,7 +61,7 @@ \ Says B A \Nonce M, X\ # evs4 \ orb" - Oops: "\evso\ orb; +| Oops: "\evso\ orb; Says Server B \Nonce M, Crypt (shrK B) \Crypt (shrK A) \Nonce NA, Key KAB\, Nonce NB, Key KAB\\ diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.thy Wed Jul 11 11:14:51 2007 +0200 @@ -22,34 +22,33 @@ IEEE Trans. SE 22 (1) *} -consts otway :: "event list set" -inductive "otway" - intros +inductive_set otway :: "event list set" + where Nil: --{*The empty trace*} "[] \ otway" - Fake: --{*The Spy may say anything he can say. The sender field is correct, + | Fake: --{*The Spy may say anything he can say. The sender field is correct, but agents don't use that information.*} "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ otway" - Reception: --{*A message that has been sent can be received by the + | Reception: --{*A message that has been sent can be received by the intended recipient.*} "[| evsr \ otway; Says A B X \set evsr |] ==> Gets B X # evsr \ otway" - OR1: --{*Alice initiates a protocol run*} + | OR1: --{*Alice initiates a protocol run*} "evs1 \ otway ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \ otway" - OR2: --{*Bob's response to Alice's message.*} + | OR2: --{*Bob's response to Alice's message.*} "[| evs2 \ otway; Gets B {|Agent A, Agent B, Nonce NA|} \set evs2 |] ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs2 \ otway" - OR3: --{*The Server receives Bob's message. Then he sends a new + | OR3: --{*The Server receives Bob's message. Then he sends a new session key to Bob with a packet for forwarding to Alice.*} "[| evs3 \ otway; Key KAB \ used evs3; Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|} @@ -59,7 +58,7 @@ Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|} # evs3 \ otway" - OR4: --{*Bob receives the Server's (?) message and compares the Nonces with + | OR4: --{*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. Need @{term "B \ Server"} because we allow messages to self.*} "[| evs4 \ otway; B \ Server; @@ -68,7 +67,7 @@ \set evs4 |] ==> Says B A X # evs4 \ otway" - Oops: --{*This message models possible leaks of session keys. The nonces + | Oops: --{*This message models possible leaks of session keys. The nonces identify the protocol run.*} "[| evso \ otway; Says Server B diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Wed Jul 11 11:14:51 2007 +0200 @@ -19,30 +19,29 @@ the protocol is open to a middleperson attack. Attempting to prove some key lemmas indicates the possibility of this attack.*} -consts otway :: "event list set" -inductive "otway" - intros +inductive_set otway :: "event list set" + where Nil: --{*The empty trace*} "[] \ otway" - Fake: --{*The Spy may say anything he can say. The sender field is correct, + | Fake: --{*The Spy may say anything he can say. The sender field is correct, but agents don't use that information.*} "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ otway" - Reception: --{*A message that has been sent can be received by the + | Reception: --{*A message that has been sent can be received by the intended recipient.*} "[| evsr \ otway; Says A B X \set evsr |] ==> Gets B X # evsr \ otway" - OR1: --{*Alice initiates a protocol run*} + | OR1: --{*Alice initiates a protocol run*} "[| evs1 \ otway; Nonce NA \ used evs1 |] ==> Says A B {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} # evs1 \ otway" - OR2: --{*Bob's response to Alice's message. + | OR2: --{*Bob's response to Alice's message. This variant of the protocol does NOT encrypt NB.*} "[| evs2 \ otway; Nonce NB \ used evs2; Gets B {|Nonce NA, Agent A, Agent B, X|} \ set evs2 |] @@ -51,7 +50,7 @@ Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} # evs2 \ otway" - OR3: --{*The Server receives Bob's message and checks that the three NAs + | OR3: --{*The Server receives Bob's message and checks that the three NAs match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*} "[| evs3 \ otway; Key KAB \ used evs3; @@ -67,7 +66,7 @@ Crypt (shrK B) {|Nonce NB, Key KAB|}|} # evs3 \ otway" - OR4: --{*Bob receives the Server's (?) message and compares the Nonces with + | OR4: --{*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. Need @{term "B \ Server"} because we allow messages to self.*} "[| evs4 \ otway; B \ Server; @@ -78,7 +77,7 @@ \ set evs4 |] ==> Says B A {|Nonce NA, X|} # evs4 \ otway" - Oops: --{*This message models possible leaks of session keys. The nonces + | Oops: --{*This message models possible leaks of session keys. The nonces identify the protocol run.*} "[| evso \ otway; Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Recur.thy Wed Jul 11 11:14:51 2007 +0200 @@ -17,16 +17,17 @@ who receives one. Perhaps the two session keys could be bundled into a single message. *) -consts respond :: "event list => (msg*msg*key)set" -inductive "respond evs" (*Server's response to the nested message*) - intros +inductive_set (*Server's response to the nested message*) + respond :: "event list => (msg*msg*key)set" + for evs :: "event list" + where One: "Key KAB \ used evs ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|}, KAB) \ respond evs" (*The most recent session key is passed up to the caller*) - Cons: "[| (PA, RA, KAB) \ respond evs; + | Cons: "[| (PA, RA, KAB) \ respond evs; Key KBC \ used evs; Key KBC \ parts {RA}; PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |] ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, @@ -40,50 +41,50 @@ (*Induction over "respond" can be difficult due to the complexity of the subgoals. Set "responses" captures the general form of certificates. *) -consts responses :: "event list => msg set" -inductive "responses evs" - intros +inductive_set + responses :: "event list => msg set" + for evs :: "event list" + where (*Server terminates lists*) Nil: "END \ responses evs" - Cons: "[| RA \ responses evs; Key KAB \ used evs |] + | Cons: "[| RA \ responses evs; Key KAB \ used evs |] ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, RA|} \ responses evs" -consts recur :: "event list set" -inductive "recur" - intros +inductive_set recur :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ recur" (*The spy MAY say anything he CAN say. Common to all similar protocols.*) - Fake: "[| evsf \ recur; X \ synth (analz (knows Spy evsf)) |] + | Fake: "[| evsf \ recur; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ recur" (*Alice initiates a protocol run. END is a placeholder to terminate the nesting.*) - RA1: "[| evs1 \ recur; Nonce NA \ used evs1 |] + | RA1: "[| evs1 \ recur; Nonce NA \ used evs1 |] ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}) # evs1 \ recur" (*Bob's response to Alice's message. C might be the Server. We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because it complicates proofs, so B may respond to any message at all!*) - RA2: "[| evs2 \ recur; Nonce NB \ used evs2; + | RA2: "[| evs2 \ recur; Nonce NB \ used evs2; Says A' B PA \ set evs2 |] ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) # evs2 \ recur" (*The Server receives Bob's message and prepares a response.*) - RA3: "[| evs3 \ recur; Says B' Server PB \ set evs3; + | RA3: "[| evs3 \ recur; Says B' Server PB \ set evs3; (PB,RB,K) \ respond evs3 |] ==> Says Server B RB # evs3 \ recur" (*Bob receives the returned message and compares the Nonces with those in the message he previously sent the Server.*) - RA4: "[| evs4 \ recur; + | RA4: "[| evs4 \ recur; Says B C {|XH, Agent B, Agent C, Nonce NB, XA, Agent A, Agent B, Nonce NA, P|} \ set evs4; Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, @@ -350,7 +351,7 @@ lemma respond_certificate: "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \ respond evs ==> Crypt (shrK A) {|Key K, B, NA|} \ parts {RA}" -apply (ind_cases "(X, RA, K) \ respond evs") +apply (ind_cases "(Hash[Key (shrK A)] \Agent A, B, NA, P\, RA, K) \ respond evs") apply simp_all done diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Smartcard/ShoupRubin.thy --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Jul 11 11:14:51 2007 +0200 @@ -36,15 +36,14 @@ ev \ set (tl (dropWhile (% z. z \ ev) evs))" -consts sr :: "event list set" -inductive "sr" - intros +inductive_set sr :: "event list set" + where Nil: "[]\ sr" - Fake: "\ evsF\ sr; X\ synth (analz (knows Spy evsF)); + | Fake: "\ evsF\ sr; X\ synth (analz (knows Spy evsF)); illegalUse(Card B) \ \ Says Spy A X # Inputs Spy (Card B) X # evsF \ sr" @@ -52,24 +51,24 @@ (*In general this rule causes the assumption Card B \ cloned in most guarantees for B - starting with confidentiality - otherwise pairK_confidential could not apply*) - Forge: + | Forge: "\ evsFo \ sr; Nonce Nb \ analz (knows Spy evsFo); Key (pairK(A,B)) \ knows Spy evsFo \ \ Notes Spy (Key (sesK(Nb,pairK(A,B)))) # evsFo \ sr" - Reception: "\ evsR\ sr; Says A B X \ set evsR \ + | Reception: "\ evsR\ sr; Says A B X \ set evsR \ \ Gets B X # evsR \ sr" (*A AND THE SERVER *) - SR1: "\ evs1\ sr; A \ Server\ + | SR1: "\ evs1\ sr; A \ Server\ \ Says A Server \Agent A, Agent B\ # evs1 \ sr" - SR2: "\ evs2\ sr; + | SR2: "\ evs2\ sr; Gets Server \Agent A, Agent B\ \ set evs2 \ \ Says Server A \Nonce (Pairkey(A,B)), Crypt (shrK A) \Nonce (Pairkey(A,B)), Agent B\ @@ -82,7 +81,7 @@ (*A AND HER CARD*) (*A cannot decrypt the verifier for she dosn't know shrK A, but the pairkey is recognisable*) - SR3: "\ evs3\ sr; legalUse(Card A); + | SR3: "\ evs3\ sr; legalUse(Card A); Says A Server \Agent A, Agent B\ \ set evs3; Gets A \Nonce Pk, Certificate\ \ set evs3 \ \ Inputs A (Card A) (Agent A) @@ -93,7 +92,7 @@ the server*) (*The card outputs the nonce Na to A*) - SR4: "\ evs4\ sr; A \ Server; + | SR4: "\ evs4\ sr; A \ Server; Nonce Na \ used evs4; legalUse(Card A); Inputs A (Card A) (Agent A) \ set evs4 \ \ Outpts (Card A) A \Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\ @@ -101,9 +100,9 @@ (*The card can be exploited by the spy*) (*because of the assumptions on the card, A is certainly not server nor spy*) - SR4Fake: "\ evs4F\ sr; Nonce Na \ used evs4F; - illegalUse(Card A); - Inputs Spy (Card A) (Agent A) \ set evs4F \ + | SR4Fake: "\ evs4F\ sr; Nonce Na \ used evs4F; + illegalUse(Card A); + Inputs Spy (Card A) (Agent A) \ set evs4F \ \ Outpts (Card A) Spy \Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\ # evs4F \ sr" @@ -111,7 +110,7 @@ (*A TOWARDS B*) - SR5: "\ evs5\ sr; + | SR5: "\ evs5\ sr; Outpts (Card A) A \Nonce Na, Certificate\ \ set evs5; \ p q. Certificate \ \p, q\ \ \ Says A B \Agent A, Nonce Na\ # evs5 \ sr" @@ -122,13 +121,13 @@ (*B AND HIS CARD*) - SR6: "\ evs6\ sr; legalUse(Card B); + | SR6: "\ evs6\ sr; legalUse(Card B); Gets B \Agent A, Nonce Na\ \ set evs6 \ \ Inputs B (Card B) \Agent A, Nonce Na\ # evs6 \ sr" (*B gets back from the card the session key and various verifiers*) - SR7: "\ evs7\ sr; + | SR7: "\ evs7\ sr; Nonce Nb \ used evs7; legalUse(Card B); B \ Server; K = sesK(Nb,pairK(A,B)); Key K \ used evs7; @@ -140,11 +139,11 @@ (*The card can be exploited by the spy*) (*because of the assumptions on the card, A is certainly not server nor spy*) - SR7Fake: "\ evs7F\ sr; Nonce Nb \ used evs7F; - illegalUse(Card B); - K = sesK(Nb,pairK(A,B)); - Key K \ used evs7F; - Inputs Spy (Card B) \Agent A, Nonce Na\ \ set evs7F \ + | SR7Fake: "\ evs7F\ sr; Nonce Nb \ used evs7F; + illegalUse(Card B); + K = sesK(Nb,pairK(A,B)); + Key K \ used evs7F; + Inputs Spy (Card B) \Agent A, Nonce Na\ \ set evs7F \ \ Outpts (Card B) Spy \Nonce Nb, Key K, Crypt (pairK(A,B)) \Nonce Na, Nonce Nb\, Crypt (pairK(A,B)) (Nonce Nb)\ @@ -156,7 +155,7 @@ (*B TOWARDS A*) (*having sent an input that mentions A is the only memory B relies on, since the output doesn't mention A - lack of explicitness*) - SR8: "\ evs8\ sr; + | SR8: "\ evs8\ sr; Inputs B (Card B) \Agent A, Nonce Na\ \ set evs8; Outpts (Card B) B \Nonce Nb, Key K, Cert1, Cert2\ \ set evs8 \ @@ -168,7 +167,7 @@ (*A AND HER CARD*) (*A cannot check the form of the verifiers - although I can prove the form of Cert2 - and just feeds her card with what she's got*) - SR9: "\ evs9\ sr; legalUse(Card A); + | SR9: "\ evs9\ sr; legalUse(Card A); Gets A \Nonce Pk, Cert1\ \ set evs9; Outpts (Card A) A \Nonce Na, Cert2\ \ set evs9; Gets A \Nonce Nb, Cert3\ \ set evs9; @@ -179,7 +178,7 @@ # evs9 \ sr" (*But the card will only give outputs to the inputs of the correct form*) - SR10: "\ evs10\ sr; legalUse(Card A); A \ Server; + | SR10: "\ evs10\ sr; legalUse(Card A); A \ Server; K = sesK(Nb,pairK(A,B)); Inputs A (Card A) \Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)), @@ -193,16 +192,16 @@ (*The card can be exploited by the spy*) (*because of the assumptions on the card, A is certainly not server nor spy*) -SR10Fake: "\ evs10F\ sr; - illegalUse(Card A); - K = sesK(Nb,pairK(A,B)); - Inputs Spy (Card A) \Agent B, Nonce Na, Nonce Nb, - Nonce (Pairkey(A,B)), - Crypt (shrK A) \Nonce (Pairkey(A,B)), - Agent B\, - Crypt (pairK(A,B)) \Nonce Na, Nonce Nb\, - Crypt (crdK (Card A)) (Nonce Na)\ - \ set evs10F \ + | SR10Fake: "\ evs10F\ sr; + illegalUse(Card A); + K = sesK(Nb,pairK(A,B)); + Inputs Spy (Card A) \Agent B, Nonce Na, Nonce Nb, + Nonce (Pairkey(A,B)), + Crypt (shrK A) \Nonce (Pairkey(A,B)), + Agent B\, + Crypt (pairK(A,B)) \Nonce Na, Nonce Nb\, + Crypt (crdK (Card A)) (Nonce Na)\ + \ set evs10F \ \ Outpts (Card A) Spy \Key K, Crypt (pairK(A,B)) (Nonce Nb)\ # evs10F \ sr" @@ -212,7 +211,7 @@ (*A TOWARDS B*) (*having initiated with B is the only memory A relies on, since the output doesn't mention B - lack of explicitness*) - SR11: "\ evs11\ sr; + | SR11: "\ evs11\ sr; Says A Server \Agent A, Agent B\ \ set evs11; Outpts (Card A) A \Key K, Certificate\ \ set evs11 \ \ Says A B (Certificate) @@ -222,13 +221,13 @@ (*Both peers may leak by accident the session keys obtained from their cards*) - Oops1: + | Oops1: "\ evsO1 \ sr; Outpts (Card B) B \Nonce Nb, Key K, Certificate, Crypt (pairK(A,B)) (Nonce Nb)\ \ set evsO1 \ \ Notes Spy \Key K, Nonce Nb, Agent A, Agent B\ # evsO1 \ sr" - Oops2: + | Oops2: "\ evsO2 \ sr; Outpts (Card A) A \Key K, Crypt (pairK(A,B)) (Nonce Nb)\ \ set evsO2 \ diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Wed Jul 11 11:14:51 2007 +0200 @@ -42,15 +42,14 @@ ev \ set (tl (dropWhile (% z. z \ ev) evs))" -consts srb :: "event list set" -inductive "srb" - intros +inductive_set srb :: "event list set" + where Nil: "[]\ srb" - Fake: "\ evsF \ srb; X \ synth (analz (knows Spy evsF)); + | Fake: "\ evsF \ srb; X \ synth (analz (knows Spy evsF)); illegalUse(Card B) \ \ Says Spy A X # Inputs Spy (Card B) X # evsF \ srb" @@ -58,24 +57,24 @@ (*In general this rule causes the assumption Card B \ cloned in most guarantees for B - starting with confidentiality - otherwise pairK_confidential could not apply*) - Forge: + | Forge: "\ evsFo \ srb; Nonce Nb \ analz (knows Spy evsFo); Key (pairK(A,B)) \ knows Spy evsFo \ \ Notes Spy (Key (sesK(Nb,pairK(A,B)))) # evsFo \ srb" - Reception: "\ evsrb\ srb; Says A B X \ set evsrb \ + | Reception: "\ evsrb\ srb; Says A B X \ set evsrb \ \ Gets B X # evsrb \ srb" (*A AND THE SERVER*) - SR_U1: "\ evs1 \ srb; A \ Server \ + | SR_U1: "\ evs1 \ srb; A \ Server \ \ Says A Server \Agent A, Agent B\ # evs1 \ srb" - SR_U2: "\ evs2 \ srb; + | SR_U2: "\ evs2 \ srb; Gets Server \Agent A, Agent B\ \ set evs2 \ \ Says Server A \Nonce (Pairkey(A,B)), Crypt (shrK A) \Nonce (Pairkey(A,B)), Agent B\ @@ -88,7 +87,7 @@ (*A AND HER CARD*) (*A cannot decrypt the verifier for she dosn't know shrK A, but the pairkey is recognisable*) - SR_U3: "\ evs3 \ srb; legalUse(Card A); + | SR_U3: "\ evs3 \ srb; legalUse(Card A); Says A Server \Agent A, Agent B\ \ set evs3; Gets A \Nonce Pk, Certificate\ \ set evs3 \ \ Inputs A (Card A) (Agent A) @@ -99,7 +98,7 @@ the server*) (*The card outputs the nonce Na to A*) - SR_U4: "\ evs4 \ srb; + | SR_U4: "\ evs4 \ srb; Nonce Na \ used evs4; legalUse(Card A); A \ Server; Inputs A (Card A) (Agent A) \ set evs4 \ \ Outpts (Card A) A \Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\ @@ -107,7 +106,7 @@ (*The card can be exploited by the spy*) (*because of the assumptions on the card, A is certainly not server nor spy*) - SR_U4Fake: "\ evs4F \ srb; Nonce Na \ used evs4F; + | SR_U4Fake: "\ evs4F \ srb; Nonce Na \ used evs4F; illegalUse(Card A); Inputs Spy (Card A) (Agent A) \ set evs4F \ \ Outpts (Card A) Spy \Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\ @@ -117,7 +116,7 @@ (*A TOWARDS B*) - SR_U5: "\ evs5 \ srb; + | SR_U5: "\ evs5 \ srb; Outpts (Card A) A \Nonce Na, Certificate\ \ set evs5; \ p q. Certificate \ \p, q\ \ \ Says A B \Agent A, Nonce Na\ # evs5 \ srb" @@ -128,12 +127,12 @@ (*B AND HIS CARD*) - SR_U6: "\ evs6 \ srb; legalUse(Card B); + | SR_U6: "\ evs6 \ srb; legalUse(Card B); Gets B \Agent A, Nonce Na\ \ set evs6 \ \ Inputs B (Card B) \Agent A, Nonce Na\ # evs6 \ srb" (*B gets back from the card the session key and various verifiers*) - SR_U7: "\ evs7 \ srb; + | SR_U7: "\ evs7 \ srb; Nonce Nb \ used evs7; legalUse(Card B); B \ Server; K = sesK(Nb,pairK(A,B)); Key K \ used evs7; @@ -144,7 +143,7 @@ # evs7 \ srb" (*The card can be exploited by the spy*) (*because of the assumptions on the card, A is certainly not server nor spy*) - SR_U7Fake: "\ evs7F \ srb; Nonce Nb \ used evs7F; + | SR_U7Fake: "\ evs7F \ srb; Nonce Nb \ used evs7F; illegalUse(Card B); K = sesK(Nb,pairK(A,B)); Key K \ used evs7F; @@ -160,7 +159,7 @@ (*B TOWARDS A*) (*having sent an input that mentions A is the only memory B relies on, since the output doesn't mention A - lack of explicitness*) - SR_U8: "\ evs8 \ srb; + | SR_U8: "\ evs8 \ srb; Inputs B (Card B) \Agent A, Nonce Na\ \ set evs8; Outpts (Card B) B \Nonce Nb, Agent A, Key K, Cert1, Cert2\ \ set evs8 \ @@ -172,7 +171,7 @@ (*A AND HER CARD*) (*A cannot check the form of the verifiers - although I can prove the form of Cert2 - and just feeds her card with what she's got*) - SR_U9: "\ evs9 \ srb; legalUse(Card A); + | SR_U9: "\ evs9 \ srb; legalUse(Card A); Gets A \Nonce Pk, Cert1\ \ set evs9; Outpts (Card A) A \Nonce Na, Cert2\ \ set evs9; Gets A \Nonce Nb, Cert3\ \ set evs9; @@ -182,7 +181,7 @@ Cert1, Cert3, Cert2\ # evs9 \ srb" (*But the card will only give outputs to the inputs of the correct form*) - SR_U10: "\ evs10 \ srb; legalUse(Card A); A \ Server; + | SR_U10: "\ evs10 \ srb; legalUse(Card A); A \ Server; K = sesK(Nb,pairK(A,B)); Inputs A (Card A) \Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)), @@ -196,7 +195,7 @@ # evs10 \ srb" (*The card can be exploited by the spy*) (*because of the assumptions on the card, A is certainly not server nor spy*) -SR_U10Fake: "\ evs10F \ srb; + | SR_U10Fake: "\ evs10F \ srb; illegalUse(Card A); K = sesK(Nb,pairK(A,B)); Inputs Spy (Card A) \Agent B, Nonce Na, Nonce Nb, @@ -216,7 +215,7 @@ (*A TOWARDS B*) (*having initiated with B is the only memory A relies on, since the output doesn't mention B - lack of explicitness*) - SR_U11: "\ evs11 \ srb; + | SR_U11: "\ evs11 \ srb; Says A Server \Agent A, Agent B\ \ set evs11; Outpts (Card A) A \Agent B, Nonce Nb, Key K, Certificate\ \ set evs11 \ @@ -227,13 +226,13 @@ (*Both peers may leak by accident the session keys obtained from their cards*) - Oops1: + | Oops1: "\ evsO1 \ srb; Outpts (Card B) B \Nonce Nb, Agent A, Key K, Cert1, Cert2\ \ set evsO1 \ \ Notes Spy \Key K, Nonce Nb, Agent A, Agent B\ # evsO1 \ srb" - Oops2: + | Oops2: "\ evsO2 \ srb; Outpts (Card A) A \Agent B, Nonce Nb, Key K, Certificate\ \ set evsO2 \ diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/TLS.thy Wed Jul 11 11:14:51 2007 +0200 @@ -99,25 +99,24 @@ sessionK_neq_shrK [iff]: "sessionK nonces \ shrK A" -consts tls :: "event list set" -inductive tls - intros +inductive_set tls :: "event list set" + where Nil: --{*The initial, empty trace*} "[] \ tls" - Fake: --{*The Spy may say anything he can say. The sender field is correct, + | Fake: --{*The Spy may say anything he can say. The sender field is correct, but agents don't use that information.*} "[| evsf \ tls; X \ synth (analz (spies evsf)) |] ==> Says Spy B X # evsf \ tls" - SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK} + | SpyKeys: --{*The spy may apply @{term PRF} and @{term sessionK} to available nonces*} "[| evsSK \ tls; {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |] ==> Notes Spy {| Nonce (PRF(M,NA,NB)), Key (sessionK((NA,NB,M),role)) |} # evsSK \ tls" - ClientHello: + | ClientHello: --{*(7.4.1.2) PA represents @{text CLIENT_VERSION}, @{text CIPHER_SUITES} and @{text COMPRESSION_METHODS}. It is uninterpreted but will be confirmed in the FINISHED messages. @@ -129,7 +128,7 @@ ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|} # evsCH \ tls" - ServerHello: + | ServerHello: --{*7.4.1.3 of the TLS Internet-Draft PB represents @{text CLIENT_VERSION}, @{text CIPHER_SUITE} and @{text COMPRESSION_METHOD}. SERVER CERTIFICATE (7.4.2) is always present. @@ -139,11 +138,11 @@ \ set evsSH |] ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH \ tls" - Certificate: + | Certificate: --{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*} "evsC \ tls ==> Says B A (certificate B (pubK B)) # evsC \ tls" - ClientKeyExch: + | ClientKeyExch: --{*CLIENT KEY EXCHANGE (7.4.7). The client, A, chooses PMS, the PREMASTER SECRET. She encrypts PMS using the supplied KB, which ought to be pubK B. @@ -158,7 +157,7 @@ # Notes A {|Agent B, Nonce PMS|} # evsCX \ tls" - CertVerify: + | CertVerify: --{*The optional Certificate Verify (7.4.8) message contains the specific components listed in the security analysis, F.1.1.2. It adds the pre-master-secret, which is also essential! @@ -174,7 +173,7 @@ among other things. The master-secret is PRF(PMS,NA,NB). Either party may send its message first.*} - ClientFinished: + | ClientFinished: --{*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the rule's applying when the Spy has satisfied the "Says A B" by repaying messages sent by the true client; in that case, the @@ -193,7 +192,7 @@ Nonce NB, Number PB, Agent B|})) # evsCF \ tls" - ServerFinished: + | ServerFinished: --{*Keeping A' and A'' distinct means B cannot even check that the two messages originate from the same source. *} "[| evsSF \ tls; @@ -208,7 +207,7 @@ Nonce NB, Number PB, Agent B|})) # evsSF \ tls" - ClientAccepts: + | ClientAccepts: --{*Having transmitted ClientFinished and received an identical message encrypted with serverK, the client stores the parameters needed to resume this session. The "Notes A ..." premise is @@ -224,7 +223,7 @@ ==> Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA \ tls" - ServerAccepts: + | ServerAccepts: --{*Having transmitted ServerFinished and received an identical message encrypted with clientK, the server stores the parameters needed to resume this session. The "Says A'' B ..." premise is @@ -241,7 +240,7 @@ ==> Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA \ tls" - ClientResume: + | ClientResume: --{*If A recalls the @{text SESSION_ID}, then she sends a FINISHED message using the new nonces and stored MASTER SECRET.*} "[| evsCR \ tls; @@ -254,7 +253,7 @@ Nonce NB, Number PB, Agent B|})) # evsCR \ tls" - ServerResume: + | ServerResume: --{*Resumption (7.3): If B finds the @{text SESSION_ID} then he can send a FINISHED message using the recovered MASTER SECRET*} "[| evsSR \ tls; @@ -267,7 +266,7 @@ Nonce NB, Number PB, Agent B|})) # evsSR \ tls" - Oops: + | Oops: --{*The most plausible compromise is of an old session key. Losing the MASTER SECRET or PREMASTER SECRET is more serious but rather unlikely. The assumption @{term "A\Spy"} is essential: diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/WooLam.thy --- a/src/HOL/Auth/WooLam.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/WooLam.thy Wed Jul 11 11:14:51 2007 +0200 @@ -18,9 +18,8 @@ Computer Security Foundations Workshop *} -consts woolam :: "event list set" -inductive woolam - intros +inductive_set woolam :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ woolam" @@ -29,20 +28,20 @@ (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "[| evsf \ woolam; X \ synth (analz (spies evsf)) |] + | Fake: "[| evsf \ woolam; X \ synth (analz (spies evsf)) |] ==> Says Spy B X # evsf \ woolam" (*Alice initiates a protocol run*) - WL1: "evs1 \ woolam ==> Says A B (Agent A) # evs1 \ woolam" + | WL1: "evs1 \ woolam ==> Says A B (Agent A) # evs1 \ woolam" (*Bob responds to Alice's message with a challenge.*) - WL2: "[| evs2 \ woolam; Says A' B (Agent A) \ set evs2 |] + | WL2: "[| evs2 \ woolam; Says A' B (Agent A) \ set evs2 |] ==> Says B A (Nonce NB) # evs2 \ woolam" (*Alice responds to Bob's challenge by encrypting NB with her key. B is *not* properly determined -- Alice essentially broadcasts her reply.*) - WL3: "[| evs3 \ woolam; + | WL3: "[| evs3 \ woolam; Says A B (Agent A) \ set evs3; Says B' A (Nonce NB) \ set evs3 |] ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \ woolam" @@ -51,13 +50,13 @@ the messages are shown in chronological order, for clarity. But here, exchanging the two events would cause the lemma WL4_analz_spies to pick up the wrong assumption!*) - WL4: "[| evs4 \ woolam; + | WL4: "[| evs4 \ woolam; Says A' B X \ set evs4; Says A'' B (Agent A) \ set evs4 |] ==> Says B Server {|Agent A, Agent B, X|} # evs4 \ woolam" (*Server decrypts Alice's response for Bob.*) - WL5: "[| evs5 \ woolam; + | WL5: "[| evs5 \ woolam; Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ set evs5 |] ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Yahalom.thy Wed Jul 11 11:14:51 2007 +0200 @@ -15,29 +15,28 @@ This theory has the prototypical example of a secrecy relation, KeyCryptNonce. *} -consts yahalom :: "event list set" -inductive "yahalom" - intros +inductive_set yahalom :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ yahalom" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] + | Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ yahalom" (*A message that has been sent can be received by the intended recipient.*) - Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] + | Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] ==> Gets B X # evsr \ yahalom" (*Alice initiates a protocol run*) - YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] + | YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] ==> Says A B {|Agent A, Nonce NA|} # evs1 \ yahalom" (*Bob's response to Alice's message.*) - YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; + | YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; Gets B {|Agent A, Nonce NA|} \ set evs2 |] ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} @@ -45,7 +44,7 @@ (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a packet for forwarding to Bob.*) - YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; KAB \ symKeys; + | YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; KAB \ symKeys; Gets Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \ set evs3 |] @@ -54,7 +53,7 @@ Crypt (shrK B) {|Agent A, Key KAB|}|} # evs3 \ yahalom" - YM4: + | YM4: --{*Alice receives the Server's (?) message, checks her Nonce, and uses the new session key to send Bob his Nonce. The premise @{term "A \ Server"} is needed for @{text Says_Server_not_range}. @@ -68,7 +67,7 @@ (*This message models possible leaks of session keys. The Nonces identify the protocol run. Quoting Server here ensures they are correct.*) - Oops: "[| evso \ yahalom; + | Oops: "[| evso \ yahalom; Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} \ set evso |] diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Yahalom2.thy --- a/src/HOL/Auth/Yahalom2.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Yahalom2.thy Wed Jul 11 11:14:51 2007 +0200 @@ -19,29 +19,28 @@ This theory has the prototypical example of a secrecy relation, KeyCryptNonce. *} -consts yahalom :: "event list set" -inductive "yahalom" - intros +inductive_set yahalom :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ yahalom" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] + | Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ yahalom" (*A message that has been sent can be received by the intended recipient.*) - Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] + | Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] ==> Gets B X # evsr \ yahalom" (*Alice initiates a protocol run*) - YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] + | YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] ==> Says A B {|Agent A, Nonce NA|} # evs1 \ yahalom" (*Bob's response to Alice's message.*) - YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; + | YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; Gets B {|Agent A, Nonce NA|} \ set evs2 |] ==> Says B Server {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} @@ -50,7 +49,7 @@ (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a certificate for forwarding to Bob. Both agents are quoted in the 2nd certificate to prevent attacks!*) - YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; + | YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; Gets Server {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \ set evs3 |] @@ -62,7 +61,7 @@ (*Alice receives the Server's (?) message, checks her Nonce, and uses the new session key to send Bob his Nonce.*) - YM4: "[| evs4 \ yahalom; + | YM4: "[| evs4 \ yahalom; Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ set evs4; Says A B {|Agent A, Nonce NA|} \ set evs4 |] @@ -71,7 +70,7 @@ (*This message models possible leaks of session keys. The nonces identify the protocol run. Quoting Server here ensures they are correct. *) - Oops: "[| evso \ yahalom; + | Oops: "[| evso \ yahalom; Says Server A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \ set evso |] diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/Yahalom_Bad.thy --- a/src/HOL/Auth/Yahalom_Bad.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/Yahalom_Bad.thy Wed Jul 11 11:14:51 2007 +0200 @@ -14,29 +14,28 @@ The issues are discussed in lcp's LICS 2000 invited lecture. *} -consts yahalom :: "event list set" -inductive "yahalom" - intros +inductive_set yahalom :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ yahalom" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] + | Fake: "[| evsf \ yahalom; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ yahalom" (*A message that has been sent can be received by the intended recipient.*) - Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] + | Reception: "[| evsr \ yahalom; Says A B X \ set evsr |] ==> Gets B X # evsr \ yahalom" (*Alice initiates a protocol run*) - YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] + | YM1: "[| evs1 \ yahalom; Nonce NA \ used evs1 |] ==> Says A B {|Agent A, Nonce NA|} # evs1 \ yahalom" (*Bob's response to Alice's message.*) - YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; + | YM2: "[| evs2 \ yahalom; Nonce NB \ used evs2; Gets B {|Agent A, Nonce NA|} \ set evs2 |] ==> Says B Server {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} @@ -44,7 +43,7 @@ (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a packet for forwarding to Bob.*) - YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; KAB \ symKeys; + | YM3: "[| evs3 \ yahalom; Key KAB \ used evs3; KAB \ symKeys; Gets Server {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \ set evs3 |] @@ -56,7 +55,7 @@ (*Alice receives the Server's (?) message, checks her Nonce, and uses the new session key to send Bob his Nonce. The premise A \ Server is needed to prove Says_Server_not_range.*) - YM4: "[| evs4 \ yahalom; A \ Server; K \ symKeys; + | YM4: "[| evs4 \ yahalom; A \ Server; K \ symKeys; Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} \ set evs4; Says A B {|Agent A, Nonce NA|} \ set evs4 |] diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Auth/ZhouGollmann.thy --- a/src/HOL/Auth/ZhouGollmann.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Auth/ZhouGollmann.thy Wed Jul 11 11:14:51 2007 +0200 @@ -29,29 +29,27 @@ declare broken_def [simp] -consts zg :: "event list set" - -inductive zg - intros +inductive_set zg :: "event list set" + where Nil: "[] \ zg" - Fake: "[| evsf \ zg; X \ synth (analz (spies evsf)) |] +| Fake: "[| evsf \ zg; X \ synth (analz (spies evsf)) |] ==> Says Spy B X # evsf \ zg" -Reception: "[| evsr \ zg; Says A B X \ set evsr |] ==> Gets B X # evsr \ zg" +| Reception: "[| evsr \ zg; Says A B X \ set evsr |] ==> Gets B X # evsr \ zg" (*L is fresh for honest agents. We don't require K to be fresh because we don't bother to prove secrecy! We just assume that the protocol's objective is to deliver K fairly, rather than to keep M secret.*) - ZG1: "[| evs1 \ zg; Nonce L \ used evs1; C = Crypt K (Number m); +| ZG1: "[| evs1 \ zg; Nonce L \ used evs1; C = Crypt K (Number m); K \ symKeys; NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|] ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \ zg" (*B must check that NRO is A's signature to learn the sender's name*) - ZG2: "[| evs2 \ zg; +| ZG2: "[| evs2 \ zg; Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \ set evs2; NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}; NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|] @@ -59,7 +57,7 @@ (*A must check that NRR is B's signature to learn the sender's name; without spy, the matching label would be enough*) - ZG3: "[| evs3 \ zg; C = Crypt K M; K \ symKeys; +| ZG3: "[| evs3 \ zg; C = Crypt K M; K \ symKeys; Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \ set evs3; Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \ set evs3; NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}; @@ -73,7 +71,7 @@ give con_K to the Spy. This makes the threat model more dangerous, while also allowing lemma @{text Crypt_used_imp_spies} to omit the condition @{term "K \ priK TTP"}. *) - ZG4: "[| evs4 \ zg; K \ symKeys; +| ZG4: "[| evs4 \ zg; K \ symKeys; Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \ set evs4; sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; diff -r 28df61d931e2 -r a455e69c31cc src/HOL/HoareParallel/OG_Hoare.thy --- a/src/HOL/HoareParallel/OG_Hoare.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/HoareParallel/OG_Hoare.thy Wed Jul 11 11:14:51 2007 +0200 @@ -36,46 +36,40 @@ "interfree Ts \ \i j. i < length Ts \ j < length Ts \ i \ j \ interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) " -consts ann_hoare :: "('a ann_com \ 'a assn) set" -syntax "_ann_hoare" :: "'a ann_com \ 'a assn \ bool" ("(2\ _// _)" [60,90] 45) -translations "\ c q" \ "(c, q) \ ann_hoare" - -consts oghoare :: "('a assn \ 'a com \ 'a assn) set" -syntax "_oghoare" :: "'a assn \ 'a com \ 'a assn \ bool" ("(3\- _//_//_)" [90,55,90] 50) -translations "\- p c q" \ "(p, c, q) \ oghoare" - -inductive oghoare ann_hoare -intros +inductive + oghoare :: "'a assn \ 'a com \ 'a assn \ bool" ("(3\- _//_//_)" [90,55,90] 50) + and ann_hoare :: "'a ann_com \ 'a assn \ bool" ("(2\ _// _)" [60,90] 45) +where AnnBasic: "r \ {s. f s \ q} \ \ (AnnBasic r f) q" - AnnSeq: "\ \ c0 pre c1; \ c1 q \ \ \ (AnnSeq c0 c1) q" +| AnnSeq: "\ \ c0 pre c1; \ c1 q \ \ \ (AnnSeq c0 c1) q" - AnnCond1: "\ r \ b \ pre c1; \ c1 q; r \ -b \ pre c2; \ c2 q\ +| AnnCond1: "\ r \ b \ pre c1; \ c1 q; r \ -b \ pre c2; \ c2 q\ \ \ (AnnCond1 r b c1 c2) q" - AnnCond2: "\ r \ b \ pre c; \ c q; r \ -b \ q \ \ \ (AnnCond2 r b c) q" +| AnnCond2: "\ r \ b \ pre c; \ c q; r \ -b \ q \ \ \ (AnnCond2 r b c) q" - AnnWhile: "\ r \ i; i \ b \ pre c; \ c i; i \ -b \ q \ +| AnnWhile: "\ r \ i; i \ b \ pre c; \ c i; i \ -b \ q \ \ \ (AnnWhile r b i c) q" - AnnAwait: "\ atom_com c; \- (r \ b) c q \ \ \ (AnnAwait r b c) q" +| AnnAwait: "\ atom_com c; \- (r \ b) c q \ \ \ (AnnAwait r b c) q" - AnnConseq: "\\ c q; q \ q' \ \ \ c q'" +| AnnConseq: "\\ c q; q \ q' \ \ \ c q'" - Parallel: "\ \ic q. Ts!i = (Some c, q) \ \ c q; interfree Ts \ +| Parallel: "\ \ic q. Ts!i = (Some c, q) \ \ c q; interfree Ts \ \ \- (\i\{i. ii\{i. i- {s. f s \q} (Basic f) q" +| Basic: "\- {s. f s \q} (Basic f) q" - Seq: "\ \- p c1 r; \- r c2 q \ \ \- p (Seq c1 c2) q " +| Seq: "\ \- p c1 r; \- r c2 q \ \ \- p (Seq c1 c2) q " - Cond: "\ \- (p \ b) c1 q; \- (p \ -b) c2 q \ \ \- p (Cond b c1 c2) q" +| Cond: "\ \- (p \ b) c1 q; \- (p \ -b) c2 q \ \ \- p (Cond b c1 c2) q" - While: "\ \- (p \ b) c p \ \ \- p (While b i c) (p \ -b)" +| While: "\ \- (p \ b) c p \ \ \- p (While b i c) (p \ -b)" - Conseq: "\ p' \ p; \- p c q ; q \ q' \ \ \- p' c q'" +| Conseq: "\ p' \ p; \- p c q ; q \ q' \ \ \- p' c q'" section {* Soundness *} (* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE @@ -147,13 +141,13 @@ subsection {* Soundness of the System for Component Programs *} inductive_cases ann_transition_cases: - "(None,s) -1\ t" - "(Some (AnnBasic r f),s) -1\ t" - "(Some (AnnSeq c1 c2), s) -1\ t" - "(Some (AnnCond1 r b c1 c2), s) -1\ t" - "(Some (AnnCond2 r b c), s) -1\ t" - "(Some (AnnWhile r b I c), s) -1\ t" - "(Some (AnnAwait r b c),s) -1\ t" + "(None,s) -1\ (c', s')" + "(Some (AnnBasic r f),s) -1\ (c', s')" + "(Some (AnnSeq c1 c2), s) -1\ (c', s')" + "(Some (AnnCond1 r b c1 c2), s) -1\ (c', s')" + "(Some (AnnCond2 r b c), s) -1\ (c', s')" + "(Some (AnnWhile r b I c), s) -1\ (c', s')" + "(Some (AnnAwait r b c),s) -1\ (c', s')" text {* Strong Soundness for Component Programs:*} @@ -174,7 +168,7 @@ apply(clarify,simp,clarify,rule_tac x=qa in exI,fast) done -lemma Help: "(transition \ {(v,v,u). True}) = (transition)" +lemma Help: "(transition \ {(x,y). True}) = (transition)" apply force done @@ -412,7 +406,7 @@ apply clarify apply(drule Parallel_length_post_PStar) apply clarify -apply (ind_cases "(Parallel Ts, s) -P1\ (Parallel Rs, t)") +apply (ind_cases "(Parallel Ts, s) -P1\ (Parallel Rs, t)" for Ts s Rs t) apply(rule conjI) apply clarify apply(case_tac "i=j") diff -r 28df61d931e2 -r a455e69c31cc src/HOL/HoareParallel/OG_Tran.thy --- a/src/HOL/HoareParallel/OG_Tran.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/HoareParallel/OG_Tran.thy Wed Jul 11 11:14:51 2007 +0200 @@ -19,71 +19,72 @@ subsection {* The Transition Relation *} -consts +inductive_set ann_transition :: "(('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a)) set" - transition :: "(('a com \ 'a) \ ('a com \ 'a)) set" - -syntax - "_ann_transition" :: "('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a) \ bool" - ("_ -1\ _"[81,81] 100) - "_ann_transition_n" :: "('a ann_com_op \ 'a) \ nat \ ('a ann_com_op \ 'a) - \ bool" ("_ -_\ _"[81,81] 100) - "_ann_transition_*" :: "('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a) \ bool" - ("_ -*\ _"[81,81] 100) + and transition :: "(('a com \ 'a) \ ('a com \ 'a)) set" + and ann_transition' :: "('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a) \ bool" + ("_ -1\ _"[81,81] 100) + and transition' :: "('a com \ 'a) \ ('a com \ 'a) \ bool" + ("_ -P1\ _"[81,81] 100) + and transitions :: "('a com \ 'a) \ ('a com \ 'a) \ bool" + ("_ -P*\ _"[81,81] 100) +where + "con_0 -1\ con_1 \ (con_0, con_1) \ ann_transition" +| "con_0 -P1\ con_1 \ (con_0, con_1) \ transition" +| "con_0 -P*\ con_1 \ (con_0, con_1) \ transition\<^sup>*" + +| AnnBasic: "(Some (AnnBasic r f), s) -1\ (None, f s)" + +| AnnSeq1: "(Some c0, s) -1\ (None, t) \ + (Some (AnnSeq c0 c1), s) -1\ (Some c1, t)" +| AnnSeq2: "(Some c0, s) -1\ (Some c2, t) \ + (Some (AnnSeq c0 c1), s) -1\ (Some (AnnSeq c2 c1), t)" + +| AnnCond1T: "s \ b \ (Some (AnnCond1 r b c1 c2), s) -1\ (Some c1, s)" +| AnnCond1F: "s \ b \ (Some (AnnCond1 r b c1 c2), s) -1\ (Some c2, s)" - "_transition" :: "('a com \ 'a) \ ('a com \ 'a) \ bool" ("_ -P1\ _"[81,81] 100) - "_transition_n" :: "('a com \ 'a) \ nat \ ('a com \ 'a) \ bool" - ("_ -P_\ _"[81,81,81] 100) - "_transition_*" :: "('a com \ 'a) \ ('a com \ 'a) \ bool" ("_ -P*\ _"[81,81] 100) +| AnnCond2T: "s \ b \ (Some (AnnCond2 r b c), s) -1\ (Some c, s)" +| AnnCond2F: "s \ b \ (Some (AnnCond2 r b c), s) -1\ (None, s)" + +| AnnWhileF: "s \ b \ (Some (AnnWhile r b i c), s) -1\ (None, s)" +| AnnWhileT: "s \ b \ (Some (AnnWhile r b i c), s) -1\ + (Some (AnnSeq c (AnnWhile i b i c)), s)" + +| AnnAwait: "\ s \ b; atom_com c; (c, s) -P*\ (Parallel [], t) \ \ + (Some (AnnAwait r b c), s) -1\ (None, t)" + +| Parallel: "\ i (r, t) \ + \ (Parallel Ts, s) -P1\ (Parallel (Ts [i:=(r, q)]), t)" + +| Basic: "(Basic f, s) -P1\ (Parallel [], f s)" + +| Seq1: "All_None Ts \ (Seq (Parallel Ts) c, s) -P1\ (c, s)" +| Seq2: "(c0, s) -P1\ (c2, t) \ (Seq c0 c1, s) -P1\ (Seq c2 c1, t)" + +| CondT: "s \ b \ (Cond b c1 c2, s) -P1\ (c1, s)" +| CondF: "s \ b \ (Cond b c1 c2, s) -P1\ (c2, s)" + +| WhileF: "s \ b \ (While b i c, s) -P1\ (Parallel [], s)" +| WhileT: "s \ b \ (While b i c, s) -P1\ (Seq c (While b i c), s)" + +monos "rtrancl_mono" text {* The corresponding syntax translations are: *} -translations - "con_0 -1\ con_1" \ "(con_0, con_1) \ ann_transition" - "con_0 -n\ con_1" \ "(con_0, con_1) \ ann_transition^n" - "con_0 -*\ con_1" \ "(con_0, con_1) \ ann_transition\<^sup>*" - - "con_0 -P1\ con_1" \ "(con_0, con_1) \ transition" - "con_0 -Pn\ con_1" \ "(con_0, con_1) \ transition^n" - "con_0 -P*\ con_1" \ "(con_0, con_1) \ transition\<^sup>*" - -inductive ann_transition transition -intros - AnnBasic: "(Some (AnnBasic r f), s) -1\ (None, f s)" - - AnnSeq1: "(Some c0, s) -1\ (None, t) \ - (Some (AnnSeq c0 c1), s) -1\ (Some c1, t)" - AnnSeq2: "(Some c0, s) -1\ (Some c2, t) \ - (Some (AnnSeq c0 c1), s) -1\ (Some (AnnSeq c2 c1), t)" - - AnnCond1T: "s \ b \ (Some (AnnCond1 r b c1 c2), s) -1\ (Some c1, s)" - AnnCond1F: "s \ b \ (Some (AnnCond1 r b c1 c2), s) -1\ (Some c2, s)" +abbreviation + ann_transition_n :: "('a ann_com_op \ 'a) \ nat \ ('a ann_com_op \ 'a) + \ bool" ("_ -_\ _"[81,81] 100) where + "con_0 -n\ con_1 \ (con_0, con_1) \ ann_transition^n" - AnnCond2T: "s \ b \ (Some (AnnCond2 r b c), s) -1\ (Some c, s)" - AnnCond2F: "s \ b \ (Some (AnnCond2 r b c), s) -1\ (None, s)" - - AnnWhileF: "s \ b \ (Some (AnnWhile r b i c), s) -1\ (None, s)" - AnnWhileT: "s \ b \ (Some (AnnWhile r b i c), s) -1\ - (Some (AnnSeq c (AnnWhile i b i c)), s)" - - AnnAwait: "\ s \ b; atom_com c; (c, s) -P*\ (Parallel [], t) \ \ - (Some (AnnAwait r b c), s) -1\ (None, t)" - - Parallel: "\ i (r, t) \ - \ (Parallel Ts, s) -P1\ (Parallel (Ts [i:=(r, q)]), t)" +abbreviation + ann_transitions :: "('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a) \ bool" + ("_ -*\ _"[81,81] 100) where + "con_0 -*\ con_1 \ (con_0, con_1) \ ann_transition\<^sup>*" - Basic: "(Basic f, s) -P1\ (Parallel [], f s)" - - Seq1: "All_None Ts \ (Seq (Parallel Ts) c, s) -P1\ (c, s)" - Seq2: "(c0, s) -P1\ (c2, t) \ (Seq c0 c1, s) -P1\ (Seq c2 c1, t)" - - CondT: "s \ b \ (Cond b c1 c2, s) -P1\ (c1, s)" - CondF: "s \ b \ (Cond b c1 c2, s) -P1\ (c2, s)" - - WhileF: "s \ b \ (While b i c, s) -P1\ (Parallel [], s)" - WhileT: "s \ b \ (While b i c, s) -P1\ (Seq c (While b i c), s)" - -monos "rtrancl_mono" +abbreviation + transition_n :: "('a com \ 'a) \ nat \ ('a com \ 'a) \ bool" + ("_ -P_\ _"[81,81,81] 100) where + "con_0 -Pn\ con_1 \ (con_0, con_1) \ transition^n" subsection {* Definition of Semantics *} diff -r 28df61d931e2 -r a455e69c31cc src/HOL/HoareParallel/RG_Hoare.thy --- a/src/HOL/HoareParallel/RG_Hoare.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/HoareParallel/RG_Hoare.thy Wed Jul 11 11:14:51 2007 +0200 @@ -11,36 +11,31 @@ stable :: "'a set \ ('a \ 'a) set \ bool" "stable \ \f g. (\x y. x \ f \ (x, y) \ g \ y \ f)" -consts rghoare :: "('a rgformula) set" -syntax - "_rghoare" :: "['a com, 'a set, ('a \ 'a) set, ('a \ 'a) set, 'a set] \ bool" - ("\ _ sat [_, _, _, _]" [60,0,0,0,0] 45) -translations - "\ P sat [pre, rely, guar, post]" \ "(P, pre, rely, guar, post) \ rghoare" - -inductive rghoare -intros +inductive + rghoare :: "['a com, 'a set, ('a \ 'a) set, ('a \ 'a) set, 'a set] \ bool" + ("\ _ sat [_, _, _, _]" [60,0,0,0,0] 45) +where Basic: "\ pre \ {s. f s \ post}; {(s,t). s \ pre \ (t=f s \ t=s)} \ guar; stable pre rely; stable post rely \ \ \ Basic f sat [pre, rely, guar, post]" - Seq: "\ \ P sat [pre, rely, guar, mid]; \ Q sat [mid, rely, guar, post] \ +| Seq: "\ \ P sat [pre, rely, guar, mid]; \ Q sat [mid, rely, guar, post] \ \ \ Seq P Q sat [pre, rely, guar, post]" - Cond: "\ stable pre rely; \ P1 sat [pre \ b, rely, guar, post]; +| Cond: "\ stable pre rely; \ P1 sat [pre \ b, rely, guar, post]; \ P2 sat [pre \ -b, rely, guar, post]; \s. (s,s)\guar \ \ \ Cond b P1 P2 sat [pre, rely, guar, post]" - While: "\ stable pre rely; (pre \ -b) \ post; stable post rely; +| While: "\ stable pre rely; (pre \ -b) \ post; stable post rely; \ P sat [pre \ b, rely, guar, pre]; \s. (s,s)\guar \ \ \ While b P sat [pre, rely, guar, post]" - Await: "\ stable pre rely; stable post rely; +| Await: "\ stable pre rely; stable post rely; \V. \ P sat [pre \ b \ {V}, {(s, t). s = t}, UNIV, {s. (V, s) \ guar} \ post] \ \ \ Await b P sat [pre, rely, guar, post]" - Conseq: "\ pre \ pre'; rely \ rely'; guar' \ guar; post' \ post; +| Conseq: "\ pre \ pre'; rely \ rely'; guar' \ guar; post' \ post; \ P sat [pre', rely', guar', post'] \ \ \ P sat [pre, rely, guar, post]" @@ -60,14 +55,10 @@ types 'a par_rgformula = "('a rgformula) list \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set" -consts par_rghoare :: "('a par_rgformula) set" -syntax - "_par_rghoare" :: "('a rgformula) list \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set \ bool" ("\ _ SAT [_, _, _, _]" [60,0,0,0,0] 45) -translations - "\ Ps SAT [pre, rely, guar, post]" \ "(Ps, pre, rely, guar, post) \ par_rghoare" - -inductive par_rghoare -intros +inductive + par_rghoare :: "('a rgformula) list \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set \ bool" + ("\ _ SAT [_, _, _, _]" [60,0,0,0,0] 45) +where Parallel: "\ \i (\j\{j. j j\i}. Guar(xs!j)) \ Rely(xs!i); (\j\{j. j guar; @@ -113,22 +104,22 @@ lemma takecptn_is_cptn [rule_format, elim!]: "\j. c \ cptn \ take (Suc j) c \ cptn" apply(induct "c") - apply(force elim: cptn.elims) + apply(force elim: cptn.cases) apply clarify apply(case_tac j) apply simp apply(rule CptnOne) apply simp -apply(force intro:cptn.intros elim:cptn.elims) +apply(force intro:cptn.intros elim:cptn.cases) done lemma dropcptn_is_cptn [rule_format,elim!]: "\j cptn \ drop j c \ cptn" apply(induct "c") - apply(force elim: cptn.elims) + apply(force elim: cptn.cases) apply clarify apply(case_tac j,simp+) -apply(erule cptn.elims) +apply(erule cptn.cases) apply simp apply force apply force @@ -137,20 +128,20 @@ lemma takepar_cptn_is_par_cptn [rule_format,elim]: "\j. c \ par_cptn \ take (Suc j) c \ par_cptn" apply(induct "c") - apply(force elim: cptn.elims) + apply(force elim: cptn.cases) apply clarify apply(case_tac j,simp) apply(rule ParCptnOne) -apply(force intro:par_cptn.intros elim:par_cptn.elims) +apply(force intro:par_cptn.intros elim:par_cptn.cases) done lemma droppar_cptn_is_par_cptn [rule_format]: "\j par_cptn \ drop j c \ par_cptn" apply(induct "c") - apply(force elim: par_cptn.elims) + apply(force elim: par_cptn.cases) apply clarify apply(case_tac j,simp+) -apply(erule par_cptn.elims) +apply(erule par_cptn.cases) apply simp apply force apply force @@ -165,16 +156,16 @@ "\s. (None, s)#xs \ cptn \ (\i xs!i)" apply(induct xs,simp+) apply clarify -apply(erule cptn.elims,simp) +apply(erule cptn.cases,simp) apply simp apply(case_tac i,simp) apply(rule Env) apply simp -apply(force elim:ctran.elims) +apply(force elim:ctran.cases) done lemma cptn_not_empty [simp]:"[] \ cptn" -apply(force elim:cptn.elims) +apply(force elim:cptn.cases) done lemma etran_or_ctran [rule_format]: @@ -183,7 +174,7 @@ \ x!i -e\ x!Suc i" apply(induct x,simp) apply clarify -apply(erule cptn.elims,simp) +apply(erule cptn.cases,simp) apply(case_tac i,simp) apply(rule Env) apply simp @@ -202,10 +193,10 @@ apply(induct x) apply simp apply clarify -apply(erule cptn.elims,simp) +apply(erule cptn.cases,simp) apply(case_tac i,simp+) apply(case_tac i,simp) - apply(force elim:etran.elims) + apply(force elim:etran.cases) apply simp done @@ -221,7 +212,7 @@ "\ (None, s) # xs \cptn; i \ \ ((None, s) # xs) ! i -c\ xs ! i" apply(frule not_ctran_None,simp) apply(case_tac i,simp) - apply(force elim:etran.elims) + apply(force elim:etranE) apply simp apply(rule etran_or_ctran2_disjI2,simp_all) apply(force intro:tl_of_cptn_is_cptn) @@ -241,9 +232,9 @@ (\i. j\i \ i x!i -e\ x!Suc i) \ snd(x!k)\p \ fst(x!j)=fst(x!k)" apply(induct x) apply clarify - apply(force elim:cptn.elims) + apply(force elim:cptn.cases) apply clarify -apply(erule cptn.elims,simp) +apply(erule cptn.cases,simp) apply simp apply(case_tac k,simp,simp) apply(case_tac j,simp) @@ -274,7 +265,7 @@ apply(case_tac k,simp,simp) apply(case_tac j) apply(erule_tac x=0 and P="\j. (?H j) \ (?J j)\etran" in allE,simp) - apply(erule etran.elims,simp) + apply(erule etran.cases,simp) apply(erule_tac x="nata" in allE) apply(erule_tac x="nat" and P="\j. (?s\j) \ (?J j)" in allE,simp) apply(subgoal_tac "(\i. i < length xs \ ((Q, t) # xs) ! i -e\ xs ! i \ (snd (((Q, t) # xs) ! i), snd (xs ! i)) \ rely)") @@ -295,7 +286,7 @@ apply(induct x,simp) apply simp apply clarify -apply(erule cptn.elims,simp) +apply(erule cptn.cases,simp) apply(case_tac i,simp+) apply clarify apply(case_tac j,simp) @@ -305,12 +296,12 @@ apply simp apply(case_tac i) apply(case_tac j,simp,simp) - apply(erule ctran.elims,simp_all) + apply(erule ctran.cases,simp_all) apply(force elim: not_ctran_None) -apply(ind_cases "((Some (Basic f), sa), Q, t) \ ctran") +apply(ind_cases "((Some (Basic f), sa), Q, t) \ ctran" for sa Q t) apply simp apply(drule_tac i=nat in not_ctran_None,simp) -apply(erule etran.elims,simp) +apply(erule etranE,simp) done lemma exists_ctran_Basic_None [rule_format]: @@ -319,7 +310,7 @@ apply(induct x,simp) apply simp apply clarify -apply(erule cptn.elims,simp) +apply(erule cptn.cases,simp) apply(case_tac i,simp,simp) apply(erule_tac x=nat in allE,simp) apply clarify @@ -349,7 +340,7 @@ apply clarify apply(drule_tac s="Some (Basic f)" in sym,simp) apply(thin_tac "\j. ?H j") - apply(force elim:ctran.elims) + apply(force elim:ctran.cases) apply clarify apply(simp add:cp_def) apply clarify @@ -368,7 +359,7 @@ apply simp apply(drule_tac s="Some (Basic f)" in sym,simp) apply(case_tac "x!Suc j",simp) -apply(rule ctran.elims,simp) +apply(rule ctran.cases,simp) apply(simp_all) apply(drule_tac c=sa in subsetD,simp) apply clarify @@ -389,7 +380,7 @@ (\j. Suc j i\j \ x!j -e\ x!Suc j)" apply(induct x,simp+) apply clarify -apply(erule cptn.elims,simp) +apply(erule cptn.cases,simp) apply(case_tac i,simp+) apply clarify apply(case_tac j,simp) @@ -399,11 +390,11 @@ apply simp apply(case_tac i) apply(case_tac j,simp,simp) - apply(erule ctran.elims,simp_all) + apply(erule ctran.cases,simp_all) apply(force elim: not_ctran_None) -apply(ind_cases "((Some (Await b c), sa), Q, t) \ ctran",simp) +apply(ind_cases "((Some (Await b c), sa), Q, t) \ ctran" for sa Q t,simp) apply(drule_tac i=nat in not_ctran_None,simp) -apply(erule etran.elims,simp) +apply(erule etranE,simp) done lemma exists_ctran_Await_None [rule_format]: @@ -411,7 +402,7 @@ \ i fst(x!i)=None \ (\j x!Suc j)" apply(induct x,simp+) apply clarify -apply(erule cptn.elims,simp) +apply(erule cptn.cases,simp) apply(case_tac i,simp+) apply(erule_tac x=nat in allE,simp) apply clarify @@ -440,7 +431,7 @@ apply force apply(simp add:cp_def) apply(case_tac l) - apply(force elim:cptn.elims) + apply(force elim:cptn.cases) apply simp apply(erule CptnComp) apply clarify @@ -466,7 +457,7 @@ apply(erule_tac i=i in unique_ctran_Await,force,simp_all) apply(simp add:cp_def) --{* here starts the different part. *} - apply(erule ctran.elims,simp_all) + apply(erule ctran.cases,simp_all) apply(drule Star_imp_cptn) apply clarify apply(erule_tac x=sa in allE) @@ -476,7 +467,7 @@ apply (simp add:cp_def) apply clarify apply(erule_tac x=ia and P="\i. ?H i \ (?J i,?I i)\ctran" in allE,simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply simp apply clarify apply(simp add:cp_def) @@ -496,7 +487,7 @@ apply simp apply(drule_tac s="Some (Await b P)" in sym,simp) apply(case_tac "x!Suc j",simp) -apply(rule ctran.elims,simp) +apply(rule ctran.cases,simp) apply(simp_all) apply(drule Star_imp_cptn) apply clarify @@ -507,7 +498,7 @@ apply (simp add:cp_def) apply clarify apply(erule_tac x=i and P="\i. ?H i \ (?J i,?I i)\ctran" in allE,simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply simp apply clarify apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all) @@ -544,7 +535,7 @@ apply (simp add:assum_def) apply(frule_tac j=0 and k="m" and p=pre in stability,simp+) apply(erule_tac m="Suc m" in etran_or_ctran,simp+) -apply(erule ctran.elims,simp_all) +apply(erule ctran.cases,simp_all) apply(erule_tac x="sa" in allE) apply(drule_tac c="drop (Suc m) x" in subsetD) apply simp @@ -616,7 +607,7 @@ apply(simp (no_asm_use) add:lift_def) apply clarify apply(erule_tac x="Suc i" in allE, simp) - apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \ ctran") + apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \ ctran" for Pa sa t) apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def) apply(erule_tac x="length xs" in allE, simp) apply(simp only:Cons_lift_append) @@ -649,7 +640,7 @@ apply(rule conjI,erule CptnEnv) apply(simp (no_asm_use) add:lift_def) apply(rule_tac x=ys in exI,simp) -apply(ind_cases "((Some (Seq Pa Q), sa), t) \ ctran") +apply(ind_cases "((Some (Seq Pa Q), sa), t) \ ctran" for Pa sa t) apply simp apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp) apply(rule conjI) @@ -724,7 +715,7 @@ apply(erule_tac P="\j. ?H j \ ?J j \ ?I j" in allE,erule impE, assumption) apply(simp add:snd_lift) apply(erule mp) - apply(force elim:etran.elims intro:Env simp add:lift_def) + apply(force elim:etranE intro:Env simp add:lift_def) apply(simp add:comm_def) apply(rule conjI) apply clarify @@ -766,7 +757,7 @@ back apply(simp add:snd_lift) apply(erule mp) - apply(force elim:etran.elims intro:Env simp add:lift_def) + apply(force elim:etranE intro:Env simp add:lift_def) apply simp apply clarify apply(erule_tac x="snd(xs!m)" in allE) @@ -786,7 +777,7 @@ apply (case_tac i, (simp add:snd_lift)+) apply(erule mp) apply(case_tac "xs!m") - apply(force elim:etran.elims intro:Env simp add:lift_def) + apply(force elim:etran.cases intro:Env simp add:lift_def) apply simp apply simp apply clarify @@ -866,7 +857,7 @@ apply simp apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps) apply(erule mp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(case_tac "fst(((Some P, s) # xs) ! i)") apply(force intro:Env simp add:lift_def) apply(force intro:Env simp add:lift_def) @@ -900,7 +891,7 @@ apply(erule mp) apply(erule tl_of_assum_in_assum,simp) --{* While-None *} -apply(ind_cases "((Some (While b P), s), None, t) \ ctran") +apply(ind_cases "((Some (While b P), s), None, t) \ ctran" for s t) apply(simp add:comm_def) apply(simp add:cptn_iff_cptn_mod [THEN sym]) apply(rule conjI,clarify) @@ -909,7 +900,7 @@ apply(rule conjI, clarify) apply(case_tac i,simp,simp) apply(force simp add:not_ctran_None2) -apply(subgoal_tac "\i. Suc i < length ((None, sa) # xs) \ (((None, sa) # xs) ! i, ((None, sa) # xs) ! Suc i)\ etran") +apply(subgoal_tac "\i. Suc i < length ((None, t) # xs) \ (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)\ etran") prefer 2 apply clarify apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+) @@ -934,7 +925,7 @@ apply(case_tac "fst(((Some P, sa) # xs) ! i)") apply(case_tac "((Some P, sa) # xs) ! i") apply (simp add:lift_def) - apply(ind_cases "(Some (While b P), ba) -c\ t") + apply(ind_cases "(Some (While b P), ba) -c\ t" for ba t) apply simp apply simp apply(simp add:snd_lift del:map.simps) @@ -946,9 +937,9 @@ apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:map.simps) apply(erule mp) apply(case_tac "fst(((Some P, sa) # xs) ! ia)") - apply(erule etran.elims,simp add:lift_def) + apply(erule etranE,simp add:lift_def) apply(rule Env) - apply(erule etran.elims,simp add:lift_def) + apply(erule etranE,simp add:lift_def) apply(rule Env) apply (simp add:comm_def del:map.simps) apply clarify @@ -986,7 +977,7 @@ apply(case_tac "fst(((Some P, sa) # xs) ! i)") apply(case_tac "((Some P, sa) # xs) ! i") apply (simp add:lift_def del:last.simps) - apply(ind_cases "(Some (While b P), ba) -c\ t") + apply(ind_cases "(Some (While b P), ba) -c\ t" for ba t) apply simp apply simp apply(simp add:snd_lift del:map.simps last.simps) @@ -998,9 +989,9 @@ apply clarify apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:map.simps last.simps, erule mp) apply(case_tac "fst(((Some P, sa) # xs) ! ia)") - apply(erule etran.elims,simp add:lift_def) + apply(erule etranE,simp add:lift_def) apply(rule Env) - apply(erule etran.elims,simp add:lift_def) + apply(erule etranE,simp add:lift_def) apply(rule Env) apply (simp add:comm_def del:map.simps) apply clarify @@ -1158,9 +1149,9 @@ --{* a c-tran in some @{text "\_{ib}"} *} apply clarify apply(case_tac "i=ib",simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(erule_tac x="ib" and P="\i. ?H i \ (?I i) \ (?J i)" in allE) - apply (erule etran.elims) + apply (erule etranE) apply(case_tac "ia=m",simp) apply simp apply(erule_tac x=ia and P="\j. ?H j \ (\ i. ?P i j)" in allE) @@ -1198,7 +1189,7 @@ apply(force simp add:same_state_def par_assum_def) apply clarify apply(case_tac "i=ia",simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(erule_tac x="ia" and P="\i. ?H i \ (?I i) \ (?J i)" in allE,simp) apply(erule_tac x=j and P="\j. \i. ?S j i \ (?I j i, ?H j i)\ ctran \ (?P i j)" in allE) apply(erule_tac x=ia and P="\j. ?S j \ (?I j, ?H j)\ ctran \ (?P j)" in allE) @@ -1237,7 +1228,7 @@ apply clarify apply(erule_tac x=i and P="\j. ?H j \ fst(?I j)=(?J j)" in all_dupE) apply(erule_tac x="Suc i" and P="\j. ?H j \ fst(?I j)=(?J j)" in allE) -apply(erule par_ctran.elims,simp) +apply(erule par_ctranE,simp) apply(erule_tac x=i and P="\j. \i. ?S j i \ (?I j i, ?H j i)\ ctran \ (?P i j)" in allE) apply(erule_tac x=ia and P="\j. ?S j \ (?I j, ?H j)\ ctran \ (?P j)" in allE) apply(rule_tac x=ia in exI) @@ -1255,7 +1246,7 @@ done lemma parcptn_not_empty [simp]:"[] \ par_cptn" -apply(force elim:par_cptn.elims) +apply(force elim:par_cptn.cases) done lemma five: @@ -1336,12 +1327,12 @@ apply(case_tac list,simp,simp) apply(case_tac i) apply(simp add:par_cp_def ParallelCom_def) - apply(erule par_ctran.elims,simp) + apply(erule par_ctranE,simp) apply(simp add:par_cp_def ParallelCom_def) apply clarify -apply(erule par_cptn.elims,simp) +apply(erule par_cptn.cases,simp) apply simp -apply(erule par_ctran.elims) +apply(erule par_ctranE) back apply simp done diff -r 28df61d931e2 -r a455e69c31cc src/HOL/HoareParallel/RG_Tran.thy --- a/src/HOL/HoareParallel/RG_Tran.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/HoareParallel/RG_Tran.thy Wed Jul 11 11:14:51 2007 +0200 @@ -10,73 +10,76 @@ types 'a conf = "(('a com) option) \ 'a" -consts etran :: "('a conf \ 'a conf) set" -syntax "_etran" :: "'a conf \ 'a conf \ bool" ("_ -e\ _" [81,81] 80) -translations "P -e\ Q" \ "(P,Q) \ etran" -inductive etran -intros - Env: "(P, s) -e\ (P, t)" +inductive_set + etran :: "('a conf \ 'a conf) set" + and etran' :: "'a conf \ 'a conf \ bool" ("_ -e\ _" [81,81] 80) +where + "P -e\ Q \ (P,Q) \ etran" +| Env: "(P, s) -e\ (P, t)" + +lemma etranE: "c -e\ c' \ (\P s t. c = (P, s) \ c' = (P, t) \ Q) \ Q" + by (induct c, induct c', erule etran.cases, blast) subsubsection {* Component transitions *} -consts ctran :: "('a conf \ 'a conf) set" -syntax - "_ctran" :: "'a conf \ 'a conf \ bool" ("_ -c\ _" [81,81] 80) - "_ctran_*":: "'a conf \ 'a conf \ bool" ("_ -c*\ _" [81,81] 80) -translations - "P -c\ Q" \ "(P,Q) \ ctran" - "P -c*\ Q" \ "(P,Q) \ ctran^*" +inductive_set + ctran :: "('a conf \ 'a conf) set" + and ctran' :: "'a conf \ 'a conf \ bool" ("_ -c\ _" [81,81] 80) + and ctrans :: "'a conf \ 'a conf \ bool" ("_ -c*\ _" [81,81] 80) +where + "P -c\ Q \ (P,Q) \ ctran" +| "P -c*\ Q \ (P,Q) \ ctran^*" -inductive ctran -intros - Basic: "(Some(Basic f), s) -c\ (None, f s)" +| Basic: "(Some(Basic f), s) -c\ (None, f s)" - Seq1: "(Some P0, s) -c\ (None, t) \ (Some(Seq P0 P1), s) -c\ (Some P1, t)" +| Seq1: "(Some P0, s) -c\ (None, t) \ (Some(Seq P0 P1), s) -c\ (Some P1, t)" - Seq2: "(Some P0, s) -c\ (Some P2, t) \ (Some(Seq P0 P1), s) -c\ (Some(Seq P2 P1), t)" +| Seq2: "(Some P0, s) -c\ (Some P2, t) \ (Some(Seq P0 P1), s) -c\ (Some(Seq P2 P1), t)" - CondT: "s\b \ (Some(Cond b P1 P2), s) -c\ (Some P1, s)" - CondF: "s\b \ (Some(Cond b P1 P2), s) -c\ (Some P2, s)" +| CondT: "s\b \ (Some(Cond b P1 P2), s) -c\ (Some P1, s)" +| CondF: "s\b \ (Some(Cond b P1 P2), s) -c\ (Some P2, s)" - WhileF: "s\b \ (Some(While b P), s) -c\ (None, s)" - WhileT: "s\b \ (Some(While b P), s) -c\ (Some(Seq P (While b P)), s)" +| WhileF: "s\b \ (Some(While b P), s) -c\ (None, s)" +| WhileT: "s\b \ (Some(While b P), s) -c\ (Some(Seq P (While b P)), s)" - Await: "\s\b; (Some P, s) -c*\ (None, t)\ \ (Some(Await b P), s) -c\ (None, t)" +| Await: "\s\b; (Some P, s) -c*\ (None, t)\ \ (Some(Await b P), s) -c\ (None, t)" monos "rtrancl_mono" subsection {* Semantics of Parallel Programs *} types 'a par_conf = "('a par_com) \ 'a" -consts + +inductive_set par_etran :: "('a par_conf \ 'a par_conf) set" + and par_etran' :: "['a par_conf,'a par_conf] \ bool" ("_ -pe\ _" [81,81] 80) +where + "P -pe\ Q \ (P,Q) \ par_etran" +| ParEnv: "(Ps, s) -pe\ (Ps, t)" + +inductive_set par_ctran :: "('a par_conf \ 'a par_conf) set" -syntax - "_par_etran":: "['a par_conf,'a par_conf] \ bool" ("_ -pe\ _" [81,81] 80) - "_par_ctran":: "['a par_conf,'a par_conf] \ bool" ("_ -pc\ _" [81,81] 80) -translations - "P -pe\ Q" \ "(P,Q) \ par_etran" - "P -pc\ Q" \ "(P,Q) \ par_ctran" + and par_ctran' :: "['a par_conf,'a par_conf] \ bool" ("_ -pc\ _" [81,81] 80) +where + "P -pc\ Q \ (P,Q) \ par_ctran" +| ParComp: "\i (r, t)\ \ (Ps, s) -pc\ (Ps[i:=r], t)" -inductive par_etran -intros - ParEnv: "(Ps, s) -pe\ (Ps, t)" - -inductive par_ctran -intros - ParComp: "\i (r, t)\ \ (Ps, s) -pc\ (Ps[i:=r], t)" +lemma par_ctranE: "c -pc\ c' \ + (\i Ps s r t. c = (Ps, s) \ c' = (Ps[i := r], t) \ i < length Ps \ + (Ps ! i, s) -c\ (r, t) \ P) \ P" + by (induct c, induct c', erule par_ctran.cases, blast) subsection {* Computations *} subsubsection {* Sequential computations *} types 'a confs = "('a conf) list" -consts cptn :: "('a confs) set" -inductive "cptn" -intros + +inductive_set cptn :: "('a confs) set" +where CptnOne: "[(P,s)] \ cptn" - CptnEnv: "(P, t)#xs \ cptn \ (P,s)#(P,t)#xs \ cptn" - CptnComp: "\(P,s) -c\ (Q,t); (Q, t)#xs \ cptn \ \ (P,s)#(Q,t)#xs \ cptn" +| CptnEnv: "(P, t)#xs \ cptn \ (P,s)#(P,t)#xs \ cptn" +| CptnComp: "\(P,s) -c\ (Q,t); (Q, t)#xs \ cptn \ \ (P,s)#(Q,t)#xs \ cptn" constdefs cp :: "('a com) option \ 'a \ ('a confs) set" @@ -85,12 +88,12 @@ subsubsection {* Parallel computations *} types 'a par_confs = "('a par_conf) list" -consts par_cptn :: "('a par_confs) set" -inductive "par_cptn" -intros + +inductive_set par_cptn :: "('a par_confs) set" +where ParCptnOne: "[(P,s)] \ par_cptn" - ParCptnEnv: "(P,t)#xs \ par_cptn \ (P,s)#(P,t)#xs \ par_cptn" - ParCptnComp: "\ (P,s) -pc\ (Q,t); (Q,t)#xs \ par_cptn \ \ (P,s)#(Q,t)#xs \ par_cptn" +| ParCptnEnv: "(P,t)#xs \ par_cptn \ (P,s)#(P,t)#xs \ par_cptn" +| ParCptnComp: "\ (P,s) -pc\ (Q,t); (Q,t)#xs \ par_cptn \ \ (P,s)#(Q,t)#xs \ par_cptn" constdefs par_cp :: "'a par_com \ 'a \ ('a par_confs) set" @@ -102,25 +105,24 @@ lift :: "'a com \ 'a conf \ 'a conf" "lift Q \ \(P, s). (if P=None then (Some Q,s) else (Some(Seq (the P) Q), s))" -consts cptn_mod :: "('a confs) set" -inductive "cptn_mod" -intros +inductive_set cptn_mod :: "('a confs) set" +where CptnModOne: "[(P, s)] \ cptn_mod" - CptnModEnv: "(P, t)#xs \ cptn_mod \ (P, s)#(P, t)#xs \ cptn_mod" - CptnModNone: "\(Some P, s) -c\ (None, t); (None, t)#xs \ cptn_mod \ \ (Some P,s)#(None, t)#xs \cptn_mod" - CptnModCondT: "\(Some P0, s)#ys \ cptn_mod; s \ b \ \ (Some(Cond b P0 P1), s)#(Some P0, s)#ys \ cptn_mod" - CptnModCondF: "\(Some P1, s)#ys \ cptn_mod; s \ b \ \ (Some(Cond b P0 P1), s)#(Some P1, s)#ys \ cptn_mod" - CptnModSeq1: "\(Some P0, s)#xs \ cptn_mod; zs=map (lift P1) xs \ +| CptnModEnv: "(P, t)#xs \ cptn_mod \ (P, s)#(P, t)#xs \ cptn_mod" +| CptnModNone: "\(Some P, s) -c\ (None, t); (None, t)#xs \ cptn_mod \ \ (Some P,s)#(None, t)#xs \cptn_mod" +| CptnModCondT: "\(Some P0, s)#ys \ cptn_mod; s \ b \ \ (Some(Cond b P0 P1), s)#(Some P0, s)#ys \ cptn_mod" +| CptnModCondF: "\(Some P1, s)#ys \ cptn_mod; s \ b \ \ (Some(Cond b P0 P1), s)#(Some P1, s)#ys \ cptn_mod" +| CptnModSeq1: "\(Some P0, s)#xs \ cptn_mod; zs=map (lift P1) xs \ \ (Some(Seq P0 P1), s)#zs \ cptn_mod" - CptnModSeq2: +| CptnModSeq2: "\(Some P0, s)#xs \ cptn_mod; fst(last ((Some P0, s)#xs)) = None; (Some P1, snd(last ((Some P0, s)#xs)))#ys \ cptn_mod; zs=(map (lift P1) xs)@ys \ \ (Some(Seq P0 P1), s)#zs \ cptn_mod" - CptnModWhile1: +| CptnModWhile1: "\ (Some P, s)#xs \ cptn_mod; s \ b; zs=map (lift (While b P)) xs \ \ (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \ cptn_mod" - CptnModWhile2: +| CptnModWhile2: "\ (Some P, s)#xs \ cptn_mod; fst(last ((Some P, s)#xs))=None; s \ b; zs=(map (lift (While b P)) xs)@ys; (Some(While b P), snd(last ((Some P, s)#xs)))#ys \ cptn_mod\ @@ -169,7 +171,7 @@ apply simp apply(simp add:lift_def) apply clarify - apply(erule ctran.elims,simp_all) + apply(erule ctran.cases,simp_all) apply clarify apply(rule_tac x="xs" in exI) apply simp @@ -185,10 +187,10 @@ apply simp_all --{* basic *} apply clarify -apply(erule ctran.elims,simp_all) +apply(erule ctran.cases,simp_all) apply(rule CptnModNone,rule Basic,simp) apply clarify -apply(erule ctran.elims,simp_all) +apply(erule ctran.cases,simp_all) --{* Seq1 *} apply(rule_tac xs="[(None,ta)]" in CptnModSeq2) apply(erule CptnModNone) @@ -216,12 +218,12 @@ apply(simp add:lift_def) --{* Cond *} apply clarify -apply(erule ctran.elims,simp_all) +apply(erule ctran.cases,simp_all) apply(force elim: CptnModCondT) apply(force elim: CptnModCondF) --{* While *} apply clarify -apply(erule ctran.elims,simp_all) +apply(erule ctran.cases,simp_all) apply(rule CptnModNone,erule WhileF,simp) apply(drule div_seq,force) apply clarify @@ -231,7 +233,7 @@ apply(force simp add:last_length elim:CptnModWhile2) --{* await *} apply clarify -apply(erule ctran.elims,simp_all) +apply(erule ctran.cases,simp_all) apply(rule CptnModNone,erule Await,simp+) done @@ -241,7 +243,7 @@ apply(erule CptnModEnv) apply(case_tac P) apply simp - apply(erule ctran.elims,simp_all) + apply(erule ctran.cases,simp_all) apply(force elim:cptn_onlyif_cptn_mod_aux) done @@ -249,7 +251,7 @@ apply(erule cptn.induct) apply(force simp add:lift_def CptnOne) apply(force intro:CptnEnv simp add:lift_def) -apply(force simp add:lift_def intro:CptnComp Seq2 Seq1 elim:ctran.elims) +apply(force simp add:lift_def intro:CptnComp Seq2 Seq1 elim:ctran.cases) done lemma cptn_append_is_cptn [rule_format]: @@ -257,7 +259,7 @@ apply(induct c1) apply simp apply clarify -apply(erule cptn.elims,simp_all) +apply(erule cptn.cases,simp_all) apply(force intro:CptnEnv) apply(force elim:CptnComp) done @@ -309,7 +311,7 @@ apply(rule CptnComp) apply(erule CondF,simp) --{* Seq1 *} -apply(erule cptn.elims,simp_all) +apply(erule cptn.cases,simp_all) apply(rule CptnOne) apply clarify apply(drule_tac P=P1 in lift_is_cptn) @@ -495,10 +497,10 @@ seq_not_eq1 [THEN not_sym] seq_not_eq2 [THEN not_sym] if_not_eq1 if_not_eq2 if_not_eq1 [THEN not_sym] if_not_eq2 [THEN not_sym] -lemma prog_not_eq_in_ctran_aux [rule_format]: "(P,s) -c\ (Q,t) \ (P\Q)" -apply(erule ctran.induct) -apply simp_all -done +lemma prog_not_eq_in_ctran_aux: + assumes c: "(P,s) -c\ (Q,t)" + shows "P\Q" using c + by (induct x1 \ "(P,s)" x2 \ "(Q,t)" arbitrary: P s Q t) auto lemma prog_not_eq_in_ctran [simp]: "\ (P,s) -c\ (P,t)" apply clarify @@ -522,7 +524,7 @@ done lemma tl_in_cptn: "\ a#xs \cptn; xs\[] \ \ xs\cptn" -apply(force elim:cptn.elims) +apply(force elim:cptn.cases) done lemma tl_zero[rule_format]: @@ -562,7 +564,7 @@ apply(case_tac "i=ia",simp,simp) apply(erule_tac x=ia and P="\j. ?H j \ ?I j \ ?J j" in allE) apply(drule_tac t=i in not_sym,simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(rule ParCptnComp) apply(erule ParComp,simp) --{* applying the induction hypothesis *} @@ -584,7 +586,7 @@ erule_tac x=1 and P="\j. ?H j \ (snd (?d j))=(snd (?e j))" in allE) apply(erule_tac x=ia and P="\j. ?H j \ ?I j \ ?J j" in allE) apply(drule_tac t=i in not_sym,simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(erule allE,erule impE,assumption,erule tl_in_cptn) apply(force simp add:same_length_def length_Suc_conv) apply(simp add:same_length_def same_state_def) @@ -620,7 +622,7 @@ apply(rule tl_zero) apply(erule_tac x=l in allE, erule impE, assumption, erule_tac x=1 and P="\j. (?H j) \ (snd (?d j))=(snd (?e j))" in allE,simp) - apply(force elim:etran.elims intro:Env) + apply(force elim:etranE intro:Env) apply force apply force apply simp @@ -637,7 +639,7 @@ erule_tac x=1 and P="\j. ?H j \ (snd (?d j))=(snd (?e j))" in allE) apply(erule_tac x=ia and P="\j. ?H j \ ?I j \ ?J j" in allE) apply(drule_tac t=i in not_sym,simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(erule tl_zero) apply force apply force @@ -654,7 +656,7 @@ apply(erule_tac x=l in allE, erule impE, assumption, erule_tac x=1 and P="\j. ?H j \ (snd (?d j))=(snd (?e j))" in allE) apply(erule_tac x=l and P="\j. ?H j \ ?I j \ ?J j" in allE,erule impE, assumption,simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(rule tl_zero) apply force apply force @@ -668,7 +670,7 @@ apply(erule_tac x=ia in allE, erule impE, assumption, erule_tac x=1 and P="\j. ?H j \ (snd (?d j))=(snd (?e j))" in allE) apply(erule_tac x=ia and P="\j. ?H j \ ?I j \ ?J j" in allE,erule impE, assumption,simp) - apply(force elim:etran.elims intro:Env) + apply(force elim:etranE intro:Env) apply force apply(erule_tac x=ia and P="\j. ?H j \ (length (?s j) = ?t)" in allE,force) apply simp @@ -681,7 +683,7 @@ apply(erule_tac x=ia and P="\j. ?H j \ (length (?s j) = ?t)" in allE,force) --{* first step is an environmental step *} apply clarify -apply(erule par_etran.elims) +apply(erule par_etran.cases) apply simp apply(rule ParCptnEnv) apply(erule_tac x="Ps" in allE) @@ -691,14 +693,14 @@ apply(rule conjI) apply clarify apply(erule_tac x=i and P="\j. ?H j \ (?I ?s j) \ cptn" in allE,simp) - apply(erule cptn.elims) + apply(erule cptn.cases) apply(simp add:same_length_def) apply(erule_tac x=i and P="\j. ?H j \ (length (?s j) = ?t)" in allE,force) apply(simp add:same_state_def) apply(erule_tac x=i in allE, erule impE, assumption, erule_tac x=1 and P="\j. ?H j \ (snd (?d j))=(snd (?e j))" in allE,simp) apply(erule_tac x=i and P="\j. ?H j \ ?J j \etran" in allE,simp) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(simp add:same_state_def same_length_def) apply(rule conjI,clarify) apply(case_tac j,simp,simp) @@ -725,7 +727,7 @@ apply(rule_tac x=i in exI,simp) apply(rule conjI) apply(erule_tac x=i and P="\i. ?H i \ ?J i \etran" in allE, erule impE, assumption) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(erule_tac x=i in allE, erule impE, assumption, erule_tac x=1 and P="\j. (?H j) \ (snd (?d j))=(snd (?e j))" in allE,simp) apply(rule nth_tl_if) @@ -735,7 +737,7 @@ apply(erule_tac x=i and P="\j. ?H j \ (length (?s j) = ?t)" in allE,force) apply clarify apply(erule_tac x=l and P="\i. ?H i \ ?J i \etran" in allE, erule impE, assumption) - apply(erule etran.elims,simp) + apply(erule etranE,simp) apply(erule_tac x=l in allE, erule impE, assumption, erule_tac x=1 and P="\j. (?H j) \ (snd (?d j))=(snd (?e j))" in allE,simp) apply(rule nth_tl_if) @@ -751,7 +753,7 @@ apply(rule tl_zero) apply(erule_tac x=i and P="\i. ?H i \ ?J i \etran" in allE, erule impE, assumption) apply(erule_tac x=i and P="\i. ?H i \ ?J i \etran" in allE, erule impE, assumption) - apply(force elim:etran.elims intro:Env) + apply(force elim:etranE intro:Env) apply force apply(erule_tac x=i and P="\j. ?H j \ (length (?s j) = ?t)" in allE,force) apply simp @@ -778,7 +780,7 @@ apply(rule nth_equalityI,simp,simp) apply(force intro: cptn.intros) apply(clarify) -apply(erule par_cptn.elims,simp) +apply(erule par_cptn.cases,simp) apply simp apply(erule_tac x="xs" in allE) apply(erule_tac x="t" in allE,simp) @@ -811,7 +813,7 @@ apply clarify apply(rule_tac x=i in exI,simp) apply force -apply(erule par_ctran.elims,simp) +apply(erule par_ctran.cases,simp) apply(erule_tac x="Ps[i:=r]" in allE) apply(erule_tac x="ta" in allE,simp) apply clarify @@ -887,7 +889,7 @@ apply(clarify) apply(simp add:par_cp_def cp_def) apply(case_tac x) - apply(force elim:par_cptn.elims) + apply(force elim:par_cptn.cases) apply simp apply(erule_tac x="list" in allE) apply clarify @@ -899,7 +901,7 @@ apply(erule_tac x=0 in allE) apply(simp add:cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def) apply clarify - apply(erule cptn.elims,force,force,force) + apply(erule cptn.cases,force,force,force) apply(simp add:par_cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def) apply clarify apply(erule_tac x=0 and P="\j. ?H j \ (length (?s j) = ?t)" in all_dupE) diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Compiler.thy --- a/src/HOL/IMP/Compiler.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Compiler.thy Wed Jul 11 11:14:51 2007 +0200 @@ -54,7 +54,7 @@ text {* The other direction! *} -inductive_cases [elim!]: "(([],p,s),next) : stepa1" +inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1" lemma [simp]: "(\[],q,s\ -n\ \p',q',t\) = (n=0 \ p' = [] \ q' = q \ t = s)" apply(rule iffI) diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Compiler0.thy --- a/src/HOL/IMP/Compiler0.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Compiler0.thy Wed Jul 11 11:14:51 2007 +0200 @@ -20,48 +20,32 @@ text {* We describe execution of programs in the machine by an operational (small step) semantics: *} -consts stepa1 :: "instr list \ ((state\nat) \ (state\nat))set" - -syntax - "_stepa1" :: "[instr list,state,nat,state,nat] \ bool" - ("_ |- (3<_,_>/ -1-> <_,_>)" [50,0,0,0,0] 50) - "_stepa" :: "[instr list,state,nat,state,nat] \ bool" - ("_ |-/ (3<_,_>/ -*-> <_,_>)" [50,0,0,0,0] 50) - - "_stepan" :: "[instr list,state,nat,nat,state,nat] \ bool" - ("_ |-/ (3<_,_>/ -(_)-> <_,_>)" [50,0,0,0,0,0] 50) - -syntax (xsymbols) - "_stepa1" :: "[instr list,state,nat,state,nat] \ bool" - ("_ \ (3\_,_\/ -1\ \_,_\)" [50,0,0,0,0] 50) - "_stepa" :: "[instr list,state,nat,state,nat] \ bool" - ("_ \/ (3\_,_\/ -*\ \_,_\)" [50,0,0,0,0] 50) - "_stepan" :: "[instr list,state,nat,nat,state,nat] \ bool" - ("_ \/ (3\_,_\/ -(_)\ \_,_\)" [50,0,0,0,0,0] 50) -syntax (HTML output) - "_stepa1" :: "[instr list,state,nat,state,nat] \ bool" - ("_ |- (3\_,_\/ -1\ \_,_\)" [50,0,0,0,0] 50) - "_stepa" :: "[instr list,state,nat,state,nat] \ bool" - ("_ |-/ (3\_,_\/ -*\ \_,_\)" [50,0,0,0,0] 50) - "_stepan" :: "[instr list,state,nat,nat,state,nat] \ bool" - ("_ |-/ (3\_,_\/ -(_)\ \_,_\)" [50,0,0,0,0,0] 50) +inductive_set + stepa1 :: "instr list \ ((state\nat) \ (state\nat))set" + and stepa1' :: "[instr list,state,nat,state,nat] \ bool" + ("_ \ (3\_,_\/ -1\ \_,_\)" [50,0,0,0,0] 50) + for P :: "instr list" +where + "P \ \s,m\ -1\ \t,n\ == ((s,m),t,n) : stepa1 P" +| ASIN[simp]: + "\ n \ P \ \s,n\ -1\ \s[x\ a s],Suc n\" +| JMPFT[simp,intro]: + "\ n \ P \ \s,n\ -1\ \s,Suc n\" +| JMPFF[simp,intro]: + "\ n \ P \ \s,n\ -1\ \s,m\" +| JMPB[simp]: + "\ n \ P \ \s,n\ -1\ \s,j\" -translations - "P \ \s,m\ -1\ \t,n\" == "((s,m),t,n) : stepa1 P" - "P \ \s,m\ -*\ \t,n\" == "((s,m),t,n) : ((stepa1 P)^*)" - "P \ \s,m\ -(i)\ \t,n\" == "((s,m),t,n) : ((stepa1 P)^i)" +abbreviation + stepa :: "[instr list,state,nat,state,nat] \ bool" + ("_ \/ (3\_,_\/ -*\ \_,_\)" [50,0,0,0,0] 50) where + "P \ \s,m\ -*\ \t,n\ == ((s,m),t,n) : ((stepa1 P)^*)" -inductive "stepa1 P" -intros -ASIN[simp]: - "\ n \ P \ \s,n\ -1\ \s[x\ a s],Suc n\" -JMPFT[simp,intro]: - "\ n \ P \ \s,n\ -1\ \s,Suc n\" -JMPFF[simp,intro]: - "\ n \ P \ \s,n\ -1\ \s,m\" -JMPB[simp]: - "\ n \ P \ \s,n\ -1\ \s,j\" +abbreviation + stepan :: "[instr list,state,nat,nat,state,nat] \ bool" + ("_ \/ (3\_,_\/ -(_)\ \_,_\)" [50,0,0,0,0,0] 50) where + "P \ \s,m\ -(i)\ \t,n\ == ((s,m),t,n) : ((stepa1 P)^i)" subsection "The compiler" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Denotation.thy --- a/src/HOL/IMP/Denotation.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Denotation.thy Wed Jul 11 11:14:51 2007 +0200 @@ -62,7 +62,7 @@ apply fast (* while *) -apply (erule lfp_induct_set [OF _ Gamma_mono]) +apply (erule lfp_induct2 [OF _ Gamma_mono]) apply (unfold Gamma_def) apply fast done diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Expr.thy --- a/src/HOL/IMP/Expr.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Expr.thy Wed Jul 11 11:14:51 2007 +0200 @@ -26,16 +26,14 @@ | Op2 "nat => nat => nat" aexp aexp subsection "Evaluation of arithmetic expressions" -consts evala :: "((aexp*state) * nat) set" -syntax "_evala" :: "[aexp*state,nat] => bool" (infixl "-a->" 50) -translations - "aesig -a-> n" == "(aesig,n) : evala" -inductive evala - intros + +inductive + evala :: "[aexp*state,nat] => bool" (infixl "-a->" 50) +where N: "(N(n),s) -a-> n" - X: "(X(x),s) -a-> s(x)" - Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)" - Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |] +| X: "(X(x),s) -a-> s(x)" +| Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)" +| Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |] ==> (Op2 f e0 e1,s) -a-> f n0 n1" lemmas [intro] = N X Op1 Op2 @@ -52,23 +50,19 @@ | ori bexp bexp (infixl "ori" 60) subsection "Evaluation of boolean expressions" -consts evalb :: "((bexp*state) * bool)set" -syntax "_evalb" :: "[bexp*state,bool] => bool" (infixl "-b->" 50) -translations - "besig -b-> b" == "(besig,b) : evalb" - -inductive evalb +inductive + evalb :: "[bexp*state,bool] => bool" (infixl "-b->" 50) -- "avoid clash with ML constructors true, false" - intros +where tru: "(true,s) -b-> True" - fls: "(false,s) -b-> False" - ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] +| fls: "(false,s) -b-> False" +| ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] ==> (ROp f a0 a1,s) -b-> f n0 n1" - noti: "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)" - andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] +| noti: "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)" +| andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] ==> (b0 andi b1,s) -b-> (w0 & w1)" - ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] +| ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] ==> (b0 ori b1,s) -b-> (w0 | w1)" lemmas [intro] = tru fls ROp noti andi ori @@ -117,21 +111,21 @@ lemma [simp]: "((ROp f a0 a1,sigma) -b-> w) = (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))" - by (rule,cases set: evalb) auto + by (rule,cases set: evalb) blast+ lemma [simp]: "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))" - by (rule,cases set: evalb) auto + by (rule,cases set: evalb) blast+ lemma [simp]: "((b0 andi b1,sigma) -b-> w) = (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))" - by (rule,cases set: evalb) auto + by (rule,cases set: evalb) blast+ lemma [simp]: "((b0 ori b1,sigma) -b-> w) = (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))" - by (rule,cases set: evalb) auto + by (rule,cases set: evalb) blast+ lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Hoare.thy --- a/src/HOL/IMP/Hoare.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Hoare.thy Wed Jul 11 11:14:51 2007 +0200 @@ -13,20 +13,17 @@ constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t" -consts hoare :: "(assn * com * assn) set" -syntax "_hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) -translations "|- {P}c{Q}" == "(P,c,Q) : hoare" - -inductive hoare -intros +inductive + hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) +where skip: "|- {P}\{P}" - ass: "|- {%s. P(s[x\a s])} x:==a {P}" - semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}" - If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==> +| ass: "|- {%s. P(s[x\a s])} x:==a {P}" +| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}" +| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==> |- {P} \ b \ c \ d {Q}" - While: "|- {%s. P s & b s} c {P} ==> +| While: "|- {%s. P s & b s} c {P} ==> |- {P} \ b \ c {%s. P s & ~b s}" - conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==> +| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P'}c{Q'}" constdefs wp :: "com => assn => assn" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Machines.thy --- a/src/HOL/IMP/Machines.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Machines.thy Wed Jul 11 11:14:51 2007 +0200 @@ -36,43 +36,28 @@ subsection "M0 with PC" -consts exec01 :: "instr list \ ((nat\state) \ (nat\state))set" -syntax - "_exec01" :: "[instrs, nat,state, nat,state] \ bool" - ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50) - "_exec0s" :: "[instrs, nat,state, nat,state] \ bool" - ("(_/ |- (1<_,/_>)/ -*-> (1<_,/_>))" [50,0,0,0,0] 50) - "_exec0n" :: "[instrs, nat,state, nat, nat,state] \ bool" - ("(_/ |- (1<_,/_>)/ -_-> (1<_,/_>))" [50,0,0,0,0] 50) - -syntax (xsymbols) - "_exec01" :: "[instrs, nat,state, nat,state] \ bool" - ("(_/ \ (1\_,/_\)/ -1\ (1\_,/_\))" [50,0,0,0,0] 50) - "_exec0s" :: "[instrs, nat,state, nat,state] \ bool" - ("(_/ \ (1\_,/_\)/ -*\ (1\_,/_\))" [50,0,0,0,0] 50) - "_exec0n" :: "[instrs, nat,state, nat, nat,state] \ bool" - ("(_/ \ (1\_,/_\)/ -_\ (1\_,/_\))" [50,0,0,0,0] 50) +inductive_set + exec01 :: "instr list \ ((nat\state) \ (nat\state))set" + and exec01' :: "[instrs, nat,state, nat,state] \ bool" + ("(_/ \ (1\_,/_\)/ -1\ (1\_,/_\))" [50,0,0,0,0] 50) + for P :: "instr list" +where + "p \ \i,s\ -1\ \j,t\ == ((i,s),j,t) : (exec01 p)" +| SET: "\ n \ P \ \n,s\ -1\ \Suc n,s[x\ a s]\" +| JMPFT: "\ n \ P \ \n,s\ -1\ \Suc n,s\" +| JMPFF: "\ nb s; m=n+i+1; m \ size P \ + \ P \ \n,s\ -1\ \m,s\" +| JMPB: "\ n n; j = n-i \ \ P \ \n,s\ -1\ \j,s\" -syntax (HTML output) - "_exec01" :: "[instrs, nat,state, nat,state] \ bool" - ("(_/ |- (1\_,/_\)/ -1\ (1\_,/_\))" [50,0,0,0,0] 50) - "_exec0s" :: "[instrs, nat,state, nat,state] \ bool" - ("(_/ |- (1\_,/_\)/ -*\ (1\_,/_\))" [50,0,0,0,0] 50) - "_exec0n" :: "[instrs, nat,state, nat, nat,state] \ bool" - ("(_/ |- (1\_,/_\)/ -_\ (1\_,/_\))" [50,0,0,0,0] 50) +abbreviation + exec0s :: "[instrs, nat,state, nat,state] \ bool" + ("(_/ \ (1\_,/_\)/ -*\ (1\_,/_\))" [50,0,0,0,0] 50) where + "p \ \i,s\ -*\ \j,t\ == ((i,s),j,t) : (exec01 p)^*" -translations - "p \ \i,s\ -1\ \j,t\" == "((i,s),j,t) : (exec01 p)" - "p \ \i,s\ -*\ \j,t\" == "((i,s),j,t) : (exec01 p)^*" - "p \ \i,s\ -n\ \j,t\" == "((i,s),j,t) : (exec01 p)^n" - -inductive "exec01 P" -intros -SET: "\ n \ P \ \n,s\ -1\ \Suc n,s[x\ a s]\" -JMPFT: "\ n \ P \ \n,s\ -1\ \Suc n,s\" -JMPFF: "\ nb s; m=n+i+1; m \ size P \ - \ P \ \n,s\ -1\ \m,s\" -JMPB: "\ n n; j = n-i \ \ P \ \n,s\ -1\ \j,s\" +abbreviation + exec0n :: "[instrs, nat,state, nat, nat,state] \ bool" + ("(_/ \ (1\_,/_\)/ -_\ (1\_,/_\))" [50,0,0,0,0] 50) where + "p \ \i,s\ -n\ \j,t\ == ((i,s),j,t) : (exec01 p)^n" subsection "M0 with lists" @@ -82,40 +67,31 @@ types config = "instrs \ instrs \ state" -consts stepa1 :: "(config \ config)set" -syntax - "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \ bool" - ("((1<_,/_,/_>)/ -1-> (1<_,/_,/_>))" 50) - "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \ bool" - ("((1<_,/_,/_>)/ -*-> (1<_,/_,/_>))" 50) - "_stepan" :: "[state,instrs,instrs, nat, instrs,instrs,state] \ bool" - ("((1<_,/_,/_>)/ -_-> (1<_,/_,/_>))" 50) - -syntax (xsymbols) - "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \ bool" - ("((1\_,/_,/_\)/ -1\ (1\_,/_,/_\))" 50) - "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \ bool" - ("((1\_,/_,/_\)/ -*\ (1\_,/_,/_\))" 50) - "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \ bool" - ("((1\_,/_,/_\)/ -_\ (1\_,/_,/_\))" 50) - -translations - "\p,q,s\ -1\ \p',q',t\" == "((p,q,s),p',q',t) : stepa1" - "\p,q,s\ -*\ \p',q',t\" == "((p,q,s),p',q',t) : (stepa1^*)" - "\p,q,s\ -i\ \p',q',t\" == "((p,q,s),p',q',t) : (stepa1^i)" - - -inductive "stepa1" -intros - "\SET x a#p,q,s\ -1\ \p,SET x a#q,s[x\ a s]\" - "b s \ \JMPF b i#p,q,s\ -1\ \p,JMPF b i#q,s\" - "\ \ b s; i \ size p \ +inductive_set + stepa1 :: "(config \ config)set" + and stepa1' :: "[instrs,instrs,state, instrs,instrs,state] \ bool" + ("((1\_,/_,/_\)/ -1\ (1\_,/_,/_\))" 50) +where + "\p,q,s\ -1\ \p',q',t\ == ((p,q,s),p',q',t) : stepa1" +| "\SET x a#p,q,s\ -1\ \p,SET x a#q,s[x\ a s]\" +| "b s \ \JMPF b i#p,q,s\ -1\ \p,JMPF b i#q,s\" +| "\ \ b s; i \ size p \ \ \JMPF b i # p, q, s\ -1\ \drop i p, rev(take i p) @ JMPF b i # q, s\" - "i \ size q +| "i \ size q \ \JMPB i # p, q, s\ -1\ \rev(take i q) @ JMPB i # p, drop i q, s\" -inductive_cases execE: "((i#is,p,s),next) : stepa1" +abbreviation + stepa :: "[instrs,instrs,state, instrs,instrs,state] \ bool" + ("((1\_,/_,/_\)/ -*\ (1\_,/_,/_\))" 50) where + "\p,q,s\ -*\ \p',q',t\ == ((p,q,s),p',q',t) : (stepa1^*)" + +abbreviation + stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \ bool" + ("((1\_,/_,/_\)/ -_\ (1\_,/_,/_\))" 50) where + "\p,q,s\ -i\ \p',q',t\ == ((p,q,s),p',q',t) : (stepa1^i)" + +inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1" lemma exec_simp[simp]: "(\i#p,q,s\ -1\ \p',q',t\) = (case i of diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Natural.thy --- a/src/HOL/IMP/Natural.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Natural.thy Wed Jul 11 11:14:51 2007 +0200 @@ -11,22 +11,12 @@ subsection "Execution of commands" -consts evalc :: "(com \ state \ state) set" -syntax "_evalc" :: "[com,state,state] \ bool" ("<_,_>/ -c-> _" [0,0,60] 60) - -syntax (xsymbols) - "_evalc" :: "[com,state,state] \ bool" ("\_,_\/ \\<^sub>c _" [0,0,60] 60) - -syntax (HTML output) - "_evalc" :: "[com,state,state] \ bool" ("\_,_\/ \\<^sub>c _" [0,0,60] 60) - text {* We write @{text "\c,s\ \\<^sub>c s'"} for \emph{Statement @{text c}, started in state @{text s}, terminates in state @{text s'}}. Formally, @{text "\c,s\ \\<^sub>c s'"} is just another form of saying \emph{the tuple @{text "(c,s,s')"} is part of the relation @{text evalc}}: *} -translations "\c,s\ \\<^sub>c s'" == "(c,s,s') \ evalc" constdefs update :: "('a \ 'b) \ 'a \ 'b \ ('a \ 'b)" ("_/[_ ::= /_]" [900,0,0] 900) @@ -38,18 +28,19 @@ text {* The big-step execution relation @{text evalc} is defined inductively: *} -inductive evalc - intros +inductive + evalc :: "[com,state,state] \ bool" ("\_,_\/ \\<^sub>c _" [0,0,60] 60) +where Skip: "\\,s\ \\<^sub>c s" - Assign: "\x :== a,s\ \\<^sub>c s[x\a s]" +| Assign: "\x :== a,s\ \\<^sub>c s[x\a s]" - Semi: "\c0,s\ \\<^sub>c s'' \ \c1,s''\ \\<^sub>c s' \ \c0; c1, s\ \\<^sub>c s'" +| Semi: "\c0,s\ \\<^sub>c s'' \ \c1,s''\ \\<^sub>c s' \ \c0; c1, s\ \\<^sub>c s'" - IfTrue: "b s \ \c0,s\ \\<^sub>c s' \ \\ b \ c0 \ c1, s\ \\<^sub>c s'" - IfFalse: "\b s \ \c1,s\ \\<^sub>c s' \ \\ b \ c0 \ c1, s\ \\<^sub>c s'" +| IfTrue: "b s \ \c0,s\ \\<^sub>c s' \ \\ b \ c0 \ c1, s\ \\<^sub>c s'" +| IfFalse: "\b s \ \c1,s\ \\<^sub>c s' \ \\ b \ c0 \ c1, s\ \\<^sub>c s'" - WhileFalse: "\b s \ \\ b \ c,s\ \\<^sub>c s" - WhileTrue: "b s \ \c,s\ \\<^sub>c s'' \ \\ b \ c, s''\ \\<^sub>c s' +| WhileFalse: "\b s \ \\ b \ c,s\ \\<^sub>c s" +| WhileTrue: "b s \ \c,s\ \\<^sub>c s'' \ \\ b \ c, s''\ \\<^sub>c s' \ \\ b \ c, s\ \\<^sub>c s'" lemmas evalc.intros [intro] -- "use those rules in automatic proofs" @@ -74,33 +65,33 @@ *} lemma skip: "\\,s\ \\<^sub>c s' = (s' = s)" - by (rule, erule evalc.elims) auto + by (rule, erule evalc.cases) auto lemma assign: "\x :== a,s\ \\<^sub>c s' = (s' = s[x\a s])" - by (rule, erule evalc.elims) auto + by (rule, erule evalc.cases) auto lemma semi: "\c0; c1, s\ \\<^sub>c s' = (\s''. \c0,s\ \\<^sub>c s'' \ \c1,s''\ \\<^sub>c s')" - by (rule, erule evalc.elims) auto + by (rule, erule evalc.cases) auto lemma ifTrue: "b s \ \\ b \ c0 \ c1, s\ \\<^sub>c s' = \c0,s\ \\<^sub>c s'" - by (rule, erule evalc.elims) auto + by (rule, erule evalc.cases) auto lemma ifFalse: "\b s \ \\ b \ c0 \ c1, s\ \\<^sub>c s' = \c1,s\ \\<^sub>c s'" - by (rule, erule evalc.elims) auto + by (rule, erule evalc.cases) auto lemma whileFalse: "\ b s \ \\ b \ c,s\ \\<^sub>c s' = (s' = s)" - by (rule, erule evalc.elims) auto + by (rule, erule evalc.cases) auto lemma whileTrue: "b s \ \\ b \ c, s\ \\<^sub>c s' = (\s''. \c,s\ \\<^sub>c s'' \ \\ b \ c, s''\ \\<^sub>c s')" - by (rule, erule evalc.elims) auto + by (rule, erule evalc.cases) auto text "Again, Isabelle may use these rules in automatic proofs:" lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/Transition.thy --- a/src/HOL/IMP/Transition.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/Transition.thy Wed Jul 11 11:14:51 2007 +0200 @@ -20,10 +20,8 @@ a statement, the transition relation is not @{typ "((com \ state) \ (com \ state)) set"} but instead: -*} -consts evalc1 :: "((com option \ state) \ (com option \ state)) set" + @{typ "((com option \ state) \ (com option \ state)) set"} -text {* Some syntactic sugar that we will use to hide the @{text option} part in configurations: *} @@ -44,53 +42,40 @@ "\s\" == "(None, s)" text {* + Now, finally, we are set to write down the rules for our small step semantics: +*} +inductive_set + evalc1 :: "((com option \ state) \ (com option \ state)) set" + and evalc1' :: "[(com option\state),(com option\state)] \ bool" + ("_ \\<^sub>1 _" [60,60] 61) +where + "cs \\<^sub>1 cs' == (cs,cs') \ evalc1" +| Skip: "\\, s\ \\<^sub>1 \s\" +| Assign: "\x :== a, s\ \\<^sub>1 \s[x \ a s]\" + +| Semi1: "\c0,s\ \\<^sub>1 \s'\ \ \c0;c1,s\ \\<^sub>1 \c1,s'\" +| Semi2: "\c0,s\ \\<^sub>1 \c0',s'\ \ \c0;c1,s\ \\<^sub>1 \c0';c1,s'\" + +| IfTrue: "b s \ \\ b \ c1 \ c2,s\ \\<^sub>1 \c1,s\" +| IfFalse: "\b s \ \\ b \ c1 \ c2,s\ \\<^sub>1 \c2,s\" + +| While: "\\ b \ c,s\ \\<^sub>1 \\ b \ c; \ b \ c \ \,s\" + +lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs" + +text {* More syntactic sugar for the transition relation, and its iteration. *} -syntax - "_evalc1" :: "[(com option\state),(com option\state)] \ bool" - ("_ -1-> _" [60,60] 60) - "_evalcn" :: "[(com option\state),nat,(com option\state)] \ bool" - ("_ -_-> _" [60,60,60] 60) - "_evalc*" :: "[(com option\state),(com option\state)] \ bool" - ("_ -*-> _" [60,60] 60) - -syntax (xsymbols) - "_evalc1" :: "[(com option\state),(com option\state)] \ bool" - ("_ \\<^sub>1 _" [60,60] 61) - "_evalcn" :: "[(com option\state),nat,(com option\state)] \ bool" - ("_ -_\\<^sub>1 _" [60,60,60] 60) - "_evalc*" :: "[(com option\state),(com option\state)] \ bool" - ("_ \\<^sub>1\<^sup>* _" [60,60] 60) - -translations - "cs \\<^sub>1 cs'" == "(cs,cs') \ evalc1" - "cs -n\\<^sub>1 cs'" == "(cs,cs') \ evalc1^n" - "cs \\<^sub>1\<^sup>* cs'" == "(cs,cs') \ evalc1^*" +abbreviation + evalcn :: "[(com option\state),nat,(com option\state)] \ bool" + ("_ -_\\<^sub>1 _" [60,60,60] 60) where + "cs -n\\<^sub>1 cs' == (cs,cs') \ evalc1^n" - -- {* Isabelle/HOL converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"}, - so we also include: *} - "cs0 \\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \ evalc1" - "cs0 -n\\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \ evalc1^n" - "cs0 \\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \ evalc1^*" - -text {* - Now, finally, we are set to write down the rules for our small step semantics: -*} -inductive evalc1 - intros - Skip: "\\, s\ \\<^sub>1 \s\" - Assign: "\x :== a, s\ \\<^sub>1 \s[x \ a s]\" - - Semi1: "\c0,s\ \\<^sub>1 \s'\ \ \c0;c1,s\ \\<^sub>1 \c1,s'\" - Semi2: "\c0,s\ \\<^sub>1 \c0',s'\ \ \c0;c1,s\ \\<^sub>1 \c0';c1,s'\" - - IfTrue: "b s \ \\ b \ c1 \ c2,s\ \\<^sub>1 \c1,s\" - IfFalse: "\b s \ \\ b \ c1 \ c2,s\ \\<^sub>1 \c2,s\" - - While: "\\ b \ c,s\ \\<^sub>1 \\ b \ c; \ b \ c \ \,s\" - -lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs" +abbreviation + evalc' :: "[(com option\state),(com option\state)] \ bool" + ("_ \\<^sub>1\<^sup>* _" [60,60] 60) where + "cs \\<^sub>1\<^sup>* cs' == (cs,cs') \ evalc1^*" (*<*) (* fixme: move to Relation_Power.thy *) @@ -120,18 +105,18 @@ syntax directed way: *} lemma SKIP_1: "\\, s\ \\<^sub>1 y = (y = \s\)" - by (rule, cases set: evalc1, auto) + by (induct y, rule, cases set: evalc1, auto) lemma Assign_1: "\x :== a, s\ \\<^sub>1 y = (y = \s[x \ a s]\)" - by (rule, cases set: evalc1, auto) + by (induct y, rule, cases set: evalc1, auto) lemma Cond_1: "\\ b \ c1 \ c2, s\ \\<^sub>1 y = ((b s \ y = \c1, s\) \ (\b s \ y = \c2, s\))" - by (rule, cases set: evalc1, auto) + by (induct y, rule, cases set: evalc1, auto) lemma While_1: "\\ b \ c, s\ \\<^sub>1 y = (y = \\ b \ c; \ b \ c \ \, s\)" - by (rule, cases set: evalc1, auto) + by (induct y, rule, cases set: evalc1, auto) lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1 @@ -197,10 +182,10 @@ has terminated and there is no next configuration: *} lemma stuck [elim!]: "\s\ \\<^sub>1 y \ P" - by (auto elim: evalc1.elims) + by (induct y, auto elim: evalc1.cases) lemma evalc_None_retrancl [simp, dest!]: "\s\ \\<^sub>1\<^sup>* s' \ s' = \s\" - by (induct set: rtrancl_set) auto + by (induct set: rtrancl) auto (*<*) (* FIXME: relpow.simps don't work *) @@ -230,10 +215,10 @@ case (Suc n) from `\c1; c2, s\ -Suc n\\<^sub>1 \s''\` - obtain y where - 1: "\c1; c2, s\ \\<^sub>1 y" and - n: "y -n\\<^sub>1 \s''\" - by blast + obtain co s''' where + 1: "\c1; c2, s\ \\<^sub>1 (co, s''')" and + n: "(co, s''') -n\\<^sub>1 \s''\" + by auto from 1 show "\i j s'. \c1, s\ -i\\<^sub>1 \s'\ \ \c2, s'\ -j\\<^sub>1 \s''\ \ Suc n = i+j" @@ -241,14 +226,14 @@ proof (cases set: evalc1) case Semi1 then obtain s' where - "y = \c2, s'\" and "\c1, s\ \\<^sub>1 \s'\" + "co = Some c2" and "s''' = s'" and "\c1, s\ \\<^sub>1 \s'\" by auto with 1 n have "?Q 1 n s'" by simp thus ?thesis by blast next case Semi2 then obtain c1' s' where - y: "y = \c1'; c2, s'\" and + "co = Some (c1'; c2)" "s''' = s'" and c1: "\c1, s\ \\<^sub>1 \c1', s'\" by auto with n have "\c1'; c2, s'\ -n\\<^sub>1 \s''\" by simp @@ -476,13 +461,13 @@ qed inductive_cases evalc1_SEs: - "\\,s\ \\<^sub>1 t" - "\x:==a,s\ \\<^sub>1 t" - "\c1;c2, s\ \\<^sub>1 t" - "\\ b \ c1 \ c2, s\ \\<^sub>1 t" - "\\ b \ c, s\ \\<^sub>1 t" + "\\,s\ \\<^sub>1 (co, s')" + "\x:==a,s\ \\<^sub>1 (co, s')" + "\c1;c2, s\ \\<^sub>1 (co, s')" + "\\ b \ c1 \ c2, s\ \\<^sub>1 (co, s')" + "\\ b \ c, s\ \\<^sub>1 (co, s')" -inductive_cases evalc1_E: "\\ b \ c, s\ \\<^sub>1 t" +inductive_cases evalc1_E: "\\ b \ c, s\ \\<^sub>1 (co, s')" declare evalc1_SEs [elim!] @@ -546,6 +531,7 @@ apply (intro strip) apply (erule rel_pow_E2) apply simp +apply (simp only: split_paired_all) apply (erule evalc1_E) apply simp diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMP/VC.thy --- a/src/HOL/IMP/VC.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMP/VC.thy Wed Jul 11 11:14:51 2007 +0200 @@ -120,11 +120,11 @@ show ?case (is "? ac. ?C ac") proof show "?C Askip" by simp qed next - case (ass P a x) + case (ass P x a) show ?case (is "? ac. ?C ac") proof show "?C(Aass x a)" by simp qed next - case (semi P Q R c1 c2) + case (semi P c1 Q c2 R) from semi.hyps obtain ac1 where ih1: "?Eq P c1 Q ac1" by fast from semi.hyps obtain ac2 where ih2: "?Eq Q c2 R ac2" by fast show ?case (is "? ac. ?C ac") @@ -133,7 +133,7 @@ using ih1 ih2 by simp (fast elim!: awp_mono vc_mono) qed next - case (If P Q b c1 c2) + case (If P b c1 Q c2) from If.hyps obtain ac1 where ih1: "?Eq (%s. P s & b s) c1 Q ac1" by fast from If.hyps obtain ac2 where ih2: "?Eq (%s. P s & ~b s) c2 Q ac2" by fast show ?case (is "? ac. ?C ac") diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMPP/Com.thy --- a/src/HOL/IMPP/Com.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMPP/Com.thy Wed Jul 11 11:14:51 2007 +0200 @@ -48,32 +48,29 @@ (* Well-typedness: all procedures called must exist *) -consts WTs :: "com set" -syntax WT :: "com => bool" -translations "WT c" == "c : WTs" -inductive WTs intros +inductive WT :: "com => bool" where Skip: "WT SKIP" - Assign: "WT (X :== a)" + | Assign: "WT (X :== a)" - Local: "WT c ==> + | Local: "WT c ==> WT (LOCAL Y := a IN c)" - Semi: "[| WT c0; WT c1 |] ==> + | Semi: "[| WT c0; WT c1 |] ==> WT (c0;; c1)" - If: "[| WT c0; WT c1 |] ==> + | If: "[| WT c0; WT c1 |] ==> WT (IF b THEN c0 ELSE c1)" - While: "WT c ==> + | While: "WT c ==> WT (WHILE b DO c)" - Body: "body pn ~= None ==> + | Body: "body pn ~= None ==> WT (BODY pn)" - Call: "WT (BODY pn) ==> + | Call: "WT (BODY pn) ==> WT (X:=CALL pn(a))" inductive_cases WTs_elim_cases: diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMPP/Hoare.thy Wed Jul 11 11:14:51 2007 +0200 @@ -34,59 +34,58 @@ consts triple_valid :: "nat => 'a triple => bool" ( "|=_:_" [0 , 58] 57) hoare_valids :: "'a triple set => 'a triple set => bool" ("_||=_" [58, 58] 57) - hoare_derivs :: "('a triple set * 'a triple set) set" syntax triples_valid:: "nat => 'a triple set => bool" ("||=_:_" [0 , 58] 57) hoare_valid :: "'a triple set => 'a triple => bool" ("_|=_" [58, 58] 57) -"@hoare_derivs":: "'a triple set => 'a triple set => bool" ("_||-_" [58, 58] 57) -"@hoare_deriv" :: "'a triple set => 'a triple => bool" ("_|-_" [58, 58] 57) defs triple_valid_def: "|=n:t == case t of {P}.c.{Q} => !Z s. P Z s --> (!s'. -n-> s' --> Q Z s')" translations "||=n:G" == "Ball G (triple_valid n)" defs hoare_valids_def: "G||=ts == !n. ||=n:G --> ||=n:ts" translations "G |=t " == " G||={t}" - "G||-ts" == "(G,ts) : hoare_derivs" - "G |-t" == " G||-{t}" (* Most General Triples *) constdefs MGT :: "com => state triple" ("{=}._.{->}" [60] 58) "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. -c-> s1}" -inductive hoare_derivs intros +inductive + hoare_derivs :: "'a triple set => 'a triple set => bool" ("_||-_" [58, 58] 57) + and hoare_deriv :: "'a triple set => 'a triple => bool" ("_|-_" [58, 58] 57) +where + "G |-t == G||-{t}" - empty: "G||-{}" - insert: "[| G |-t; G||-ts |] +| empty: "G||-{}" +| insert: "[| G |-t; G||-ts |] ==> G||-insert t ts" - asm: "ts <= G ==> +| asm: "ts <= G ==> G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *) - cut: "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *) +| cut: "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *) - weaken: "[| G||-ts' ; ts <= ts' |] ==> G||-ts" +| weaken: "[| G||-ts' ; ts <= ts' |] ==> G||-ts" - conseq: "!Z s. P Z s --> (? P' Q'. G|-{P'}.c.{Q'} & +| conseq: "!Z s. P Z s --> (? P' Q'. G|-{P'}.c.{Q'} & (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s')) ==> G|-{P}.c.{Q}" - Skip: "G|-{P}. SKIP .{P}" +| Skip: "G|-{P}. SKIP .{P}" - Ass: "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}" +| Ass: "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}" - Local: "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'])} +| Local: "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'])} ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}" - Comp: "[| G|-{P}.c.{Q}; +| Comp: "[| G|-{P}.c.{Q}; G|-{Q}.d.{R} |] ==> G|-{P}. (c;;d) .{R}" - If: "[| G|-{P &> b }.c.{Q}; +| If: "[| G|-{P &> b }.c.{Q}; G|-{P &> (Not o b)}.d.{Q} |] ==> G|-{P}. IF b THEN c ELSE d .{Q}" - Loop: "G|-{P &> b}.c.{P} ==> +| Loop: "G|-{P &> b}.c.{P} ==> G|-{P}. WHILE b DO c .{P &> (Not o b)}" (* @@ -94,11 +93,11 @@ |-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}" *) - Body: "[| G Un (%p. {P p}. BODY p .{Q p})`Procs +| Body: "[| G Un (%p. {P p}. BODY p .{Q p})`Procs ||-(%p. {P p}. the (body p) .{Q p})`Procs |] ==> G||-(%p. {P p}. BODY p .{Q p})`Procs" - Call: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s])} +| Call: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s])} ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}. X:=CALL pn(a) .{Q}" @@ -283,7 +282,7 @@ apply (blast) (* asm *) apply (blast) (* cut *) apply (blast) (* weaken *) -apply (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *}) +apply (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "hoare_derivs ?x ?y", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *}) apply (simp_all (no_asm_use) add: triple_valid_def2) apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *) apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *) diff -r 28df61d931e2 -r a455e69c31cc src/HOL/IMPP/Natural.thy --- a/src/HOL/IMPP/Natural.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/IMPP/Natural.thy Wed Jul 11 11:14:51 2007 +0200 @@ -11,17 +11,6 @@ begin (** Execution of commands **) -consts - evalc :: "(com * state * state) set" - evaln :: "(com * state * nat * state) set" - -syntax - "@evalc":: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51) - "@evaln":: "[com,state,nat,state] => bool" ("<_,_>/ -_-> _" [0,0,0,51] 51) - -translations - " -c-> s'" == "(c,s, s') : evalc" - " -n-> s'" == "(c,s,n,s') : evaln" consts newlocs :: locals @@ -33,63 +22,65 @@ translations "s" == "getlocs s X" -inductive evalc - intros +inductive + evalc :: "[com,state, state] => bool" ("<_,_>/ -c-> _" [0,0, 51] 51) + where Skip: " -c-> s" - Assign: " -c-> s[X::=a s]" + | Assign: " -c-> s[X::=a s]" - Local: " -c-> s1 ==> + | Local: " -c-> s1 ==> -c-> s1[Loc Y::=s0]" - Semi: "[| -c-> s1; -c-> s2 |] ==> + | Semi: "[| -c-> s1; -c-> s2 |] ==> -c-> s2" - IfTrue: "[| b s; -c-> s1 |] ==> + | IfTrue: "[| b s; -c-> s1 |] ==> -c-> s1" - IfFalse: "[| ~b s; -c-> s1 |] ==> + | IfFalse: "[| ~b s; -c-> s1 |] ==> -c-> s1" - WhileFalse: "~b s ==> -c-> s" + | WhileFalse: "~b s ==> -c-> s" - WhileTrue: "[| b s0; -c-> s1; -c-> s2 |] ==> + | WhileTrue: "[| b s0; -c-> s1; -c-> s2 |] ==> -c-> s2" - Body: " -c-> s1 ==> + | Body: " -c-> s1 ==> -c-> s1" - Call: " -c-> s1 ==> + | Call: " -c-> s1 ==> -c-> (setlocs s1 (getlocs s0)) [X::=s1]" -inductive evaln - intros +inductive + evaln :: "[com,state,nat,state] => bool" ("<_,_>/ -_-> _" [0,0,0,51] 51) + where Skip: " -n-> s" - Assign: " -n-> s[X::=a s]" + | Assign: " -n-> s[X::=a s]" - Local: " -n-> s1 ==> + | Local: " -n-> s1 ==> -n-> s1[Loc Y::=s0]" - Semi: "[| -n-> s1; -n-> s2 |] ==> + | Semi: "[| -n-> s1; -n-> s2 |] ==> -n-> s2" - IfTrue: "[| b s; -n-> s1 |] ==> + | IfTrue: "[| b s; -n-> s1 |] ==> -n-> s1" - IfFalse: "[| ~b s; -n-> s1 |] ==> + | IfFalse: "[| ~b s; -n-> s1 |] ==> -n-> s1" - WhileFalse: "~b s ==> -n-> s" + | WhileFalse: "~b s ==> -n-> s" - WhileTrue: "[| b s0; -n-> s1; -n-> s2 |] ==> + | WhileTrue: "[| b s0; -n-> s1; -n-> s2 |] ==> -n-> s2" - Body: " - n-> s1 ==> + | Body: " - n-> s1 ==> -Suc n-> s1" - Call: " -n-> s1 ==> + | Call: " -n-> s1 ==> -n-> (setlocs s1 (getlocs s0)) [X::=s1]" diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/Com.thy --- a/src/HOL/Induct/Com.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/Com.thy Wed Jul 11 11:14:51 2007 +0200 @@ -15,8 +15,6 @@ types state = "loc => nat" n2n2n = "nat => nat => nat" -arities loc :: type - datatype exp = N nat | X loc @@ -33,36 +31,38 @@ subsection {* Commands *} text{* Execution of commands *} -consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" - -abbreviation - exec_rel ("_/ -[_]-> _" [50,0,50] 50) - "csig -[eval]-> s == (csig,s) \ exec eval" abbreviation (input) - generic_rel ("_/ -|[_]-> _" [50,0,50] 50) + generic_rel ("_/ -|[_]-> _" [50,0,50] 50) where "esig -|[eval]-> ns == (esig,ns) \ eval" text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*} -inductive "exec eval" - intros - Skip: "(SKIP,s) -[eval]-> s" - Assign: "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)" +inductive_set + exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" + and exec_rel :: "com * state => ((exp*state) * (nat*state)) set => state => bool" + ("_/ -[_]-> _" [50,0,50] 50) + for eval :: "((exp*state) * (nat*state)) set" + where + "csig -[eval]-> s == (csig,s) \ exec eval" - Semi: "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] + | Skip: "(SKIP,s) -[eval]-> s" + + | Assign: "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)" + + | Semi: "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] ==> (c0 ;; c1, s) -[eval]-> s1" - IfTrue: "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] + | IfTrue: "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" - IfFalse: "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |] + | IfFalse: "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |] ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" - WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) + | WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1" - WhileTrue: "[| (e,s) -|[eval]-> (0,s1); + | WhileTrue: "[| (e,s) -|[eval]-> (0,s1); (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |] ==> (WHILE e DO c, s) -[eval]-> s3" @@ -79,11 +79,20 @@ text{*Justifies using "exec" in the inductive definition of "eval"*} lemma exec_mono: "A<=B ==> exec(A) <= exec(B)" -apply (unfold exec.defs ) -apply (rule lfp_mono) -apply (assumption | rule basic_monos)+ +apply (rule subsetI) +apply (simp add: split_paired_all) +apply (erule exec.induct) +apply blast+ done +lemma [pred_set_conv]: + "((\x x' y y'. ((x, x'), (y, y')) \ R) <= (\x x' y y'. ((x, x'), (y, y')) \ S)) = (R <= S)" + by (auto simp add: le_fun_def le_bool_def) + +lemma [pred_set_conv]: + "((\x x' y. ((x, x'), y) \ R) <= (\x x' y. ((x, x'), y) \ S)) = (R <= S)" + by (auto simp add: le_fun_def le_bool_def) + ML {* Unify.trace_bound := 30; Unify.search_bound := 60; @@ -102,23 +111,21 @@ subsection {* Expressions *} text{* Evaluation of arithmetic expressions *} -consts - eval :: "((exp*state) * (nat*state)) set" - -abbreviation - eval_rel :: "[exp*state,nat*state] => bool" (infixl "-|->" 50) - "esig -|-> ns == (esig, ns) \ eval" -inductive eval - intros - N [intro!]: "(N(n),s) -|-> (n,s)" +inductive_set + eval :: "((exp*state) * (nat*state)) set" + and eval_rel :: "[exp*state,nat*state] => bool" (infixl "-|->" 50) + where + "esig -|-> ns == (esig, ns) \ eval" - X [intro!]: "(X(x),s) -|-> (s(x),s)" + | N [intro!]: "(N(n),s) -|-> (n,s)" - Op [intro]: "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |] + | X [intro!]: "(X(x),s) -|-> (s(x),s)" + + | Op [intro]: "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |] ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)" - valOf [intro]: "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |] + | valOf [intro]: "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |] ==> (VALOF c RESULTIS e, s) -|-> (n, s1)" monos exec_mono @@ -135,7 +142,7 @@ by (rule fun_upd_same [THEN subst], fast) -text{* Make the induction rule look nicer -- though eta_contract makes the new +text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new version look worse than it is...*} lemma split_lemma: @@ -167,11 +174,11 @@ done -text{*Lemma for Function_eval. The major premise is that (c,s) executes to s1 +text{*Lemma for @{text Function_eval}. The major premise is that @{text "(c,s)"} executes to @{text "s1"} using eval restricted to its functional part. Note that the execution - (c,s) -[eval]-> s2 can use unrestricted eval! The reason is that - the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is - functional on the argument (c,s). + @{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}! The reason is that + the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is + functional on the argument @{text "(c,s)"}. *} lemma com_Unique: "(c,s) -[eval Int {((e,s),(n,t)). \nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/Comb.thy --- a/src/HOL/Induct/Comb.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/Comb.thy Wed Jul 11 11:14:51 2007 +0200 @@ -34,47 +34,39 @@ (multi-step) reductions, @{text "--->"}. *} -consts - contract :: "(comb*comb) set" - -abbreviation - contract_rel1 :: "[comb,comb] => bool" (infixl "-1->" 50) where - "x -1-> y == (x,y) \ contract" +inductive_set + contract :: "(comb*comb) set" + and contract_rel1 :: "[comb,comb] => bool" (infixl "-1->" 50) + where + "x -1-> y == (x,y) \ contract" + | K: "K##x##y -1-> x" + | S: "S##x##y##z -1-> (x##z)##(y##z)" + | Ap1: "x-1->y ==> x##z -1-> y##z" + | Ap2: "x-1->y ==> z##x -1-> z##y" abbreviation contract_rel :: "[comb,comb] => bool" (infixl "--->" 50) where "x ---> y == (x,y) \ contract^*" -inductive contract - intros - K: "K##x##y -1-> x" - S: "S##x##y##z -1-> (x##z)##(y##z)" - Ap1: "x-1->y ==> x##z -1-> y##z" - Ap2: "x-1->y ==> z##x -1-> z##y" - text {* Inductive definition of parallel contractions, @{text "=1=>"} and (multi-step) parallel reductions, @{text "===>"}. *} -consts +inductive_set parcontract :: "(comb*comb) set" - -abbreviation - parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50) where - "x =1=> y == (x,y) \ parcontract" + and parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50) + where + "x =1=> y == (x,y) \ parcontract" + | refl: "x =1=> x" + | K: "K##x##y =1=> x" + | S: "S##x##y##z =1=> (x##z)##(y##z)" + | Ap: "[| x=1=>y; z=1=>w |] ==> x##z =1=> y##w" abbreviation parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50) where "x ===> y == (x,y) \ parcontract^*" -inductive parcontract - intros - refl: "x =1=> x" - K: "K##x##y =1=> x" - S: "S##x##y##z =1=> (x##z)##(y##z)" - Ap: "[| x=1=>y; z=1=>w |] ==> x##z =1=> y##w" - text {* Misc definitions. *} diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/LFilter.thy --- a/src/HOL/Induct/LFilter.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/LFilter.thy Wed Jul 11 11:14:51 2007 +0200 @@ -9,13 +9,12 @@ theory LFilter imports LList begin -consts +inductive_set findRel :: "('a => bool) => ('a llist * 'a llist)set" - -inductive "findRel p" - intros + for p :: "'a => bool" + where found: "p x ==> (LCons x l, LCons x l) \ findRel p" - seek: "[| ~p x; (l,l') \ findRel p |] ==> (LCons x l, l') \ findRel p" + | seek: "[| ~p x; (l,l') \ findRel p |] ==> (LCons x l, l') \ findRel p" declare findRel.intros [intro] diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/LList.thy --- a/src/HOL/Induct/LList.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/LList.thy Wed Jul 11 11:14:51 2007 +0200 @@ -24,21 +24,19 @@ theory LList imports SList begin -consts - +coinductive_set llist :: "'a item set => 'a item set" - LListD :: "('a item * 'a item)set => ('a item * 'a item)set" - + for A :: "'a item set" + where + NIL_I: "NIL \ llist(A)" + | CONS_I: "[| a \ A; M \ llist(A) |] ==> CONS a M \ llist(A)" -coinductive "llist(A)" - intros - NIL_I: "NIL \ llist(A)" - CONS_I: "[| a \ A; M \ llist(A) |] ==> CONS a M \ llist(A)" - -coinductive "LListD(r)" - intros +coinductive_set + LListD :: "('a item * 'a item)set => ('a item * 'a item)set" + for r :: "('a item * 'a item)set" + where NIL_I: "(NIL, NIL) \ LListD(r)" - CONS_I: "[| (a,b) \ r; (M,N) \ LListD(r) |] + | CONS_I: "[| (a,b) \ r; (M,N) \ LListD(r) |] ==> (CONS a M, CONS b N) \ LListD(r)" @@ -159,11 +157,19 @@ declare option.split [split] text{*This justifies using llist in other recursive type definitions*} -lemma llist_mono: "A\B ==> llist(A) \ llist(B)" -apply (simp add: llist.defs) -apply (rule gfp_mono) -apply (assumption | rule basic_monos)+ -done +lemma llist_mono: + assumes subset: "A \ B" + shows "llist A \ llist B" +proof + fix x + assume "x \ llist A" + then show "x \ llist B" + proof coinduct + case llist + then show ?case using subset + by cases blast+ + qed +qed lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))" @@ -195,9 +201,9 @@ text{*Utilise the ``strong'' part, i.e. @{text "gfp(f)"}*} lemma list_Fun_llist_I: "M \ llist(A) ==> M \ list_Fun A (X Un llist(A))" -apply (unfold llist.defs list_Fun_def) -apply (rule gfp_fun_UnI2) -apply (rule monoI, auto) +apply (unfold list_Fun_def) +apply (erule llist.cases) +apply auto done subsection{* @{text LList_corec} satisfies the desired recurion equation *} @@ -278,10 +284,10 @@ text{*The domain of the @{text LListD} relation*} lemma Domain_LListD: "Domain (LListD(diag A)) \ llist(A)" -apply (simp add: llist.defs NIL_def CONS_def) -apply (rule gfp_upperbound) -txt{*avoids unfolding @{text LListD} on the rhs*} -apply (rule_tac P = "%x. Domain x \ ?B" in LListD_unfold [THEN ssubst], auto) +apply (rule subsetI) +apply (erule llist.coinduct) +apply (simp add: NIL_def CONS_def) +apply (drule_tac P = "%x. xa \ Domain x" in LListD_unfold [THEN subst], auto) done text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*} @@ -305,6 +311,7 @@ lemma LListD_coinduct: "[| M \ X; X \ LListD_Fun r (X Un LListD(r)) |] ==> M \ LListD(r)" +apply (cases M) apply (simp add: LListD_Fun_def) apply (erule LListD.coinduct) apply (auto ); @@ -320,9 +327,10 @@ text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*} lemma LListD_Fun_LListD_I: "M \ LListD(r) ==> M \ LListD_Fun r (X Un LListD(r))" -apply (unfold LListD.defs LListD_Fun_def) -apply (rule gfp_fun_UnI2) -apply (rule monoI, auto) +apply (cases M) +apply (simp add: LListD_Fun_def) +apply (erule LListD.cases) +apply auto done @@ -523,7 +531,7 @@ apply (rule LList_equalityI) apply (erule imageI) apply (rule image_subsetI) -apply (erule_tac aa=x in llist.cases) +apply (erule_tac a=x in llist.cases) apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast) done @@ -608,8 +616,8 @@ apply (rule_tac X = "\u\llist (A) . \v \ llist (A) . {Lappend u v}" in llist_coinduct) apply fast apply safe -apply (erule_tac aa = u in llist.cases) -apply (erule_tac aa = v in llist.cases, simp_all, blast) +apply (erule_tac a = u in llist.cases) +apply (erule_tac a = v in llist.cases, simp_all, blast) done text{*strong co-induction: bisimulation and case analysis on one variable*} @@ -617,7 +625,7 @@ apply (rule_tac X = "(%u. Lappend u N) `llist (A)" in llist_coinduct) apply (erule imageI) apply (rule image_subsetI) -apply (erule_tac aa = x in llist.cases) +apply (erule_tac a = x in llist.cases) apply (simp add: list_Fun_llist_I, simp) done diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/Mutil.thy --- a/src/HOL/Induct/Mutil.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/Mutil.thy Wed Jul 11 11:14:51 2007 +0200 @@ -15,18 +15,19 @@ the Mutilated Checkerboard Problem by J McCarthy. *} -consts tiling :: "'a set set => 'a set set" -inductive "tiling A" - intros +inductive_set + tiling :: "'a set set => 'a set set" + for A :: "'a set set" + where empty [simp, intro]: "{} \ tiling A" - Un [simp, intro]: "[| a \ A; t \ tiling A; a \ t = {} |] + | Un [simp, intro]: "[| a \ A; t \ tiling A; a \ t = {} |] ==> a \ t \ tiling A" -consts domino :: "(nat \ nat) set set" -inductive domino - intros +inductive_set + domino :: "(nat \ nat) set set" + where horiz [simp]: "{(i, j), (i, Suc j)} \ domino" - vertl [simp]: "{(i, j), (Suc i, j)} \ domino" + | vertl [simp]: "{(i, j), (Suc i, j)} \ domino" text {* \medskip Sets of squares of the given colour*} diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/PropLog.thy --- a/src/HOL/Induct/PropLog.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/PropLog.thy Wed Jul 11 11:14:51 2007 +0200 @@ -26,20 +26,15 @@ subsection {* The proof system *} -consts - thms :: "'a pl set => 'a pl set" - -abbreviation - thm_rel :: "['a pl set, 'a pl] => bool" (infixl "|-" 50) where - "H |- p == p \ thms H" - -inductive "thms(H)" - intros - H [intro]: "p\H ==> H |- p" - K: "H |- p->q->p" - S: "H |- (p->q->r) -> (p->q) -> p->r" - DN: "H |- ((p->false) -> false) -> p" - MP: "[| H |- p->q; H |- p |] ==> H |- q" +inductive + thms :: "['a pl set, 'a pl] => bool" (infixl "|-" 50) + for H :: "'a pl set" + where + H [intro]: "p\H ==> H |- p" + | K: "H |- p->q->p" + | S: "H |- (p->q->r) -> (p->q) -> p->r" + | DN: "H |- ((p->false) -> false) -> p" + | MP: "[| H |- p->q; H |- p |] ==> H |- q" subsection {* The semantics *} @@ -80,9 +75,9 @@ subsection {* Proof theory of propositional logic *} lemma thms_mono: "G<=H ==> thms(G) <= thms(H)" -apply (unfold thms.defs ) -apply (rule lfp_mono) -apply (assumption | rule basic_monos)+ +apply (rule predicate1I) +apply (erule thms.induct) +apply (auto intro: thms.intros) done lemma thms_I: "H |- p->p" @@ -94,7 +89,7 @@ lemma weaken_left: "[| G \ H; G|-p |] ==> H|-p" -- {* Order of premises is convenient with @{text THEN} *} - by (erule thms_mono [THEN subsetD]) + by (erule thms_mono [THEN predicate1D]) lemmas weaken_left_insert = subset_insertI [THEN weaken_left] diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/QuoDataType.thy Wed Jul 11 11:14:51 2007 +0200 @@ -19,31 +19,25 @@ | DECRYPT nat freemsg text{*The equivalence relation, which makes encryption and decryption inverses -provided the keys are the same.*} -consts msgrel :: "(freemsg * freemsg) set" - -abbreviation - msg_rel :: "[freemsg, freemsg] => bool" (infixl "~~" 50) where - "X ~~ Y == (X,Y) \ msgrel" +provided the keys are the same. -notation (xsymbols) - msg_rel (infixl "\" 50) -notation (HTML output) - msg_rel (infixl "\" 50) - -text{*The first two rules are the desired equations. The next four rules +The first two rules are the desired equations. The next four rules make the equations applicable to subterms. The last two rules are symmetry and transitivity.*} -inductive "msgrel" - intros - CD: "CRYPT K (DECRYPT K X) \ X" - DC: "DECRYPT K (CRYPT K X) \ X" - NONCE: "NONCE N \ NONCE N" - MPAIR: "\X \ X'; Y \ Y'\ \ MPAIR X Y \ MPAIR X' Y'" - CRYPT: "X \ X' \ CRYPT K X \ CRYPT K X'" - DECRYPT: "X \ X' \ DECRYPT K X \ DECRYPT K X'" - SYM: "X \ Y \ Y \ X" - TRANS: "\X \ Y; Y \ Z\ \ X \ Z" + +inductive_set + msgrel :: "(freemsg * freemsg) set" + and msg_rel :: "[freemsg, freemsg] => bool" (infixl "\" 50) + where + "X \ Y == (X,Y) \ msgrel" + | CD: "CRYPT K (DECRYPT K X) \ X" + | DC: "DECRYPT K (CRYPT K X) \ X" + | NONCE: "NONCE N \ NONCE N" + | MPAIR: "\X \ X'; Y \ Y'\ \ MPAIR X Y \ MPAIR X' Y'" + | CRYPT: "X \ X' \ CRYPT K X \ CRYPT K X'" + | DECRYPT: "X \ X' \ DECRYPT K X \ DECRYPT K X'" + | SYM: "X \ Y \ Y \ X" + | TRANS: "\X \ Y; Y \ Z\ \ X \ Z" text{*Proving that it is an equivalence relation*} diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Jul 11 11:14:51 2007 +0200 @@ -18,28 +18,21 @@ | FNCALL nat "freeExp list" text{*The equivalence relation, which makes PLUS associative.*} -consts exprel :: "(freeExp * freeExp) set" - -abbreviation - exp_rel :: "[freeExp, freeExp] => bool" (infixl "~~" 50) where - "X ~~ Y == (X,Y) \ exprel" - -notation (xsymbols) - exp_rel (infixl "\" 50) -notation (HTML output) - exp_rel (infixl "\" 50) text{*The first rule is the desired equation. The next three rules make the equations applicable to subterms. The last two rules are symmetry and transitivity.*} -inductive "exprel" - intros - ASSOC: "PLUS X (PLUS Y Z) \ PLUS (PLUS X Y) Z" - VAR: "VAR N \ VAR N" - PLUS: "\X \ X'; Y \ Y'\ \ PLUS X Y \ PLUS X' Y'" - FNCALL: "(Xs,Xs') \ listrel exprel \ FNCALL F Xs \ FNCALL F Xs'" - SYM: "X \ Y \ Y \ X" - TRANS: "\X \ Y; Y \ Z\ \ X \ Z" +inductive_set + exprel :: "(freeExp * freeExp) set" + and exp_rel :: "[freeExp, freeExp] => bool" (infixl "\" 50) + where + "X \ Y == (X,Y) \ exprel" + | ASSOC: "PLUS X (PLUS Y Z) \ PLUS (PLUS X Y) Z" + | VAR: "VAR N \ VAR N" + | PLUS: "\X \ X'; Y \ Y'\ \ PLUS X Y \ PLUS X' Y'" + | FNCALL: "(Xs,Xs') \ listrel exprel \ FNCALL F Xs \ FNCALL F Xs'" + | SYM: "X \ Y \ Y \ X" + | TRANS: "\X \ Y; Y \ Z\ \ X \ Z" monos listrel_mono @@ -47,7 +40,7 @@ lemma exprel_refl: "X \ X" and list_exprel_refl: "(Xs,Xs) \ listrel(exprel)" - by (induct X and Xs) (blast intro: exprel.intros listrel_intros)+ + by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+ theorem equiv_exprel: "equiv UNIV exprel" proof - @@ -63,13 +56,13 @@ lemma FNCALL_Nil: "FNCALL F [] \ FNCALL F []" apply (rule exprel.intros) -apply (rule listrel_intros) +apply (rule listrel.intros) done lemma FNCALL_Cons: "\X \ X'; (Xs,Xs') \ listrel(exprel)\ \ FNCALL F (X#Xs) \ FNCALL F (X'#Xs')" -by (blast intro: exprel.intros listrel_intros) +by (blast intro: exprel.intros listrel.intros) @@ -98,7 +91,7 @@ (the abstract constructor) is injective*} theorem exprel_imp_eq_freevars: "U \ V \ freevars U = freevars V" apply (induct set: exprel) -apply (erule_tac [4] listrel_induct) +apply (erule_tac [4] listrel.induct) apply (simp_all add: Un_assoc) done @@ -129,7 +122,7 @@ theorem exprel_imp_eq_freefun: "U \ V \ freefun U = freefun V" - by (induct set: exprel) (simp_all add: listrel_intros) + by (induct set: exprel) (simp_all add: listrel.intros) text{*This function, which returns the list of function arguments, is used to @@ -143,8 +136,8 @@ theorem exprel_imp_eqv_freeargs: "U \ V \ (freeargs U, freeargs V) \ listrel exprel" apply (induct set: exprel) -apply (erule_tac [4] listrel_induct) -apply (simp_all add: listrel_intros) +apply (erule_tac [4] listrel.induct) +apply (simp_all add: listrel.intros) apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]]) apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]]) done @@ -258,7 +251,7 @@ "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})" proof - have "(\U. exprel `` {FNCALL F [U]}) respects exprel" - by (simp add: congruent_def FNCALL_Cons listrel_intros) + by (simp add: congruent_def FNCALL_Cons listrel.intros) thus ?thesis by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel]) qed diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/ROOT.ML --- a/src/HOL/Induct/ROOT.ML Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/ROOT.ML Wed Jul 11 11:14:51 2007 +0200 @@ -13,3 +13,4 @@ time_use_thy "PropLog"; time_use_thy "SList"; time_use_thy "LFilter"; +time_use_thy "Com"; diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/SList.thy --- a/src/HOL/Induct/SList.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/SList.thy Wed Jul 11 11:14:51 2007 +0200 @@ -46,12 +46,12 @@ CONS :: "['a item, 'a item] => 'a item" where "CONS M N = In1(Scons M N)" -consts - list :: "'a item set => 'a item set" -inductive "list(A)" - intros +inductive_set + list :: "'a item set => 'a item set" + for A :: "'a item set" + where NIL_I: "NIL: list A" - CONS_I: "[| a: A; M: list A |] ==> CONS a M : list A" + | CONS_I: "[| a: A; M: list A |] ==> CONS a M : list A" typedef (List) @@ -149,6 +149,8 @@ ttl :: "'a list => 'a list" where "ttl xs = list_rec xs [] (%x xs r. xs)" +(*<*)no_syntax + member :: "'a \ 'a list \ bool" (infixl "mem" 55)(*>*) definition member :: "['a, 'a list] => bool" (infixl "mem" 55) where "x mem xs = list_rec xs False (%y ys r. if y=x then True else r)" @@ -254,16 +256,17 @@ (*This justifies using list in other recursive type definitions*) lemma list_mono: "A<=B ==> list(A) <= list(B)" -apply (unfold list.defs ) -apply (rule lfp_mono) -apply (assumption | rule basic_monos)+ +apply (rule subsetI) +apply (erule list.induct) +apply (auto intro!: list.intros) done (*Type checking -- list creates well-founded sets*) lemma list_sexp: "list(sexp) <= sexp" -apply (unfold NIL_def CONS_def list.defs) -apply (rule lfp_lowerbound) -apply (fast intro: sexp.intros sexp_In0I sexp_In1I) +apply (rule subsetI) +apply (erule list.induct) +apply (unfold NIL_def CONS_def) +apply (auto intro: sexp.intros sexp_In0I sexp_In1I) done (* A <= sexp ==> list(A) <= sexp *) diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/Sexp.thy --- a/src/HOL/Induct/Sexp.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/Sexp.thy Wed Jul 11 11:14:51 2007 +0200 @@ -14,14 +14,12 @@ abbreviation "Leaf == Datatype.Leaf" abbreviation "Numb == Datatype.Numb" -consts +inductive_set sexp :: "'a item set" - -inductive sexp - intros + where LeafI: "Leaf(a) \ sexp" - NumbI: "Numb(i) \ sexp" - SconsI: "[| M \ sexp; N \ sexp |] ==> Scons M N \ sexp" + | NumbI: "Numb(i) \ sexp" + | SconsI: "[| M \ sexp; N \ sexp |] ==> Scons M N \ sexp" definition sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Induct/Sigma_Algebra.thy --- a/src/HOL/Induct/Sigma_Algebra.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Induct/Sigma_Algebra.thy Wed Jul 11 11:14:51 2007 +0200 @@ -13,15 +13,14 @@ \}-algebra over a given set of sets. *} -consts +inductive_set \_algebra :: "'a set set => 'a set set" - -inductive "\_algebra A" - intros + for A :: "'a set set" + where basic: "a \ A ==> a \ \_algebra A" - UNIV: "UNIV \ \_algebra A" - complement: "a \ \_algebra A ==> -a \ \_algebra A" - Union: "(!!i::nat. a i \ \_algebra A) ==> (\i. a i) \ \_algebra A" + | UNIV: "UNIV \ \_algebra A" + | complement: "a \ \_algebra A ==> -a \ \_algebra A" + | Union: "(!!i::nat. a i \ \_algebra A) ==> (\i. a i) \ \_algebra A" text {* The following basic facts are consequences of the closure properties diff -r 28df61d931e2 -r a455e69c31cc src/HOL/Isar_examples/MutilatedCheckerboard.thy --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Jul 11 11:13:08 2007 +0200 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Jul 11 11:14:51 2007 +0200 @@ -17,13 +17,12 @@ subsection {* Tilings *} -consts +inductive_set tiling :: "'a set set => 'a set set" - -inductive "tiling A" - intros + for A :: "'a set set" + where empty: "{} : tiling A" - Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A" + | Un: "a : A ==> t : tiling A ==> a <= - t ==> a Un t : tiling A" text "The union of two disjoint tilings is a tiling." @@ -118,13 +117,11 @@ subsection {* Dominoes *} -consts +inductive_set domino :: "(nat * nat) set set" - -inductive domino - intros + where horiz: "{(i, j), (i, j + 1)} : domino" - vertl: "{(i, j), (i + 1, j)} : domino" + | vertl: "{(i, j), (i + 1, j)} : domino" lemma dominoes_tile_row: "{i} <*> below (2 * n) : tiling domino"