--- a/src/ZF/Coind/BCR.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/BCR.thy Tue Dec 25 10:02:01 2001 +0100
@@ -3,25 +3,3 @@
Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
*)
-
-BCR = Values + Types +
-
-(*Basic correspondence relation -- not completely specified, as it is a
- parameter of the proof. A concrete version could be defined inductively.*)
-
-consts
- isof :: [i,i] => o
-rules
- isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
-
-(*Its extension to environments*)
-
-consts
- isofenv :: [i,i] => o
-defs
- isofenv_def "isofenv(ve,te) ==
- ve_dom(ve) = te_dom(te) &
- ( \\<forall>x \\<in> ve_dom(ve).
- \\<exists>c \\<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
-
-end
--- a/src/ZF/Coind/Dynamic.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Dynamic.thy Tue Dec 25 10:02:01 2001 +0100
@@ -4,38 +4,37 @@
Copyright 1995 University of Cambridge
*)
-Dynamic = Values +
+theory Dynamic = Values:
consts
EvalRel :: i
inductive
domains "EvalRel" <= "ValEnv * Exp * Val"
- intrs
- eval_constI
- " [| ve \\<in> ValEnv; c \\<in> Const |] ==>
+ intros
+ eval_constI:
+ " [| ve \<in> ValEnv; c \<in> Const |] ==>
<ve,e_const(c),v_const(c)>:EvalRel"
- eval_varI
- " [| ve \\<in> ValEnv; x \\<in> ExVar; x \\<in> ve_dom(ve) |] ==>
+ eval_varI:
+ " [| ve \<in> ValEnv; x \<in> ExVar; x \<in> ve_dom(ve) |] ==>
<ve,e_var(x),ve_app(ve,x)>:EvalRel"
- eval_fnI
- " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp |] ==>
+ eval_fnI:
+ " [| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp |] ==>
<ve,e_fn(x,e),v_clos(x,e,ve)>:EvalRel "
- eval_fixI
- " [| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val;
+ eval_fixI:
+ " [| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;
v_clos(x,e,ve_owr(ve,f,cl))=cl |] ==>
<ve,e_fix(f,x,e),cl>:EvalRel "
- eval_appI1
- " [| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const;
+ eval_appI1:
+ " [| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;
<ve,e1,v_const(c1)>:EvalRel;
<ve,e2,v_const(c2)>:EvalRel |] ==>
<ve,e_app(e1,e2),v_const(c_app(c1,c2))>:EvalRel "
- eval_appI2
- " [| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val;
+ eval_appI2:
+ " [| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; v \<in> Val;
<ve,e1,v_clos(xm,em,vem)>:EvalRel;
<ve,e2,v2>:EvalRel;
<ve_owr(vem,xm,v2),em,v>:EvalRel |] ==>
<ve,e_app(e1,e2),v>:EvalRel "
- type_intrs "c_appI::ve_appI::ve_empI::ve_owrI::Exp.intrs@Val_ValEnv.intrs"
+ type_intros c_appI ve_appI ve_empI ve_owrI Exp.intros Val_ValEnv.intros
-
end
--- a/src/ZF/Coind/ECR.ML Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(* Title: ZF/Coind/ECR.ML
- ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-*)
-
-(* Specialised co-induction rule *)
-
-Goal "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv; \
-\ <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \
-\ {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}: \
-\ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] \
-\ ==> <v_clos(x, e, ve),t>:HasTyRel";
-by (rtac (singletonI RS HasTyRel.coinduct) 1);
-by (ALLGOALS Blast_tac);
-qed "htr_closCI";
-
-(* Specialised elimination rules *)
-
-val htr_constE = HasTyRel.mk_cases "<v_const(c),t>:HasTyRel";
-
-val htr_closE = HasTyRel.mk_cases "<v_clos(x,e,ve),t>:HasTyRel";
-
-(* Classical reasoning sets *)
-
-fun mk_htr_cs cs =
- let open HasTyRel in
- ( cs
- addSIs [htr_constI]
- addSEs [htr_constE]
- addIs [htr_closI,htr_closCI]
- addEs [htr_closE])
- end;
-
-claset_ref() := mk_htr_cs (claset());
-
-(* Properties of the pointwise extension to environments *)
-
-bind_thm ("HasTyRel_non_zero",
- HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE);
-
-Goalw [hastyenv_def]
- "[| ve \\<in> ValEnv; te \\<in> TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \
-\ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))";
-by (asm_full_simp_tac
- (simpset() addsimps [ve_app_owr, HasTyRel_non_zero, ve_dom_owr]) 1);
-by Auto_tac;
-qed "hastyenv_owr";
-
-Goalw [isofenv_def,hastyenv_def]
- "[| ve \\<in> ValEnv; te \\<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)";
-by Safe_tac;
-by (dtac bspec 1);
-by (assume_tac 1);
-by Safe_tac;
-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);
-qed "basic_consistency_lem";
-
-
-
--- a/src/ZF/Coind/ECR.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/ECR.thy Tue Dec 25 10:02:01 2001 +0100
@@ -4,7 +4,7 @@
Copyright 1995 University of Cambridge
*)
-ECR = Static + Dynamic +
+theory ECR = Static + Dynamic:
(* The extended correspondence relation *)
@@ -12,27 +12,161 @@
HasTyRel :: i
coinductive
domains "HasTyRel" <= "Val * Ty"
- intrs
- htr_constI
- "[| c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
- htr_closI
- "[| x \\<in> ExVar; e \\<in> Exp; t \\<in> Ty; ve \\<in> ValEnv; te \\<in> TyEnv;
- <te,e_fn(x,e),t>:ElabRel;
+ intros
+ htr_constI [intro!]:
+ "[| c \<in> Const; t \<in> Ty; isof(c,t) |] ==> <v_const(c),t> \<in> HasTyRel"
+ htr_closI [intro]:
+ "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;
+ <te,e_fn(x,e),t> \<in> ElabRel;
ve_dom(ve) = te_dom(te);
- {<ve_app(ve,y),te_app(te,y)>.y \\<in> ve_dom(ve)}:Pow(HasTyRel)
- |] ==>
- <v_clos(x,e,ve),t>:HasTyRel"
+ {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in> Pow(HasTyRel) |]
+ ==> <v_clos(x,e,ve),t> \<in> HasTyRel"
monos Pow_mono
- type_intrs "Val_ValEnv.intrs"
+ type_intros Val_ValEnv.intros
(* Pointwise extension to environments *)
-consts
- hastyenv :: [i,i] => o
-defs
- hastyenv_def
- " hastyenv(ve,te) ==
- ve_dom(ve) = te_dom(te) &
- (\\<forall>x \\<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+constdefs
+ hastyenv :: "[i,i] => o"
+ "hastyenv(ve,te) ==
+ ve_dom(ve) = te_dom(te) &
+ (\<forall>x \<in> ve_dom(ve). <ve_app(ve,x),te_app(te,x)> \<in> HasTyRel)"
+
+(* Specialised co-induction rule *)
+
+lemma htr_closCI [intro]:
+ "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;
+ <te, e_fn(x, e), t> \<in> ElabRel; ve_dom(ve) = te_dom(te);
+ {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
+ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]
+ ==> <v_clos(x, e, ve),t> \<in> HasTyRel"
+apply (rule singletonI [THEN HasTyRel.coinduct])
+apply auto
+done
+
+(* Specialised elimination rules *)
+
+inductive_cases htr_constE [elim!]: "<v_const(c),t> \<in> HasTyRel"
+inductive_cases htr_closE [elim]: "<v_clos(x,e,ve),t> \<in> HasTyRel"
+
+
+(* Properties of the pointwise extension to environments *)
+
+lemmas HasTyRel_non_zero =
+ HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE, standard]
+
+lemma hastyenv_owr:
+ "[| ve \<in> ValEnv; te \<in> TyEnv; hastyenv(ve,te); <v,t> \<in> HasTyRel |]
+ ==> hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"
+by (auto simp add: hastyenv_def ve_app_owr HasTyRel_non_zero)
+
+lemma basic_consistency_lem:
+ "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"
+apply (unfold isofenv_def hastyenv_def)
+apply (force intro: te_appI ve_domI)
+done
+
+
+(* ############################################################ *)
+(* The Consistency theorem *)
+(* ############################################################ *)
+
+lemma consistency_const:
+ "[| c \<in> Const; hastyenv(ve,te);<te,e_const(c),t> \<in> ElabRel |]
+ ==> <v_const(c), t> \<in> HasTyRel"
+by blast
+
+
+lemma consistency_var:
+ "[| x \<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t> \<in> ElabRel |] ==>
+ <ve_app(ve,x),t> \<in> HasTyRel"
+by (unfold hastyenv_def, blast)
+
+lemma consistency_fn:
+ "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; hastyenv(ve,te);
+ <te,e_fn(x,e),t> \<in> ElabRel
+ |] ==> <v_clos(x, e, ve), t> \<in> HasTyRel"
+by (unfold hastyenv_def, blast)
+
+declare ElabRel.dom_subset [THEN subsetD, dest]
+
+declare Ty.intros [simp, intro!]
+declare TyEnv.intros [simp, intro!]
+declare Val_ValEnv.intros [simp, intro!]
+
+lemma consistency_fix:
+ "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;
+ v_clos(x,e,ve_owr(ve,f,cl)) = cl;
+ hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel |] ==>
+ <cl,t> \<in> HasTyRel"
+apply (unfold hastyenv_def)
+apply (erule elab_fixE)
+apply safe
+apply (rule subst, assumption)
+apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
+apply simp_all
+apply (blast intro: ve_owrI)
+apply (rule ElabRel.fnI)
+apply (simp_all add: ValNEE)
+apply force
+done
+
+
+lemma consistency_app1:
+ "[| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;
+ <ve,e1,v_const(c1)> \<in> EvalRel;
+ \<forall>t te.
+ hastyenv(ve,te) --> <te,e1,t> \<in> ElabRel --> <v_const(c1),t> \<in> HasTyRel;
+ <ve, e2, v_const(c2)> \<in> EvalRel;
+ \<forall>t te.
+ hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v_const(c2),t> \<in> HasTyRel;
+ hastyenv(ve, te);
+ <te,e_app(e1,e2),t> \<in> ElabRel |]
+ ==> <v_const(c_app(c1, c2)),t> \<in> HasTyRel"
+by (blast intro!: c_appI intro: isof_app)
+
+lemma consistency_app2:
+ "[| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar;
+ v \<in> Val;
+ <ve,e1,v_clos(xm,em,vem)> \<in> EvalRel;
+ \<forall>t te. hastyenv(ve,te) -->
+ <te,e1,t> \<in> ElabRel --> <v_clos(xm,em,vem),t> \<in> HasTyRel;
+ <ve,e2,v2> \<in> EvalRel;
+ \<forall>t te. hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v2,t> \<in> HasTyRel;
+ <ve_owr(vem,xm,v2),em,v> \<in> EvalRel;
+ \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) -->
+ <te,em,t> \<in> ElabRel --> <v,t> \<in> HasTyRel;
+ hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |]
+ ==> <v,t> \<in> HasTyRel"
+apply (erule elab_appE)
+apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
+apply (drule spec [THEN spec, THEN mp, THEN mp], assumption+)
+apply (erule htr_closE)
+apply (erule elab_fnE)
+apply simp
+apply clarify
+apply (drule spec [THEN spec, THEN mp, THEN mp])
+prefer 2 apply assumption+
+apply (rule hastyenv_owr)
+apply assumption
+apply assumption
+apply (simp add: hastyenv_def)
+apply blast+
+done
+
+lemma consistency [rule_format]:
+ "<ve,e,v> \<in> EvalRel
+ ==> (\<forall>t te. hastyenv(ve,te) --> <te,e,t> \<in> ElabRel --> <v,t> \<in> HasTyRel)"
+apply (erule EvalRel.induct)
+apply (simp_all add: consistency_const consistency_var consistency_fn
+ consistency_fix consistency_app1)
+apply (blast intro: consistency_app2)
+done
+
+lemma basic_consistency:
+ "[| ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te);
+ <ve,e,v_const(c)> \<in> EvalRel; <te,e,t> \<in> ElabRel |]
+ ==> isof(c,t)"
+by (blast dest: consistency intro!: basic_consistency_lem)
end
--- a/src/ZF/Coind/Language.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Language.thy Tue Dec 25 10:02:01 2001 +0100
@@ -4,15 +4,17 @@
Copyright 1995 University of Cambridge
*)
-Language = Main +
+theory Language = Main:
consts
Const :: i (* Abstract type of constants *)
- c_app :: [i,i] => i (* Abstract constructor for fun application*)
+ c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
+
-rules
- constNEE "c \\<in> Const ==> c \\<noteq> 0"
- c_appI "[| c1 \\<in> Const; c2 \\<in> Const |] ==> c_app(c1,c2):Const"
+text{*these really can't be definitions without losing the abstraction*}
+axioms
+ constNEE: "c \<in> Const ==> c \<noteq> 0"
+ c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
consts
@@ -20,10 +22,10 @@
ExVar :: i (* Abstract type of variables *)
datatype
- "Exp" = e_const ("c \\<in> Const")
- | e_var ("x \\<in> ExVar")
- | e_fn ("x \\<in> ExVar","e \\<in> Exp")
- | e_fix ("x1 \\<in> ExVar","x2 \\<in> ExVar","e \\<in> Exp")
- | e_app ("e1 \\<in> Exp","e2 \\<in> Exp")
+ "Exp" = e_const ("c \<in> Const")
+ | e_var ("x \<in> ExVar")
+ | e_fn ("x \<in> ExVar","e \<in> Exp")
+ | e_fix ("x1 \<in> ExVar","x2 \<in> ExVar","e \<in> Exp")
+ | e_app ("e1 \<in> Exp","e2 \<in> Exp")
end
--- a/src/ZF/Coind/MT.ML Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,149 +0,0 @@
-(* Title: ZF/Coind/MT.ML
- ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-*)
-
-(* ############################################################ *)
-(* The Consistency theorem *)
-(* ############################################################ *)
-
-Goal "[| c \\<in> Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \
-\ <v_const(c), t> \\<in> HasTyRel";
-by (Fast_tac 1);
-qed "consistency_const";
-
-
-Goalw [hastyenv_def]
- "[| x \\<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \
-\ <ve_app(ve,x),t>:HasTyRel";
-by (Fast_tac 1);
-qed "consistency_var";
-
-
-Goalw [hastyenv_def]
- "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; hastyenv(ve,te); \
-\ <te,e_fn(x,e),t>:ElabRel \
-\ |] ==> <v_clos(x, e, ve), t> \\<in> HasTyRel";
-by (Blast_tac 1);
-qed "consistency_fn";
-
-AddDs [te_owrE, ElabRel.dom_subset RS subsetD];
-
-Addsimps [ve_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));
-
-Goalw [hastyenv_def]
- "[| ve \\<in> ValEnv; x \\<in> ExVar; e \\<in> Exp; f \\<in> ExVar; cl \\<in> Val; \
-\ v_clos(x,e,ve_owr(ve,f,cl)) = cl; \
-\ hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==> \
-\ <cl,t>:HasTyRel";
-by (etac elab_fixE 1);
-by Safe_tac;
-by (EVERY [ftac 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.fnI 1);
-by clean_tac;
-by (Asm_simp_tac 1);
-by (stac ve_dom_owr 1);
-by (assume_tac 1);
-by (etac subst 1);
-by (rtac v_closNE 1);
-by (Asm_simp_tac 1);
-
-by (rtac PowI 1);
-by (stac ve_dom_owr 1);
-by (assume_tac 1);
-by (etac subst 1);
-by (rtac v_closNE 1);
-by (rtac subsetI 1);
-by (etac RepFunE 1);
-by (case_tac "f=y" 1);
-by Auto_tac;
-qed "consistency_fix";
-
-
-Goal "[| ve \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; c1 \\<in> Const; c2 \\<in> Const; \
-\ <ve,e1,v_const(c1)>:EvalRel; \
-\ \\<forall>t te. \
-\ hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
-\ <ve, e2, v_const(c2)> \\<in> EvalRel; \
-\ \\<forall>t te. \
-\ hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \
-\ hastyenv(ve, te); \
-\ <te,e_app(e1,e2),t>:ElabRel |] ==> \
-\ <v_const(c_app(c1, c2)),t>:HasTyRel";
-by (etac elab_appE 1);
-by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
-qed "consistency_app1";
-
-Goal "[| ve \\<in> ValEnv; vem \\<in> ValEnv; e1 \\<in> Exp; e2 \\<in> Exp; em \\<in> Exp; xm \\<in> ExVar; v \\<in> Val; \
-\ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \
-\ \\<forall>t te. \
-\ hastyenv(ve,te) --> \
-\ <te,e1,t>:ElabRel --> \
-\ <v_clos(xm,em,vem),t>:HasTyRel; \
-\ <ve,e2,v2>:EvalRel; \
-\ \\<forall>t te. \
-\ hastyenv(ve,te) --> \
-\ <te,e2,t>:ElabRel --> \
-\ <v2,t>:HasTyRel; \
-\ <ve_owr(vem,xm,v2),em,v>:EvalRel; \
-\ \\<forall>t te. \
-\ hastyenv(ve_owr(vem,xm,v2),te) --> \
-\ <te,em,t>:ElabRel --> \
-\ <v,t>:HasTyRel; \
-\ hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==> \
-\ <v,t>:HasTyRel ";
-by (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 (Full_simp_tac 1);
-by (Clarify_tac 1);
-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 (asm_simp_tac (simpset() addsimps [hastyenv_def]) 1);
-by (Fast_tac 1);
-qed "consistency_app2";
-
-Goal "<ve,e,v>:EvalRel ==> \
-\ (\\<forall>t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
-by (etac EvalRel.induct 1);
-by (blast_tac (claset() addIs [consistency_app2]) 6);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1])));
-qed "consistency";
-
-
-Goal "[| ve \\<in> ValEnv; te \\<in> TyEnv; \
-\ isofenv(ve,te); \
-\ <ve,e,v_const(c)>:EvalRel; \
-\ <te,e,t>:ElabRel \
-\ |] ==> isof(c,t)";
-by (rtac htr_constE 1);
-by (dtac consistency 1);
-by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
-by (assume_tac 1);
-qed "basic_consistency";
--- a/src/ZF/Coind/MT.thy Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-MT = ECR
--- a/src/ZF/Coind/Map.ML Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,206 +0,0 @@
-(* Title: ZF/Coind/Map.ML
- ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-*)
-
-(** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
-
-Goalw [TMap_def] "{0,1} \\<subseteq> {1} Un TMap(I, {0,1})";
-by (Blast_tac 1);
-result();
-
-Goalw [TMap_def] "{0} Un TMap(I,1) \\<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))";
-by (Blast_tac 1);
-result();
-
-Goalw [TMap_def] "{0,1} Un TMap(I,2) \\<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))";
-by (Blast_tac 1);
-result();
-
-(*
-Goalw [TMap_def]
- "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \\<subseteq> \
-\ {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
-by (Blast_tac 1);
-result();
-*)
-
-
-(* ############################################################ *)
-(* Lemmas *)
-(* ############################################################ *)
-
-Goal "Sigma(A,B)``{a} = (if a \\<in> A then B(a) else 0)";
-by Auto_tac;
-qed "qbeta_if";
-
-Goal "a \\<in> A ==> Sigma(A,B)``{a} = B(a)";
-by (Fast_tac 1);
-qed "qbeta";
-
-Goal "a\\<notin>A ==> Sigma(A,B)``{a} = 0";
-by (Fast_tac 1);
-qed "qbeta_emp";
-
-Goal "a \\<notin> A ==> Sigma(A,B)``{a}=0";
-by (Fast_tac 1);
-qed "image_Sigma1";
-
-
-(* ############################################################ *)
-(* Inclusion in Quine Universes *)
-(* ############################################################ *)
-
-(* Lemmas *)
-
-Goalw [quniv_def]
- "A \\<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \\<subseteq> 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 (simpset() addsimps [Union_Pow_eq]) 1);
-qed "MapQU_lemma";
-
-(* Theorems *)
-
-val prems = goalw Map.thy [PMap_def,TMap_def]
- "[| m \\<in> PMap(A,quniv(B)); !!x. x \\<in> A ==> x \\<in> univ(B) |] ==> m \\<in> 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 1);
-qed "mapQU";
-
-(* ############################################################ *)
-(* Monotonicity *)
-(* ############################################################ *)
-
-Goalw [PMap_def,TMap_def] "B \\<subseteq> C ==> PMap(A,B)<=PMap(A,C)";
-by (Blast_tac 1);
-qed "map_mono";
-
-(* Rename to pmap_mono *)
-
-(* ############################################################ *)
-(* Introduction Rules *)
-(* ############################################################ *)
-
-(** map_emp **)
-
-Goalw [map_emp_def,PMap_def,TMap_def] "map_emp \\<in> PMap(A,B)";
-by Auto_tac;
-qed "pmap_empI";
-
-(** map_owr **)
-
-
-Goalw [map_owr_def,PMap_def,TMap_def]
- "[| m \\<in> PMap(A,B); a \\<in> A; b \\<in> B |] ==> map_owr(m,a,b):PMap(A,B)";
-by Safe_tac;
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [if_iff])));
-by (Fast_tac 1);
-by (Fast_tac 1);
-by (Deepen_tac 2 1);
-(*Remaining subgoal*)
-by (rtac (excluded_middle RS disjE) 1);
-by (etac image_Sigma1 1);
-by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps [qbeta]) 1);
-by Safe_tac;
-by (dres_inst_tac [("psi", "?uu \\<notin> B")] asm_rl 3);
-by (ALLGOALS Asm_full_simp_tac);
-by (Fast_tac 1);
-qed "pmap_owrI";
-
-(** map_app **)
-
-Goalw [TMap_def,map_app_def]
- "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a) \\<noteq>0";
-by (etac domainE 1);
-by (dtac imageI 1);
-by (Fast_tac 1);
-by (etac not_emptyI 1);
-qed "tmap_app_notempty";
-
-Goalw [TMap_def,map_app_def,domain_def]
- "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
-by (Fast_tac 1);
-qed "tmap_appI";
-
-Goalw [PMap_def]
- "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> map_app(m,a):B";
-by (ftac tmap_app_notempty 1);
-by (assume_tac 1);
-by (dtac tmap_appI 1);
-by (assume_tac 1);
-by (Fast_tac 1);
-qed "pmap_appI";
-
-(** domain **)
-
-Goalw [TMap_def]
- "[| m \\<in> TMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
-by (Fast_tac 1);
-qed "tmap_domainD";
-
-Goalw [PMap_def,TMap_def]
- "[| m \\<in> PMap(A,B); a \\<in> domain(m) |] ==> a \\<in> A";
-by (Fast_tac 1);
-qed "pmap_domainD";
-
-(* ############################################################ *)
-(* Equalities *)
-(* ############################################################ *)
-
-(** Domain **)
-
-(* Lemmas *)
-
-Goal "domain(\\<Union>x \\<in> A. B(x)) = (\\<Union>x \\<in> A. domain(B(x)))";
-by (Fast_tac 1);
-qed "domain_UN";
-
-Goal "domain(Sigma(A,B)) = {x \\<in> A. \\<exists>y. y \\<in> B(x)}";
-by (simp_tac (simpset() addsimps [domain_UN,domain_0,domain_cons]) 1);
-by (Fast_tac 1);
-qed "domain_Sigma";
-
-(* Theorems *)
-
-Goalw [map_emp_def] "domain(map_emp) = 0";
-by (Fast_tac 1);
-qed "map_domain_emp";
-
-Goalw [map_owr_def]
- "b \\<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
-by (simp_tac (simpset() addsimps [domain_Sigma]) 1);
-by (rtac equalityI 1);
-by (Fast_tac 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 1);
-by (Fast_tac 1);
-by (fast_tac (claset() addss (simpset())) 1);
-qed "map_domain_owr";
-
-(** Application **)
-
-Goalw [map_app_def,map_owr_def]
- "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))";
-by (asm_simp_tac (simpset() addsimps [qbeta_if]) 1);
-by (Fast_tac 1);
-qed "map_app_owr";
-
-Goal "map_app(map_owr(f,a,b),a) = b";
-by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
-qed "map_app_owr1";
-
-Goal "c \\<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
-by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
-qed "map_app_owr2";
--- a/src/ZF/Coind/Map.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Map.thy Tue Dec 25 10:02:01 2001 +0100
@@ -2,25 +2,185 @@
ID: $Id$
Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
+
+
+Some sample proofs of inclusions for the final coalgebra "U" (by lcp)
+
*)
-Map = Main +
+theory Map = Main:
constdefs
- TMap :: [i,i] => i
- "TMap(A,B) == {m \\<in> Pow(A*Union(B)).\\<forall>a \\<in> A. m``{a} \\<in> B}"
+ TMap :: "[i,i] => i"
+ "TMap(A,B) == {m \<in> Pow(A*Union(B)).\<forall>a \<in> A. m``{a} \<in> B}"
- PMap :: [i,i] => i
+ PMap :: "[i,i] => i"
"PMap(A,B) == TMap(A,cons(0,B))"
-(* Note: 0 \\<in> B ==> TMap(A,B) = PMap(A,B) *)
+(* Note: 0 \<in> B ==> TMap(A,B) = PMap(A,B) *)
map_emp :: i
"map_emp == 0"
- map_owr :: [i,i,i]=>i
- "map_owr(m,a,b) == \\<Sigma>x \\<in> {a} Un domain(m). if x=a then b else m``{x}"
- map_app :: [i,i]=>i
+ map_owr :: "[i,i,i]=>i"
+ "map_owr(m,a,b) == \<Sigma>x \<in> {a} Un domain(m). if x=a then b else m``{x}"
+
+ map_app :: "[i,i]=>i"
"map_app(m,a) == m``{a}"
+lemma "{0,1} \<subseteq> {1} Un TMap(I, {0,1})"
+by (unfold TMap_def, blast)
+
+lemma "{0} Un TMap(I,1) \<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))"
+by (unfold TMap_def, blast)
+
+lemma "{0,1} Un TMap(I,2) \<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))"
+by (unfold TMap_def, blast)
+
+(*A bit too slow.
+lemma "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \<subseteq>
+ {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))"
+by (unfold TMap_def, blast)
+*)
+
+(* ############################################################ *)
+(* Lemmas *)
+(* ############################################################ *)
+
+lemma qbeta_if: "Sigma(A,B)``{a} = (if a \<in> A then B(a) else 0)"
+by auto
+
+lemma qbeta: "a \<in> A ==> Sigma(A,B)``{a} = B(a)"
+by fast
+
+lemma qbeta_emp: "a\<notin>A ==> Sigma(A,B)``{a} = 0"
+by fast
+
+lemma image_Sigma1: "a \<notin> A ==> Sigma(A,B)``{a}=0"
+by fast
+
+
+(* ############################################################ *)
+(* Inclusion in Quine Universes *)
+(* ############################################################ *)
+
+(* Lemmas *)
+
+lemma MapQU_lemma:
+ "A \<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \<subseteq> quniv(X)"
+apply (unfold quniv_def)
+apply (rule Pow_mono)
+apply (rule subset_trans [OF Sigma_mono product_univ])
+apply (erule subset_trans)
+apply (rule arg_subset_eclose [THEN univ_mono])
+apply (simp add: Union_Pow_eq)
+done
+
+(* Theorems *)
+
+lemma mapQU:
+ "[| m \<in> PMap(A,quniv(B)); !!x. x \<in> A ==> x \<in> univ(B) |] ==> m \<in> quniv(B)"
+apply (unfold PMap_def TMap_def)
+apply (blast intro!: MapQU_lemma [THEN subsetD])
+done
+
+(* ############################################################ *)
+(* Monotonicity *)
+(* ############################################################ *)
+
+lemma PMap_mono: "B \<subseteq> C ==> PMap(A,B)<=PMap(A,C)"
+by (unfold PMap_def TMap_def, blast)
+
+
+(* ############################################################ *)
+(* Introduction Rules *)
+(* ############################################################ *)
+
+(** map_emp **)
+
+lemma pmap_empI: "map_emp \<in> PMap(A,B)"
+by (unfold map_emp_def PMap_def TMap_def, auto)
+
+(** map_owr **)
+
+lemma pmap_owrI:
+ "[| m \<in> PMap(A,B); a \<in> A; b \<in> B |] ==> map_owr(m,a,b):PMap(A,B)"
+apply (unfold map_owr_def PMap_def TMap_def)
+apply safe
+apply (simp_all add: if_iff)
+apply auto
+(*Remaining subgoal*)
+apply (rule excluded_middle [THEN disjE])
+apply (erule image_Sigma1)
+apply (drule_tac psi = "?uu \<notin> B" in asm_rl)
+apply (auto simp add: qbeta)
+done
+
+(** map_app **)
+
+lemma tmap_app_notempty:
+ "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a) \<noteq>0"
+by (unfold TMap_def map_app_def, blast)
+
+lemma tmap_appI:
+ "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
+by (unfold TMap_def map_app_def domain_def, blast)
+
+lemma pmap_appI:
+ "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> map_app(m,a):B"
+apply (unfold PMap_def)
+apply (frule tmap_app_notempty, assumption)
+apply (drule tmap_appI)
+apply auto
+done
+
+(** domain **)
+
+lemma tmap_domainD:
+ "[| m \<in> TMap(A,B); a \<in> domain(m) |] ==> a \<in> A"
+by (unfold TMap_def, blast)
+
+lemma pmap_domainD:
+ "[| m \<in> PMap(A,B); a \<in> domain(m) |] ==> a \<in> A"
+by (unfold PMap_def TMap_def, blast)
+
+
+(* ############################################################ *)
+(* Equalities *)
+(* ############################################################ *)
+
+(** Domain **)
+
+(* Lemmas *)
+
+lemma domain_UN: "domain(\<Union>x \<in> A. B(x)) = (\<Union>x \<in> A. domain(B(x)))"
+by fast
+
+
+lemma domain_Sigma: "domain(Sigma(A,B)) = {x \<in> A. \<exists>y. y \<in> B(x)}"
+by blast
+
+(* Theorems *)
+
+lemma map_domain_emp: "domain(map_emp) = 0"
+by (unfold map_emp_def, blast)
+
+lemma map_domain_owr:
+ "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"
+apply (unfold map_owr_def)
+apply (auto simp add: domain_Sigma)
+done
+
+(** Application **)
+
+lemma map_app_owr:
+ "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))"
+by (simp add: qbeta_if map_app_def map_owr_def, blast)
+
+lemma map_app_owr1: "map_app(map_owr(f,a,b),a) = b"
+by (simp add: map_app_owr)
+
+lemma map_app_owr2: "c \<noteq> a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"
+by (simp add: map_app_owr)
+
end
--- a/src/ZF/Coind/ROOT.ML Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/ROOT.ML Tue Dec 25 10:02:01 2001 +0100
@@ -13,4 +13,4 @@
Report, Computer Lab, University of Cambridge (1995).
*)
-time_use_thy "MT";
+time_use_thy "ECR";
--- a/src/ZF/Coind/Static.ML Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Title: ZF/Coind/Static.ML
- ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-*)
-
-val elab_constE = ElabRel.mk_cases "<te,e_const(c),t>:ElabRel";
-
-val elab_varE = ElabRel.mk_cases "<te,e_var(x),t>:ElabRel";
-
-val elab_fnE = ElabRel.mk_cases "<te,e_fn(x,e),t>:ElabRel";
-
-val elab_fixE = ElabRel.mk_cases "<te,e_fix(f,x,e),t>:ElabRel";
-
-val elab_appE = ElabRel.mk_cases "<te,e_app(e1,e2),t>:ElabRel";
-
-AddSEs [elab_constE, elab_varE, elab_fixE];
-
-AddSIs [ElabRel.constI, ElabRel.varI, ElabRel.fnI, ElabRel.fixI];
-
-AddIs [ElabRel.appI];
-
-AddEs [elab_appE, elab_fnE];
-
-AddDs [ElabRel.dom_subset RS subsetD];
--- a/src/ZF/Coind/Static.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Static.thy Tue Dec 25 10:02:01 2001 +0100
@@ -4,33 +4,63 @@
Copyright 1995 University of Cambridge
*)
-Static = BCR +
+theory Static = Values + Types:
+
+(*** Basic correspondence relation -- not completely specified, as it is a
+ parameter of the proof. A concrete version could be defined inductively.
+***)
+
+consts
+ isof :: "[i,i] => o"
+
+axioms
+ isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
+
+(*Its extension to environments*)
+
+constdefs
+ isofenv :: "[i,i] => o"
+ "isofenv(ve,te) ==
+ ve_dom(ve) = te_dom(te) &
+ (\<forall>x \<in> ve_dom(ve).
+ \<exists>c \<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
+
+
+(*** Elaboration ***)
consts ElabRel :: i
inductive
domains "ElabRel" <= "TyEnv * Exp * Ty"
- intrs
- constI
- " [| te \\<in> TyEnv; c \\<in> Const; t \\<in> Ty; isof(c,t) |] ==>
- <te,e_const(c),t>:ElabRel "
- varI
- " [| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==>
- <te,e_var(x),te_app(te,x)>:ElabRel "
- fnI
- " [| te \\<in> TyEnv; x \\<in> ExVar; e \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;
- <te_owr(te,x,t1),e,t2>:ElabRel |] ==>
- <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
- fixI
- " [| te \\<in> TyEnv; f \\<in> ExVar; x \\<in> ExVar; t1 \\<in> Ty; t2 \\<in> Ty;
- <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>
- <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
- appI
- " [| te \\<in> TyEnv; e1 \\<in> Exp; e2 \\<in> Exp; t1 \\<in> Ty; t2 \\<in> Ty;
- <te,e1,t_fun(t1,t2)>:ElabRel;
- <te,e2,t1>:ElabRel |] ==>
- <te,e_app(e1,e2),t2>:ElabRel "
- type_intrs "te_appI::Exp.intrs@Ty.intrs"
+ intros
+ constI [intro!]:
+ "[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==>
+ <te,e_const(c),t> \<in> ElabRel"
+ varI [intro!]:
+ "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==>
+ <te,e_var(x),te_app(te,x)> \<in> ElabRel"
+ fnI [intro!]:
+ "[| te \<in> TyEnv; x \<in> ExVar; e \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;
+ <te_owr(te,x,t1),e,t2> \<in> ElabRel |] ==>
+ <te,e_fn(x,e),t_fun(t1,t2)> \<in> ElabRel"
+ fixI [intro!]:
+ "[| te \<in> TyEnv; f \<in> ExVar; x \<in> ExVar; t1 \<in> Ty; t2 \<in> Ty;
+ <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2> \<in> ElabRel |] ==>
+ <te,e_fix(f,x,e),t_fun(t1,t2)> \<in> ElabRel"
+ appI [intro]:
+ "[| te \<in> TyEnv; e1 \<in> Exp; e2 \<in> Exp; t1 \<in> Ty; t2 \<in> Ty;
+ <te,e1,t_fun(t1,t2)> \<in> ElabRel;
+ <te,e2,t1> \<in> ElabRel |] ==> <te,e_app(e1,e2),t2> \<in> ElabRel"
+ type_intros te_appI Exp.intros Ty.intros
+
+
+inductive_cases elab_constE [elim!]: "<te,e_const(c),t> \<in> ElabRel"
+inductive_cases elab_varE [elim!]: "<te,e_var(x),t> \<in> ElabRel"
+inductive_cases elab_fnE [elim]: "<te,e_fn(x,e),t> \<in> ElabRel"
+inductive_cases elab_fixE [elim!]: "<te,e_fix(f,x,e),t> \<in> ElabRel"
+inductive_cases elab_appE [elim]: "<te,e_app(e1,e2),t> \<in> ElabRel"
+
+declare ElabRel.dom_subset [THEN subsetD, dest]
end
--- a/src/ZF/Coind/Types.ML Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: ZF/Coind/Types.ML
- ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-*)
-
-val te_owrE = TyEnv.mk_cases "te_owr(te,f,t):TyEnv";
-
-Goal "te_app(te_owr(te,x,t),x) = t";
-by (Simp_tac 1);
-qed "te_app_owr1";
-
-Goal "x \\<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
-by Auto_tac;
-qed "te_app_owr2";
-
-Goal "[| te \\<in> TyEnv; x \\<in> ExVar; x \\<in> te_dom(te) |] ==> te_app(te,x):Ty";
-by (res_inst_tac [("P","x \\<in> te_dom(te)")] impE 1);
-by (assume_tac 2);
-by (assume_tac 2);
-by (etac TyEnv.induct 1);
-by (Simp_tac 1);
-by (case_tac "xa = x" 1);
-by Auto_tac;
-qed "te_appI";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/ZF/Coind/Types.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Types.thy Tue Dec 25 10:02:01 2001 +0100
@@ -4,15 +4,15 @@
Copyright 1995 University of Cambridge
*)
-Types = Language +
+theory Types = Language:
consts
- Ty :: i (* Datatype of types *)
+ Ty :: i (* Datatype of types *)
TyConst :: i (* Abstract type of type constants *)
datatype
- "Ty" = t_const ("tc \\<in> TyConst")
- | t_fun ("t1 \\<in> Ty","t2 \\<in> Ty")
+ "Ty" = t_const ("tc \<in> TyConst")
+ | t_fun ("t1 \<in> Ty","t2 \<in> Ty")
(* Definition of type environments and associated operators *)
@@ -22,24 +22,57 @@
datatype
"TyEnv" = te_emp
- | te_owr ("te \\<in> TyEnv","x \\<in> ExVar","t \\<in> Ty")
+ | te_owr ("te \<in> TyEnv","x \<in> ExVar","t \<in> Ty")
consts
- te_dom :: i => i
- te_app :: [i,i] => i
+ te_dom :: "i => i"
+ te_app :: "[i,i] => i"
primrec (*domain of the type environment*)
"te_dom (te_emp) = 0"
- "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"
+ "te_dom (te_owr(te,x,v)) = te_dom(te) Un {x}"
primrec (*lookup up identifiers in the type environment*)
"te_app (te_emp,x) = 0"
"te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"
-end
+inductive_cases te_owrE [elim!]: "te_owr(te,f,t) \<in> TyEnv"
+
+(*redundant??*)
+lemma te_app_owr1: "te_app(te_owr(te,x,t),x) = t"
+by simp
+
+(*redundant??*)
+lemma te_app_owr2: "x \<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"
+by auto
+
+lemma te_app_owr [simp]:
+ "te_app(te_owr(te,x,t),y) = (if x=y then t else te_app(te,y))"
+by auto
+
+lemma te_appI:
+ "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> te_app(te,x) \<in> Ty"
+apply (erule_tac P = "x \<in> te_dom (te) " in rev_mp)
+apply (erule TyEnv.induct)
+apply auto
+done
+
+
+
+
+
+
+
+
+
+
+
+
+
+end
--- a/src/ZF/Coind/Values.ML Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-(* Title: ZF/Coind/Values.ML
- ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-*)
-
-open Values;
-
-(* Elimination rules *)
-
-val prems = goalw Values.thy (Part_def::(tl (tl Val_ValEnv.defs)))
- "[| ve \\<in> ValEnv; !!m.[| ve=ve_mk(m); m \\<in> PMap(ExVar,Val) |] ==> Q |] ==> Q";
-by (cut_facts_tac prems 1);
-by (etac CollectE 1);
-by (etac exE 1);
-by (etac Val_ValEnv.elim 1);
-by (eresolve_tac prems 3);
-by (rewrite_tac Val_ValEnv.con_defs);
-by (ALLGOALS Fast_tac);
-qed "ValEnvE";
-
-val prems = goalw Values.thy (Part_def::[hd (tl Val_ValEnv.defs)])
- "[| v \\<in> Val; \
-\ !!c. [| v = v_const(c); c \\<in> Const |] ==> Q;\
-\ !!e ve x. \
-\ [| v = v_clos(x,e,ve); x \\<in> ExVar; e \\<in> Exp; ve \\<in> ValEnv |] ==> Q \
-\ |] ==> \
-\ Q";
-by (cut_facts_tac prems 1);
-by (etac CollectE 1);
-by (etac exE 1);
-by (etac Val_ValEnv.elim 1);
-by (eresolve_tac prems 1);
-by (assume_tac 1);
-by (eresolve_tac prems 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (rewrite_tac Val_ValEnv.con_defs);
-by (Fast_tac 1);
-qed "ValE";
-
-(* Nonempty sets *)
-
-Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
- "v_clos(x,e,ve) \\<noteq> 0";
-by (Blast_tac 1);
-qed "v_closNE";
-
-Addsimps [v_closNE];
-AddSEs [v_closNE RS notE];
-
-Goalw (QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
- "c \\<in> Const ==> v_const(c) \\<noteq> 0";
-by (dtac constNEE 1);
-by Auto_tac;
-qed "v_constNE";
-
-Addsimps [v_constNE];
-
-(* Proving that the empty set is not a value *)
-
-Goal "v \\<in> Val ==> v \\<noteq> 0";
-by (etac ValE 1);
-by Auto_tac;
-qed "ValNEE";
-
-(* Equalities for value environments *)
-
-Goal "[| ve \\<in> ValEnv; v \\<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
-by (etac ValEnvE 1);
-by (auto_tac (claset(),
- simpset() addsimps [map_domain_owr]));
-qed "ve_dom_owr";
-
-Goal "ve \\<in> ValEnv \
-\ ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))";
-by (etac ValEnvE 1);
-by (asm_simp_tac (simpset() addsimps [map_app_owr]) 1);
-qed "ve_app_owr";
-
-Goal "ve \\<in> ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v";
-by (etac ValEnvE 1);
-by (Asm_full_simp_tac 1);
-by (rtac map_app_owr1 1);
-qed "ve_app_owr1";
-
-Goal "ve \\<in> ValEnv ==> x \\<noteq> y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
-by (etac ValEnvE 1);
-by (Asm_full_simp_tac 1);
-by (rtac map_app_owr2 1);
-by (Fast_tac 1);
-qed "ve_app_owr2";
-
-(* Introduction rules for operators on value environments *)
-
-Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> ve_app(ve,x):Val";
-by (etac ValEnvE 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-by (rtac pmap_appI 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "ve_appI";
-
-Goal "[| ve \\<in> ValEnv; x \\<in> ve_dom(ve) |] ==> x \\<in> ExVar";
-by (etac ValEnvE 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-by (rtac pmap_domainD 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "ve_domI";
-
-Goalw [ve_emp_def] "ve_emp \\<in> ValEnv";
-by (rtac Val_ValEnv.ve_mk_I 1);
-by (rtac pmap_empI 1);
-qed "ve_empI";
-
-Goal "[|ve \\<in> ValEnv; x \\<in> ExVar; v \\<in> Val |] ==> ve_owr(ve,x,v):ValEnv";
-by (etac ValEnvE 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-by (rtac Val_ValEnv.ve_mk_I 1);
-by (etac pmap_owrI 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "ve_owrI";
-
-
-
--- a/src/ZF/Coind/Values.thy Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Values.thy Tue Dec 25 10:02:01 2001 +0100
@@ -4,25 +4,27 @@
Copyright 1995 University of Cambridge
*)
-Values = Language + Map +
+theory Values = Language + Map:
(* Values, values environments and associated operators *)
consts
- Val, ValEnv, Val_ValEnv :: i
+ Val :: i
+ ValEnv :: i
+ Val_ValEnv :: i;
codatatype
- "Val" = v_const ("c \\<in> Const")
- | v_clos ("x \\<in> ExVar","e \\<in> Exp","ve \\<in> ValEnv")
+ "Val" = v_const ("c \<in> Const")
+ | v_clos ("x \<in> ExVar","e \<in> Exp","ve \<in> ValEnv")
and
- "ValEnv" = ve_mk ("m \\<in> PMap(ExVar,Val)")
- monos map_mono
- type_intrs A_into_univ, mapQU
+ "ValEnv" = ve_mk ("m \<in> PMap(ExVar,Val)")
+ monos PMap_mono
+ type_intros A_into_univ mapQU
consts
- ve_owr :: [i,i,i] => i
- ve_dom :: i=>i
- ve_app :: [i,i] => i
+ ve_owr :: "[i,i,i] => i"
+ ve_dom :: "i=>i"
+ ve_app :: "[i,i] => i"
primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))"
@@ -35,7 +37,87 @@
ve_emp :: i
"ve_emp == ve_mk(map_emp)"
-end
+
+(* Elimination rules *)
+
+lemma ValEnvE:
+ "[| ve \<in> ValEnv; !!m.[| ve=ve_mk(m); m \<in> PMap(ExVar,Val) |] ==> Q |] ==> Q"
+apply (unfold Part_def Val_def ValEnv_def)
+apply (clarify );
+apply (erule Val_ValEnv.cases)
+apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs)
+done
+
+lemma ValE:
+ "[| v \<in> Val;
+ !!c. [| v = v_const(c); c \<in> Const |] ==> Q;
+ !!e ve x.
+ [| v = v_clos(x,e,ve); x \<in> ExVar; e \<in> Exp; ve \<in> ValEnv |] ==> Q
+ |] ==>
+ Q"
+apply (unfold Part_def Val_def ValEnv_def)
+apply (clarify );
+apply (erule Val_ValEnv.cases)
+apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs);
+done
+
+(* Nonempty sets *)
+
+lemma v_closNE [simp]: "v_clos(x,e,ve) \<noteq> 0"
+apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
+apply blast
+done
+
+declare v_closNE [THEN notE, elim!]
+
+
+lemma v_constNE [simp]: "c \<in> Const ==> v_const(c) \<noteq> 0"
+apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
+apply (drule constNEE)
+apply auto
+done
+(* Proving that the empty set is not a value *)
+lemma ValNEE: "v \<in> Val ==> v \<noteq> 0"
+by (erule ValE, auto)
+
+(* Equalities for value environments *)
+
+lemma ve_dom_owr [simp]:
+ "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"
+apply (erule ValEnvE)
+apply (auto simp add: map_domain_owr)
+done
+
+lemma ve_app_owr [simp]:
+ "ve \<in> ValEnv
+ ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))"
+by (erule ValEnvE, simp add: map_app_owr)
+
+(* Introduction rules for operators on value environments *)
+
+lemma ve_appI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> ve_app(ve,x):Val"
+by (erule ValEnvE, simp add: pmap_appI)
+
+lemma ve_domI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> x \<in> ExVar"
+apply (erule ValEnvE)
+apply (simp );
+apply (blast dest: pmap_domainD)
+done
+
+lemma ve_empI: "ve_emp \<in> ValEnv"
+apply (unfold ve_emp_def)
+apply (rule Val_ValEnv.intros)
+apply (rule pmap_empI)
+done
+
+lemma ve_owrI:
+ "[|ve \<in> ValEnv; x \<in> ExVar; v \<in> Val |] ==> ve_owr(ve,x,v):ValEnv"
+apply (erule ValEnvE)
+apply simp
+apply (blast intro: pmap_owrI Val_ValEnv.intros)
+done
+
+end
--- a/src/ZF/IsaMakefile Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/IsaMakefile Tue Dec 25 10:02:01 2001 +0100
@@ -75,10 +75,8 @@
ZF-Coind: ZF $(LOG)/ZF-Coind.gz
$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/BCR.thy Coind/Dynamic.thy \
- Coind/ECR.ML Coind/ECR.thy Coind/Language.thy Coind/MT.ML Coind/MT.thy \
- Coind/Map.ML Coind/Map.thy Coind/ROOT.ML Coind/Static.ML \
- Coind/Static.thy Coind/Types.ML Coind/Types.thy Coind/Values.ML \
- Coind/Values.thy
+ Coind/ECR.thy Coind/Language.thy Coind/Map.thy Coind/ROOT.ML \
+ Coind/Static.thy Coind/Types.thy Coind/Values.thy
@$(ISATOOL) usedir $(OUT)/ZF Coind
@@ -95,9 +93,9 @@
ZF-Resid: ZF $(LOG)/ZF-Resid.gz
-$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \
- Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \
- Resid/Substitution.thy
+$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML \
+ Resid/Confluence.thy Resid/Redex.thy \
+ Resid/Reduction.thy Resid/Residuals.thy Resid/Substitution.thy
@$(ISATOOL) usedir $(OUT)/ZF Resid
--- a/src/ZF/Resid/Conversion.thy Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* Title: Conversion.thy
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-
-*)
-
-Conversion = Confluence+
-
-consts
- Sconv1 :: i
- "<-1->" :: [i,i]=>o (infixl 50)
- Sconv :: i
- "<--->" :: [i,i]=>o (infixl 50)
-
-translations
- "a<-1->b" == "<a,b>:Sconv1"
- "a<--->b" == "<a,b>:Sconv"
-
-inductive
- domains "Sconv1" <= "lambda*lambda"
- intrs
- red1 "m -1-> n ==> m<-1->n"
- expl "n -1-> m ==> m<-1->n"
- type_intrs "[red1D1,red1D2]@lambda.intrs@bool_typechecks"
-
-inductive
- domains "Sconv" <= "lambda*lambda"
- intrs
- one_step "m<-1->n ==> m<--->n"
- refl "m \\<in> lambda ==> m<--->m"
- trans "[|m<--->n; n<--->p|] ==> m<--->p"
- type_intrs "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
-end
-
--- a/src/ZF/Resid/Cube.thy Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(* Title: Cube.thy
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-Cube = Residuals
--- a/src/ZF/Resid/Terms.thy Sat Dec 22 19:46:16 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Terms.thy
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-Terms = Cube+
-
-consts
- lambda :: i
- unmark :: i=>i
- Apl :: [i,i]=>i
-
-translations
- "Apl(n,m)" == "App(0,n,m)"
-
-inductive
- domains "lambda" <= "redexes"
- intrs
- Lambda_Var " n \\<in> nat ==> Var(n):lambda"
- Lambda_Fun " u \\<in> lambda ==> Fun(u):lambda"
- Lambda_App "[|u \\<in> lambda; v \\<in> lambda|]==> Apl(u,v):lambda"
- type_intrs "redexes.intrs@bool_typechecks"
-
-primrec
- "unmark(Var(n)) = Var(n)"
- "unmark(Fun(u)) = Fun(unmark(u))"
- "unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
-
-end
-
-