section ‹Strong_Normalisation›

theory Strong_Normalisation
  imports Main
  abbrevs "⟶w" = "⟶⇩w"
      and "→p" = "→⇩p"
      and "⟶b" = "⟶⇩β"
begin

(* definition of types for combinatory terms *)

datatype tp = is_At:  TAtt "nat" | TArr "tp" "tp" (infixr "→⇩p" 200)

abbreviation is_Arr :: "tp ⇒ bool" where
  "is_Arr τ ≡ ¬ (is_At τ)"

(* head of a combinatory term *)

datatype (plugins del: size) hd =
  is_Var: Var (var: string)(type: tp) ("_:_" [100,100] 100)
| is_S : S (type: tp)  ("S:_" 100)
| is_K : K (type: tp)  ("K:_" 100)
| is_Sym: Sym (sym: string)(type: tp) ("_:_" [100,100] 100)

abbreviation is_Comb :: " hd ⇒ bool" where
  "is_Comb ζ ≡ (is_S ζ) ∨  (is_K ζ)"

subsection ‹Terms›

consts head0 :: 'a

(* combinatory term *)

datatype  tm =
  is_Hd: Hd "hd"
| App ("fun":  "tm") (arg: " tm")
where
  "head (App s _) = head0 s"
| "fun (Hd ζ) = Hd ζ"
| "arg (Hd ζ) = Hd ζ"

overloading head0 ≡ "head0 :: tm ⇒ hd"
begin

primrec head0 :: "tm ⇒ hd" where
  "head0 (Hd ζ) = ζ"
| "head0 (App s _) = head0 s"

end

subsection ‹Definition of types and combinators›

fun args :: "tm ⇒ tm list" where
  "args (Hd _) = []"
| "args (App s t) = args s @ [t]"

(* type of head symbol *)
definition type_hd :: "hd ⇒ tp" where
  "type_hd t = type(t)"

(* type of term *)
fun type :: "tm ⇒ tp" where
"type (Hd h) = type_hd h" |
"type (App s t) = (case (type s) of
                    TAtt τ ⇒ TAtt τ |
                    (α →⇩p γ) ⇒ γ)"

fun size_tp :: "tp ⇒ nat" where
 "size_tp (TAtt τ) = 0" |
 "size_tp (α →⇩p γ) = 1 + size_tp α + size_tp γ"

(* inductive predicate that holds if term is well-typed *)
inductive typed :: "tm ⇒ bool" where
"typed (Hd (Var _ _))" |
"typed (Hd (Sym _ _))" |
"typed (Hd (K (σ →⇩p γ →⇩p σ)))" |
"typed (Hd (S ((σ →⇩p τ →⇩p γ) →⇩p (σ →⇩p τ) →⇩p σ →⇩p γ)))" |
"typed t1 ⟹ (type t1 = (σ →⇩p γ)) ⟹ typed t2 ⟹ (type t1 = σ) ⟹ typed (App t1 t2)"


(* inductive definition of combinatory (weak) reduction *)
inductive
  weak_reduce :: "tm ⇒ tm ⇒ bool" (" _ ⟶⇩w _" [80,80] 80)
where
  w1[intro!]: "t1 ⟶⇩w t2 ⟹ App t1 t ⟶⇩w App t2 t"
| w2[intro!]: "t1 ⟶⇩w t2 ⟹ App t t1 ⟶⇩w App t t2"
| w4[intro!]: "App (App (Hd (K _)) t1) t2 ⟶⇩w t1"
| w7[intro!]: "App (App (App (Hd (S _)) t1) t2 ) t3 ⟶⇩w App (App t1 t3) (App t2 t3)"

inductive
 weak_star :: "tm ⇒ tm ⇒ nat ⇒ bool"  (" _ ⟶⇩w* _ _" [80,80] 80)
where
 ws1[intro!] : "t ⟶⇩w* t 0"
|ws2[intro!] : "⟦(t ⟶⇩w t'); (t' ⟶⇩w* t'' n)⟧ ⟹ (t ⟶⇩w* t'' (n+1))"

definition normal_form :: "tm ⇒ bool" where
 "normal_form t1 = (∀ x. ¬(t1 ⟶⇩w x))"

definition normalizable :: "tm ⇒ bool" where
 "normalizable t1 = (∃ x n. ((t1 ⟶⇩w* x n) ∧ (normal_form x)))"

definition bounded_sn :: "nat ⇒ tm ⇒ bool" where
  "bounded_sn n t1 ⟷ (∀m. ∀ t. (t1 ⟶⇩w* t m) ⟶ m ≤ n)"

definition sn :: "tm ⇒ bool" where
 "sn t1 = (∃n. bounded_sn n t1)"

function sc :: "tm ⇒ bool" where
 "sc t1 = (case (type t1) of
            TAtt τ ⇒ sn t1 |
            (α →⇩p γ) ⇒ (∀ t2. (type t2 = α) ⟶ (sc t2 ⟶  sc (App t1 t2) ) ))"
  by auto
  termination
    by (relation "measure (λ(t). size_tp (type t))") auto

lemma a3_10 :
  fixes τ :: "tp" and
        t :: "tm"
  assumes "typed t" and
          "type t = τ" and
          " ¬ (is_Comb (head t))"
  shows  "∀s ∈ (set (args t)). sn s ⟹ sc t" and
         "sc t ⟹ sn t"
  using assms
proof(induction "size_tp τ")
  case 0
  then show ?thesis sorry
next
  case (Suc x)
  then show ?thesis sorry
qed

proof(induction "size_tp τ")
  case 0
  case 1
  show ?case
    sorry
next
  case 0
  case 2
  show ?case
    sorry
next
  case (Suc x)
  case 1
  show ?case
    sorry
next
  case (Suc x)
  case 2
  show ?case
    sorry
qed