src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
author wenzelm
Mon Feb 25 12:17:50 2013 +0100 (2013-02-25)
changeset 51272 9c8d63b4b6be
parent 45125 c15b0faeb70a
child 53015 a1119cf551e8
permissions -rw-r--r--
prefer stateless 'ML_val' for tests;
bulwahn@36033
     1
theory Specialisation_Examples
wenzelm@41413
     2
imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
bulwahn@36033
     3
begin
bulwahn@36033
     4
bulwahn@45125
     5
declare [[values_timeout = 960.0]]
krauss@42142
     6
bulwahn@36033
     7
section {* Specialisation Examples *}
bulwahn@36033
     8
haftmann@39919
     9
primrec nth_el'
bulwahn@36033
    10
where
bulwahn@36033
    11
  "nth_el' [] i = None"
bulwahn@36033
    12
| "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"
bulwahn@36033
    13
bulwahn@36033
    14
definition
bulwahn@36033
    15
  "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
bulwahn@36033
    16
bulwahn@36257
    17
code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
wenzelm@51272
    18
ML_val {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
bulwahn@36033
    19
bulwahn@36033
    20
thm greater_than_index.equation
bulwahn@36033
    21
bulwahn@36033
    22
values [expected "{()}"] "{x. greater_than_index [1,2,4,6]}"
bulwahn@36033
    23
values [expected "{}"] "{x. greater_than_index [0,2,3,2]}"
bulwahn@36033
    24
bulwahn@36033
    25
subsection {* Common subterms *}
bulwahn@36033
    26
bulwahn@36033
    27
text {* If a predicate is called with common subterms as arguments,
bulwahn@36033
    28
  this predicate should be specialised. 
bulwahn@36033
    29
*}
bulwahn@36033
    30
bulwahn@36033
    31
definition max_nat :: "nat => nat => nat"
bulwahn@36033
    32
  where "max_nat a b = (if a <= b then b else a)"
bulwahn@36033
    33
bulwahn@36033
    34
lemma [code_pred_inline]:
bulwahn@36033
    35
  "max = max_nat"
nipkow@39302
    36
by (simp add: fun_eq_iff max_def max_nat_def)
bulwahn@36033
    37
bulwahn@36033
    38
definition
bulwahn@36033
    39
  "max_of_my_Suc x = max x (Suc x)"
bulwahn@36033
    40
bulwahn@36033
    41
text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
bulwahn@36033
    42
bulwahn@36257
    43
code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc .
bulwahn@36033
    44
bulwahn@36033
    45
thm max_of_my_SucP.equation
bulwahn@36033
    46
wenzelm@51272
    47
ML_val {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
bulwahn@36033
    48
bulwahn@36033
    49
values "{x. max_of_my_SucP x 6}"
bulwahn@36033
    50
bulwahn@36033
    51
subsection {* Sorts *}
bulwahn@36033
    52
haftmann@39919
    53
declare sorted.Nil [code_pred_intro]
haftmann@39919
    54
  sorted_single [code_pred_intro]
haftmann@39919
    55
  sorted_many [code_pred_intro]
haftmann@39919
    56
haftmann@39919
    57
code_pred sorted proof -
haftmann@39919
    58
  assume "sorted xa"
haftmann@39919
    59
  assume 1: "xa = [] \<Longrightarrow> thesis"
haftmann@39919
    60
  assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
haftmann@39919
    61
  assume 3: "\<And>x y zs. xa = x # y # zs \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> thesis"
haftmann@39919
    62
  show thesis proof (cases xa)
haftmann@39919
    63
    case Nil with 1 show ?thesis .
haftmann@39919
    64
  next
haftmann@39919
    65
    case (Cons x xs) show ?thesis proof (cases xs)
haftmann@39919
    66
      case Nil with Cons 2 show ?thesis by simp
haftmann@39919
    67
    next
haftmann@39919
    68
      case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
haftmann@39919
    69
      moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
haftmann@39919
    70
      ultimately show ?thesis by (rule 3)
haftmann@39919
    71
    qed
haftmann@39919
    72
  qed
haftmann@39919
    73
qed
bulwahn@36033
    74
thm sorted.equation
bulwahn@36033
    75
bulwahn@36033
    76
section {* Specialisation in POPLmark theory *}
bulwahn@36033
    77
bulwahn@36033
    78
notation
bulwahn@36033
    79
  Some ("\<lfloor>_\<rfloor>")
bulwahn@36033
    80
bulwahn@36033
    81
notation
bulwahn@36033
    82
  None ("\<bottom>")
bulwahn@36033
    83
bulwahn@36033
    84
notation
bulwahn@36033
    85
  length ("\<parallel>_\<parallel>")
bulwahn@36033
    86
bulwahn@36033
    87
notation
bulwahn@36033
    88
  Cons ("_ \<Colon>/ _" [66, 65] 65)
bulwahn@36033
    89
bulwahn@36033
    90
primrec
bulwahn@36033
    91
  nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
bulwahn@36033
    92
where
bulwahn@36033
    93
  "[]\<langle>i\<rangle> = \<bottom>"
bulwahn@36033
    94
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> \<lfloor>x\<rfloor> | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
bulwahn@36033
    95
bulwahn@36033
    96
primrec assoc :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" ("_\<langle>_\<rangle>\<^isub>?" [90, 0] 91)
bulwahn@36033
    97
where
bulwahn@36033
    98
  "[]\<langle>a\<rangle>\<^isub>? = \<bottom>"
bulwahn@36033
    99
| "(x # xs)\<langle>a\<rangle>\<^isub>? = (if fst x = a then \<lfloor>snd x\<rfloor> else xs\<langle>a\<rangle>\<^isub>?)"
bulwahn@36033
   100
bulwahn@36033
   101
primrec unique :: "('a \<times> 'b) list \<Rightarrow> bool"
bulwahn@36033
   102
where
bulwahn@36033
   103
  "unique [] = True"
bulwahn@36033
   104
| "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^isub>? = \<bottom> \<and> unique xs)"
bulwahn@36033
   105
bulwahn@36033
   106
datatype type =
bulwahn@36033
   107
    TVar nat
bulwahn@36033
   108
  | Top
bulwahn@36033
   109
  | Fun type type    (infixr "\<rightarrow>" 200)
bulwahn@36033
   110
  | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
bulwahn@36033
   111
bulwahn@36033
   112
datatype binding = VarB type | TVarB type
wenzelm@42463
   113
type_synonym env = "binding list"
bulwahn@36033
   114
bulwahn@36033
   115
primrec is_TVarB :: "binding \<Rightarrow> bool"
bulwahn@36033
   116
where
bulwahn@36033
   117
  "is_TVarB (VarB T) = False"
bulwahn@36033
   118
| "is_TVarB (TVarB T) = True"
bulwahn@36033
   119
bulwahn@36033
   120
primrec type_ofB :: "binding \<Rightarrow> type"
bulwahn@36033
   121
where
bulwahn@36033
   122
  "type_ofB (VarB T) = T"
bulwahn@36033
   123
| "type_ofB (TVarB T) = T"
bulwahn@36033
   124
bulwahn@36033
   125
primrec mapB :: "(type \<Rightarrow> type) \<Rightarrow> binding \<Rightarrow> binding"
bulwahn@36033
   126
where
bulwahn@36033
   127
  "mapB f (VarB T) = VarB (f T)"
bulwahn@36033
   128
| "mapB f (TVarB T) = TVarB (f T)"
bulwahn@36033
   129
bulwahn@36033
   130
datatype trm =
bulwahn@36033
   131
    Var nat
bulwahn@36033
   132
  | Abs type trm   ("(3\<lambda>:_./ _)" [0, 10] 10)
bulwahn@36033
   133
  | TAbs type trm  ("(3\<lambda><:_./ _)" [0, 10] 10)
bulwahn@36033
   134
  | App trm trm    (infixl "\<bullet>" 200)
bulwahn@36033
   135
  | TApp trm type  (infixl "\<bullet>\<^isub>\<tau>" 200)
bulwahn@36033
   136
bulwahn@36033
   137
primrec liftT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("\<up>\<^isub>\<tau>")
bulwahn@36033
   138
where
bulwahn@36033
   139
  "\<up>\<^isub>\<tau> n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
bulwahn@36033
   140
| "\<up>\<^isub>\<tau> n k Top = Top"
bulwahn@36033
   141
| "\<up>\<^isub>\<tau> n k (T \<rightarrow> U) = \<up>\<^isub>\<tau> n k T \<rightarrow> \<up>\<^isub>\<tau> n k U"
bulwahn@36033
   142
| "\<up>\<^isub>\<tau> n k (\<forall><:T. U) = (\<forall><:\<up>\<^isub>\<tau> n k T. \<up>\<^isub>\<tau> n (k + 1) U)"
bulwahn@36033
   143
bulwahn@36033
   144
primrec lift :: "nat \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm" ("\<up>")
bulwahn@36033
   145
where
bulwahn@36033
   146
  "\<up> n k (Var i) = (if i < k then Var i else Var (i + n))"
bulwahn@36033
   147
| "\<up> n k (\<lambda>:T. t) = (\<lambda>:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)"
bulwahn@36033
   148
| "\<up> n k (\<lambda><:T. t) = (\<lambda><:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)"
bulwahn@36033
   149
| "\<up> n k (s \<bullet> t) = \<up> n k s \<bullet> \<up> n k t"
bulwahn@36033
   150
| "\<up> n k (t \<bullet>\<^isub>\<tau> T) = \<up> n k t \<bullet>\<^isub>\<tau> \<up>\<^isub>\<tau> n k T"
bulwahn@36033
   151
bulwahn@36033
   152
primrec substTT :: "type \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type"  ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>\<tau>" [300, 0, 0] 300)
bulwahn@36033
   153
where
bulwahn@36033
   154
  "(TVar i)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> =
bulwahn@36033
   155
     (if k < i then TVar (i - 1) else if i = k then \<up>\<^isub>\<tau> k 0 S else TVar i)"
bulwahn@36033
   156
| "Top[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = Top"
bulwahn@36033
   157
| "(T \<rightarrow> U)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> \<rightarrow> U[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>"
bulwahn@36033
   158
| "(\<forall><:T. U)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = (\<forall><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. U[k+1 \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>)"
bulwahn@36033
   159
bulwahn@36033
   160
primrec decT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type"  ("\<down>\<^isub>\<tau>")
bulwahn@36033
   161
where
bulwahn@36033
   162
  "\<down>\<^isub>\<tau> 0 k T = T"
bulwahn@36033
   163
| "\<down>\<^isub>\<tau> (Suc n) k T = \<down>\<^isub>\<tau> n k (T[k \<mapsto>\<^isub>\<tau> Top]\<^isub>\<tau>)"
bulwahn@36033
   164
bulwahn@36033
   165
primrec subst :: "trm \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm"  ("_[_ \<mapsto> _]" [300, 0, 0] 300)
bulwahn@36033
   166
where
bulwahn@36033
   167
  "(Var i)[k \<mapsto> s] = (if k < i then Var (i - 1) else if i = k then \<up> k 0 s else Var i)"
bulwahn@36033
   168
| "(t \<bullet> u)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet> u[k \<mapsto> s]"
bulwahn@36033
   169
| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet>\<^isub>\<tau> \<down>\<^isub>\<tau> 1 k T"
bulwahn@36033
   170
| "(\<lambda>:T. t)[k \<mapsto> s] = (\<lambda>:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])"
bulwahn@36033
   171
| "(\<lambda><:T. t)[k \<mapsto> s] = (\<lambda><:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])"
bulwahn@36033
   172
bulwahn@36033
   173
primrec substT :: "trm \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> trm"    ("_[_ \<mapsto>\<^isub>\<tau> _]" [300, 0, 0] 300)
bulwahn@36033
   174
where
bulwahn@36033
   175
  "(Var i)[k \<mapsto>\<^isub>\<tau> S] = (if k < i then Var (i - 1) else Var i)"
bulwahn@36033
   176
| "(t \<bullet> u)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet> u[k \<mapsto>\<^isub>\<tau> S]"
bulwahn@36033
   177
| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet>\<^isub>\<tau> T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>"
bulwahn@36033
   178
| "(\<lambda>:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda>:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])"
bulwahn@36033
   179
| "(\<lambda><:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])"
bulwahn@36033
   180
bulwahn@36033
   181
primrec liftE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env" ("\<up>\<^isub>e")
bulwahn@36033
   182
where
bulwahn@36033
   183
  "\<up>\<^isub>e n k [] = []"
bulwahn@36033
   184
| "\<up>\<^isub>e n k (B \<Colon> \<Gamma>) = mapB (\<up>\<^isub>\<tau> n (k + \<parallel>\<Gamma>\<parallel>)) B \<Colon> \<up>\<^isub>e n k \<Gamma>"
bulwahn@36033
   185
bulwahn@36033
   186
primrec substE :: "env \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> env"  ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>e" [300, 0, 0] 300)
bulwahn@36033
   187
where
bulwahn@36033
   188
  "[][k \<mapsto>\<^isub>\<tau> T]\<^isub>e = []"
bulwahn@36033
   189
| "(B \<Colon> \<Gamma>)[k \<mapsto>\<^isub>\<tau> T]\<^isub>e = mapB (\<lambda>U. U[k + \<parallel>\<Gamma>\<parallel> \<mapsto>\<^isub>\<tau> T]\<^isub>\<tau>) B \<Colon> \<Gamma>[k \<mapsto>\<^isub>\<tau> T]\<^isub>e"
bulwahn@36033
   190
bulwahn@36033
   191
primrec decE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env"  ("\<down>\<^isub>e")
bulwahn@36033
   192
where
bulwahn@36033
   193
  "\<down>\<^isub>e 0 k \<Gamma> = \<Gamma>"
bulwahn@36033
   194
| "\<down>\<^isub>e (Suc n) k \<Gamma> = \<down>\<^isub>e n k (\<Gamma>[k \<mapsto>\<^isub>\<tau> Top]\<^isub>e)"
bulwahn@36033
   195
bulwahn@36033
   196
inductive
bulwahn@36033
   197
  well_formed :: "env \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wf\<^esub> _" [50, 50] 50)
bulwahn@36033
   198
where
bulwahn@36033
   199
  wf_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB T\<rfloor> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
bulwahn@36033
   200
| wf_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
bulwahn@36033
   201
| wf_arrow: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
bulwahn@36033
   202
| wf_all: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> TVarB T \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
bulwahn@36033
   203
bulwahn@36033
   204
inductive
bulwahn@36033
   205
  well_formedE :: "env \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wf\<^esub>" [50] 50)
bulwahn@36033
   206
  and well_formedB :: "env \<Rightarrow> binding \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wfB\<^esub> _" [50, 50] 50)
bulwahn@36033
   207
where
bulwahn@36033
   208
  "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<equiv> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> type_ofB B"
bulwahn@36033
   209
| wf_Nil: "[] \<turnstile>\<^bsub>wf\<^esub>"
bulwahn@36033
   210
| wf_Cons: "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
bulwahn@36033
   211
bulwahn@36033
   212
inductive_cases well_formed_cases:
bulwahn@36033
   213
  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
bulwahn@36033
   214
  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
bulwahn@36033
   215
  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
bulwahn@36033
   216
  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
bulwahn@36033
   217
bulwahn@36033
   218
inductive_cases well_formedE_cases:
bulwahn@36033
   219
  "B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
bulwahn@36033
   220
bulwahn@36033
   221
inductive
bulwahn@36033
   222
  subtyping :: "env \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ <: _" [50, 50, 50] 50)
bulwahn@36033
   223
where
bulwahn@36033
   224
  SA_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> S \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
bulwahn@36033
   225
| SA_refl_TVar: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: TVar i"
bulwahn@36033
   226
| SA_trans_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB U\<rfloor> \<Longrightarrow>
bulwahn@36033
   227
    \<Gamma> \<turnstile> \<up>\<^isub>\<tau> (Suc i) 0 U <: T \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: T"
bulwahn@36033
   228
| SA_arrow: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2"
bulwahn@36033
   229
| SA_all: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow>
bulwahn@36033
   230
    \<Gamma> \<turnstile> (\<forall><:S\<^isub>1. S\<^isub>2) <: (\<forall><:T\<^isub>1. T\<^isub>2)"
bulwahn@36033
   231
bulwahn@36033
   232
inductive
bulwahn@36033
   233
  typing :: "env \<Rightarrow> trm \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
bulwahn@36033
   234
where
bulwahn@36033
   235
  T_Var: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^isub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T"
bulwahn@36033
   236
| T_Abs: "VarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> \<down>\<^isub>\<tau> 1 0 T\<^isub>2"
haftmann@39919
   237
| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>11 \<rightarrow> T\<^isub>12 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>12"
bulwahn@36033
   238
| T_TAbs: "TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda><:T\<^isub>1. t\<^isub>2) : (\<forall><:T\<^isub>1. T\<^isub>2)"
haftmann@39919
   239
| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>11. T\<^isub>12) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11 \<Longrightarrow>
haftmann@39919
   240
    \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>12[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
bulwahn@36033
   241
| T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
bulwahn@36033
   242
bulwahn@36257
   243
code_pred [inductify, skip_proof, specialise] typing .
bulwahn@36033
   244
bulwahn@36033
   245
thm typing.equation
bulwahn@36033
   246
bulwahn@36033
   247
values 6 "{(E, t, T). typing E t T}"
bulwahn@36033
   248
bulwahn@36033
   249
subsection {* Higher-order predicate *}
bulwahn@36033
   250
bulwahn@36033
   251
code_pred [inductify] mapB .
bulwahn@36033
   252
bulwahn@36033
   253
subsection {* Multiple instances *}
bulwahn@36033
   254
bulwahn@36033
   255
inductive subtype_refl' where
bulwahn@36033
   256
  "\<Gamma> \<turnstile> t : T ==> \<not> (\<Gamma> \<turnstile> T <: T) ==> subtype_refl' t T"
bulwahn@36033
   257
bulwahn@36033
   258
code_pred (modes: i => i => bool, o => i => bool, i => o => bool, o => o => bool) [inductify] subtype_refl' .
bulwahn@36033
   259
bulwahn@36033
   260
thm subtype_refl'.equation
bulwahn@36033
   261
bulwahn@36033
   262
bulwahn@45125
   263
end