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