src/ZF/Coind/Values.ML

--- 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";
-
-
-