adding specialisation examples of the predicate compiler
authorbulwahn
Mon Mar 29 17:30:52 2010 +0200 (2010-03-29)
changeset 360337106f079bd05
parent 36032 dfd30b5b4e73
child 36034 ee84eac07290
adding specialisation examples of the predicate compiler
src/HOL/Predicate_Compile_Examples/ROOT.ML
src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Mon Mar 29 17:30:52 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Mon Mar 29 17:30:52 2010 +0200
     1.3 @@ -1,1 +1,1 @@
     1.4 -use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples"];
     1.5 +use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Mar 29 17:30:52 2010 +0200
     2.3 @@ -0,0 +1,241 @@
     2.4 +theory Specialisation_Examples
     2.5 +imports Main "../ex/Predicate_Compile_Alternative_Defs"
     2.6 +begin
     2.7 +
     2.8 +section {* Specialisation Examples *}
     2.9 +
    2.10 +fun nth_el'
    2.11 +where
    2.12 +  "nth_el' [] i = None"
    2.13 +| "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"
    2.14 +
    2.15 +definition
    2.16 +  "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
    2.17 +
    2.18 +code_pred (expected_modes: i => bool) [inductify] greater_than_index .
    2.19 +ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
    2.20 +
    2.21 +thm greater_than_index.equation
    2.22 +
    2.23 +values [expected "{()}"] "{x. greater_than_index [1,2,4,6]}"
    2.24 +values [expected "{}"] "{x. greater_than_index [0,2,3,2]}"
    2.25 +
    2.26 +subsection {* Common subterms *}
    2.27 +
    2.28 +text {* If a predicate is called with common subterms as arguments,
    2.29 +  this predicate should be specialised. 
    2.30 +*}
    2.31 +
    2.32 +definition max_nat :: "nat => nat => nat"
    2.33 +  where "max_nat a b = (if a <= b then b else a)"
    2.34 +
    2.35 +lemma [code_pred_inline]:
    2.36 +  "max = max_nat"
    2.37 +by (simp add: expand_fun_eq max_def max_nat_def)
    2.38 +
    2.39 +definition
    2.40 +  "max_of_my_Suc x = max x (Suc x)"
    2.41 +
    2.42 +text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
    2.43 +
    2.44 +code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
    2.45 +
    2.46 +thm max_of_my_SucP.equation
    2.47 +
    2.48 +ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_max_natP} *}
    2.49 +
    2.50 +values "{x. max_of_my_SucP x 6}"
    2.51 +
    2.52 +subsection {* Sorts *}
    2.53 +
    2.54 +code_pred [inductify] sorted .
    2.55 +thm sorted.equation
    2.56 +
    2.57 +section {* Specialisation in POPLmark theory *}
    2.58 +
    2.59 +notation
    2.60 +  Some ("\<lfloor>_\<rfloor>")
    2.61 +
    2.62 +notation
    2.63 +  None ("\<bottom>")
    2.64 +
    2.65 +notation
    2.66 +  length ("\<parallel>_\<parallel>")
    2.67 +
    2.68 +notation
    2.69 +  Cons ("_ \<Colon>/ _" [66, 65] 65)
    2.70 +
    2.71 +primrec
    2.72 +  nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
    2.73 +where
    2.74 +  "[]\<langle>i\<rangle> = \<bottom>"
    2.75 +| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> \<lfloor>x\<rfloor> | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
    2.76 +
    2.77 +primrec assoc :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" ("_\<langle>_\<rangle>\<^isub>?" [90, 0] 91)
    2.78 +where
    2.79 +  "[]\<langle>a\<rangle>\<^isub>? = \<bottom>"
    2.80 +| "(x # xs)\<langle>a\<rangle>\<^isub>? = (if fst x = a then \<lfloor>snd x\<rfloor> else xs\<langle>a\<rangle>\<^isub>?)"
    2.81 +
    2.82 +primrec unique :: "('a \<times> 'b) list \<Rightarrow> bool"
    2.83 +where
    2.84 +  "unique [] = True"
    2.85 +| "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^isub>? = \<bottom> \<and> unique xs)"
    2.86 +
    2.87 +datatype type =
    2.88 +    TVar nat
    2.89 +  | Top
    2.90 +  | Fun type type    (infixr "\<rightarrow>" 200)
    2.91 +  | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
    2.92 +
    2.93 +datatype binding = VarB type | TVarB type
    2.94 +types env = "binding list"
    2.95 +
    2.96 +primrec is_TVarB :: "binding \<Rightarrow> bool"
    2.97 +where
    2.98 +  "is_TVarB (VarB T) = False"
    2.99 +| "is_TVarB (TVarB T) = True"
   2.100 +
   2.101 +primrec type_ofB :: "binding \<Rightarrow> type"
   2.102 +where
   2.103 +  "type_ofB (VarB T) = T"
   2.104 +| "type_ofB (TVarB T) = T"
   2.105 +
   2.106 +primrec mapB :: "(type \<Rightarrow> type) \<Rightarrow> binding \<Rightarrow> binding"
   2.107 +where
   2.108 +  "mapB f (VarB T) = VarB (f T)"
   2.109 +| "mapB f (TVarB T) = TVarB (f T)"
   2.110 +
   2.111 +datatype trm =
   2.112 +    Var nat
   2.113 +  | Abs type trm   ("(3\<lambda>:_./ _)" [0, 10] 10)
   2.114 +  | TAbs type trm  ("(3\<lambda><:_./ _)" [0, 10] 10)
   2.115 +  | App trm trm    (infixl "\<bullet>" 200)
   2.116 +  | TApp trm type  (infixl "\<bullet>\<^isub>\<tau>" 200)
   2.117 +
   2.118 +primrec liftT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("\<up>\<^isub>\<tau>")
   2.119 +where
   2.120 +  "\<up>\<^isub>\<tau> n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
   2.121 +| "\<up>\<^isub>\<tau> n k Top = Top"
   2.122 +| "\<up>\<^isub>\<tau> n k (T \<rightarrow> U) = \<up>\<^isub>\<tau> n k T \<rightarrow> \<up>\<^isub>\<tau> n k U"
   2.123 +| "\<up>\<^isub>\<tau> n k (\<forall><:T. U) = (\<forall><:\<up>\<^isub>\<tau> n k T. \<up>\<^isub>\<tau> n (k + 1) U)"
   2.124 +
   2.125 +primrec lift :: "nat \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm" ("\<up>")
   2.126 +where
   2.127 +  "\<up> n k (Var i) = (if i < k then Var i else Var (i + n))"
   2.128 +| "\<up> n k (\<lambda>:T. t) = (\<lambda>:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)"
   2.129 +| "\<up> n k (\<lambda><:T. t) = (\<lambda><:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)"
   2.130 +| "\<up> n k (s \<bullet> t) = \<up> n k s \<bullet> \<up> n k t"
   2.131 +| "\<up> n k (t \<bullet>\<^isub>\<tau> T) = \<up> n k t \<bullet>\<^isub>\<tau> \<up>\<^isub>\<tau> n k T"
   2.132 +
   2.133 +primrec substTT :: "type \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type"  ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>\<tau>" [300, 0, 0] 300)
   2.134 +where
   2.135 +  "(TVar i)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> =
   2.136 +     (if k < i then TVar (i - 1) else if i = k then \<up>\<^isub>\<tau> k 0 S else TVar i)"
   2.137 +| "Top[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = Top"
   2.138 +| "(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>"
   2.139 +| "(\<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>)"
   2.140 +
   2.141 +primrec decT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type"  ("\<down>\<^isub>\<tau>")
   2.142 +where
   2.143 +  "\<down>\<^isub>\<tau> 0 k T = T"
   2.144 +| "\<down>\<^isub>\<tau> (Suc n) k T = \<down>\<^isub>\<tau> n k (T[k \<mapsto>\<^isub>\<tau> Top]\<^isub>\<tau>)"
   2.145 +
   2.146 +primrec subst :: "trm \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm"  ("_[_ \<mapsto> _]" [300, 0, 0] 300)
   2.147 +where
   2.148 +  "(Var i)[k \<mapsto> s] = (if k < i then Var (i - 1) else if i = k then \<up> k 0 s else Var i)"
   2.149 +| "(t \<bullet> u)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet> u[k \<mapsto> s]"
   2.150 +| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet>\<^isub>\<tau> \<down>\<^isub>\<tau> 1 k T"
   2.151 +| "(\<lambda>:T. t)[k \<mapsto> s] = (\<lambda>:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])"
   2.152 +| "(\<lambda><:T. t)[k \<mapsto> s] = (\<lambda><:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])"
   2.153 +
   2.154 +primrec substT :: "trm \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> trm"    ("_[_ \<mapsto>\<^isub>\<tau> _]" [300, 0, 0] 300)
   2.155 +where
   2.156 +  "(Var i)[k \<mapsto>\<^isub>\<tau> S] = (if k < i then Var (i - 1) else Var i)"
   2.157 +| "(t \<bullet> u)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet> u[k \<mapsto>\<^isub>\<tau> S]"
   2.158 +| "(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>"
   2.159 +| "(\<lambda>:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda>:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])"
   2.160 +| "(\<lambda><:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])"
   2.161 +
   2.162 +primrec liftE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env" ("\<up>\<^isub>e")
   2.163 +where
   2.164 +  "\<up>\<^isub>e n k [] = []"
   2.165 +| "\<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>"
   2.166 +
   2.167 +primrec substE :: "env \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> env"  ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>e" [300, 0, 0] 300)
   2.168 +where
   2.169 +  "[][k \<mapsto>\<^isub>\<tau> T]\<^isub>e = []"
   2.170 +| "(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"
   2.171 +
   2.172 +primrec decE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env"  ("\<down>\<^isub>e")
   2.173 +where
   2.174 +  "\<down>\<^isub>e 0 k \<Gamma> = \<Gamma>"
   2.175 +| "\<down>\<^isub>e (Suc n) k \<Gamma> = \<down>\<^isub>e n k (\<Gamma>[k \<mapsto>\<^isub>\<tau> Top]\<^isub>e)"
   2.176 +
   2.177 +inductive
   2.178 +  well_formed :: "env \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wf\<^esub> _" [50, 50] 50)
   2.179 +where
   2.180 +  wf_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB T\<rfloor> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
   2.181 +| wf_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
   2.182 +| wf_arrow: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
   2.183 +| 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)"
   2.184 +
   2.185 +inductive
   2.186 +  well_formedE :: "env \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wf\<^esub>" [50] 50)
   2.187 +  and well_formedB :: "env \<Rightarrow> binding \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wfB\<^esub> _" [50, 50] 50)
   2.188 +where
   2.189 +  "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<equiv> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> type_ofB B"
   2.190 +| wf_Nil: "[] \<turnstile>\<^bsub>wf\<^esub>"
   2.191 +| wf_Cons: "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
   2.192 +
   2.193 +inductive_cases well_formed_cases:
   2.194 +  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
   2.195 +  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
   2.196 +  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
   2.197 +  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
   2.198 +
   2.199 +inductive_cases well_formedE_cases:
   2.200 +  "B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
   2.201 +
   2.202 +inductive
   2.203 +  subtyping :: "env \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ <: _" [50, 50, 50] 50)
   2.204 +where
   2.205 +  SA_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> S \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
   2.206 +| SA_refl_TVar: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: TVar i"
   2.207 +| SA_trans_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB U\<rfloor> \<Longrightarrow>
   2.208 +    \<Gamma> \<turnstile> \<up>\<^isub>\<tau> (Suc i) 0 U <: T \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: T"
   2.209 +| 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"
   2.210 +| 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>
   2.211 +    \<Gamma> \<turnstile> (\<forall><:S\<^isub>1. S\<^isub>2) <: (\<forall><:T\<^isub>1. T\<^isub>2)"
   2.212 +
   2.213 +inductive
   2.214 +  typing :: "env \<Rightarrow> trm \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   2.215 +where
   2.216 +  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"
   2.217 +| 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"
   2.218 +| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>1\<^isub>2"
   2.219 +| 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)"
   2.220 +| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1 \<Longrightarrow>
   2.221 +    \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
   2.222 +| T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
   2.223 +
   2.224 +code_pred [inductify] typing .
   2.225 +
   2.226 +thm typing.equation
   2.227 +
   2.228 +values 6 "{(E, t, T). typing E t T}"
   2.229 +
   2.230 +subsection {* Higher-order predicate *}
   2.231 +
   2.232 +code_pred [inductify] mapB .
   2.233 +
   2.234 +subsection {* Multiple instances *}
   2.235 +
   2.236 +inductive subtype_refl' where
   2.237 +  "\<Gamma> \<turnstile> t : T ==> \<not> (\<Gamma> \<turnstile> T <: T) ==> subtype_refl' t T"
   2.238 +
   2.239 +code_pred (modes: i => i => bool, o => i => bool, i => o => bool, o => o => bool) [inductify] subtype_refl' .
   2.240 +
   2.241 +thm subtype_refl'.equation
   2.242 +
   2.243 +
   2.244 +end
   2.245 \ No newline at end of file