# HG changeset patch # User berghofe # Date 1184146093 -7200 # Node ID 1c4672d130b1a069a59dd2551ed3dad2fb1e1cf9 # Parent 75873e94357cceb4ab18e9293413a8e596261068 Adapted to new inductive definition package. diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Coinductive_List.thy --- a/src/HOL/Library/Coinductive_List.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Coinductive_List.thy Wed Jul 11 11:28:13 2007 +0200 @@ -38,17 +38,27 @@ subsection {* Corecursive lists *} -consts +coinductive_set LList :: "'a Datatype.item set \ 'a Datatype.item set" - -coinductive "LList A" - intros + for A :: "'a Datatype.item set" + where NIL [intro]: "NIL \ LList A" - CONS [intro]: "a \ A \ M \ LList A \ CONS a M \ LList A" + | CONS [intro]: "a \ A \ M \ LList A \ CONS a M \ LList A" -lemma LList_mono: "A \ B \ LList A \ LList B" +lemma LList_mono: + assumes subset: "A \ B" + shows "LList A \ LList B" -- {* This justifies using @{text LList} in other recursive type definitions. *} - unfolding LList.defs by (blast intro!: gfp_mono) +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 consts LList_corec_aux :: "nat \ ('a \ ('b Datatype.item \ 'a) option) \ @@ -92,7 +102,7 @@ lemma LList_corec_type: "LList_corec a f \ LList UNIV" proof - - have "LList_corec a f \ {LList_corec a f | a. True}" by blast + have "\x. LList_corec a f = LList_corec x f" by blast then show ?thesis proof coinduct case (LList L) @@ -185,7 +195,7 @@ with Abs_llist have "l = LNil" by (simp add: LNil_def) with LNil show ?thesis . next - case (CONS K a) + case (CONS a K) then have "K \ llist" by (blast intro: llistI) then obtain l' where "K = Rep_llist l'" by cases with CONS and Abs_llist obtain x where "l = LCons x l'" @@ -228,7 +238,7 @@ (is "?corec a \ _") proof (unfold llist_def) let "LList_corec a ?g" = "?corec a" - have "?corec a \ {?corec x | x. True}" by blast + have "\x. ?corec a = ?corec x" by blast then show "?corec a \ LList (range Datatype.Leaf)" proof coinduct case (LList L) @@ -282,14 +292,13 @@ subsection {* Equality as greatest fixed-point -- the bisimulation principle *} -consts +coinductive_set EqLList :: "('a Datatype.item \ 'a Datatype.item) set \ ('a Datatype.item \ 'a Datatype.item) set" - -coinductive "EqLList r" - intros + for r :: "('a Datatype.item \ 'a Datatype.item) set" + where EqNIL: "(NIL, NIL) \ EqLList r" - EqCONS: "(a, b) \ r \ (M, N) \ EqLList r \ + | EqCONS: "(a, b) \ r \ (M, N) \ EqLList r \ (CONS a M, CONS b N) \ EqLList r" lemma EqLList_unfold: @@ -310,10 +319,10 @@ done lemma Domain_EqLList: "Domain (EqLList (diag A)) \ LList A" - apply (simp add: LList.defs NIL_def CONS_def) - apply (rule gfp_upperbound) - apply (subst EqLList_unfold) - apply auto + apply (rule subsetI) + apply (erule LList.coinduct) + apply (subst (asm) EqLList_unfold) + apply (auto simp add: NIL_def CONS_def) done lemma EqLList_diag: "EqLList (diag A) = diag (LList A)" @@ -328,23 +337,23 @@ assumption) apply (erule DomainI [THEN Domain_EqLList [THEN subsetD]]) done - show "?rhs \ ?lhs" - proof - fix p assume "p \ diag (LList A)" - then show "p \ EqLList (diag A)" + { + fix M N assume "(M, N) \ diag (LList A)" + then have "(M, N) \ EqLList (diag A)" proof coinduct - case (EqLList q) - then obtain L where L: "L \ LList A" and q: "q = (L, L)" .. + case (EqLList M N) + then obtain L where L: "L \ LList A" and MN: "M = L" "N = L" by blast from L show ?case proof cases - case NIL with q have ?EqNIL by simp + case NIL with MN have ?EqNIL by simp then show ?thesis .. next - case CONS with q have ?EqCONS by (simp add: diagI) + case CONS with MN have ?EqCONS by (simp add: diagI) then show ?thesis .. qed qed - qed + } + then show "?rhs \ ?lhs" by auto qed lemma EqLList_diag_iff [iff]: "(p \ EqLList (diag A)) = (p \ diag (LList A))" @@ -359,11 +368,11 @@ lemma LList_equalityI [consumes 1, case_names EqLList, case_conclusion EqLList EqNIL EqCONS]: assumes r: "(M, N) \ r" - and step: "\p. p \ r \ - p = (NIL, NIL) \ - (\M N a b. - p = (CONS a M, CONS b N) \ (a, b) \ diag A \ - (M, N) \ r \ EqLList (diag A))" + and step: "\M N. (M, N) \ r \ + M = NIL \ N = NIL \ + (\a b M' N'. + M = CONS a M' \ N = CONS b N' \ (a, b) \ diag A \ + ((M', N') \ r \ (M', N') \ EqLList (diag A)))" shows "M = N" proof - from r have "(M, N) \ EqLList (diag A)" @@ -391,39 +400,39 @@ have "(f M, g M) \ ?bisim" using M by blast then show ?thesis proof (coinduct taking: A rule: LList_equalityI) - case (EqLList q) - then obtain L where q: "q = (f L, g L)" and L: "L \ LList A" by blast + case (EqLList M N) + then obtain L where MN: "M = f L" "N = g L" and L: "L \ LList A" by blast from L show ?case proof (cases L) case NIL - with fun_NIL and q have "q \ diag (LList A)" by auto - then have "q \ EqLList (diag A)" .. + with fun_NIL and MN have "(M, N) \ diag (LList A)" by auto + then have "(M, N) \ EqLList (diag A)" .. then show ?thesis by cases simp_all next - case (CONS K a) + case (CONS a K) from fun_CONS and `a \ A` `K \ LList A` have "?fun_CONS a K" (is "?NIL \ ?CONS") . then show ?thesis proof assume ?NIL - with q CONS have "q \ diag (LList A)" by auto - then have "q \ EqLList (diag A)" .. + with MN CONS have "(M, N) \ diag (LList A)" by auto + then have "(M, N) \ EqLList (diag A)" .. then show ?thesis by cases simp_all next assume ?CONS - with CONS obtain a b M N where - fg: "(f L, g L) = (CONS a M, CONS b N)" + with CONS obtain a b M' N' where + fg: "(f L, g L) = (CONS a M', CONS b N')" and ab: "(a, b) \ diag A" - and MN: "(M, N) \ ?bisim \ diag (LList A)" + and M'N': "(M', N') \ ?bisim \ diag (LList A)" by blast - from MN show ?thesis + from M'N' show ?thesis proof - assume "(M, N) \ ?bisim" - with q fg ab show ?thesis by simp + assume "(M', N') \ ?bisim" + with MN fg ab show ?thesis by simp next - assume "(M, N) \ diag (LList A)" - then have "(M, N) \ EqLList (diag A)" .. - with q fg ab show ?thesis by simp + assume "(M', N') \ diag (LList A)" + then have "(M', N') \ EqLList (diag A)" .. + with MN fg ab show ?thesis by simp qed qed qed @@ -446,18 +455,18 @@ have "(h x, h' x) \ {(h u, h' u) | u. True}" by blast then show "h x = h' x" proof (coinduct rule: LList_equalityI [where A = UNIV]) - case (EqLList q) - then obtain x where q: "q = (h x, h' x)" by blast + case (EqLList M N) + then obtain x where MN: "M = h x" "N = h' x" by blast show ?case proof (cases "f x") case None - with h h' q have ?EqNIL by simp + with h h' MN have ?EqNIL by simp then show ?thesis .. next case (Some p) - with h h' q have "q = - (CONS (fst p) (h (snd p)), CONS (fst p) (h' (snd p)))" - by (simp split: prod.split) + with h h' MN have "M = CONS (fst p) (h (snd p))" + and "N = CONS (fst p) (h' (snd p))" + by (simp_all split: prod.split) then have ?EqCONS by (auto iff: diag_iff) then show ?thesis .. qed @@ -481,18 +490,18 @@ by blast then have "M = N" proof (coinduct rule: LList_equalityI [where A = UNIV]) - case (EqLList q) + case (EqLList M N) then obtain l1 l2 where - q: "q = (Rep_llist l1, Rep_llist l2)" and r: "(l1, l2) \ r" + MN: "M = Rep_llist l1" "N = Rep_llist l2" and r: "(l1, l2) \ r" by auto from step [OF r] show ?case proof assume "?EqLNil (l1, l2)" - with q have ?EqNIL by (simp add: Rep_llist_LNil) + with MN have ?EqNIL by (simp add: Rep_llist_LNil) then show ?thesis .. next assume "?EqLCons (l1, l2)" - with q have ?EqCONS + with MN have ?EqCONS by (force simp add: Rep_llist_LCons EqLList_diag intro: Rep_llist_UNIV) then show ?thesis .. qed @@ -546,7 +555,7 @@ assumes "M \ A" shows "Lconst M \ LList A" proof - - have "Lconst M \ {Lconst M}" by simp + have "Lconst M \ {Lconst (id M)}" by simp then show ?thesis proof coinduct case (LList N) @@ -617,16 +626,16 @@ then show ?thesis proof (coinduct taking: "range (\N :: 'a Datatype.item. N)" rule: LList_equalityI) - case (EqLList q) - then obtain N where q: "q = (?lhs N, ?rhs N)" and N: "N \ LList A" by blast + case (EqLList L M) + then obtain N where LM: "L = ?lhs N" "M = ?rhs N" and N: "N \ LList A" by blast from N show ?case proof cases case NIL - with q have ?EqNIL by simp + with LM have ?EqNIL by simp then show ?thesis .. next case CONS - with q have ?EqCONS by auto + with LM have ?EqCONS by auto then show ?thesis .. qed qed @@ -640,16 +649,16 @@ then show ?thesis proof (coinduct taking: "range (\N :: 'a Datatype.item. N)" rule: LList_equalityI) - case (EqLList q) - then obtain N where q: "q = (?lmap N, N)" and N: "N \ LList A" by blast + case (EqLList L M) + then obtain N where LM: "L = ?lmap N" "M = N" and N: "N \ LList A" by blast from N show ?case proof cases case NIL - with q have ?EqNIL by simp + with LM have ?EqNIL by simp then show ?thesis .. next case CONS - with q have ?EqCONS by auto + with LM have ?EqCONS by auto then show ?thesis .. qed qed diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Graphs.thy --- a/src/HOL/Library/Graphs.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Graphs.thy Wed Jul 11 11:28:13 2007 +0200 @@ -321,7 +321,7 @@ types ('n, 'e) fpath = "('n \ ('e \ 'n) list)" -inductive2 has_fpath :: "('n, 'e) graph \ ('n, 'e) fpath \ bool" +inductive has_fpath :: "('n, 'e) graph \ ('n, 'e) fpath \ bool" for G :: "('n, 'e) graph" where has_fpath_empty: "has_fpath G (n, [])" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Permutation.thy Wed Jul 11 11:28:13 2007 +0200 @@ -8,19 +8,13 @@ imports Multiset begin -consts - perm :: "('a list * 'a list) set" - -abbreviation - perm_rel :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) where - "x <~~> y == (x, y) \ perm" - -inductive perm - intros +inductive + perm :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) + where Nil [intro!]: "[] <~~> []" - swap [intro!]: "y # x # l <~~> x # y # l" - Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys" - trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs" + | swap [intro!]: "y # x # l <~~> x # y # l" + | Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys" + | trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs" lemma perm_refl [iff]: "l <~~> l" by (induct l) auto diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/Library/Zorn.thy Wed Jul 11 11:28:13 2007 +0200 @@ -33,12 +33,12 @@ (if c \ chain S | c \ maxchain S then c else SOME c'. c' \ super S c)" -consts +inductive_set TFin :: "'a set set => 'a set set set" -inductive "TFin S" - intros + for S :: "'a set set" + where succI: "x \ TFin S ==> succ S x \ TFin S" - Pow_UnionI: "Y \ Pow(TFin S) ==> Union(Y) \ TFin S" + | Pow_UnionI: "Y \ Pow(TFin S) ==> Union(Y) \ TFin S" monos Pow_mono diff -r 75873e94357c -r 1c4672d130b1 src/HOL/MetisExamples/Message.thy --- a/src/HOL/MetisExamples/Message.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/MetisExamples/Message.thy Wed Jul 11 11:28:13 2007 +0200 @@ -68,13 +68,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" ML{*ResAtp.problem_name := "Message__parts_mono"*} @@ -329,13 +330,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" @@ -456,14 +458,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 75873e94357c -r 1c4672d130b1 src/HOL/NanoJava/AxSem.thy --- a/src/HOL/NanoJava/AxSem.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/NanoJava/AxSem.thy Wed Jul 11 11:28:13 2007 +0200 @@ -18,116 +18,102 @@ "triple" \ (type)"assn \ stmt \ assn" "etriple" \ (type)"assn \ expr \ vassn" -consts hoare :: "(triple set \ triple set) set" -consts ehoare :: "(triple set \ etriple ) set" -syntax (xsymbols) - "@hoare" :: "[triple set, triple set ] => bool" ("_ |\/ _" [61,61] 60) - "@hoare1" :: "[triple set, assn,stmt,assn] => bool" - ("_ \/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60) -"@ehoare" :: "[triple set, etriple ] => bool" ("_ |\\<^sub>e/ _"[61,61]60) -"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool" - ("_ \\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60) -syntax - "@hoare" :: "[triple set, triple set ] => bool" ("_ ||-/ _" [61,61] 60) - "@hoare1" :: "[triple set, assn,stmt,assn] => bool" - ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60) -"@ehoare" :: "[triple set, etriple ] => bool" ("_ ||-e/ _"[61,61] 60) -"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool" - ("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60) - -translations "A |\ C" \ "(A,C) \ hoare" - "A \ {P}c{Q}" \ "A |\ {(P,c,Q)}" - "A |\\<^sub>e t" \ "(A,t) \ ehoare" - "A |\\<^sub>e (P,e,Q)" \ "(A,P,e,Q) \ ehoare" (* shouldn't be necessary *) - "A \\<^sub>e {P}e{Q}" \ "A |\\<^sub>e (P,e,Q)" - subsection "Hoare Logic Rules" -inductive hoare ehoare -intros - - Skip: "A |- {P} Skip {P}" - - Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}" +inductive + hoare :: "[triple set, triple set] => bool" ("_ |\/ _" [61, 61] 60) + and ehoare :: "[triple set, etriple] => bool" ("_ |\\<^sub>e/ _" [61, 61] 60) + and hoare1 :: "[triple set, assn,stmt,assn] => bool" + ("_ \/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60) + and ehoare1 :: "[triple set, assn,expr,vassn]=> bool" + ("_ \\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60) +where - Cond: "[| A |-e {P} e {Q}; - \v. A |- {Q v} (if v \ Null then c1 else c2) {R} |] ==> - A |- {P} If(e) c1 Else c2 {R}" + "A \ {P}c{Q} \ A |\ {(P,c,Q)}" +| "A \\<^sub>e {P}e{Q} \ A |\\<^sub>e (P,e,Q)" - Loop: "A |- {\s. P s \ s \ Null} c {P} ==> - A |- {P} While(x) c {\s. P s \ s = Null}" +| Skip: "A \ {P} Skip {P}" + +| Comp: "[| A \ {P} c1 {Q}; A \ {Q} c2 {R} |] ==> A \ {P} c1;;c2 {R}" - LAcc: "A |-e {\s. P (s) s} LAcc x {P}" +| Cond: "[| A \\<^sub>e {P} e {Q}; + \v. A \ {Q v} (if v \ Null then c1 else c2) {R} |] ==> + A \ {P} If(e) c1 Else c2 {R}" - LAss: "A |-e {P} e {\v s. Q (lupd(x\v) s)} ==> - A |- {P} x:==e {Q}" +| Loop: "A \ {\s. P s \ s \ Null} c {P} ==> + A \ {P} While(x) c {\s. P s \ s = Null}" + +| LAcc: "A \\<^sub>e {\s. P (s) s} LAcc x {P}" - FAcc: "A |-e {P} e {\v s. \a. v=Addr a --> Q (get_field s a f) s} ==> - A |-e {P} e..f {Q}" +| LAss: "A \\<^sub>e {P} e {\v s. Q (lupd(x\v) s)} ==> + A \ {P} x:==e {Q}" + +| FAcc: "A \\<^sub>e {P} e {\v s. \a. v=Addr a --> Q (get_field s a f) s} ==> + A \\<^sub>e {P} e..f {Q}" - FAss: "[| A |-e {P} e1 {\v s. \a. v=Addr a --> Q a s}; - \a. A |-e {Q a} e2 {\v s. R (upd_obj a f v s)} |] ==> - A |- {P} e1..f:==e2 {R}" +| FAss: "[| A \\<^sub>e {P} e1 {\v s. \a. v=Addr a --> Q a s}; + \a. A \\<^sub>e {Q a} e2 {\v s. R (upd_obj a f v s)} |] ==> + A \ {P} e1..f:==e2 {R}" - NewC: "A |-e {\s. \a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)} +| NewC: "A \\<^sub>e {\s. \a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)} new C {P}" - Cast: "A |-e {P} e {\v s. (case v of Null => True +| Cast: "A \\<^sub>e {P} e {\v s. (case v of Null => True | Addr a => obj_class s a <=C C) --> Q v s} ==> - A |-e {P} Cast C e {Q}" + A \\<^sub>e {P} Cast C e {Q}" - Call: "[| A |-e {P} e1 {Q}; \a. A |-e {Q a} e2 {R a}; - \a p ls. A |- {\s'. \s. R a p s \ ls = s \ +| Call: "[| A \\<^sub>e {P} e1 {Q}; \a. A \\<^sub>e {Q a} e2 {R a}; + \a p ls. A \ {\s'. \s. R a p s \ ls = s \ s' = lupd(This\a)(lupd(Par\p)(del_locs s))} Meth (C,m) {\s. S (s) (set_locs ls s)} |] ==> - A |-e {P} {C}e1..m(e2) {S}" + A \\<^sub>e {P} {C}e1..m(e2) {S}" - Meth: "\D. A |- {\s'. \s a. s = Addr a \ D = obj_class s a \ D <=C C \ +| Meth: "\D. A \ {\s'. \s a. s = Addr a \ D = obj_class s a \ D <=C C \ P s \ s' = init_locs D m s} Impl (D,m) {Q} ==> - A |- {P} Meth (C,m) {Q}" + A \ {P} Meth (C,m) {Q}" --{* @{text "\Z"} instead of @{text "\Z"} in the conclusion and\\ Z restricted to type state due to limitations of the inductive package *} - Impl: "\Z::state. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- +| Impl: "\Z::state. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\ (\Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> - A ||- (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" + A |\ (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" --{* structural rules *} - Asm: " a \ A ==> A ||- {a}" +| Asm: " a \ A ==> A |\ {a}" - ConjI: " \c \ C. A ||- {c} ==> A ||- C" +| ConjI: " \c \ C. A |\ {c} ==> A |\ C" - ConjE: "[|A ||- C; c \ C |] ==> A ||- {c}" +| ConjE: "[|A |\ C; c \ C |] ==> A |\ {c}" --{* Z restricted to type state due to limitations of the inductive package *} - Conseq:"[| \Z::state. A |- {P' Z} c {Q' Z}; +| Conseq:"[| \Z::state. A \ {P' Z} c {Q' Z}; \s t. (\Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> - A |- {P} c {Q }" + A \ {P} c {Q }" --{* Z restricted to type state due to limitations of the inductive package *} - eConseq:"[| \Z::state. A |-e {P' Z} e {Q' Z}; +| eConseq:"[| \Z::state. A \\<^sub>e {P' Z} e {Q' Z}; \s v t. (\Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> - A |-e {P} e {Q }" + A \\<^sub>e {P} e {Q }" subsection "Fully polymorphic variants, required for Example only" axioms - Conseq:"[| \Z. A |- {P' Z} c {Q' Z}; + Conseq:"[| \Z. A \ {P' Z} c {Q' Z}; \s t. (\Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> - A |- {P} c {Q }" + A \ {P} c {Q }" - eConseq:"[| \Z. A |-e {P' Z} e {Q' Z}; + eConseq:"[| \Z. A \\<^sub>e {P' Z} e {Q' Z}; \s v t. (\Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> - A |-e {P} e {Q }" + A \\<^sub>e {P} e {Q }" - Impl: "\Z. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- + Impl: "\Z. A\ (\Z. (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\ (\Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> - A ||- (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" + A |\ (\Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" subsection "Derived Rules" diff -r 75873e94357c -r 1c4672d130b1 src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Wed Jul 11 11:27:46 2007 +0200 +++ b/src/HOL/NanoJava/Equivalence.thy Wed Jul 11 11:28:13 2007 +0200 @@ -12,17 +12,17 @@ constdefs valid :: "[assn,stmt, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) - "|= {P} c {Q} \ \s t. P s --> (\n. s -c -n-> t) --> Q t" + "|= {P} c {Q} \ \s t. P s --> (\n. s -c -n\ t) --> Q t" evalid :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) - "|=e {P} e {Q} \ \s v t. P s --> (\