--- 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,b> = <a',b'> <-> (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=<a,b> & t'=<a',b'> & 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 "[| <t,u> : R; R <= POgen(R) |] ==> t [= u";
+val prems = goal (the_context ()) "[| <t,u> : 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 "[| <t,u> : R; R <= EQgen(R) |] ==> t = u";
+val prems = goal (the_context ()) "[| <t,u> : 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 ())
"[| <t,u> : 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(<x,y>); !!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]));
--- 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 "<a,b> ---> <a,b>"
- 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 ---> <a,b>; 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: "<a,b> ---> <a,b>"
+ 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 ---> <a,b>; 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==<a,b> ==> u--->v;
- !!f. c==lam x. f(x) ==> u--->v |] ==>
+ canonical: "[| t ---> c; c==true ==> u--->v;
+ c==false ==> u--->v;
+ !!a b. c==<a,b> ==> 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=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
+ SIM_def:
+ "SIM(t,t',R) == (t=true & t'=true) | (t=false & t'=false) |
+ (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) |
(EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"
- POgen_def "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
- EQgen_def "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
+ POgen_def: "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
+ EQgen_def: "EQgen(R) == {p. EX t t'. p=<t,t'> & (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' <-> <t,t'> : PO"
- EQ_iff "t = t' <-> <t,t'> : EQ"
+
+ PO_iff: "t [= t' <-> <t,t'> : PO"
+ EQ_iff: "t = t' <-> <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(<a,b>,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(<a,b>,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
--- 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=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)} <= \
\ POgen({p. EX a b. p=<a,b> & (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=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & 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(<x,y>); \
\ !!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";
-
--- 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.<f`x, f`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
--- 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);
--- 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
--- 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,b> & 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 |] ==> <a,b> : 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=<a,b> & 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";
*)
--- 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,b> & a : R & b : R) |
+ HTTgen_def:
+ "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b> & 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
--- 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
--- 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";
-
--- 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
--- 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;
--- 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));
--- 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
--- 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);
--- 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) == <true,a>"
- inr_def "inr(b) == <false,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(<h,t>)"
- 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(<x,y>),%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'(<u,v>)))
- in f(%x y. g'(<x,y>))"
-
- 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'(<u,<v,w>>))))
- in f(%x y z. g'(<x,<y,z>>))"
-
- 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) == <true,a>"
+ inr_def: "inr(b) == <false,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(<h,t>)"
+ 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(<x,y>),%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'(<u,v>)))
+ in f(%x y. g'(<x,y>))"
+
+ 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'(<u,<v,w>>))))
+ in f(%x y z. g'(<x,<y,z>>))"
+
+ napply_def: "f ^n` a == nrec(n,a,%x g. f(g))"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+end
--- 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. [| <x,y>:r; <y,z>:r |] ==> <x,z>:r) ==> trans(r)";
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
qed "transI";
-val major::prems = goalw Trancl.thy [trans_def]
+val major::prems = goalw (the_context ()) [trans_def]
"[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
by (cut_facts_tac [major] 1);
by (fast_tac (FOL_cs addIs prems) 1);
@@ -27,15 +17,15 @@
(** Identity relation **)
-Goalw [id_def] "<a,a> : id";
+Goalw [id_def] "<a,a> : id";
by (rtac CollectI 1);
by (rtac exI 1);
by (rtac refl 1);
qed "idI";
-val major::prems = goalw Trancl.thy [id_def]
+val major::prems = goalw (the_context ()) [id_def]
"[| p: id; !!x.[| p = <x,x> |] ==> 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]
"[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
by (fast_tac (set_cs addIs prems) 1);
qed "compI";
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
-val prems = goalw Trancl.thy [comp_def]
+val prems = goalw (the_context ()) [comp_def]
"[| xz : r O s; \
\ !!x y z. [| xz = <x,z>; <x,y>:s; <y,z>: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 ())
"[| <a,c> : r O s; \
\ !!y. [| <a,y>:s; <y,c>: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 ())
"[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*";
by (stac rtrancl_unfold 1);
by (fast_tac (comp_cs addIs prems) 1);
qed "rtrancl_into_rtrancl";
(*rtrancl of r contains r*)
-val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*";
+val [prem] = goal (the_context ()) "[| <a,b> : r |] ==> <a,b> : 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 ())
"[| <a,b> : r^*; \
\ !!x. P(<x,x>); \
\ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \
@@ -117,7 +107,7 @@
qed "rtrancl_full_induct";
(*nice induction rule*)
-val major::prems = goal Trancl.thy
+val major::prems = goal (the_context ())
"[| <a,b> : r^*; \
\ P(a); \
\ !!y z.[| <a,y> : r^*; <y,z> : 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 ())
"[| <a,b> : r^*; (a = b) ==> P; \
\ !!y.[| <a,y> : r^*; <y,b> : 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]
"[| <a,b> : r^+ |] ==> <a,b> : r^*";
by (resolve_tac [major RS compEpair] 1);
by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
qed "trancl_into_rtrancl";
(*r^+ contains r*)
-val [prem] = goalw Trancl.thy [trancl_def]
+val [prem] = goalw (the_context ()) [trancl_def]
"[| <a,b> : r |] ==> <a,b> : r^+";
by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
qed "r_into_trancl";
(*intro rule by definition: from rtrancl and r*)
-val prems = goalw Trancl.thy [trancl_def]
+val prems = goalw (the_context ()) [trancl_def]
"[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+";
by (REPEAT (resolve_tac ([compI]@prems) 1));
qed "rtrancl_into_trancl1";
(*intro rule from r and rtrancl*)
-val prems = goal Trancl.thy
+val prems = goal (the_context ())
"[| <a,b> : r; <b,c> : r^* |] ==> <a,c> : 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 ())
"[| <a,b> : r^+; \
\ <a,b> : r ==> P; \
\ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \
@@ -207,7 +197,7 @@
by (REPEAT (assume_tac 1));
qed "trans_trancl";
-val prems = goal Trancl.thy
+val prems = goal (the_context ())
"[| <a,b> : r; <b,c> : r^+ |] ==> <a,c> : r^+";
by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
by (resolve_tac prems 1);
--- 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. <x,y>:r --> <y,z>:r --> <x,z>:r)"
-comp_def (*composition of relations*)
- "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
-id_def (*the identity relation*)
- "id == {p. EX x. p = <x,x>}"
-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. <x,y>:r --> <y,z>:r --> <x,z>:r)"
+ comp_def: (*composition of relations*)
+ "r O s == {xz. EX x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
+ id_def: (*the identity relation*)
+ "id == {p. EX x. p = <x,x>}"
+ rtrancl_def: "r^* == lfp(%s. id Un (r O s))"
+ trancl_def: "r^+ == r O rtrancl(r)"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- 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=<x,y> |] ==> c(x,y):C(<x,y>) |] ==> \
\ 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 ())
"[| <a,b> : 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);
--- 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=<a,b>}"
- 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=<a,b>}"
+ 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=<x,y> & A=B(x,y)})"
+ SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
-
-
-ML
-
-val print_translation =
- [("Pi", dependent_tr' ("@Pi", "@->")),
- ("Sigma", dependent_tr' ("@Sigma", "@*"))];
-
--- 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. <y,x>: 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.<x,y> : R ==> Q(x); \
-\ ALL x. (ALL y. <y,x> : 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); <a,x>:r; <x,a>:r |] ==> P";
-by (subgoal_tac "ALL x. <a,x>:r --> <x,a>: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); <a,a>: 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 = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
-by (fast_tac ccl_cs 1);
-qed "lexXH";
-
-val prems = goal Wfd.thy
- "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb";
-by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
-qed "lexI1";
-
-val prems = goal Wfd.thy
- "<b,b'> : rb ==> <<a,b>,<a,b'>> : 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'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R; \
-\ !!a b b'.[| <b,b'> : rb; p = <<a,b>,<a,b'>> |] ==> 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 = <<a,b>,<a',b'>> ==> 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=<a,b>" 1);
-by (fast_tac (term_cs addSEs [lex_pair]) 1);
-by (subgoal_tac "ALL a b.<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=<x,y> & <f(x),f(y)> : r)";
-by (fast_tac ccl_cs 1);
-qed "wmapXH";
-
-val prems = goal Wfd.thy
- "<f(a),f(b)> : r ==> <a,b> : 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.[| <f(a),f(b)> : r; p=<a,b> |] ==> 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 "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
-by (rtac wmapI 1);
-by (simp_tac (term_ss addsimps prems) 1);
-qed "wfstI";
-
-val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
-by (rtac wmapI 1);
-by (simp_tac (term_ss addsimps prems) 1);
-qed "wsndI";
-
-val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : 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=<x,succ(x)>)";
-by (fast_tac set_cs 1);
-qed "NatPRXH";
-
-Goalw [ListPR_def] "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
-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";
-
--- 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.<y,x> : 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=<x,y> & <f(x),f(y)> : R}"
- lex_def
+ wmap_def: "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}"
+ lex_def:
"ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
- NatPR_def "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
- ListPR_def "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
+ NatPR_def: "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
+ ListPR_def: "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
+use "wfd.ML"
+use "genrec.ML"
+use "typecheck.ML"
+use "eval.ML"
+
end
--- 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',b'> : A |] ==> <a,b> : A";
+val prems = goal (the_context ()) "[| a=a'; b=b'; <a',b'> : A |] ==> <a,b> : 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 "<a,a> : PO";
+goal (the_context ()) "<a,a> : 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)
["<true,true> : POgen(R)",
"<false,false> : POgen(R)",
"[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : 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 "<a,a> : EQ";
+goal (the_context ()) "<a,a> : 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)
["<true,true> : EQgen(R)",
"<false,false> : EQgen(R)",
"[| <a,a'> : R; <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
@@ -93,15 +93,15 @@
\ <h$t,h'$t'> : 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 <a,b> : EQgen(R) using rews and *)
(* then reduce this to a goal <a',b'> : 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
--- 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";
--- 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(<x,y>)))) \
\ 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 []);
-
--- 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)]));
--- 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, <red$lr,<lw,lb>>,
- <lr,<white$lw,lb>>,
- <lr,<lw,blue$lb>>))))
- 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, <red$lr,<lw,lb>>,
+ <lr,<white$lw,lb>>,
+ <lr,<lw,blue$lb>>))))
+ in flagx(l)"
- Flag_def
- "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
- x = <lr,<lw,lb>> -->
- (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 = <lr,<lw,lb>> -->
+ (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
--- 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);
-
--- 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,<a,b>,%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
--- 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<b *)
-val prems = goalw Nat.thy [sub_def] "[| a:Nat; b:Nat |] ==> 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);
--- 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
--- 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";
--- 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=<x,y> & (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=<x,y> & (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=<x,y> & (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=<x,y> & (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=<x,y> & (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=<x,y> & (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,
--- 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
--- 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. <x,p>: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(<a,b>,B) = B(a,b)";
+goalw (the_context ()) [SPLIT_def] "SPLIT(<a,b>,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. <<x,y>,<p,q>>: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(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)";
+goal (the_context ()) "SPLIT(<a,<b,c>>,%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. <<x,<y,z>>,<p,<q,r>>> : 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.<x,p>:wf(R)}.g(x):D(x); \
\ g(a) : D(a) ==> g(a) : E; a:A; <a,p>: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.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
\ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>: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.<<x,<y,z>>,<p,<q,r>>>: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; <<a,<b,c>>,<p,<q,r>>> : 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.<x,p>:wf(R)}.g(x):D(x); \
\ [| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); b=g(a); g(a) : D(a) |] ==> P; \
\ ALL x:{x:A.<x,p>: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.<x,p>:wf(R)}.g(x):D(x);\
\ [| b=g(a); g(a) : D(a) |] ==> P; a:A; <a,p>: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.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
\ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \
\ a:A; b:B; <<a,b>,<p,q>>: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.<<x,<y,z>>,<p,<q,r>>>: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.<x,p>: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.<<x,y>,<p,q>>: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.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
\ P |] ==> \
\ P";
--- 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";
--- 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)",
--- 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,y>)}} ==> <a,b> : {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;
-
-
--- /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. <y,x>: 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.<x,y> : R ==> Q(x); \
+\ ALL x. (ALL y. <y,x> : 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); <a,x>:r; <x,a>:r |] ==> P";
+by (subgoal_tac "ALL x. <a,x>:r --> <x,a>: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); <a,a>: 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 = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
+by (fast_tac ccl_cs 1);
+qed "lexXH";
+
+val prems = goal (the_context ())
+ "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb";
+by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
+qed "lexI1";
+
+val prems = goal (the_context ())
+ "<b,b'> : rb ==> <<a,b>,<a,b'>> : 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'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R; \
+\ !!a b b'.[| <b,b'> : rb; p = <<a,b>,<a,b'>> |] ==> 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 = <<a,b>,<a',b'>> ==> 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=<a,b>" 1);
+by (fast_tac (term_cs addSEs [lex_pair]) 1);
+by (subgoal_tac "ALL a b.<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=<x,y> & <f(x),f(y)> : r)";
+by (fast_tac ccl_cs 1);
+qed "wmapXH";
+
+val prems = goal (the_context ())
+ "<f(a),f(b)> : r ==> <a,b> : 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.[| <f(a),f(b)> : r; p=<a,b> |] ==> 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 ()) "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
+by (rtac wmapI 1);
+by (simp_tac (term_ss addsimps prems) 1);
+qed "wfstI";
+
+val prems = goal (the_context ()) "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
+by (rtac wmapI 1);
+by (simp_tac (term_ss addsimps prems) 1);
+qed "wsndI";
+
+val prems = goal (the_context ()) "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : 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=<x,succ(x)>)";
+by (fast_tac set_cs 1);
+qed "NatPRXH";
+
+Goalw [ListPR_def] "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
+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";