src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy

 | "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"
 
 definition
   "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
 
-code_pred (expected_modes: i => bool) [inductify] greater_than_index .
+code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
 ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
 
 thm greater_than_index.equation
 
 values [expected "{()}"] "{x. greater_than_index [1,2,4,6]}"

 definition
   "max_of_my_Suc x = max x (Suc x)"
 
 text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
 
-code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
+code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc .
 
 thm max_of_my_SucP.equation
 
 ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_max_natP} *}
 

 | 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)"
 | 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>
     \<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>"
 | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
 
-code_pred [inductify, skip_proof] typing .
+code_pred [inductify, skip_proof, specialise] typing .
 
 thm typing.equation
 
 values 6 "{(E, t, T). typing E t T}"