Theory Tait

(*<*)
theory Tait = Main:
(*>*)

text {*
In this section, we will compare the Coq and Minlog formalizations
of the normalization proof with a formalization in the theorem prover
Isabelle/HOL. We start by giving the definition of types and terms:
*}

(*<*)
lemma cheating: "PROP P" sorry

typedecl name

consts inj_name :: "nat => name"          ("\<sharp> _" 100)

lemma name_eq_dec: "((n::name) = n') ∨ (n ≠ n')"
  sorry

consts
  name_eq_dec :: "name => name => sumbool"

realizers
  name_eq_dec: "name_eq_dec" "cheating · _"
(*>*)
datatype type =  
   Iota                 
 | Arrow type type         (infix "\<rightharpoonup>" 80)

datatype trm = 
   Var name        ("´_" 90)             
 | App trm trm     (infix "¨" 80)
 | Abs name trm    (" λ[_]._ " [70,70] 80)
(*<*)
types ctxt = "name => type" 

types substitution = "name => trm" 

constdefs 
 subst_id :: substitution
 "subst_id x ≡ ´x"

constdefs
 update :: "(name=>'a)=>name=>'a=>name=>'a"
 "update f x a y ≡ if x=y then a else f y"


consts TypJ :: "(ctxt×trm×type)set"
syntax "_TypJ" :: "ctxt => trm => type => bool"   (" _ \<turnstile> _ : _" [80,80,80] 80)
translations " (ρs \<turnstile> r : ρ)" \<rightleftharpoons> "(ρs,r,ρ) ∈ TypJ"
inductive TypJ
intros
 Typ_Var : " ρs \<turnstile> ´x : ρs x"
 Typ_Abs : "(update ρs x ρ) \<turnstile> r : σ ==> 
            ρs \<turnstile> λ[x].r : ρ\<rightharpoonup>σ"
 Typ_App : "ρs \<turnstile> r : ρ\<rightharpoonup>σ  ==> 
            ρs \<turnstile> s : ρ  ==> 
            ρs \<turnstile> r¨s : σ"

consts sub :: "trm => substitution => trm" (infix "•" 70)

axioms sub_Var : "(´x)•ϑ == ϑ x"  
axioms sub_App : "(r¨s)•ϑ == (r•ϑ)¨(s•ϑ)"
axioms sub_id :  "r•subst_id = r"

consts F :: "trm => nat => bool" 
consts N :: "trm => trm => bool" 
consts A :: "trm => trm => bool"
consts H :: "trm => trm => bool"

constdefs 
 SN :: "trm => bool"
 "SN r ≡ ∀k. F r k --> (∃s. N r s)" 
 SA :: "trm => bool"
 "SA r ≡ ∀k. F r k --> (∃s. A r s)" 
(*>*)

text {*
The judgement stating that @{term t} has type @{term "τ"} in context
@{term "ρs"} is denoted by \mbox{@{term "ρs \<turnstile> t : τ"}}. The definition of
the typing judgement is as usual.
In contrast to Minlog, Isabelle/HOL allows the definition of predicates
by recursion over datatypes (also called ``strong elimination'' in Coq
jargon). Thus, we can simply define @{text SC} by recursion over the
datatype @{text type}:
*}

consts SC :: "type => trm => bool"
primrec 
SC_Atom: "SC Iota r = SN r"
SC_Fun: "SC (ρ\<rightharpoonup>σ) r = (∀s. (SC ρ s) --> (SC σ (r¨s)))"
(*<*)
declare SN_def [extraction_expand]
declare SA_def [extraction_expand]
(*>*)

text {*
However, when it comes to extracting a program from a proof involving
@{text SC}, we face a problem: Since predicates in a proof become types
in the extracted program, predicates such as @{text SC} defined by recursion
on datatypes give rise to programs using dependent types. Such programs
can neither be expressed inside Isabelle/HOL, nor can they easily be
translated to functional programming languages such as ML. In order
to get a program which is typable in a functional programming language
without dependent types, we realize the formula @{term "SC τ t"} by
a datatype @{text D} with two constructors @{term "Term"} and @{term "Func"}.
The former corresponds to the case where @{term "τ"} is a base type,
whereas the latter corresponds to the case where @{term "τ"} is a
function type. In ML, one would define the datatype @{text D} as follows:
\begin{verbatim}
  datatype D = Term of nat -> trm | Func of trm -> D -> D
\end{verbatim}
This datatype is beyond the scope of Isabelle/HOL, since @{text D}
occurs {\it negatively} in the argument type of @{text Func}.
It is interesting to note that in the logic HOLCF, which is a conservative
extension of HOL with LCF, one can actually define the above datatype,
provided that the type of partial continuous functions is used instead
of the type of total functions.
For the moment, we just assert the existence of type @{text D}, together
with suitable constructors:
*}

typedecl D

consts
  Term :: "(nat => trm) => D"
  Func :: "(trm => D => D) => D"
  destTerm :: "D => nat => trm"
  destFunc :: "D => trm => D => D"
(*<*)
  realizes_SC :: "D => type => trm => bool"

extract_type
  "typeof (SC T t) ≡ Type (TYPE(D))"

realizability
  "(realizes e (SC T t)) ≡ (realizes_SC e T t)"
(*>*)

text {*
Here, @{term destTerm} and @{term destFunc} are {\it destructors}
corresponding to the constructors of the datatype @{text D}. These
can be implemented using pattern matching. We can now assign
realizing terms to the two characteristic equations for @{term SC}.
Since we can view an equation between propositions as a conjunction
of two implications, the equations for @{term SC} are realized
by pairs, of which the first component is a destructor, and the second
component is a constructor:
*}

realizers
  SC_Atom: "λ t. (destTerm, Term)" (*<*) "cheating · _" (*>*)

  SC_Fun: "λ ρ σ t. (destFunc, Func)" (*<*) "cheating · _" (*>*)
(*<*)
axioms 
 Ax1 : "F r k ==> 
        N (r¨´\<sharp>k) t ==>
        N r (λ[\<sharp>k].t)"
 Ax2 : "A r s ==> N r s"
 Ax3 : "A (´x) (´x)"
 Ax4 : "A r r' ==> N s s' ==> A (r¨s) (r'¨s')"
 Ax5 : "H r s ==> N s t ==> N r t"
 Ax6 : "SN s ==> H (((λ[x].r)•ϑ)¨s) (r•(update ϑ x s))"
 Ax7 : "H r s ==> H (r¨t) (s¨t)"
 Ax8 : "F r k ==> F (r¨´\<sharp>k) (Suc k)"
 Ax9 : "F (r¨s) k ==> F s k"
 Ax10 : "F (r¨s) k ==> F r k"
 Ax11 : "F r k ==> H r s ==> F s k"

lemma Ax6_corr:
  "∀k. F s k --> N s (f k) ==> H (((λ[x].r)•ϑ)¨s) (r•(update ϑ x s))"
  apply (rule Ax6)
  apply (auto simp add: SN_def)
  done

realizers
  Ax6: "Null" "Λ s x r ϑ f. Ax6_corr · _ · _ · _ · _ · _"
(*>*)

text {*
The proof of strong normalization is composed of the following parts:
*}

lemma One : "∀r. (SC ρ r --> SN r) ∧ (SA r --> SC ρ r)"
(*<*)
apply (induct_tac ρ)
apply simp
apply (intro impI allI)
apply (simp add:SA_def SN_def)
apply (rules intro:Ax2)
(* old manual proof: *)
(*apply (rule impI, drule mp, assumption)*)
(*apply (erule exE)+*)
(*apply (rule exI, rule Ax2, assumption)*)
(* or apply (rule_tac x="x" in exI) for an explicit instantiation *)

apply (simp (no_asm) add:SN_def)
apply (intro allI conjI impI)
apply (erule exE)
apply (subgoal_tac "SA (´\<sharp>k)") prefer 2
  apply (simp add:SA_def, rules intro:Ax3)
apply (subgoal_tac "SN (r¨´\<sharp>k)") prefer 2 
  apply (rules)
apply (simp only:SN_def)
apply (drule_tac x="Suc k" in spec)
apply (drule mp)
apply (rule Ax8, assumption)
apply (erule exE)
apply (rule exI, rule Ax1, rules, assumption)

apply (drule_tac x="r¨s" in spec)
back
apply (rule conjE,assumption)
apply (rule mp,assumption)
apply (simp (no_asm) add:SA_def)
apply (rule impI, erule exE)
apply (subgoal_tac "SN s") prefer 2 
  apply (rules)
apply (simp only:SN_def)
apply (drule_tac x="k" in spec)
apply (drule mp,rule Ax9,assumption)
apply (erule exE)
apply (simp only:SA_def)
apply (drule_tac x="k" in spec)
apply (drule mp,rule Ax10,assumption)
apply (erule exE)
apply (rule exI, rule Ax4, rules, assumption)
done
(*>*)

lemma Two : "∀r r'. SC ρ r' --> H r r' --> SC ρ r"
(*<*)
apply (induct_tac ρ)
apply (simp add:SN_def)
apply (rules intro:Ax5 intro:Ax11)
apply (rule allI)+
apply (simp (no_asm_use))
apply (rule impI allI)+
apply (rules intro:Ax7)
done

lemma spec3 [extraction_expand]: "∀x y z. P x y z ==> P x y z"
apply rules
done

lemma app_type_elim:
  "Γ \<turnstile> r ¨ s : ρ ==> ∃ σ . (Γ \<turnstile> r : (σ \<rightharpoonup> ρ)) ∧  Γ \<turnstile> s : σ"
  by (ind_cases "ρs \<turnstile> trm1 ¨ trm2 : ρ") auto

consts
  app_type_elim :: "ctxt => trm => trm => type => type"

realizers
  app_type_elim: "app_type_elim" "cheating · _"

lemma abs_type_elim:
  "Γ \<turnstile> λ[x]. t : ρ ==> ∃ σ σ' . ρ = (σ \<rightharpoonup> σ') ∧ update Γ x σ \<turnstile> t : σ'"
  apply (cases "ρ")
  apply (rule FalseE)
  apply (ind_cases "Γ \<turnstile> λ[x]. t : ρ")
  apply simp
  apply (rule_tac x=type1 in exI)
  apply (rule_tac x=type2 in exI)
  apply (ind_cases "Γ \<turnstile> λ[x]. t : ρ")
  apply simp
  done

lemma var_type_elim: "ρs \<turnstile> ´x : ρ ==> ρ = ρs x"
  by (ind_cases "ρs \<turnstile> ´x : ρ") simp
(*>*)

lemma Three : "∀ρs ϑ ρ. ρs \<turnstile> r : ρ  --> (∀z. SC (ρs z) (ϑ z)) --> SC ρ (r•ϑ)"
(*<*)
apply (induct_tac r)
apply (rename_tac x)
apply (simp add:sub_Var)
apply (rule allI impI)+
apply (drule var_type_elim)
apply simp

apply (simp add:sub_App)
apply (rule allI impI)+
apply (drule app_type_elim)
apply (erule exE conjE)+
apply (drule_tac x=ρs and y=ϑ and z="σ \<rightharpoonup> ρ" in spec3)
apply (simp)

apply (rule allI impI)+
apply (drule abs_type_elim)
apply (erule exE conjE)+
apply simp
apply (rule allI impI)+
apply (rule Two[THEN spec, THEN spec, THEN mp, THEN mp])
defer
apply (rule Ax6)
apply (rule One[THEN spec, THEN conjunct1, THEN mp], assumption)
apply (drule_tac x="update ρs name σ" and y="update ϑ name s" in spec3)
apply (drule mp, assumption, drule mp) defer apply (assumption)
apply (rule allI)
apply (cut_tac n="name" and n'="z" in name_eq_dec)
apply (erule disjE)
apply (simp add:update_def)
apply (simp add:update_def)
done
(*>*)

lemma Norm: "∀ ρs ρ r. ρs \<turnstile> r : ρ --> (∀k. F r k --> (∃s. N r s))" (*<*)
apply (rule allI impI)+
apply (subgoal_tac "SC ρ (r•subst_id)") defer
 apply (rule Three[THEN spec, THEN spec, THEN spec, THEN mp, THEN mp])
 apply (assumption)
 apply (simp add:subst_id_def)
 apply (rule allI)
 apply (rule One[THEN spec, THEN conjunct2, THEN mp])
 apply (simp add:SA_def)
 apply (rules intro:Ax3)
apply (subgoal_tac "SN r") defer
 apply (simp add:sub_id)
 apply (rule One[THEN spec, THEN conjunct1, THEN mp], assumption)
apply (simp add:SN_def, rules)
done

declare all_simps [extraction_expand]

extract Norm
(*>*)
text {*
The computationally relevant predicates @{term "SN"} and @{term "SA"} are
defined by
@{thm [display] SN_def [no_vars] SA_def [no_vars]}
The programs extracted from the above theorems have the types
\begin{center}
\begin{tabular}{ll}
@{text "One:"} & @{typeof [unique_names=false] One} \\
@{text "Two:"} & @{typeof [unique_names=false] Two} \\
@{text "Three:"} & \begin{minipage}[t]{8cm} @{typeof [unique_names=false,break,margin=60] Three} \end{minipage} \\
@{text "Norm:"} & @{typeof [unique_names=false] Norm}
\end{tabular}
\end{center}
They are defined as follows:
@{thm [display] One_def[simplified]}
@{thm [display] Two_def[simplified]}
@{thm [display] Three_def[simplified]}
@{thm [display] Norm_def}
Due to the lack of non-computational quantifiers in Isabelle, the
above programs contain typing information for the term to be
normalized, which is unnecessary for the computation.
In particular, the extracted programs use auxiliary functions
corresponding to the elimination rules
\begin{center}
\begin{tabular}{ll}
@{text "var_type_elim:"} & @{thm var_type_elim [no_vars]} \\
@{text "abs_type_elim:"} & \begin{minipage}[t]{8cm} @{thm [break,margin=60] abs_type_elim [no_vars]} \end{minipage} \\
@{text "app_type_elim:"} & @{thm app_type_elim [no_vars]} \\
\end{tabular}
\end{center}
for the typing judgement.
It turns out that all typing information can be omitted from function
@{text Three}. This may seem a bit surprising, since @{text Three} calls
function @{text Two}, which is defined by recursion on types. However,
a closer look reveals that @{text Two} is actually just a complicated
formulation of the identity function and can therefore be omitted.
Unfortunately, Isabelle's program extraction framework cannot detect
this automatically.
*}

(*<*)
end
(*>*)