Theory Specialisation_Examples

theory Specialisation_Examples
imports Main "~~/src/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 {* 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 {* 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) with `xa = x # xs` have "xa = x # y # zs" by simp
      moreover with `sorted xa` have "x ≤ y" and "sorted (y # zs)" by simp_all
      ultimately show ?thesis by (rule 3)
    qed
  qed
qed
thm sorted.equation

section {* Specialisation in POPLmark theory *}

notation
  Some ("⌊_⌋")

notation
  None ("⊥")

notation
  length ("\<parallel>_\<parallel>")

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" ("\<up>⇣τ")
where
  "\<up>⇣τ n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
| "\<up>⇣τ n k Top = Top"
| "\<up>⇣τ n k (T -> U) = \<up>⇣τ n k T -> \<up>⇣τ n k U"
| "\<up>⇣τ n k (∀<:T. U) = (∀<:\<up>⇣τ n k T. \<up>⇣τ n (k + 1) U)"

primrec lift :: "nat => nat => trm => trm" ("\<up>")
where
  "\<up> n k (Var i) = (if i < k then Var i else Var (i + n))"
| "\<up> n k (λ:T. t) = (λ:\<up>⇣τ n k T. \<up> n (k + 1) t)"
| "\<up> n k (λ<:T. t) = (λ<:\<up>⇣τ n k T. \<up> n (k + 1) t)"
| "\<up> n k (s • t) = \<up> n k s • \<up> n k t"
| "\<up> n k (t •⇣τ T) = \<up> n k t •⇣τ \<up>⇣τ n k T"

primrec substTT :: "type => nat => type => type"  ("_[_ \<mapsto>⇣τ _]⇣τ" [300, 0, 0] 300)
where
  "(TVar i)[k \<mapsto>⇣τ S]⇣τ =
     (if k < i then TVar (i - 1) else if i = k then \<up>⇣τ k 0 S else TVar i)"
| "Top[k \<mapsto>⇣τ S]⇣τ = Top"
| "(T -> U)[k \<mapsto>⇣τ S]⇣τ = T[k \<mapsto>⇣τ S]⇣τ -> U[k \<mapsto>⇣τ S]⇣τ"
| "(∀<:T. U)[k \<mapsto>⇣τ S]⇣τ = (∀<:T[k \<mapsto>⇣τ S]⇣τ. U[k+1 \<mapsto>⇣τ S]⇣τ)"

primrec decT :: "nat => nat => type => type"  ("\<down>⇣τ")
where
  "\<down>⇣τ 0 k T = T"
| "\<down>⇣τ (Suc n) k T = \<down>⇣τ n k (T[k \<mapsto>⇣τ Top]⇣τ)"

primrec subst :: "trm => nat => trm => trm"  ("_[_ \<mapsto> _]" [300, 0, 0] 300)
where
  "(Var i)[k \<mapsto> s] = (if k < i then Var (i - 1) else if i = k then \<up> k 0 s else Var i)"
| "(t • u)[k \<mapsto> s] = t[k \<mapsto> s] • u[k \<mapsto> s]"
| "(t •⇣τ T)[k \<mapsto> s] = t[k \<mapsto> s] •⇣τ \<down>⇣τ 1 k T"
| "(λ:T. t)[k \<mapsto> s] = (λ:\<down>⇣τ 1 k T. t[k+1 \<mapsto> s])"
| "(λ<:T. t)[k \<mapsto> s] = (λ<:\<down>⇣τ 1 k T. t[k+1 \<mapsto> s])"

primrec substT :: "trm => nat => type => trm"    ("_[_ \<mapsto>⇣τ _]" [300, 0, 0] 300)
where
  "(Var i)[k \<mapsto>⇣τ S] = (if k < i then Var (i - 1) else Var i)"
| "(t • u)[k \<mapsto>⇣τ S] = t[k \<mapsto>⇣τ S] • u[k \<mapsto>⇣τ S]"
| "(t •⇣τ T)[k \<mapsto>⇣τ S] = t[k \<mapsto>⇣τ S] •⇣τ T[k \<mapsto>⇣τ S]⇣τ"
| "(λ:T. t)[k \<mapsto>⇣τ S] = (λ:T[k \<mapsto>⇣τ S]⇣τ. t[k+1 \<mapsto>⇣τ S])"
| "(λ<:T. t)[k \<mapsto>⇣τ S] = (λ<:T[k \<mapsto>⇣τ S]⇣τ. t[k+1 \<mapsto>⇣τ S])"

primrec liftE :: "nat => nat => env => env" ("\<up>⇣e")
where
  "\<up>⇣e n k [] = []"
| "\<up>⇣e n k (B :: Γ) = mapB (\<up>⇣τ n (k + \<parallel>Γ\<parallel>)) B :: \<up>⇣e n k Γ"

primrec substE :: "env => nat => type => env"  ("_[_ \<mapsto>⇣τ _]⇣e" [300, 0, 0] 300)
where
  "[][k \<mapsto>⇣τ T]⇣e = []"
| "(B :: Γ)[k \<mapsto>⇣τ T]⇣e = mapB (λU. U[k + \<parallel>Γ\<parallel> \<mapsto>⇣τ T]⇣τ) B :: Γ[k \<mapsto>⇣τ T]⇣e"

primrec decE :: "nat => nat => env => env"  ("\<down>⇣e")
where
  "\<down>⇣e 0 k Γ = Γ"
| "\<down>⇣e (Suc n) k Γ = \<down>⇣e n k (Γ[k \<mapsto>⇣τ Top]⇣e)"

inductive
  well_formed :: "env => type => bool"  ("_ \<turnstile>⇘wf⇙ _" [50, 50] 50)
where
  wf_TVar: "Γ⟨i⟩ = ⌊TVarB T⌋ ==> Γ \<turnstile>⇘wf⇙ TVar i"
| wf_Top: "Γ \<turnstile>⇘wf⇙ Top"
| wf_arrow: "Γ \<turnstile>⇘wf⇙ T ==> Γ \<turnstile>⇘wf⇙ U ==> Γ \<turnstile>⇘wf⇙ T -> U"
| wf_all: "Γ \<turnstile>⇘wf⇙ T ==> TVarB T :: Γ \<turnstile>⇘wf⇙ U ==> Γ \<turnstile>⇘wf⇙ (∀<:T. U)"

inductive
  well_formedE :: "env => bool"  ("_ \<turnstile>⇘wf⇙" [50] 50)
  and well_formedB :: "env => binding => bool"  ("_ \<turnstile>⇘wfB⇙ _" [50, 50] 50)
where
  "Γ \<turnstile>⇘wfB⇙ B ≡ Γ \<turnstile>⇘wf⇙ type_ofB B"
| wf_Nil: "[] \<turnstile>⇘wf⇙"
| wf_Cons: "Γ \<turnstile>⇘wfB⇙ B ==> Γ \<turnstile>⇘wf⇙ ==> B :: Γ \<turnstile>⇘wf⇙"

inductive_cases well_formed_cases:
  "Γ \<turnstile>⇘wf⇙ TVar i"
  "Γ \<turnstile>⇘wf⇙ Top"
  "Γ \<turnstile>⇘wf⇙ T -> U"
  "Γ \<turnstile>⇘wf⇙ (∀<:T. U)"

inductive_cases well_formedE_cases:
  "B :: Γ \<turnstile>⇘wf⇙"

inductive
  subtyping :: "env => type => type => bool"  ("_ \<turnstile> _ <: _" [50, 50, 50] 50)
where
  SA_Top: "Γ \<turnstile>⇘wf⇙ ==> Γ \<turnstile>⇘wf⇙ S ==> Γ \<turnstile> S <: Top"
| SA_refl_TVar: "Γ \<turnstile>⇘wf⇙ ==> Γ \<turnstile>⇘wf⇙ TVar i ==> Γ \<turnstile> TVar i <: TVar i"
| SA_trans_TVar: "Γ⟨i⟩ = ⌊TVarB U⌋ ==>
    Γ \<turnstile> \<up>⇣τ (Suc i) 0 U <: T ==> Γ \<turnstile> TVar i <: T"
| SA_arrow: "Γ \<turnstile> T⇣1 <: S⇣1 ==> Γ \<turnstile> S⇣2 <: T⇣2 ==> Γ \<turnstile> S⇣1 -> S⇣2 <: T⇣1 -> T⇣2"
| SA_all: "Γ \<turnstile> T⇣1 <: S⇣1 ==> TVarB T⇣1 :: Γ \<turnstile> S⇣2 <: T⇣2 ==>
    Γ \<turnstile> (∀<:S⇣1. S⇣2) <: (∀<:T⇣1. T⇣2)"

inductive
  typing :: "env => trm => type => bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
where
  T_Var: "Γ \<turnstile>⇘wf⇙ ==> Γ⟨i⟩ = ⌊VarB U⌋ ==> T = \<up>⇣τ (Suc i) 0 U ==> Γ \<turnstile> Var i : T"
| T_Abs: "VarB T⇣1 :: Γ \<turnstile> t⇣2 : T⇣2 ==> Γ \<turnstile> (λ:T⇣1. t⇣2) : T⇣1 -> \<down>⇣τ 1 0 T⇣2"
| T_App: "Γ \<turnstile> t⇣1 : T⇣11 -> T⇣12 ==> Γ \<turnstile> t⇣2 : T⇣11 ==> Γ \<turnstile> t⇣1 • t⇣2 : T⇣12"
| T_TAbs: "TVarB T⇣1 :: Γ \<turnstile> t⇣2 : T⇣2 ==> Γ \<turnstile> (λ<:T⇣1. t⇣2) : (∀<:T⇣1. T⇣2)"
| T_TApp: "Γ \<turnstile> t⇣1 : (∀<:T⇣11. T⇣12) ==> Γ \<turnstile> T⇣2 <: T⇣11 ==>
    Γ \<turnstile> t⇣1 •⇣τ T⇣2 : T⇣12[0 \<mapsto>⇣τ T⇣2]⇣τ"
| T_Sub: "Γ \<turnstile> t : S ==> Γ \<turnstile> S <: T ==> Γ \<turnstile> 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
  "Γ \<turnstile> t : T ==> ¬ (Γ \<turnstile> 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