--- a/src/ZF/Coind/ECR.thy Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Coind/ECR.thy Tue Sep 27 16:51:35 2022 +0100
@@ -13,13 +13,13 @@
domains "HasTyRel" \<subseteq> "Val * Ty"
intros
htr_constI [intro!]:
- "[| c \<in> Const; t \<in> Ty; isof(c,t) |] ==> <v_const(c),t> \<in> HasTyRel"
+ "\<lbrakk>c \<in> Const; t \<in> Ty; isof(c,t)\<rbrakk> \<Longrightarrow> <v_const(c),t> \<in> HasTyRel"
htr_closI [intro]:
- "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;
+ "\<lbrakk>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(HasTyRel) |]
- ==> <v_clos(x,e,ve),t> \<in> HasTyRel"
+ {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in> Pow(HasTyRel)\<rbrakk>
+ \<Longrightarrow> <v_clos(x,e,ve),t> \<in> HasTyRel"
monos Pow_mono
type_intros Val_ValEnv.intros
@@ -27,18 +27,18 @@
definition
hastyenv :: "[i,i] => o" where
- "hastyenv(ve,te) ==
+ "hastyenv(ve,te) \<equiv>
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;
+ "\<lbrakk>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>} \<union> HasTyRel) |]
- ==> <v_clos(x, e, ve),t> \<in> HasTyRel"
+ Pow({<v_clos(x,e,ve),t>} \<union> HasTyRel)\<rbrakk>
+ \<Longrightarrow> <v_clos(x, e, ve),t> \<in> HasTyRel"
apply (rule singletonI [THEN HasTyRel.coinduct], auto)
done
@@ -55,12 +55,12 @@
HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE]
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))"
+ "\<lbrakk>ve \<in> ValEnv; te \<in> TyEnv; hastyenv(ve,te); <v,t> \<in> HasTyRel\<rbrakk>
+ \<Longrightarrow> 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)"
+ "\<lbrakk>ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te)\<rbrakk> \<Longrightarrow> hastyenv(ve,te)"
apply (unfold isofenv_def hastyenv_def)
apply (force intro: te_appI ve_domI)
done
@@ -71,20 +71,20 @@
(* ############################################################ *)
lemma consistency_const:
- "[| c \<in> Const; hastyenv(ve,te);<te,e_const(c),t> \<in> ElabRel |]
- ==> <v_const(c), t> \<in> HasTyRel"
+ "\<lbrakk>c \<in> Const; hastyenv(ve,te);<te,e_const(c),t> \<in> ElabRel\<rbrakk>
+ \<Longrightarrow> <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 |] ==>
+ "\<lbrakk>x \<in> ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t> \<in> ElabRel\<rbrakk> \<Longrightarrow>
<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);
+ "\<lbrakk>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"
+\<rbrakk> \<Longrightarrow> <v_clos(x, e, ve), t> \<in> HasTyRel"
by (unfold hastyenv_def, blast)
declare ElabRel.dom_subset [THEN subsetD, dest]
@@ -94,9 +94,9 @@
declare Val_ValEnv.intros [simp, intro!]
lemma consistency_fix:
- "[| ve \<in> ValEnv; x \<in> ExVar; e \<in> Exp; f \<in> ExVar; cl \<in> Val;
+ "\<lbrakk>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 |] ==>
+ hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel\<rbrakk> \<Longrightarrow>
<cl,t> \<in> HasTyRel"
apply (unfold hastyenv_def)
apply (erule elab_fixE, safe)
@@ -111,7 +111,7 @@
lemma consistency_app1:
- "[| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;
+ "\<lbrakk>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) \<longrightarrow> <te,e1,t> \<in> ElabRel \<longrightarrow> <v_const(c1),t> \<in> HasTyRel;
@@ -119,12 +119,12 @@
\<forall>t te.
hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <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"
+ <te,e_app(e1,e2),t> \<in> ElabRel\<rbrakk>
+ \<Longrightarrow> <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;
+ "\<lbrakk>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) \<longrightarrow>
@@ -134,8 +134,8 @@
<ve_owr(vem,xm,v2),em,v> \<in> EvalRel;
\<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) \<longrightarrow>
<te,em,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel;
- hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |]
- ==> <v,t> \<in> HasTyRel"
+ hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel\<rbrakk>
+ \<Longrightarrow> <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+)
@@ -151,7 +151,7 @@
lemma consistency [rule_format]:
"<ve,e,v> \<in> EvalRel
- ==> (\<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel)"
+ \<Longrightarrow> (\<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel)"
apply (erule EvalRel.induct)
apply (simp_all add: consistency_const consistency_var consistency_fn
consistency_fix consistency_app1)
@@ -159,9 +159,9 @@
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)"
+ "\<lbrakk>ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te);
+ <ve,e,v_const(c)> \<in> EvalRel; <te,e,t> \<in> ElabRel\<rbrakk>
+ \<Longrightarrow> isof(c,t)"
by (blast dest: consistency intro!: basic_consistency_lem)
end