1.1 --- a/src/ZF/Coind/BCR.thy Sat Dec 22 19:46:16 2001 +0100
1.2 +++ b/src/ZF/Coind/BCR.thy Tue Dec 25 10:02:01 2001 +0100
1.3 @@ -3,25 +3,3 @@
1.4 Author: Jacob Frost, Cambridge University Computer Laboratory
1.5 Copyright 1995 University of Cambridge
1.6 *)
1.7 -
1.8 -BCR = Values + Types +
1.9 -
1.10 -(*Basic correspondence relation -- not completely specified, as it is a
1.11 - parameter of the proof. A concrete version could be defined inductively.*)
1.12 -
1.13 -consts
1.14 - isof :: [i,i] => o
1.15 -rules
1.16 - isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
1.17 -
1.18 -(*Its extension to environments*)
1.19 -
1.20 -consts
1.21 - isofenv :: [i,i] => o
1.22 -defs
1.23 - isofenv_def "isofenv(ve,te) ==
1.24 - ve_dom(ve) = te_dom(te) &
1.25 - ( \\<forall>x \\<in> ve_dom(ve).
1.26 - \\<exists>c \\<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
1.27 -
1.28 -end
2.1 --- a/src/ZF/Coind/Dynamic.thy Sat Dec 22 19:46:16 2001 +0100
2.2 +++ b/src/ZF/Coind/Dynamic.thy Tue Dec 25 10:02:01 2001 +0100
2.3 @@ -4,38 +4,37 @@
2.4 Copyright 1995 University of Cambridge
2.5 *)
2.6
2.7 -Dynamic = Values +
2.8 +theory Dynamic = Values:
2.9
2.10 consts
2.11 EvalRel :: i
2.12 inductive
2.13 domains "EvalRel" <= "ValEnv * Exp * Val"
2.14 - intrs
2.15 - eval_constI
2.16 - " [| ve \\<in> ValEnv; c \\<in> Const |] ==>
2.17 + intros
2.18 + eval_constI:
2.19 + " [| ve \<in> ValEnv; c \<in> Const |] ==>
2.20 <ve,e_const(c),v_const(c)>:EvalRel"
2.21 - eval_varI
2.22 - " [| ve \\<in> ValEnv; x \\<in> ExVar; x \\<in> ve_dom(ve) |] ==>
2.23 + eval_varI:
2.24 + " [| ve \<in> ValEnv; x \<in> ExVar; x \<in> ve_dom(ve) |] ==>
2.25 <ve,e_var(x),ve_app(ve,x)>:EvalRel"
2.26 - eval_fnI
2.27 - " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp |] ==>
2.28 + eval_fnI:
2.29 + " [| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp |] ==>
2.30 <ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "
2.31 - eval_fixI
2.32 - " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val;
2.33 + eval_fixI:
2.34 + " [| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;
2.35 v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>
2.36 <ve,e_fix(f,x,e),cl>:EvalRel "
2.37 - eval_appI1
2.38 - " [| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const;
2.39 + eval_appI1:
2.40 + " [| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;
2.41 <ve,e1,v_const(c1)>:EvalRel;
2.42 <ve,e2,v_const(c2)>:EvalRel |] ==>
2.43 <ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
2.44 - eval_appI2
2.45 - " [| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val;
2.46 + eval_appI2:
2.47 + " [| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; v \<in> Val;
2.48 <ve,e1,v_clos(xm,em,vem)>:EvalRel;
2.49 <ve,e2,v2>:EvalRel;
2.50 <ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>
2.51 <ve,e_app(e1,e2),v>:EvalRel "
2.52 - type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
2.53 + type_intros c_appI ve_appI ve_empI ve_owrI Exp.intros Val_ValEnv.intros
2.54
2.55 -
2.56 end
3.1 --- a/src/ZF/Coind/ECR.ML Sat Dec 22 19:46:16 2001 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,64 +0,0 @@
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 -(* Specialised co-induction rule *)
3.11 -
3.12 -Goal "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv; \
3.13 -\ <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
3.14 -\ {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}: \
3.15 -\ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] \
3.16 -\ ==> <v_clos(x, e, ve),t>:HasTyRel";
3.17 -by (rtac (singletonI RS HasTyRel.coinduct) 1);
3.18 -by (ALLGOALS Blast_tac);
3.19 -qed "htr_closCI";
3.20 -
3.21 -(* Specialised elimination rules *)
3.22 -
3.23 -val htr_constE = HasTyRel.mk_cases "<v_const(c),t>:HasTyRel";
3.24 -
3.25 -val htr_closE = HasTyRel.mk_cases "<v_clos(x,e,ve),t>:HasTyRel";
3.26 -
3.27 -(* Classical reasoning sets *)
3.28 -
3.29 -fun mk_htr_cs cs =
3.30 - let open HasTyRel in
3.31 - ( cs
3.32 - addSIs [htr_constI]
3.33 - addSEs [htr_constE]
3.34 - addIs [htr_closI,htr_closCI]
3.35 - addEs [htr_closE])
3.36 - end;
3.37 -
3.38 -claset_ref() := mk_htr_cs (claset());
3.39 -
3.40 -(* Properties of the pointwise extension to environments *)
3.41 -
3.42 -bind_thm ("HasTyRel_non_zero",
3.43 - HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE);
3.44 -
3.45 -Goalw [hastyenv_def]
3.46 - "[| ve \\<in> ValEnv; te \\<in> TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
3.47 -\ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
3.48 -by (asm_full_simp_tac
3.49 - (simpset() addsimps [ve_app_owr, HasTyRel_non_zero, ve_dom_owr]) 1);
3.50 -by Auto_tac;
3.51 -qed "hastyenv_owr";
3.52 -
3.53 -Goalw [isofenv_def,hastyenv_def]
3.54 - "[| ve \\<in> ValEnv; te \\<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
3.55 -by Safe_tac;
3.56 -by (dtac bspec 1);
3.57 -by (assume_tac 1);
3.58 -by Safe_tac;
3.59 -by (dtac HasTyRel.htr_constI 1);
3.60 -by (assume_tac 2);
3.61 -by (etac te_appI 1);
3.62 -by (etac ve_domI 1);
3.63 -by (ALLGOALS Asm_full_simp_tac);
3.64 -qed "basic_consistency_lem";
3.65 -
3.66 -
3.67 -
4.1 --- a/src/ZF/Coind/ECR.thy Sat Dec 22 19:46:16 2001 +0100
4.2 +++ b/src/ZF/Coind/ECR.thy Tue Dec 25 10:02:01 2001 +0100
4.3 @@ -4,7 +4,7 @@
4.4 Copyright 1995 University of Cambridge
4.5 *)
4.6
4.7 -ECR = Static + Dynamic +
4.8 +theory ECR = Static + Dynamic:
4.9
4.10 (* The extended correspondence relation *)
4.11
4.12 @@ -12,27 +12,161 @@
4.13 HasTyRel :: i
4.14 coinductive
4.15 domains "HasTyRel" <= "Val * Ty"
4.16 - intrs
4.17 - htr_constI
4.18 - "[| c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
4.19 - htr_closI
4.20 - "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv;
4.21 - <te,e_fn(x,e),t>:ElabRel;
4.22 + intros
4.23 + htr_constI [intro!]:
4.24 + "[| c \<in> Const; t \<in> Ty; isof(c,t) |] ==> <v_const(c),t> \<in> HasTyRel"
4.25 + htr_closI [intro]:
4.26 + "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;
4.27 + <te,e_fn(x,e),t> \<in> ElabRel;
4.28 ve_dom(ve) = te_dom(te);
4.29 - {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}:Pow(HasTyRel)
4.30 - |] ==>
4.31 - <v_clos(x,e,ve),t>:HasTyRel"
4.32 + {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in> Pow(HasTyRel) |]
4.33 + ==> <v_clos(x,e,ve),t> \<in> HasTyRel"
4.34 monos Pow_mono
4.35 - type_intrs "Val_ValEnv.intrs"
4.36 + type_intros Val_ValEnv.intros
4.37
4.38 (* Pointwise extension to environments *)
4.39
4.40 -consts
4.41 - hastyenv :: [i,i] => o
4.42 -defs
4.43 - hastyenv_def
4.44 - " hastyenv(ve,te) ==
4.45 - ve_dom(ve) = te_dom(te) &
4.46 - (\\<forall>x \\<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
4.47 +constdefs
4.48 + hastyenv :: "[i,i] => o"
4.49 + "hastyenv(ve,te) ==
4.50 + ve_dom(ve) = te_dom(te) &
4.51 + (\<forall>x \<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)> \<in> HasTyRel)"
4.52 +
4.53 +(* Specialised co-induction rule *)
4.54 +
4.55 +lemma htr_closCI [intro]:
4.56 + "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;
4.57 + <te, e_fn(x, e), t> \<in> ElabRel; ve_dom(ve) = te_dom(te);
4.58 + {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
4.59 + Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]
4.60 + ==> <v_clos(x, e, ve),t> \<in> HasTyRel"
4.61 +apply (rule singletonI [THEN HasTyRel.coinduct])
4.62 +apply auto
4.63 +done
4.64 +
4.65 +(* Specialised elimination rules *)
4.66 +
4.67 +inductive_cases htr_constE [elim!]: "<v_const(c),t> \<in> HasTyRel"
4.68 +inductive_cases htr_closE [elim]: "<v_clos(x,e,ve),t> \<in> HasTyRel"
4.69 +
4.70 +
4.71 +(* Properties of the pointwise extension to environments *)
4.72 +
4.73 +lemmas HasTyRel_non_zero =
4.74 + HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE, standard]
4.75 +
4.76 +lemma hastyenv_owr:
4.77 + "[| ve \<in> ValEnv; te \<in> TyEnv; hastyenv(ve,te); <v,t> \<in> HasTyRel |]
4.78 + ==> hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"
4.79 +by (auto simp add: hastyenv_def ve_app_owr HasTyRel_non_zero)
4.80 +
4.81 +lemma basic_consistency_lem:
4.82 + "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"
4.83 +apply (unfold isofenv_def hastyenv_def)
4.84 +apply (force intro: te_appI ve_domI)
4.85 +done
4.86 +
4.87 +
4.88 +(* ############################################################ *)
4.89 +(* The Consistency theorem *)
4.90 +(* ############################################################ *)
4.91 +
4.92 +lemma consistency_const:
4.93 + "[| c \<in> Const; hastyenv(ve,te);<te,e_const(c),t> \<in> ElabRel |]
4.94 + ==> <v_const(c), t> \<in> HasTyRel"
4.95 +by blast
4.96 +
4.97 +
4.98 +lemma consistency_var:
4.99 + "[| x \<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t> \<in> ElabRel |] ==>
4.100 + <ve_app(ve,x),t> \<in> HasTyRel"
4.101 +by (unfold hastyenv_def, blast)
4.102 +
4.103 +lemma consistency_fn:
4.104 + "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; hastyenv(ve,te);
4.105 + <te,e_fn(x,e),t> \<in> ElabRel
4.106 + |] ==> <v_clos(x, e, ve), t> \<in> HasTyRel"
4.107 +by (unfold hastyenv_def, blast)
4.108 +
4.109 +declare ElabRel.dom_subset [THEN subsetD, dest]
4.110 +
4.111 +declare Ty.intros [simp, intro!]
4.112 +declare TyEnv.intros [simp, intro!]
4.113 +declare Val_ValEnv.intros [simp, intro!]
4.114 +
4.115 +lemma consistency_fix:
4.116 + "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;
4.117 + v_clos(x,e,ve_owr(ve,f,cl)) = cl;
4.118 + hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel |] ==>
4.119 + <cl,t> \<in> HasTyRel"
4.120 +apply (unfold hastyenv_def)
4.121 +apply (erule elab_fixE)
4.122 +apply safe
4.123 +apply (rule subst, assumption)
4.124 +apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
4.125 +apply simp_all
4.126 +apply (blast intro: ve_owrI)
4.127 +apply (rule ElabRel.fnI)
4.128 +apply (simp_all add: ValNEE)
4.129 +apply force
4.130 +done
4.131 +
4.132 +
4.133 +lemma consistency_app1:
4.134 + "[| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;
4.135 + <ve,e1,v_const(c1)> \<in> EvalRel;
4.136 + \<forall>t te.
4.137 + hastyenv(ve,te) --> <te,e1,t> \<in> ElabRel --> <v_const(c1),t> \<in> HasTyRel;
4.138 + <ve, e2, v_const(c2)> \<in> EvalRel;
4.139 + \<forall>t te.
4.140 + hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v_const(c2),t> \<in> HasTyRel;
4.141 + hastyenv(ve, te);
4.142 + <te,e_app(e1,e2),t> \<in> ElabRel |]
4.143 + ==> <v_const(c_app(c1, c2)),t> \<in> HasTyRel"
4.144 +by (blast intro!: c_appI intro: isof_app)
4.145 +
4.146 +lemma consistency_app2:
4.147 + "[| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar;
4.148 + v \<in> Val;
4.149 + <ve,e1,v_clos(xm,em,vem)> \<in> EvalRel;
4.150 + \<forall>t te. hastyenv(ve,te) -->
4.151 + <te,e1,t> \<in> ElabRel --> <v_clos(xm,em,vem),t> \<in> HasTyRel;
4.152 + <ve,e2,v2> \<in> EvalRel;
4.153 + \<forall>t te. hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v2,t> \<in> HasTyRel;
4.154 + <ve_owr(vem,xm,v2),em,v> \<in> EvalRel;
4.155 + \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) -->
4.156 + <te,em,t> \<in> ElabRel --> <v,t> \<in> HasTyRel;
4.157 + hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |]
4.158 + ==> <v,t> \<in> HasTyRel"
4.159 +apply (erule elab_appE)
4.160 +apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
4.161 +apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
4.162 +apply (erule htr_closE)
4.163 +apply (erule elab_fnE)
4.164 +apply simp
4.165 +apply clarify
4.166 +apply (drule spec [THEN spec, THEN mp, THEN mp])
4.167 +prefer 2 apply assumption+
4.168 +apply (rule hastyenv_owr)
4.169 +apply assumption
4.170 +apply assumption
4.171 +apply (simp add: hastyenv_def)
4.172 +apply blast+
4.173 +done
4.174 +
4.175 +lemma consistency [rule_format]:
4.176 + "<ve,e,v> \<in> EvalRel
4.177 + ==> (\<forall>t te. hastyenv(ve,te) --> <te,e,t> \<in> ElabRel --> <v,t> \<in> HasTyRel)"
4.178 +apply (erule EvalRel.induct)
4.179 +apply (simp_all add: consistency_const consistency_var consistency_fn
4.180 + consistency_fix consistency_app1)
4.181 +apply (blast intro: consistency_app2)
4.182 +done
4.183 +
4.184 +lemma basic_consistency:
4.185 + "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te);
4.186 + <ve,e,v_const(c)> \<in> EvalRel; <te,e,t> \<in> ElabRel |]
4.187 + ==> isof(c,t)"
4.188 +by (blast dest: consistency intro!: basic_consistency_lem)
4.189
4.190 end
5.1 --- a/src/ZF/Coind/Language.thy Sat Dec 22 19:46:16 2001 +0100
5.2 +++ b/src/ZF/Coind/Language.thy Tue Dec 25 10:02:01 2001 +0100
5.3 @@ -4,15 +4,17 @@
5.4 Copyright 1995 University of Cambridge
5.5 *)
5.6
5.7 -Language = Main +
5.8 +theory Language = Main:
5.9
5.10 consts
5.11 Const :: i (* Abstract type of constants *)
5.12 - c_app :: [i,i] => i (* Abstract constructor for fun application*)
5.13 + c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
5.14
5.15 -rules
5.16 - constNEE "c \\<in> Const ==> c \\<noteq> 0"
5.17 - c_appI "[| c1 \\<in> Const; c2 \\<in> Const |] ==> c_app(c1,c2):Const"
5.18 +
5.19 +text{*these really can't be definitions without losing the abstraction*}
5.20 +axioms
5.21 + constNEE: "c \<in> Const ==> c \<noteq> 0"
5.22 + c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
5.23
5.24
5.25 consts
5.26 @@ -20,10 +22,10 @@
5.27 ExVar :: i (* Abstract type of variables *)
5.28
5.29 datatype
5.30 - "Exp" = e_const ("c \\<in> Const")
5.31 - | e_var ("x \\<in> ExVar")
5.32 - | e_fn ("x \\<in> ExVar","e \\<in> Exp")
5.33 - | e_fix ("x1 \\<in> ExVar","x2 \\<in> ExVar","e \\<in> Exp")
5.34 - | e_app ("e1 \\<in> Exp","e2 \\<in> Exp")
5.35 + "Exp" = e_const ("c \<in> Const")
5.36 + | e_var ("x \<in> ExVar")
5.37 + | e_fn ("x \<in> ExVar","e \<in> Exp")
5.38 + | e_fix ("x1 \<in> ExVar","x2 \<in> ExVar","e \<in> Exp")
5.39 + | e_app ("e1 \<in> Exp","e2 \<in> Exp")
5.40
5.41 end
6.1 --- a/src/ZF/Coind/MT.ML Sat Dec 22 19:46:16 2001 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,149 +0,0 @@
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 -(* ############################################################ *)
6.11 -(* The Consistency theorem *)
6.12 -(* ############################################################ *)
6.13 -
6.14 -Goal "[| c \\<in> Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \
6.15 -\ <v_const(c), t> \\<in> HasTyRel";
6.16 -by (Fast_tac 1);
6.17 -qed "consistency_const";
6.18 -
6.19 -
6.20 -Goalw [hastyenv_def]
6.21 - "[| x \\<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
6.22 -\ <ve_app(ve,x),t>:HasTyRel";
6.23 -by (Fast_tac 1);
6.24 -qed "consistency_var";
6.25 -
6.26 -
6.27 -Goalw [hastyenv_def]
6.28 - "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; hastyenv(ve,te); \
6.29 -\ <te,e_fn(x,e),t>:ElabRel \
6.30 -\ |] ==> <v_clos(x, e, ve), t> \\<in> HasTyRel";
6.31 -by (Blast_tac 1);
6.32 -qed "consistency_fn";
6.33 -
6.34 -AddDs [te_owrE, ElabRel.dom_subset RS subsetD];
6.35 -
6.36 -Addsimps [ve_dom_owr, ve_app_owr1, ve_app_owr2,
6.37 - te_app_owr1, te_app_owr2];
6.38 -
6.39 -val clean_tac =
6.40 - REPEAT_FIRST (fn i =>
6.41 - (eq_assume_tac i) ORELSE
6.42 - (match_tac (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) i) ORELSE
6.43 - (ematch_tac [te_owrE] i));
6.44 -
6.45 -Goalw [hastyenv_def]
6.46 - "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val; \
6.47 -\ v_clos(x,e,ve_owr(ve,f,cl)) = cl; \
6.48 -\ hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==> \
6.49 -\ <cl,t>:HasTyRel";
6.50 -by (etac elab_fixE 1);
6.51 -by Safe_tac;
6.52 -by (EVERY [ftac subst 1,atac 2,rtac htr_closCI 1]);
6.53 -by clean_tac;
6.54 -by (rtac ve_owrI 1);
6.55 -by clean_tac;
6.56 -by (dtac (ElabRel.dom_subset RS subsetD) 1);
6.57 -by (eres_inst_tac [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")]
6.58 - (SigmaD1 RS te_owrE) 1);
6.59 -by (assume_tac 1);
6.60 -by (rtac ElabRel.fnI 1);
6.61 -by clean_tac;
6.62 -by (Asm_simp_tac 1);
6.63 -by (stac ve_dom_owr 1);
6.64 -by (assume_tac 1);
6.65 -by (etac subst 1);
6.66 -by (rtac v_closNE 1);
6.67 -by (Asm_simp_tac 1);
6.68 -
6.69 -by (rtac PowI 1);
6.70 -by (stac ve_dom_owr 1);
6.71 -by (assume_tac 1);
6.72 -by (etac subst 1);
6.73 -by (rtac v_closNE 1);
6.74 -by (rtac subsetI 1);
6.75 -by (etac RepFunE 1);
6.76 -by (case_tac "f=y" 1);
6.77 -by Auto_tac;
6.78 -qed "consistency_fix";
6.79 -
6.80 -
6.81 -Goal "[| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const; \
6.82 -\ <ve,e1,v_const(c1)>:EvalRel; \
6.83 -\ \\<forall>t te. \
6.84 -\ hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
6.85 -\ <ve, e2, v_const(c2)> \\<in> EvalRel; \
6.86 -\ \\<forall>t te. \
6.87 -\ hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \
6.88 -\ hastyenv(ve, te); \
6.89 -\ <te,e_app(e1,e2),t>:ElabRel |] ==> \
6.90 -\ <v_const(c_app(c1, c2)),t>:HasTyRel";
6.91 -by (etac elab_appE 1);
6.92 -by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
6.93 -qed "consistency_app1";
6.94 -
6.95 -Goal "[| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val; \
6.96 -\ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \
6.97 -\ \\<forall>t te. \
6.98 -\ hastyenv(ve,te) --> \
6.99 -\ <te,e1,t>:ElabRel --> \
6.100 -\ <v_clos(xm,em,vem),t>:HasTyRel; \
6.101 -\ <ve,e2,v2>:EvalRel; \
6.102 -\ \\<forall>t te. \
6.103 -\ hastyenv(ve,te) --> \
6.104 -\ <te,e2,t>:ElabRel --> \
6.105 -\ <v2,t>:HasTyRel; \
6.106 -\ <ve_owr(vem,xm,v2),em,v>:EvalRel; \
6.107 -\ \\<forall>t te. \
6.108 -\ hastyenv(ve_owr(vem,xm,v2),te) --> \
6.109 -\ <te,em,t>:ElabRel --> \
6.110 -\ <v,t>:HasTyRel; \
6.111 -\ hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==> \
6.112 -\ <v,t>:HasTyRel ";
6.113 -by (etac elab_appE 1);
6.114 -by (dtac (spec RS spec RS mp RS mp) 1);
6.115 -by (assume_tac 1);
6.116 -by (assume_tac 1);
6.117 -by (dtac (spec RS spec RS mp RS mp) 1);
6.118 -by (assume_tac 1);
6.119 -by (assume_tac 1);
6.120 -by (etac htr_closE 1);
6.121 -by (etac elab_fnE 1);
6.122 -by (Full_simp_tac 1);
6.123 -by (Clarify_tac 1);
6.124 -by (dtac (spec RS spec RS mp RS mp) 1);
6.125 -by (assume_tac 3);
6.126 -by (assume_tac 2);
6.127 -by (rtac hastyenv_owr 1);
6.128 -by (assume_tac 1);
6.129 -by (assume_tac 1);
6.130 -by (assume_tac 2);
6.131 -by (asm_simp_tac (simpset() addsimps [hastyenv_def]) 1);
6.132 -by (Fast_tac 1);
6.133 -qed "consistency_app2";
6.134 -
6.135 -Goal "<ve,e,v>:EvalRel ==> \
6.136 -\ (\\<forall>t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
6.137 -by (etac EvalRel.induct 1);
6.138 -by (blast_tac (claset() addIs [consistency_app2]) 6);
6.139 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1])));
6.140 -qed "consistency";
6.141 -
6.142 -
6.143 -Goal "[| ve \\<in> ValEnv; te \\<in> TyEnv; \
6.144 -\ isofenv(ve,te); \
6.145 -\ <ve,e,v_const(c)>:EvalRel; \
6.146 -\ <te,e,t>:ElabRel \
6.147 -\ |] ==> isof(c,t)";
6.148 -by (rtac htr_constE 1);
6.149 -by (dtac consistency 1);
6.150 -by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
6.151 -by (assume_tac 1);
6.152 -qed "basic_consistency";
7.1 --- a/src/ZF/Coind/MT.thy Sat Dec 22 19:46:16 2001 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,1 +0,0 @@
7.4 -MT = ECR
8.1 --- a/src/ZF/Coind/Map.ML Sat Dec 22 19:46:16 2001 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,206 +0,0 @@
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 -(** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
8.11 -
8.12 -Goalw [TMap_def] "{0,1} \\<subseteq> {1} Un TMap(I, {0,1})";
8.13 -by (Blast_tac 1);
8.14 -result();
8.15 -
8.16 -Goalw [TMap_def] "{0} Un TMap(I,1) \\<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))";
8.17 -by (Blast_tac 1);
8.18 -result();
8.19 -
8.20 -Goalw [TMap_def] "{0,1} Un TMap(I,2) \\<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))";
8.21 -by (Blast_tac 1);
8.22 -result();
8.23 -
8.24 -(*
8.25 -Goalw [TMap_def]
8.26 - "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \\<subseteq> \
8.27 -\ {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
8.28 -by (Blast_tac 1);
8.29 -result();
8.30 -*)
8.31 -
8.32 -
8.33 -(* ############################################################ *)
8.34 -(* Lemmas *)
8.35 -(* ############################################################ *)
8.36 -
8.37 -Goal "Sigma(A,B)``{a} = (if a \\<in> A then B(a) else 0)";
8.38 -by Auto_tac;
8.39 -qed "qbeta_if";
8.40 -
8.41 -Goal "a \\<in> A ==> Sigma(A,B)``{a} = B(a)";
8.42 -by (Fast_tac 1);
8.43 -qed "qbeta";
8.44 -
8.45 -Goal "a\\<notin>A ==> Sigma(A,B)``{a} = 0";
8.46 -by (Fast_tac 1);
8.47 -qed "qbeta_emp";
8.48 -
8.49 -Goal "a \\<notin> A ==> Sigma(A,B)``{a}=0";
8.50 -by (Fast_tac 1);
8.51 -qed "image_Sigma1";
8.52 -
8.53 -
8.54 -(* ############################################################ *)
8.55 -(* Inclusion in Quine Universes *)
8.56 -(* ############################################################ *)
8.57 -
8.58 -(* Lemmas *)
8.59 -
8.60 -Goalw [quniv_def]
8.61 - "A \\<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \\<subseteq> quniv(X)";
8.62 -by (rtac Pow_mono 1);
8.63 -by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
8.64 -by (etac subset_trans 1);
8.65 -by (rtac (arg_subset_eclose RS univ_mono) 1);
8.66 -by (simp_tac (simpset() addsimps [Union_Pow_eq]) 1);
8.67 -qed "MapQU_lemma";
8.68 -
8.69 -(* Theorems *)
8.70 -
8.71 -val prems = goalw Map.thy [PMap_def,TMap_def]
8.72 - "[| m \\<in> PMap(A,quniv(B)); !!x. x \\<in> A ==> x \\<in> univ(B) |] ==> m \\<in> quniv(B)";
8.73 -by (cut_facts_tac prems 1);
8.74 -by (rtac (MapQU_lemma RS subsetD) 1);
8.75 -by (rtac subsetI 1);
8.76 -by (eresolve_tac prems 1);
8.77 -by (Fast_tac 1);
8.78 -qed "mapQU";
8.79 -
8.80 -(* ############################################################ *)
8.81 -(* Monotonicity *)
8.82 -(* ############################################################ *)
8.83 -
8.84 -Goalw [PMap_def,TMap_def] "B \\<subseteq> C ==> PMap(A,B)<=PMap(A,C)";
8.85 -by (Blast_tac 1);
8.86 -qed "map_mono";
8.87 -
8.88 -(* Rename to pmap_mono *)
8.89 -
8.90 -(* ############################################################ *)
8.91 -(* Introduction Rules *)
8.92 -(* ############################################################ *)
8.93 -
8.94 -(** map_emp **)
8.95 -
8.96 -Goalw [map_emp_def,PMap_def,TMap_def] "map_emp \\<in> PMap(A,B)";
8.97 -by Auto_tac;
8.98 -qed "pmap_empI";
8.99 -
8.100 -(** map_owr **)
8.101 -
8.102 -
8.103 -Goalw [map_owr_def,PMap_def,TMap_def]
8.104 - "[| m \\<in> PMap(A,B); a \\<in> A; b \\<in> B |] ==> map_owr(m,a,b):PMap(A,B)";
8.105 -by Safe_tac;
8.106 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [if_iff])));
8.107 -by (Fast_tac 1);
8.108 -by (Fast_tac 1);
8.109 -by (Deepen_tac 2 1);
8.110 -(*Remaining subgoal*)
8.111 -by (rtac (excluded_middle RS disjE) 1);
8.112 -by (etac image_Sigma1 1);
8.113 -by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 1);
8.114 -by (asm_full_simp_tac (simpset() addsimps [qbeta]) 1);
8.115 -by Safe_tac;
8.116 -by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 3);
8.117 -by (ALLGOALS Asm_full_simp_tac);
8.118 -by (Fast_tac 1);
8.119 -qed "pmap_owrI";
8.120 -
8.121 -(** map_app **)
8.122 -
8.123 -Goalw [TMap_def,map_app_def]
8.124 - "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a) \\<noteq>0";
8.125 -by (etac domainE 1);
8.126 -by (dtac imageI 1);
8.127 -by (Fast_tac 1);
8.128 -by (etac not_emptyI 1);
8.129 -qed "tmap_app_notempty";
8.130 -
8.131 -Goalw [TMap_def,map_app_def,domain_def]
8.132 - "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
8.133 -by (Fast_tac 1);
8.134 -qed "tmap_appI";
8.135 -
8.136 -Goalw [PMap_def]
8.137 - "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
8.138 -by (ftac tmap_app_notempty 1);
8.139 -by (assume_tac 1);
8.140 -by (dtac tmap_appI 1);
8.141 -by (assume_tac 1);
8.142 -by (Fast_tac 1);
8.143 -qed "pmap_appI";
8.144 -
8.145 -(** domain **)
8.146 -
8.147 -Goalw [TMap_def]
8.148 - "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
8.149 -by (Fast_tac 1);
8.150 -qed "tmap_domainD";
8.151 -
8.152 -Goalw [PMap_def,TMap_def]
8.153 - "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
8.154 -by (Fast_tac 1);
8.155 -qed "pmap_domainD";
8.156 -
8.157 -(* ############################################################ *)
8.158 -(* Equalities *)
8.159 -(* ############################################################ *)
8.160 -
8.161 -(** Domain **)
8.162 -
8.163 -(* Lemmas *)
8.164 -
8.165 -Goal "domain(\\<Union>x \\<in> A. B(x)) = (\\<Union>x \\<in> A. domain(B(x)))";
8.166 -by (Fast_tac 1);
8.167 -qed "domain_UN";
8.168 -
8.169 -Goal "domain(Sigma(A,B)) = {x \\<in> A. \\<exists>y. y \\<in> B(x)}";
8.170 -by (simp_tac (simpset() addsimps [domain_UN,domain_0,domain_cons]) 1);
8.171 -by (Fast_tac 1);
8.172 -qed "domain_Sigma";
8.173 -
8.174 -(* Theorems *)
8.175 -
8.176 -Goalw [map_emp_def] "domain(map_emp) = 0";
8.177 -by (Fast_tac 1);
8.178 -qed "map_domain_emp";
8.179 -
8.180 -Goalw [map_owr_def]
8.181 - "b \\<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
8.182 -by (simp_tac (simpset() addsimps [domain_Sigma]) 1);
8.183 -by (rtac equalityI 1);
8.184 -by (Fast_tac 1);
8.185 -by (rtac subsetI 1);
8.186 -by (rtac CollectI 1);
8.187 -by (assume_tac 1);
8.188 -by (etac UnE' 1);
8.189 -by (etac singletonE 1);
8.190 -by (Asm_simp_tac 1);
8.191 -by (Fast_tac 1);
8.192 -by (fast_tac (claset() addss (simpset())) 1);
8.193 -qed "map_domain_owr";
8.194 -
8.195 -(** Application **)
8.196 -
8.197 -Goalw [map_app_def,map_owr_def]
8.198 - "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))";
8.199 -by (asm_simp_tac (simpset() addsimps [qbeta_if]) 1);
8.200 -by (Fast_tac 1);
8.201 -qed "map_app_owr";
8.202 -
8.203 -Goal "map_app(map_owr(f,a,b),a) = b";
8.204 -by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
8.205 -qed "map_app_owr1";
8.206 -
8.207 -Goal "c \\<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
8.208 -by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
8.209 -qed "map_app_owr2";
9.1 --- a/src/ZF/Coind/Map.thy Sat Dec 22 19:46:16 2001 +0100
9.2 +++ b/src/ZF/Coind/Map.thy Tue Dec 25 10:02:01 2001 +0100
9.3 @@ -2,25 +2,185 @@
9.4 ID: $Id$
9.5 Author: Jacob Frost, Cambridge University Computer Laboratory
9.6 Copyright 1995 University of Cambridge
9.7 +
9.8 +
9.9 +Some sample proofs of inclusions for the final coalgebra "U" (by lcp)
9.10 +
9.11 *)
9.12
9.13 -Map = Main +
9.14 +theory Map = Main:
9.15
9.16 constdefs
9.17 - TMap :: [i,i] => i
9.18 - "TMap(A,B) == {m \\<in> Pow(A*Union(B)).\\<forall>a \\<in> A. m``{a} \\<in> B}"
9.19 + TMap :: "[i,i] => i"
9.20 + "TMap(A,B) == {m \<in> Pow(A*Union(B)).\<forall>a \<in> A. m``{a} \<in> B}"
9.21
9.22 - PMap :: [i,i] => i
9.23 + PMap :: "[i,i] => i"
9.24 "PMap(A,B) == TMap(A,cons(0,B))"
9.25
9.26 -(* Note: 0 \\<in> B ==> TMap(A,B) = PMap(A,B) *)
9.27 +(* Note: 0 \<in> B ==> TMap(A,B) = PMap(A,B) *)
9.28
9.29 map_emp :: i
9.30 "map_emp == 0"
9.31
9.32 - map_owr :: [i,i,i]=>i
9.33 - "map_owr(m,a,b) == \\<Sigma>x \\<in> {a} Un domain(m). if x=a then b else m``{x}"
9.34 - map_app :: [i,i]=>i
9.35 + map_owr :: "[i,i,i]=>i"
9.36 + "map_owr(m,a,b) == \<Sigma>x \<in> {a} Un domain(m). if x=a then b else m``{x}"
9.37 +
9.38 + map_app :: "[i,i]=>i"
9.39 "map_app(m,a) == m``{a}"
9.40
9.41 +lemma "{0,1} \<subseteq> {1} Un TMap(I, {0,1})"
9.42 +by (unfold TMap_def, blast)
9.43 +
9.44 +lemma "{0} Un TMap(I,1) \<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))"
9.45 +by (unfold TMap_def, blast)
9.46 +
9.47 +lemma "{0,1} Un TMap(I,2) \<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))"
9.48 +by (unfold TMap_def, blast)
9.49 +
9.50 +(*A bit too slow.
9.51 +lemma "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \<subseteq>
9.52 + {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))"
9.53 +by (unfold TMap_def, blast)
9.54 +*)
9.55 +
9.56 +(* ############################################################ *)
9.57 +(* Lemmas *)
9.58 +(* ############################################################ *)
9.59 +
9.60 +lemma qbeta_if: "Sigma(A,B)``{a} = (if a \<in> A then B(a) else 0)"
9.61 +by auto
9.62 +
9.63 +lemma qbeta: "a \<in> A ==> Sigma(A,B)``{a} = B(a)"
9.64 +by fast
9.65 +
9.66 +lemma qbeta_emp: "a\<notin>A ==> Sigma(A,B)``{a} = 0"
9.67 +by fast
9.68 +
9.69 +lemma image_Sigma1: "a \<notin> A ==> Sigma(A,B)``{a}=0"
9.70 +by fast
9.71 +
9.72 +
9.73 +(* ############################################################ *)
9.74 +(* Inclusion in Quine Universes *)
9.75 +(* ############################################################ *)
9.76 +
9.77 +(* Lemmas *)
9.78 +
9.79 +lemma MapQU_lemma:
9.80 + "A \<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \<subseteq> quniv(X)"
9.81 +apply (unfold quniv_def)
9.82 +apply (rule Pow_mono)
9.83 +apply (rule subset_trans [OF Sigma_mono product_univ])
9.84 +apply (erule subset_trans)
9.85 +apply (rule arg_subset_eclose [THEN univ_mono])
9.86 +apply (simp add: Union_Pow_eq)
9.87 +done
9.88 +
9.89 +(* Theorems *)
9.90 +
9.91 +lemma mapQU:
9.92 + "[| m \<in> PMap(A,quniv(B)); !!x. x \<in> A ==> x \<in> univ(B) |] ==> m \<in> quniv(B)"
9.93 +apply (unfold PMap_def TMap_def)
9.94 +apply (blast intro!: MapQU_lemma [THEN subsetD])
9.95 +done
9.96 +
9.97 +(* ############################################################ *)
9.98 +(* Monotonicity *)
9.99 +(* ############################################################ *)
9.100 +
9.101 +lemma PMap_mono: "B \<subseteq> C ==> PMap(A,B)<=PMap(A,C)"
9.102 +by (unfold PMap_def TMap_def, blast)
9.103 +
9.104 +
9.105 +(* ############################################################ *)
9.106 +(* Introduction Rules *)
9.107 +(* ############################################################ *)
9.108 +
9.109 +(** map_emp **)
9.110 +
9.111 +lemma pmap_empI: "map_emp \<in> PMap(A,B)"
9.112 +by (unfold map_emp_def PMap_def TMap_def, auto)
9.113 +
9.114 +(** map_owr **)
9.115 +
9.116 +lemma pmap_owrI:
9.117 + "[| m \<in> PMap(A,B); a \<in> A; b \<in> B |] ==> map_owr(m,a,b):PMap(A,B)"
9.118 +apply (unfold map_owr_def PMap_def TMap_def)
9.119 +apply safe
9.120 +apply (simp_all add: if_iff)
9.121 +apply auto
9.122 +(*Remaining subgoal*)
9.123 +apply (rule excluded_middle [THEN disjE])
9.124 +apply (erule image_Sigma1)
9.125 +apply (drule_tac psi = "?uu \<notin> B" in asm_rl)
9.126 +apply (auto simp add: qbeta)
9.127 +done
9.128 +
9.129 +(** map_app **)
9.130 +
9.131 +lemma tmap_app_notempty:
9.132 + "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a) \<noteq>0"
9.133 +by (unfold TMap_def map_app_def, blast)
9.134 +
9.135 +lemma tmap_appI:
9.136 + "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
9.137 +by (unfold TMap_def map_app_def domain_def, blast)
9.138 +
9.139 +lemma pmap_appI:
9.140 + "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
9.141 +apply (unfold PMap_def)
9.142 +apply (frule tmap_app_notempty, assumption)
9.143 +apply (drule tmap_appI)
9.144 +apply auto
9.145 +done
9.146 +
9.147 +(** domain **)
9.148 +
9.149 +lemma tmap_domainD:
9.150 + "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> a \<in> A"
9.151 +by (unfold TMap_def, blast)
9.152 +
9.153 +lemma pmap_domainD:
9.154 + "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> a \<in> A"
9.155 +by (unfold PMap_def TMap_def, blast)
9.156 +
9.157 +
9.158 +(* ############################################################ *)
9.159 +(* Equalities *)
9.160 +(* ############################################################ *)
9.161 +
9.162 +(** Domain **)
9.163 +
9.164 +(* Lemmas *)
9.165 +
9.166 +lemma domain_UN: "domain(\<Union>x \<in> A. B(x)) = (\<Union>x \<in> A. domain(B(x)))"
9.167 +by fast
9.168 +
9.169 +
9.170 +lemma domain_Sigma: "domain(Sigma(A,B)) = {x \<in> A. \<exists>y. y \<in> B(x)}"
9.171 +by blast
9.172 +
9.173 +(* Theorems *)
9.174 +
9.175 +lemma map_domain_emp: "domain(map_emp) = 0"
9.176 +by (unfold map_emp_def, blast)
9.177 +
9.178 +lemma map_domain_owr:
9.179 + "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"
9.180 +apply (unfold map_owr_def)
9.181 +apply (auto simp add: domain_Sigma)
9.182 +done
9.183 +
9.184 +(** Application **)
9.185 +
9.186 +lemma map_app_owr:
9.187 + "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))"
9.188 +by (simp add: qbeta_if map_app_def map_owr_def, blast)
9.189 +
9.190 +lemma map_app_owr1: "map_app(map_owr(f,a,b),a) = b"
9.191 +by (simp add: map_app_owr)
9.192 +
9.193 +lemma map_app_owr2: "c \<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"
9.194 +by (simp add: map_app_owr)
9.195 +
9.196 end
10.1 --- a/src/ZF/Coind/ROOT.ML Sat Dec 22 19:46:16 2001 +0100
10.2 +++ b/src/ZF/Coind/ROOT.ML Tue Dec 25 10:02:01 2001 +0100
10.3 @@ -13,4 +13,4 @@
10.4 Report, Computer Lab, University of Cambridge (1995).
10.5 *)
10.6
10.7 -time_use_thy "MT";
10.8 +time_use_thy "ECR";
11.1 --- a/src/ZF/Coind/Static.ML Sat Dec 22 19:46:16 2001 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,25 +0,0 @@
11.4 -(* Title: ZF/Coind/Static.ML
11.5 - ID: $Id$
11.6 - Author: Jacob Frost, Cambridge University Computer Laboratory
11.7 - Copyright 1995 University of Cambridge
11.8 -*)
11.9 -
11.10 -val elab_constE = ElabRel.mk_cases "<te,e_const(c),t>:ElabRel";
11.11 -
11.12 -val elab_varE = ElabRel.mk_cases "<te,e_var(x),t>:ElabRel";
11.13 -
11.14 -val elab_fnE = ElabRel.mk_cases "<te,e_fn(x,e),t>:ElabRel";
11.15 -
11.16 -val elab_fixE = ElabRel.mk_cases "<te,e_fix(f,x,e),t>:ElabRel";
11.17 -
11.18 -val elab_appE = ElabRel.mk_cases "<te,e_app(e1,e2),t>:ElabRel";
11.19 -
11.20 -AddSEs [elab_constE, elab_varE, elab_fixE];
11.21 -
11.22 -AddSIs [ElabRel.constI, ElabRel.varI, ElabRel.fnI, ElabRel.fixI];
11.23 -
11.24 -AddIs [ElabRel.appI];
11.25 -
11.26 -AddEs [elab_appE, elab_fnE];
11.27 -
11.28 -AddDs [ElabRel.dom_subset RS subsetD];
12.1 --- a/src/ZF/Coind/Static.thy Sat Dec 22 19:46:16 2001 +0100
12.2 +++ b/src/ZF/Coind/Static.thy Tue Dec 25 10:02:01 2001 +0100
12.3 @@ -4,33 +4,63 @@
12.4 Copyright 1995 University of Cambridge
12.5 *)
12.6
12.7 -Static = BCR +
12.8 +theory Static = Values + Types:
12.9 +
12.10 +(*** Basic correspondence relation -- not completely specified, as it is a
12.11 + parameter of the proof. A concrete version could be defined inductively.
12.12 +***)
12.13 +
12.14 +consts
12.15 + isof :: "[i,i] => o"
12.16 +
12.17 +axioms
12.18 + isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
12.19 +
12.20 +(*Its extension to environments*)
12.21 +
12.22 +constdefs
12.23 + isofenv :: "[i,i] => o"
12.24 + "isofenv(ve,te) ==
12.25 + ve_dom(ve) = te_dom(te) &
12.26 + (\<forall>x \<in> ve_dom(ve).
12.27 + \<exists>c \<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
12.28 +
12.29 +
12.30 +(*** Elaboration ***)
12.31
12.32 consts ElabRel :: i
12.33
12.34 inductive
12.35 domains "ElabRel" <= "TyEnv * Exp * Ty"
12.36 - intrs
12.37 - constI
12.38 - " [| te \\<in> TyEnv; c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==>
12.39 - <te,e_const(c),t>:ElabRel "
12.40 - varI
12.41 - " [| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==>
12.42 - <te,e_var(x),te_app(te,x)>:ElabRel "
12.43 - fnI
12.44 - " [| te \\<in> TyEnv; x \\<in> ExVar; e \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;
12.45 - <te_owr(te,x,t1),e,t2>:ElabRel |] ==>
12.46 - <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
12.47 - fixI
12.48 - " [| te \\<in> TyEnv; f \\<in> ExVar; x \\<in> ExVar; t1 \\<in> Ty; t2 \\<in> Ty;
12.49 - <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>
12.50 - <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
12.51 - appI
12.52 - " [| te \\<in> TyEnv; e1 \\<in> Exp; e2 \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;
12.53 - <te,e1,t_fun(t1,t2)>:ElabRel;
12.54 - <te,e2,t1>:ElabRel |] ==>
12.55 - <te,e_app(e1,e2),t2>:ElabRel "
12.56 - type_intrs "te_appI::Exp.intrs@Ty.intrs"
12.57 + intros
12.58 + constI [intro!]:
12.59 + "[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==>
12.60 + <te,e_const(c),t> \<in> ElabRel"
12.61 + varI [intro!]:
12.62 + "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==>
12.63 + <te,e_var(x),te_app(te,x)> \<in> ElabRel"
12.64 + fnI [intro!]:
12.65 + "[| te \<in> TyEnv; x \<in> ExVar; e \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;
12.66 + <te_owr(te,x,t1),e,t2> \<in> ElabRel |] ==>
12.67 + <te,e_fn(x,e),t_fun(t1,t2)> \<in> ElabRel"
12.68 + fixI [intro!]:
12.69 + "[| te \<in> TyEnv; f \<in> ExVar; x \<in> ExVar; t1 \<in> Ty; t2 \<in> Ty;
12.70 + <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> \<in> ElabRel |] ==>
12.71 + <te,e_fix(f,x,e),t_fun(t1,t2)> \<in> ElabRel"
12.72 + appI [intro]:
12.73 + "[| te \<in> TyEnv; e1 \<in> Exp; e2 \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;
12.74 + <te,e1,t_fun(t1,t2)> \<in> ElabRel;
12.75 + <te,e2,t1> \<in> ElabRel |] ==> <te,e_app(e1,e2),t2> \<in> ElabRel"
12.76 + type_intros te_appI Exp.intros Ty.intros
12.77 +
12.78 +
12.79 +inductive_cases elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
12.80 +inductive_cases elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel"
12.81 +inductive_cases elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel"
12.82 +inductive_cases elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
12.83 +inductive_cases elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel"
12.84 +
12.85 +declare ElabRel.dom_subset [THEN subsetD, dest]
12.86
12.87 end
12.88
13.1 --- a/src/ZF/Coind/Types.ML Sat Dec 22 19:46:16 2001 +0100
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,43 +0,0 @@
13.4 -(* Title: ZF/Coind/Types.ML
13.5 - ID: $Id$
13.6 - Author: Jacob Frost, Cambridge University Computer Laboratory
13.7 - Copyright 1995 University of Cambridge
13.8 -*)
13.9 -
13.10 -val te_owrE = TyEnv.mk_cases "te_owr(te,f,t):TyEnv";
13.11 -
13.12 -Goal "te_app(te_owr(te,x,t),x) = t";
13.13 -by (Simp_tac 1);
13.14 -qed "te_app_owr1";
13.15 -
13.16 -Goal "x \\<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
13.17 -by Auto_tac;
13.18 -qed "te_app_owr2";
13.19 -
13.20 -Goal "[| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==> te_app(te,x):Ty";
13.21 -by (res_inst_tac [("P","x \\<in> te_dom(te)")] impE 1);
13.22 -by (assume_tac 2);
13.23 -by (assume_tac 2);
13.24 -by (etac TyEnv.induct 1);
13.25 -by (Simp_tac 1);
13.26 -by (case_tac "xa = x" 1);
13.27 -by Auto_tac;
13.28 -qed "te_appI";
13.29 -
13.30 -
13.31 -
13.32 -
13.33 -
13.34 -
13.35 -
13.36 -
13.37 -
13.38 -
13.39 -
13.40 -
13.41 -
13.42 -
13.43 -
13.44 -
13.45 -
13.46 -
14.1 --- a/src/ZF/Coind/Types.thy Sat Dec 22 19:46:16 2001 +0100
14.2 +++ b/src/ZF/Coind/Types.thy Tue Dec 25 10:02:01 2001 +0100
14.3 @@ -4,15 +4,15 @@
14.4 Copyright 1995 University of Cambridge
14.5 *)
14.6
14.7 -Types = Language +
14.8 +theory Types = Language:
14.9
14.10 consts
14.11 - Ty :: i (* Datatype of types *)
14.12 + Ty :: i (* Datatype of types *)
14.13 TyConst :: i (* Abstract type of type constants *)
14.14
14.15 datatype
14.16 - "Ty" = t_const ("tc \\<in> TyConst")
14.17 - | t_fun ("t1 \\<in> Ty","t2 \\<in> Ty")
14.18 + "Ty" = t_const ("tc \<in> TyConst")
14.19 + | t_fun ("t1 \<in> Ty","t2 \<in> Ty")
14.20
14.21
14.22 (* Definition of type environments and associated operators *)
14.23 @@ -22,24 +22,57 @@
14.24
14.25 datatype
14.26 "TyEnv" = te_emp
14.27 - | te_owr ("te \\<in> TyEnv","x \\<in> ExVar","t \\<in> Ty")
14.28 + | te_owr ("te \<in> TyEnv","x \<in> ExVar","t \<in> Ty")
14.29
14.30 consts
14.31 - te_dom :: i => i
14.32 - te_app :: [i,i] => i
14.33 + te_dom :: "i => i"
14.34 + te_app :: "[i,i] => i"
14.35
14.36
14.37 primrec (*domain of the type environment*)
14.38 "te_dom (te_emp) = 0"
14.39 - "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"
14.40 + "te_dom (te_owr(te,x,v)) = te_dom(te) Un {x}"
14.41
14.42 primrec (*lookup up identifiers in the type environment*)
14.43 "te_app (te_emp,x) = 0"
14.44 "te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"
14.45
14.46 +inductive_cases te_owrE [elim!]: "te_owr(te,f,t) \<in> TyEnv"
14.47 +
14.48 +(*redundant??*)
14.49 +lemma te_app_owr1: "te_app(te_owr(te,x,t),x) = t"
14.50 +by simp
14.51 +
14.52 +(*redundant??*)
14.53 +lemma te_app_owr2: "x \<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"
14.54 +by auto
14.55 +
14.56 +lemma te_app_owr [simp]:
14.57 + "te_app(te_owr(te,x,t),y) = (if x=y then t else te_app(te,y))"
14.58 +by auto
14.59 +
14.60 +lemma te_appI:
14.61 + "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> te_app(te,x) \<in> Ty"
14.62 +apply (erule_tac P = "x \<in> te_dom (te) " in rev_mp)
14.63 +apply (erule TyEnv.induct)
14.64 +apply auto
14.65 +done
14.66 +
14.67 +
14.68 +
14.69 +
14.70 +
14.71 +
14.72 +
14.73 +
14.74 +
14.75 +
14.76 +
14.77 +
14.78 +
14.79 +
14.80 +
14.81 +
14.82 +
14.83 +
14.84 end
14.85 -
14.86 -
14.87 -
14.88 -
14.89 -
15.1 --- a/src/ZF/Coind/Values.ML Sat Dec 22 19:46:16 2001 +0100
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,131 +0,0 @@
15.4 -(* Title: ZF/Coind/Values.ML
15.5 - ID: $Id$
15.6 - Author: Jacob Frost, Cambridge University Computer Laboratory
15.7 - Copyright 1995 University of Cambridge
15.8 -*)
15.9 -
15.10 -open Values;
15.11 -
15.12 -(* Elimination rules *)
15.13 -
15.14 -val prems = goalw Values.thy (Part_def::(tl (tl Val_ValEnv.defs)))
15.15 - "[| ve \\<in> ValEnv; !!m.[| ve=ve_mk(m); m \\<in> PMap(ExVar,Val) |] ==> Q |] ==> Q";
15.16 -by (cut_facts_tac prems 1);
15.17 -by (etac CollectE 1);
15.18 -by (etac exE 1);
15.19 -by (etac Val_ValEnv.elim 1);
15.20 -by (eresolve_tac prems 3);
15.21 -by (rewrite_tac Val_ValEnv.con_defs);
15.22 -by (ALLGOALS Fast_tac);
15.23 -qed "ValEnvE";
15.24 -
15.25 -val prems = goalw Values.thy (Part_def::[hd (tl Val_ValEnv.defs)])
15.26 - "[| v \\<in> Val; \
15.27 -\ !!c. [| v = v_const(c); c \\<in> Const |] ==> Q;\
15.28 -\ !!e ve x. \
15.29 -\ [| v = v_clos(x,e,ve); x \\<in> ExVar; e \\<in> Exp; ve \\<in> ValEnv |] ==> Q \
15.30 -\ |] ==> \
15.31 -\ Q";
15.32 -by (cut_facts_tac prems 1);
15.33 -by (etac CollectE 1);
15.34 -by (etac exE 1);
15.35 -by (etac Val_ValEnv.elim 1);
15.36 -by (eresolve_tac prems 1);
15.37 -by (assume_tac 1);
15.38 -by (eresolve_tac prems 1);
15.39 -by (assume_tac 1);
15.40 -by (assume_tac 1);
15.41 -by (assume_tac 1);
15.42 -by (rewrite_tac Val_ValEnv.con_defs);
15.43 -by (Fast_tac 1);
15.44 -qed "ValE";
15.45 -
15.46 -(* Nonempty sets *)
15.47 -
15.48 -Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
15.49 - "v_clos(x,e,ve) \\<noteq> 0";
15.50 -by (Blast_tac 1);
15.51 -qed "v_closNE";
15.52 -
15.53 -Addsimps [v_closNE];
15.54 -AddSEs [v_closNE RS notE];
15.55 -
15.56 -Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
15.57 - "c \\<in> Const ==> v_const(c) \\<noteq> 0";
15.58 -by (dtac constNEE 1);
15.59 -by Auto_tac;
15.60 -qed "v_constNE";
15.61 -
15.62 -Addsimps [v_constNE];
15.63 -
15.64 -(* Proving that the empty set is not a value *)
15.65 -
15.66 -Goal "v \\<in> Val ==> v \\<noteq> 0";
15.67 -by (etac ValE 1);
15.68 -by Auto_tac;
15.69 -qed "ValNEE";
15.70 -
15.71 -(* Equalities for value environments *)
15.72 -
15.73 -Goal "[| ve \\<in> ValEnv; v \\<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
15.74 -by (etac ValEnvE 1);
15.75 -by (auto_tac (claset(),
15.76 - simpset() addsimps [map_domain_owr]));
15.77 -qed "ve_dom_owr";
15.78 -
15.79 -Goal "ve \\<in> ValEnv \
15.80 -\ ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))";
15.81 -by (etac ValEnvE 1);
15.82 -by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
15.83 -qed "ve_app_owr";
15.84 -
15.85 -Goal "ve \\<in> ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v";
15.86 -by (etac ValEnvE 1);
15.87 -by (Asm_full_simp_tac 1);
15.88 -by (rtac map_app_owr1 1);
15.89 -qed "ve_app_owr1";
15.90 -
15.91 -Goal "ve \\<in> ValEnv ==> x \\<noteq> y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
15.92 -by (etac ValEnvE 1);
15.93 -by (Asm_full_simp_tac 1);
15.94 -by (rtac map_app_owr2 1);
15.95 -by (Fast_tac 1);
15.96 -qed "ve_app_owr2";
15.97 -
15.98 -(* Introduction rules for operators on value environments *)
15.99 -
15.100 -Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> ve_app(ve,x):Val";
15.101 -by (etac ValEnvE 1);
15.102 -by (hyp_subst_tac 1);
15.103 -by (Asm_full_simp_tac 1);
15.104 -by (rtac pmap_appI 1);
15.105 -by (assume_tac 1);
15.106 -by (assume_tac 1);
15.107 -qed "ve_appI";
15.108 -
15.109 -Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> x \\<in> ExVar";
15.110 -by (etac ValEnvE 1);
15.111 -by (hyp_subst_tac 1);
15.112 -by (Asm_full_simp_tac 1);
15.113 -by (rtac pmap_domainD 1);
15.114 -by (assume_tac 1);
15.115 -by (assume_tac 1);
15.116 -qed "ve_domI";
15.117 -
15.118 -Goalw [ve_emp_def] "ve_emp \\<in> ValEnv";
15.119 -by (rtac Val_ValEnv.ve_mk_I 1);
15.120 -by (rtac pmap_empI 1);
15.121 -qed "ve_empI";
15.122 -
15.123 -Goal "[|ve \\<in> ValEnv; x \\<in> ExVar; v \\<in> Val |] ==> ve_owr(ve,x,v):ValEnv";
15.124 -by (etac ValEnvE 1);
15.125 -by (hyp_subst_tac 1);
15.126 -by (Asm_full_simp_tac 1);
15.127 -by (rtac Val_ValEnv.ve_mk_I 1);
15.128 -by (etac pmap_owrI 1);
15.129 -by (assume_tac 1);
15.130 -by (assume_tac 1);
15.131 -qed "ve_owrI";
15.132 -
15.133 -
15.134 -
16.1 --- a/src/ZF/Coind/Values.thy Sat Dec 22 19:46:16 2001 +0100
16.2 +++ b/src/ZF/Coind/Values.thy Tue Dec 25 10:02:01 2001 +0100
16.3 @@ -4,25 +4,27 @@
16.4 Copyright 1995 University of Cambridge
16.5 *)
16.6
16.7 -Values = Language + Map +
16.8 +theory Values = Language + Map:
16.9
16.10 (* Values, values environments and associated operators *)
16.11
16.12 consts
16.13 - Val, ValEnv, Val_ValEnv :: i
16.14 + Val :: i
16.15 + ValEnv :: i
16.16 + Val_ValEnv :: i;
16.17
16.18 codatatype
16.19 - "Val" = v_const ("c \\<in> Const")
16.20 - | v_clos ("x \\<in> ExVar","e \\<in> Exp","ve \\<in> ValEnv")
16.21 + "Val" = v_const ("c \<in> Const")
16.22 + | v_clos ("x \<in> ExVar","e \<in> Exp","ve \<in> ValEnv")
16.23 and
16.24 - "ValEnv" = ve_mk ("m \\<in> PMap(ExVar,Val)")
16.25 - monos map_mono
16.26 - type_intrs A_into_univ, mapQU
16.27 + "ValEnv" = ve_mk ("m \<in> PMap(ExVar,Val)")
16.28 + monos PMap_mono
16.29 + type_intros A_into_univ mapQU
16.30
16.31 consts
16.32 - ve_owr :: [i,i,i] => i
16.33 - ve_dom :: i=>i
16.34 - ve_app :: [i,i] => i
16.35 + ve_owr :: "[i,i,i] => i"
16.36 + ve_dom :: "i=>i"
16.37 + ve_app :: "[i,i] => i"
16.38
16.39
16.40 primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))"
16.41 @@ -35,7 +37,87 @@
16.42 ve_emp :: i
16.43 "ve_emp == ve_mk(map_emp)"
16.44
16.45 +
16.46 +(* Elimination rules *)
16.47 +
16.48 +lemma ValEnvE:
16.49 + "[| ve \<in> ValEnv; !!m.[| ve=ve_mk(m); m \<in> PMap(ExVar,Val) |] ==> Q |] ==> Q"
16.50 +apply (unfold Part_def Val_def ValEnv_def)
16.51 +apply (clarify );
16.52 +apply (erule Val_ValEnv.cases)
16.53 +apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs)
16.54 +done
16.55 +
16.56 +lemma ValE:
16.57 + "[| v \<in> Val;
16.58 + !!c. [| v = v_const(c); c \<in> Const |] ==> Q;
16.59 + !!e ve x.
16.60 + [| v = v_clos(x,e,ve); x \<in> ExVar; e \<in> Exp; ve \<in> ValEnv |] ==> Q
16.61 + |] ==>
16.62 + Q"
16.63 +apply (unfold Part_def Val_def ValEnv_def)
16.64 +apply (clarify );
16.65 +apply (erule Val_ValEnv.cases)
16.66 +apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs);
16.67 +done
16.68 +
16.69 +(* Nonempty sets *)
16.70 +
16.71 +lemma v_closNE [simp]: "v_clos(x,e,ve) \<noteq> 0"
16.72 +apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
16.73 +apply blast
16.74 +done
16.75 +
16.76 +declare v_closNE [THEN notE, elim!]
16.77 +
16.78 +
16.79 +lemma v_constNE [simp]: "c \<in> Const ==> v_const(c) \<noteq> 0"
16.80 +apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
16.81 +apply (drule constNEE)
16.82 +apply auto
16.83 +done
16.84 +
16.85 +
16.86 +(* Proving that the empty set is not a value *)
16.87 +
16.88 +lemma ValNEE: "v \<in> Val ==> v \<noteq> 0"
16.89 +by (erule ValE, auto)
16.90 +
16.91 +(* Equalities for value environments *)
16.92 +
16.93 +lemma ve_dom_owr [simp]:
16.94 + "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"
16.95 +apply (erule ValEnvE)
16.96 +apply (auto simp add: map_domain_owr)
16.97 +done
16.98 +
16.99 +lemma ve_app_owr [simp]:
16.100 + "ve \<in> ValEnv
16.101 + ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))"
16.102 +by (erule ValEnvE, simp add: map_app_owr)
16.103 +
16.104 +(* Introduction rules for operators on value environments *)
16.105 +
16.106 +lemma ve_appI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> ve_app(ve,x):Val"
16.107 +by (erule ValEnvE, simp add: pmap_appI)
16.108 +
16.109 +lemma ve_domI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> x \<in> ExVar"
16.110 +apply (erule ValEnvE)
16.111 +apply (simp );
16.112 +apply (blast dest: pmap_domainD)
16.113 +done
16.114 +
16.115 +lemma ve_empI: "ve_emp \<in> ValEnv"
16.116 +apply (unfold ve_emp_def)
16.117 +apply (rule Val_ValEnv.intros)
16.118 +apply (rule pmap_empI)
16.119 +done
16.120 +
16.121 +lemma ve_owrI:
16.122 + "[|ve \<in> ValEnv; x \<in> ExVar; v \<in> Val |] ==> ve_owr(ve,x,v):ValEnv"
16.123 +apply (erule ValEnvE)
16.124 +apply simp
16.125 +apply (blast intro: pmap_owrI Val_ValEnv.intros)
16.126 +done
16.127 +
16.128 end
16.129 -
16.130 -
16.131 -
17.1 --- a/src/ZF/IsaMakefile Sat Dec 22 19:46:16 2001 +0100
17.2 +++ b/src/ZF/IsaMakefile Tue Dec 25 10:02:01 2001 +0100
17.3 @@ -75,10 +75,8 @@
17.4 ZF-Coind: ZF $(LOG)/ZF-Coind.gz
17.5
17.6 $(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
17.7 - Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \
17.8 - Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \
17.9 - Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \
17.10 - Coind/Values.thy
17.11 + Coind/ECR.thy Coind/Language.thy Coind/Map.thy Coind/ROOT.ML \
17.12 + Coind/Static.thy Coind/Types.thy Coind/Values.thy
17.13 @$(ISATOOL) usedir $(OUT)/ZF Coind
17.14
17.15
17.16 @@ -95,9 +93,9 @@
17.17
17.18 ZF-Resid: ZF $(LOG)/ZF-Resid.gz
17.19
17.20 -$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \
17.21 - Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \
17.22 - Resid/Substitution.thy
17.23 +$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML \
17.24 + Resid/Confluence.thy Resid/Redex.thy \
17.25 + Resid/Reduction.thy Resid/Residuals.thy Resid/Substitution.thy
17.26 @$(ISATOOL) usedir $(OUT)/ZF Resid
17.27
17.28
18.1 --- a/src/ZF/Resid/Conversion.thy Sat Dec 22 19:46:16 2001 +0100
18.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
18.3 @@ -1,36 +0,0 @@
18.4 -(* Title: Conversion.thy
18.5 - ID: $Id$
18.6 - Author: Ole Rasmussen
18.7 - Copyright 1995 University of Cambridge
18.8 - Logic Image: ZF
18.9 -
18.10 -*)
18.11 -
18.12 -Conversion = Confluence+
18.13 -
18.14 -consts
18.15 - Sconv1 :: i
18.16 - "<-1->" :: [i,i]=>o (infixl 50)
18.17 - Sconv :: i
18.18 - "<--->" :: [i,i]=>o (infixl 50)
18.19 -
18.20 -translations
18.21 - "a<-1->b" == "<a,b>:Sconv1"
18.22 - "a<--->b" == "<a,b>:Sconv"
18.23 -
18.24 -inductive
18.25 - domains "Sconv1" <= "lambda*lambda"
18.26 - intrs
18.27 - red1 "m -1-> n ==> m<-1->n"
18.28 - expl "n -1-> m ==> m<-1->n"
18.29 - type_intrs "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
18.30 -
18.31 -inductive
18.32 - domains "Sconv" <= "lambda*lambda"
18.33 - intrs
18.34 - one_step "m<-1->n ==> m<--->n"
18.35 - refl "m \\<in> lambda ==> m<--->m"
18.36 - trans "[|m<--->n; n<--->p|] ==> m<--->p"
18.37 - type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
18.38 -end
18.39 -
19.1 --- a/src/ZF/Resid/Cube.thy Sat Dec 22 19:46:16 2001 +0100
19.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
19.3 @@ -1,8 +0,0 @@
19.4 -(* Title: Cube.thy
19.5 - ID: $Id$
19.6 - Author: Ole Rasmussen
19.7 - Copyright 1995 University of Cambridge
19.8 - Logic Image: ZF
19.9 -*)
19.10 -
19.11 -Cube = Residuals
20.1 --- a/src/ZF/Resid/Terms.thy Sat Dec 22 19:46:16 2001 +0100
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,33 +0,0 @@
20.4 -(* Title: Terms.thy
20.5 - ID: $Id$
20.6 - Author: Ole Rasmussen
20.7 - Copyright 1995 University of Cambridge
20.8 - Logic Image: ZF
20.9 -*)
20.10 -
20.11 -Terms = Cube+
20.12 -
20.13 -consts
20.14 - lambda :: i
20.15 - unmark :: i=>i
20.16 - Apl :: [i,i]=>i
20.17 -
20.18 -translations
20.19 - "Apl(n,m)" == "App(0,n,m)"
20.20 -
20.21 -inductive
20.22 - domains "lambda" <= "redexes"
20.23 - intrs
20.24 - Lambda_Var " n \\<in> nat ==> Var(n):lambda"
20.25 - Lambda_Fun " u \\<in> lambda ==> Fun(u):lambda"
20.26 - Lambda_App "[|u \\<in> lambda; v \\<in> lambda|]==> Apl(u,v):lambda"
20.27 - type_intrs "redexes.intrs@bool_typechecks"
20.28 -
20.29 -primrec
20.30 - "unmark(Var(n)) = Var(n)"
20.31 - "unmark(Fun(u)) = Fun(unmark(u))"
20.32 - "unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
20.33 -
20.34 -end
20.35 -
20.36 -