--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Language.ML Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,55 @@
+(* Title: ZF/Coind/Language.ML
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+(* ############################################################ *)
+(* General lemmas *)
+(* ############################################################ *)
+
+goal ZF.thy "!!a.~a=b ==> ~a:{b}";
+by (fast_tac ZF_cs 1);
+qed "notsingletonI";
+
+goal ZF.thy "!!a.~a:{b} ==> ~a=b";
+by (fast_tac ZF_cs 1);
+qed "notsingletonD";
+
+val prems = goal ZF.thy "[| a~:{b}; a~=b ==> P |] ==> P";
+by (cut_facts_tac prems 1);
+by (resolve_tac prems 1);
+by (fast_tac ZF_cs 1);
+qed "notsingletonE";
+
+goal ZF.thy "!!x. x : A Un B ==> x: B Un A";
+by (fast_tac ZF_cs 1);
+qed "lem_fix";
+
+goal ZF.thy "!!A.[| x~:A; x=y |] ==> y~:A";
+by (fast_tac ZF_cs 1);
+qed "map_lem1";
+
+
+open Language;
+
+(* ############################################################ *)
+(* Inclusion in Quine Universes *)
+(* ############################################################ *)
+
+goal Language.thy "!!c.c:Const ==> c:quniv(A)";
+by (fast_tac (ZF_cs addIs [univ_subset_quniv RS subsetD,constU]) 1);
+qed "constQU";
+
+goal Language.thy "!!x.x:ExVar ==> x:quniv(A)";
+by (fast_tac (ZF_cs addIs [univ_subset_quniv RS subsetD,exvarU]) 1);
+qed "exvarQU";
+
+goal Language.thy "!!e.e:Exp ==> e:quniv(0)";
+by (rtac subsetD 1);
+by (rtac subset_trans 1);
+by (rtac Exp.dom_subset 1);
+by (rtac univ_subset_quniv 1);
+by (assume_tac 1);
+qed "expQU";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/ROOT.ML Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,21 @@
+(* Title: ZF/Coind/MT.ML
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+
+Based upon the article
+ Robin Milner and Mads Tofte,
+ Co-induction in Relational Semantics,
+ Theoretical Computer Science 87 (1991), pages 209-220.
+
+Written up as
+ Jacob Frost, A Case Study of Co_induction in Isabelle
+ Report, Computer Lab, University of Cambridge (1995).
+*)
+
+ZF_build_completed; (*Make examples fail if ZF did*)
+
+writeln"Root file for ZF/Coind";
+proof_timing := true;
+loadpath := [".","Coind"];
+time_use_thy "MT" handle _ => exit 1;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Static.ML Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,40 @@
+(* Title: ZF/Coind/Static.ML
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+open BCR Static;
+
+val elab_constE =
+ ElabRel.mk_cases Exp.con_defs "<te,e_const(c),t>:ElabRel";
+
+val elab_varE =
+ ElabRel.mk_cases Exp.con_defs "<te,e_var(x),t>:ElabRel";
+
+val elab_fnE =
+ ElabRel.mk_cases Exp.con_defs "<te,e_fn(x,e),t>:ElabRel";
+
+val elab_fixE =
+ ElabRel.mk_cases Exp.con_defs "<te,e_fix(f,x,e),t>:ElabRel";
+
+val elab_appE =
+ ElabRel.mk_cases Exp.con_defs "<te,e_app(e1,e2),t>:ElabRel";
+
+fun mk_static_cs cs=
+ let open ElabRel in
+ ( cs
+ addSIs [elab_constI,elab_varI,elab_fnI,elab_fixI]
+ addSEs [elab_constE,elab_varE,elab_fixE]
+ addIs [elab_appI]
+ addEs [elab_appE,elab_fnE]
+ addDs [ElabRel.dom_subset RS subsetD]
+ ) end ;
+
+val static_cs = mk_static_cs ZF_cs;
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Static.thy Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,57 @@
+(* Title: ZF/Coind/Static.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+Static = BCR +
+
+consts
+ ElabRel :: "i"
+inductive
+ domains "ElabRel" <= "TyEnv * Exp * Ty"
+ intrs
+ elab_constI
+ " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==> \
+\ <te,e_const(c),t>:ElabRel "
+ elab_varI
+ " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> \
+\ <te,e_var(x),te_app(te,x)>:ElabRel "
+ elab_fnI
+ " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty; \
+\ <te_owr(te,x,t1),e,t2>:ElabRel |] ==> \
+\ <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
+ elab_fixI
+ " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty; \
+\ <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==> \
+\ <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
+ elab_appI
+ " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty; \
+\ <te,e1,t_fun(t1,t2)>:ElabRel; \
+\ <te,e2,t1>:ElabRel |] ==> \
+\ <te,e_app(e1,e2),t2>:ElabRel "
+ type_intrs "te_appI::Exp.intrs@Ty.intrs"
+
+end
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Types.ML Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,79 @@
+(* Title: ZF/Coind/Types.ML
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+open Types;
+
+val te_owrE =
+ TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv";
+
+goalw Types.thy TyEnv.con_defs "rank(te) < rank(te_owr(te,x,t))";
+by (simp_tac rank_ss 1);
+qed "rank_te_owr1";
+
+goal Types.thy "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp";
+by (rtac (te_rec_def RS def_Vrec RS trans) 1);
+by (simp_tac (ZF_ss addsimps TyEnv.case_eqns) 1);
+qed "te_rec_emp";
+
+goal Types.thy
+ " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
+\ f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))";
+by (rtac (te_rec_def RS def_Vrec RS trans) 1);
+by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
+qed "te_rec_owr";
+
+goalw Types.thy [te_dom_def] "te_dom(te_emp) = 0";
+by (simp_tac (ZF_ss addsimps [te_rec_emp]) 1);
+qed "te_dom_emp";
+
+goalw Types.thy [te_dom_def] "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}";
+by (simp_tac (ZF_ss addsimps [te_rec_owr]) 1);
+qed "te_dom_owr";
+
+goalw Types.thy [te_app_def] "te_app(te_owr(te,x,t),x) = t";
+by (simp_tac (ZF_ss addsimps [te_rec_owr]) 1);
+qed "te_app_owr1";
+
+val prems = goalw Types.thy [te_app_def]
+ "x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
+by (cut_facts_tac prems 1);
+by (asm_simp_tac (ZF_ss addsimps [te_rec_owr,(not_sym RS if_not_P)]) 1);
+qed "te_app_owr2";
+
+val prems = goal Types.thy
+ "[| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("P","x:te_dom(te)")] impE 1);
+by (assume_tac 2);
+by (assume_tac 2);
+by (etac TyEnv.induct 1);
+by (simp_tac (ZF_ss addsimps [te_dom_emp]) 1);
+by (rtac impI 1);
+by (rtac (excluded_middle RS disjE) 1);
+by (rtac (te_app_owr2 RS ssubst) 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (ZF_ss addsimps [te_dom_owr]) 1);
+by (fast_tac ZF_cs 1);
+by (asm_simp_tac (ZF_ss addsimps [te_app_owr1]) 1);
+qed "te_appI";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Types.thy Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,58 @@
+(* Title: ZF/Coind/Types.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+Types = Language +
+
+(* Abstract type of type constants *)
+
+consts
+ TyConst :: "i"
+rules
+ tyconstU "tc:TyConst ==> tc:univ(0)"
+
+
+(* Datatype of types *)
+
+consts
+ Ty :: "i"
+datatype
+ "Ty" =
+ t_const("tc:TyConst") |
+ t_fun("t1:Ty","t2:Ty")
+ type_intrs "[tyconstU]"
+
+
+(* Definition of type environments and associated operators *)
+
+consts
+ TyEnv :: "i"
+datatype
+ "TyEnv" =
+ te_emp |
+ te_owr("te:TyEnv","x:ExVar","t:Ty")
+ type_intrs "[exvarU,Ty.dom_subset RS subsetD]"
+
+consts
+ te_rec :: "[i,i,[i,i,i,i]=>i] => i"
+rules
+ te_rec_def
+ "te_rec(te,c,h) == \
+\ Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
+
+consts
+ te_dom :: "i => i"
+ te_app :: "[i,i] => i"
+rules
+ te_dom_def "te_dom(te) == te_rec(te,0,% te x t r.r Un {x})"
+ te_app_def "te_app(te,x) == te_rec(te,0, % te y t r.if(x=y,t,r))"
+
+
+end
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Values.ML Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,151 @@
+(* Title: ZF/Coind/Values.ML
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+open Values;
+
+(* Elimination rules *)
+
+val prems = goalw Values.thy (Part_def::(tl (tl Val_ValEnv.defs)))
+ "[| ve:ValEnv; !!m.[| ve=ve_mk(m); m:PMap(ExVar,Val) |] ==> Q |] ==> Q";
+by (cut_facts_tac prems 1);
+by (etac CollectE 1);
+by (etac exE 1);
+by (etac Val_ValEnv.elim 1);
+by (eresolve_tac prems 3);
+by (rewrite_tac Val_ValEnv.con_defs);
+by (ALLGOALS (fast_tac qsum_cs));
+qed "ValEnvE";
+
+val prems = goalw Values.thy (Part_def::[hd (tl Val_ValEnv.defs)])
+ "[| v:Val; \
+\ !!c. [| v = v_const(c); c:Const |] ==> Q;\
+\ !!e ve x. \
+\ [| v = v_clos(x,e,ve); x:ExVar; e:Exp; ve:ValEnv |] ==> Q \
+\ |] ==> \
+\ Q";
+by (cut_facts_tac prems 1);
+by (etac CollectE 1);
+by (etac exE 1);
+by (etac Val_ValEnv.elim 1);
+by (eresolve_tac prems 1);
+by (assume_tac 1);
+by (eresolve_tac prems 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rewrite_tac Val_ValEnv.con_defs);
+by (fast_tac qsum_cs 1);
+qed "ValE";
+
+(* Nonempty sets *)
+
+val prems = goal Values.thy "A ~= 0 ==> EX a.a:A";
+by (cut_facts_tac prems 1);
+by (rtac (foundation RS disjE) 1);
+by (fast_tac ZF_cs 1);
+by (fast_tac ZF_cs 1);
+qed "set_notemptyE";
+
+goalw Values.thy (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
+ "v_clos(x,e,ve) ~= 0";
+by (rtac not_emptyI 1);
+by (rtac UnI2 1);
+by (rtac SigmaI 1);
+by (rtac singletonI 1);
+by (rtac UnI1 1);
+by (fast_tac ZF_cs 1);
+qed "v_closNE";
+
+goalw Values.thy (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
+ "!!c.c:Const ==> v_const(c) ~= 0";
+by (dtac constNEE 1);
+by (etac not_emptyE 1);
+by (rtac not_emptyI 1);
+by (rtac UnI2 1);
+by (rtac SigmaI 1);
+by (rtac singletonI 1);
+by (rtac UnI2 1);
+by (rtac SigmaI 1);
+by (rtac singletonI 1);
+by (assume_tac 1);
+qed "v_constNE";
+
+(* Proving that the empty set is not a value *)
+
+goal Values.thy "!!v.v:Val ==> v ~= 0";
+by (etac ValE 1);
+by (ALLGOALS hyp_subst_tac);
+by (etac v_constNE 1);
+by (rtac v_closNE 1);
+qed "ValNEE";
+
+(* Equalities for value environments *)
+
+val prems = goalw Values.thy [ve_dom_def,ve_owr_def]
+ "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
+by (cut_facts_tac prems 1);
+by (etac ValEnvE 1);
+by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
+by (rtac (map_domain_owr RS ssubst) 1);
+by (assume_tac 1);
+by (rtac Un_commute 1);
+qed "ve_dom_owr";
+
+goalw Values.thy [ve_app_def,ve_owr_def]
+"!!ve. ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v";
+by (etac ValEnvE 1);
+by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
+by (rtac map_app_owr1 1);
+qed "ve_app_owr1";
+
+goalw Values.thy [ve_app_def,ve_owr_def]
+ "!!ve.ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
+by (etac ValEnvE 1);
+by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
+by (rtac map_app_owr2 1);
+by (fast_tac ZF_cs 1);
+qed "ve_app_owr2";
+
+(* Introduction rules for operators on value environments *)
+
+goalw Values.thy [ve_app_def,ve_owr_def,ve_dom_def]
+ "!!ve.[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val";
+by (etac ValEnvE 1);
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
+by (rtac pmap_appI 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "ve_appI";
+
+goalw Values.thy [ve_dom_def]
+ "!!ve.[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar";
+by (etac ValEnvE 1);
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
+by (rtac pmap_domainD 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "ve_domI";
+
+goalw Values.thy [ve_emp_def] "ve_emp:ValEnv";
+by (rtac Val_ValEnv.ve_mk_I 1);
+by (rtac pmap_empI 1);
+qed "ve_empI";
+
+goalw Values.thy [ve_owr_def]
+ "!!ve.[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv";
+by (etac ValEnvE 1);
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
+by (rtac Val_ValEnv.ve_mk_I 1);
+by (etac pmap_owrI 1);
+by (assume_tac 1);
+by (assume_tac 1);
+qed "ve_owrI";
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Values.thy Tue Feb 28 10:33:52 1995 +0100
@@ -0,0 +1,40 @@
+(* Title: ZF/Coind/Values.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+Values = Language + Map +
+
+(* Values, values environments and associated operators *)
+
+consts
+ Val :: "i" ValEnv :: "i" Val_ValEnv :: "i"
+codatatype
+ "Val" =
+ v_const("c:Const") |
+ v_clos("x:ExVar","e:Exp","ve:ValEnv") and
+ "ValEnv" =
+ ve_mk("m:PMap(ExVar,Val)")
+ monos "[map_mono]"
+ type_intrs "[constQU,exvarQU,exvarU,expQU,mapQU]"
+
+consts
+ ve_emp :: "i"
+ ve_owr :: "[i,i,i] => i"
+ ve_dom :: "i=>i"
+ ve_app :: "[i,i] => i"
+rules
+ ve_emp_def "ve_emp == ve_mk(map_emp)"
+ ve_owr_def
+ "ve_owr(ve,x,v) == \
+\ ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
+ ve_dom_def
+ "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)"
+ ve_app_def
+ "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m.map_app(m,a),ve)"
+
+end
+
+
+