# HG changeset patch # User wenzelm # Date 1126971326 -7200 # Node ID bcf7544875b26f4712686157182094daa11e9471 # Parent 151e76f0e3c78d7c41c7b5732b928349e2bd5be4 converted to Isar theory format; diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/CCL.ML --- a/src/CCL/CCL.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/CCL.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,13 +1,9 @@ -(* Title: CCL/ccl +(* Title: CCL/CCL.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -For ccl.thy. *) -open CCL; - val ccl_data_defs = [apply_def,fix_def]; val CCL_ss = set_ss addsimps [po_refl]; @@ -15,11 +11,11 @@ (*** Congruence Rules ***) (*similar to AP_THM in Gordon's HOL*) -qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)" +qed_goal "fun_cong" (the_context ()) "(f::'a=>'b) = g ==> f(x)=g(x)" (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) -qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)" +qed_goal "arg_cong" (the_context ()) "x=y ==> f(x)=f(y)" (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); Goal "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))"; @@ -27,10 +23,10 @@ by (fast_tac (set_cs addIs [po_abstractn]) 1); bind_thm("abstractn", standard (allI RS (result() RS mp))); -fun type_of_terms (Const("Trueprop",_) $ +fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t; -fun abs_prems thm = +fun abs_prems thm = let fun do_abs n thm (Type ("fun", [_,t])) = do_abs n (abstractn RSN (n,thm)) t | do_abs n thm _ = thm fun do_prems n [] thm = thm @@ -52,12 +48,12 @@ (*** Constructors are injective ***) -val prems = goal CCL.thy +val prems = goal (the_context ()) "[| x=a; y=b; x=y |] ==> a=b"; by (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals])))); qed "eq_lemma"; -fun mk_inj_rl thy rews s = +fun mk_inj_rl thy rews s = let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]); val inj_lemmas = List.concat (map mk_inj_lemmas rews); val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE @@ -66,7 +62,7 @@ in prove_goal thy s (fn _ => [tac]) end; -val ccl_injs = map (mk_inj_rl CCL.thy caseBs) +val ccl_injs = map (mk_inj_rl (the_context ()) caseBs) [" = <-> (a=a' & b=b')", "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"]; @@ -82,7 +78,7 @@ | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs; (* Doesn't handle binder types correctly *) - fun saturate thy sy name = + fun saturate thy sy name = let fun arg_str 0 a s = s | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")" | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s); @@ -94,9 +90,9 @@ fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b"); - val lemma = prove_goal CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)" + val lemma = prove_goal (the_context ()) "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)" (fn _ => [simp_tac CCL_ss 1]) RS mp; - fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL + fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL [distinctness RS notE,sym RS (distinctness RS notE)]; in fun mk_lemmas rls = List.concat (map mk_lemma (mk_combs pair rls)); @@ -106,14 +102,14 @@ val caseB_lemmas = mk_lemmas caseBs; -val ccl_dstncts = - let fun mk_raw_dstnct_thm rls s = - prove_goal CCL.thy s (fn _=> [rtac notI 1,eresolve_tac rls 1]) - in map (mk_raw_dstnct_thm caseB_lemmas) - (mk_dstnct_rls CCL.thy ["bot","true","false","pair","lambda"]) end; +val ccl_dstncts = + let fun mk_raw_dstnct_thm rls s = + prove_goal (the_context ()) s (fn _=> [rtac notI 1,eresolve_tac rls 1]) + in map (mk_raw_dstnct_thm caseB_lemmas) + (mk_dstnct_rls (the_context ()) ["bot","true","false","pair","lambda"]) end; -fun mk_dstnct_thms thy defs inj_rls xs = - let fun mk_dstnct_thm rls s = prove_goalw thy defs s +fun mk_dstnct_thms thy defs inj_rls xs = + let fun mk_dstnct_thm rls s = prove_goalw thy defs s (fn _ => [simp_tac (CCL_ss addsimps (rls@inj_rls)) 1]) in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end; @@ -131,12 +127,12 @@ val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts; val ccl_ss = CCL_ss addsimps ccl_rews; -val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) +val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) addSDs (XH_to_Ds ccl_injs); (****** Facts from gfp Definition of [= and = ******) -val major::prems = goal Set.thy "[| A=B; a:B <-> P |] ==> a:A <-> P"; +val major::prems = goal (the_context ()) "[| A=B; a:B <-> P |] ==> a:A <-> P"; by (resolve_tac (prems RL [major RS ssubst]) 1); qed "XHlemma1"; @@ -166,7 +162,7 @@ \ (EX a a' b b'. t= & t'= & a [= a' & b [= b') | \ \ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))"; by (simp_tac (ccl_ss addsimps [PO_iff] delsimps ex_simps) 1); -by (rtac (rewrite_rule [POgen_def,SIM_def] +by (rtac (rewrite_rule [POgen_def,SIM_def] (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1); by (rtac (iff_refl RS XHlemma2) 1); qed "poXH"; @@ -198,31 +194,31 @@ val ccl_porews = [po_bot,po_pair,po_lam]; -val [p1,p2,p3,p4,p5] = goal CCL.thy +val [p1,p2,p3,p4,p5] = goal (the_context ()) "[| t [= t'; a [= a'; b [= b'; !!x y. c(x,y) [= c'(x,y); \ \ !!u. d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')"; by (rtac (p1 RS po_cong RS po_trans) 1); by (rtac (p2 RS po_cong RS po_trans) 1); by (rtac (p3 RS po_cong RS po_trans) 1); by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1); -by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] +by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] (p5 RS po_abstractn RS po_cong RS po_trans) 1); by (rtac po_refl 1); qed "case_pocong"; -val [p1,p2] = goalw CCL.thy ccl_data_defs +val [p1,p2] = goalw (the_context ()) ccl_data_defs "[| f [= f'; a [= a' |] ==> f ` a [= f' ` a'"; by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1)); qed "apply_pocong"; -val prems = goal CCL.thy "~ lam x. b(x) [= bot"; +val prems = goal (the_context ()) "~ lam x. b(x) [= bot"; by (rtac notI 1); by (dtac bot_poleast 1); by (etac (distinctness RS notE) 1); qed "npo_lam_bot"; -val eq1::eq2::prems = goal CCL.thy +val eq1::eq2::prems = goal (the_context ()) "[| x=a; y=b; x[=y |] ==> a[=b"; by (rtac (eq1 RS subst) 1); by (rtac (eq2 RS subst) 1); @@ -243,7 +239,7 @@ by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)); qed "npo_lam_pair"; -fun mk_thm s = prove_goal CCL.thy s (fn _ => +fun mk_thm s = prove_goal (the_context ()) s (fn _ => [rtac notI 1,dtac case_pocong 1,etac rev_mp 5, ALLGOALS (simp_tac ccl_ss), REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]); @@ -257,7 +253,7 @@ (* Coinduction for [= *) -val prems = goal CCL.thy "[| : R; R <= POgen(R) |] ==> t [= u"; +val prems = goal (the_context ()) "[| : R; R <= POgen(R) |] ==> t [= u"; by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1); by (REPEAT (ares_tac prems 1)); qed "po_coinduct"; @@ -297,12 +293,12 @@ by (rtac (iff_refl RS XHlemma2) 1); qed "eqXH"; -val prems = goal CCL.thy "[| : R; R <= EQgen(R) |] ==> t = u"; +val prems = goal (the_context ()) "[| : R; R <= EQgen(R) |] ==> t = u"; by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1); by (REPEAT (ares_tac prems 1)); qed "eq_coinduct"; -val prems = goal CCL.thy +val prems = goal (the_context ()) "[| : R; R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u"; by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1); by (REPEAT (ares_tac (EQgen_mono::prems) 1)); @@ -323,7 +319,7 @@ by (fast_tac set_cs 1); qed "exhaustion"; -val prems = goal CCL.thy +val prems = goal (the_context ()) "[| P(bot); P(true); P(false); !!x y. P(); !!b. P(lam x. b(x)) |] ==> P(t)"; by (cut_facts_tac [exhaustion] 1); by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst])); diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/CCL.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,27 +1,30 @@ -(* Title: CCL/ccl.thy +(* Title: CCL/CCL.thy ID: $Id$ Author: Martin Coen Copyright 1993 University of Cambridge - -Classical Computational Logic for Untyped Lambda Calculus with reduction to -weak head-normal form. - -Based on FOL extended with set collection, a primitive higher-order logic. -HOL is too strong - descriptions prevent a type of programs being defined -which contains only executable terms. *) -CCL = Gfp + +header {* Classical Computational Logic for Untyped Lambda Calculus + with reduction to weak head-normal form *} -classes prog < term - -default prog +theory CCL +imports Gfp +begin -types i +text {* + Based on FOL extended with set collection, a primitive higher-order + logic. HOL is too strong - descriptions prevent a type of programs + being defined which contains only executable terms. +*} -arities - i :: prog - fun :: (prog,prog)prog +classes prog < "term" +defaultsort prog + +arities fun :: (prog, prog) prog + +typedecl i +arities i :: prog + consts (*** Evaluation Judgement ***) @@ -30,22 +33,26 @@ (*** Bisimulations for pre-order and equality ***) "[=" :: "['a,'a]=>o" (infixl 50) SIM :: "[i,i,i set]=>o" - POgen,EQgen :: "i set => i set" - PO,EQ :: "i set" + POgen :: "i set => i set" + EQgen :: "i set => i set" + PO :: "i set" + EQ :: "i set" (*** Term Formers ***) - true,false :: "i" + true :: "i" + false :: "i" pair :: "[i,i]=>i" ("(1<_,/_>)") lambda :: "(i=>i)=>i" (binder "lam " 55) - case :: "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i" + "case" :: "[i,i,i,[i,i]=>i,(i=>i)=>i]=>i" "`" :: "[i,i]=>i" (infixl 56) bot :: "i" - fix :: "(i=>i)=>i" + "fix" :: "(i=>i)=>i" (*** Defined Predicates ***) - Trm,Dvg :: "i => o" + Trm :: "i => o" + Dvg :: "i => o" -rules +axioms (******* EVALUATION SEMANTICS *******) @@ -53,96 +60,96 @@ (** It is included here just as an evaluator for FUN and has no influence on **) (** inference in the theory CCL. **) - trueV "true ---> true" - falseV "false ---> false" - pairV " ---> " - lamV "lam x. b(x) ---> lam x. b(x)" - caseVtrue "[| t ---> true; d ---> c |] ==> case(t,d,e,f,g) ---> c" - caseVfalse "[| t ---> false; e ---> c |] ==> case(t,d,e,f,g) ---> c" - caseVpair "[| t ---> ; f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c" - caseVlam "[| t ---> lam x. b(x); g(b) ---> c |] ==> case(t,d,e,f,g) ---> c" + trueV: "true ---> true" + falseV: "false ---> false" + pairV: " ---> " + lamV: "lam x. b(x) ---> lam x. b(x)" + caseVtrue: "[| t ---> true; d ---> c |] ==> case(t,d,e,f,g) ---> c" + caseVfalse: "[| t ---> false; e ---> c |] ==> case(t,d,e,f,g) ---> c" + caseVpair: "[| t ---> ; f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c" + caseVlam: "[| t ---> lam x. b(x); g(b) ---> c |] ==> case(t,d,e,f,g) ---> c" (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***) - canonical "[| t ---> c; c==true ==> u--->v; - c==false ==> u--->v; - !!a b. c== ==> u--->v; - !!f. c==lam x. f(x) ==> u--->v |] ==> + canonical: "[| t ---> c; c==true ==> u--->v; + c==false ==> u--->v; + !!a b. c== ==> u--->v; + !!f. c==lam x. f(x) ==> u--->v |] ==> u--->v" (* Should be derivable - but probably a bitch! *) - substitute "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')" + substitute: "[| a==a'; t(a)--->c(a) |] ==> t(a')--->c(a')" (************** LOGIC ***************) (*** Definitions used in the following rules ***) - apply_def "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))" - bot_def "bot == (lam x. x`x)`(lam x. x`x)" - fix_def "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))" + apply_def: "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))" + bot_def: "bot == (lam x. x`x)`(lam x. x`x)" + fix_def: "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))" (* The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *) (* as a bisimulation. They can both be expressed as (bi)simulations up to *) (* behavioural equivalence (ie the relations PO and EQ defined below). *) - SIM_def - "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) | - (EX a a' b b'. t= & t'= & : R & : R) | + SIM_def: + "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) | + (EX a a' b b'. t= & t'= & : R & : R) | (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. : R))" - POgen_def "POgen(R) == {p. EX t t'. p= & (t = bot | SIM(t,t',R))}" - EQgen_def "EQgen(R) == {p. EX t t'. p= & (t = bot & t' = bot | SIM(t,t',R))}" + POgen_def: "POgen(R) == {p. EX t t'. p= & (t = bot | SIM(t,t',R))}" + EQgen_def: "EQgen(R) == {p. EX t t'. p= & (t = bot & t' = bot | SIM(t,t',R))}" - PO_def "PO == gfp(POgen)" - EQ_def "EQ == gfp(EQgen)" + PO_def: "PO == gfp(POgen)" + EQ_def: "EQ == gfp(EQgen)" (*** Rules ***) (** Partial Order **) - po_refl "a [= a" - po_trans "[| a [= b; b [= c |] ==> a [= c" - po_cong "a [= b ==> f(a) [= f(b)" + po_refl: "a [= a" + po_trans: "[| a [= b; b [= c |] ==> a [= c" + po_cong: "a [= b ==> f(a) [= f(b)" (* Extend definition of [= to program fragments of higher type *) - po_abstractn "(!!x. f(x) [= g(x)) ==> (%x. f(x)) [= (%x. g(x))" + po_abstractn: "(!!x. f(x) [= g(x)) ==> (%x. f(x)) [= (%x. g(x))" (** Equality - equivalence axioms inherited from FOL.thy **) (** - congruence of "=" is axiomatised implicitly **) - eq_iff "t = t' <-> t [= t' & t' [= t" + eq_iff: "t = t' <-> t [= t' & t' [= t" (** Properties of canonical values given by greatest fixed point definitions **) - - PO_iff "t [= t' <-> : PO" - EQ_iff "t = t' <-> : EQ" + + PO_iff: "t [= t' <-> : PO" + EQ_iff: "t = t' <-> : EQ" (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **) - caseBtrue "case(true,d,e,f,g) = d" - caseBfalse "case(false,d,e,f,g) = e" - caseBpair "case(,d,e,f,g) = f(a,b)" - caseBlam "case(lam x. b(x),d,e,f,g) = g(b)" - caseBbot "case(bot,d,e,f,g) = bot" (* strictness *) + caseBtrue: "case(true,d,e,f,g) = d" + caseBfalse: "case(false,d,e,f,g) = e" + caseBpair: "case(,d,e,f,g) = f(a,b)" + caseBlam: "case(lam x. b(x),d,e,f,g) = g(b)" + caseBbot: "case(bot,d,e,f,g) = bot" (* strictness *) (** The theory is non-trivial **) - distinctness "~ lam x. b(x) = bot" + distinctness: "~ lam x. b(x) = bot" (*** Definitions of Termination and Divergence ***) - Dvg_def "Dvg(t) == t = bot" - Trm_def "Trm(t) == ~ Dvg(t)" + Dvg_def: "Dvg(t) == t = bot" + Trm_def: "Trm(t) == ~ Dvg(t)" -end - - -(* +text {* Would be interesting to build a similar theory for a typed programming language: ie. true :: bool, fix :: ('a=>'a)=>'a etc...... This is starting to look like LCF. -What are the advantages of this approach? - - less axiomatic +What are the advantages of this approach? + - less axiomatic - wfd induction / coinduction and fixed point induction available - -*) +*} + +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Fix.ML --- a/src/CCL/Fix.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Fix.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,16 +1,12 @@ -(* Title: CCL/fix +(* Title: CCL/Fix.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -For fix.thy. *) -open Fix; - (*** Fixed Point Induction ***) -val [base,step,incl] = goalw Fix.thy [INCL_def] +val [base,step,incl] = goalw (the_context ()) [INCL_def] "[| P(bot); !!x. P(x) ==> P(f(x)); INCL(P) |] ==> P(fix(f))"; by (rtac (incl RS spec RS mp) 1); by (rtac (Nat_ind RS ballI) 1 THEN atac 1); @@ -20,23 +16,23 @@ (*** Inclusive Predicates ***) -val prems = goalw Fix.thy [INCL_def] +val prems = goalw (the_context ()) [INCL_def] "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))"; by (rtac iff_refl 1); qed "inclXH"; -val prems = goal Fix.thy +val prems = goal (the_context ()) "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))"; by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1); qed "inclI"; -val incl::prems = goal Fix.thy +val incl::prems = goal (the_context ()) "[| INCL(P); !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))"; -by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] +by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] @ prems)) 1); qed "inclD"; -val incl::prems = goal Fix.thy +val incl::prems = goal (the_context ()) "[| INCL(P); (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R"; by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1); qed "inclE"; @@ -55,15 +51,15 @@ by (rtac po_cong 1 THEN rtac po_bot 1); qed "npo_INCL"; -val prems = goal Fix.thy "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))"; +val prems = goal (the_context ()) "[| INCL(P); INCL(Q) |] ==> INCL(%x. P(x) & Q(x))"; by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; qed "conj_INCL"; -val prems = goal Fix.thy "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))"; +val prems = goal (the_context ()) "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))"; by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; qed "all_INCL"; -val prems = goal Fix.thy "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))"; +val prems = goal (the_context ()) "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))"; by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);; qed "ball_INCL"; @@ -88,7 +84,7 @@ (* All fixed points are lam-expressions *) -val [prem] = goal Fix.thy "idgen(d) = d ==> d = lam x.?f(x)"; +val [prem] = goal (the_context ()) "idgen(d) = d ==> d = lam x.?f(x)"; by (rtac (prem RS subst) 1); by (rewtac idgen_def); by (rtac refl 1); @@ -96,13 +92,13 @@ (* Lemmas for rewriting fixed points of idgen *) -val prems = goalw Fix.thy [idgen_def] +val prems = goalw (the_context ()) [idgen_def] "[| a = b; a ` t = u |] ==> b ` t = u"; by (simp_tac (term_ss addsimps (prems RL [sym])) 1); qed "l_lemma"; val idgen_lemmas = - let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s + let fun mk_thm s = prove_goalw (the_context ()) [idgen_def] s (fn [prem] => [rtac (prem RS l_lemma) 1,simp_tac term_ss 1]) in map mk_thm [ "idgen(d) = d ==> d ` bot = bot", @@ -112,22 +108,22 @@ "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"] end; -(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points +(* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points of idgen and hence are they same *) -val [p1,p2,p3] = goal CCL.thy +val [p1,p2,p3] = goal (the_context ()) "[| ALL x. t ` x [= u ` x; EX f. t=lam x. f(x); EX f. u=lam x. f(x) |] ==> t [= u"; by (stac (p2 RS cond_eta) 1); by (stac (p3 RS cond_eta) 1); by (rtac (p1 RS (po_lam RS iffD2)) 1); qed "po_eta"; -val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)"; +val [prem] = goalw (the_context ()) [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)"; by (rtac (prem RS subst) 1); by (rtac refl 1); qed "po_eta_lemma"; -val [prem] = goal Fix.thy +val [prem] = goal (the_context ()) "idgen(d) = d ==> \ \ {p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)} <= \ \ POgen({p. EX a b. p= & (EX t. a=fix(idgen) ` t & b = d ` t)})"; @@ -137,14 +133,14 @@ by (ALLGOALS (fast_tac set_cs)); qed "lemma1"; -val [prem] = goal Fix.thy +val [prem] = goal (the_context ()) "idgen(d) = d ==> fix(idgen) [= d"; by (rtac (allI RS po_eta) 1); by (rtac (lemma1 RSN(2,po_coinduct)) 1); by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp]))); qed "fix_least_idgen"; -val [prem] = goal Fix.thy +val [prem] = goal (the_context ()) "idgen(d) = d ==> \ \ {p. EX a b. p= & b = d ` a} <= POgen({p. EX a b. p= & b = d ` a})"; by (REPEAT (step_tac term_cs 1)); @@ -153,7 +149,7 @@ by (ALLGOALS (fast_tac set_cs)); qed "lemma2"; -val [prem] = goal Fix.thy +val [prem] = goal (the_context ()) "idgen(d) = d ==> lam x. x [= d"; by (rtac (allI RS po_eta) 1); by (rtac (lemma2 RSN(2,po_coinduct)) 1); @@ -169,12 +165,12 @@ (********) -val [prem] = goal Fix.thy "f = lam x. x ==> f`t = t"; +val [prem] = goal (the_context ()) "f = lam x. x ==> f`t = t"; by (rtac (prem RS sym RS subst) 1); by (rtac applyB 1); qed "id_apply"; -val prems = goal Fix.thy +val prems = goal (the_context ()) "[| P(bot); P(true); P(false); \ \ !!x y.[| P(x); P(y) |] ==> P(); \ \ !!u.(!!x. P(u(x))) ==> P(lam x. u(x)); INCL(P) |] ==> \ @@ -191,4 +187,3 @@ by (ALLGOALS (simp_tac term_ss)); by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems)))); qed "term_ind"; - diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Fix.thy --- a/src/CCL/Fix.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Fix.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,26 +1,27 @@ -(* Title: CCL/Lazy/fix.thy +(* Title: CCL/Fix.thy ID: $Id$ Author: Martin Coen Copyright 1993 University of Cambridge - -Tentative attempt at including fixed point induction. -Justified by Smith. *) -Fix = Type + +header {* Tentative attempt at including fixed point induction; justified by Smith *} + +theory Fix +imports Type +begin consts - idgen :: "[i]=>i" INCL :: "[i=>o]=>o" -rules - - idgen_def +axioms + idgen_def: "idgen(f) == lam t. case(t,true,false,%x y.,%u. lam x. f ` u(x))" - INCL_def "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" - po_INCL "INCL(%x. a(x) [= b(x))" - INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" + INCL_def: "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" + po_INCL: "INCL(%x. a(x) [= b(x))" + INCL_subst: "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Gfp.ML --- a/src/CCL/Gfp.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Gfp.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,55 +1,46 @@ -(* Title: CCL/gfp +(* Title: CCL/Gfp.ML ID: $Id$ - -Modified version of - Title: HOL/gfp - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -For gfp.thy. The Knaster-Tarski Theorem for greatest fixed points. *) -open Gfp; - (*** Proof of Knaster-Tarski Theorem using gfp ***) (* gfp(f) is the least upper bound of {u. u <= f(u)} *) -val prems = goalw Gfp.thy [gfp_def] "[| A <= f(A) |] ==> A <= gfp(f)"; +val prems = goalw (the_context ()) [gfp_def] "[| A <= f(A) |] ==> A <= gfp(f)"; by (rtac (CollectI RS Union_upper) 1); by (resolve_tac prems 1); qed "gfp_upperbound"; -val prems = goalw Gfp.thy [gfp_def] +val prems = goalw (the_context ()) [gfp_def] "[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A"; by (REPEAT (ares_tac ([Union_least]@prems) 1)); by (etac CollectD 1); qed "gfp_least"; -val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))"; +val [mono] = goal (the_context ()) "mono(f) ==> gfp(f) <= f(gfp(f))"; by (EVERY1 [rtac gfp_least, rtac subset_trans, atac, rtac (mono RS monoD), rtac gfp_upperbound, atac]); qed "gfp_lemma2"; -val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)"; +val [mono] = goal (the_context ()) "mono(f) ==> f(gfp(f)) <= gfp(f)"; by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), rtac gfp_lemma2, rtac mono]); qed "gfp_lemma3"; -val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))"; +val [mono] = goal (the_context ()) "mono(f) ==> gfp(f) = f(gfp(f))"; by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1)); qed "gfp_Tarski"; (*** Coinduction rules for greatest fixed points ***) (*weak version*) -val prems = goal Gfp.thy +val prems = goal (the_context ()) "[| a: A; A <= f(A) |] ==> a : gfp(f)"; by (rtac (gfp_upperbound RS subsetD) 1); by (REPEAT (ares_tac prems 1)); qed "coinduct"; -val [prem,mono] = goal Gfp.thy +val [prem,mono] = goal (the_context ()) "[| A <= f(A) Un gfp(f); mono(f) |] ==> \ \ A Un gfp(f) <= f(A Un gfp(f))"; by (rtac subset_trans 1); @@ -60,7 +51,7 @@ qed "coinduct2_lemma"; (*strong version, thanks to Martin Coen*) -val ainA::prems = goal Gfp.thy +val ainA::prems = goal (the_context ()) "[| a: A; A <= f(A) Un gfp(f); mono(f) |] ==> a : gfp(f)"; by (rtac coinduct 1); by (rtac (prems MRS coinduct2_lemma) 2); @@ -71,11 +62,11 @@ - instead of the condition A <= f(A) consider A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***) -val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un A Un B)"; +val [prem] = goal (the_context ()) "mono(f) ==> mono(%x. f(x) Un A Un B)"; by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1)); qed "coinduct3_mono_lemma"; -val [prem,mono] = goal Gfp.thy +val [prem,mono] = goal (the_context ()) "[| A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> \ \ lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))"; by (rtac subset_trans 1); @@ -89,7 +80,7 @@ by (rtac Un_upper2 1); qed "coinduct3_lemma"; -val ainA::prems = goal Gfp.thy +val ainA::prems = goal (the_context ()) "[| a:A; A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)"; by (rtac coinduct 1); by (rtac (prems MRS coinduct3_lemma) 2); @@ -100,31 +91,31 @@ (** Definition forms of gfp_Tarski, to control unfolding **) -val [rew,mono] = goal Gfp.thy "[| h==gfp(f); mono(f) |] ==> h = f(h)"; +val [rew,mono] = goal (the_context ()) "[| h==gfp(f); mono(f) |] ==> h = f(h)"; by (rewtac rew); by (rtac (mono RS gfp_Tarski) 1); qed "def_gfp_Tarski"; -val rew::prems = goal Gfp.thy +val rew::prems = goal (the_context ()) "[| h==gfp(f); a:A; A <= f(A) |] ==> a: h"; by (rewtac rew); by (REPEAT (ares_tac (prems @ [coinduct]) 1)); qed "def_coinduct"; -val rew::prems = goal Gfp.thy +val rew::prems = goal (the_context ()) "[| h==gfp(f); a:A; A <= f(A) Un h; mono(f) |] ==> a: h"; by (rewtac rew); by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct2]) 1)); qed "def_coinduct2"; -val rew::prems = goal Gfp.thy +val rew::prems = goal (the_context ()) "[| h==gfp(f); a:A; A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a: h"; by (rewtac rew); by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1)); qed "def_coinduct3"; (*Monotonicity of gfp!*) -val prems = goal Gfp.thy +val prems = goal (the_context ()) "[| mono(f); !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"; by (rtac gfp_upperbound 1); by (rtac subset_trans 1); diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Gfp.thy --- a/src/CCL/Gfp.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Gfp.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,14 +1,19 @@ -(* Title: HOL/gfp.thy +(* Title: CCL/Gfp.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge - -Greatest fixed points *) -Gfp = Lfp + -consts gfp :: "['a set=>'a set] => 'a set" -rules - (*greatest fixed point*) - gfp_def "gfp(f) == Union({u. u <= f(u)})" +header {* Greatest fixed points *} + +theory Gfp +imports Lfp +begin + +constdefs + gfp :: "['a set=>'a set] => 'a set" (*greatest fixed point*) + "gfp(f) == Union({u. u <= f(u)})" + +ML {* use_legacy_bindings (the_context ()) *} + end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Hered.ML --- a/src/CCL/Hered.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Hered.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,13 +1,9 @@ -(* Title: CCL/hered +(* Title: CCL/Hered.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -For hered.thy. *) -open Hered; - fun type_of_terms (Const("Trueprop",_) $ (Const("op =",(Type ("fun", [t,_])))$_$_)) = t; (*** Hereditary Termination ***) @@ -26,7 +22,7 @@ Goal "t : HTT <-> t=true | t=false | (EX a b. t= & a : HTT & b : HTT) | \ \ (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))"; -by (rtac (rewrite_rule [HTTgen_def] +by (rtac (rewrite_rule [HTTgen_def] (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1); by (fast_tac set_cs 1); qed "HTTXH"; @@ -60,7 +56,7 @@ local val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam]; - fun mk_thm s = prove_goalw Hered.thy data_defs s (fn _ => + fun mk_thm s = prove_goalw (the_context ()) data_defs s (fn _ => [simp_tac (term_ss addsimps raw_HTTrews) 1]); in val HTT_rews = raw_HTTrews @ @@ -77,14 +73,14 @@ (*** Coinduction for HTT ***) -val prems = goal Hered.thy "[| t : R; R <= HTTgen(R) |] ==> t : HTT"; +val prems = goal (the_context ()) "[| t : R; R <= HTTgen(R) |] ==> t : HTT"; by (rtac (HTT_def RS def_coinduct) 1); by (REPEAT (ares_tac prems 1)); qed "HTT_coinduct"; fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i; -val prems = goal Hered.thy +val prems = goal (the_context ()) "[| t : R; R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT"; by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1); by (REPEAT (ares_tac prems 1)); @@ -93,7 +89,7 @@ fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i; -val HTTgenIs = map (mk_genIs Hered.thy data_defs HTTgenXH HTTgen_mono) +val HTTgenIs = map (mk_genIs (the_context ()) data_defs HTTgenXH HTTgen_mono) ["true : HTTgen(R)", "false : HTTgen(R)", "[| a : R; b : R |] ==> : HTTgen(R)", @@ -121,12 +117,12 @@ by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); qed "BoolF"; -val prems = goal Hered.thy "[| A <= HTT; B <= HTT |] ==> A + B <= HTT"; +val prems = goal (the_context ()) "[| A <= HTT; B <= HTT |] ==> A + B <= HTT"; by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1); by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); qed "PlusF"; -val prems = goal Hered.thy +val prems = goal (the_context ()) "[| A <= HTT; !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT"; by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1); by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1); @@ -146,38 +142,38 @@ Goal "Nat <= HTT"; by (safe_tac set_cs); by (etac HTT_coinduct3 1); -by (fast_tac (set_cs addIs HTTgenIs +by (fast_tac (set_cs addIs HTTgenIs addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1); qed "NatF"; -val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT"; +val [prem] = goal (the_context ()) "A <= HTT ==> List(A) <= HTT"; by (safe_tac set_cs); by (etac HTT_coinduct3 1); -by (fast_tac (set_cs addSIs HTTgenIs - addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] +by (fast_tac (set_cs addSIs HTTgenIs + addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] addEs [XH_to_E ListXH]) 1); qed "ListF"; -val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT"; +val [prem] = goal (the_context ()) "A <= HTT ==> Lists(A) <= HTT"; by (safe_tac set_cs); by (etac HTT_coinduct3 1); -by (fast_tac (set_cs addSIs HTTgenIs - addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] +by (fast_tac (set_cs addSIs HTTgenIs + addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] addEs [XH_to_E ListsXH]) 1); qed "ListsF"; -val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT"; +val [prem] = goal (the_context ()) "A <= HTT ==> ILists(A) <= HTT"; by (safe_tac set_cs); by (etac HTT_coinduct3 1); -by (fast_tac (set_cs addSIs HTTgenIs - addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] +by (fast_tac (set_cs addSIs HTTgenIs + addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] addEs [XH_to_E IListsXH]) 1); qed "IListsF"; (*** A possible use for this predicate is proving equality from pre-order ***) (*** but it seems as easy (and more general) to do this directly by coinduction ***) (* -val prems = goal Hered.thy "[| t : HTT; t [= u |] ==> u [= t"; +val prems = goal (the_context ()) "[| t : HTT; t [= u |] ==> u [= t"; by (po_coinduct_tac "{p. EX a b. p= & b : HTT & b [= a}" 1); by (fast_tac (ccl_cs addIs prems) 1); by (safe_tac ccl_cs); @@ -188,7 +184,7 @@ by (ALLGOALS (fast_tac ccl_cs)); qed "HTT_po_op"; -val prems = goal Hered.thy "[| t : HTT; t [= u |] ==> t = u"; +val prems = goal (the_context ()) "[| t : HTT; t [= u |] ==> t = u"; by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1)); qed "HTT_po_eq"; *) diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Hered.thy --- a/src/CCL/Hered.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Hered.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,30 +1,35 @@ -(* Title: CCL/hered.thy +(* Title: CCL/Hered.thy ID: $Id$ Author: Martin Coen Copyright 1993 University of Cambridge - -Hereditary Termination - cf. Martin Lo\"f - -Note that this is based on an untyped equality and so lam x.b(x) is only -hereditarily terminating if ALL x.b(x) is. Not so useful for functions! - *) -Hered = Type + +header {* Hereditary Termination -- cf. Martin Lo\"f *} + +theory Hered +imports Type +uses "coinduction.ML" +begin + +text {* + Note that this is based on an untyped equality and so @{text "lam + x. b(x)"} is only hereditarily terminating if @{text "ALL x. b(x)"} + is. Not so useful for functions! +*} consts (*** Predicates ***) HTTgen :: "i set => i set" HTT :: "i set" - -rules - +axioms (*** Definitions of Hereditary Termination ***) - HTTgen_def - "HTTgen(R) == {t. t=true | t=false | (EX a b. t= & a : R & b : R) | + HTTgen_def: + "HTTgen(R) == {t. t=true | t=false | (EX a b. t= & a : R & b : R) | (EX f. t=lam x. f(x) & (ALL x. f(x) : R))}" - HTT_def "HTT == gfp(HTTgen)" + HTT_def: "HTT == gfp(HTTgen)" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/IsaMakefile --- a/src/CCL/IsaMakefile Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/IsaMakefile Sat Sep 17 17:35:26 2005 +0200 @@ -30,7 +30,7 @@ $(OUT)/CCL: $(OUT)/FOL CCL.ML CCL.thy Fix.ML Fix.thy Gfp.ML Gfp.thy \ Hered.ML Hered.thy Lfp.ML Lfp.thy ROOT.ML Set.ML Set.thy Term.ML \ - Term.thy Trancl.ML Trancl.thy Type.ML Type.thy Wfd.ML Wfd.thy \ + Term.thy Trancl.ML Trancl.thy Type.ML Type.thy wfd.ML Wfd.thy \ coinduction.ML equalities.ML eval.ML genrec.ML mono.ML subset.ML \ typecheck.ML @$(ISATOOL) usedir -b -r $(OUT)/FOL CCL diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Lfp.ML --- a/src/CCL/Lfp.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Lfp.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,55 +1,46 @@ -(* Title: CCL/lfp +(* Title: CCL/Lfp.ML ID: $Id$ - -Modified version of - Title: HOL/lfp.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -For lfp.thy. The Knaster-Tarski Theorem *) -open Lfp; - (*** Proof of Knaster-Tarski Theorem ***) (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) -val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A"; +val prems = goalw (the_context ()) [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A"; by (rtac (CollectI RS Inter_lower) 1); by (resolve_tac prems 1); qed "lfp_lowerbound"; -val prems = goalw Lfp.thy [lfp_def] +val prems = goalw (the_context ()) [lfp_def] "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)"; by (REPEAT (ares_tac ([Inter_greatest]@prems) 1)); by (etac CollectD 1); qed "lfp_greatest"; -val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)"; +val [mono] = goal (the_context ()) "mono(f) ==> f(lfp(f)) <= lfp(f)"; by (EVERY1 [rtac lfp_greatest, rtac subset_trans, rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]); qed "lfp_lemma2"; -val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))"; -by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), +val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) <= f(lfp(f))"; +by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), rtac lfp_lemma2, rtac mono]); qed "lfp_lemma3"; -val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))"; +val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) = f(lfp(f))"; by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1)); qed "lfp_Tarski"; (*** General induction rule for least fixed points ***) -val [lfp,mono,indhyp] = goal Lfp.thy +val [lfp,mono,indhyp] = goal (the_context ()) "[| a: lfp(f); mono(f); \ \ !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x) \ \ |] ==> P(a)"; by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1); by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1); -by (EVERY1 [rtac Int_greatest, rtac subset_trans, +by (EVERY1 [rtac Int_greatest, rtac subset_trans, rtac (Int_lower1 RS (mono RS monoD)), rtac (mono RS lfp_lemma2), rtac (CollectI RS subsetI), rtac indhyp, atac]); @@ -57,12 +48,12 @@ (** Definition forms of lfp_Tarski and induct, to control unfolding **) -val [rew,mono] = goal Lfp.thy "[| h==lfp(f); mono(f) |] ==> h = f(h)"; +val [rew,mono] = goal (the_context ()) "[| h==lfp(f); mono(f) |] ==> h = f(h)"; by (rewtac rew); by (rtac (mono RS lfp_Tarski) 1); qed "def_lfp_Tarski"; -val rew::prems = goal Lfp.thy +val rew::prems = goal (the_context ()) "[| A == lfp(f); a:A; mono(f); \ \ !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) \ \ |] ==> P(a)"; @@ -71,7 +62,7 @@ qed "def_induct"; (*Monotonicity of lfp!*) -val prems = goal Lfp.thy +val prems = goal (the_context ()) "[| mono(g); !!Z. f(Z)<=g(Z) |] ==> lfp(f) <= lfp(g)"; by (rtac lfp_lowerbound 1); by (rtac subset_trans 1); @@ -79,4 +70,3 @@ by (rtac lfp_lemma2 1); by (resolve_tac prems 1); qed "lfp_mono"; - diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Lfp.thy --- a/src/CCL/Lfp.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Lfp.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,14 +1,20 @@ -(* Title: HOL/lfp.thy +(* Title: CCL/Lfp.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge - -The Knaster-Tarski Theorem *) -Lfp = Set + -consts lfp :: "['a set=>'a set] => 'a set" -rules - (*least fixed point*) - lfp_def "lfp(f) == Inter({u. f(u) <= u})" +header {* The Knaster-Tarski Theorem *} + +theory Lfp +imports Set +uses "subset.ML" "equalities.ML" "mono.ML" +begin + +constdefs + lfp :: "['a set=>'a set] => 'a set" (*least fixed point*) + "lfp(f) == Inter({u. f(u) <= u})" + +ML {* use_legacy_bindings (the_context ()) *} + end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ROOT.ML Sat Sep 17 17:35:26 2005 +0200 @@ -3,39 +3,18 @@ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Adds Classical Computational Logic to a database containing First-Order Logic. +Classical Computational Logic based on First-Order Logic. *) val banner = "Classical Computational Logic (in FOL)"; writeln banner; -print_depth 1; set eta_contract; -(* Higher-Order Set Theory Extension to FOL *) -(* used as basis for CCL *) - -use_thy "Set"; -use "subset.ML"; -use "equalities.ML"; -use "mono.ML"; -use_thy "Lfp"; -use_thy "Gfp"; - (* CCL - a computational logic for an untyped functional language *) (* with evaluation to weak head-normal form *) use_thy "CCL"; -use_thy "Term"; -use_thy "Type"; -use "coinduction.ML"; use_thy "Hered"; - -use_thy "Trancl"; use_thy "Wfd"; -use "genrec.ML"; -use "typecheck.ML"; -use "eval.ML"; use_thy "Fix"; - -print_depth 8; diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Set.ML --- a/src/CCL/Set.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Set.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,47 +1,36 @@ -(* Title: set/set +(* Title: Set/Set.ML ID: $Id$ - -For set.thy. - -Modified version of - Title: HOL/set - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -For set.thy. Set theory for higher-order logic. A set is simply a predicate. *) -open Set; - -val [prem] = goal Set.thy "[| P(a) |] ==> a : {x. P(x)}"; +val [prem] = goal (the_context ()) "[| P(a) |] ==> a : {x. P(x)}"; by (rtac (mem_Collect_iff RS iffD2) 1); by (rtac prem 1); qed "CollectI"; -val prems = goal Set.thy "[| a : {x. P(x)} |] ==> P(a)"; +val prems = goal (the_context ()) "[| a : {x. P(x)} |] ==> P(a)"; by (resolve_tac (prems RL [mem_Collect_iff RS iffD1]) 1); qed "CollectD"; val CollectE = make_elim CollectD; -val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B"; +val [prem] = goal (the_context ()) "[| !!x. x:A <-> x:B |] ==> A = B"; by (rtac (set_extension RS iffD2) 1); by (rtac (prem RS allI) 1); qed "set_ext"; (*** Bounded quantifiers ***) -val prems = goalw Set.thy [Ball_def] +val prems = goalw (the_context ()) [Ball_def] "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"; by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); qed "ballI"; -val [major,minor] = goalw Set.thy [Ball_def] +val [major,minor] = goalw (the_context ()) [Ball_def] "[| ALL x:A. P(x); x:A |] ==> P(x)"; by (rtac (minor RS (major RS spec RS mp)) 1); qed "bspec"; -val major::prems = goalw Set.thy [Ball_def] +val major::prems = goalw (the_context ()) [Ball_def] "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"; by (rtac (major RS spec RS impCE) 1); by (REPEAT (eresolve_tac prems 1)); @@ -50,32 +39,32 @@ (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*) fun ball_tac i = etac ballE i THEN contr_tac (i+1); -val prems = goalw Set.thy [Bex_def] +val prems = goalw (the_context ()) [Bex_def] "[| P(x); x:A |] ==> EX x:A. P(x)"; by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)); qed "bexI"; -qed_goal "bexCI" Set.thy +qed_goal "bexCI" (the_context ()) "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A. P(x)" (fn prems=> [ (rtac classical 1), (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); -val major::prems = goalw Set.thy [Bex_def] +val major::prems = goalw (the_context ()) [Bex_def] "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; by (rtac (major RS exE) 1); by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); qed "bexE"; (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) -val prems = goal Set.thy +val prems = goal (the_context ()) "(ALL x:A. True) <-> True"; by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); qed "ball_rew"; (** Congruence rules **) -val prems = goal Set.thy +val prems = goal (the_context ()) "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \ \ (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"; by (resolve_tac (prems RL [ssubst,iffD2]) 1); @@ -83,7 +72,7 @@ ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1)); qed "ball_cong"; -val prems = goal Set.thy +val prems = goal (the_context ()) "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \ \ (EX x:A. P(x)) <-> (EX x:A'. P'(x))"; by (resolve_tac (prems RL [ssubst,iffD2]) 1); @@ -93,18 +82,18 @@ (*** Rules for subsets ***) -val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; +val prems = goalw (the_context ()) [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; by (REPEAT (ares_tac (prems @ [ballI]) 1)); qed "subsetI"; (*Rule in Modus Ponens style*) -val major::prems = goalw Set.thy [subset_def] "[| A <= B; c:A |] ==> c:B"; +val major::prems = goalw (the_context ()) [subset_def] "[| A <= B; c:A |] ==> c:B"; by (rtac (major RS bspec) 1); by (resolve_tac prems 1); qed "subsetD"; (*Classical elimination rule*) -val major::prems = goalw Set.thy [subset_def] +val major::prems = goalw (the_context ()) [subset_def] "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P"; by (rtac (major RS ballE) 1); by (REPEAT (eresolve_tac prems 1)); @@ -113,7 +102,7 @@ (*Takes assumptions A<=B; c:A and creates the assumption c:B *) fun set_mp_tac i = etac subsetCE i THEN mp_tac i; -qed_goal "subset_refl" Set.thy "A <= A" +qed_goal "subset_refl" (the_context ()) "A <= A" (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]); Goal "[| A<=B; B<=C |] ==> A<=C"; @@ -125,30 +114,30 @@ (*** Rules for equality ***) (*Anti-symmetry of the subset relation*) -val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = B"; +val prems = goal (the_context ()) "[| A <= B; B <= A |] ==> A = B"; by (rtac (iffI RS set_ext) 1); by (REPEAT (ares_tac (prems RL [subsetD]) 1)); qed "subset_antisym"; val equalityI = subset_antisym; (* Equality rules from ZF set theory -- are they appropriate here? *) -val prems = goal Set.thy "A = B ==> A<=B"; +val prems = goal (the_context ()) "A = B ==> A<=B"; by (resolve_tac (prems RL [subst]) 1); by (rtac subset_refl 1); qed "equalityD1"; -val prems = goal Set.thy "A = B ==> B<=A"; +val prems = goal (the_context ()) "A = B ==> B<=A"; by (resolve_tac (prems RL [subst]) 1); by (rtac subset_refl 1); qed "equalityD2"; -val prems = goal Set.thy +val prems = goal (the_context ()) "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"; by (resolve_tac prems 1); by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); qed "equalityE"; -val major::prems = goal Set.thy +val major::prems = goal (the_context ()) "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"; by (rtac (major RS equalityE) 1); by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); @@ -157,7 +146,7 @@ (*Lemma for creating induction formulae -- for "pattern matching" on p To make the induction hypotheses usable, apply "spec" or "bspec" to put universal quantifiers over the free variables in p. *) -val prems = goal Set.thy +val prems = goal (the_context ()) "[| p:A; !!z. z:A ==> p=z --> R |] ==> R"; by (rtac mp 1); by (REPEAT (resolve_tac (refl::prems) 1)); @@ -169,22 +158,22 @@ (*** Rules for binary union -- Un ***) -val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B"; +val prems = goalw (the_context ()) [Un_def] "c:A ==> c : A Un B"; by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1)); qed "UnI1"; -val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B"; +val prems = goalw (the_context ()) [Un_def] "c:B ==> c : A Un B"; by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1)); qed "UnI2"; (*Classical introduction rule: no commitment to A vs B*) -qed_goal "UnCI" Set.thy "(~c:B ==> c:A) ==> c : A Un B" +qed_goal "UnCI" (the_context ()) "(~c:B ==> c:A) ==> c : A Un B" (fn prems=> [ (rtac classical 1), (REPEAT (ares_tac (prems@[UnI1,notI]) 1)), (REPEAT (ares_tac (prems@[UnI2,notE]) 1)) ]); -val major::prems = goalw Set.thy [Un_def] +val major::prems = goalw (the_context ()) [Un_def] "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; by (rtac (major RS CollectD RS disjE) 1); by (REPEAT (eresolve_tac prems 1)); @@ -193,20 +182,20 @@ (*** Rules for small intersection -- Int ***) -val prems = goalw Set.thy [Int_def] +val prems = goalw (the_context ()) [Int_def] "[| c:A; c:B |] ==> c : A Int B"; by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)); qed "IntI"; -val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:A"; +val [major] = goalw (the_context ()) [Int_def] "c : A Int B ==> c:A"; by (rtac (major RS CollectD RS conjunct1) 1); qed "IntD1"; -val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:B"; +val [major] = goalw (the_context ()) [Int_def] "c : A Int B ==> c:B"; by (rtac (major RS CollectD RS conjunct2) 1); qed "IntD2"; -val [major,minor] = goal Set.thy +val [major,minor] = goal (the_context ()) "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; by (rtac minor 1); by (rtac (major RS IntD1) 1); @@ -216,7 +205,7 @@ (*** Rules for set complement -- Compl ***) -val prems = goalw Set.thy [Compl_def] +val prems = goalw (the_context ()) [Compl_def] "[| c:A ==> False |] ==> c : Compl(A)"; by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); qed "ComplI"; @@ -224,7 +213,7 @@ (*This form, with negated conclusion, works well with the Classical prover. Negated assumptions behave like formulae on the right side of the notional turnstile...*) -val major::prems = goalw Set.thy [Compl_def] +val major::prems = goalw (the_context ()) [Compl_def] "[| c : Compl(A) |] ==> ~c:A"; by (rtac (major RS CollectD) 1); qed "ComplD"; @@ -238,13 +227,13 @@ by (rtac refl 1); qed "empty_eq"; -val [prem] = goalw Set.thy [empty_def] "a : {} ==> P"; +val [prem] = goalw (the_context ()) [empty_def] "a : {} ==> P"; by (rtac (prem RS CollectD RS FalseE) 1); qed "emptyD"; val emptyE = make_elim emptyD; -val [prem] = goal Set.thy "~ A={} ==> (EX x. x:A)"; +val [prem] = goal (the_context ()) "~ A={} ==> (EX x. x:A)"; by (rtac (prem RS swap) 1); by (rtac equalityI 1); by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD]))); @@ -257,7 +246,7 @@ by (rtac refl 1); qed "singletonI"; -val [major] = goalw Set.thy [singleton_def] "b : {a} ==> b=a"; +val [major] = goalw (the_context ()) [singleton_def] "b : {a} ==> b=a"; by (rtac (major RS CollectD) 1); qed "singletonD"; @@ -266,46 +255,46 @@ (*** Unions of families ***) (*The order of the premises presupposes that A is rigid; b may be flexible*) -val prems = goalw Set.thy [UNION_def] +val prems = goalw (the_context ()) [UNION_def] "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))"; by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1)); qed "UN_I"; -val major::prems = goalw Set.thy [UNION_def] +val major::prems = goalw (the_context ()) [UNION_def] "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R"; by (rtac (major RS CollectD RS bexE) 1); by (REPEAT (ares_tac prems 1)); qed "UN_E"; -val prems = goal Set.thy +val prems = goal (the_context ()) "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ \ (UN x:A. C(x)) = (UN x:B. D(x))"; by (REPEAT (etac UN_E 1 - ORELSE ares_tac ([UN_I,equalityI,subsetI] @ + ORELSE ares_tac ([UN_I,equalityI,subsetI] @ (prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); qed "UN_cong"; (*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *) -val prems = goalw Set.thy [INTER_def] +val prems = goalw (the_context ()) [INTER_def] "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); qed "INT_I"; -val major::prems = goalw Set.thy [INTER_def] +val major::prems = goalw (the_context ()) [INTER_def] "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)"; by (rtac (major RS CollectD RS bspec) 1); by (resolve_tac prems 1); qed "INT_D"; (*"Classical" elimination rule -- does not require proving X:C *) -val major::prems = goalw Set.thy [INTER_def] +val major::prems = goalw (the_context ()) [INTER_def] "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R"; by (rtac (major RS CollectD RS ballE) 1); by (REPEAT (eresolve_tac prems 1)); qed "INT_E"; -val prems = goal Set.thy +val prems = goal (the_context ()) "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ \ (INT x:A. C(x)) = (INT x:B. D(x))"; by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); @@ -316,12 +305,12 @@ (*** Rules for Unions ***) (*The order of the premises presupposes that C is rigid; A may be flexible*) -val prems = goalw Set.thy [Union_def] +val prems = goalw (the_context ()) [Union_def] "[| X:C; A:X |] ==> A : Union(C)"; by (REPEAT (resolve_tac (prems @ [UN_I]) 1)); qed "UnionI"; -val major::prems = goalw Set.thy [Union_def] +val major::prems = goalw (the_context ()) [Union_def] "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R"; by (rtac (major RS UN_E) 1); by (REPEAT (ares_tac prems 1)); @@ -329,21 +318,21 @@ (*** Rules for Inter ***) -val prems = goalw Set.thy [Inter_def] +val prems = goalw (the_context ()) [Inter_def] "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"; by (REPEAT (ares_tac ([INT_I] @ prems) 1)); qed "InterI"; (*A "destruct" rule -- every X in C contains A as an element, but A:X can hold when X:C does not! This rule is analogous to "spec". *) -val major::prems = goalw Set.thy [Inter_def] +val major::prems = goalw (the_context ()) [Inter_def] "[| A : Inter(C); X:C |] ==> A:X"; by (rtac (major RS INT_D) 1); by (resolve_tac prems 1); qed "InterD"; (*"Classical" elimination rule -- does not require proving X:C *) -val major::prems = goalw Set.thy [Inter_def] +val major::prems = goalw (the_context ()) [Inter_def] "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R"; by (rtac (major RS INT_E) 1); by (REPEAT (eresolve_tac prems 1)); diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Set.thy --- a/src/CCL/Set.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Set.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,28 +1,29 @@ -(* Title: CCL/set.thy +(* Title: CCL/Set.thy ID: $Id$ - -Modified version of HOL/set.thy that extends FOL - *) -Set = FOL + +header {* Extending FOL by a modified version of HOL set theory *} + +theory Set +imports FOL +begin global -types - 'a set - -arities - set :: (term) term +typedecl 'a set +arities set :: ("term") "term" consts Collect :: "['a => o] => 'a set" (*comprehension*) Compl :: "('a set) => 'a set" (*complement*) Int :: "['a set, 'a set] => 'a set" (infixl 70) Un :: "['a set, 'a set] => 'a set" (infixl 65) - Union, Inter :: "(('a set)set) => 'a set" (*...of a set*) - UNION, INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) - Ball, Bex :: "['a set, 'a => o] => o" (*bounded quants*) + Union :: "(('a set)set) => 'a set" (*...of a set*) + Inter :: "(('a set)set) => 'a set" (*...of a set*) + UNION :: "['a set, 'a => 'b set] => 'b set" (*general*) + INTER :: "['a set, 'a => 'b set] => 'b set" (*general*) + Ball :: "['a set, 'a => o] => o" (*bounded quants*) + Bex :: "['a set, 'a => o] => o" (*bounded quants*) mono :: "['a set => 'b set] => o" (*monotonicity*) ":" :: "['a, 'a set] => o" (infixl 50) (*membership*) "<=" :: "['a set, 'a set] => o" (infixl 50) @@ -43,7 +44,6 @@ "@Ball" :: "[idt, 'a set, o] => o" ("(ALL _:_./ _)" [0, 0, 0] 10) "@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10) - translations "{x. P}" == "Collect(%x. P)" "INT x:A. B" == "INTER(A, %x. B)" @@ -53,23 +53,26 @@ local -rules - mem_Collect_iff "(a : {x. P(x)}) <-> P(a)" - set_extension "A=B <-> (ALL x. x:A <-> x:B)" +axioms + mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)" + set_extension: "A=B <-> (ALL x. x:A <-> x:B)" - Ball_def "Ball(A, P) == ALL x. x:A --> P(x)" - Bex_def "Bex(A, P) == EX x. x:A & P(x)" - mono_def "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))" - subset_def "A <= B == ALL x:A. x:B" - singleton_def "{a} == {x. x=a}" - empty_def "{} == {x. False}" - Un_def "A Un B == {x. x:A | x:B}" - Int_def "A Int B == {x. x:A & x:B}" - Compl_def "Compl(A) == {x. ~x:A}" - INTER_def "INTER(A, B) == {y. ALL x:A. y: B(x)}" - UNION_def "UNION(A, B) == {y. EX x:A. y: B(x)}" - Inter_def "Inter(S) == (INT x:S. x)" - Union_def "Union(S) == (UN x:S. x)" +defs + Ball_def: "Ball(A, P) == ALL x. x:A --> P(x)" + Bex_def: "Bex(A, P) == EX x. x:A & P(x)" + mono_def: "mono(f) == (ALL A B. A <= B --> f(A) <= f(B))" + subset_def: "A <= B == ALL x:A. x:B" + singleton_def: "{a} == {x. x=a}" + empty_def: "{} == {x. False}" + Un_def: "A Un B == {x. x:A | x:B}" + Int_def: "A Int B == {x. x:A & x:B}" + Compl_def: "Compl(A) == {x. ~x:A}" + INTER_def: "INTER(A, B) == {y. ALL x:A. y: B(x)}" + UNION_def: "UNION(A, B) == {y. EX x:A. y: B(x)}" + Inter_def: "Inter(S) == (INT x:S. x)" + Union_def: "Union(S) == (UN x:S. x)" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Term.ML --- a/src/CCL/Term.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Term.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,13 +1,9 @@ -(* Title: CCL/terms +(* Title: CCL/Term.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -For terms.thy. *) -open Term; - val simp_can_defs = [one_def,inl_def,inr_def]; val simp_ncan_defs = [if_def,when_def,split_def,fst_def,snd_def,thd_def]; val simp_defs = simp_can_defs @ simp_ncan_defs; @@ -49,19 +45,19 @@ Goalw [letrec_def] "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))"; -by (resolve_tac [fixB RS ssubst] 1 THEN +by (resolve_tac [fixB RS ssubst] 1 THEN resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1); qed "letrecB"; val rawBs = caseBs @ [applyB,applyBbot]; -fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s +fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s (fn _ => [stac letrecB 1, simp_tac (CCL_ss addsimps rawBs) 1]); fun mk_beta_rl s = raw_mk_beta_rl data_defs s; -fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s - (fn _ => [simp_tac (CCL_ss addsimps rawBs +fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s + (fn _ => [simp_tac (CCL_ss addsimps rawBs setloop (stac letrecB)) 1]); fun mk_beta_rl s = raw_mk_beta_rl data_defs s; @@ -115,7 +111,7 @@ (*** Constructors are injective ***) -val term_injs = map (mk_inj_rl Term.thy +val term_injs = map (mk_inj_rl (the_context ()) [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons]) ["(inl(a) = inl(a')) <-> (a=a')", "(inr(a) = inr(a')) <-> (a=a')", @@ -124,13 +120,13 @@ (*** Constructors are distinct ***) -val term_dstncts = mkall_dstnct_thms Term.thy data_defs (ccl_injs @ term_injs) +val term_dstncts = mkall_dstnct_thms (the_context ()) data_defs (ccl_injs @ term_injs) [["bot","inl","inr"],["bot","zero","succ"],["bot","nil","op $"]]; (*** Rules for pre-order [= ***) local - fun mk_thm s = prove_goalw Term.thy data_defs s (fn _ => + fun mk_thm s = prove_goalw (the_context ()) data_defs s (fn _ => [simp_tac (ccl_ss addsimps (ccl_porews)) 1]); in val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'", @@ -144,5 +140,5 @@ val term_rews = termBs @ term_injs @ term_dstncts @ ccl_porews @ term_porews; val term_ss = ccl_ss addsimps term_rews; -val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) +val term_cs = ccl_cs addSEs (term_dstncts RL [notE]) addSDs (XH_to_Ds term_injs); diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Term.thy --- a/src/CCL/Term.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Term.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,13 +1,14 @@ -(* Title: CCL/terms.thy +(* Title: CCL/Term.thy ID: $Id$ Author: Martin Coen Copyright 1993 University of Cambridge - -Definitions of usual program constructs in CCL. - *) -Term = CCL + +header {* Definitions of usual program constructs in CCL *} + +theory Term +imports CCL +begin consts @@ -15,11 +16,13 @@ if :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60) - inl,inr :: "i=>i" - when :: "[i,i=>i,i=>i]=>i" + inl :: "i=>i" + inr :: "i=>i" + when :: "[i,i=>i,i=>i]=>i" split :: "[i,[i,i]=>i]=>i" - fst,snd, + fst :: "i=>i" + snd :: "i=>i" thd :: "i=>i" zero :: "i" @@ -32,10 +35,10 @@ lcase :: "[i,i,[i,i]=>i]=>i" lrec :: "[i,i,[i,i,i]=>i]=>i" - let :: "[i,i=>i]=>i" + "let" :: "[i,i=>i]=>i" letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" - letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" + letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" syntax "@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" @@ -50,47 +53,7 @@ "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) -consts - napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) - -rules - - one_def "one == true" - if_def "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" - inl_def "inl(a) == " - inr_def "inr(b) == " - when_def "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))" - split_def "split(t,f) == case(t,bot,bot,f,%u. bot)" - fst_def "fst(t) == split(t,%x y. x)" - snd_def "snd(t) == split(t,%x y. y)" - thd_def "thd(t) == split(t,%x p. split(p,%y z. z))" - zero_def "zero == inl(one)" - succ_def "succ(n) == inr(n)" - ncase_def "ncase(n,b,c) == when(n,%x. b,%y. c(y))" - nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)" - nil_def "[] == inl(one)" - cons_def "h$t == inr()" - lcase_def "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))" - lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)" - - let_def "let x be t in f(x) == case(t,f(true),f(false),%x y. f(),%u. f(lam x. u(x)))" - letrec_def - "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)" - - letrec2_def "letrec g x y be h(x,y,g) in f(g)== - letrec g' p be split(p,%x y. h(x,y,%u v. g'())) - in f(%x y. g'())" - - letrec3_def "letrec g x y z be h(x,y,z,g) in f(g) == - letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(>)))) - in f(%x y z. g'(>))" - - napply_def "f ^n` a == nrec(n,a,%x g. f(g))" - -end - -ML - +ML {* (** Quantifier translations: variable binding **) (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *) @@ -100,11 +63,11 @@ let val (id',b') = variant_abs(id,T,b) in Const("@let",dummyT) $ Free(id',T) $ a $ b' end; -fun letrec_tr [Free(f,S),Free(x,T),a,b] = +fun letrec_tr [Free(f,S),Free(x,T),a,b] = Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b); -fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = +fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b); -fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = +fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b); fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = @@ -128,15 +91,57 @@ in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' end; -val parse_translation= - [("@let", let_tr), - ("@letrec", letrec_tr), - ("@letrec2", letrec2_tr), - ("@letrec3", letrec3_tr) - ]; -val print_translation= - [("let", let_tr'), - ("letrec", letrec_tr'), - ("letrec2", letrec2_tr'), - ("letrec3", letrec3_tr') - ]; +*} + +parse_translation {* + [("@let", let_tr), + ("@letrec", letrec_tr), + ("@letrec2", letrec2_tr), + ("@letrec3", letrec3_tr)] *} + +print_translation {* + [("let", let_tr'), + ("letrec", letrec_tr'), + ("letrec2", letrec2_tr'), + ("letrec3", letrec3_tr')] *} + +consts + napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) + +axioms + + one_def: "one == true" + if_def: "if b then t else u == case(b,t,u,% x y. bot,%v. bot)" + inl_def: "inl(a) == " + inr_def: "inr(b) == " + when_def: "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))" + split_def: "split(t,f) == case(t,bot,bot,f,%u. bot)" + fst_def: "fst(t) == split(t,%x y. x)" + snd_def: "snd(t) == split(t,%x y. y)" + thd_def: "thd(t) == split(t,%x p. split(p,%y z. z))" + zero_def: "zero == inl(one)" + succ_def: "succ(n) == inr(n)" + ncase_def: "ncase(n,b,c) == when(n,%x. b,%y. c(y))" + nrec_def: " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)" + nil_def: "[] == inl(one)" + cons_def: "h$t == inr()" + lcase_def: "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))" + lrec_def: "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)" + + let_def: "let x be t in f(x) == case(t,f(true),f(false),%x y. f(),%u. f(lam x. u(x)))" + letrec_def: + "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)" + + letrec2_def: "letrec g x y be h(x,y,g) in f(g)== + letrec g' p be split(p,%x y. h(x,y,%u v. g'())) + in f(%x y. g'())" + + letrec3_def: "letrec g x y z be h(x,y,z,g) in f(g) == + letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(>)))) + in f(%x y z. g'(>))" + + napply_def: "f ^n` a == nrec(n,a,%x g. f(g))" + +ML {* use_legacy_bindings (the_context ()) *} + +end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Trancl.ML --- a/src/CCL/Trancl.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Trancl.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,25 +1,15 @@ -(* Title: CCL/trancl +(* Title: CCL/Trancl.ML ID: $Id$ - -For trancl.thy. - -Modified version of - Title: HOL/trancl.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - *) -open Trancl; - (** Natural deduction for trans(r) **) -val prems = goalw Trancl.thy [trans_def] +val prems = goalw (the_context ()) [trans_def] "(!! x y z. [| :r; :r |] ==> :r) ==> trans(r)"; by (REPEAT (ares_tac (prems@[allI,impI]) 1)); qed "transI"; -val major::prems = goalw Trancl.thy [trans_def] +val major::prems = goalw (the_context ()) [trans_def] "[| trans(r); :r; :r |] ==> :r"; by (cut_facts_tac [major] 1); by (fast_tac (FOL_cs addIs prems) 1); @@ -27,15 +17,15 @@ (** Identity relation **) -Goalw [id_def] " : id"; +Goalw [id_def] " : id"; by (rtac CollectI 1); by (rtac exI 1); by (rtac refl 1); qed "idI"; -val major::prems = goalw Trancl.thy [id_def] +val major::prems = goalw (the_context ()) [id_def] "[| p: id; !!x.[| p = |] ==> P \ -\ |] ==> P"; +\ |] ==> P"; by (rtac (major RS CollectE) 1); by (etac exE 1); by (eresolve_tac prems 1); @@ -43,13 +33,13 @@ (** Composition of two relations **) -val prems = goalw Trancl.thy [comp_def] +val prems = goalw (the_context ()) [comp_def] "[| :s; :r |] ==> : 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] +val prems = goalw (the_context ()) [comp_def] "[| xz : r O s; \ \ !!x y z. [| xz = ; :s; :r |] ==> P \ \ |] ==> P"; @@ -57,7 +47,7 @@ by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1)); qed "compE"; -val prems = goal Trancl.thy +val prems = goal (the_context ()) "[| : r O s; \ \ !!y. [| :s; :r |] ==> P \ \ |] ==> P"; @@ -65,11 +55,11 @@ by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [pair_inject,ssubst] 1)); qed "compEpair"; -val comp_cs = set_cs addIs [compI,idI] - addEs [compE,idE] +val comp_cs = set_cs addIs [compI,idI] + addEs [compE,idE] addSEs [pair_inject]; -val prems = goal Trancl.thy +val prems = goal (the_context ()) "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; by (cut_facts_tac prems 1); by (fast_tac comp_cs 1); @@ -91,14 +81,14 @@ qed "rtrancl_refl"; (*Closure under composition with r*) -val prems = goal Trancl.thy +val prems = goal (the_context ()) "[| : r^*; : r |] ==> : 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 (the_context ()) "[| : r |] ==> : r^*"; by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1); by (rtac prem 1); qed "r_into_rtrancl"; @@ -106,7 +96,7 @@ (** standard induction rule **) -val major::prems = goal Trancl.thy +val major::prems = goal (the_context ()) "[| : r^*; \ \ !!x. P(); \ \ !!x y z.[| P(); : r^*; : r |] ==> P() |] \ @@ -117,7 +107,7 @@ qed "rtrancl_full_induct"; (*nice induction rule*) -val major::prems = goal Trancl.thy +val major::prems = goal (the_context ()) "[| : r^*; \ \ P(a); \ \ !!y z.[| : r^*; : r; P(y) |] ==> P(z) |] \ @@ -140,7 +130,7 @@ qed "trans_rtrancl"; (*elimination of rtrancl -- by induction on a special formula*) -val major::prems = goal Trancl.thy +val major::prems = goal (the_context ()) "[| : r^*; (a = b) ==> P; \ \ !!y.[| : r^*; : r |] ==> P |] \ \ ==> P"; @@ -156,26 +146,26 @@ (** Conversions between trancl and rtrancl **) -val [major] = goalw Trancl.thy [trancl_def] +val [major] = goalw (the_context ()) [trancl_def] "[| : r^+ |] ==> : 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] +val [prem] = goalw (the_context ()) [trancl_def] "[| : r |] ==> : 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] +val prems = goalw (the_context ()) [trancl_def] "[| : r^*; : r |] ==> : r^+"; by (REPEAT (resolve_tac ([compI]@prems) 1)); qed "rtrancl_into_trancl1"; (*intro rule from r and rtrancl*) -val prems = goal Trancl.thy +val prems = goal (the_context ()) "[| : r; : r^* |] ==> : r^+"; by (resolve_tac (prems RL [rtranclE]) 1); by (etac subst 1); @@ -185,7 +175,7 @@ qed "rtrancl_into_trancl2"; (*elimination of r^+ -- NOT an induction rule*) -val major::prems = goal Trancl.thy +val major::prems = goal (the_context ()) "[| : r^+; \ \ : r ==> P; \ \ !!y.[| : r^+; : r |] ==> P \ @@ -207,7 +197,7 @@ by (REPEAT (assume_tac 1)); qed "trans_trancl"; -val prems = goal Trancl.thy +val prems = goal (the_context ()) "[| : r; : r^+ |] ==> : r^+"; by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1); by (resolve_tac prems 1); diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Trancl.thy --- a/src/CCL/Trancl.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Trancl.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,28 +1,31 @@ -(* Title: CCL/trancl.thy +(* Title: CCL/Trancl.thy ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -Transitive closure of a relation *) -Trancl = CCL + +header {* Transitive closure of a relation *} + +theory Trancl +imports CCL +begin consts - trans :: "i set => o" (*transitivity predicate*) - id :: "i set" - rtrancl :: "i set => i set" ("(_^*)" [100] 100) - trancl :: "i set => i set" ("(_^+)" [100] 100) - O :: "[i set,i set] => i set" (infixr 60) - -rules + trans :: "i set => o" (*transitivity predicate*) + id :: "i set" + rtrancl :: "i set => i set" ("(_^*)" [100] 100) + trancl :: "i set => i set" ("(_^+)" [100] 100) + O :: "[i set,i set] => i set" (infixr 60) -trans_def "trans(r) == (ALL x y z. :r --> :r --> :r)" -comp_def (*composition of relations*) - "r O s == {xz. EX x y z. xz = & :s & :r}" -id_def (*the identity relation*) - "id == {p. EX x. p = }" -rtrancl_def "r^* == lfp(%s. id Un (r O s))" -trancl_def "r^+ == r O rtrancl(r)" +axioms + trans_def: "trans(r) == (ALL x y z. :r --> :r --> :r)" + comp_def: (*composition of relations*) + "r O s == {xz. EX x y z. xz = & :s & :r}" + id_def: (*the identity relation*) + "id == {p. EX x. p = }" + rtrancl_def: "r^* == lfp(%s. id Un (r O s))" + trancl_def: "r^+ == r O rtrancl(r)" + +ML {* use_legacy_bindings (the_context ()) *} end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Type.ML --- a/src/CCL/Type.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Type.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,13 +1,9 @@ -(* Title: CCL/types +(* Title: CCL/Type.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge - -For types.thy. *) -open Type; - val simp_type_defs = [Subtype_def,Unit_def,Bool_def,Plus_def,Sigma_def,Pi_def, Lift_def,Tall_def,Tex_def]; val ind_type_defs = [Nat_def,List_def]; @@ -15,14 +11,14 @@ val simp_data_defs = [one_def,inl_def,inr_def]; val ind_data_defs = [zero_def,succ_def,nil_def,cons_def]; -goal Set.thy "A <= B <-> (ALL x. x:A --> x:B)"; +goal (the_context ()) "A <= B <-> (ALL x. x:A --> x:B)"; by (fast_tac set_cs 1); qed "subsetXH"; (*** Exhaustion Rules ***) fun mk_XH_tac thy defs rls s = prove_goalw thy defs s (fn _ => [cfast_tac rls 1]); -val XH_tac = mk_XH_tac Type.thy simp_type_defs []; +val XH_tac = mk_XH_tac (the_context ()) simp_type_defs []; val EmptyXH = XH_tac "a : {} <-> False"; val SubtypeXH = XH_tac "a : {x:A. P(x)} <-> (a:A & P(a))"; @@ -42,9 +38,9 @@ (*** Canonical Type Rules ***) -fun mk_canT_tac thy xhs s = prove_goal thy s +fun mk_canT_tac thy xhs s = prove_goal thy s (fn prems => [fast_tac (set_cs addIs (prems @ (xhs RL [iffD2]))) 1]); -val canT_tac = mk_canT_tac Type.thy XHs; +val canT_tac = mk_canT_tac (the_context ()) XHs; val oneT = canT_tac "one : Unit"; val trueT = canT_tac "true : Bool"; @@ -59,32 +55,32 @@ (*** Non-Canonical Type Rules ***) local -val lemma = prove_goal Type.thy "[| a:B(u); u=v |] ==> a : B(v)" +val lemma = prove_goal (the_context ()) "[| a:B(u); u=v |] ==> a : B(v)" (fn prems => [cfast_tac prems 1]); in -fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s +fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s (fn major::prems => [(resolve_tac ([major] RL top_crls) 1), (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), (ALLGOALS (asm_simp_tac term_ss)), - (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' + (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' etac bspec )), (safe_tac (ccl_cs addSIs prems))]); end; -val ncanT_tac = mk_ncanT_tac Type.thy [] case_rls case_rls; +val ncanT_tac = mk_ncanT_tac (the_context ()) [] case_rls case_rls; -val ifT = ncanT_tac +val ifT = ncanT_tac "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> \ \ if b then t else u : A(b)"; -val applyT = ncanT_tac +val applyT = ncanT_tac "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)"; -val splitT = ncanT_tac +val splitT = ncanT_tac "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p= |] ==> c(x,y):C() |] ==> \ \ split(p,c):C(p)"; -val whenT = ncanT_tac +val whenT = ncanT_tac "[| p:A+B; !!x.[| x:A; p=inl(x) |] ==> a(x):C(inl(x)); \ \ !!y.[| y:B; p=inr(y) |] ==> b(y):C(inr(y)) |] ==> \ \ when(p,a,b) : C(p)"; @@ -96,12 +92,12 @@ val SubtypeD1 = standard ((SubtypeXH RS iffD1) RS conjunct1); val SubtypeD2 = standard ((SubtypeXH RS iffD1) RS conjunct2); -val prems = goal Type.thy +val prems = goal (the_context ()) "[| a:A; P(a) |] ==> a : {x:A. P(x)}"; by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1)); qed "SubtypeI"; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q"; by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1)); qed "SubtypeE"; @@ -116,7 +112,7 @@ by (REPEAT (ares_tac [monoI,subset_refl] 1)); qed "constM"; -val major::prems = goal Type.thy +val major::prems = goal (the_context ()) "mono(%X. A(X)) ==> mono(%X.[A(X)])"; by (rtac (subsetI RS monoI) 1); by (dtac (LiftXH RS iffD1) 1); @@ -127,7 +123,7 @@ by (assume_tac 1); qed "LiftM"; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> \ \ mono(%X. Sigma(A(X),B(X)))"; by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE @@ -136,7 +132,7 @@ hyp_subst_tac 1)); qed "SgM"; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))"; by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE @@ -144,7 +140,7 @@ hyp_subst_tac 1)); qed "PiM"; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| mono(%X. A(X)); mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))"; by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE @@ -176,7 +172,7 @@ (*** Exhaustion Rules ***) -fun mk_iXH_tac teqs ddefs rls s = prove_goalw Type.thy ddefs s +fun mk_iXH_tac teqs ddefs rls s = prove_goalw (the_context ()) ddefs s (fn _ => [resolve_tac (teqs RL [XHlemma1]) 1, fast_tac (set_cs addSIs canTs addSEs case_rls) 1]); @@ -192,8 +188,8 @@ (*** Type Rules ***) -val icanT_tac = mk_canT_tac Type.thy iXHs; -val incanT_tac = mk_ncanT_tac Type.thy [] icase_rls case_rls; +val icanT_tac = mk_canT_tac (the_context ()) iXHs; +val incanT_tac = mk_ncanT_tac (the_context ()) [] icase_rls case_rls; val zeroT = icanT_tac "zero : Nat"; val succT = icanT_tac "n:Nat ==> succ(n) : Nat"; @@ -202,7 +198,7 @@ val icanTs = [zeroT,succT,nilT,consT]; -val ncaseT = incanT_tac +val ncaseT = incanT_tac "[| n:Nat; n=zero ==> b:C(zero); \ \ !!x.[| x:Nat; n=succ(x) |] ==> c(x):C(succ(x)) |] ==> \ \ ncase(n,b,c) : C(n)"; @@ -218,7 +214,7 @@ val ind_Ms = [NatM,ListM]; -fun mk_ind_tac ddefs tdefs Ms canTs case_rls s = prove_goalw Type.thy ddefs s +fun mk_ind_tac ddefs tdefs Ms canTs case_rls s = prove_goalw (the_context ()) ddefs s (fn major::prems => [resolve_tac (Ms RL ([major] RL (tdefs RL [def_induct]))) 1, fast_tac (set_cs addSIs (prems @ canTs) addSEs case_rls) 1]); @@ -237,7 +233,7 @@ (*** Primitive Recursive Rules ***) -fun mk_prec_tac inds s = prove_goal Type.thy s +fun mk_prec_tac inds s = prove_goal (the_context ()) s (fn major::prems => [resolve_tac ([major] RL inds) 1, ALLGOALS (simp_tac term_ss THEN' fast_tac (set_cs addSIs prems))]); @@ -258,7 +254,7 @@ (*** Theorem proving ***) -val [major,minor] = goal Type.thy +val [major,minor] = goal (the_context ()) "[| : Sigma(A,B); [| a:A; b:B(a) |] ==> P \ \ |] ==> P"; by (rtac (major RS (XH_to_E SgXH)) 1); @@ -276,13 +272,13 @@ (*** Infinite Data Types ***) -val [mono] = goal Type.thy "mono(f) ==> lfp(f) <= gfp(f)"; +val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) <= gfp(f)"; by (rtac (lfp_lowerbound RS subset_trans) 1); by (rtac (mono RS gfp_lemma3) 1); by (rtac subset_refl 1); qed "lfp_subset_gfp"; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \ \ t(a) : gfp(B)"; by (rtac coinduct 1); @@ -290,7 +286,7 @@ by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); qed "gfpI"; -val rew::prem::prems = goal Type.thy +val rew::prem::prems = goal (the_context ()) "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \ \ t(a) : C"; by (rewtac rew); @@ -299,7 +295,7 @@ (* EG *) -val prems = goal Type.thy +val prems = goal (the_context ()) "letrec g x be zero$g(x) in g(bot) : Lists(Nat)"; by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1); by (stac letrecB 1); diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Type.thy --- a/src/CCL/Type.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Type.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,13 +1,14 @@ -(* Title: CCL/types.thy +(* Title: CCL/Type.thy ID: $Id$ Author: Martin Coen Copyright 1993 University of Cambridge - -Types in CCL are defined as sets of terms. - *) -Type = Term + +header {* Types in CCL are defined as sets of terms *} + +theory Type +imports Term +begin consts @@ -33,7 +34,7 @@ "@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" [0,0,60] 60) - + "@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53) "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) "@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") @@ -45,32 +46,29 @@ "A * B" => "Sigma(A, _K(B))" "{x: A. B}" == "Subtype(A, %x. B)" -rules +print_translation {* + [("Pi", dependent_tr' ("@Pi", "@->")), + ("Sigma", dependent_tr' ("@Sigma", "@*"))] *} - Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}" - Unit_def "Unit == {x. x=one}" - Bool_def "Bool == {x. x=true | x=false}" - Plus_def "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" - Pi_def "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" - Sigma_def "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=}" - Nat_def "Nat == lfp(% X. Unit + X)" - List_def "List(A) == lfp(% X. Unit + A*X)" +axioms + Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" + Unit_def: "Unit == {x. x=one}" + Bool_def: "Bool == {x. x=true | x=false}" + Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" + Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" + Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=}" + Nat_def: "Nat == lfp(% X. Unit + X)" + List_def: "List(A) == lfp(% X. Unit + A*X)" - Lists_def "Lists(A) == gfp(% X. Unit + A*X)" - ILists_def "ILists(A) == gfp(% X.{} + A*X)" + Lists_def: "Lists(A) == gfp(% X. Unit + A*X)" + ILists_def: "ILists(A) == gfp(% X.{} + A*X)" - Tall_def "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" - Tex_def "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" - Lift_def "[A] == A Un {bot}" + Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" + Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" + Lift_def: "[A] == A Un {bot}" - SPLIT_def "SPLIT(p,B) == Union({A. EX x y. p= & A=B(x,y)})" + SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p= & A=B(x,y)})" + +ML {* use_legacy_bindings (the_context ()) *} end - - -ML - -val print_translation = - [("Pi", dependent_tr' ("@Pi", "@->")), - ("Sigma", dependent_tr' ("@Sigma", "@*"))]; - diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Wfd.ML --- a/src/CCL/Wfd.ML Sat Sep 17 14:02:31 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,204 +0,0 @@ -(* Title: CCL/wfd.ML - ID: $Id$ - -For wfd.thy. - -Based on - Titles: ZF/wf.ML and HOL/ex/lex-prod - Authors: Lawrence C Paulson and Tobias Nipkow - Copyright 1992 University of Cambridge - -*) - -open Wfd; - -(***********) - -val [major,prem] = goalw Wfd.thy [Wfd_def] - "[| Wfd(R); \ -\ !!x.[| ALL y. : R --> P(y) |] ==> P(x) |] ==> \ -\ P(a)"; -by (rtac (major RS spec RS mp RS spec RS CollectD) 1); -by (fast_tac (set_cs addSIs [prem RS CollectI]) 1); -qed "wfd_induct"; - -val [p1,p2,p3] = goal Wfd.thy - "[| !!x y. : R ==> Q(x); \ -\ ALL x. (ALL y. : R --> y : P) --> x : P; \ -\ !!x. Q(x) ==> x:P |] ==> a:P"; -by (rtac (p2 RS spec RS mp) 1); -by (fast_tac (set_cs addSIs [p1 RS p3]) 1); -qed "wfd_strengthen_lemma"; - -fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN - assume_tac (i+1); - -val wfd::prems = goal Wfd.thy "[| Wfd(r); :r; :r |] ==> P"; -by (subgoal_tac "ALL x. :r --> :r --> P" 1); -by (fast_tac (FOL_cs addIs prems) 1); -by (rtac (wfd RS wfd_induct) 1); -by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); -qed "wf_anti_sym"; - -val prems = goal Wfd.thy "[| Wfd(r); : r |] ==> P"; -by (rtac wf_anti_sym 1); -by (REPEAT (resolve_tac prems 1)); -qed "wf_anti_refl"; - -(*** Irreflexive transitive closure ***) - -val [prem] = goal Wfd.thy "Wfd(R) ==> Wfd(R^+)"; -by (rewtac Wfd_def); -by (REPEAT (ares_tac [allI,ballI,impI] 1)); -(*must retain the universal formula for later use!*) -by (rtac allE 1 THEN assume_tac 1); -by (etac mp 1); -by (rtac (prem RS wfd_induct) 1); -by (rtac (impI RS allI) 1); -by (etac tranclE 1); -by (fast_tac ccl_cs 1); -by (etac (spec RS mp RS spec RS mp) 1); -by (REPEAT (atac 1)); -qed "trancl_wf"; - -(*** Lexicographic Ordering ***) - -Goalw [lex_def] - "p : ra**rb <-> (EX a a' b b'. p = <,> & ( : ra | a=a' & : rb))"; -by (fast_tac ccl_cs 1); -qed "lexXH"; - -val prems = goal Wfd.thy - " : ra ==> <,> : ra**rb"; -by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1); -qed "lexI1"; - -val prems = goal Wfd.thy - " : rb ==> <,> : ra**rb"; -by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1); -qed "lexI2"; - -val major::prems = goal Wfd.thy - "[| p : ra**rb; \ -\ !!a a' b b'.[| : ra; p=<,> |] ==> R; \ -\ !!a b b'.[| : rb; p = <,> |] ==> R |] ==> \ -\ R"; -by (rtac (major RS (lexXH RS iffD1) RS exE) 1); -by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); -by (ALLGOALS (fast_tac ccl_cs)); -qed "lexE"; - -val [major,minor] = goal Wfd.thy - "[| p : r**s; !!a a' b b'. p = <,> ==> P |] ==>P"; -by (rtac (major RS lexE) 1); -by (ALLGOALS (fast_tac (set_cs addSEs [minor]))); -qed "lex_pair"; - -val [wfa,wfb] = goal Wfd.thy - "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)"; -by (rewtac Wfd_def); -by (safe_tac ccl_cs); -by (wfd_strengthen_tac "%x. EX a b. x=" 1); -by (fast_tac (term_cs addSEs [lex_pair]) 1); -by (subgoal_tac "ALL a b.:P" 1); -by (fast_tac ccl_cs 1); -by (rtac (wfa RS wfd_induct RS allI) 1); -by (rtac (wfb RS wfd_induct RS allI) 1);back(); -by (fast_tac (type_cs addSEs [lexE]) 1); -qed "lex_wf"; - -(*** Mapping ***) - -Goalw [wmap_def] - "p : wmap(f,r) <-> (EX x y. p= & : r)"; -by (fast_tac ccl_cs 1); -qed "wmapXH"; - -val prems = goal Wfd.thy - " : r ==> : wmap(f,r)"; -by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1); -qed "wmapI"; - -val major::prems = goal Wfd.thy - "[| p : wmap(f,r); !!a b.[| : r; p= |] ==> R |] ==> R"; -by (rtac (major RS (wmapXH RS iffD1) RS exE) 1); -by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); -by (ALLGOALS (fast_tac ccl_cs)); -qed "wmapE"; - -val [wf] = goal Wfd.thy - "Wfd(r) ==> Wfd(wmap(f,r))"; -by (rewtac Wfd_def); -by (safe_tac ccl_cs); -by (subgoal_tac "ALL b. ALL a. f(a)=b-->a:P" 1); -by (fast_tac ccl_cs 1); -by (rtac (wf RS wfd_induct RS allI) 1); -by (safe_tac ccl_cs); -by (etac (spec RS mp) 1); -by (safe_tac (ccl_cs addSEs [wmapE])); -by (etac (spec RS mp RS spec RS mp) 1); -by (assume_tac 1); -by (rtac refl 1); -qed "wmap_wf"; - -(* Projections *) - -val prems = goal Wfd.thy " : r ==> <,> : wmap(fst,r)"; -by (rtac wmapI 1); -by (simp_tac (term_ss addsimps prems) 1); -qed "wfstI"; - -val prems = goal Wfd.thy " : r ==> <,> : wmap(snd,r)"; -by (rtac wmapI 1); -by (simp_tac (term_ss addsimps prems) 1); -qed "wsndI"; - -val prems = goal Wfd.thy " : r ==> <>,>> : wmap(thd,r)"; -by (rtac wmapI 1); -by (simp_tac (term_ss addsimps prems) 1); -qed "wthdI"; - -(*** Ground well-founded relations ***) - -val prems = goalw Wfd.thy [wf_def] - "[| Wfd(r); a : r |] ==> a : wf(r)"; -by (fast_tac (set_cs addSIs prems) 1); -qed "wfI"; - -val prems = goalw Wfd.thy [Wfd_def] "Wfd({})"; -by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1); -qed "Empty_wf"; - -val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))"; -by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1); -by (ALLGOALS (asm_simp_tac CCL_ss)); -by (rtac Empty_wf 1); -qed "wf_wf"; - -Goalw [NatPR_def] "p : NatPR <-> (EX x:Nat. p=)"; -by (fast_tac set_cs 1); -qed "NatPRXH"; - -Goalw [ListPR_def] "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=)"; -by (fast_tac set_cs 1); -qed "ListPRXH"; - -val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2)); -val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2))); - -Goalw [Wfd_def] "Wfd(NatPR)"; -by (safe_tac set_cs); -by (wfd_strengthen_tac "%x. x:Nat" 1); -by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1); -by (etac Nat_ind 1); -by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH]))); -qed "NatPR_wf"; - -Goalw [Wfd_def] "Wfd(ListPR(A))"; -by (safe_tac set_cs); -by (wfd_strengthen_tac "%x. x:List(A)" 1); -by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1); -by (etac List_ind 1); -by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH]))); -qed "ListPR_wf"; - diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/Wfd.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,12 +1,15 @@ -(* Title: CCL/wfd.thy +(* Title: CCL/Wfd.thy ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -Well-founded relations in CCL. *) -Wfd = Trancl + Type + +header {* Well-founded relations in CCL *} + +theory Wfd +imports Trancl Type Hered +uses ("wfd.ML") ("genrec.ML") ("typecheck.ML") ("eval.ML") +begin consts (*** Predicates ***) @@ -18,17 +21,25 @@ NatPR :: "i set" ListPR :: "i set => i set" -rules +axioms - Wfd_def + Wfd_def: "Wfd(R) == ALL P.(ALL x.(ALL y. : R --> y:P) --> x:P) --> (ALL a. a:P)" - wf_def "wf(R) == {x. x:R & Wfd(R)}" + wf_def: "wf(R) == {x. x:R & Wfd(R)}" - wmap_def "wmap(f,R) == {p. EX x y. p= & : R}" - lex_def + wmap_def: "wmap(f,R) == {p. EX x y. p= & : R}" + lex_def: "ra**rb == {p. EX a a' b b'. p = <,> & ( : ra | (a=a' & : rb))}" - NatPR_def "NatPR == {p. EX x:Nat. p=}" - ListPR_def "ListPR(A) == {p. EX h:A. EX t:List(A). p=}" + NatPR_def: "NatPR == {p. EX x:Nat. p=}" + ListPR_def: "ListPR(A) == {p. EX h:A. EX t:List(A). p=}" + +ML {* use_legacy_bindings (the_context ()) *} + +use "wfd.ML" +use "genrec.ML" +use "typecheck.ML" +use "eval.ML" + end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/coinduction.ML --- a/src/CCL/coinduction.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/coinduction.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,4 +1,4 @@ -(* Title: 92/CCL/coinduction +(* Title: CCL/Coinduction.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -6,23 +6,23 @@ Lemmas and tactics for using the rule coinduct3 on [= and =. *) -val [mono,prem] = goal Lfp.thy "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)"; +val [mono,prem] = goal (the_context ()) "[| mono(f); a : f(lfp(f)) |] ==> a : lfp(f)"; by (stac (mono RS lfp_Tarski) 1); by (rtac prem 1); qed "lfpI"; -val prems = goal CCL.thy "[| a=a'; a' : A |] ==> a : A"; +val prems = goal (the_context ()) "[| a=a'; a' : A |] ==> a : A"; by (simp_tac (term_ss addsimps prems) 1); qed "ssubst_single"; -val prems = goal CCL.thy "[| a=a'; b=b'; : A |] ==> : A"; +val prems = goal (the_context ()) "[| a=a'; b=b'; : A |] ==> : A"; by (simp_tac (term_ss addsimps prems) 1); qed "ssubst_pair"; (***) -local -fun mk_thm s = prove_goal Term.thy s (fn mono::prems => +local +fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems => [fast_tac (term_cs addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1]); in val ci3_RI = mk_thm "[| mono(Agen); a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"; @@ -31,20 +31,20 @@ val ci3_AI = mk_thm "[| mono(Agen); a : A |] ==> a : lfp(%x. Agen(x) Un R Un A)"; end; -fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s +fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s (fn prems => [rtac (genXH RS iffD2) 1, (simp_tac term_ss 1), - TRY (fast_tac (term_cs addIs + TRY (fast_tac (term_cs addIs ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] @ prems)) 1)]); (** POgen **) -goal Term.thy " : PO"; +goal (the_context ()) " : PO"; by (rtac (po_refl RS (XH_to_D PO_iff)) 1); qed "PO_refl"; -val POgenIs = map (mk_genIs Term.thy data_defs POgenXH POgen_mono) +val POgenIs = map (mk_genIs (the_context ()) data_defs POgenXH POgen_mono) [" : POgen(R)", " : POgen(R)", "[| : R; : R |] ==> <,> : POgen(R)", @@ -65,16 +65,16 @@ fun POgen_tac (rla,rlb) i = SELECT_GOAL (safe_tac ccl_cs) i THEN rtac (rlb RS (rla RS ssubst_pair)) i THEN - (REPEAT (resolve_tac (POgenIs @ [PO_refl RS (POgen_mono RS ci3_AI)] @ + (REPEAT (resolve_tac (POgenIs @ [PO_refl RS (POgen_mono RS ci3_AI)] @ (POgenIs RL [POgen_mono RS ci3_AgenI]) @ [POgen_mono RS ci3_RI]) i)); (** EQgen **) -goal Term.thy " : EQ"; +goal (the_context ()) " : EQ"; by (rtac (refl RS (EQ_iff RS iffD1)) 1); qed "EQ_refl"; -val EQgenIs = map (mk_genIs Term.thy data_defs EQgenXH EQgen_mono) +val EQgenIs = map (mk_genIs (the_context ()) data_defs EQgenXH EQgen_mono) [" : EQgen(R)", " : EQgen(R)", "[| : R; : R |] ==> <,> : EQgen(R)", @@ -93,15 +93,15 @@ \ : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"]; fun EQgen_raw_tac i = - (REPEAT (resolve_tac (EQgenIs @ [EQ_refl RS (EQgen_mono RS ci3_AI)] @ + (REPEAT (resolve_tac (EQgenIs @ [EQ_refl RS (EQgen_mono RS ci3_AI)] @ (EQgenIs RL [EQgen_mono RS ci3_AgenI]) @ [EQgen_mono RS ci3_RI]) i)); (* Goals of the form R <= EQgen(R) - rewrite elements : EQgen(R) using rews and *) (* then reduce this to a goal : R (hopefully?) *) (* rews are rewrite rules that would cause looping in the simpifier *) -fun EQgen_tac simp_set rews i = - SELECT_GOAL +fun EQgen_tac simp_set rews i = + SELECT_GOAL (TRY (safe_tac ccl_cs) THEN resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [ssubst_pair])) i THEN ALLGOALS (simp_tac simp_set) THEN diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/equalities.ML --- a/src/CCL/equalities.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/equalities.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,134 +1,127 @@ -(* Title: CCL/equalities +(* Title: CCL/equalities.ML ID: $Id$ -Modified version of - Title: HOL/equalities - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - Equalities involving union, intersection, inclusion, etc. *) -writeln"File HOL/equalities"; - val eq_cs = set_cs addSIs [equalityI]; (** Binary Intersection **) -goal Set.thy "A Int A = A"; +goal (the_context ()) "A Int A = A"; by (fast_tac eq_cs 1); qed "Int_absorb"; -goal Set.thy "A Int B = B Int A"; +goal (the_context ()) "A Int B = B Int A"; by (fast_tac eq_cs 1); qed "Int_commute"; -goal Set.thy "(A Int B) Int C = A Int (B Int C)"; +goal (the_context ()) "(A Int B) Int C = A Int (B Int C)"; by (fast_tac eq_cs 1); qed "Int_assoc"; -goal Set.thy "(A Un B) Int C = (A Int C) Un (B Int C)"; +goal (the_context ()) "(A Un B) Int C = (A Int C) Un (B Int C)"; by (fast_tac eq_cs 1); qed "Int_Un_distrib"; -goal Set.thy "(A<=B) <-> (A Int B = A)"; +goal (the_context ()) "(A<=B) <-> (A Int B = A)"; by (fast_tac (eq_cs addSEs [equalityE]) 1); qed "subset_Int_eq"; (** Binary Union **) -goal Set.thy "A Un A = A"; +goal (the_context ()) "A Un A = A"; by (fast_tac eq_cs 1); qed "Un_absorb"; -goal Set.thy "A Un B = B Un A"; +goal (the_context ()) "A Un B = B Un A"; by (fast_tac eq_cs 1); qed "Un_commute"; -goal Set.thy "(A Un B) Un C = A Un (B Un C)"; +goal (the_context ()) "(A Un B) Un C = A Un (B Un C)"; by (fast_tac eq_cs 1); qed "Un_assoc"; -goal Set.thy "(A Int B) Un C = (A Un C) Int (B Un C)"; +goal (the_context ()) "(A Int B) Un C = (A Un C) Int (B Un C)"; by (fast_tac eq_cs 1); qed "Un_Int_distrib"; -goal Set.thy +goal (the_context ()) "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"; by (fast_tac eq_cs 1); qed "Un_Int_crazy"; -goal Set.thy "(A<=B) <-> (A Un B = B)"; +goal (the_context ()) "(A<=B) <-> (A Un B = B)"; by (fast_tac (eq_cs addSEs [equalityE]) 1); qed "subset_Un_eq"; (** Simple properties of Compl -- complement of a set **) -goal Set.thy "A Int Compl(A) = {x. False}"; +goal (the_context ()) "A Int Compl(A) = {x. False}"; by (fast_tac eq_cs 1); qed "Compl_disjoint"; -goal Set.thy "A Un Compl(A) = {x. True}"; +goal (the_context ()) "A Un Compl(A) = {x. True}"; by (fast_tac eq_cs 1); qed "Compl_partition"; -goal Set.thy "Compl(Compl(A)) = A"; +goal (the_context ()) "Compl(Compl(A)) = A"; by (fast_tac eq_cs 1); qed "double_complement"; -goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)"; +goal (the_context ()) "Compl(A Un B) = Compl(A) Int Compl(B)"; by (fast_tac eq_cs 1); qed "Compl_Un"; -goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)"; +goal (the_context ()) "Compl(A Int B) = Compl(A) Un Compl(B)"; by (fast_tac eq_cs 1); qed "Compl_Int"; -goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"; +goal (the_context ()) "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"; by (fast_tac eq_cs 1); qed "Compl_UN"; -goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"; +goal (the_context ()) "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"; by (fast_tac eq_cs 1); qed "Compl_INT"; (*Halmos, Naive Set Theory, page 16.*) -goal Set.thy "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)"; +goal (the_context ()) "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)"; by (fast_tac (eq_cs addSEs [equalityE]) 1); qed "Un_Int_assoc_eq"; (** Big Union and Intersection **) -goal Set.thy "Union(A Un B) = Union(A) Un Union(B)"; +goal (the_context ()) "Union(A Un B) = Union(A) Un Union(B)"; by (fast_tac eq_cs 1); qed "Union_Un_distrib"; -val prems = goal Set.thy +val prems = goal (the_context ()) "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})"; by (fast_tac (eq_cs addSEs [equalityE]) 1); qed "Union_disjoint"; -goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)"; +goal (the_context ()) "Inter(A Un B) = Inter(A) Int Inter(B)"; by (best_tac eq_cs 1); qed "Inter_Un_distrib"; (** Unions and Intersections of Families **) -goal Set.thy "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"; +goal (the_context ()) "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"; by (fast_tac eq_cs 1); qed "UN_eq"; (*Look: it has an EXISTENTIAL quantifier*) -goal Set.thy "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"; +goal (the_context ()) "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"; by (fast_tac eq_cs 1); qed "INT_eq"; -goal Set.thy "A Int Union(B) = (UN C:B. A Int C)"; +goal (the_context ()) "A Int Union(B) = (UN C:B. A Int C)"; by (fast_tac eq_cs 1); qed "Int_Union_image"; -goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)"; +goal (the_context ()) "A Un Inter(B) = (INT C:B. A Un C)"; by (fast_tac eq_cs 1); qed "Un_Inter_image"; diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/eval.ML --- a/src/CCL/eval.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/eval.ML Sat Sep 17 17:35:26 2005 +0200 @@ -2,39 +2,36 @@ ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge - *) - - (*** Evaluation ***) val EVal_rls = ref [trueV,falseV,pairV,lamV,caseVtrue,caseVfalse,caseVpair,caseVlam]; val eval_tac = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls) 1); fun ceval_tac rls = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls@rls) 1); -val prems = goalw thy [apply_def] +val prems = goalw (the_context ()) [apply_def] "[| f ---> lam x. b(x); b(a) ---> c |] ==> f ` a ---> c"; by (ceval_tac prems); qed "applyV"; EVal_rls := !EVal_rls @ [applyV]; -val major::prems = goalw thy [let_def] +val major::prems = goalw (the_context ()) [let_def] "[| t ---> a; f(a) ---> c |] ==> let x be t in f(x) ---> c"; by (rtac (major RS canonical) 1); by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE etac substitute 1))); qed "letV"; -val prems = goalw thy [fix_def] +val prems = goalw (the_context ()) [fix_def] "f(fix(f)) ---> c ==> fix(f) ---> c"; by (rtac applyV 1); by (rtac lamV 1); by (resolve_tac prems 1); qed "fixV"; -val prems = goalw thy [letrec_def] +val prems = goalw (the_context ()) [letrec_def] "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> \ \ letrec g x be h(x,g) in g(t) ---> c"; by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1)); @@ -42,9 +39,9 @@ EVal_rls := !EVal_rls @ [letV,letrecV,fixV]; -fun mk_V_rl s = prove_goalw thy data_defs s (fn prems => [ceval_tac prems]); +fun mk_V_rl s = prove_goalw (the_context ()) data_defs s (fn prems => [ceval_tac prems]); -val V_rls = map mk_V_rl +val V_rls = map mk_V_rl ["true ---> true", "false ---> false", "[| b--->true; t--->c |] ==> if b then t else u ---> c", @@ -68,19 +65,19 @@ (* Factorial *) -val prems = goal thy +val prems = goal (the_context ()) "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \ \ in f(succ(succ(zero))) ---> ?a"; by (ceval_tac []); -val prems = goal thy +val prems = goal (the_context ()) "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \ \ in f(succ(succ(succ(zero)))) ---> ?a"; by (ceval_tac []); (* Less Than Or Equal *) -fun isle x y = prove_goal thy +fun isle x y = prove_goal (the_context ()) ("letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f()))) \ \ in f(<"^x^","^y^">) ---> ?a") (fn prems => [ceval_tac []]); @@ -92,13 +89,12 @@ (* Reverse *) -val prems = goal thy +val prems = goal (the_context ()) "letrec id l be lcase(l,[],%x xs. x$id(xs)) \ \ in id(zero$succ(zero)$[]) ---> ?a"; by (ceval_tac []); -val prems = goal thy +val prems = goal (the_context ()) "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) \ \ in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a"; by (ceval_tac []); - diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/Flag.ML --- a/src/CCL/ex/Flag.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/Flag.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,37 +1,33 @@ -(* Title: CCL/ex/flag +(* Title: CCL/ex/Flag.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -For flag.thy. *) -open Flag; - (******) val flag_defs = [Colour_def,red_def,white_def,blue_def,ccase_def]; (******) -val ColourXH = mk_XH_tac Flag.thy (simp_type_defs @flag_defs) [] +val ColourXH = mk_XH_tac (the_context ()) (simp_type_defs @flag_defs) [] "a : Colour <-> (a=red | a=white | a=blue)"; val Colour_case = XH_to_E ColourXH; -val redT = mk_canT_tac Flag.thy [ColourXH] "red : Colour"; -val whiteT = mk_canT_tac Flag.thy [ColourXH] "white : Colour"; -val blueT = mk_canT_tac Flag.thy [ColourXH] "blue : Colour"; +val redT = mk_canT_tac (the_context ()) [ColourXH] "red : Colour"; +val whiteT = mk_canT_tac (the_context ()) [ColourXH] "white : Colour"; +val blueT = mk_canT_tac (the_context ()) [ColourXH] "blue : Colour"; -val ccaseT = mk_ncanT_tac Flag.thy flag_defs case_rls case_rls +val ccaseT = mk_ncanT_tac (the_context ()) flag_defs case_rls case_rls "[| c:Colour; \ \ c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> \ \ ccase(c,r,w,b) : C(c)"; (***) -val prems = goalw Flag.thy [flag_def] +val prems = goalw (the_context ()) [flag_def] "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"; by (typechk_tac [redT,whiteT,blueT,ccaseT] 1); by clean_ccs_tac; @@ -40,7 +36,7 @@ result(); -val prems = goalw Flag.thy [flag_def] +val prems = goalw (the_context ()) [flag_def] "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"; by (gen_ccs_tac [redT,whiteT,blueT,ccaseT] 1); by (REPEAT_SOME (ares_tac [ListPRI RS (ListPR_wf RS wfI)])); diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/Flag.thy --- a/src/CCL/ex/Flag.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/Flag.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,48 +1,49 @@ -(* Title: CCL/ex/flag.thy +(* Title: CCL/ex/Flag.thy ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -Dutch national flag program - except that the point of Dijkstra's example was to use -arrays and this uses lists. - *) -Flag = List + +header {* Dutch national flag program -- except that the point of Dijkstra's example was to use + arrays and this uses lists. *} + +theory Flag +imports List +begin consts - Colour :: "i set" - red, white, blue :: "i" + red :: "i" + white :: "i" + blue :: "i" ccase :: "[i,i,i,i]=>i" flag :: "i" -rules +axioms - Colour_def "Colour == Unit + Unit + Unit" - red_def "red == inl(one)" - white_def "white == inr(inl(one))" - blue_def "blue == inr(inr(one))" + Colour_def: "Colour == Unit + Unit + Unit" + red_def: "red == inl(one)" + white_def: "white == inr(inl(one))" + blue_def: "blue == inr(inr(one))" - ccase_def "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))" + ccase_def: "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))" - flag_def "flag == lam l. letrec - flagx l be lcase(l,<[],<[],[]>>, - %h t. split(flagx(t),%lr p. split(p,%lw lb. - ccase(h, >, - >, - >)))) - in flagx(l)" + flag_def: "flag == lam l. letrec + flagx l be lcase(l,<[],<[],[]>>, + %h t. split(flagx(t),%lr p. split(p,%lw lb. + ccase(h, >, + >, + >)))) + in flagx(l)" - Flag_def - "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). - x = > --> - (ALL c:Colour.(c mem lr = true --> c=red) & - (c mem lw = true --> c=white) & - (c mem lb = true --> c=blue)) & + Flag_def: + "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). + x = > --> + (ALL c:Colour.(c mem lr = true --> c=red) & + (c mem lw = true --> c=white) & + (c mem lb = true --> c=blue)) & Perm(l,lr @ lw @ lb)" -end +ML {* use_legacy_bindings (the_context ()) *} - - +end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/List.ML --- a/src/CCL/ex/List.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/List.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,19 +1,15 @@ -(* Title: CCL/ex/list +(* Title: CCL/ex/List.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -For list.thy. *) -open List; - val list_defs = [map_def,comp_def,append_def,filter_def,flat_def, insert_def,isort_def,partition_def,qsort_def]; (****) -val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [simp_tac term_ss 1])) +val listBs = map (fn s=>prove_goalw (the_context ()) list_defs s (fn _ => [simp_tac term_ss 1])) ["(f o g) = (%a. f(g(a)))", "(f o g)(a) = f(g(a))", "map(f,[]) = []", @@ -31,57 +27,57 @@ (****) -val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []"; +val [prem] = goal (the_context ()) "n:Nat ==> map(f) ^ n ` [] = []"; by (rtac (prem RS Nat_ind) 1); by (ALLGOALS (asm_simp_tac list_ss)); qed "nmapBnil"; -val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)"; +val [prem] = goal (the_context ()) "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)"; by (rtac (prem RS Nat_ind) 1); by (ALLGOALS (asm_simp_tac list_ss)); qed "nmapBcons"; (***) -val prems = goalw List.thy [map_def] +val prems = goalw (the_context ()) [map_def] "[| !!x. x:A==>f(x):B; l : List(A) |] ==> map(f,l) : List(B)"; by (typechk_tac prems 1); qed "mapT"; -val prems = goalw List.thy [append_def] +val prems = goalw (the_context ()) [append_def] "[| l : List(A); m : List(A) |] ==> l @ m : List(A)"; by (typechk_tac prems 1); qed "appendT"; -val prems = goal List.thy +val prems = goal (the_context ()) "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}"; by (cut_facts_tac prems 1); by (fast_tac (set_cs addSIs [SubtypeI,appendT] addSEs [SubtypeE]) 1); qed "appendTS"; -val prems = goalw List.thy [filter_def] +val prems = goalw (the_context ()) [filter_def] "[| f:A->Bool; l : List(A) |] ==> filter(f,l) : List(A)"; by (typechk_tac prems 1); qed "filterT"; -val prems = goalw List.thy [flat_def] +val prems = goalw (the_context ()) [flat_def] "l : List(List(A)) ==> flat(l) : List(A)"; by (typechk_tac (appendT::prems) 1); qed "flatT"; -val prems = goalw List.thy [insert_def] +val prems = goalw (the_context ()) [insert_def] "[| f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)"; by (typechk_tac prems 1); qed "insertT"; -val prems = goal List.thy +val prems = goal (the_context ()) "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> \ \ insert(f,a,l) : {x:List(A). P(x)}"; by (cut_facts_tac prems 1); by (fast_tac (set_cs addSIs [SubtypeI,insertT] addSEs [SubtypeE]) 1); qed "insertTS"; -val prems = goalw List.thy [partition_def] +val prems = goalw (the_context ()) [partition_def] "[| f:A->Bool; l : List(A) |] ==> partition(f,l) : List(A)*List(A)"; by (typechk_tac prems 1); by clean_ccs_tac; @@ -93,14 +89,13 @@ (*** Correctness Conditions for Insertion Sort ***) -val prems = goalw List.thy [isort_def] +val prems = goalw (the_context ()) [isort_def] "f:A->A->Bool ==> isort(f) : PROD l:List(A).{x: List(A). Ord(f,x) & Perm(x,l)}"; by (gen_ccs_tac ([insertTS,insertT]@prems) 1); (*** Correctness Conditions for Quick Sort ***) -val prems = goalw List.thy [qsort_def] +val prems = goalw (the_context ()) [qsort_def] "f:A->A->Bool ==> qsort(f) : PROD l:List(A).{x: List(A). Ord(f,x) & Perm(x,l)}"; by (gen_ccs_tac ([partitionT,appendTS,appendT]@prems) 1); - diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/List.thy --- a/src/CCL/ex/List.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/List.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,12 +1,14 @@ -(* Title: CCL/ex/list.thy +(* Title: CCL/ex/List.thy ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -Programs defined over lists. *) -List = Nat + +header {* Programs defined over lists *} + +theory List +imports Nat +begin consts map :: "[i=>i,i]=>i" @@ -20,25 +22,27 @@ isort :: "i=>i" qsort :: "i=>i" -rules +axioms - map_def "map(f,l) == lrec(l,[],%x xs g. f(x)$g)" - comp_def "f o g == (%x. f(g(x)))" - append_def "l @ m == lrec(l,m,%x xs g. x$g)" - mem_def "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)" - filter_def "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)" - flat_def "flat(l) == lrec(l,[],%h t g. h @ g)" + map_def: "map(f,l) == lrec(l,[],%x xs g. f(x)$g)" + comp_def: "f o g == (%x. f(g(x)))" + append_def: "l @ m == lrec(l,m,%x xs g. x$g)" + mem_def: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)" + filter_def: "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)" + flat_def: "flat(l) == lrec(l,[],%h t g. h @ g)" - insert_def "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)" - isort_def "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))" + insert_def: "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)" + isort_def: "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))" - partition_def + partition_def: "partition(f,l) == letrec part l a b be lcase(l,,%x xs. - if f`x then part(xs,x$a,b) else part(xs,a,x$b)) + if f`x then part(xs,x$a,b) else part(xs,a,x$b)) in part(l,[],[])" - qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. - let p be partition(f`h,t) - in split(p,%x y. qsortx(x) @ h$qsortx(y))) + qsort_def: "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. + let p be partition(f`h,t) + in split(p,%x y. qsortx(x) @ h$qsortx(y))) in qsortx(l)" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/Nat.ML --- a/src/CCL/ex/Nat.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/Nat.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,16 +1,12 @@ -(* Title: CCL/ex/nat +(* Title: CCL/ex/Nat.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -For nat.thy. *) -open Nat; - val nat_defs = [not_def,add_def,mult_def,sub_def,le_def,lt_def,ack_def,napply_def]; -val natBs = map (fn s=>prove_goalw Nat.thy nat_defs s (fn _ => [simp_tac term_ss 1])) +val natBs = map (fn s=>prove_goalw (the_context ()) nat_defs s (fn _ => [simp_tac term_ss 1])) ["not(true) = false", "not(false) = true", "zero #+ n = n", @@ -24,47 +20,47 @@ (*** Lemma for napply ***) -val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a"; +val [prem] = goal (the_context ()) "n:Nat ==> f^n`f(a) = f^succ(n)`a"; by (rtac (prem RS Nat_ind) 1); by (ALLGOALS (asm_simp_tac nat_ss)); qed "napply_f"; (****) -val prems = goalw Nat.thy [add_def] "[| a:Nat; b:Nat |] ==> a #+ b : Nat"; +val prems = goalw (the_context ()) [add_def] "[| a:Nat; b:Nat |] ==> a #+ b : Nat"; by (typechk_tac prems 1); qed "addT"; -val prems = goalw Nat.thy [mult_def] "[| a:Nat; b:Nat |] ==> a #* b : Nat"; +val prems = goalw (the_context ()) [mult_def] "[| a:Nat; b:Nat |] ==> a #* b : Nat"; by (typechk_tac (addT::prems) 1); qed "multT"; (* Defined to return zero if a a #- b : Nat"; +val prems = goalw (the_context ()) [sub_def] "[| a:Nat; b:Nat |] ==> a #- b : Nat"; by (typechk_tac (prems) 1); by clean_ccs_tac; by (etac (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1); qed "subT"; -val prems = goalw Nat.thy [le_def] "[| a:Nat; b:Nat |] ==> a #<= b : Bool"; +val prems = goalw (the_context ()) [le_def] "[| a:Nat; b:Nat |] ==> a #<= b : Bool"; by (typechk_tac (prems) 1); by clean_ccs_tac; by (etac (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1); qed "leT"; -val prems = goalw Nat.thy [not_def,lt_def] "[| a:Nat; b:Nat |] ==> a #< b : Bool"; +val prems = goalw (the_context ()) [not_def,lt_def] "[| a:Nat; b:Nat |] ==> a #< b : Bool"; by (typechk_tac (prems@[leT]) 1); qed "ltT"; (* Correctness conditions for subtractive division **) -val prems = goalw Nat.thy [div_def] +val prems = goalw (the_context ()) [div_def] "[| a:Nat; b:{x:Nat.~x=zero} |] ==> a ## b : {x:Nat. DIV(a,b,x)}"; by (gen_ccs_tac (prems@[ltT,subT]) 1); (* Termination Conditions for Ackermann's Function *) -val prems = goalw Nat.thy [ack_def] +val prems = goalw (the_context ()) [ack_def] "[| a:Nat; b:Nat |] ==> ackermann(a,b) : Nat"; by (gen_ccs_tac prems 1); val relI = NatPR_wf RS (NatPR_wf RS lex_wf RS wfI); diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/Nat.thy --- a/src/CCL/ex/Nat.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/Nat.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,38 +1,46 @@ -(* Title: CCL/ex/nat.thy +(* Title: CCL/ex/Nat.thy ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -Programs defined over the natural numbers *) -Nat = Wfd + +header {* Programs defined over the natural numbers *} + +theory Nat +imports Wfd +begin consts - not :: "i=>i" - "#+","#*","#-", - "##","#<","#<=" :: "[i,i]=>i" (infixr 60) - ackermann :: "[i,i]=>i" + not :: "i=>i" + "#+" :: "[i,i]=>i" (infixr 60) + "#*" :: "[i,i]=>i" (infixr 60) + "#-" :: "[i,i]=>i" (infixr 60) + "##" :: "[i,i]=>i" (infixr 60) + "#<" :: "[i,i]=>i" (infixr 60) + "#<=" :: "[i,i]=>i" (infixr 60) + ackermann :: "[i,i]=>i" -rules +defs - not_def "not(b) == if b then false else true" + not_def: "not(b) == if b then false else true" - add_def "a #+ b == nrec(a,b,%x g. succ(g))" - mult_def "a #* b == nrec(a,zero,%x g. b #+ g)" - sub_def "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy))) + add_def: "a #+ b == nrec(a,b,%x g. succ(g))" + mult_def: "a #* b == nrec(a,zero,%x g. b #+ g)" + sub_def: "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy))) in sub(a,b)" - le_def "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy))) + le_def: "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy))) in le(a,b)" - lt_def "a #< b == not(b #<= a)" + lt_def: "a #< b == not(b #<= a)" - div_def "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y)) + div_def: "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y)) in div(a,b)" - ack_def - "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. + ack_def: + "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y)))) in ack(a,b)" +ML {* use_legacy_bindings (the_context ()) *} + end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/ROOT.ML --- a/src/CCL/ex/ROOT.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/ROOT.ML Sat Sep 17 17:35:26 2005 +0200 @@ -3,7 +3,7 @@ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Executes all examples for Classical Computational Logic +Examples for Classical Computational Logic. *) time_use_thy "Nat"; diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/Stream.ML --- a/src/CCL/ex/Stream.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/Stream.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,21 +1,17 @@ -(* Title: CCL/ex/stream +(* Title: CCL/ex/Stream.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -For stream.thy. - Proving properties about infinite lists using coinduction: Lists(A) is the set of all finite and infinite lists of elements of A. ILists(A) is the set of infinite lists of elements of A. *) -open Stream; - (*** Map of composition is composition of maps ***) -val prems = goal Stream.thy "l:Lists(A) ==> map(f o g,l) = map(f,map(g,l))"; -by (eq_coinduct3_tac +val prems = goal (the_context ()) "l:Lists(A) ==> map(f o g,l) = map(f,map(g,l))"; +by (eq_coinduct3_tac "{p. EX x y. p= & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}" 1); by (fast_tac (ccl_cs addSIs prems) 1); by (safe_tac type_cs); @@ -27,8 +23,8 @@ (*** Mapping the identity function leaves a list unchanged ***) -val prems = goal Stream.thy "l:Lists(A) ==> map(%x. x,l) = l"; -by (eq_coinduct3_tac +val prems = goal (the_context ()) "l:Lists(A) ==> map(%x. x,l) = l"; +by (eq_coinduct3_tac "{p. EX x y. p= & (EX l:Lists(A).x=map(%x. x,l) & y=l)}" 1); by (fast_tac (ccl_cs addSIs prems) 1); by (safe_tac type_cs); @@ -39,7 +35,7 @@ (*** Mapping distributes over append ***) -val prems = goal Stream.thy +val prems = goal (the_context ()) "[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)"; by (eq_coinduct3_tac "{p. EX x y. p= & (EX l:Lists(A).EX m:Lists(A). \ \ x=map(f,l@m) & y=map(f,l) @ map(f,m))}" 1); @@ -54,9 +50,9 @@ (*** Append is associative ***) -val prems = goal Stream.thy +val prems = goal (the_context ()) "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m"; -by (eq_coinduct3_tac +by (eq_coinduct3_tac "{p. EX x y. p= & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \ \ x=k @ l @ m & y=(k @ l) @ m)}" 1); by (fast_tac (ccl_cs addSIs prems) 1); @@ -69,7 +65,7 @@ (*** Appending anything to an infinite list doesn't alter it ****) -val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l"; +val prems = goal (the_context ()) "l:ILists(A) ==> l @ m = l"; by (eq_coinduct3_tac "{p. EX x y. p= & (EX l:ILists(A).EX m. x=l@m & y=l)}" 1); by (fast_tac (ccl_cs addSIs prems) 1); @@ -94,7 +90,7 @@ by (rtac refl 1); qed "iter2B"; -val [prem] =goal Stream.thy +val [prem] =goal (the_context ()) "n:Nat ==> \ \ map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))"; by (res_inst_tac [("P", "%x. ?lhs(x) = ?rhs")] (iter2B RS ssubst) 1); @@ -102,7 +98,7 @@ qed "iter2Blemma"; Goal "iter1(f,a) = iter2(f,a)"; -by (eq_coinduct3_tac +by (eq_coinduct3_tac "{p. EX x y. p= & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}" 1); by (fast_tac (type_cs addSIs [napplyBzero RS sym, diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/ex/Stream.thy --- a/src/CCL/ex/Stream.thy Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/ex/Stream.thy Sat Sep 17 17:35:26 2005 +0200 @@ -1,20 +1,24 @@ -(* Title: CCL/ex/stream.thy +(* Title: CCL/ex/Stream.thy ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -Programs defined over streams. *) -Stream = List + +header {* Programs defined over streams *} + +theory Stream +imports List +begin consts + iter1 :: "[i=>i,i]=>i" + iter2 :: "[i=>i,i]=>i" - iter1,iter2 :: "[i=>i,i]=>i" +defs -rules + iter1_def: "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" + iter2_def: "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" - iter1_def "iter1(f,a) == letrec iter x be x$iter(f(x)) in iter(a)" - iter2_def "iter2(f,a) == letrec iter x be x$map(f,iter(x)) in iter(a)" +ML {* use_legacy_bindings (the_context ()) *} end diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/genrec.ML --- a/src/CCL/genrec.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/genrec.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,4 +1,4 @@ -(* Title: 92/CCL/genrec +(* Title: CCL/genrec.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -7,7 +7,7 @@ (*** General Recursive Functions ***) -val major::prems = goal Wfd.thy +val major::prems = goal (the_context ()) "[| a : A; \ \ !!p g.[| p:A; ALL x:{x: A. :wf(R)}. g(x) : D(x) |] ==>\ \ h(p,g) : D(p) |] ==> \ @@ -22,12 +22,12 @@ by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1)); qed "letrecT"; -goalw Wfd.thy [SPLIT_def] "SPLIT(,B) = B(a,b)"; +goalw (the_context ()) [SPLIT_def] "SPLIT(,B) = B(a,b)"; by (rtac set_ext 1); by (fast_tac ccl_cs 1); qed "SPLITB"; -val prems = goalw Wfd.thy [letrec2_def] +val prems = goalw (the_context ()) [letrec2_def] "[| a : A; b : B; \ \ !!p q g.[| p:A; q:B; \ \ ALL x:A. ALL y:{y: B. <,>:wf(R)}. g(x,y) : D(x,y) |] ==>\ @@ -38,15 +38,15 @@ by (stac SPLITB 1); by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); by (rtac (SPLITB RS subst) 1); -by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE +by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); qed "letrec2T"; -goal Wfd.thy "SPLIT(>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"; +goal (the_context ()) "SPLIT(>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"; by (simp_tac (ccl_ss addsimps [SPLITB]) 1); qed "lemma"; -val prems = goalw Wfd.thy [letrec3_def] +val prems = goalw (the_context ()) [letrec3_def] "[| a : A; b : B; c : C; \ \ !!p q r g.[| p:A; q:B; r:C; \ \ ALL x:A. ALL y:B. ALL z:{z:C. <>,>> : wf(R)}. \ @@ -58,7 +58,7 @@ by (simp_tac (ccl_ss addsimps [SPLITB]) 1); by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); by (rtac (lemma RS subst) 1); -by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE +by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); qed "letrec3T"; @@ -67,21 +67,21 @@ (*** Type Checking for Recursive Calls ***) -val major::prems = goal Wfd.thy +val major::prems = goal (the_context ()) "[| ALL x:{x:A.:wf(R)}.g(x):D(x); \ \ g(a) : D(a) ==> g(a) : E; a:A; :wf(R) |] ==> \ \ g(a) : E"; by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1)); qed "rcallT"; -val major::prems = goal Wfd.thy +val major::prems = goal (the_context ()) "[| ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); \ \ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <,>:wf(R) |] ==> \ \ g(a,b) : E"; by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1)); qed "rcall2T"; -val major::prems = goal Wfd.thy +val major::prems = goal (the_context ()) "[| ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}. g(x,y,z):D(x,y,z); \ \ g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; \ \ a:A; b:B; c:C; <>,>> : wf(R) |] ==> \ @@ -93,7 +93,7 @@ (*** Instantiating an induction hypothesis with an equality assumption ***) -val prems = goal Wfd.thy +val prems = goal (the_context ()) "[| g(a) = b; ALL x:{x:A.:wf(R)}.g(x):D(x); \ \ [| ALL x:{x:A.:wf(R)}.g(x):D(x); b=g(a); g(a) : D(a) |] ==> P; \ \ ALL x:{x:A.:wf(R)}.g(x):D(x) ==> a:A; \ @@ -105,7 +105,7 @@ by (REPEAT (ares_tac prems 1)); val hyprcallT = result(); -val prems = goal Wfd.thy +val prems = goal (the_context ()) "[| g(a) = b; ALL x:{x:A.:wf(R)}.g(x):D(x);\ \ [| b=g(a); g(a) : D(a) |] ==> P; a:A; :wf(R) |] ==> \ \ P"; @@ -115,7 +115,7 @@ by (REPEAT (ares_tac prems 1)); qed "hyprcallT"; -val prems = goal Wfd.thy +val prems = goal (the_context ()) "[| g(a,b) = c; ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); \ \ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \ \ a:A; b:B; <,>:wf(R) |] ==> \ @@ -126,7 +126,7 @@ by (REPEAT (ares_tac prems 1)); qed "hyprcall2T"; -val prems = goal Wfd.thy +val prems = goal (the_context ()) "[| g(a,b,c) = d; \ \ ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z); \ \ [| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P; \ @@ -142,19 +142,19 @@ (*** Rules to Remove Induction Hypotheses after Type Checking ***) -val prems = goal Wfd.thy +val prems = goal (the_context ()) "[| ALL x:{x:A.:wf(R)}.g(x):D(x); P |] ==> \ \ P"; by (REPEAT (ares_tac prems 1)); qed "rmIH1"; -val prems = goal Wfd.thy +val prems = goal (the_context ()) "[| ALL x:A. ALL y:{y:B.<,>:wf(R)}.g(x,y):D(x,y); P |] ==> \ \ P"; by (REPEAT (ares_tac prems 1)); qed "rmIH2"; -val prems = goal Wfd.thy +val prems = goal (the_context ()) "[| ALL x:A. ALL y:B. ALL z:{z:C.<>,>>:wf(R)}.g(x,y,z):D(x,y,z); \ \ P |] ==> \ \ P"; diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/mono.ML --- a/src/CCL/mono.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/mono.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,46 +1,39 @@ -(* Title: CCL/mono +(* Title: CCL/mono.ML ID: $Id$ -Modified version of - Title: HOL/mono - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Monotonicity of various operations +Monotonicity of various operations. *) -writeln"File HOL/mono"; - -val prems = goal Set.thy "A<=B ==> Union(A) <= Union(B)"; +val prems = goal (the_context ()) "A<=B ==> Union(A) <= Union(B)"; by (cfast_tac prems 1); qed "Union_mono"; -val prems = goal Set.thy "[| B<=A |] ==> Inter(A) <= Inter(B)"; +val prems = goal (the_context ()) "[| B<=A |] ==> Inter(A) <= Inter(B)"; by (cfast_tac prems 1); qed "Inter_anti_mono"; -val prems = goal Set.thy +val prems = goal (the_context ()) "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \ \ (UN x:A. f(x)) <= (UN x:B. g(x))"; by (REPEAT (eresolve_tac [UN_E,ssubst] 1 ORELSE ares_tac ((prems RL [subsetD]) @ [subsetI,UN_I]) 1)); qed "UN_mono"; -val prems = goal Set.thy +val prems = goal (the_context ()) "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \ \ (INT x:A. f(x)) <= (INT x:A. g(x))"; by (REPEAT (ares_tac ((prems RL [subsetD]) @ [subsetI,INT_I]) 1 ORELSE etac INT_D 1)); qed "INT_anti_mono"; -val prems = goal Set.thy "[| A<=C; B<=D |] ==> A Un B <= C Un D"; +val prems = goal (the_context ()) "[| A<=C; B<=D |] ==> A Un B <= C Un D"; by (cfast_tac prems 1); qed "Un_mono"; -val prems = goal Set.thy "[| A<=C; B<=D |] ==> A Int B <= C Int D"; +val prems = goal (the_context ()) "[| A<=C; B<=D |] ==> A Int B <= C Int D"; by (cfast_tac prems 1); qed "Int_mono"; -val prems = goal Set.thy "[| A<=B |] ==> Compl(B) <= Compl(A)"; +val prems = goal (the_context ()) "[| A<=B |] ==> Compl(B) <= Compl(A)"; by (cfast_tac prems 1); qed "Compl_anti_mono"; diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/subset.ML --- a/src/CCL/subset.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/subset.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,23 +1,18 @@ -(* Title: CCL/subset +(* Title: CCL/subsetI ID: $Id$ -Modified version of - Title: HOL/subset - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Derived rules involving subsets -Union and Intersection as lattice operations +Derived rules involving subsets. +Union and Intersection as lattice operations. *) (*** Big Union -- least upper bound of a set ***) -val prems = goal Set.thy +val prems = goal (the_context ()) "B:A ==> B <= Union(A)"; by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1)); qed "Union_upper"; -val prems = goal Set.thy +val prems = goal (the_context ()) "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C"; by (REPEAT (ares_tac [subsetI] 1 ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1)); @@ -26,13 +21,13 @@ (*** Big Intersection -- greatest lower bound of a set ***) -val prems = goal Set.thy +val prems = goal (the_context ()) "B:A ==> Inter(A) <= B"; by (REPEAT (resolve_tac (prems@[subsetI]) 1 ORELSE etac InterD 1)); qed "Inter_lower"; -val prems = goal Set.thy +val prems = goal (the_context ()) "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)"; by (REPEAT (ares_tac [subsetI,InterI] 1 ORELSE eresolve_tac (prems RL [subsetD]) 1)); @@ -40,15 +35,15 @@ (*** Finite Union -- the least upper bound of 2 sets ***) -goal Set.thy "A <= A Un B"; +goal (the_context ()) "A <= A Un B"; by (REPEAT (ares_tac [subsetI,UnI1] 1)); qed "Un_upper1"; -goal Set.thy "B <= A Un B"; +goal (the_context ()) "B <= A Un B"; by (REPEAT (ares_tac [subsetI,UnI2] 1)); qed "Un_upper2"; -val prems = goal Set.thy "[| A<=C; B<=C |] ==> A Un B <= C"; +val prems = goal (the_context ()) "[| A<=C; B<=C |] ==> A Un B <= C"; by (cut_facts_tac prems 1); by (DEPTH_SOLVE (ares_tac [subsetI] 1 ORELSE eresolve_tac [UnE,subsetD] 1)); @@ -56,15 +51,15 @@ (*** Finite Intersection -- the greatest lower bound of 2 sets *) -goal Set.thy "A Int B <= A"; +goal (the_context ()) "A Int B <= A"; by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); qed "Int_lower1"; -goal Set.thy "A Int B <= B"; +goal (the_context ()) "A Int B <= B"; by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1)); qed "Int_lower2"; -val prems = goal Set.thy "[| C<=A; C<=B |] ==> C <= A Int B"; +val prems = goal (the_context ()) "[| C<=A; C<=B |] ==> C <= A Int B"; by (cut_facts_tac prems 1); by (REPEAT (ares_tac [subsetI,IntI] 1 ORELSE etac subsetD 1)); @@ -72,24 +67,24 @@ (*** Monotonicity ***) -val [prem] = goalw Set.thy [mono_def] +val [prem] = goalw (the_context ()) [mono_def] "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; by (REPEAT (ares_tac [allI, impI, prem] 1)); qed "monoI"; -val [major,minor] = goalw Set.thy [mono_def] +val [major,minor] = goalw (the_context ()) [mono_def] "[| mono(f); A <= B |] ==> f(A) <= f(B)"; by (rtac (major RS spec RS spec RS mp) 1); by (rtac minor 1); qed "monoD"; -val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; +val [prem] = goal (the_context ()) "mono(f) ==> f(A) Un f(B) <= f(A Un B)"; by (rtac Un_least 1); by (rtac (Un_upper1 RS (prem RS monoD)) 1); by (rtac (Un_upper2 RS (prem RS monoD)) 1); qed "mono_Un"; -val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; +val [prem] = goal (the_context ()) "mono(f) ==> f(A Int B) <= f(A) Int f(B)"; by (rtac Int_greatest 1); by (rtac (Int_lower1 RS (prem RS monoD)) 1); by (rtac (Int_lower2 RS (prem RS monoD)) 1); @@ -107,7 +102,7 @@ fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs; -fun prover s = prove_goal Set.thy s (fn _=>[fast_tac set_cs 1]); +fun prover s = prove_goal (the_context ()) s (fn _=>[fast_tac set_cs 1]); val mem_rews = [trivial_set,empty_eq] @ (map prover [ "(a : A Un B) <-> (a:A | a:B)", diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/typecheck.ML --- a/src/CCL/typecheck.ML Sat Sep 17 14:02:31 2005 +0200 +++ b/src/CCL/typecheck.ML Sat Sep 17 17:35:26 2005 +0200 @@ -1,8 +1,7 @@ -(* Title: CCL/typecheck +(* Title: CCL/typecheck.ML ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - *) (*** Lemmas for constructors and subtypes ***) @@ -10,11 +9,11 @@ (* 0-ary constructors do not need additional rules as they are handled *) (* correctly by applying SubtypeI *) (* -val Subtype_canTs = +val Subtype_canTs = let fun tac prems = cut_facts_tac prems 1 THEN REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE etac SubtypeE 1) - fun solve s = prove_goal Type.thy s (fn prems => [tac prems]) + fun solve s = prove_goal (the_context ()) s (fn prems => [tac prems]) in map solve ["P(one) ==> one : {x:Unit.P(x)}", "P(true) ==> true : {x:Bool.P(x)}", @@ -28,11 +27,11 @@ "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" ] end; *) -val Subtype_canTs = +val Subtype_canTs = let fun tac prems = cut_facts_tac prems 1 THEN REPEAT (ares_tac (SubtypeI::canTs@icanTs) 1 ORELSE etac SubtypeE 1) - fun solve s = prove_goal Type.thy s (fn prems => [tac prems]) + fun solve s = prove_goal (the_context ()) s (fn prems => [tac prems]) in map solve ["a : {x:A. b:{y:B(a).P()}} ==> : {x:Sigma(A,B).P(x)}", "a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}", @@ -41,24 +40,24 @@ "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" ] end; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B"; by (cut_facts_tac prems 1); by (etac (letB RS ssubst) 1); by (assume_tac 1); qed "letT"; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)"; by (REPEAT (ares_tac (applyT::prems) 1)); qed "applyT2"; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| a:A; a:A ==> P(a) |] ==> a : {x:A. P(x)}"; by (fast_tac (type_cs addSIs prems) 1); qed "rcall_lemma1"; -val prems = goal Type.thy +val prems = goal (the_context ()) "[| a:{x:A. Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}"; by (cut_facts_tac prems 1); by (fast_tac (type_cs addSIs prems) 1); @@ -71,7 +70,7 @@ fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l) | bvars _ l = l; -fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t +fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t | get_bno l n (Const("op :",_) $ t $ _) = get_bno l n t @@ -98,8 +97,8 @@ val type_rls = canTs@icanTs@(applyT2::ncanTs)@incanTs@ precTs@letrecTs@[letT]@Subtype_canTs; -fun is_rigid_prog t = - case (Logic.strip_assums_concl t) of +fun is_rigid_prog t = + case (Logic.strip_assums_concl t) of (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) => (term_vars a = []) | _ => false; @@ -125,7 +124,7 @@ val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([SubtypeE]@rmIHs) ORELSE' hyp_subst_tac); -val clean_ccs_tac = +val clean_ccs_tac = let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i; in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE' eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE' @@ -133,5 +132,3 @@ fun gen_ccs_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls) THEN clean_ccs_tac) i; - - diff -r 151e76f0e3c7 -r bcf7544875b2 src/CCL/wfd.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/CCL/wfd.ML Sat Sep 17 17:35:26 2005 +0200 @@ -0,0 +1,193 @@ +(* Title: CCL/Wfd.ML + ID: $Id$ +*) + +(***********) + +val [major,prem] = goalw (the_context ()) [Wfd_def] + "[| Wfd(R); \ +\ !!x.[| ALL y. : R --> P(y) |] ==> P(x) |] ==> \ +\ P(a)"; +by (rtac (major RS spec RS mp RS spec RS CollectD) 1); +by (fast_tac (set_cs addSIs [prem RS CollectI]) 1); +qed "wfd_induct"; + +val [p1,p2,p3] = goal (the_context ()) + "[| !!x y. : R ==> Q(x); \ +\ ALL x. (ALL y. : R --> y : P) --> x : P; \ +\ !!x. Q(x) ==> x:P |] ==> a:P"; +by (rtac (p2 RS spec RS mp) 1); +by (fast_tac (set_cs addSIs [p1 RS p3]) 1); +qed "wfd_strengthen_lemma"; + +fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN + assume_tac (i+1); + +val wfd::prems = goal (the_context ()) "[| Wfd(r); :r; :r |] ==> P"; +by (subgoal_tac "ALL x. :r --> :r --> P" 1); +by (fast_tac (FOL_cs addIs prems) 1); +by (rtac (wfd RS wfd_induct) 1); +by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); +qed "wf_anti_sym"; + +val prems = goal (the_context ()) "[| Wfd(r); : r |] ==> P"; +by (rtac wf_anti_sym 1); +by (REPEAT (resolve_tac prems 1)); +qed "wf_anti_refl"; + +(*** Irreflexive transitive closure ***) + +val [prem] = goal (the_context ()) "Wfd(R) ==> Wfd(R^+)"; +by (rewtac Wfd_def); +by (REPEAT (ares_tac [allI,ballI,impI] 1)); +(*must retain the universal formula for later use!*) +by (rtac allE 1 THEN assume_tac 1); +by (etac mp 1); +by (rtac (prem RS wfd_induct) 1); +by (rtac (impI RS allI) 1); +by (etac tranclE 1); +by (fast_tac ccl_cs 1); +by (etac (spec RS mp RS spec RS mp) 1); +by (REPEAT (atac 1)); +qed "trancl_wf"; + +(*** Lexicographic Ordering ***) + +Goalw [lex_def] + "p : ra**rb <-> (EX a a' b b'. p = <,> & ( : ra | a=a' & : rb))"; +by (fast_tac ccl_cs 1); +qed "lexXH"; + +val prems = goal (the_context ()) + " : ra ==> <,> : ra**rb"; +by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1); +qed "lexI1"; + +val prems = goal (the_context ()) + " : rb ==> <,> : ra**rb"; +by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1); +qed "lexI2"; + +val major::prems = goal (the_context ()) + "[| p : ra**rb; \ +\ !!a a' b b'.[| : ra; p=<,> |] ==> R; \ +\ !!a b b'.[| : rb; p = <,> |] ==> R |] ==> \ +\ R"; +by (rtac (major RS (lexXH RS iffD1) RS exE) 1); +by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); +by (ALLGOALS (fast_tac ccl_cs)); +qed "lexE"; + +val [major,minor] = goal (the_context ()) + "[| p : r**s; !!a a' b b'. p = <,> ==> P |] ==>P"; +by (rtac (major RS lexE) 1); +by (ALLGOALS (fast_tac (set_cs addSEs [minor]))); +qed "lex_pair"; + +val [wfa,wfb] = goal (the_context ()) + "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)"; +by (rewtac Wfd_def); +by (safe_tac ccl_cs); +by (wfd_strengthen_tac "%x. EX a b. x=" 1); +by (fast_tac (term_cs addSEs [lex_pair]) 1); +by (subgoal_tac "ALL a b.:P" 1); +by (fast_tac ccl_cs 1); +by (rtac (wfa RS wfd_induct RS allI) 1); +by (rtac (wfb RS wfd_induct RS allI) 1);back(); +by (fast_tac (type_cs addSEs [lexE]) 1); +qed "lex_wf"; + +(*** Mapping ***) + +Goalw [wmap_def] + "p : wmap(f,r) <-> (EX x y. p= & : r)"; +by (fast_tac ccl_cs 1); +qed "wmapXH"; + +val prems = goal (the_context ()) + " : r ==> : wmap(f,r)"; +by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1); +qed "wmapI"; + +val major::prems = goal (the_context ()) + "[| p : wmap(f,r); !!a b.[| : r; p= |] ==> R |] ==> R"; +by (rtac (major RS (wmapXH RS iffD1) RS exE) 1); +by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems))); +by (ALLGOALS (fast_tac ccl_cs)); +qed "wmapE"; + +val [wf] = goal (the_context ()) + "Wfd(r) ==> Wfd(wmap(f,r))"; +by (rewtac Wfd_def); +by (safe_tac ccl_cs); +by (subgoal_tac "ALL b. ALL a. f(a)=b-->a:P" 1); +by (fast_tac ccl_cs 1); +by (rtac (wf RS wfd_induct RS allI) 1); +by (safe_tac ccl_cs); +by (etac (spec RS mp) 1); +by (safe_tac (ccl_cs addSEs [wmapE])); +by (etac (spec RS mp RS spec RS mp) 1); +by (assume_tac 1); +by (rtac refl 1); +qed "wmap_wf"; + +(* Projections *) + +val prems = goal (the_context ()) " : r ==> <,> : wmap(fst,r)"; +by (rtac wmapI 1); +by (simp_tac (term_ss addsimps prems) 1); +qed "wfstI"; + +val prems = goal (the_context ()) " : r ==> <,> : wmap(snd,r)"; +by (rtac wmapI 1); +by (simp_tac (term_ss addsimps prems) 1); +qed "wsndI"; + +val prems = goal (the_context ()) " : r ==> <>,>> : wmap(thd,r)"; +by (rtac wmapI 1); +by (simp_tac (term_ss addsimps prems) 1); +qed "wthdI"; + +(*** Ground well-founded relations ***) + +val prems = goalw (the_context ()) [wf_def] + "[| Wfd(r); a : r |] ==> a : wf(r)"; +by (fast_tac (set_cs addSIs prems) 1); +qed "wfI"; + +val prems = goalw (the_context ()) [Wfd_def] "Wfd({})"; +by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1); +qed "Empty_wf"; + +val prems = goalw (the_context ()) [wf_def] "Wfd(wf(R))"; +by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1); +by (ALLGOALS (asm_simp_tac CCL_ss)); +by (rtac Empty_wf 1); +qed "wf_wf"; + +Goalw [NatPR_def] "p : NatPR <-> (EX x:Nat. p=)"; +by (fast_tac set_cs 1); +qed "NatPRXH"; + +Goalw [ListPR_def] "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=)"; +by (fast_tac set_cs 1); +qed "ListPRXH"; + +val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2)); +val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2))); + +Goalw [Wfd_def] "Wfd(NatPR)"; +by (safe_tac set_cs); +by (wfd_strengthen_tac "%x. x:Nat" 1); +by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1); +by (etac Nat_ind 1); +by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH]))); +qed "NatPR_wf"; + +Goalw [Wfd_def] "Wfd(ListPR(A))"; +by (safe_tac set_cs); +by (wfd_strengthen_tac "%x. x:List(A)" 1); +by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1); +by (etac List_ind 1); +by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH]))); +qed "ListPR_wf";