# HG changeset patch # User clasohm # Date 796044635 -3600 # Node ID e61b058d58d254b86ac8247b62cabc9d28df9ddc # Parent f4815812665bf91107b499cd7cfbac147dd4fc4a changed syntax of tuples from <..., ...> to (..., ...) diff -r f4815812665b -r e61b058d58d2 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Arith.ML Fri Mar 24 12:30:35 1995 +0100 @@ -175,7 +175,7 @@ val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans); -goalw Nat.thy [less_def] " : pred_nat^+ = (mn. + m - n = 0 iff m<=n and m - n = Suc(k) iff m)n. Also, nat_rec(m, 0, %z w.z) is pred(m). *) diff -r f4815812665b -r e61b058d58d2 src/HOL/IMP/Com.thy --- a/src/HOL/IMP/Com.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IMP/Com.thy Fri Mar 24 12:30:35 1995 +0100 @@ -26,9 +26,9 @@ (** Evaluation of arithmetic expressions **) consts evala :: "(aexp*state*nat)set" - "@evala" :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _" [0,0,50] 50) + "@evala" :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _" [0,0,50] 50) translations - " -a-> n" == " : evala" + " -a-> n" == "(ae,sig,n) : evala" inductive "evala" intrs N " -a-> n" @@ -51,10 +51,10 @@ (** Evaluation of boolean expressions **) consts evalb :: "(bexp*state*bool)set" - "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _" [0,0,50] 50) + "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _" [0,0,50] 50) translations - " -b-> b" == " : evalb" + " -b-> b" == "(be,sig,b) : evalb" inductive "evalb" intrs (*avoid clash with ML constructors true, false*) @@ -79,11 +79,11 @@ (** Execution of commands **) consts evalc :: "(com*state*state)set" - "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50) - "assign" :: "[state,nat,loc] => state" ("_[_'/_]" [95,0,0] 95) + "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50) + "assign" :: "[state,nat,loc] => state" ("_[_'/_]" [95,0,0] 95) translations - " -c-> s" == " : evalc" + " -c-> s" == "(ce,sig,s) : evalc" rules assign_def "s[m/x] == (%y. if y=x then m else s y)" diff -r f4815812665b -r e61b058d58d2 src/HOL/IMP/Equiv.ML --- a/src/HOL/IMP/Equiv.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IMP/Equiv.ML Fri Mar 24 12:30:35 1995 +0100 @@ -25,7 +25,7 @@ val BfstD = read_instantiate_sg (sign_of Equiv.thy) [("P","%x.B ?b x")] (fst_conv RS subst); -goal Equiv.thy "!!c. -c-> t ==> : C(c)"; +goal Equiv.thy "!!c. -c-> t ==> (s,t) : C(c)"; (* start with rule induction *) be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; diff -r f4815812665b -r e61b058d58d2 src/HOL/IMP/Hoare.ML --- a/src/HOL/IMP/Hoare.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IMP/Hoare.ML Fri Mar 24 12:30:35 1995 +0100 @@ -39,8 +39,8 @@ qed"hoare_if"; val major::prems = goal Hoare.thy - "[| :lfp f; mono f; \ -\ !!a b. : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b"; + "[| (a,b) :lfp f; mono f; \ +\ !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b"; by(res_inst_tac [("c1","P")] (split RS subst) 1); br (major RS induct) 1; brs prems 1; diff -r f4815812665b -r e61b058d58d2 src/HOL/IMP/Hoare.thy --- a/src/HOL/IMP/Hoare.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IMP/Hoare.thy Fri Mar 24 12:30:35 1995 +0100 @@ -12,7 +12,7 @@ (* syntax "@spec" :: "[bool,com,bool] => bool" *) ("{{(1_)}}/ (_)/ {{(1_)}}" 10) defs - spec_def "spec P c Q == !s t. : C(c) --> P s --> Q t" + spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t" end (* Pretty-printing of assertions. Not very helpful as long as programs are not pretty-printed. diff -r f4815812665b -r e61b058d58d2 src/HOL/IOA/meta_theory/Asig.thy --- a/src/HOL/IOA/meta_theory/Asig.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IOA/meta_theory/Asig.thy Fri Mar 24 12:30:35 1995 +0100 @@ -39,7 +39,7 @@ mk_ext_asig_def - "mk_ext_asig(triple) == " + "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" end diff -r f4815812665b -r e61b058d58d2 src/HOL/IOA/meta_theory/IOA.ML --- a/src/HOL/IOA/meta_theory/IOA.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IOA/meta_theory/IOA.ML Fri Mar 24 12:30:35 1995 +0100 @@ -13,12 +13,12 @@ val exec_rws = [executions_def,is_execution_fragment_def]; goal IOA.thy -"asig_of() = x & starts_of() = y & trans_of() = z"; +"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z"; by (simp_tac (SS addsimps ioa_projections) 1); qed "ioa_triple_proj"; goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def] - "!!A. [| IOA(A); :trans_of(A) |] ==> a:actions(asig_of(A))"; + "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))"; by (REPEAT(etac conjE 1)); by (EVERY1[etac allE, etac impE, atac]); by (asm_full_simp_tac SS 1); @@ -45,18 +45,18 @@ qed "mk_behaviour_thm"; goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s"; - by (res_inst_tac [("x","<%i.None,%i.s>")] bexI 1); + by (res_inst_tac [("x","(%i.None,%i.s)")] bexI 1); by (simp_tac SS 1); by (asm_simp_tac (SS addsimps exec_rws) 1); qed "reachable_0"; goalw IOA.thy (reachable_def::exec_rws) -"!!A. [| reachable A s; : trans_of(A) |] ==> reachable A t"; +"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; by(asm_full_simp_tac SS 1); by(safe_tac set_cs); - by(res_inst_tac [("x","<%i.if i")] bexI 1); +\ %i.if i P(s); \ -\ !!s t a. [|reachable A s; P(s)|] ==> : trans_of(A) --> P(t) |] \ +\ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \ \ ==> invariant A P"; by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); by (safe_tac set_cs); @@ -91,7 +91,7 @@ val [p1,p2] = goal IOA.thy "[| !!s. s : starts_of(A) ==> P(s); \ -\ !!s t a. reachable A s ==> P(s) --> :trans_of(A) --> P(t) \ +\ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \ \ |] ==> invariant A P"; by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1); qed "invariantI1"; @@ -121,18 +121,18 @@ goal IOA.thy -" : trans_of(A || B || C || D) = \ +"(s,a,t) : trans_of(A || B || C || D) = \ \ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | \ \ a:actions(asig_of(D))) & \ -\ (if a:actions(asig_of(A)) then :trans_of(A) \ +\ (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) \ \ else fst t=fst s) & \ -\ (if a:actions(asig_of(B)) then :trans_of(B) \ +\ (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) \ \ else fst(snd(t))=fst(snd(s))) & \ \ (if a:actions(asig_of(C)) then \ -\ :trans_of(C) \ +\ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) \ \ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \ \ (if a:actions(asig_of(D)) then \ -\ :trans_of(D) \ +\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ \ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; by(simp_tac (SS addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@ ioa_projections) diff -r f4815812665b -r e61b058d58d2 src/HOL/IOA/meta_theory/IOA.thy --- a/src/HOL/IOA/meta_theory/IOA.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IOA/meta_theory/IOA.thy Fri Mar 24 12:30:35 1995 +0100 @@ -62,7 +62,7 @@ state_trans_def "state_trans asig R == \ \ (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \ - \ (!a. (a:inputs(asig)) --> (!s1. ? s2. :R))" + \ (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" asig_of_def "asig_of == fst" @@ -83,7 +83,7 @@ "is_execution_fragment A ex == \ \ let act = fst(ex); state = snd(ex) \ \ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & \ - \ (act(n)=Some(a) --> :trans_of(A))" + \ (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))" executions_def @@ -98,7 +98,7 @@ * ---------------- * reachable(ioa,x) * - * reachable(ioa,s) & ? :trans_of(ioa) + * reachable(ioa,s) & ? (s,a,s'):trans_of(ioa) * ------------------------------------------- * reachable(ioa,s') * @@ -147,35 +147,35 @@ asig_comp_def "asig_comp a1 a2 == \ - \ (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), \ + \ (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), \ \ (outputs(a1) Un outputs(a2)), \ - \ (internals(a1) Un internals(a2))>)" + \ (internals(a1) Un internals(a2))))" par_def "(ioa1 || ioa2) == \ - \ :trans_of(ioa1) \ + \ (fst(s),a,fst(t)):trans_of(ioa1) \ \ else fst(t) = fst(s)) \ \ & \ \ (if a:actions(asig_of(ioa2)) then \ - \ :trans_of(ioa2) \ - \ else snd(t) = snd(s))}>" + \ (snd(s),a,snd(t)):trans_of(ioa2) \ + \ else snd(t) = snd(s))})" restrict_asig_def "restrict_asig asig actns == \ -\ " +\ (inputs(asig) Int actns, outputs(asig) Int actns, \ +\ internals(asig) Un (externals(asig) - actns))" restrict_def "restrict ioa actns == \ -\ " +\ (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))" ioa_implements_def diff -r f4815812665b -r e61b058d58d2 src/HOL/IOA/meta_theory/Solve.ML --- a/src/HOL/IOA/meta_theory/Solve.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IOA/meta_theory/Solve.ML Fri Mar 24 12:30:35 1995 +0100 @@ -18,7 +18,7 @@ by (safe_tac set_cs); (* give execution of abstract automata *) - by (res_inst_tac[("x","")] bexI 1); + by (res_inst_tac[("x","(mk_behaviour A (fst ex),%i.f(snd ex i))")] bexI 1); (* Behaviours coincide *) by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1); diff -r f4815812665b -r e61b058d58d2 src/HOL/IOA/meta_theory/Solve.thy --- a/src/HOL/IOA/meta_theory/Solve.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/IOA/meta_theory/Solve.thy Fri Mar 24 12:30:35 1995 +0100 @@ -18,9 +18,9 @@ "is_weak_pmap f C A == \ \ (!s:starts_of(C). f(s):starts_of(A)) & \ \ (!s t a. reachable C s & \ -\ :trans_of(C) \ +\ (s,a,t):trans_of(C) \ \ --> (if a:externals(asig_of(C)) then \ -\ :trans_of(A) \ +\ (f(s),a,f(t)):trans_of(A) \ \ else f(s)=f(t)))" end diff -r f4815812665b -r e61b058d58d2 src/HOL/Integ/Equiv.ML --- a/src/HOL/Integ/Equiv.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Integ/Equiv.ML Fri Mar 24 12:30:35 1995 +0100 @@ -19,24 +19,24 @@ by (fast_tac (comp_cs addSEs [converseD]) 1); qed "sym_trans_comp_subset"; -val [major,minor]=goal Equiv.thy "[|:r; z=|] ==> z:r"; +val [major,minor]=goal Equiv.thy "[|(x,y):r; z=(x,y)|] ==> z:r"; by (simp_tac (prod_ss addsimps [minor]) 1); by (rtac major 1); qed "BreakPair"; -val [major]=goal Equiv.thy "[|? x y. :r & z=|] ==> z:r"; +val [major]=goal Equiv.thy "[|? x y. (x,y):r & z=(x,y)|] ==> z:r"; by (resolve_tac [major RS exE] 1); by (etac exE 1); by (etac conjE 1); by (asm_simp_tac (prod_ss addsimps [minor]) 1); qed "BreakPair1"; -val [major,minor]=goal Equiv.thy "[|z:r; z=|] ==> :r"; +val [major,minor]=goal Equiv.thy "[|z:r; z=(x,y)|] ==> (x,y):r"; by (simp_tac (prod_ss addsimps [minor RS sym]) 1); by (rtac major 1); qed "BuildPair"; -val [major]=goal Equiv.thy "[|? z:r. =z|] ==> :r"; +val [major]=goal Equiv.thy "[|? z:r. (x,y)=z|] ==> (x,y):r"; by (resolve_tac [major RS bexE] 1); by (asm_simp_tac (prod_ss addsimps []) 1); qed "BuildPair1"; @@ -65,7 +65,7 @@ goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def] "!!A r. [| converse(r) O r = r; Domain(r) = A |] ==> equiv A r"; by (etac equalityE 1); -by (subgoal_tac "ALL x y. : r --> : r" 1); +by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1); by (safe_tac set_cs); by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3); by (fast_tac (set_cs addSIs [converseI] addIs [compI] addSEs [DomainE]) 2); @@ -84,14 +84,14 @@ (*Lemma for the next result*) goalw Equiv.thy [equiv_def,trans_def,sym_def] - "!!A r. [| equiv A r; : r |] ==> r^^{a} <= r^^{b}"; + "!!A r. [| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}"; by (safe_tac rel_cs); by (rtac ImageI 1); by (fast_tac rel_cs 2); by (fast_tac rel_cs 1); qed "equiv_class_subset"; -goal Equiv.thy "!!A r. [| equiv A r; : r |] ==> r^^{a} = r^^{b}"; +goal Equiv.thy "!!A r. [| equiv A r; (a,b): r |] ==> r^^{a} = r^^{b}"; by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); by (rewrite_goals_tac [equiv_def,sym_def]); by (fast_tac rel_cs 1); @@ -105,18 +105,18 @@ (*Lemma for the next result*) goalw Equiv.thy [equiv_def,refl_def] - "!!A r. [| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> : r"; + "!!A r. [| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r"; by (fast_tac rel_cs 1); qed "subset_equiv_class"; val prems = goal Equiv.thy - "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> : r"; + "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r"; by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1)); qed "eq_equiv_class"; (*thus r^^{a} = r^^{b} as well*) goalw Equiv.thy [equiv_def,trans_def,sym_def] - "!!A r. [| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> : r"; + "!!A r. [| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r"; by (fast_tac rel_cs 1); qed "equiv_class_nondisjoint"; @@ -126,7 +126,7 @@ qed "equiv_type"; goal Equiv.thy - "!!A r. equiv A r ==> (: r) = (r^^{x} = r^^{y} & x:A & y:A)"; + "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)"; by (safe_tac rel_cs); by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1)); by ((rtac eq_equiv_class 3) THEN @@ -138,7 +138,7 @@ qed "equiv_class_eq_iff"; goal Equiv.thy - "!!A r. [| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = (: r)"; + "!!A r. [| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)"; by (safe_tac rel_cs); by ((rtac eq_equiv_class 1) THEN (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1)); @@ -227,7 +227,7 @@ val _::_::prems = goalw Equiv.thy [quotient_def] "[| equiv A r; congruent r b; \ \ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \ -\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> :r |] \ +\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \ \ ==> X=Y"; by (cut_facts_tac prems 1); by (safe_tac rel_cs); @@ -286,8 +286,8 @@ than the direct proof*) val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def] "[| equiv A r; \ -\ !! y z w. [| w: A; : r |] ==> b y w = b z w; \ -\ !! y z w. [| w: A; : r |] ==> b w y = b w z \ +\ !! y z w. [| w: A; (y,z) : r |] ==> b y w = b z w; \ +\ !! y z w. [| w: A; (y,z) : r |] ==> b w y = b w z \ \ |] ==> congruent2 r b"; by (cut_facts_tac prems 1); by (safe_tac rel_cs); @@ -299,7 +299,7 @@ val [equivA,commute,congt] = goal Equiv.thy "[| equiv A r; \ \ !! y z. [| y: A; z: A |] ==> b y z = b z y; \ -\ !! y z w. [| w: A; : r |] ==> b w y = b w z \ +\ !! y z w. [| w: A; (y,z): r |] ==> b w y = b w z \ \ |] ==> congruent2 r b"; by (resolve_tac [equivA RS congruent2I] 1); by (rtac (commute RS trans) 1); diff -r f4815812665b -r e61b058d58d2 src/HOL/Integ/Equiv.thy --- a/src/HOL/Integ/Equiv.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Integ/Equiv.thy Fri Mar 24 12:30:35 1995 +0100 @@ -18,11 +18,11 @@ congruent2 :: "[('a*'a) set,['a,'a]=>'b]=>bool" defs - refl_def "refl A r == r <= Sigma A (%x.A) & (ALL x: A. : r)" - sym_def "sym(r) == ALL x y. : r --> : r" + refl_def "refl A r == r <= Sigma A (%x.A) & (ALL x: A. (x,x) : r)" + sym_def "sym(r) == ALL x y. (x,y): r --> (y,x): r" equiv_def "equiv A r == refl A r & sym(r) & trans(r)" quotient_def "A/r == UN x:A. {r^^{x}}" - congruent_def "congruent r b == ALL y z. :r --> b(y)=b(z)" + congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. \ -\ :r --> :r --> b y1 y2 = b z1 z2" +\ (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2" end diff -r f4815812665b -r e61b058d58d2 src/HOL/Integ/Integ.ML --- a/src/HOL/Integ/Integ.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Integ/Integ.ML Fri Mar 24 12:30:35 1995 +0100 @@ -34,20 +34,20 @@ val prems = goalw Integ.thy [intrel_def] "[| x1+y2 = x2+y1|] ==> \ -\ <,>: intrel"; +\ ((x1,y1),(x2,y2)): intrel"; by (fast_tac (rel_cs addIs prems) 1); qed "intrelI"; (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) goalw Integ.thy [intrel_def] "p: intrel --> (EX x1 y1 x2 y2. \ -\ p = <,> & x1+y2 = x2+y1)"; +\ p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)"; by (fast_tac rel_cs 1); qed "intrelE_lemma"; val [major,minor] = goal Integ.thy "[| p: intrel; \ -\ !!x1 y1 x2 y2. [| p = <,>; x1+y2 = x2+y1|] ==> Q |] \ +\ !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1|] ==> Q |] \ \ ==> Q"; by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1); by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); @@ -55,11 +55,11 @@ val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE]; -goal Integ.thy "<,>: intrel = (x1+y2 = x2+y1)"; +goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)"; by (fast_tac intrel_cs 1); qed "intrel_iff"; -goal Integ.thy ": intrel"; +goal Integ.thy "(x,x): intrel"; by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1); qed "intrel_refl"; @@ -74,7 +74,7 @@ ([CollectI, CollectI] MRS (equiv_intrel RS eq_equiv_class_iff)); -goalw Integ.thy [Integ_def,intrel_def,quotient_def] "intrel^^{}:Integ"; +goalw Integ.thy [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ"; by (fast_tac set_cs 1); qed "intrel_in_integ"; @@ -113,7 +113,7 @@ (**** zminus: unary negation on Integ ****) goalw Integ.thy [congruent_def] - "congruent intrel (%p. split (%x y. intrel^^{}) p)"; + "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)"; by (safe_tac intrel_cs); by (asm_simp_tac (intrel_ss addsimps add_ac) 1); qed "zminus_congruent"; @@ -123,7 +123,7 @@ val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; goalw Integ.thy [zminus_def] - "$~ Abs_Integ(intrel^^{}) = Abs_Integ(intrel ^^ {})"; + "$~ Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})"; by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); by (simp_tac (set_ss addsimps [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1); @@ -133,7 +133,7 @@ (*by lcp*) val [prem] = goal Integ.thy - "(!!x y. z = Abs_Integ(intrel^^{}) ==> P) ==> P"; + "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P"; by (res_inst_tac [("x1","z")] (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1); by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1); @@ -202,7 +202,7 @@ qed "diff_Suc_add_inverse"; goalw Integ.thy [congruent_def] - "congruent intrel (split (%x y. intrel^^{<(y-x) + (x-(y::nat)),0>}))"; + "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))"; by (safe_tac intrel_cs); by (asm_simp_tac intrel_ss 1); by (etac rev_mp 1); @@ -225,8 +225,8 @@ goalw Integ.thy [zmagnitude_def] - "zmagnitude (Abs_Integ(intrel^^{})) = \ -\ Abs_Integ(intrel^^{<(y - x) + (x - y),0>})"; + "zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \ +\ Abs_Integ(intrel^^{((y - x) + (x - y),0)})"; by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); by (asm_simp_tac (intrel_ss addsimps [zmagnitude_ize UN_equiv_class]) 1); qed "zmagnitude"; @@ -246,7 +246,7 @@ goalw Integ.thy [congruent2_def] "congruent2 intrel (%p1 p2. \ -\ split (%x1 y1. split (%x2 y2. intrel^^{}) p2) p1)"; +\ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"; (*Proof via congruent2_commuteI seems longer*) by (safe_tac intrel_cs); by (asm_simp_tac (intrel_ss addsimps [add_assoc]) 1); @@ -260,8 +260,8 @@ val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; goalw Integ.thy [zadd_def] - "Abs_Integ(intrel^^{}) + Abs_Integ(intrel^^{}) = \ -\ Abs_Integ(intrel^^{})"; + "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ +\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; by (asm_simp_tac (intrel_ss addsimps [zadd_ize UN_equiv_class2]) 1); qed "zadd"; @@ -333,7 +333,7 @@ goal Integ.thy "congruent2 intrel (%p1 p2. \ \ split (%x1 y1. split (%x2 y2. \ -\ intrel^^{}) p2) p1)"; +\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"; by (rtac (equiv_intrel RS congruent2_commuteI) 1); by (safe_tac intrel_cs); by (rewtac split_def); @@ -352,8 +352,8 @@ val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; goalw Integ.thy [zmult_def] - "Abs_Integ((intrel^^{})) * Abs_Integ((intrel^^{})) = \ -\ Abs_Integ(intrel ^^ {})"; + "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ +\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; by (simp_tac (intrel_ss addsimps [zmult_ize UN_equiv_class2]) 1); qed "zmult"; diff -r f4815812665b -r e61b058d58d2 src/HOL/Integ/Integ.thy --- a/src/HOL/Integ/Integ.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Integ/Integ.thy Fri Mar 24 12:30:35 1995 +0100 @@ -14,7 +14,7 @@ defs intrel_def - "intrel == {p. ? x1 y1 x2 y2. p=<,> & x1+y2 = x2+y1}" + "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}" subtype (Integ) int = "{x::(nat*nat).True}/intrel" ("quotient_def") @@ -35,21 +35,21 @@ defs zNat_def "zNat == {x::nat. True}" - znat_def "$# m == Abs_Integ(intrel ^^ {})" + znat_def "$# m == Abs_Integ(intrel ^^ {(m,0)})" zminus_def - "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{}) p)" + "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)" znegative_def - "znegative(Z) == EX x y. x:Rep_Integ(Z)" + "znegative(Z) == EX x y. x}) p)" + "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)" zadd_def "Z1 + Z2 == \ \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). \ -\ split (%x1 y1. split (%x2 y2. intrel^^{}) p2) p1)" +\ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)" @@ -60,19 +60,19 @@ zmult_def "Z1 * Z2 == \ \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \ -\ split (%x2 y2. intrel^^{}) p2) p1)" +\ split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)" zdiv_def "Z1 zdiv Z2 == \ \ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \ -\ split (%x2 y2. intrel^^{<(x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), \ -\ (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2)>}) p2) p1)" +\ split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), \ +\ (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)" zmod_def "Z1 zmod Z2 == \ \ Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1. \ -\ split (%x2 y2. intrel^^{<(x1-y1)mod((x2-y2)+(y2-x2)), \ -\ (x1-y1)mod((x2-y2)+(x2-y2))>}) p2) p1)" +\ split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)), \ +\ (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)" zsuc_def "zsuc(Z) == Z + $# Suc(0)" diff -r f4815812665b -r e61b058d58d2 src/HOL/Integ/Relation.ML --- a/src/HOL/Integ/Relation.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Integ/Relation.ML Fri Mar 24 12:30:35 1995 +0100 @@ -12,18 +12,18 @@ open Relation; -goalw Relation.thy [converse_def] "!!a b r. :r ==> :converse(r)"; +goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)"; by (simp_tac prod_ss 1); by (fast_tac set_cs 1); qed "converseI"; -goalw Relation.thy [converse_def] "!!a b r. : converse(r) ==> : r"; +goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r"; by (fast_tac comp_cs 1); qed "converseD"; qed_goalw "converseE" Relation.thy [converse_def] "[| yx : converse(r); \ -\ !!x y. [| yx=; :r |] ==> P \ +\ !!x y. [| yx=(y,x); (x,y):r |] ==> P \ \ |] ==> P" (fn [major,minor]=> [ (rtac (major RS CollectE) 1), @@ -35,23 +35,23 @@ addSEs [converseD,converseE]; qed_goalw "Domain_iff" Relation.thy [Domain_def] - "a: Domain(r) = (EX y. : r)" + "a: Domain(r) = (EX y. (a,y): r)" (fn _=> [ (fast_tac comp_cs 1) ]); -qed_goal "DomainI" Relation.thy "!!a b r. : r ==> a: Domain(r)" +qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)" (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]); qed_goal "DomainE" Relation.thy - "[| a : Domain(r); !!y. : r ==> P |] ==> P" + "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P" (fn prems=> [ (rtac (Domain_iff RS iffD1 RS exE) 1), (REPEAT (ares_tac prems 1)) ]); -qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.: r ==> b : Range(r)" +qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)" (fn _ => [ (etac (converseI RS DomainI) 1) ]); qed_goalw "RangeE" Relation.thy [Range_def] - "[| b : Range(r); !!x. : r ==> P |] ==> P" + "[| b : Range(r); !!x. (x,b): r ==> P |] ==> P" (fn major::prems=> [ (rtac (major RS DomainE) 1), (resolve_tac prems 1), @@ -60,23 +60,23 @@ (*** Image of a set under a function/relation ***) qed_goalw "Image_iff" Relation.thy [Image_def] - "b : r^^A = (? x:A. :r)" + "b : r^^A = (? x:A. (x,b):r)" (fn _ => [ fast_tac (comp_cs addIs [RangeI]) 1 ]); qed_goal "Image_singleton_iff" Relation.thy - "(b : r^^{a}) = (:r)" + "(b : r^^{a}) = ((a,b):r)" (fn _ => [ rtac (Image_iff RS trans) 1, fast_tac comp_cs 1 ]); qed_goalw "ImageI" Relation.thy [Image_def] - "!!a b r. [| : r; a:A |] ==> b : r^^A" + "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A" (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)), (resolve_tac [conjI ] 1), (resolve_tac [RangeI] 1), (REPEAT (fast_tac set_cs 1))]); qed_goalw "ImageE" Relation.thy [Image_def] - "[| b: r^^A; !!x.[| : r; x:A |] ==> P |] ==> P" + "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P" (fn major::prems=> [ (rtac (major RS CollectE) 1), (safe_tac set_cs), diff -r f4815812665b -r e61b058d58d2 src/HOL/Integ/Relation.thy --- a/src/HOL/Integ/Relation.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Integ/Relation.thy Fri Mar 24 12:30:35 1995 +0100 @@ -16,9 +16,9 @@ Range :: "('a*'a) set => 'a set" defs - converse_def "converse(r) == {z. (? w:r. ? x y. w= & z=)}" - Domain_def "Domain(r) == {z. ! x. (z=x --> (? y. :r))}" + converse_def "converse(r) == {z. (? w:r. ? x y. w=(x,y) & z=(y,x))}" + Domain_def "Domain(r) == {z. ! x. (z=x --> (? y. (x,y):r))}" Range_def "Range(r) == Domain(converse(r))" - Image_def "r ^^ s == {y. y:Range(r) & (? x:s. :r)}" + Image_def "r ^^ s == {y. y:Range(r) & (? x:s. (x,y):r)}" end diff -r f4815812665b -r e61b058d58d2 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Nat.ML Fri Mar 24 12:30:35 1995 +0100 @@ -136,12 +136,12 @@ (** Introduction rules for 'pred_nat' **) -goalw Nat.thy [pred_nat_def] " : pred_nat"; +goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat"; by (fast_tac set_cs 1); qed "pred_natI"; val major::prems = goalw Nat.thy [pred_nat_def] - "[| p : pred_nat; !!x n. [| p = |] ==> R \ + "[| p : pred_nat; !!x n. [| p = (n, Suc(n)) |] ==> R \ \ |] ==> R"; by (rtac (major RS CollectE) 1); by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1)); @@ -204,7 +204,7 @@ by (rtac (pred_natI RS r_into_trancl) 1); qed "lessI"; -(* i i i(Suc(j) *) val less_SucI = lessI RSN (2, less_trans); goal Nat.thy "0 < Suc(n)"; @@ -220,7 +220,7 @@ by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1); qed "less_not_sym"; -(* [| n R *) +(* [| n(m; m(n |] ==> R *) bind_thm ("less_asym", (less_not_sym RS notE)); goalw Nat.thy [less_def] "~ n<(n::nat)"; @@ -228,7 +228,7 @@ by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1); qed "less_not_refl"; -(* n R *) +(* n(n ==> R *) bind_thm ("less_anti_refl", (less_not_refl RS notE)); goal Nat.thy "!!m. n m ~= (n::nat)"; diff -r f4815812665b -r e61b058d58d2 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Nat.thy Fri Mar 24 12:30:35 1995 +0100 @@ -59,9 +59,9 @@ (*nat operations and recursion*) nat_case_def "nat_case a f n == @z. (n=0 --> z=a) \ \ & (!x. n=Suc(x) --> z=f(x))" - pred_nat_def "pred_nat == {p. ? n. p = }" + pred_nat_def "pred_nat == {p. ? n. p = (n, Suc(n))}" - less_def "m:trancl(pred_nat)" + less_def "m = ; [| a=a'; b=b' |] ==> R |] ==> R"; + "[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1); by (REPEAT (ares_tac (prems@[ProdI]) 1)); qed "Pair_inject"; -goal Prod.thy "( = ) = (a=a' & b=b')"; +goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')"; by (fast_tac (set_cs addIs [Pair_inject]) 1); qed "Pair_eq"; -goalw Prod.thy [fst_def] "fst() = a"; +goalw Prod.thy [fst_def] "fst((a,b)) = a"; by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1); qed "fst_conv"; -goalw Prod.thy [snd_def] "snd() = b"; +goalw Prod.thy [snd_def] "snd((a,b)) = b"; by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1); qed "snd_conv"; -goalw Prod.thy [Pair_def] "? x y. p = "; +goalw Prod.thy [Pair_def] "? x y. p = (x,y)"; by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); qed "PairE_lemma"; -val [prem] = goal Prod.thy "[| !!x y. p = ==> Q |] ==> Q"; +val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q"; by (rtac (PairE_lemma RS exE) 1); by (REPEAT (eresolve_tac [prem,exE] 1)); qed "PairE"; -goalw Prod.thy [split_def] "split c = c a b"; +goalw Prod.thy [split_def] "split c (a,b) = c a b"; by (sstac [fst_conv, snd_conv] 1); by (rtac refl 1); qed "split"; @@ -72,18 +72,18 @@ (fn [prem] => [rtac (prem RS arg_cong) 1]); (* Do not add as rewrite rule: invalidates some proofs in IMP *) -goal Prod.thy "p = "; +goal Prod.thy "p = (fst(p),snd(p))"; by (res_inst_tac [("p","p")] PairE 1); by (asm_simp_tac prod_ss 1); qed "surjective_pairing"; -goal Prod.thy "p = split (%x y.) p"; +goal Prod.thy "p = split (%x y.(x,y)) p"; by (res_inst_tac [("p","p")] PairE 1); by (asm_simp_tac prod_ss 1); qed "surjective_pairing2"; (*For use with split_tac and the simplifier*) -goal Prod.thy "R(split c p) = (! x y. p = --> R(c x y))"; +goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))"; by (stac surjective_pairing 1); by (stac split 1); by (fast_tac (HOL_cs addSEs [Pair_inject]) 1); @@ -94,31 +94,31 @@ (*These rules are for use with fast_tac. Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) -goal Prod.thy "!!a b c. c a b ==> split c "; +goal Prod.thy "!!a b c. c a b ==> split c (a,b)"; by (asm_simp_tac prod_ss 1); qed "splitI"; val prems = goalw Prod.thy [split_def] - "[| split c p; !!x y. [| p = ; c x y |] ==> Q |] ==> Q"; + "[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q"; by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); qed "splitE"; -goal Prod.thy "!!R a b. split R ==> R a b"; +goal Prod.thy "!!R a b. split R (a,b) ==> R a b"; by (etac (split RS iffD1) 1); qed "splitD"; -goal Prod.thy "!!a b c. z: c a b ==> z: split c "; +goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)"; by (asm_simp_tac prod_ss 1); qed "mem_splitI"; val prems = goalw Prod.thy [split_def] - "[| z: split c p; !!x y. [| p = ; z: c x y |] ==> Q |] ==> Q"; + "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"; by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); qed "mem_splitE"; (*** prod_fun -- action of the product functor upon functions ***) -goalw Prod.thy [prod_fun_def] "prod_fun f g = "; +goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; by (rtac split 1); qed "prod_fun"; @@ -135,14 +135,14 @@ by (asm_simp_tac (prod_ss addsimps [prod_fun]) 1); qed "prod_fun_ident"; -val prems = goal Prod.thy ":r ==> : (prod_fun f g)``r"; +val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r"; by (rtac image_eqI 1); by (rtac (prod_fun RS sym) 1); by (resolve_tac prems 1); qed "prod_fun_imageI"; val major::prems = goal Prod.thy - "[| c: (prod_fun f g)``r; !!x y. [| c=; :r |] ==> P \ + "[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \ \ |] ==> P"; by (rtac (major RS imageE) 1); by (res_inst_tac [("p","x")] PairE 1); @@ -154,31 +154,31 @@ (*** Disjoint union of a family of sets - Sigma ***) qed_goalw "SigmaI" Prod.thy [Sigma_def] - "[| a:A; b:B(a) |] ==> : Sigma A B" + "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); (*The general elimination rule*) qed_goalw "SigmaE" Prod.thy [Sigma_def] "[| c: Sigma A B; \ -\ !!x y.[| x:A; y:B(x); c= |] ==> P \ +\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \ \ |] ==> P" (fn major::prems=> [ (cut_facts_tac [major] 1), (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); -(** Elimination of :A*B -- introduces no eigenvariables **) -qed_goal "SigmaD1" Prod.thy " : Sigma A B ==> a : A" +(** Elimination of (a,b):A*B -- introduces no eigenvariables **) +qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A" (fn [major]=> [ (rtac (major RS SigmaE) 1), (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); -qed_goal "SigmaD2" Prod.thy " : Sigma A B ==> b : B(a)" +qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)" (fn [major]=> [ (rtac (major RS SigmaE) 1), (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); qed_goal "SigmaE2" Prod.thy - "[| : Sigma A B; \ + "[| (a,b) : Sigma A B; \ \ [| a:A; b:B(a) |] ==> P \ \ |] ==> P" (fn [major,minor]=> @@ -188,7 +188,7 @@ (*** Domain of a relation ***) -val prems = goalw Prod.thy [image_def] " : r ==> a : fst``r"; +val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r"; by (rtac CollectI 1); by (rtac bexI 1); by (rtac (fst_conv RS sym) 1); @@ -196,7 +196,7 @@ qed "fst_imageI"; val major::prems = goal Prod.thy - "[| a : fst``r; !!y.[| : r |] ==> P |] ==> P"; + "[| a : fst``r; !!y.[| (a,y) : r |] ==> P |] ==> P"; by (rtac (major RS imageE) 1); by (resolve_tac prems 1); by (etac ssubst 1); @@ -206,7 +206,7 @@ (*** Range of a relation ***) -val prems = goalw Prod.thy [image_def] " : r ==> b : snd``r"; +val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r"; by (rtac CollectI 1); by (rtac bexI 1); by (rtac (snd_conv RS sym) 1); @@ -214,7 +214,7 @@ qed "snd_imageI"; val major::prems = goal Prod.thy - "[| a : snd``r; !!y.[| : r |] ==> P |] ==> P"; + "[| a : snd``r; !!y.[| (y,a) : r |] ==> P |] ==> P"; by (rtac (major RS imageE) 1); by (resolve_tac prems 1); by (etac ssubst 1); @@ -225,7 +225,7 @@ (** Exhaustion rule for unit -- a degenerate form of induction **) goalw Prod.thy [Unity_def] - "u = Unity"; + "u = ()"; by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1); by (rtac (Rep_Unit_inverse RS sym) 1); qed "unit_eq"; diff -r f4815812665b -r e61b058d58d2 src/HOL/Prod.thy --- a/src/HOL/Prod.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Prod.thy Fri Mar 24 12:30:35 1995 +0100 @@ -35,20 +35,19 @@ Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" syntax - "@Tuple" :: "args => 'a * 'b" ("(1<_>)") + "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))") translations - "" == ">" - "" == "Pair x y" - "" => "x" + "(x, y, z)" == "(x, (y, z))" + "(x, y)" == "Pair x y" defs Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)" - fst_def "fst(p) == @a. ? b. p = " - snd_def "snd(p) == @b. ? a. p = " + fst_def "fst(p) == @a. ? b. p = (a, b)" + snd_def "snd(p) == @b. ? a. p = (a, b)" split_def "split c p == c (fst p) (snd p)" - prod_fun_def "prod_fun f g == split(%x y.)" - Sigma_def "Sigma A B == UN x:A. UN y:B(x). {}" + prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))" + Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" @@ -58,9 +57,9 @@ unit = "{p. p = True}" consts - Unity :: "unit" ("'(')") + "()" :: "unit" ("'(')") defs - Unity_def "Unity == Abs_Unit(True)" + Unity_def "() == Abs_Unit(True)" end diff -r f4815812665b -r e61b058d58d2 src/HOL/Sexp.ML --- a/src/HOL/Sexp.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Sexp.ML Fri Mar 24 12:30:35 1995 +0100 @@ -63,19 +63,19 @@ by (fast_tac sexp_cs 1); qed "pred_sexp_subset_Sigma"; -(* : pred_sexp^+ ==> a : sexp *) +(* (a,b) : pred_sexp^+ ==> a : sexp *) val trancl_pred_sexpD1 = pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1 and trancl_pred_sexpD2 = pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2; val prems = goalw Sexp.thy [pred_sexp_def] - "[| M: sexp; N: sexp |] ==> : pred_sexp"; + "[| M: sexp; N: sexp |] ==> (M, M$N) : pred_sexp"; by (fast_tac (set_cs addIs prems) 1); qed "pred_sexpI1"; val prems = goalw Sexp.thy [pred_sexp_def] - "[| M: sexp; N: sexp |] ==> : pred_sexp"; + "[| M: sexp; N: sexp |] ==> (N, M$N) : pred_sexp"; by (fast_tac (set_cs addIs prems) 1); qed "pred_sexpI2"; @@ -86,7 +86,7 @@ val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD) and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD); -(*Proves goals of the form :pred_sexp^+ provided M,N:sexp*) +(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*) val pred_sexp_simps = sexp.intrs @ [pred_sexp_t1, pred_sexp_t2, @@ -95,8 +95,8 @@ val major::prems = goalw Sexp.thy [pred_sexp_def] "[| p : pred_sexp; \ -\ !!M N. [| p = ; M: sexp; N: sexp |] ==> R; \ -\ !!M N. [| p = ; M: sexp; N: sexp |] ==> R \ +\ !!M N. [| p = (M, M$N); M: sexp; N: sexp |] ==> R; \ +\ !!M N. [| p = (N, M$N); M: sexp; N: sexp |] ==> R \ \ |] ==> R"; by (cut_facts_tac [major] 1); by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1)); diff -r f4815812665b -r e61b058d58d2 src/HOL/Sexp.thy --- a/src/HOL/Sexp.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Sexp.thy Fri Mar 24 12:30:35 1995 +0100 @@ -32,7 +32,7 @@ \ | (? N1 N2. M = N1 $ N2 & z=e N1 N2)" pred_sexp_def - "pred_sexp == UN M: sexp. UN N: sexp. {, }" + "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}" sexp_rec_def "sexp_rec M c d e == wfrec pred_sexp M \ diff -r f4815812665b -r e61b058d58d2 src/HOL/Subst/AList.ML --- a/src/HOL/Subst/AList.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Subst/AList.ML Fri Mar 24 12:30:35 1995 +0100 @@ -12,13 +12,13 @@ (fn _ => [simp_tac list_ss 1]) in map mk_thm ["alist_rec [] c d = c", - "alist_rec (#al) c d = d a b al (alist_rec al c d)", + "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)", "assoc v d [] = d", - "assoc v d (#al) = (if v=a then b else assoc v d al)"] end; + "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] end; val prems = goal AList.thy "[| P([]); \ -\ !!x y xs. P(xs) ==> P(#xs) |] ==> P(l)"; +\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"; by (list.induct_tac "l" 1); by (resolve_tac prems 1); by (rtac PairE 1); diff -r f4815812665b -r e61b058d58d2 src/HOL/Subst/Subst.ML --- a/src/HOL/Subst/Subst.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Subst/Subst.ML Fri Mar 24 12:30:35 1995 +0100 @@ -19,9 +19,9 @@ ["Const(c) <| al = Const(c)", "Comb t u <| al = Comb (t <| al) (u <| al)", "[] <> bl = bl", - "(#al) <> bl = # (al <> bl)", + "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)", "sdom([]) = {}", - "sdom(#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \ + "sdom((a,b)#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \ \ else (sdom al) Un {a})" ]; (* This rewrite isn't always desired *) @@ -42,10 +42,10 @@ by (ALLGOALS (asm_simp_tac subst_ss)); val subst_mono = store_thm("subst_mono", result() RS mp); -goal Subst.thy "~ (Var(v) <: t) --> t <| #s = t <| s"; +goal Subst.thy "~ (Var(v) <: t) --> t <| (v,t <| s)#s = t <| s"; by (imp_excluded_middle_tac "t = Var(v)" 1); by (res_inst_tac [("P", - "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| #s=x<|s")] + "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")] uterm_induct 2); by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst]))); by (fast_tac HOL_cs 1); @@ -59,13 +59,13 @@ by (ALLGOALS (fast_tac HOL_cs)); qed "agreement"; -goal Subst.thy "~ v: vars_of(t) --> t <| #s = t <| s"; +goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s"; by(simp_tac(subst_ss addsimps [agreement,Var_subst] setloop (split_tac [expand_if])) 1); val repl_invariance = store_thm("repl_invariance", result() RS mp); val asms = goal Subst.thy - "v : vars_of(t) --> w : vars_of(t <| #s)"; + "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"; by (uterm_ind_tac "t" 1); by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst]))); val Var_in_subst = store_thm("Var_in_subst", result() RS mp); @@ -113,7 +113,7 @@ by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1); qed "comp_assoc"; -goal Subst.thy "#s =s= s"; +goal Subst.thy "(w,Var(w) <| s)#s =s= s"; by (rtac (allI RS (subst_eq_iff RS iffD2)) 1); by (uterm_ind_tac "t" 1); by (REPEAT (etac rev_mp 3)); diff -r f4815812665b -r e61b058d58d2 src/HOL/Subst/Subst.thy --- a/src/HOL/Subst/Subst.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Subst/Subst.thy Fri Mar 24 12:30:35 1995 +0100 @@ -26,7 +26,7 @@ \ (%x.Const(x)) \ \ (%u v q r.Comb q r)" - comp_def "al <> bl == alist_rec al bl (%x y xs g.#g)" + comp_def "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)" sdom_def "sdom(al) == alist_rec al {} \ diff -r f4815812665b -r e61b058d58d2 src/HOL/Subst/Unifier.ML --- a/src/HOL/Subst/Unifier.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Subst/Unifier.ML Fri Mar 24 12:30:35 1995 +0100 @@ -25,7 +25,7 @@ goal Unifier.thy "~v : vars_of(t) --> ~v : vars_of(u) -->Unifier s t u --> \ -\ Unifier (#s) t u"; +\ Unifier ((v,r)#s) t u"; by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1); val Cons_Unifier = store_thm("Cons_Unifier", result() RS mp RS mp RS mp); @@ -49,7 +49,7 @@ qed "MGU_iff"; val [prem] = goal Unifier.thy - "~ Var(v) <: t ==> MGUnifier [] (Var v) t"; + "~ Var(v) <: t ==> MGUnifier [(v,t)] (Var v) t"; by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1); by (REPEAT_SOME (step_tac set_cs)); by (etac subst 1); @@ -85,7 +85,7 @@ by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1); qed "Idem_Nil"; -goal Unifier.thy "~ (Var(v) <: t) --> Idem([])"; +goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])"; by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff] setloop (split_tac [expand_if])) 1); by (fast_tac set_cs 1); @@ -114,8 +114,8 @@ val prems = goal Unifier.thy "x : sdom(s) --> ~x : srange(s) --> \ -\ ~vars_of(Var(x) <| s<> #s) = \ -\ vars_of(Var(x) <| #s)"; +\ ~vars_of(Var(x) <| s<> (x,Var(x))#s) = \ +\ vars_of(Var(x) <| (x,Var(x))#s)"; by (simp_tac (subst_ss addsimps [not_equal_iff]) 1); by (REPEAT (resolve_tac [impI,disjI2] 1)); by(res_inst_tac [("x","x")] exI 1); @@ -141,8 +141,8 @@ val prems = goal Unifier.thy "~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \ -\ ~vars_of(Var(w) <| s<> #s) = \ -\ vars_of(Var(w) <| #s)"; +\ ~vars_of(Var(w) <| s<> (x,Var(w))#s) = \ +\ vars_of(Var(w) <| (x,Var(w))#s)"; by (simp_tac (subst_ss addsimps [not_equal_iff]) 1); by (REPEAT (resolve_tac [impI,disjI1] 1)); by(res_inst_tac [("x","w")] exI 1); @@ -167,10 +167,10 @@ (* *) (* fun unify Const(m) Const(n) = if m=n then Nil else Fail *) (* | unify Const(m) _ = Fail *) -(* | unify Var(v) t = if Var(v)<:t then Fail else #Nil *) +(* | unify Var(v) t = if Var(v)<:t then Fail else (v,t)#Nil *) (* | unify Comb(t,u) Const(n) = Fail *) (* | unify Comb(t,u) Var(v) = if Var(v) <: Comb(t,u) then Fail *) -(* else #Nil *) +(* else (v,Comb(t,u)#Nil *) (* | unify Comb(t,u) Comb(v,w) = let s = unify t v *) (* in if s=Fail then Fail *) (* else unify (u<|s) (w<|s); *) @@ -191,7 +191,7 @@ val Unify2 = store_thm("Unify2", result() RS mp); val [prem] = goalw Unifier.thy [MGIUnifier_def] - "~Var(v) <: t ==> MGIUnifier [] (Var v) t"; + "~Var(v) <: t ==> MGIUnifier [(v,t)] (Var v) t"; by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1); qed "Unify3"; diff -r f4815812665b -r e61b058d58d2 src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Trancl.ML Fri Mar 24 12:30:35 1995 +0100 @@ -11,55 +11,55 @@ (** Natural deduction for trans(r) **) val prems = goalw Trancl.thy [trans_def] - "(!! x y z. [| :r; :r |] ==> :r) ==> trans(r)"; + "(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)"; by (REPEAT (ares_tac (prems@[allI,impI]) 1)); qed "transI"; val major::prems = goalw Trancl.thy [trans_def] - "[| trans(r); :r; :r |] ==> :r"; + "[| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r"; by (cut_facts_tac [major] 1); by (fast_tac (HOL_cs addIs prems) 1); qed "transD"; (** Identity relation **) -goalw Trancl.thy [id_def] " : id"; +goalw Trancl.thy [id_def] "(a,a) : id"; by (rtac CollectI 1); by (rtac exI 1); by (rtac refl 1); qed "idI"; val major::prems = goalw Trancl.thy [id_def] - "[| p: id; !!x.[| p = |] ==> P \ + "[| p: id; !!x.[| p = (x,x) |] ==> P \ \ |] ==> P"; by (rtac (major RS CollectE) 1); by (etac exE 1); by (eresolve_tac prems 1); qed "idE"; -goalw Trancl.thy [id_def] ":id = (a=b)"; +goalw Trancl.thy [id_def] "(a,b):id = (a=b)"; by(fast_tac prod_cs 1); qed "pair_in_id_conv"; (** Composition of two relations **) val prems = goalw Trancl.thy [comp_def] - "[| :s; :r |] ==> : r O s"; + "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s"; by (fast_tac (set_cs addIs prems) 1); qed "compI"; (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) val prems = goalw Trancl.thy [comp_def] "[| xz : r O s; \ -\ !!x y z. [| xz = ; :s; :r |] ==> P \ +\ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \ \ |] ==> P"; by (cut_facts_tac prems 1); by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1)); qed "compE"; val prems = goal Trancl.thy - "[| : r O s; \ -\ !!y. [| :s; :r |] ==> P \ + "[| (a,c) : r O s; \ +\ !!y. [| (a,y):s; (y,c):r |] ==> P \ \ |] ==> P"; by (rtac compE 1); by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1)); @@ -88,20 +88,20 @@ val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski); (*Reflexivity of rtrancl*) -goal Trancl.thy " : r^*"; +goal Trancl.thy "(a,a) : r^*"; by (stac rtrancl_unfold 1); by (fast_tac comp_cs 1); qed "rtrancl_refl"; (*Closure under composition with r*) val prems = goal Trancl.thy - "[| : r^*; : r |] ==> : r^*"; + "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*"; by (stac rtrancl_unfold 1); by (fast_tac (comp_cs addIs prems) 1); qed "rtrancl_into_rtrancl"; (*rtrancl of r contains r*) -val [prem] = goal Trancl.thy "[| : r |] ==> : r^*"; +val [prem] = goal Trancl.thy "[| (a,b) : r |] ==> (a,b) : r^*"; by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1); by (rtac prem 1); qed "r_into_rtrancl"; @@ -114,22 +114,22 @@ (** standard induction rule **) val major::prems = goal Trancl.thy - "[| : r^*; \ -\ !!x. P(); \ -\ !!x y z.[| P(); : r^*; : r |] ==> P() |] \ -\ ==> P()"; + "[| (a,b) : r^*; \ +\ !!x. P((x,x)); \ +\ !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |] ==> P((x,z)) |] \ +\ ==> P((a,b))"; by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1); by (fast_tac (comp_cs addIs prems) 1); qed "rtrancl_full_induct"; (*nice induction rule*) val major::prems = goal Trancl.thy - "[| : r^*; \ + "[| (a::'a,b) : r^*; \ \ P(a); \ -\ !!y z.[| : r^*; : r; P(y) |] ==> P(z) |] \ +\ !!y z.[| (a,y) : r^*; (y,z) : r; P(y) |] ==> P(z) |] \ \ ==> P(b)"; (*by induction on this formula*) -by (subgoal_tac "! y. = --> P(y)" 1); +by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1); (*now solve first subgoal: this formula is sufficient*) by (fast_tac HOL_cs 1); (*now do the induction*) @@ -147,10 +147,10 @@ (*elimination of rtrancl -- by induction on a special formula*) val major::prems = goal Trancl.thy - "[| : r^*; (a = b) ==> P; \ -\ !!y.[| : r^*; : r |] ==> P \ + "[| (a::'a,b) : r^*; (a = b) ==> P; \ +\ !!y.[| (a,y) : r^*; (y,b) : r |] ==> P \ \ |] ==> P"; -by (subgoal_tac "(a::'a) = b | (? y. : r^* & : r)" 1); +by (subgoal_tac "(a::'a) = b | (? y. (a,y) : r^* & (y,b) : r)" 1); by (rtac (major RS rtrancl_induct) 2); by (fast_tac (set_cs addIs prems) 2); by (fast_tac (set_cs addIs prems) 2); @@ -163,26 +163,26 @@ (** Conversions between trancl and rtrancl **) val [major] = goalw Trancl.thy [trancl_def] - " : r^+ ==> : r^*"; + "(a,b) : r^+ ==> (a,b) : r^*"; by (resolve_tac [major RS compEpair] 1); by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1)); qed "trancl_into_rtrancl"; (*r^+ contains r*) val [prem] = goalw Trancl.thy [trancl_def] - "[| : r |] ==> : r^+"; + "[| (a,b) : r |] ==> (a,b) : r^+"; by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1)); qed "r_into_trancl"; (*intro rule by definition: from rtrancl and r*) val prems = goalw Trancl.thy [trancl_def] - "[| : r^*; : r |] ==> : r^+"; + "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^+"; by (REPEAT (resolve_tac ([compI]@prems) 1)); qed "rtrancl_into_trancl1"; (*intro rule from r and rtrancl*) val prems = goal Trancl.thy - "[| : r; : r^* |] ==> : r^+"; + "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+"; by (resolve_tac (prems RL [rtranclE]) 1); by (etac subst 1); by (resolve_tac (prems RL [r_into_trancl]) 1); @@ -192,11 +192,11 @@ (*elimination of r^+ -- NOT an induction rule*) val major::prems = goal Trancl.thy - "[| : r^+; \ -\ : r ==> P; \ -\ !!y.[| : r^+; : r |] ==> P \ + "[| (a::'a,b) : r^+; \ +\ (a,b) : r ==> P; \ +\ !!y.[| (a,y) : r^+; (y,b) : r |] ==> P \ \ |] ==> P"; -by (subgoal_tac " : r | (? y. : r^+ & : r)" 1); +by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+ & (y,b) : r)" 1); by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1)); by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); by (etac rtranclE 1); @@ -214,7 +214,7 @@ qed "trans_trancl"; val prems = goal Trancl.thy - "[| : r; : r^+ |] ==> : r^+"; + "[| (a,b) : r; (b,c) : r^+ |] ==> (a,c) : r^+"; by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1); by (resolve_tac prems 1); by (resolve_tac prems 1); @@ -222,7 +222,7 @@ val major::prems = goal Trancl.thy - "[| : r^*; r <= Sigma A (%x.A) |] ==> a=b | a:A"; + "[| (a,b) : r^*; r <= Sigma A (%x.A) |] ==> a=b | a:A"; by (cut_facts_tac prems 1); by (rtac (major RS rtrancl_induct) 1); by (rtac (refl RS disjI1) 1); diff -r f4815812665b -r e61b058d58d2 src/HOL/Trancl.thy --- a/src/HOL/Trancl.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Trancl.thy Fri Mar 24 12:30:35 1995 +0100 @@ -16,11 +16,11 @@ trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100) O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60) defs -trans_def "trans(r) == (!x y z. :r --> :r --> :r)" +trans_def "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)" comp_def (*composition of relations*) - "r O s == {xz. ? x y z. xz = & :s & :r}" + "r O s == {xz. ? x y z. xz = (x,z) & (x,y):s & (y,z):r}" id_def (*the identity relation*) - "id == {p. ? x. p = }" + "id == {p. ? x. p = (x,x)}" rtrancl_def "r^* == lfp(%s. id Un (r O s))" trancl_def "r^+ == r O rtrancl(r)" end diff -r f4815812665b -r e61b058d58d2 src/HOL/Univ.ML --- a/src/HOL/Univ.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Univ.ML Fri Mar 24 12:30:35 1995 +0100 @@ -51,12 +51,12 @@ (** apfst -- can be used in similar type definitions **) -goalw Univ.thy [apfst_def] "apfst f = "; +goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)"; by (rtac split 1); qed "apfst"; val [major,minor] = goal Univ.thy - "[| q = apfst f p; !!x y. [| p = ; q = |] ==> R \ + "[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R \ \ |] ==> R"; by (rtac PairE 1); by (rtac minor 1); @@ -109,7 +109,7 @@ (*** Introduction rules for Node ***) -goalw Univ.thy [Node_def] "<%k. 0,a> : Node"; +goalw Univ.thy [Node_def] "(%k. 0,a) : Node"; by (fast_tac set_cs 1); qed "Node_K0_I"; @@ -256,7 +256,7 @@ val univ_ss = nat_ss addsimps univ_simps; -goalw Univ.thy [ndepth_def] "ndepth (Abs_Node(<%k.0, x>)) = 0"; +goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0"; by (sstac [Node_K0_I RS Abs_Node_inverse, split] 1); by (rtac Least_equality 1); by (rtac refl 1); @@ -496,7 +496,7 @@ (*** Equality : the diagonal relation ***) -goalw Univ.thy [diag_def] "!!a A. [| a=b; a:A |] ==> : diag(A)"; +goalw Univ.thy [diag_def] "!!a A. [| a=b; a:A |] ==> (a,b) : diag(A)"; by (fast_tac set_cs 1); qed "diag_eqI"; @@ -505,7 +505,7 @@ (*The general elimination rule*) val major::prems = goalw Univ.thy [diag_def] "[| c : diag(A); \ -\ !!x y. [| x:A; c = |] ==> P \ +\ !!x y. [| x:A; c = (x,x) |] ==> P \ \ |] ==> P"; by (rtac (major RS UN_E) 1); by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1)); @@ -514,14 +514,14 @@ (*** Equality for Cartesian Product ***) goalw Univ.thy [dprod_def] - "!!r s. [| :r; :s |] ==> : r<**>s"; + "!!r s. [| (M,M'):r; (N,N'):s |] ==> (M$N, M'$N') : r<**>s"; by (fast_tac prod_cs 1); qed "dprodI"; (*The general elimination rule*) val major::prems = goalw Univ.thy [dprod_def] "[| c : r<**>s; \ -\ !!x y x' y'. [| : r; : s; c = |] ==> P \ +\ !!x y x' y'. [| (x,x') : r; (y,y') : s; c = (x$y,x'$y') |] ==> P \ \ |] ==> P"; by (cut_facts_tac [major] 1); by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE])); @@ -531,18 +531,18 @@ (*** Equality for Disjoint Sum ***) -goalw Univ.thy [dsum_def] "!!r. :r ==> : r<++>s"; +goalw Univ.thy [dsum_def] "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s"; by (fast_tac prod_cs 1); qed "dsum_In0I"; -goalw Univ.thy [dsum_def] "!!r. :s ==> : r<++>s"; +goalw Univ.thy [dsum_def] "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s"; by (fast_tac prod_cs 1); qed "dsum_In1I"; val major::prems = goalw Univ.thy [dsum_def] "[| w : r<++>s; \ -\ !!x x'. [| : r; w = |] ==> P; \ -\ !!y y'. [| : s; w = |] ==> P \ +\ !!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; \ +\ !!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P \ \ |] ==> P"; by (cut_facts_tac [major] 1); by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE])); diff -r f4815812665b -r e61b058d58d2 src/HOL/Univ.thy --- a/src/HOL/Univ.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Univ.thy Fri Mar 24 12:30:35 1995 +0100 @@ -16,7 +16,7 @@ (** lists, trees will be sets of nodes **) subtype (Node) - 'a node = "{p. EX f x k. p = nat, x::'a+nat> & f(k)=0}" + 'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}" types 'a item = "'a node set" @@ -58,13 +58,13 @@ Push_Node_def "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" (*crude "lists" of nats -- needed for the constructions*) - apfst_def "apfst == (%f. split(%x y. ))" + apfst_def "apfst == (%f. split(%x y. (f(x),y)))" Push_def "Push == (%b h. nat_case (Suc b) h)" (** operations on S-expressions -- sets of nodes **) (*S-expression constructors*) - Atom_def "Atom == (%x. {Abs_Node(<%k.0, x>)})" + Atom_def "Atom == (%x. {Abs_Node((%k.0, x))})" Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)" (*Leaf nodes, with arbitrary or nat labels*) @@ -92,12 +92,12 @@ (** diagonal sets and equality for the "universe" **) - diag_def "diag(A) == UN x:A. {}" + diag_def "diag(A) == UN x:A. {(x,x)}" dprod_def "r<**>s == UN u:r. split (%x x'. \ -\ UN v:s. split (%y y'. {}) v) u" +\ UN v:s. split (%y y'. {(x$y,x'$y')}) v) u" - dsum_def "r<++>s == (UN u:r. split (%x x'. {}) u) Un \ -\ (UN v:s. split (%y y'. {}) v)" + dsum_def "r<++>s == (UN u:r. split (%x x'. {(In0(x),In0(x'))}) u) Un \ +\ (UN v:s. split (%y y'. {(In1(y),In1(y'))}) v)" end diff -r f4815812665b -r e61b058d58d2 src/HOL/WF.ML --- a/src/HOL/WF.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/WF.ML Fri Mar 24 12:30:35 1995 +0100 @@ -14,7 +14,7 @@ (*Restriction to domain A. If r is well-founded over A then wf(r)*) val [prem1,prem2] = goalw WF.thy [wf_def] "[| r <= Sigma A (%u.A); \ -\ !!x P. [| ! x. (! y. : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ +\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ \ ==> wf(r)"; by (strip_tac 1); by (rtac allE 1); @@ -24,7 +24,7 @@ val major::prems = goalw WF.thy [wf_def] "[| wf(r); \ -\ !!x.[| ! y. : r --> P(y) |] ==> P(x) \ +\ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \ \ |] ==> P(a)"; by (rtac (major RS spec RS mp RS spec) 1); by (fast_tac (HOL_cs addEs prems) 1); @@ -36,14 +36,14 @@ rename_last_tac a ["1"] (i+1), ares_tac prems i]; -val prems = goal WF.thy "[| wf(r); :r; :r |] ==> P"; -by (subgoal_tac "! x. :r --> :r --> P" 1); +val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P"; +by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1); by (fast_tac (HOL_cs addIs prems) 1); by (wf_ind_tac "a" prems 1); by (fast_tac set_cs 1); qed "wf_asym"; -val prems = goal WF.thy "[| wf(r); : r |] ==> P"; +val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P"; by (rtac wf_asym 1); by (REPEAT (resolve_tac prems 1)); qed "wf_anti_refl"; @@ -68,12 +68,12 @@ (*This rewrite rule works upon formulae; thus it requires explicit use of H_cong to expose the equality*) goalw WF.thy [cut_def] - "(cut f r x = cut g r x) = (!y. :r --> f(y)=g(y))"; + "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))"; by(simp_tac (HOL_ss addsimps [expand_fun_eq] setloop (split_tac [expand_if])) 1); qed "cut_cut_eq"; -goalw WF.thy [cut_def] "!!x. :r ==> (cut f r a)(x) = f(x)"; +goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)"; by(asm_simp_tac HOL_ss 1); qed "cut_apply"; @@ -81,12 +81,12 @@ (*** is_recfun ***) goalw WF.thy [is_recfun_def,cut_def] - "!!f. [| is_recfun r a H f; ~:r |] ==> f(b) = (@z.True)"; + "!!f. [| is_recfun r a H f; ~(b,a):r |] ==> f(b) = (@z.True)"; by (etac ssubst 1); by(asm_simp_tac HOL_ss 1); qed "is_recfun_undef"; -(*eresolve_tac transD solves :r using transitivity AT MOST ONCE +(*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE mp amd allE instantiate induction hypotheses*) fun indhyp_tac hyps = ares_tac (TrueI::hyps) ORELSE' @@ -104,7 +104,7 @@ val prems = goalw WF.thy [is_recfun_def,cut_def] "[| wf(r); trans(r); is_recfun r a H f; is_recfun r b H g |] ==> \ - \ :r --> :r --> f(x)=g(x)"; + \ (x,a):r --> (x,b):r --> f(x)=g(x)"; by (cut_facts_tac prems 1); by (etac wf_induct 1); by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); @@ -115,7 +115,7 @@ val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def] "[| wf(r); trans(r); \ -\ is_recfun r a H f; is_recfun r b H g; :r |] ==> \ +\ is_recfun r a H f; is_recfun r b H g; (b,a):r |] ==> \ \ cut f r b = g"; val gundef = recgb RS is_recfun_undef and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); @@ -150,13 +150,13 @@ (*Beware incompleteness of unification!*) val prems = goal WF.thy - "[| wf(r); trans(r); :r; :r |] \ + "[| wf(r); trans(r); (c,a):r; (c,b):r |] \ \ ==> the_recfun r a H c = the_recfun r b H c"; by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1)); qed "the_recfun_equal"; val prems = goal WF.thy - "[| wf(r); trans(r); :r |] \ + "[| wf(r); trans(r); (b,a):r |] \ \ ==> cut (the_recfun r a H) r b = the_recfun r b H"; by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1)); qed "the_recfun_cut"; diff -r f4815812665b -r e61b058d58d2 src/HOL/WF.thy --- a/src/HOL/WF.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/WF.thy Fri Mar 24 12:30:35 1995 +0100 @@ -15,9 +15,9 @@ the_recfun :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b" defs - wf_def "wf(r) == (!P. (!x. (!y. :r --> P(y)) --> P(x)) --> (!x.P(x)))" + wf_def "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))" - cut_def "cut f r x == (%y. if :r then f y else @z.True)" + cut_def "cut f r x == (%y. if (y,x):r then f y else @z.True)" is_recfun_def "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)" diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/Acc.ML --- a/src/HOL/ex/Acc.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/Acc.ML Fri Mar 24 12:30:35 1995 +0100 @@ -13,12 +13,12 @@ (*The intended introduction rule*) val prems = goal Acc.thy - "[| !!b. :r ==> b: acc(r) |] ==> a: acc(r)"; + "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)"; by (fast_tac (set_cs addIs (prems @ map (rewrite_rule [pred_def]) acc.intrs)) 1); qed "accI"; -goal Acc.thy "!!a b r. [| b: acc(r); : r |] ==> a: acc(r)"; +goal Acc.thy "!!a b r. [| b: acc(r); (a,b): r |] ==> a: acc(r)"; by (etac acc.elim 1); by (rewtac pred_def); by (fast_tac set_cs 1); @@ -26,7 +26,7 @@ val [major,indhyp] = goal Acc.thy "[| a : acc(r); \ -\ !!x. [| x: acc(r); ALL y. :r --> P(y) |] ==> P(x) \ +\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ \ |] ==> P(a)"; by (rtac (major RS acc.induct) 1); by (rtac indhyp 1); @@ -44,7 +44,7 @@ by (fast_tac set_cs 1); qed "acc_wfI"; -val [major] = goal Acc.thy "wf(r) ==> ALL x. : r | :r --> y: acc(r)"; +val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)"; by (rtac (major RS wf_induct) 1); br (impI RS allI) 1; br accI 1; diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/Acc.thy --- a/src/HOL/ex/Acc.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/Acc.thy Fri Mar 24 12:30:35 1995 +0100 @@ -16,7 +16,7 @@ acc :: "('a * 'a)set => 'a set" (*Accessible part*) defs - pred_def "pred x r == {y. :r}" + pred_def "pred x r == {y. (y,x):r}" inductive "acc(r)" intrs diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/LList.ML --- a/src/HOL/ex/LList.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/LList.ML Fri Mar 24 12:30:35 1995 +0100 @@ -135,7 +135,7 @@ (*Lemma for the proof of llist_corec*) goal LList.thy - "LList_corec a (%z.sum_case Inl (split(%v w.Inr())) (f z)) : \ + "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \ \ llist(range(Leaf))"; by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1); by (rtac rangeI 1); @@ -156,7 +156,7 @@ end; qed "LListD_unfold"; -goal LList.thy "!M N. : LListD(diag(A)) --> ntrunc k M = ntrunc k N"; +goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N"; by (res_inst_tac [("n", "k")] less_induct 1); by (safe_tac set_cs); by (etac LListD.elim 1); @@ -202,12 +202,12 @@ ba 1; qed "LListD_coinduct"; -goalw LList.thy [LListD_Fun_def,NIL_def] " : LListD_Fun r s"; +goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s"; by (fast_tac set_cs 1); qed "LListD_Fun_NIL_I"; goalw LList.thy [LListD_Fun_def,CONS_def] - "!!x. [| x:A; :s |] ==> : LListD_Fun (diag A) s"; + "!!x. [| x:A; (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s"; by (fast_tac univ_cs 1); qed "LListD_Fun_CONS_I"; @@ -237,7 +237,7 @@ qed "LListD_eq_diag"; goal LList.thy - "!!M N. M: llist(A) ==> : LListD_Fun (diag A) (X Un diag(llist(A)))"; + "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))"; by (rtac (LListD_eq_diag RS subst) 1); br LListD_Fun_LListD_I 1; by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag, diagI]) 1); @@ -248,7 +248,7 @@ [also admits true equality] Replace "A" by some particular set, like {x.True}??? *) goal LList.thy - "!!r. [| : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \ + "!!r. [| (M,N) : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \ \ |] ==> M=N"; by (rtac (LListD_subset_diag RS subsetD RS diagE) 1); by (etac LListD_coinduct 1); @@ -267,7 +267,7 @@ by (rtac ext 1); (*next step avoids an unknown (and flexflex pair) in simplification*) by (res_inst_tac [("A", "{u.True}"), - ("r", "range(%u. )")] LList_equalityI 1); + ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1); by (rtac rangeI 1); by (safe_tac set_cs); by (stac prem1 1); @@ -332,14 +332,14 @@ by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1)); qed "Lconst_type"; -goal LList.thy "Lconst(M) = LList_corec M (%x.Inr())"; +goal LList.thy "Lconst(M) = LList_corec M (%x.Inr((x,x)))"; by (rtac (equals_LList_corec RS fun_cong) 1); by (simp_tac sum_ss 1); by (rtac Lconst 1); qed "Lconst_eq_LList_corec"; (*Thus we could have used gfp in the definition of Lconst*) -goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr())"; +goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))"; by (rtac (equals_LList_corec RS fun_cong) 1); by (simp_tac sum_ss 1); by (rtac (Lconst_fun_mono RS gfp_Tarski) 1); @@ -420,8 +420,8 @@ "[| M: llist(A); g(NIL): llist(A); \ \ f(NIL)=g(NIL); \ \ !!x l. [| x:A; l: llist(A) |] ==> \ -\ : \ -\ LListD_Fun (diag A) ((%u.)``llist(A) Un \ +\ (f(CONS x l),g(CONS x l)) : \ +\ LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un \ \ diag(llist(A))) \ \ |] ==> f(M) = g(M)"; by (rtac LList_equalityI 1); @@ -637,7 +637,7 @@ qed "prod_fun_lemma"; goal LList.thy - "prod_fun Rep_llist Rep_llist `` range(%x. ) = \ + "prod_fun Rep_llist Rep_llist `` range(%x. (x, x)) = \ \ diag(llist(range(Leaf)))"; br equalityI 1; by (fast_tac (univ_cs addIs [Rep_llist]) 1); @@ -647,7 +647,7 @@ (** To show two llists are equal, exhibit a bisimulation! [also admits true equality] **) val [prem1,prem2] = goalw LList.thy [llistD_Fun_def] - "[| : r; r <= llistD_Fun(r Un range(%x.)) |] ==> l1=l2"; + "[| (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2"; by (rtac (inj_Rep_llist RS injD) 1); by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"), ("A", "range(Leaf)")] @@ -664,19 +664,19 @@ qed "llist_equalityI"; (** Rules to prove the 2nd premise of llist_equalityI **) -goalw LList.thy [llistD_Fun_def,LNil_def] " : llistD_Fun(r)"; +goalw LList.thy [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)"; by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1); qed "llistD_Fun_LNil_I"; val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def] - ":r ==> : llistD_Fun(r)"; + "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)"; by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1); by (rtac (prem RS prod_fun_imageI) 1); qed "llistD_Fun_LCons_I"; (*Utilise the "strong" part, i.e. gfp(f)*) goalw LList.thy [llistD_Fun_def] - "!!l. : llistD_Fun(r Un range(%x.))"; + "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))"; br (Rep_llist_inverse RS subst) 1; br prod_fun_imageI 1; by (rtac (image_Un RS ssubst) 1); @@ -687,10 +687,10 @@ (*A special case of list_equality for functions over lazy lists*) val [prem1,prem2] = goal LList.thy "[| f(LNil)=g(LNil); \ -\ !!x l. : \ -\ llistD_Fun(range(%u. ) Un range(%v. )) \ +\ !!x l. (f(LCons x l),g(LCons x l)) : \ +\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \ \ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"; -by (res_inst_tac [("r", "range(%u. )")] llist_equalityI 1); +by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1); by (rtac rangeI 1); by (rtac subsetI 1); by (etac rangeE 1); @@ -744,7 +744,7 @@ qed "iterates"; goal LList.thy "lmap f (iterates f x) = iterates f (f x)"; -by (res_inst_tac [("r", "range(%u.)")] +by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] llist_equalityI 1); by (rtac rangeI 1); by (safe_tac set_cs); @@ -777,14 +777,14 @@ val Pair_cong = read_instantiate_sg (sign_of Prod.thy) [("f","Pair")] (standard(refl RS cong RS cong)); -(*The bisimulation consists of {} +(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))} for all u and all n::nat.*) val [prem] = goal LList.thy "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"; br ext 1; by (res_inst_tac [("r", - "UN u. range(%n. )")] + "UN u. range(%n. (nat_rec n (h u) (%m y.lmap f y), \ +\ nat_rec n (iterates f u) (%m y.lmap f y)))")] llist_equalityI 1); by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1)); by (safe_tac set_cs); @@ -834,7 +834,7 @@ (*The infinite first argument blocks the second*) goal LList.thy "lappend (iterates f x) N = iterates f x"; -by (res_inst_tac [("r", "range(%u.)")] +by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] llist_equalityI 1); by (rtac rangeI 1); by (safe_tac set_cs); @@ -848,7 +848,7 @@ goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"; by (res_inst_tac [("r", - "UN n. range(%l.)")] + "UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")] llist_equalityI 1); by (rtac UN1_I 1); by (rtac rangeI 1); diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/LList.thy --- a/src/HOL/ex/LList.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/LList.thy Fri Mar 24 12:30:35 1995 +0100 @@ -19,8 +19,8 @@ Previous definition of llistD_Fun was explicit: llistD_Fun_def "llistD_Fun(r) == \ -\ {} Un \ -\ (UN x. (split(%l1 l2.))``r)" +\ {(LNil,LNil)} Un \ +\ (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)" *) LList = Gfp + SList + @@ -69,9 +69,9 @@ coinductive "LListD(r)" intrs - NIL_I " : LListD(r)" - CONS_I "[| : r; : LListD(r) \ -\ |] ==> : LListD(r)" + NIL_I "(NIL, NIL) : LListD(r)" + CONS_I "[| (a,b): r; (M,N) : LListD(r) \ +\ |] ==> (CONS a M, CONS b N) : LListD(r)" defs (*Now used exclusively for abbreviating the coinduction rule*) @@ -79,9 +79,9 @@ \ {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}" LListD_Fun_def "LListD_Fun r X == \ -\ {z. z = | \ -\ (? M N a b. z = & \ -\ : r & : X)}" +\ {z. z = (NIL, NIL) | \ +\ (? M N a b. z = (CONS a M, CONS b N) & \ +\ (a, b) : r & (M, N) : X)}" (*defining the abstract constructors*) LNil_def "LNil == Abs_llist(NIL)" @@ -102,7 +102,7 @@ llist_corec_def "llist_corec a f == \ \ Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \ -\ (split(%v w. Inr())) (f z)))" +\ (split(%v w. Inr((Leaf(v), w)))) (f z)))" llistD_Fun_def "llistD_Fun(r) == \ @@ -113,28 +113,28 @@ Lconst_def "Lconst(M) == lfp(%N. CONS M N)" Lmap_def - "Lmap f M == LList_corec M (List_case (Inl Unity) (%x M'. Inr()))" + "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))" lmap_def - "lmap f l == llist_corec l (llist_case (Inl Unity) (%y z. Inr()))" + "lmap f l == llist_corec l (llist_case (Inl ()) (%y z. Inr((f(y), z))))" - iterates_def "iterates f a == llist_corec a (%x. Inr())" + iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))" (*Append generates its result by applying f, where - f() = Inl(Unity) - f() = Inr() - f() = Inr() + f((NIL,NIL)) = Inl(()) + f((NIL, CONS N1 N2)) = Inr((N1, (NIL,N2)) + f((CONS M1 M2, N)) = Inr((M1, (M2,N)) *) Lappend_def - "Lappend M N == LList_corec \ -\ (split(List_case (List_case (Inl Unity) (%N1 N2. Inr(>))) \ -\ (%M1 M2 N. Inr(>))))" + "Lappend M N == LList_corec (M,N) \ +\ (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) \ +\ (%M1 M2 N. Inr((M1, (M2,N))))))" lappend_def - "lappend l n == llist_corec \ -\ (split(llist_case (llist_case (Inl Unity) (%n1 n2. Inr(>))) \ -\ (%l1 l2 n. Inr(>))))" + "lappend l n == llist_corec (l,n) \ +\ (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) \ +\ (%l1 l2 n. Inr((l1, (l2,n))))))" rules (*faking a type definition...*) diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/LexProd.ML --- a/src/HOL/ex/LexProd.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/LexProd.ML Fri Mar 24 12:30:35 1995 +0100 @@ -7,7 +7,7 @@ The lexicographic product of two wellfounded relations is again wellfounded. *) -val prems = goal Prod.thy "!a b. P() ==> !p.P(p)"; +val prems = goal Prod.thy "!a b. P((a,b)) ==> !p.P(p)"; by (cut_facts_tac prems 1); by (rtac allI 1); by (rtac (surjective_pairing RS ssubst) 1); diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/LexProd.thy --- a/src/HOL/ex/LexProd.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/LexProd.thy Fri Mar 24 12:30:35 1995 +0100 @@ -10,6 +10,6 @@ consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70) rules lex_prod_def "ra**rb == {p. ? a a' b b'. \ -\ p = <,> & ( : ra | a=a' & : rb)}" +\ p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}" end diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/MT.ML --- a/src/HOL/ex/MT.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/MT.ML Fri Mar 24 12:30:35 1995 +0100 @@ -45,13 +45,13 @@ (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1) ); -val prems = goal MT.thy "P a b ==> P (fst ) (snd )"; +val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))"; by (rtac (fst_conv RS ssubst) 1); by (rtac (snd_conv RS ssubst) 1); by (resolve_tac prems 1); qed "infsys_p1"; -val prems = goal MT.thy "P (fst ) (snd ) ==> P a b"; +val prems = goal MT.thy "P (fst (a,b)) (snd (a,b)) ==> P a b"; by (cut_facts_tac prems 1); by (dtac (fst_conv RS subst) 1); by (dtac (snd_conv RS subst) 1); @@ -59,7 +59,7 @@ qed "infsys_p2"; val prems = goal MT.thy - "P a b c ==> P (fst(fst <,c>)) (snd(fst <,c>)) (snd <,c>)"; + "P a b c ==> P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))"; by (rtac (fst_conv RS ssubst) 1); by (rtac (fst_conv RS ssubst) 1); by (rtac (snd_conv RS ssubst) 1); @@ -68,7 +68,7 @@ qed "infsys_pp1"; val prems = goal MT.thy - "P (fst(fst <,c>)) (snd(fst <,c>)) (snd <,c>) ==> P a b c"; + "P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c)) ==> P a b c"; by (cut_facts_tac prems 1); by (dtac (fst_conv RS subst) 1); by (dtac (fst_conv RS subst) 1); @@ -240,23 +240,23 @@ val prems = goalw MT.thy [eval_def, eval_rel_def] " [| ve |- e ---> v; \ -\ !!ve c. P(<,v_const(c)>); \ -\ !!ev ve. ev:ve_dom(ve) ==> P(<,ve_app ve ev>); \ -\ !!ev ve e. P(< e>,v_clos(<|ev,e,ve|>)>); \ +\ !!ve c. P(((ve,e_const(c)),v_const(c))); \ +\ !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \ +\ !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \ \ !!ev1 ev2 ve cl e. \ \ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \ -\ P(<,v_clos(cl)>); \ +\ P(((ve,fix ev2(ev1) = e),v_clos(cl))); \ \ !!ve c1 c2 e1 e2. \ -\ [| P(<,v_const(c1)>); P(<,v_const(c2)>) |] ==> \ -\ P(<,v_const(c_app c1 c2)>); \ +\ [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \ +\ P(((ve,e1 @ e2),v_const(c_app c1 c2))); \ \ !!ve vem xm e1 e2 em v v2. \ -\ [| P(<,v_clos(<|xm,em,vem|>)>); \ -\ P(<,v2>); \ -\ P(< v2},em>,v>) \ +\ [| P(((ve,e1),v_clos(<|xm,em,vem|>))); \ +\ P(((ve,e2),v2)); \ +\ P(((vem + {xm |-> v2},em),v)) \ \ |] ==> \ -\ P(<,v>) \ +\ P(((ve,e1 @ e2),v)) \ \ |] ==> \ -\ P(<,v>)"; +\ P(((ve,e),v))"; by (resolve_tac (prems RL [lfp_ind2]) 1); by (rtac eval_fun_mono 1); by (rewtac eval_fun_def); @@ -356,23 +356,23 @@ val prems = goalw MT.thy [elab_def, elab_rel_def] " [| te |- e ===> t; \ -\ !!te c t. c isof t ==> P(<,t>); \ -\ !!te x. x:te_dom(te) ==> P(<,te_app te x>); \ +\ !!te c t. c isof t ==> P(((te,e_const(c)),t)); \ +\ !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \ \ !!te x e t1 t2. \ -\ [| te + {x |=> t1} |- e ===> t2; P(< t1},e>,t2>) |] ==> \ -\ P(< e>,t1->t2>); \ +\ [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \ +\ P(((te,fn x => e),t1->t2)); \ \ !!te f x e t1 t2. \ \ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \ -\ P(< t1->t2} + {x |=> t1},e>,t2>) \ +\ P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \ \ |] ==> \ -\ P(<,t1->t2>); \ +\ P(((te,fix f(x) = e),t1->t2)); \ \ !!te e1 e2 t1 t2. \ -\ [| te |- e1 ===> t1->t2; P(<,t1->t2>); \ -\ te |- e2 ===> t1; P(<,t1>) \ +\ [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \ +\ te |- e2 ===> t1; P(((te,e2),t1)) \ \ |] ==> \ -\ P(<,t2>) \ +\ P(((te,e1 @ e2),t2)) \ \ |] ==> \ -\ P(<,t>)"; +\ P(((te,e),t))"; by (resolve_tac (prems RL [lfp_ind2]) 1); by (rtac elab_fun_mono 1); by (rewtac elab_fun_def); @@ -412,18 +412,18 @@ val prems = goalw MT.thy [elab_def, elab_rel_def] " [| te |- e ===> t; \ -\ !!te c t. c isof t ==> P(<,t>); \ -\ !!te x. x:te_dom(te) ==> P(<,te_app te x>); \ +\ !!te c t. c isof t ==> P(((te,e_const(c)),t)); \ +\ !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \ \ !!te x e t1 t2. \ -\ te + {x |=> t1} |- e ===> t2 ==> P(< e>,t1->t2>); \ +\ te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \ \ !!te f x e t1 t2. \ \ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \ -\ P(<,t1->t2>); \ +\ P(((te,fix f(x) = e),t1->t2)); \ \ !!te e1 e2 t1 t2. \ \ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \ -\ P(<,t2>) \ +\ P(((te,e1 @ e2),t2)) \ \ |] ==> \ -\ P(<,t>)"; +\ P(((te,e),t))"; by (resolve_tac (prems RL [lfp_elim2]) 1); by (rtac elab_fun_mono 1); by (rewtac elab_fun_def); @@ -545,7 +545,7 @@ (* First strong indtroduction (co-induction) rule for hasty_rel *) -val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> : hasty_rel"; +val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel"; by (cut_facts_tac prems 1); by (rtac gfp_coind2 1); by (rewtac MT.hasty_fun_def); @@ -561,9 +561,9 @@ \ ve_dom(ve) = te_dom(te); \ \ ! ev1. \ \ ev1:ve_dom(ve) --> \ -\ : {),t>} Un hasty_rel \ +\ (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \ \ |] ==> \ -\ ),t> : hasty_rel"; +\ (v_clos(<|ev,e,ve|>),t) : hasty_rel"; by (cut_facts_tac prems 1); by (rtac gfp_coind2 1); by (rewtac hasty_fun_def); @@ -575,14 +575,14 @@ (* Elimination rule for hasty_rel *) val prems = goalw MT.thy [hasty_rel_def] - " [| !! c t.c isof t ==> P(); \ + " [| !! c t.c isof t ==> P((v_const(c),t)); \ \ !! te ev e t ve. \ \ [| te |- fn ev => e ===> t; \ \ ve_dom(ve) = te_dom(te); \ -\ !ev1.ev1:ve_dom(ve) --> : hasty_rel \ -\ |] ==> P(),t>); \ -\ : hasty_rel \ -\ |] ==> P()"; +\ !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \ +\ |] ==> P((v_clos(<|ev,e,ve|>),t)); \ +\ (v,t) : hasty_rel \ +\ |] ==> P((v,t))"; by (cut_facts_tac prems 1); by (etac gfp_elim2 1); by (rtac mono_hasty_fun 1); @@ -595,12 +595,12 @@ qed "hasty_rel_elim0"; val prems = goal MT.thy - " [| : hasty_rel; \ + " [| (v,t) : hasty_rel; \ \ !! c t.c isof t ==> P (v_const c) t; \ \ !! te ev e t ve. \ \ [| te |- fn ev => e ===> t; \ \ ve_dom(ve) = te_dom(te); \ -\ !ev1.ev1:ve_dom(ve) --> : hasty_rel \ +\ !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \ \ |] ==> P (v_clos <|ev,e,ve|>) t \ \ |] ==> P v t"; by (res_inst_tac [("P","P")] infsys_p2 1); diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/MT.thy --- a/src/HOL/ex/MT.thy Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/MT.thy Fri Mar 24 12:30:35 1995 +0100 @@ -196,27 +196,27 @@ eval_fun_def " eval_fun(s) == \ \ { pp. \ -\ (? ve c. pp=<,v_const(c)>) | \ -\ (? ve x. pp=<,ve_app ve x> & x:ve_dom(ve)) |\ -\ (? ve e x. pp=< e>,v_clos(<|x,e,ve|>)>)| \ +\ (? ve c. pp=((ve,e_const(c)),v_const(c))) | \ +\ (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |\ +\ (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| \ \ ( ? ve e x f cl. \ -\ pp=<,v_clos(cl)> & \ +\ pp=((ve,fix f(x) = e),v_clos(cl)) & \ \ cl=<|x, e, ve+{f |-> v_clos(cl)} |> \ \ ) | \ \ ( ? ve e1 e2 c1 c2. \ -\ pp=<,v_const(c_app c1 c2)> & \ -\ <,v_const(c1)>:s & <,v_const(c2)>:s \ +\ pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & \ +\ ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s \ \ ) | \ \ ( ? ve vem e1 e2 em xm v v2. \ -\ pp=<,v> & \ -\ <,v_clos(<|xm,em,vem|>)>:s & \ -\ <,v2>:s & \ -\ < v2},em>,v>:s \ +\ pp=((ve,e1 @ e2),v) & \ +\ ((ve,e1),v_clos(<|xm,em,vem|>)):s & \ +\ ((ve,e2),v2):s & \ +\ ((vem+{xm |-> v2},em),v):s \ \ ) \ \ }" eval_rel_def "eval_rel == lfp(eval_fun)" - eval_def "ve |- e ---> v == <,v>:eval_rel" + eval_def "ve |- e ---> v == ((ve,e),v):eval_rel" (* The static semantics is defined in the same way as the dynamic semantics. The relation te |- e ===> t express the expression e has the @@ -226,19 +226,19 @@ elab_fun_def "elab_fun(s) == \ \ { pp. \ -\ (? te c t. pp=<,t> & c isof t) | \ -\ (? te x. pp=<,te_app te x> & x:te_dom(te)) | \ -\ (? te x e t1 t2. pp=< e>,t1->t2> & < t1},e>,t2>:s) | \ +\ (? te c t. pp=((te,e_const(c)),t) & c isof t) | \ +\ (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | \ +\ (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | \ \ (? te f x e t1 t2. \ -\ pp=<,t1->t2> & < t1->t2}+{x |=> t1},e>,t2>:s \ +\ pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s \ \ ) | \ \ (? te e1 e2 t1 t2. \ -\ pp=<,t2> & <,t1->t2>:s & <,t1>:s \ +\ pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s \ \ ) \ \ }" elab_rel_def "elab_rel == lfp(elab_fun)" - elab_def "te |- e ===> t == <,t>:elab_rel" + elab_def "te |- e ===> t == ((te,e),t):elab_rel" (* The original correspondence relation *) @@ -258,18 +258,18 @@ hasty_fun_def " hasty_fun(r) == \ \ { p. \ -\ ( ? c t. p = & c isof t) | \ +\ ( ? c t. p = (v_const(c),t) & c isof t) | \ \ ( ? ev e ve t te. \ -\ p = ),t> & \ +\ p = (v_clos(<|ev,e,ve|>),t) & \ \ te |- fn ev => e ===> t & \ \ ve_dom(ve) = te_dom(te) & \ -\ (! ev1.ev1:ve_dom(ve) --> : r) \ +\ (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) \ \ ) \ \ } \ \ " hasty_rel_def "hasty_rel == gfp(hasty_fun)" - hasty_def "v hasty t == : hasty_rel" + hasty_def "v hasty t == (v,t) : hasty_rel" hasty_env_def " ve hastyenv te == \ \ ve_dom(ve) = te_dom(te) & \ diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/ROOT.ML Fri Mar 24 12:30:35 1995 +0100 @@ -8,7 +8,7 @@ CHOL_build_completed; (*Cause examples to fail if CHOL did*) -(writeln"Root file for CHOL examples"; +(writeln "Root file for CHOL examples"; proof_timing := true; loadpath := ["ex"]; time_use "ex/cla.ML"; @@ -28,5 +28,5 @@ time_use_thy "Term"; time_use_thy "Simult"; time_use_thy "MT"; - writeln "END: Root file for HOL examples" + writeln "END: Root file for CHOL examples" ) handle _ => exit 1; diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/SList.ML --- a/src/HOL/ex/SList.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/SList.ML Fri Mar 24 12:30:35 1995 +0100 @@ -156,18 +156,18 @@ (** pred_sexp lemmas **) goalw SList.thy [CONS_def,In1_def] - "!!M. [| M: sexp; N: sexp |] ==> : pred_sexp^+"; + "!!M. [| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+"; by (asm_simp_tac pred_sexp_ss 1); qed "pred_sexp_CONS_I1"; goalw SList.thy [CONS_def,In1_def] - "!!M. [| M: sexp; N: sexp |] ==> : pred_sexp^+"; + "!!M. [| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+"; by (asm_simp_tac pred_sexp_ss 1); qed "pred_sexp_CONS_I2"; val [prem] = goal SList.thy - " : pred_sexp^+ ==> \ -\ : pred_sexp^+ & : pred_sexp^+"; + "(CONS M1 M2, N) : pred_sexp^+ ==> \ +\ (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"; by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaE2)) 1); by (etac (sexp_CONS_D RS conjE) 1); diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/Term.ML --- a/src/HOL/ex/Term.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/Term.ML Fri Mar 24 12:30:35 1995 +0100 @@ -119,7 +119,7 @@ val [prem] = goal Term.thy "N: list(term(A)) ==> \ -\ !M. : pred_sexp^+ --> \ +\ !M. (N,M): pred_sexp^+ --> \ \ Abs_map (cut h (pred_sexp^+) M) N = \ \ Abs_map h N"; by (rtac (prem RS list.induct) 1); diff -r f4815812665b -r e61b058d58d2 src/HOL/ex/rel.ML --- a/src/HOL/ex/rel.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/ex/rel.ML Fri Mar 24 12:30:35 1995 +0100 @@ -17,8 +17,8 @@ ], None) [ - ("domain_def", "domain(r) == {a. ? b. : r}" ), - ("range2_def", "range2(r) == {b. ? a. : r}" ), + ("domain_def", "domain(r) == {a. ? b. (a,b) : r}" ), + ("range2_def", "range2(r) == {b. ? a. (a,b) : r}" ), ("field_def", "field(r) == domain(r) Un range2(r)" ) ]; end; @@ -33,12 +33,12 @@ (*** domain ***) -val [prem] = goalw Rel.thy [domain_def,Pair_def] ": r ==> a : domain(r)"; +val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)"; by (fast_tac (set_cs addIs [prem]) 1); qed "domainI"; val major::prems = goalw Rel.thy [domain_def] - "[| a : domain(r); !!y. : r ==> P |] ==> P"; + "[| a : domain(r); !!y. (a,y): r ==> P |] ==> P"; by (rtac (major RS CollectE) 1); by (etac exE 1); by (REPEAT (ares_tac prems 1)); @@ -47,12 +47,12 @@ (*** range2 ***) -val [prem] = goalw Rel.thy [range2_def,Pair_def] ": r ==> b : range2(r)"; +val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)"; by (fast_tac (set_cs addIs [prem]) 1); qed "range2I"; val major::prems = goalw Rel.thy [range2_def] - "[| b : range2(r); !!x. : r ==> P |] ==> P"; + "[| b : range2(r); !!x. (x,b): r ==> P |] ==> P"; by (rtac (major RS CollectE) 1); by (etac exE 1); by (REPEAT (ares_tac prems 1)); @@ -61,16 +61,16 @@ (*** field ***) -val [prem] = goalw Rel.thy [field_def] ": r ==> a : field(r)"; +val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> a : field(r)"; by (rtac (prem RS domainI RS UnI1) 1); qed "fieldI1"; -val [prem] = goalw Rel.thy [field_def] ": r ==> b : field(r)"; +val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> b : field(r)"; by (rtac (prem RS range2I RS UnI2) 1); qed "fieldI2"; val [prem] = goalw Rel.thy [field_def] - "(~ :r ==> : r) ==> a : field(r)"; + "(~ (c,a):r ==> (a,b): r) ==> a : field(r)"; by (rtac (prem RS domainI RS UnCI) 1); by (swap_res_tac [range2I] 1); by (etac notnotD 1); @@ -78,8 +78,8 @@ val major::prems = goalw Rel.thy [field_def] "[| a : field(r); \ -\ !!x. : r ==> P; \ -\ !!x. : r ==> P |] ==> P"; +\ !!x. (a,x): r ==> P; \ +\ !!x. (x,a): r ==> P |] ==> P"; by (rtac (major RS UnE) 1); by (REPEAT (eresolve_tac (prems@[domainE,range2E]) 1)); qed "fieldE"; @@ -98,7 +98,7 @@ (*If r allows well-founded induction then wf(r)*) val [prem1,prem2] = goalw Rel.thy [wf_def] "[| field(r)<=A; \ -\ !!P u. ! x:A. (! y. : r --> P(y)) --> P(x) ==> P(u) |] \ +\ !!P u. ! x:A. (! y. (y,x): r --> P(y)) --> P(x) ==> P(u) |] \ \ ==> wf(r)"; by (rtac (prem1 RS wfI) 1); by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);