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