src/ZF/Coind/Values.ML
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1461 6bcb44e4d6e5
child 2034 5079fdf938dd
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/Coind/Values.ML
     2     ID:         $Id$
     3     Author:     Jacob Frost, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 *)
     6 
     7 open Values;
     8 
     9 (* Elimination rules *)
    10 
    11 val prems = goalw Values.thy (Part_def::(tl (tl Val_ValEnv.defs)))
    12   "[| ve:ValEnv; !!m.[| ve=ve_mk(m); m:PMap(ExVar,Val) |] ==> Q |] ==> Q";
    13 by (cut_facts_tac prems 1);
    14 by (etac CollectE 1);
    15 by (etac exE 1);
    16 by (etac Val_ValEnv.elim 1);
    17 by (eresolve_tac prems 3);
    18 by (rewrite_tac Val_ValEnv.con_defs);
    19 by (ALLGOALS (fast_tac qsum_cs));
    20 qed "ValEnvE";
    21 
    22 val prems = goalw Values.thy (Part_def::[hd (tl Val_ValEnv.defs)])
    23   "[| v:Val; \
    24 \     !!c. [| v = v_const(c); c:Const |] ==> Q;\
    25 \     !!e ve x. \
    26 \       [| v = v_clos(x,e,ve); x:ExVar; e:Exp; ve:ValEnv |] ==> Q \
    27 \  |] ==> \
    28 \  Q";
    29 by (cut_facts_tac prems 1);
    30 by (etac CollectE 1);
    31 by (etac exE 1);
    32 by (etac Val_ValEnv.elim 1);
    33 by (eresolve_tac prems 1);
    34 by (assume_tac 1);
    35 by (eresolve_tac prems 1);
    36 by (assume_tac 1);
    37 by (assume_tac 1);
    38 by (assume_tac 1);
    39 by (rewrite_tac Val_ValEnv.con_defs);
    40 by (fast_tac qsum_cs 1);
    41 qed "ValE";
    42 
    43 (* Nonempty sets *)
    44 
    45 val prems = goal Values.thy "A ~= 0 ==> EX a.a:A";
    46 by (cut_facts_tac prems 1);
    47 by (rtac (foundation RS disjE) 1);
    48 by (fast_tac ZF_cs 1);
    49 by (fast_tac ZF_cs 1);
    50 qed "set_notemptyE";
    51 
    52 goalw Values.thy (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
    53   "v_clos(x,e,ve) ~= 0";
    54 by (rtac not_emptyI 1);
    55 by (rtac UnI2 1);
    56 by (rtac SigmaI 1);
    57 by (rtac singletonI 1);
    58 by (rtac UnI1 1);
    59 by (fast_tac ZF_cs 1);
    60 qed "v_closNE";
    61 
    62 goalw Values.thy (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
    63   "!!c.c:Const ==> v_const(c) ~= 0";
    64 by (dtac constNEE 1);
    65 by (etac not_emptyE 1);
    66 by (rtac not_emptyI 1);
    67 by (rtac UnI2 1);
    68 by (rtac SigmaI 1);
    69 by (rtac singletonI 1);
    70 by (rtac UnI2 1);
    71 by (rtac SigmaI 1);
    72 by (rtac singletonI 1);
    73 by (assume_tac 1);
    74 qed "v_constNE";
    75 
    76 (* Proving that the empty set is not a value *)
    77 
    78 goal Values.thy "!!v.v:Val ==> v ~= 0";
    79 by (etac ValE 1);
    80 by (ALLGOALS hyp_subst_tac);
    81 by (etac v_constNE 1);
    82 by (rtac v_closNE 1);
    83 qed "ValNEE";
    84 
    85 (* Equalities for value environments *)
    86 
    87 val prems = goalw Values.thy [ve_dom_def,ve_owr_def]
    88   "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}";
    89 by (cut_facts_tac prems 1);
    90 by (etac ValEnvE 1);
    91 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
    92 by (rtac (map_domain_owr RS ssubst) 1);
    93 by (assume_tac 1);
    94 by (rtac Un_commute 1);
    95 qed "ve_dom_owr";
    96 
    97 goalw Values.thy [ve_app_def,ve_owr_def]
    98 "!!ve. ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v"; 
    99 by (etac ValEnvE 1);
   100 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
   101 by (rtac map_app_owr1 1);
   102 qed "ve_app_owr1";
   103 
   104 goalw Values.thy [ve_app_def,ve_owr_def]
   105  "!!ve.ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
   106 by (etac ValEnvE 1);
   107 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
   108 by (rtac map_app_owr2 1);
   109 by (fast_tac ZF_cs 1);
   110 qed "ve_app_owr2";
   111 
   112 (* Introduction rules for operators on value environments *)
   113 
   114 goalw Values.thy [ve_app_def,ve_owr_def,ve_dom_def]
   115   "!!ve.[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val";
   116 by (etac ValEnvE 1);
   117 by (hyp_subst_tac 1);
   118 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
   119 by (rtac pmap_appI 1);
   120 by (assume_tac 1);
   121 by (assume_tac 1);
   122 qed "ve_appI";
   123 
   124 goalw Values.thy [ve_dom_def]
   125   "!!ve.[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar";
   126 by (etac ValEnvE 1);
   127 by (hyp_subst_tac 1);
   128 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
   129 by (rtac pmap_domainD 1);
   130 by (assume_tac 1);
   131 by (assume_tac 1);
   132 qed "ve_domI";
   133 
   134 goalw Values.thy [ve_emp_def] "ve_emp:ValEnv";
   135 by (rtac Val_ValEnv.ve_mk_I 1);
   136 by (rtac pmap_empI 1);
   137 qed "ve_empI";
   138 
   139 goalw Values.thy [ve_owr_def] 
   140   "!!ve.[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv";
   141 by (etac ValEnvE 1);
   142 by (hyp_subst_tac 1);
   143 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1);
   144 by (rtac Val_ValEnv.ve_mk_I 1);
   145 by (etac pmap_owrI 1);
   146 by (assume_tac 1);
   147 by (assume_tac 1);
   148 qed "ve_owrI";
   149 
   150 
   151