# Theory Specialisation_Examples

theory Specialisation_Examples
imports Predicate_Compile_Alternative_Defs
```theory Specialisation_Examples
imports Main "HOL-Library.Predicate_Compile_Alternative_Defs"
begin

declare [[values_timeout = 960.0]]

section ‹Specialisation Examples›

primrec nth_el'
where
"nth_el' [] i = None"
| "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"

definition
"greater_than_index xs = (∀i x. nth_el' xs i = Some x --> x > i)"

code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
ML_val ‹Core_Data.intros_of @{context} @{const_name specialised_nth_el'P}›

thm greater_than_index.equation

values [expected "{()}"] "{x. greater_than_index [1,2,4,6]}"
values [expected "{}"] "{x. greater_than_index [0,2,3,2]}"

subsection ‹Common subterms›

text ‹If a predicate is called with common subterms as arguments,
this predicate should be specialised.
›

definition max_nat :: "nat => nat => nat"
where "max_nat a b = (if a <= b then b else a)"

lemma [code_pred_inline]:
"max = max_nat"
by (simp add: fun_eq_iff max_def max_nat_def)

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, specialise, skip_proof] max_of_my_Suc .

thm max_of_my_SucP.equation

ML_val ‹Core_Data.intros_of @{context} @{const_name specialised_max_natP}›

values "{x. max_of_my_SucP x 6}"

subsection ‹Sorts›

declare sorted.Nil [code_pred_intro]
sorted_single [code_pred_intro]
sorted_many [code_pred_intro]

code_pred sorted
proof -
assume "sorted xa"
assume 1: "xa = [] ⟹ thesis"
assume 2: "⋀x. xa = [x] ⟹ thesis"
assume 3: "⋀x y zs. xa = x # y # zs ⟹ x ≤ y ⟹ sorted (y # zs) ⟹ thesis"
show thesis proof (cases xa)
case Nil with 1 show ?thesis .
next
case (Cons x xs) show ?thesis proof (cases xs)
case Nil with Cons 2 show ?thesis by simp
next
case (Cons y zs)
show ?thesis
proof (rule 3)
from Cons ‹xa = x # xs› show "xa = x # y # zs" by simp
with ‹sorted xa› show "x ≤ y" and "sorted (y # zs)" by simp_all
qed
qed
qed
qed
thm sorted.equation

section ‹Specialisation in POPLmark theory›

notation
Some ("⌊_⌋")

notation
None ("⊥")

notation
length ("∥_∥")

notation
Cons ("_ ∷/ _" [66, 65] 65)

primrec
nth_el :: "'a list ⇒ nat ⇒ 'a option" ("_⟨_⟩" [90, 0] 91)
where
"[]⟨i⟩ = ⊥"
| "(x # xs)⟨i⟩ = (case i of 0 ⇒ ⌊x⌋ | Suc j ⇒ xs ⟨j⟩)"

primrec assoc :: "('a × 'b) list ⇒ 'a ⇒ 'b option" ("_⟨_⟩⇩?" [90, 0] 91)
where
"[]⟨a⟩⇩? = ⊥"
| "(x # xs)⟨a⟩⇩? = (if fst x = a then ⌊snd x⌋ else xs⟨a⟩⇩?)"

primrec unique :: "('a × 'b) list ⇒ bool"
where
"unique [] = True"
| "unique (x # xs) = (xs⟨fst x⟩⇩? = ⊥ ∧ unique xs)"

datatype type =
TVar nat
| Top
| Fun type type    (infixr "→" 200)
| TyAll type type  ("(3∀<:_./ _)" [0, 10] 10)

datatype binding = VarB type | TVarB type
type_synonym env = "binding list"

primrec is_TVarB :: "binding ⇒ bool"
where
"is_TVarB (VarB T) = False"
| "is_TVarB (TVarB T) = True"

primrec type_ofB :: "binding ⇒ type"
where
"type_ofB (VarB T) = T"
| "type_ofB (TVarB T) = T"

primrec mapB :: "(type ⇒ type) ⇒ binding ⇒ binding"
where
"mapB f (VarB T) = VarB (f T)"
| "mapB f (TVarB T) = TVarB (f T)"

datatype trm =
Var nat
| Abs type trm   ("(3λ:_./ _)" [0, 10] 10)
| TAbs type trm  ("(3λ<:_./ _)" [0, 10] 10)
| App trm trm    (infixl "∙" 200)
| TApp trm type  (infixl "∙⇩τ" 200)

primrec liftT :: "nat ⇒ nat ⇒ type ⇒ type" ("↑⇩τ")
where
"↑⇩τ n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
| "↑⇩τ n k Top = Top"
| "↑⇩τ n k (T → U) = ↑⇩τ n k T → ↑⇩τ n k U"
| "↑⇩τ n k (∀<:T. U) = (∀<:↑⇩τ n k T. ↑⇩τ n (k + 1) U)"

primrec lift :: "nat ⇒ nat ⇒ trm ⇒ trm" ("↑")
where
"↑ n k (Var i) = (if i < k then Var i else Var (i + n))"
| "↑ n k (λ:T. t) = (λ:↑⇩τ n k T. ↑ n (k + 1) t)"
| "↑ n k (λ<:T. t) = (λ<:↑⇩τ n k T. ↑ n (k + 1) t)"
| "↑ n k (s ∙ t) = ↑ n k s ∙ ↑ n k t"
| "↑ n k (t ∙⇩τ T) = ↑ n k t ∙⇩τ ↑⇩τ n k T"

primrec substTT :: "type ⇒ nat ⇒ type ⇒ type"  ("_[_ ↦⇩τ _]⇩τ" [300, 0, 0] 300)
where
"(TVar i)[k ↦⇩τ S]⇩τ =
(if k < i then TVar (i - 1) else if i = k then ↑⇩τ k 0 S else TVar i)"
| "Top[k ↦⇩τ S]⇩τ = Top"
| "(T → U)[k ↦⇩τ S]⇩τ = T[k ↦⇩τ S]⇩τ → U[k ↦⇩τ S]⇩τ"
| "(∀<:T. U)[k ↦⇩τ S]⇩τ = (∀<:T[k ↦⇩τ S]⇩τ. U[k+1 ↦⇩τ S]⇩τ)"

primrec decT :: "nat ⇒ nat ⇒ type ⇒ type"  ("↓⇩τ")
where
"↓⇩τ 0 k T = T"
| "↓⇩τ (Suc n) k T = ↓⇩τ n k (T[k ↦⇩τ Top]⇩τ)"

primrec subst :: "trm ⇒ nat ⇒ trm ⇒ trm"  ("_[_ ↦ _]" [300, 0, 0] 300)
where
"(Var i)[k ↦ s] = (if k < i then Var (i - 1) else if i = k then ↑ k 0 s else Var i)"
| "(t ∙ u)[k ↦ s] = t[k ↦ s] ∙ u[k ↦ s]"
| "(t ∙⇩τ T)[k ↦ s] = t[k ↦ s] ∙⇩τ ↓⇩τ 1 k T"
| "(λ:T. t)[k ↦ s] = (λ:↓⇩τ 1 k T. t[k+1 ↦ s])"
| "(λ<:T. t)[k ↦ s] = (λ<:↓⇩τ 1 k T. t[k+1 ↦ s])"

primrec substT :: "trm ⇒ nat ⇒ type ⇒ trm"    ("_[_ ↦⇩τ _]" [300, 0, 0] 300)
where
"(Var i)[k ↦⇩τ S] = (if k < i then Var (i - 1) else Var i)"
| "(t ∙ u)[k ↦⇩τ S] = t[k ↦⇩τ S] ∙ u[k ↦⇩τ S]"
| "(t ∙⇩τ T)[k ↦⇩τ S] = t[k ↦⇩τ S] ∙⇩τ T[k ↦⇩τ S]⇩τ"
| "(λ:T. t)[k ↦⇩τ S] = (λ:T[k ↦⇩τ S]⇩τ. t[k+1 ↦⇩τ S])"
| "(λ<:T. t)[k ↦⇩τ S] = (λ<:T[k ↦⇩τ S]⇩τ. t[k+1 ↦⇩τ S])"

primrec liftE :: "nat ⇒ nat ⇒ env ⇒ env" ("↑⇩e")
where
"↑⇩e n k [] = []"
| "↑⇩e n k (B ∷ Γ) = mapB (↑⇩τ n (k + ∥Γ∥)) B ∷ ↑⇩e n k Γ"

primrec substE :: "env ⇒ nat ⇒ type ⇒ env"  ("_[_ ↦⇩τ _]⇩e" [300, 0, 0] 300)
where
"[][k ↦⇩τ T]⇩e = []"
| "(B ∷ Γ)[k ↦⇩τ T]⇩e = mapB (λU. U[k + ∥Γ∥ ↦⇩τ T]⇩τ) B ∷ Γ[k ↦⇩τ T]⇩e"

primrec decE :: "nat ⇒ nat ⇒ env ⇒ env"  ("↓⇩e")
where
"↓⇩e 0 k Γ = Γ"
| "↓⇩e (Suc n) k Γ = ↓⇩e n k (Γ[k ↦⇩τ Top]⇩e)"

inductive
well_formed :: "env ⇒ type ⇒ bool"  ("_ ⊢⇩w⇩f _" [50, 50] 50)
where
wf_TVar: "Γ⟨i⟩ = ⌊TVarB T⌋ ⟹ Γ ⊢⇩w⇩f TVar i"
| wf_Top: "Γ ⊢⇩w⇩f Top"
| wf_arrow: "Γ ⊢⇩w⇩f T ⟹ Γ ⊢⇩w⇩f U ⟹ Γ ⊢⇩w⇩f T → U"
| wf_all: "Γ ⊢⇩w⇩f T ⟹ TVarB T ∷ Γ ⊢⇩w⇩f U ⟹ Γ ⊢⇩w⇩f (∀<:T. U)"

inductive
well_formedE :: "env ⇒ bool"  ("_ ⊢⇩w⇩f" [50] 50)
and well_formedB :: "env ⇒ binding ⇒ bool"  ("_ ⊢⇩w⇩f⇩B _" [50, 50] 50)
where
"Γ ⊢⇩w⇩f⇩B B ≡ Γ ⊢⇩w⇩f type_ofB B"
| wf_Nil: "[] ⊢⇩w⇩f"
| wf_Cons: "Γ ⊢⇩w⇩f⇩B B ⟹ Γ ⊢⇩w⇩f ⟹ B ∷ Γ ⊢⇩w⇩f"

inductive_cases well_formed_cases:
"Γ ⊢⇩w⇩f TVar i"
"Γ ⊢⇩w⇩f Top"
"Γ ⊢⇩w⇩f T → U"
"Γ ⊢⇩w⇩f (∀<:T. U)"

inductive_cases well_formedE_cases:
"B ∷ Γ ⊢⇩w⇩f"

inductive
subtyping :: "env ⇒ type ⇒ type ⇒ bool"  ("_ ⊢ _ <: _" [50, 50, 50] 50)
where
SA_Top: "Γ ⊢⇩w⇩f ⟹ Γ ⊢⇩w⇩f S ⟹ Γ ⊢ S <: Top"
| SA_refl_TVar: "Γ ⊢⇩w⇩f ⟹ Γ ⊢⇩w⇩f TVar i ⟹ Γ ⊢ TVar i <: TVar i"
| SA_trans_TVar: "Γ⟨i⟩ = ⌊TVarB U⌋ ⟹
Γ ⊢ ↑⇩τ (Suc i) 0 U <: T ⟹ Γ ⊢ TVar i <: T"
| SA_arrow: "Γ ⊢ T⇩1 <: S⇩1 ⟹ Γ ⊢ S⇩2 <: T⇩2 ⟹ Γ ⊢ S⇩1 → S⇩2 <: T⇩1 → T⇩2"
| SA_all: "Γ ⊢ T⇩1 <: S⇩1 ⟹ TVarB T⇩1 ∷ Γ ⊢ S⇩2 <: T⇩2 ⟹
Γ ⊢ (∀<:S⇩1. S⇩2) <: (∀<:T⇩1. T⇩2)"

inductive
typing :: "env ⇒ trm ⇒ type ⇒ bool"    ("_ ⊢ _ : _" [50, 50, 50] 50)
where
T_Var: "Γ ⊢⇩w⇩f ⟹ Γ⟨i⟩ = ⌊VarB U⌋ ⟹ T = ↑⇩τ (Suc i) 0 U ⟹ Γ ⊢ Var i : T"
| T_Abs: "VarB T⇩1 ∷ Γ ⊢ t⇩2 : T⇩2 ⟹ Γ ⊢ (λ:T⇩1. t⇩2) : T⇩1 → ↓⇩τ 1 0 T⇩2"
| T_App: "Γ ⊢ t⇩1 : T⇩11 → T⇩12 ⟹ Γ ⊢ t⇩2 : T⇩11 ⟹ Γ ⊢ t⇩1 ∙ t⇩2 : T⇩12"
| T_TAbs: "TVarB T⇩1 ∷ Γ ⊢ t⇩2 : T⇩2 ⟹ Γ ⊢ (λ<:T⇩1. t⇩2) : (∀<:T⇩1. T⇩2)"
| T_TApp: "Γ ⊢ t⇩1 : (∀<:T⇩11. T⇩12) ⟹ Γ ⊢ T⇩2 <: T⇩11 ⟹
Γ ⊢ t⇩1 ∙⇩τ T⇩2 : T⇩12[0 ↦⇩τ T⇩2]⇩τ"
| T_Sub: "Γ ⊢ t : S ⟹ Γ ⊢ S <: T ⟹ Γ ⊢ t : T"

code_pred [inductify, skip_proof, specialise] typing .

thm typing.equation

values 6 "{(E, t, T). typing E t T}"

subsection ‹Higher-order predicate›

code_pred [inductify] mapB .

subsection ‹Multiple instances›

inductive subtype_refl' where
"Γ ⊢ t : T ==> ¬ (Γ ⊢ T <: T) ==> subtype_refl' t T"

code_pred (modes: i => i => bool, o => i => bool, i => o => bool, o => o => bool) [inductify] subtype_refl' .

thm subtype_refl'.equation

end
```