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