# HG changeset patch # User lcp # Date 793905141 -3600 # Node ID 6dae0daf57b7a68fb7dbf661c96b5b2161e073b2 # Parent cae574c091378787ba033ef018f993b8b7d3b90b New example by Jacob Frost, tidied by lcp diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/BCR.thy --- /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 diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/Dynamic.thy --- /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 |] ==> \ +\ :EvalRel" + eval_varI + " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==> \ +\ :EvalRel" + eval_fnI + " [| ve:ValEnv; x:ExVar; e:Exp |] ==> \ +\ :EvalRel " + eval_fixI + " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \ +\ v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==> \ +\ :EvalRel " + eval_appI1 + " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \ +\ :EvalRel; \ +\ :EvalRel |] ==> \ +\ :EvalRel " + eval_appI2 + " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \ +\ :EvalRel; \ +\ :EvalRel; \ +\ :EvalRel |] ==> \ +\ :EvalRel " + type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs" + + +end diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/ECR.ML --- /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; \ +\ :ElabRel; ve_dom(ve) = te_dom(te); \ +\ {.y:ve_dom(ve)}: \ +\ Pow({} Un HasTyRel) |] ==> \ +\ :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 ":HasTyRel"); + +val htr_closE = + (HasTyRel.mk_cases Val_ValEnv.con_defs ":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); :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"; + + + diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/ECR.thy --- /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) |] ==> :HasTyRel" + htr_closI + "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \ +\ :ElabRel; \ +\ ve_dom(ve) = te_dom(te); \ +\ {.y:ve_dom(ve)}:Pow(HasTyRel) \ +\ |] ==> \ +\ :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). :HasTyRel)" + +end diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/Language.thy --- /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 + + + + diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/MT.ML --- /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);:ElabRel |] ==> \ +\ : 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); :ElabRel |] ==> \ +\ :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); \ +\ :ElabRel \ +\ |] ==> \ +\ : 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); :ElabRel |] ==> \ +\ :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; \ +\ :EvalRel; \ +\ ALL t te. \ +\ hastyenv(ve,te) --> :ElabRel --> :HasTyRel; \ +\ : EvalRel; \ +\ ALL t te. \ +\ hastyenv(ve,te) --> :ElabRel --> :HasTyRel; \ +\ hastyenv(ve, te); \ +\ :ElabRel |] ==> \ +\ :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; \ +\ :EvalRel; \ +\ ALL t te. \ +\ hastyenv(ve,te) --> \ +\ :ElabRel --> \ +\ :HasTyRel; \ +\ :EvalRel; \ +\ ALL t te. \ +\ hastyenv(ve,te) --> \ +\ :ElabRel --> \ +\ :HasTyRel; \ +\ :EvalRel; \ +\ ALL t te. \ +\ hastyenv(ve_owr(vem,xm,v2),te) --> \ +\ :ElabRel --> \ +\ :HasTyRel; \ +\ hastyenv(ve,te); :ElabRel |] ==> \ +\ :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 + ":EvalRel ==> \ +\ (ALL t te. hastyenv(ve,te) --> :ElabRel --> :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); \ +\ :EvalRel; \ +\ :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"; + + + + diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/MT.thy --- /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 diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/Map.ML --- /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"; + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r cae574c09137 -r 6dae0daf57b7 src/ZF/Coind/Map.thy --- /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