New example by Jacob Frost, tidied by lcp
authorlcp
Mon Feb 27 18:12:21 1995 +0100 (1995-02-27)
changeset 9156dae0daf57b7
parent 914 cae574c09137
child 916 d03bb9f50b3b
New example by Jacob Frost, tidied by lcp
src/ZF/Coind/BCR.thy
src/ZF/Coind/Dynamic.thy
src/ZF/Coind/ECR.ML
src/ZF/Coind/ECR.thy
src/ZF/Coind/Language.thy
src/ZF/Coind/MT.ML
src/ZF/Coind/MT.thy
src/ZF/Coind/Map.ML
src/ZF/Coind/Map.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Coind/BCR.thy	Mon Feb 27 18:12:21 1995 +0100
     1.3 @@ -0,0 +1,27 @@
     1.4 +(*  Title: 	ZF/Coind/BCR.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     1.7 +    Copyright   1995  University of Cambridge
     1.8 +*)
     1.9 +
    1.10 +BCR = Values + Types +
    1.11 +
    1.12 +(* Basic correspondence relation *)
    1.13 +
    1.14 +consts
    1.15 +  isof :: "[i,i] => o"
    1.16 +rules
    1.17 +  isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
    1.18 +
    1.19 +(* Extension to environments *)
    1.20 +
    1.21 +consts
    1.22 +  isofenv :: "[i,i] => o"
    1.23 +rules
    1.24 +  isofenv_def "isofenv(ve,te) ==   \
    1.25 +\   ve_dom(ve) = te_dom(te) &   \
    1.26 +\   ( ALL x:ve_dom(ve).   \
    1.27 +\     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
    1.28 +
    1.29 +  
    1.30 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/Coind/Dynamic.thy	Mon Feb 27 18:12:21 1995 +0100
     2.3 @@ -0,0 +1,41 @@
     2.4 +(*  Title: 	ZF/Coind/Dynamic.thy
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     2.7 +    Copyright   1995  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +Dynamic = Values +
    2.11 +
    2.12 +consts
    2.13 +  EvalRel :: "i"
    2.14 +inductive
    2.15 +  domains "EvalRel" <= "ValEnv * Exp * Val"
    2.16 +  intrs
    2.17 +    eval_constI
    2.18 +      " [| ve:ValEnv; c:Const |] ==>   \
    2.19 +\       <ve,e_const(c),v_const(c)>:EvalRel"
    2.20 +    eval_varI
    2.21 +      " [| ve:ValEnv; x:ExVar; x:ve_dom(ve) |] ==>   \
    2.22 +\       <ve,e_var(x),ve_app(ve,x)>:EvalRel" 
    2.23 +    eval_fnI
    2.24 +      " [| ve:ValEnv; x:ExVar; e:Exp |] ==>   \
    2.25 +\       <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "  
    2.26 +    eval_fixI
    2.27 +      " [| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val;   \
    2.28 +\          v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>   \
    2.29 +\       <ve,e_fix(f,x,e),cl>:EvalRel " 
    2.30 +    eval_appI1
    2.31 +      " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
    2.32 +\          <ve,e1,v_const(c1)>:EvalRel;   \
    2.33 +\          <ve,e2,v_const(c2)>:EvalRel |] ==>   \
    2.34 +\       <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
    2.35 +    eval_appI2
    2.36 +      " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;   \
    2.37 +\          <ve,e1,v_clos(xm,em,vem)>:EvalRel;   \
    2.38 +\          <ve,e2,v2>:EvalRel;   \
    2.39 +\          <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>   \
    2.40 +\       <ve,e_app(e1,e2),v>:EvalRel "
    2.41 +  type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
    2.42 +
    2.43 +  
    2.44 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/Coind/ECR.ML	Mon Feb 27 18:12:21 1995 +0100
     3.3 @@ -0,0 +1,84 @@
     3.4 +(*  Title: 	ZF/Coind/ECR.ML
     3.5 +    ID:         $Id$
     3.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     3.7 +    Copyright   1995  University of Cambridge
     3.8 +*)
     3.9 +
    3.10 +open Dynamic ECR;
    3.11 +
    3.12 +(* Specialised co-induction rule *)
    3.13 +
    3.14 +goal ECR.thy
    3.15 + "!!x.[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
    3.16 +\    <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
    3.17 +\    {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \
    3.18 +\    Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] ==>  \
    3.19 +\ <v_clos(x, e, ve),t>:HasTyRel";
    3.20 +by (rtac HasTyRel.coinduct 1);
    3.21 +by (rtac singletonI 1);
    3.22 +by (fast_tac (ZF_cs addIs Val_ValEnv.intrs) 1);
    3.23 +by (rtac disjI2 1);
    3.24 +by (etac singletonE 1); 
    3.25 +by (REPEAT_FIRST (resolve_tac [conjI,exI]));
    3.26 +by (REPEAT (atac 1));
    3.27 +qed "htr_closCI";
    3.28 +
    3.29 +(* Specialised elimination rules *)
    3.30 +
    3.31 +val htr_constE = 
    3.32 +  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_const(c),t>:HasTyRel");
    3.33 +
    3.34 +val htr_closE =
    3.35 +  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_clos(x,e,ve),t>:HasTyRel");
    3.36 +
    3.37 +(* Classical reasoning sets *)
    3.38 +
    3.39 +fun mk_htr_cs cs =
    3.40 +  let open HasTyRel in 
    3.41 +    ( cs 
    3.42 +      addSIs [htr_constI] 
    3.43 +      addSEs [htr_constE]
    3.44 +      addIs [htr_closI,htr_closCI]
    3.45 +      addEs [htr_closE])
    3.46 +  end;
    3.47 +
    3.48 +val htr_cs = mk_htr_cs(static_cs);
    3.49 +
    3.50 +(* Properties of the pointwise extension to environments *)
    3.51 +
    3.52 +goalw ECR.thy [hastyenv_def]
    3.53 +  "!!ve.[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
    3.54 +\   hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
    3.55 +by (safe_tac ZF_cs);
    3.56 +by (rtac (ve_dom_owr RS ssubst) 1);
    3.57 +by (assume_tac 1);
    3.58 +by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
    3.59 +by (rtac (te_dom_owr RS ssubst) 1);
    3.60 +by (asm_simp_tac ZF_ss 1);
    3.61 +by (rtac (excluded_middle RS disjE) 1);
    3.62 +by (rtac (ve_app_owr2 RS ssubst) 1);
    3.63 +by (assume_tac 1);
    3.64 +by (assume_tac 1);
    3.65 +by (rtac (te_app_owr2 RS ssubst) 1);
    3.66 +by (assume_tac 1);
    3.67 +by (dtac (ve_dom_owr RS subst) 1);
    3.68 +by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1);
    3.69 +by ((fast_tac ZF_cs 1) THEN (fast_tac ZF_cs 1));
    3.70 +by (asm_simp_tac (ZF_ss addsimps [ve_app_owr1,te_app_owr1]) 1);
    3.71 +qed "hastyenv_owr";
    3.72 +
    3.73 +goalw ECR.thy  [isofenv_def,hastyenv_def]
    3.74 +  "!!ve.[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
    3.75 +by (safe_tac ZF_cs);
    3.76 +by (dtac bspec 1);
    3.77 +by (assume_tac 1);
    3.78 +by (safe_tac ZF_cs);
    3.79 +by (dtac HasTyRel.htr_constI 1);
    3.80 +by (assume_tac 2);
    3.81 +by (etac te_appI 1);
    3.82 +by (etac ve_domI 1);
    3.83 +by (ALLGOALS (asm_full_simp_tac ZF_ss));
    3.84 +qed "basic_consistency_lem";
    3.85 +
    3.86 +
    3.87 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/Coind/ECR.thy	Mon Feb 27 18:12:21 1995 +0100
     4.3 @@ -0,0 +1,38 @@
     4.4 +(*  Title: 	ZF/Coind/ECR.thy
     4.5 +    ID:         $Id$
     4.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     4.7 +    Copyright   1995  University of Cambridge
     4.8 +*)
     4.9 +
    4.10 +ECR = Static + Dynamic +
    4.11 +
    4.12 +(* The extended correspondence relation *)
    4.13 +
    4.14 +consts
    4.15 +  HasTyRel :: "i"
    4.16 +coinductive
    4.17 +  domains "HasTyRel" <= "Val * Ty"
    4.18 +  intrs
    4.19 +    htr_constI
    4.20 +      "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
    4.21 +    htr_closI
    4.22 +      "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
    4.23 +\	  <te,e_fn(x,e),t>:ElabRel;  \
    4.24 +\	  ve_dom(ve) = te_dom(te);   \
    4.25 +\	  {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  \
    4.26 +\      |] ==>   \
    4.27 +\      <v_clos(x,e,ve),t>:HasTyRel" 
    4.28 +  monos "[Pow_mono]"
    4.29 +  type_intrs "Val_ValEnv.intrs"
    4.30 +  
    4.31 +(* Pointwise extension to environments *)
    4.32 + 
    4.33 +consts
    4.34 +  hastyenv :: "[i,i] => o"
    4.35 +rules
    4.36 +  hastyenv_def 
    4.37 +    " hastyenv(ve,te) == \
    4.38 +\     ve_dom(ve) = te_dom(te) & \
    4.39 +\     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
    4.40 +
    4.41 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/ZF/Coind/Language.thy	Mon Feb 27 18:12:21 1995 +0100
     5.3 @@ -0,0 +1,51 @@
     5.4 +(*  Title: 	ZF/Coind/Language.thy
     5.5 +    ID:         $Id$
     5.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     5.7 +    Copyright   1995  University of Cambridge
     5.8 +*)
     5.9 +
    5.10 +Language ="Datatype" + QUniv +
    5.11 +
    5.12 +(* Abstract type of constants *)
    5.13 +
    5.14 +consts
    5.15 +  Const :: "i"
    5.16 +rules
    5.17 +  constU "c:Const ==> c:univ(A)"
    5.18 +  constNEE "c:Const ==> c ~= 0"
    5.19 + 
    5.20 +(* A function that captures how constant functions are applied to
    5.21 +   constants *)
    5.22 +  
    5.23 +consts
    5.24 +  c_app :: "[i,i] => i"
    5.25 +rules
    5.26 +  c_appI "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
    5.27 +
    5.28 +
    5.29 +(* Abstract type of variables *)
    5.30 +
    5.31 +consts
    5.32 +  ExVar :: "i"
    5.33 +rules
    5.34 +  exvarU "x:ExVar ==> x:univ(A)"
    5.35 +
    5.36 +
    5.37 +(* Datatype of expressions *)
    5.38 +
    5.39 +consts
    5.40 +  Exp :: "i"
    5.41 +datatype
    5.42 +  "Exp" =
    5.43 +    e_const("c:Const") |
    5.44 +    e_var("x:ExVar") |
    5.45 +    e_fn("x:ExVar","e:Exp") | 
    5.46 +    e_fix("x1:ExVar","x2:ExVar","e:Exp") | 
    5.47 +    e_app("e1:Exp","e2:Exp")
    5.48 +  type_intrs "[constU,exvarU]"
    5.49 +
    5.50 +end
    5.51 +
    5.52 +
    5.53 +
    5.54 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/ZF/Coind/MT.ML	Mon Feb 27 18:12:21 1995 +0100
     6.3 @@ -0,0 +1,190 @@
     6.4 +(*  Title: 	ZF/Coind/MT.ML
     6.5 +    ID:         $Id$
     6.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     6.7 +    Copyright   1995  University of Cambridge
     6.8 +*)
     6.9 +
    6.10 +open MT;
    6.11 +
    6.12 +       
    6.13 +(* ############################################################ *)
    6.14 +(* The Consistency theorem                                      *)
    6.15 +(* ############################################################ *)
    6.16 +
    6.17 +val prems = goal MT.thy 
    6.18 +  "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> 	\
    6.19 +\  <v_const(c), t> : HasTyRel";
    6.20 +by (cut_facts_tac prems 1);
    6.21 +by (fast_tac htr_cs 1);
    6.22 +qed "consistency_const";
    6.23 +
    6.24 +
    6.25 +val prems = goalw  MT.thy [hastyenv_def]
    6.26 +  "[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> 	\
    6.27 +\  <ve_app(ve,x),t>:HasTyRel";
    6.28 +by (cut_facts_tac prems 1);
    6.29 +by (fast_tac static_cs 1);
    6.30 +qed "consistency_var";
    6.31 +
    6.32 +
    6.33 +val prems = goalw MT.thy [hastyenv_def]
    6.34 +  "[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); 	\
    6.35 +\     <te,e_fn(x,e),t>:ElabRel 	\
    6.36 +\  |] ==> 	\
    6.37 +\  <v_clos(x, e, ve), t> : HasTyRel";
    6.38 +by (cut_facts_tac prems 1);
    6.39 +by (best_tac htr_cs 1);
    6.40 +qed "consistency_fn";
    6.41 +
    6.42 +val MT_cs = ZF_cs 
    6.43 +  addIs (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs)
    6.44 +  addDs [te_owrE,(ElabRel.dom_subset RS subsetD)];
    6.45 +
    6.46 +val MT_ss = 
    6.47 +  ZF_ss addsimps 
    6.48 +  [ve_dom_owr,te_dom_owr,ve_app_owr1,ve_app_owr2,te_app_owr1,te_app_owr2];
    6.49 +
    6.50 +val clean_tac = 
    6.51 +  REPEAT_FIRST (fn i => 
    6.52 +    (eq_assume_tac i) ORELSE 
    6.53 +    (match_tac (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) i) ORELSE
    6.54 +    (ematch_tac [te_owrE] i));
    6.55 +
    6.56 +val prems = goalw MT.thy [hastyenv_def]
    6.57 +  "[| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; 		\
    6.58 +\     v_clos(x,e,ve_owr(ve,f,cl)) = cl; 			\ 
    6.59 +\     hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==> 	\
    6.60 +\  <cl,t>:HasTyRel";
    6.61 +by (cut_facts_tac prems 1);
    6.62 +by (etac elab_fixE 1);
    6.63 +by (safe_tac ZF_cs);
    6.64 +by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]);
    6.65 +by clean_tac;
    6.66 +by (rtac ve_owrI 1);
    6.67 +by clean_tac;
    6.68 +by (dtac (ElabRel.dom_subset RS subsetD) 1);
    6.69 +by ( eres_inst_tac 
    6.70 +     [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")] 
    6.71 +     (SigmaD1 RS te_owrE) 1
    6.72 +   );
    6.73 +by (assume_tac 1);
    6.74 +by (rtac ElabRel.elab_fnI 1);
    6.75 +by clean_tac;
    6.76 +by (asm_simp_tac MT_ss 1);
    6.77 +by (rtac (ve_dom_owr RS ssubst) 1);
    6.78 +by (assume_tac 1);
    6.79 +by (etac subst 1);
    6.80 +by (rtac v_closNE 1);
    6.81 +by (asm_simp_tac ZF_ss 1);
    6.82 +
    6.83 +by (rtac PowI 1);
    6.84 +by (rtac (ve_dom_owr RS ssubst) 1);
    6.85 +by (assume_tac 1);
    6.86 +by (etac subst 1);
    6.87 +by (rtac v_closNE 1);
    6.88 +by (rtac subsetI 1);
    6.89 +by (etac RepFunE 1);
    6.90 +by (dtac lem_fix 1);
    6.91 +by (etac UnE' 1);
    6.92 +by (rtac UnI1 1);
    6.93 +by (etac singletonE 1);
    6.94 +by (asm_full_simp_tac MT_ss 1);
    6.95 +by (rtac UnI2 1);
    6.96 +by (etac notsingletonE 1);
    6.97 +by (dtac not_sym 1);
    6.98 +by (asm_full_simp_tac MT_ss 1);
    6.99 +qed "consistency_fix";
   6.100 +
   6.101 +
   6.102 +val prems = goal MT.thy
   6.103 +  " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; 	\
   6.104 +\     <ve,e1,v_const(c1)>:EvalRel; 			\
   6.105 +\     ALL t te. 					\
   6.106 +\       hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
   6.107 +\     <ve, e2, v_const(c2)> : EvalRel; 			\
   6.108 +\     ALL t te. 					\
   6.109 +\       hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \
   6.110 +\     hastyenv(ve, te); 				\
   6.111 +\     <te,e_app(e1,e2),t>:ElabRel |] ==> 		\
   6.112 +\   <v_const(c_app(c1, c2)),t>:HasTyRel";
   6.113 +by (cut_facts_tac prems 1);
   6.114 +by (etac elab_appE 1);
   6.115 +by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
   6.116 +qed "consistency_app1";
   6.117 +
   6.118 +val prems = goal MT.thy
   6.119 +  " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; 	\
   6.120 +\      <ve,e1,v_clos(xm,em,vem)>:EvalRel; 	\
   6.121 +\      ALL t te. 				\
   6.122 +\        hastyenv(ve,te) --> 			\
   6.123 +\        <te,e1,t>:ElabRel --> 			\
   6.124 +\        <v_clos(xm,em,vem),t>:HasTyRel; 	\
   6.125 +\      <ve,e2,v2>:EvalRel; 			\
   6.126 +\      ALL t te. 				\
   6.127 +\        hastyenv(ve,te) --> 			\
   6.128 +\        <te,e2,t>:ElabRel -->		 	\
   6.129 +\        <v2,t>:HasTyRel; 			\
   6.130 +\      <ve_owr(vem,xm,v2),em,v>:EvalRel; 	\
   6.131 +\      ALL t te. 				\
   6.132 +\        hastyenv(ve_owr(vem,xm,v2),te) --> 	\
   6.133 +\        <te,em,t>:ElabRel --> 			\
   6.134 +\        <v,t>:HasTyRel; 			\
   6.135 +\      hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==> 	\
   6.136 +\   <v,t>:HasTyRel ";
   6.137 +by (cut_facts_tac prems 1);
   6.138 +by (etac elab_appE 1);
   6.139 +by (dtac (spec RS spec RS mp RS mp) 1);
   6.140 +by (assume_tac 1);
   6.141 +by (assume_tac 1);
   6.142 +by (dtac (spec RS spec RS mp RS mp) 1);
   6.143 +by (assume_tac 1);
   6.144 +by (assume_tac 1);
   6.145 +by (etac htr_closE 1);
   6.146 +by (etac elab_fnE 1);
   6.147 +by (rewrite_tac Ty.con_defs);
   6.148 +by (safe_tac sum_cs);
   6.149 +by (dtac (spec RS spec RS mp RS mp) 1);
   6.150 +by (assume_tac 3);
   6.151 +by (assume_tac 2);
   6.152 +by (rtac hastyenv_owr 1);
   6.153 +by (assume_tac 1);
   6.154 +by (assume_tac 1);
   6.155 +by (assume_tac 2);
   6.156 +by (rewrite_tac [hastyenv_def]);
   6.157 +by (fast_tac ZF_cs 1);
   6.158 +qed "consistency_app2";
   6.159 +
   6.160 +fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac)); 
   6.161 +
   6.162 +val prems = goal MT.thy 
   6.163 +  "<ve,e,v>:EvalRel ==> 	\
   6.164 +\  (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
   6.165 +by (rtac (EvalRel.mutual_induct RS spec RS spec RS spec RS impE) 1);
   6.166 +by (resolve_tac prems 7 THEN assume_tac 7);
   6.167 +by (safe_tac ZF_cs);
   6.168 +by (mt_cases_tac consistency_const);
   6.169 +by (mt_cases_tac consistency_var);
   6.170 +by (mt_cases_tac consistency_fn);
   6.171 +by (mt_cases_tac consistency_fix);
   6.172 +by (mt_cases_tac consistency_app1);
   6.173 +by (mt_cases_tac consistency_app2);
   6.174 +qed "consistency";
   6.175 +
   6.176 +
   6.177 +val prems = goal MT.thy
   6.178 +  "[| ve:ValEnv; te:TyEnv;		\
   6.179 +\     isofenv(ve,te); 			\
   6.180 +\     <ve,e,v_const(c)>:EvalRel; 	\
   6.181 +\     <te,e,t>:ElabRel 			\
   6.182 +\  |] ==>				\
   6.183 +\  isof(c,t)";
   6.184 +by (cut_facts_tac prems 1);
   6.185 +by (rtac (htr_constE) 1);
   6.186 +by (dtac consistency 1);
   6.187 +by (fast_tac (ZF_cs addSIs [basic_consistency_lem]) 1);
   6.188 +by (assume_tac 1);
   6.189 +qed "basic_consistency";
   6.190 +
   6.191 +
   6.192 +
   6.193 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/Coind/MT.thy	Mon Feb 27 18:12:21 1995 +0100
     7.3 @@ -0,0 +1,1 @@
     7.4 +MT = ECR
     7.5 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/ZF/Coind/Map.ML	Mon Feb 27 18:12:21 1995 +0100
     8.3 @@ -0,0 +1,249 @@
     8.4 +(*  Title: 	ZF/Coind/Map.ML
     8.5 +    ID:         $Id$
     8.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     8.7 +    Copyright   1995  University of Cambridge
     8.8 +*)
     8.9 +
    8.10 +open Map;
    8.11 +
    8.12 +(* ############################################################ *)
    8.13 +(* Lemmas                                                       *)
    8.14 +(* ############################################################ *)
    8.15 +
    8.16 +goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)";
    8.17 +by (fast_tac eq_cs 1);
    8.18 +qed "qbeta";
    8.19 +
    8.20 +goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0";
    8.21 +by (fast_tac eq_cs 1);
    8.22 +qed "qbeta_emp";
    8.23 +
    8.24 +goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
    8.25 +by (fast_tac eq_cs 1);
    8.26 +qed "image_Sigma1";
    8.27 +
    8.28 +goal Map.thy "0``A = 0";
    8.29 +by (fast_tac eq_cs 1);
    8.30 +qed "image_02";
    8.31 +
    8.32 +(* ############################################################ *)
    8.33 +(* Inclusion in Quine Universes                                 *)
    8.34 +(* ############################################################ *)
    8.35 +
    8.36 +(* Lemmas *)
    8.37 +
    8.38 +goalw Map.thy [quniv_def]
    8.39 +    "!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)";
    8.40 +by (rtac Pow_mono 1);
    8.41 +by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
    8.42 +by (etac subset_trans 1);
    8.43 +by (rtac (arg_subset_eclose RS univ_mono) 1);
    8.44 +by (simp_tac (ZF_ss addsimps [Union_Pow_eq]) 1);
    8.45 +qed "MapQU_lemma";
    8.46 +
    8.47 +(* Theorems *)
    8.48 +
    8.49 +val prems = goalw Map.thy [PMap_def,TMap_def]
    8.50 +  "[| m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) |] ==> m:quniv(B)";
    8.51 +by (cut_facts_tac prems 1);
    8.52 +by (rtac (MapQU_lemma RS subsetD) 1);
    8.53 +by (rtac subsetI 1);
    8.54 +by (eresolve_tac prems 1);
    8.55 +by (fast_tac ZF_cs 1);
    8.56 +by flexflex_tac;
    8.57 +qed "mapQU";
    8.58 +
    8.59 +(* ############################################################ *)
    8.60 +(* Monotonicity                                                 *)
    8.61 +(* ############################################################ *)
    8.62 +
    8.63 +goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
    8.64 +by (fast_tac ZF_cs 1);
    8.65 +by (flexflex_tac);
    8.66 +qed "map_mono";
    8.67 +
    8.68 +(* Rename to pmap_mono *)
    8.69 +
    8.70 +(* ############################################################ *)
    8.71 +(* Introduction Rules                                           *)
    8.72 +(* ############################################################ *)
    8.73 +
    8.74 +(** map_emp **)
    8.75 +
    8.76 +goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
    8.77 +by (safe_tac ZF_cs);
    8.78 +by (rtac image_02 1);
    8.79 +qed "pmap_empI";
    8.80 +
    8.81 +(** map_owr **)
    8.82 +
    8.83 +goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
    8.84 +  "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
    8.85 +by (safe_tac ZF_cs);
    8.86 +
    8.87 +by (asm_full_simp_tac if_ss 1);
    8.88 +by (fast_tac ZF_cs 1);
    8.89 +
    8.90 +by (fast_tac ZF_cs 1);
    8.91 +
    8.92 +by (rtac (excluded_middle RS disjE) 1);
    8.93 +by (dtac (if_not_P RS subst) 1);
    8.94 +by (assume_tac 1);
    8.95 +by (fast_tac ZF_cs 1);
    8.96 +by (hyp_subst_tac 1);
    8.97 +by (asm_full_simp_tac if_ss 1);
    8.98 +by (fast_tac ZF_cs 1);
    8.99 +
   8.100 +by (rtac (excluded_middle RS disjE) 1);
   8.101 +by (etac image_Sigma1 1);
   8.102 +by (rtac (qbeta RS ssubst) 1);
   8.103 +by (assume_tac 1);
   8.104 +by (dtac map_lem1 1);
   8.105 +by (etac qbeta 1);
   8.106 +by (etac UnE'  1);
   8.107 +by (etac singletonE 1);
   8.108 +by (hyp_subst_tac 1);
   8.109 +by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
   8.110 +by (etac notsingletonE 1);
   8.111 +by (dtac map_lem1 1);
   8.112 +by (rtac if_not_P 1);
   8.113 +by (assume_tac 1);
   8.114 +by (asm_full_simp_tac (if_ss addsimps [qbeta]) 1);
   8.115 +by (fast_tac ZF_cs 1);
   8.116 +qed "pmap_owrI";
   8.117 +
   8.118 +(** map_app **)
   8.119 +
   8.120 +goalw Map.thy [TMap_def,map_app_def] 
   8.121 +  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
   8.122 +by (etac domainE 1);
   8.123 +by (dtac imageI 1);
   8.124 +by (fast_tac ZF_cs 1);
   8.125 +by (etac not_emptyI 1);
   8.126 +qed "tmap_app_notempty";
   8.127 +
   8.128 +goalw Map.thy [TMap_def,map_app_def,domain_def] 
   8.129 +  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
   8.130 +by (fast_tac eq_cs 1);
   8.131 +qed "tmap_appI";
   8.132 +
   8.133 +goalw Map.thy [PMap_def]
   8.134 +  "!!m.[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
   8.135 +by (forward_tac [tmap_app_notempty] 1); 
   8.136 +by (assume_tac 1);
   8.137 +by (dtac tmap_appI 1); 
   8.138 +by (assume_tac 1);
   8.139 +by (fast_tac ZF_cs 1);
   8.140 +qed "pmap_appI";
   8.141 +
   8.142 +(** domain **)
   8.143 +
   8.144 +goalw Map.thy [TMap_def]
   8.145 +  "!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A";
   8.146 +by (fast_tac eq_cs 1);
   8.147 +qed "tmap_domainD";
   8.148 +
   8.149 +goalw Map.thy [PMap_def,TMap_def]
   8.150 +  "!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A";
   8.151 +by (fast_tac eq_cs 1);
   8.152 +qed "pmap_domainD";
   8.153 +
   8.154 +(* ############################################################ *)
   8.155 +(* Equalitites                                                  *)
   8.156 +(* ############################################################ *)
   8.157 +
   8.158 +(** Domain **)
   8.159 +
   8.160 +(* Lemmas *)
   8.161 +
   8.162 +goal Map.thy  "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
   8.163 +by (fast_tac eq_cs 1);
   8.164 +qed "domain_UN";
   8.165 +
   8.166 +goal Map.thy  "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
   8.167 +by (simp_tac (ZF_ss addsimps [domain_UN,domain_0,domain_cons]) 1);
   8.168 +by (fast_tac eq_cs 1);
   8.169 +qed "domain_Sigma";
   8.170 +
   8.171 +(* Theorems *)
   8.172 +
   8.173 +goalw Map.thy [map_emp_def] "domain(map_emp) = 0";
   8.174 +by (fast_tac eq_cs 1);
   8.175 +qed "map_domain_emp";
   8.176 +
   8.177 +goalw Map.thy [map_owr_def] 
   8.178 +  "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
   8.179 +by (simp_tac (if_ss addsimps [domain_Sigma]) 1);
   8.180 +by (rtac equalityI 1);
   8.181 +by (fast_tac eq_cs 1);
   8.182 +by (rtac subsetI 1);
   8.183 +by (rtac CollectI 1);
   8.184 +by (assume_tac 1);
   8.185 +by (etac UnE' 1);
   8.186 +by (etac singletonE 1);
   8.187 +by (asm_simp_tac if_ss 1);
   8.188 +by (fast_tac eq_cs 1);
   8.189 +by (etac notsingletonE 1);
   8.190 +by (asm_simp_tac if_ss 1);
   8.191 +by (fast_tac eq_cs 1);
   8.192 +qed "map_domain_owr";
   8.193 +
   8.194 +(** Application **)
   8.195 +
   8.196 +goalw Map.thy [map_app_def,map_owr_def] 
   8.197 +  "map_app(map_owr(f,a,b),a) = b";
   8.198 +by (rtac (qbeta RS ssubst) 1);
   8.199 +by (fast_tac ZF_cs 1);
   8.200 +by (simp_tac if_ss 1);
   8.201 +qed "map_app_owr1";
   8.202 +
   8.203 +goalw Map.thy [map_app_def,map_owr_def] 
   8.204 +  "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
   8.205 +by (rtac (excluded_middle RS disjE) 1);
   8.206 +by (rtac (qbeta_emp RS ssubst) 1);
   8.207 +by (assume_tac 1);
   8.208 +by (fast_tac eq_cs 1);
   8.209 +by (etac (qbeta RS ssubst) 1);
   8.210 +by (asm_simp_tac if_ss 1);
   8.211 +qed "map_app_owr2";
   8.212 +
   8.213 +
   8.214 +
   8.215 +
   8.216 +
   8.217 +
   8.218 +
   8.219 +
   8.220 +
   8.221 +
   8.222 +
   8.223 +
   8.224 +
   8.225 +
   8.226 +
   8.227 +
   8.228 +
   8.229 +
   8.230 +
   8.231 +
   8.232 +
   8.233 +
   8.234 +
   8.235 +
   8.236 +
   8.237 +
   8.238 +
   8.239 +
   8.240 +
   8.241 +
   8.242 +
   8.243 +
   8.244 +
   8.245 +
   8.246 +
   8.247 +
   8.248 +
   8.249 +
   8.250 +
   8.251 +
   8.252 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/ZF/Coind/Map.thy	Mon Feb 27 18:12:21 1995 +0100
     9.3 @@ -0,0 +1,27 @@
     9.4 +(*  Title: 	ZF/Coind/Map.thy
     9.5 +    ID:         $Id$
     9.6 +    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     9.7 +    Copyright   1995  University of Cambridge
     9.8 +*)
     9.9 +
    9.10 +Map = QUniv +
    9.11 +
    9.12 +consts
    9.13 +  TMap :: "[i,i] => i"
    9.14 +  PMap :: "[i,i] => i"
    9.15 +rules
    9.16 +  TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
    9.17 +  PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
    9.18 +
    9.19 +(* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
    9.20 +  
    9.21 +consts
    9.22 +  map_emp :: "i"
    9.23 +  map_owr :: "[i,i,i]=>i"
    9.24 +  map_app :: "[i,i]=>i"
    9.25 +rules
    9.26 +  map_emp_def "map_emp == 0"
    9.27 +  map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
    9.28 +  map_app_def "map_app(m,a) == m``{a}"
    9.29 +  
    9.30 +end