--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/BCR.thy Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,27 @@
+(* Title: ZF/Coind/BCR.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+BCR = Values + Types +
+
+(* Basic correspondence relation *)
+
+consts
+ isof :: "[i,i] => o"
+rules
+ isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
+
+(* Extension to environments *)
+
+consts
+ isofenv :: "[i,i] => o"
+rules
+ isofenv_def "isofenv(ve,te) == \
+\ ve_dom(ve) = te_dom(te) & \
+\ ( ALL x:ve_dom(ve). \
+\ EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Dynamic.thy Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,41 @@
+(* Title: ZF/Coind/Dynamic.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+Dynamic = Values +
+
+consts
+ EvalRel :: "i"
+inductive
+ domains "EvalRel" <= "ValEnv * Exp * Val"
+ intrs
+ eval_constI
+ " [| ve:ValEnv; c:Const |] ==> \
+\ <ve,e_const(c),v_const(c)>:EvalRel"
+ eval_varI
+ " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==> \
+\ <ve,e_var(x),ve_app(ve,x)>:EvalRel"
+ eval_fnI
+ " [| ve:ValEnv; x:ExVar; e:Exp |] ==> \
+\ <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "
+ eval_fixI
+ " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \
+\ v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==> \
+\ <ve,e_fix(f,x,e),cl>:EvalRel "
+ eval_appI1
+ " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \
+\ <ve,e1,v_const(c1)>:EvalRel; \
+\ <ve,e2,v_const(c2)>:EvalRel |] ==> \
+\ <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
+ eval_appI2
+ " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \
+\ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \
+\ <ve,e2,v2>:EvalRel; \
+\ <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==> \
+\ <ve,e_app(e1,e2),v>:EvalRel "
+ type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/ECR.ML Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,84 @@
+(* Title: ZF/Coind/ECR.ML
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+open Dynamic ECR;
+
+(* Specialised co-induction rule *)
+
+goal ECR.thy
+ "!!x.[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
+\ <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
+\ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
+\ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] ==> \
+\ <v_clos(x, e, ve),t>:HasTyRel";
+by (rtac HasTyRel.coinduct 1);
+by (rtac singletonI 1);
+by (fast_tac (ZF_cs addIs Val_ValEnv.intrs) 1);
+by (rtac disjI2 1);
+by (etac singletonE 1);
+by (REPEAT_FIRST (resolve_tac [conjI,exI]));
+by (REPEAT (atac 1));
+qed "htr_closCI";
+
+(* Specialised elimination rules *)
+
+val htr_constE =
+ (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_const(c),t>:HasTyRel");
+
+val htr_closE =
+ (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_clos(x,e,ve),t>:HasTyRel");
+
+(* Classical reasoning sets *)
+
+fun mk_htr_cs cs =
+ let open HasTyRel in
+ ( cs
+ addSIs [htr_constI]
+ addSEs [htr_constE]
+ addIs [htr_closI,htr_closCI]
+ addEs [htr_closE])
+ end;
+
+val htr_cs = mk_htr_cs(static_cs);
+
+(* Properties of the pointwise extension to environments *)
+
+goalw ECR.thy [hastyenv_def]
+ "!!ve.[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
+\ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
+by (safe_tac ZF_cs);
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (assume_tac 1);
+by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
+by (rtac (te_dom_owr RS ssubst) 1);
+by (asm_simp_tac ZF_ss 1);
+by (rtac (excluded_middle RS disjE) 1);
+by (rtac (ve_app_owr2 RS ssubst) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac (te_app_owr2 RS ssubst) 1);
+by (assume_tac 1);
+by (dtac (ve_dom_owr RS subst) 1);
+by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
+by ((fast_tac ZF_cs 1) THEN (fast_tac ZF_cs 1));
+by (asm_simp_tac (ZF_ss addsimps [ve_app_owr1,te_app_owr1]) 1);
+qed "hastyenv_owr";
+
+goalw ECR.thy [isofenv_def,hastyenv_def]
+ "!!ve.[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
+by (safe_tac ZF_cs);
+by (dtac bspec 1);
+by (assume_tac 1);
+by (safe_tac ZF_cs);
+by (dtac HasTyRel.htr_constI 1);
+by (assume_tac 2);
+by (etac te_appI 1);
+by (etac ve_domI 1);
+by (ALLGOALS (asm_full_simp_tac ZF_ss));
+qed "basic_consistency_lem";
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/ECR.thy Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,38 @@
+(* Title: ZF/Coind/ECR.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+ECR = Static + Dynamic +
+
+(* The extended correspondence relation *)
+
+consts
+ HasTyRel :: "i"
+coinductive
+ domains "HasTyRel" <= "Val * Ty"
+ intrs
+ htr_constI
+ "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
+ htr_closI
+ "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
+\ <te,e_fn(x,e),t>:ElabRel; \
+\ ve_dom(ve) = te_dom(te); \
+\ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel) \
+\ |] ==> \
+\ <v_clos(x,e,ve),t>:HasTyRel"
+ monos "[Pow_mono]"
+ type_intrs "Val_ValEnv.intrs"
+
+(* Pointwise extension to environments *)
+
+consts
+ hastyenv :: "[i,i] => o"
+rules
+ hastyenv_def
+ " hastyenv(ve,te) == \
+\ ve_dom(ve) = te_dom(te) & \
+\ (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Language.thy Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,51 @@
+(* Title: ZF/Coind/Language.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+Language ="Datatype" + QUniv +
+
+(* Abstract type of constants *)
+
+consts
+ Const :: "i"
+rules
+ constU "c:Const ==> c:univ(A)"
+ constNEE "c:Const ==> c ~= 0"
+
+(* A function that captures how constant functions are applied to
+ constants *)
+
+consts
+ c_app :: "[i,i] => i"
+rules
+ c_appI "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
+
+
+(* Abstract type of variables *)
+
+consts
+ ExVar :: "i"
+rules
+ exvarU "x:ExVar ==> x:univ(A)"
+
+
+(* Datatype of expressions *)
+
+consts
+ Exp :: "i"
+datatype
+ "Exp" =
+ e_const("c:Const") |
+ e_var("x:ExVar") |
+ e_fn("x:ExVar","e:Exp") |
+ e_fix("x1:ExVar","x2:ExVar","e:Exp") |
+ e_app("e1:Exp","e2:Exp")
+ type_intrs "[constU,exvarU]"
+
+end
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/MT.ML Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,190 @@
+(* Title: ZF/Coind/MT.ML
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+open MT;
+
+
+(* ############################################################ *)
+(* The Consistency theorem *)
+(* ############################################################ *)
+
+val prems = goal MT.thy
+ "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \
+\ <v_const(c), t> : HasTyRel";
+by (cut_facts_tac prems 1);
+by (fast_tac htr_cs 1);
+qed "consistency_const";
+
+
+val prems = goalw MT.thy [hastyenv_def]
+ "[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
+\ <ve_app(ve,x),t>:HasTyRel";
+by (cut_facts_tac prems 1);
+by (fast_tac static_cs 1);
+qed "consistency_var";
+
+
+val prems = goalw MT.thy [hastyenv_def]
+ "[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \
+\ <te,e_fn(x,e),t>:ElabRel \
+\ |] ==> \
+\ <v_clos(x, e, ve), t> : HasTyRel";
+by (cut_facts_tac prems 1);
+by (best_tac htr_cs 1);
+qed "consistency_fn";
+
+val MT_cs = ZF_cs
+ addIs (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs)
+ addDs [te_owrE,(ElabRel.dom_subset RS subsetD)];
+
+val MT_ss =
+ ZF_ss addsimps
+ [ve_dom_owr,te_dom_owr,ve_app_owr1,ve_app_owr2,te_app_owr1,te_app_owr2];
+
+val clean_tac =
+ REPEAT_FIRST (fn i =>
+ (eq_assume_tac i) ORELSE
+ (match_tac (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) i) ORELSE
+ (ematch_tac [te_owrE] i));
+
+val prems = goalw MT.thy [hastyenv_def]
+ "[| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \
+\ v_clos(x,e,ve_owr(ve,f,cl)) = cl; \
+\ hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==> \
+\ <cl,t>:HasTyRel";
+by (cut_facts_tac prems 1);
+by (etac elab_fixE 1);
+by (safe_tac ZF_cs);
+by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]);
+by clean_tac;
+by (rtac ve_owrI 1);
+by clean_tac;
+by (dtac (ElabRel.dom_subset RS subsetD) 1);
+by ( eres_inst_tac
+ [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")]
+ (SigmaD1 RS te_owrE) 1
+ );
+by (assume_tac 1);
+by (rtac ElabRel.elab_fnI 1);
+by clean_tac;
+by (asm_simp_tac MT_ss 1);
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (assume_tac 1);
+by (etac subst 1);
+by (rtac v_closNE 1);
+by (asm_simp_tac ZF_ss 1);
+
+by (rtac PowI 1);
+by (rtac (ve_dom_owr RS ssubst) 1);
+by (assume_tac 1);
+by (etac subst 1);
+by (rtac v_closNE 1);
+by (rtac subsetI 1);
+by (etac RepFunE 1);
+by (dtac lem_fix 1);
+by (etac UnE' 1);
+by (rtac UnI1 1);
+by (etac singletonE 1);
+by (asm_full_simp_tac MT_ss 1);
+by (rtac UnI2 1);
+by (etac notsingletonE 1);
+by (dtac not_sym 1);
+by (asm_full_simp_tac MT_ss 1);
+qed "consistency_fix";
+
+
+val prems = goal MT.thy
+ " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \
+\ <ve,e1,v_const(c1)>:EvalRel; \
+\ ALL t te. \
+\ hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
+\ <ve, e2, v_const(c2)> : EvalRel; \
+\ ALL t te. \
+\ hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \
+\ hastyenv(ve, te); \
+\ <te,e_app(e1,e2),t>:ElabRel |] ==> \
+\ <v_const(c_app(c1, c2)),t>:HasTyRel";
+by (cut_facts_tac prems 1);
+by (etac elab_appE 1);
+by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
+qed "consistency_app1";
+
+val prems = goal MT.thy
+ " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \
+\ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \
+\ ALL t te. \
+\ hastyenv(ve,te) --> \
+\ <te,e1,t>:ElabRel --> \
+\ <v_clos(xm,em,vem),t>:HasTyRel; \
+\ <ve,e2,v2>:EvalRel; \
+\ ALL t te. \
+\ hastyenv(ve,te) --> \
+\ <te,e2,t>:ElabRel --> \
+\ <v2,t>:HasTyRel; \
+\ <ve_owr(vem,xm,v2),em,v>:EvalRel; \
+\ ALL t te. \
+\ hastyenv(ve_owr(vem,xm,v2),te) --> \
+\ <te,em,t>:ElabRel --> \
+\ <v,t>:HasTyRel; \
+\ hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==> \
+\ <v,t>:HasTyRel ";
+by (cut_facts_tac prems 1);
+by (etac elab_appE 1);
+by (dtac (spec RS spec RS mp RS mp) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (dtac (spec RS spec RS mp RS mp) 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (etac htr_closE 1);
+by (etac elab_fnE 1);
+by (rewrite_tac Ty.con_defs);
+by (safe_tac sum_cs);
+by (dtac (spec RS spec RS mp RS mp) 1);
+by (assume_tac 3);
+by (assume_tac 2);
+by (rtac hastyenv_owr 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 2);
+by (rewrite_tac [hastyenv_def]);
+by (fast_tac ZF_cs 1);
+qed "consistency_app2";
+
+fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac));
+
+val prems = goal MT.thy
+ "<ve,e,v>:EvalRel ==> \
+\ (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
+by (rtac (EvalRel.mutual_induct RS spec RS spec RS spec RS impE) 1);
+by (resolve_tac prems 7 THEN assume_tac 7);
+by (safe_tac ZF_cs);
+by (mt_cases_tac consistency_const);
+by (mt_cases_tac consistency_var);
+by (mt_cases_tac consistency_fn);
+by (mt_cases_tac consistency_fix);
+by (mt_cases_tac consistency_app1);
+by (mt_cases_tac consistency_app2);
+qed "consistency";
+
+
+val prems = goal MT.thy
+ "[| ve:ValEnv; te:TyEnv; \
+\ isofenv(ve,te); \
+\ <ve,e,v_const(c)>:EvalRel; \
+\ <te,e,t>:ElabRel \
+\ |] ==> \
+\ isof(c,t)";
+by (cut_facts_tac prems 1);
+by (rtac (htr_constE) 1);
+by (dtac consistency 1);
+by (fast_tac (ZF_cs addSIs [basic_consistency_lem]) 1);
+by (assume_tac 1);
+qed "basic_consistency";
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/MT.thy Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,1 @@
+MT = ECR
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Map.ML Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,249 @@
+(* Title: ZF/Coind/Map.ML
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+open Map;
+
+(* ############################################################ *)
+(* Lemmas *)
+(* ############################################################ *)
+
+goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)";
+by (fast_tac eq_cs 1);
+qed "qbeta";
+
+goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0";
+by (fast_tac eq_cs 1);
+qed "qbeta_emp";
+
+goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
+by (fast_tac eq_cs 1);
+qed "image_Sigma1";
+
+goal Map.thy "0``A = 0";
+by (fast_tac eq_cs 1);
+qed "image_02";
+
+(* ############################################################ *)
+(* Inclusion in Quine Universes *)
+(* ############################################################ *)
+
+(* Lemmas *)
+
+goalw Map.thy [quniv_def]
+ "!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)";
+by (rtac Pow_mono 1);
+by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
+by (etac subset_trans 1);
+by (rtac (arg_subset_eclose RS univ_mono) 1);
+by (simp_tac (ZF_ss addsimps [Union_Pow_eq]) 1);
+qed "MapQU_lemma";
+
+(* Theorems *)
+
+val prems = goalw Map.thy [PMap_def,TMap_def]
+ "[| m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) |] ==> m:quniv(B)";
+by (cut_facts_tac prems 1);
+by (rtac (MapQU_lemma RS subsetD) 1);
+by (rtac subsetI 1);
+by (eresolve_tac prems 1);
+by (fast_tac ZF_cs 1);
+by flexflex_tac;
+qed "mapQU";
+
+(* ############################################################ *)
+(* Monotonicity *)
+(* ############################################################ *)
+
+goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
+by (fast_tac ZF_cs 1);
+by (flexflex_tac);
+qed "map_mono";
+
+(* Rename to pmap_mono *)
+
+(* ############################################################ *)
+(* Introduction Rules *)
+(* ############################################################ *)
+
+(** map_emp **)
+
+goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
+by (safe_tac ZF_cs);
+by (rtac image_02 1);
+qed "pmap_empI";
+
+(** map_owr **)
+
+goalw Map.thy [map_owr_def,PMap_def,TMap_def]
+ "!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)";
+by (safe_tac ZF_cs);
+
+by (asm_full_simp_tac if_ss 1);
+by (fast_tac ZF_cs 1);
+
+by (fast_tac ZF_cs 1);
+
+by (rtac (excluded_middle RS disjE) 1);
+by (dtac (if_not_P RS subst) 1);
+by (assume_tac 1);
+by (fast_tac ZF_cs 1);
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac if_ss 1);
+by (fast_tac ZF_cs 1);
+
+by (rtac (excluded_middle RS disjE) 1);
+by (etac image_Sigma1 1);
+by (rtac (qbeta RS ssubst) 1);
+by (assume_tac 1);
+by (dtac map_lem1 1);
+by (etac qbeta 1);
+by (etac UnE' 1);
+by (etac singletonE 1);
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
+by (etac notsingletonE 1);
+by (dtac map_lem1 1);
+by (rtac if_not_P 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
+by (fast_tac ZF_cs 1);
+qed "pmap_owrI";
+
+(** map_app **)
+
+goalw Map.thy [TMap_def,map_app_def]
+ "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
+by (etac domainE 1);
+by (dtac imageI 1);
+by (fast_tac ZF_cs 1);
+by (etac not_emptyI 1);
+qed "tmap_app_notempty";
+
+goalw Map.thy [TMap_def,map_app_def,domain_def]
+ "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
+by (fast_tac eq_cs 1);
+qed "tmap_appI";
+
+goalw Map.thy [PMap_def]
+ "!!m.[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
+by (forward_tac [tmap_app_notempty] 1);
+by (assume_tac 1);
+by (dtac tmap_appI 1);
+by (assume_tac 1);
+by (fast_tac ZF_cs 1);
+qed "pmap_appI";
+
+(** domain **)
+
+goalw Map.thy [TMap_def]
+ "!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A";
+by (fast_tac eq_cs 1);
+qed "tmap_domainD";
+
+goalw Map.thy [PMap_def,TMap_def]
+ "!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A";
+by (fast_tac eq_cs 1);
+qed "pmap_domainD";
+
+(* ############################################################ *)
+(* Equalitites *)
+(* ############################################################ *)
+
+(** Domain **)
+
+(* Lemmas *)
+
+goal Map.thy "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
+by (fast_tac eq_cs 1);
+qed "domain_UN";
+
+goal Map.thy "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
+by (simp_tac (ZF_ss addsimps [domain_UN,domain_0,domain_cons]) 1);
+by (fast_tac eq_cs 1);
+qed "domain_Sigma";
+
+(* Theorems *)
+
+goalw Map.thy [map_emp_def] "domain(map_emp) = 0";
+by (fast_tac eq_cs 1);
+qed "map_domain_emp";
+
+goalw Map.thy [map_owr_def]
+ "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
+by (simp_tac (if_ss addsimps [domain_Sigma]) 1);
+by (rtac equalityI 1);
+by (fast_tac eq_cs 1);
+by (rtac subsetI 1);
+by (rtac CollectI 1);
+by (assume_tac 1);
+by (etac UnE' 1);
+by (etac singletonE 1);
+by (asm_simp_tac if_ss 1);
+by (fast_tac eq_cs 1);
+by (etac notsingletonE 1);
+by (asm_simp_tac if_ss 1);
+by (fast_tac eq_cs 1);
+qed "map_domain_owr";
+
+(** Application **)
+
+goalw Map.thy [map_app_def,map_owr_def]
+ "map_app(map_owr(f,a,b),a) = b";
+by (rtac (qbeta RS ssubst) 1);
+by (fast_tac ZF_cs 1);
+by (simp_tac if_ss 1);
+qed "map_app_owr1";
+
+goalw Map.thy [map_app_def,map_owr_def]
+ "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
+by (rtac (excluded_middle RS disjE) 1);
+by (rtac (qbeta_emp RS ssubst) 1);
+by (assume_tac 1);
+by (fast_tac eq_cs 1);
+by (etac (qbeta RS ssubst) 1);
+by (asm_simp_tac if_ss 1);
+qed "map_app_owr2";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/Map.thy Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,27 @@
+(* Title: ZF/Coind/Map.thy
+ ID: $Id$
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+*)
+
+Map = QUniv +
+
+consts
+ TMap :: "[i,i] => i"
+ PMap :: "[i,i] => i"
+rules
+ TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
+ PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
+
+(* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
+
+consts
+ map_emp :: "i"
+ map_owr :: "[i,i,i]=>i"
+ map_app :: "[i,i]=>i"
+rules
+ map_emp_def "map_emp == 0"
+ map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
+ map_app_def "map_app(m,a) == m``{a}"
+
+end