src/HOL/ex/MT.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 17289 8608f7a881eb
child 24326 3e9d3ba894b8
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
clasohm@1476
     1
(*  Title:      HOL/ex/mt.thy
clasohm@969
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
clasohm@969
     4
    Copyright   1993  University of Cambridge
clasohm@969
     5
clasohm@969
     6
Based upon the article
clasohm@969
     7
    Robin Milner and Mads Tofte,
clasohm@969
     8
    Co-induction in Relational Semantics,
clasohm@969
     9
    Theoretical Computer Science 87 (1991), pages 209-220.
clasohm@969
    10
clasohm@969
    11
Written up as
clasohm@969
    12
    Jacob Frost, A Case Study of Co_induction in Isabelle/HOL
clasohm@969
    13
    Report 308, Computer Lab, University of Cambridge (1993).
clasohm@969
    14
*)
clasohm@969
    15
wenzelm@17289
    16
theory MT
wenzelm@17289
    17
imports Main
wenzelm@17289
    18
begin
clasohm@969
    19
wenzelm@17289
    20
typedecl Const
clasohm@969
    21
wenzelm@17289
    22
typedecl ExVar
wenzelm@17289
    23
typedecl Ex
clasohm@969
    24
wenzelm@17289
    25
typedecl TyConst
wenzelm@17289
    26
typedecl Ty
clasohm@969
    27
wenzelm@17289
    28
typedecl Clos
wenzelm@17289
    29
typedecl Val
clasohm@969
    30
wenzelm@17289
    31
typedecl ValEnv
wenzelm@17289
    32
typedecl TyEnv
clasohm@969
    33
clasohm@969
    34
consts
paulson@15450
    35
  c_app :: "[Const, Const] => Const"
clasohm@969
    36
paulson@15450
    37
  e_const :: "Const => Ex"
paulson@15450
    38
  e_var :: "ExVar => Ex"
paulson@15450
    39
  e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
paulson@15450
    40
  e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
wenzelm@17289
    41
  e_app :: "[Ex, Ex] => Ex" ("_ @@ _" [51,51] 1000)
paulson@15450
    42
  e_const_fst :: "Ex => Const"
clasohm@969
    43
paulson@15450
    44
  t_const :: "TyConst => Ty"
paulson@15450
    45
  t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
clasohm@969
    46
paulson@15450
    47
  v_const :: "Const => Val"
paulson@15450
    48
  v_clos :: "Clos => Val"
wenzelm@17289
    49
clasohm@1376
    50
  ve_emp :: ValEnv
paulson@15450
    51
  ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
paulson@15450
    52
  ve_dom :: "ValEnv => ExVar set"
paulson@15450
    53
  ve_app :: "[ValEnv, ExVar] => Val"
clasohm@969
    54
paulson@15450
    55
  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
clasohm@969
    56
clasohm@1376
    57
  te_emp :: TyEnv
paulson@15450
    58
  te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
paulson@15450
    59
  te_app :: "[TyEnv, ExVar] => Ty"
paulson@15450
    60
  te_dom :: "TyEnv => ExVar set"
clasohm@969
    61
clasohm@969
    62
  eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
clasohm@969
    63
  eval_rel :: "((ValEnv * Ex) * Val) set"
paulson@15450
    64
  eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
clasohm@969
    65
clasohm@969
    66
  elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
clasohm@969
    67
  elab_rel :: "((TyEnv * Ex) * Ty) set"
paulson@15450
    68
  elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
wenzelm@17289
    69
paulson@15450
    70
  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
paulson@15450
    71
  isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
clasohm@969
    72
clasohm@969
    73
  hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
clasohm@969
    74
  hasty_rel :: "(Val * Ty) set"
paulson@15450
    75
  hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
paulson@15450
    76
  hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
clasohm@969
    77
wenzelm@17289
    78
axioms
clasohm@969
    79
wenzelm@17289
    80
(*
clasohm@969
    81
  Expression constructors must be injective, distinct and it must be possible
clasohm@969
    82
  to do induction over expressions.
clasohm@969
    83
*)
clasohm@969
    84
clasohm@969
    85
(* All the constructors are injective *)
clasohm@969
    86
wenzelm@17289
    87
  e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2"
wenzelm@17289
    88
  e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
wenzelm@17289
    89
  e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
wenzelm@17289
    90
  e_fix_inj:
wenzelm@17289
    91
    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
wenzelm@17289
    92
     ev11 = ev21 & ev12 = ev22 & e1 = e2
clasohm@1151
    93
   "
wenzelm@17289
    94
  e_app_inj: "e11 @@ e12 = e21 @@ e22 ==> e11 = e21 & e12 = e22"
clasohm@969
    95
clasohm@969
    96
(* All constructors are distinct *)
clasohm@969
    97
wenzelm@17289
    98
  e_disj_const_var: "~e_const(c) = e_var(ev)"
wenzelm@17289
    99
  e_disj_const_fn: "~e_const(c) = fn ev => e"
wenzelm@17289
   100
  e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e"
wenzelm@17289
   101
  e_disj_const_app: "~e_const(c) = e1 @@ e2"
wenzelm@17289
   102
  e_disj_var_fn: "~e_var(ev1) = fn ev2 => e"
wenzelm@17289
   103
  e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e"
wenzelm@17289
   104
  e_disj_var_app: "~e_var(ev) = e1 @@ e2"
wenzelm@17289
   105
  e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2"
wenzelm@17289
   106
  e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22"
wenzelm@17289
   107
  e_disj_fix_app: "~fix ev11(ev12) = e1 = e21 @@ e22"
clasohm@969
   108
clasohm@969
   109
(* Strong elimination, induction on expressions  *)
clasohm@969
   110
wenzelm@17289
   111
  e_ind:
wenzelm@17289
   112
    " [|  !!ev. P(e_var(ev));
wenzelm@17289
   113
         !!c. P(e_const(c));
wenzelm@17289
   114
         !!ev e. P(e) ==> P(fn ev => e);
wenzelm@17289
   115
         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e);
wenzelm@17289
   116
         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @@ e2)
wenzelm@17289
   117
     |] ==>
wenzelm@17289
   118
   P(e)
clasohm@1151
   119
   "
clasohm@969
   120
clasohm@969
   121
(* Types - same scheme as for expressions *)
clasohm@969
   122
wenzelm@17289
   123
(* All constructors are injective *)
clasohm@969
   124
wenzelm@17289
   125
  t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2"
wenzelm@17289
   126
  t_fun_inj: "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22"
clasohm@969
   127
clasohm@969
   128
(* All constructors are distinct, not needed so far ... *)
clasohm@969
   129
clasohm@969
   130
(* Strong elimination, induction on types *)
clasohm@969
   131
wenzelm@17289
   132
 t_ind:
wenzelm@17289
   133
    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |]
clasohm@1151
   134
    ==> P(t)"
clasohm@969
   135
clasohm@969
   136
clasohm@969
   137
(* Values - same scheme again *)
clasohm@969
   138
wenzelm@17289
   139
(* All constructors are injective *)
clasohm@969
   140
wenzelm@17289
   141
  v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2"
wenzelm@17289
   142
  v_clos_inj:
wenzelm@17289
   143
    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
clasohm@1151
   144
     ev1 = ev2 & e1 = e2 & ve1 = ve2"
wenzelm@17289
   145
clasohm@969
   146
(* All constructors are distinct *)
clasohm@969
   147
wenzelm@17289
   148
  v_disj_const_clos: "~v_const(c) = v_clos(cl)"
clasohm@969
   149
paulson@15450
   150
(* No induction on values: they are a codatatype! ... *)
clasohm@969
   151
clasohm@969
   152
wenzelm@17289
   153
(*
clasohm@969
   154
  Value environments bind variables to values. Only the following trivial
clasohm@969
   155
  properties are needed.
clasohm@969
   156
*)
clasohm@969
   157
wenzelm@17289
   158
  ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}"
wenzelm@17289
   159
wenzelm@17289
   160
  ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v"
wenzelm@17289
   161
  ve_app_owr2: "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2"
clasohm@969
   162
clasohm@969
   163
clasohm@969
   164
(* Type Environments bind variables to types. The following trivial
clasohm@969
   165
properties are needed.  *)
clasohm@969
   166
wenzelm@17289
   167
  te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}"
wenzelm@17289
   168
wenzelm@17289
   169
  te_app_owr1: "te_app (te + {ev |=> t}) ev=t"
wenzelm@17289
   170
  te_app_owr2: "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2"
clasohm@969
   171
clasohm@969
   172
clasohm@969
   173
(* The dynamic semantics is defined inductively by a set of inference
clasohm@969
   174
rules.  These inference rules allows one to draw conclusions of the form ve
clasohm@969
   175
|- e ---> v, read the expression e evaluates to the value v in the value
clasohm@969
   176
environment ve.  Therefore the relation _ |- _ ---> _ is defined in Isabelle
clasohm@969
   177
as the least fixpoint of the functor eval_fun below.  From this definition
clasohm@969
   178
introduction rules and a strong elimination (induction) rule can be
wenzelm@17289
   179
derived.
clasohm@969
   180
*)
clasohm@969
   181
wenzelm@17289
   182
defs
wenzelm@17289
   183
  eval_fun_def:
wenzelm@17289
   184
    " eval_fun(s) ==
wenzelm@17289
   185
     { pp.
wenzelm@17289
   186
       (? ve c. pp=((ve,e_const(c)),v_const(c))) |
clasohm@1151
   187
       (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
wenzelm@17289
   188
       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))|
wenzelm@17289
   189
       ( ? ve e x f cl.
wenzelm@17289
   190
           pp=((ve,fix f(x) = e),v_clos(cl)) &
wenzelm@17289
   191
           cl=<|x, e, ve+{f |-> v_clos(cl)} |>
wenzelm@17289
   192
       ) |
wenzelm@17289
   193
       ( ? ve e1 e2 c1 c2.
wenzelm@17289
   194
           pp=((ve,e1 @@ e2),v_const(c_app c1 c2)) &
wenzelm@17289
   195
           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s
wenzelm@17289
   196
       ) |
wenzelm@17289
   197
       ( ? ve vem e1 e2 em xm v v2.
wenzelm@17289
   198
           pp=((ve,e1 @@ e2),v) &
wenzelm@17289
   199
           ((ve,e1),v_clos(<|xm,em,vem|>)):s &
wenzelm@17289
   200
           ((ve,e2),v2):s &
wenzelm@17289
   201
           ((vem+{xm |-> v2},em),v):s
wenzelm@17289
   202
       )
clasohm@1151
   203
     }"
clasohm@969
   204
wenzelm@17289
   205
  eval_rel_def: "eval_rel == lfp(eval_fun)"
wenzelm@17289
   206
  eval_def: "ve |- e ---> v == ((ve,e),v):eval_rel"
clasohm@969
   207
clasohm@969
   208
(* The static semantics is defined in the same way as the dynamic
clasohm@969
   209
semantics.  The relation te |- e ===> t express the expression e has the
clasohm@969
   210
type t in the type environment te.
clasohm@969
   211
*)
clasohm@969
   212
wenzelm@17289
   213
  elab_fun_def:
wenzelm@17289
   214
  "elab_fun(s) ==
wenzelm@17289
   215
  { pp.
wenzelm@17289
   216
    (? te c t. pp=((te,e_const(c)),t) & c isof t) |
wenzelm@17289
   217
    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
wenzelm@17289
   218
    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
wenzelm@17289
   219
    (? te f x e t1 t2.
wenzelm@17289
   220
       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
wenzelm@17289
   221
    ) |
wenzelm@17289
   222
    (? te e1 e2 t1 t2.
wenzelm@17289
   223
       pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
wenzelm@17289
   224
    )
clasohm@1151
   225
  }"
clasohm@969
   226
wenzelm@17289
   227
  elab_rel_def: "elab_rel == lfp(elab_fun)"
wenzelm@17289
   228
  elab_def: "te |- e ===> t == ((te,e),t):elab_rel"
clasohm@969
   229
clasohm@969
   230
(* The original correspondence relation *)
clasohm@969
   231
wenzelm@17289
   232
  isof_env_def:
wenzelm@17289
   233
    " ve isofenv te ==
wenzelm@17289
   234
     ve_dom(ve) = te_dom(te) &
wenzelm@17289
   235
     ( ! x.
wenzelm@17289
   236
         x:ve_dom(ve) -->
wenzelm@17289
   237
         (? c. ve_app ve x = v_const(c) & c isof te_app te x)
wenzelm@17289
   238
     )
clasohm@1151
   239
   "
clasohm@969
   240
wenzelm@17289
   241
axioms
wenzelm@17289
   242
  isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
clasohm@969
   243
wenzelm@17289
   244
defs
clasohm@969
   245
(* The extented correspondence relation *)
clasohm@969
   246
wenzelm@17289
   247
  hasty_fun_def:
wenzelm@17289
   248
    " hasty_fun(r) ==
wenzelm@17289
   249
     { p.
wenzelm@17289
   250
       ( ? c t. p = (v_const(c),t) & c isof t) |
wenzelm@17289
   251
       ( ? ev e ve t te.
wenzelm@17289
   252
           p = (v_clos(<|ev,e,ve|>),t) &
wenzelm@17289
   253
           te |- fn ev => e ===> t &
wenzelm@17289
   254
           ve_dom(ve) = te_dom(te) &
wenzelm@17289
   255
           (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
wenzelm@17289
   256
       )
wenzelm@17289
   257
     }
clasohm@1151
   258
   "
clasohm@969
   259
wenzelm@17289
   260
  hasty_rel_def: "hasty_rel == gfp(hasty_fun)"
wenzelm@17289
   261
  hasty_def: "v hasty t == (v,t) : hasty_rel"
wenzelm@17289
   262
  hasty_env_def:
wenzelm@17289
   263
    " ve hastyenv te ==
wenzelm@17289
   264
     ve_dom(ve) = te_dom(te) &
clasohm@1151
   265
     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
clasohm@969
   266
wenzelm@17289
   267
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17289
   268
clasohm@969
   269
end