# HG changeset patch # User lcp # Date 793964032 -3600 # Node ID d03bb9f50b3b5319b32422709bba724d0f8e2683 # Parent 6dae0daf57b7a68fb7dbf661c96b5b2161e073b2 New example by Jacob Frost, tidied by lcp diff -r 6dae0daf57b7 -r d03bb9f50b3b src/ZF/Coind/Language.ML --- /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"; + diff -r 6dae0daf57b7 -r d03bb9f50b3b src/ZF/Coind/ROOT.ML --- /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; diff -r 6dae0daf57b7 -r d03bb9f50b3b src/ZF/Coind/Static.ML --- /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 ":ElabRel"; + +val elab_varE = + ElabRel.mk_cases Exp.con_defs ":ElabRel"; + +val elab_fnE = + ElabRel.mk_cases Exp.con_defs ":ElabRel"; + +val elab_fixE = + ElabRel.mk_cases Exp.con_defs ":ElabRel"; + +val elab_appE = + ElabRel.mk_cases Exp.con_defs ":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; + + + + + + diff -r 6dae0daf57b7 -r d03bb9f50b3b src/ZF/Coind/Static.thy --- /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) |] ==> \ +\ :ElabRel " + elab_varI + " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> \ +\ :ElabRel " + elab_fnI + " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty; \ +\ :ElabRel |] ==> \ +\ :ElabRel " + elab_fixI + " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty; \ +\ :ElabRel |] ==> \ +\ :ElabRel " + elab_appI + " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty; \ +\ :ElabRel; \ +\ :ElabRel |] ==> \ +\ :ElabRel " + type_intrs "te_appI::Exp.intrs@Ty.intrs" + +end + + + + + + + + + + + + + + + + + + + + + + diff -r 6dae0daf57b7 -r d03bb9f50b3b src/ZF/Coind/Types.ML --- /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"; + + + + + + + + + + + + + + + + + + diff -r 6dae0daf57b7 -r d03bb9f50b3b src/ZF/Coind/Types.thy --- /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 + + + + + diff -r 6dae0daf57b7 -r d03bb9f50b3b src/ZF/Coind/Values.ML --- /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"; + + + diff -r 6dae0daf57b7 -r d03bb9f50b3b src/ZF/Coind/Values.thy --- /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 + + +