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