src/HOL/Nominal/Examples/Crary.thy
changeset 22418 49e2d9744ae1
parent 22231 f76f187c91f9
child 22421 51a18dd1ea86
equal deleted inserted replaced
22417:014e7696ac6b 22418:49e2d9744ae1
     6 (* Types and Programming Languages, MIT Press 2005    *)
     6 (* Types and Programming Languages, MIT Press 2005    *)
     7 
     7 
     8 (* The formalisation was done by Julien Narboux and   *)
     8 (* The formalisation was done by Julien Narboux and   *)
     9 (* Christian Urban                                    *)
     9 (* Christian Urban                                    *)
    10 
    10 
       
    11 (*<*)
    11 theory Crary
    12 theory Crary
    12   imports "Nominal"
    13   imports "../Nominal"
    13 begin
    14 begin
    14 
    15 
       
    16 (* We put this def here because of some incompatibility of LatexSugar and Nominal *)
       
    17 
       
    18 syntax (Rule output)
       
    19   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
       
    20   ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
       
    21 
       
    22   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
       
    23   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
       
    24 
       
    25   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
       
    26   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
       
    27 
       
    28   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
       
    29 
       
    30 syntax (IfThen output)
       
    31   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
       
    32   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
       
    33   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
       
    34   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshapce\normalsize \,>then\<^raw:\,}>/ _.")
       
    35   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
       
    36   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
       
    37 
       
    38 syntax (IfThenNoBox output)
       
    39   "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
       
    40   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
       
    41   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
       
    42   ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
       
    43   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
       
    44   "_asm" :: "prop \<Rightarrow> asms" ("_")
       
    45 
       
    46 
       
    47 (*>*)
       
    48 
       
    49 text {* 
       
    50 \section{Definition of the language} 
       
    51 \subsection{Definition of the terms and types} 
       
    52 
       
    53 First we define the type of atom names which will be used for binders.
       
    54 Each atom type is infinitely many atoms and equality is decidable. *}
       
    55 
    15 atom_decl name 
    56 atom_decl name 
       
    57 
       
    58 text {* We define the datatype representing types. Although, It does not contain any binder we still use the \texttt{nominal\_datatype} command because the Nominal datatype package will prodive permutation functions and useful lemmas. *}
    16 
    59 
    17 nominal_datatype ty = TBase 
    60 nominal_datatype ty = TBase 
    18                     | TUnit 
    61                     | TUnit 
    19                     | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
    62                     | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
       
    63 
       
    64 text {* The datatype of terms contains a binder. The notation @{text "\<guillemotleft>name\<guillemotright> trm"} means that the name is bound inside trm. *}
    20 
    65 
    21 nominal_datatype trm = Unit
    66 nominal_datatype trm = Unit
    22                      | Var "name"
    67                      | Var "name"
    23                      | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
    68                      | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
    24                      | App "trm" "trm"
    69                      | App "trm" "trm"
    25                      | Const "nat"
    70                      | Const "nat"
    26 
    71 
    27 (* The next 3 lemmas should be in the nominal library *)
    72 text {* As the datatype of types does not contain any binder, the application of a permutation is the identity function. In the future, this will be automatically derived by the package. *}
    28 lemma eq_eqvt:
       
    29   fixes pi::"name prm"
       
    30   and   x::"'a::pt_name"
       
    31   shows "pi\<bullet>(x=y) = (pi\<bullet>x=pi\<bullet>y)"
       
    32   apply(simp add: perm_bool perm_bij)
       
    33   done
       
    34 
       
    35 lemma in_eqvt:
       
    36   fixes pi::"name prm"
       
    37   and   x::"'a::pt_name"
       
    38   assumes "x\<in>X"
       
    39   shows "pi\<bullet>x \<in> pi\<bullet>X"
       
    40   using assms by (perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst])
       
    41 
       
    42 lemma set_eqvt:
       
    43   fixes pi::"name prm"
       
    44   and   xs::"('a::pt_name) list"
       
    45   shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
       
    46   by (perm_simp add: pt_list_set_pi[OF pt_name_inst])
       
    47 (* end of library *)
       
    48 
    73 
    49 lemma perm_ty[simp]: 
    74 lemma perm_ty[simp]: 
    50   fixes T::"ty"
    75   fixes T::"ty"
    51   and   pi::"name prm"
    76   and   pi::"name prm"
    52   shows "pi\<bullet>T = T"
    77   shows "pi\<bullet>T = T"
    58   shows "x\<sharp>T"
    83   shows "x\<sharp>T"
    59   by (simp add: fresh_def supp_def)
    84   by (simp add: fresh_def supp_def)
    60 
    85 
    61 lemma ty_cases:
    86 lemma ty_cases:
    62   fixes T::ty
    87   fixes T::ty
    63   shows "(\<exists> T1 T2. T=T1\<rightarrow>T2) \<or> T=TUnit \<or> T=TBase"
    88   shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
    64 by (induct T rule:ty.induct_weak) (auto)
    89 by (induct T rule:ty.induct_weak) (auto)
    65 
    90 
    66 text {* Size Functions *} 
    91 text {* 
       
    92 \subsection{Size functions}
       
    93 
       
    94 We define size functions for types and terms. As Isabelle allows overloading we can use the same notation for both functions.
       
    95 
       
    96 These function are automatically generated for non nominal datatypes. In the future, we need to extend the package to generate size function for nominal datatypes as well.
       
    97  *} 
    67 
    98 
    68 instance ty :: size ..
    99 instance ty :: size ..
    69 
   100 
    70 nominal_primrec
   101 nominal_primrec
    71   "size (TBase) = 1"
   102   "size (TBase) = 1"
    72   "size (TUnit) = 1"
   103   "size (TUnit) = 1"
    73   "size (T1\<rightarrow>T2) = size T1 + size T2"
   104   "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
    74 by (rule TrueI)+
   105 by (rule TrueI)+
    75 
   106 
    76 instance trm :: size ..
   107 instance trm :: size ..
    77 
   108 
    78 nominal_primrec 
   109 nominal_primrec 
    79   "size (Unit) = 1"
   110   "size (Unit) = 1"
    80   "size (Var x) = 1"
   111   "size (Var x) = 1"
    81   "size (Lam [x].t) = size t + 1"
   112   "size (Lam [x].t) = size t + 1"
    82   "size (App t1 t2) = size t1 + size t2"
   113   "size (App t1 t2) = size t1 + size t2"
    83   "size (Const n) = 1"
   114   "size (Const n) = 1"
    84 apply(finite_guess add: fs_name1 perm_nat_def)+
   115 apply(finite_guess)+
    85 apply(perm_full_simp add: perm_nat_def)
       
    86 apply(simp add: fs_name1)
       
    87 apply(rule TrueI)+
   116 apply(rule TrueI)+
    88 apply(simp add: fresh_nat)+
   117 apply(simp add: fresh_nat)+
    89 apply(fresh_guess add: fs_name1 perm_nat_def)+
   118 apply(fresh_guess)+
    90 done
   119 done
    91 
   120 
    92 lemma ty_size_greater_zero[simp]:
   121 lemma ty_size_greater_zero[simp]:
    93   fixes T::"ty"
   122   fixes T::"ty"
    94   shows "size T > 0"
   123   shows "size T > 0"
    95 by (nominal_induct rule:ty.induct) (simp_all)
   124 by (nominal_induct rule:ty.induct) (simp_all)
    96 
   125 
    97 text {* valid contexts *}
   126 text {* 
    98 
   127 \subsection{Typing}
       
   128 
       
   129 \subsubsection{Typing contexts}
       
   130 
       
   131 This section contains the definition and some properties of a typing context. As the concept of context often appears in the litterature and is general, we should in the future provide these lemmas in a library.
       
   132 
       
   133 \paragraph{Definition of the Validity of contexts}\strut\\
       
   134 
       
   135 First we define what valid contexts are. Informally a context is valid is it does not contains twice the same variable.
       
   136 
       
   137 We use the following two inference rules: *}
       
   138 
       
   139 (*<*)
    99 inductive2
   140 inductive2
   100   valid :: "(name \<times> 'a::pt_name) list \<Rightarrow> bool"
   141   valid :: "(name \<times> 'a::pt_name) list \<Rightarrow> bool"
   101 where
   142 where
   102     v_nil[intro]:  "valid []"
   143     v_nil[intro]:  "valid []"
   103   | v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
   144   | v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
   104 
   145 (*>*)
   105 lemma valid_eqvt[eqvt]:
   146 
   106   fixes   pi:: "name prm"
   147 text {*
   107   assumes a: "valid \<Gamma>"
   148 \begin{center}
   108   shows "valid (pi\<bullet>\<Gamma>)"
   149 \isastyle
   109   using a
   150 @{thm[mode=Rule] v_nil[no_vars]}{\sc{v\_nil}}
   110   by (induct) (auto simp add: fresh_bij)
   151 \qquad
       
   152 @{thm[mode=Rule] v_cons[no_vars]}{\sc{v\_cons}}
       
   153 \end{center}
       
   154 *} 
       
   155 
       
   156 text{* We generate the equivariance lemma for the relation \texttt{valid}. *}
       
   157 
       
   158 nominal_inductive valid
       
   159 
       
   160 text{* We obtain a lemma called \texttt{valid\_eqvt}:
       
   161 \begin{center} 
       
   162 @{thm[mode=IfThen] valid_eqvt}
       
   163 \end{center}
       
   164 *}
       
   165 
       
   166 
       
   167 text{* We generate the inversion lemma for non empty lists. We add the \texttt{elim} attribute to tell the automated tactics to use it.
       
   168  *}
   111 
   169 
   112 inductive_cases2  
   170 inductive_cases2  
   113   valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
   171   valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
   114 
   172 
   115 text {* typing judgements for terms *}
   173 text{*
       
   174 The generated theorem is the following:
       
   175 \begin{center}
       
   176 @{thm "valid_cons_elim_auto"[no_vars] }
       
   177 \end{center}
       
   178 *}
       
   179 
       
   180 text{* \paragraph{Lemmas about valid contexts} 
       
   181  Now, we can prove two useful lemmas about valid contexts. 
       
   182 *}
       
   183 
       
   184 lemma fresh_context: 
       
   185   fixes  \<Gamma> :: "(name\<times>ty) list"
       
   186   and    a :: "name"
       
   187   assumes "a\<sharp>\<Gamma>"
       
   188   shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
       
   189 using assms by (induct \<Gamma>, auto simp add: fresh_prod fresh_list_cons fresh_atm)
       
   190 
       
   191 lemma type_unicity_in_context:
       
   192   fixes  \<Gamma> :: "(name\<times>ty)list"
       
   193   and    pi:: "name prm"
       
   194   and    a :: "name"
       
   195   and    \<tau> :: "ty"
       
   196   assumes "valid \<Gamma>" and "(x,T\<^isub>1) \<in> set \<Gamma>" and "(x,T\<^isub>2) \<in> set \<Gamma>"
       
   197   shows "T\<^isub>1=T\<^isub>2"
       
   198 using assms by (induct \<Gamma>, auto dest!: fresh_context)
       
   199 
       
   200 text {* \paragraph{Definition of sub-contexts}
       
   201 
       
   202 The definition of sub context is standard. We do not use the subset definition to prevent the need for unfolding the definition. We include validity in the definition to shorten the statements.
       
   203  *}
       
   204 
       
   205 
       
   206 abbreviation
       
   207   "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [55,55] 55)
       
   208 where
       
   209   "\<Gamma>\<^isub>1 \<lless> \<Gamma>\<^isub>2 \<equiv> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>\<^isub>2) \<and> valid \<Gamma>\<^isub>2"
       
   210 
       
   211 text {* 
       
   212 \subsubsection{Definition of the typing relation}
       
   213 
       
   214 Now, we can define the typing judgements for terms. The rules are given in figure~\ref{typing}. *}
       
   215 
       
   216 (*<*)
   116 
   217 
   117 inductive2
   218 inductive2
   118   typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
   219   typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
   119 where
   220 where
   120   t_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
   221   t_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
   121 | t_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> e1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> e2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : T2"
   222 | t_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2"
   122 | t_Lam[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
   223 | t_Lam[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
   123 | t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
   224 | t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
   124 | t_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
   225 | t_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
       
   226 (*>*)
       
   227 
       
   228 text {* 
       
   229 \begin{figure}
       
   230 \begin{center}
       
   231 \isastyle %smaller fonts
       
   232 @{thm[mode=Rule] t_Var[no_vars]}{\sc{t\_Var}}\qquad
       
   233 @{thm[mode=Rule] t_App[no_vars]}{\sc{t\_App}}\\
       
   234 @{thm[mode=Rule] t_Lam[no_vars]}{\sc{t\_Lam}}\\
       
   235 @{thm[mode=Rule] t_Const[no_vars]}{\sc{t\_Const}} \qquad
       
   236 @{thm[mode=Rule] t_Unit[no_vars]}{\sc{t\_Unit}}
       
   237 \end{center}
       
   238 \caption{Typing rules\label{typing}}
       
   239 \end{figure}
       
   240 *}
   125 
   241 
   126 lemma typing_valid:
   242 lemma typing_valid:
   127   assumes "\<Gamma> \<turnstile> t : T"
   243   assumes "\<Gamma> \<turnstile> t : T"
   128   shows "valid \<Gamma>"
   244   shows "valid \<Gamma>"
   129   using assms
   245   using assms by (induct)(auto)
   130   by (induct) (auto)
   246 
   131  
   247 nominal_inductive typing
   132 lemma typing_eqvt[eqvt]:
   248 
   133   fixes pi::"name prm"
   249 text {* 
   134   assumes "\<Gamma> \<turnstile> t : T"
   250 \subsubsection{Inversion lemmas for the typing relation}
   135   shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : (pi\<bullet>T)"
   251 
   136   using assms
   252 We generate some inversion lemmas for 
   137   apply(induct)
   253 the typing judgment and add them as elimination rules for the automatic tactics.
   138   apply(auto simp add: fresh_bij set_eqvt valid_eqvt) 
   254 During the generation of these lemmas, we need the injectivity properties of the constructor of the nominal datatypes. These are not added by default in the set of simplification rules to prevent unwanted simplifications in the rest of the development. In the future, the \texttt{inductive\_cases} will be reworked to allow to use its own set of rules instead of the whole 'simpset'.
   139   apply(rule t_Var)
   255 *}
   140   apply(drule valid_eqvt)
       
   141   apply(assumption)
       
   142   apply(drule in_eqvt)
       
   143   apply(simp add: set_eqvt)
       
   144   done
       
   145 
       
   146 text {* Inversion lemmas for the typing judgment *}
       
   147 
   256 
   148 declare trm.inject [simp add]
   257 declare trm.inject [simp add]
   149 declare ty.inject  [simp add]
   258 declare ty.inject  [simp add]
   150 
   259 
   151 inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
   260 inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
   154 inductive_cases2  t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
   263 inductive_cases2  t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
   155 inductive_cases2  t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
   264 inductive_cases2  t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
   156 
   265 
   157 declare trm.inject [simp del]
   266 declare trm.inject [simp del]
   158 declare ty.inject [simp del]
   267 declare ty.inject [simp del]
       
   268 
       
   269 text {* 
       
   270 \subsubsection{Strong induction principle}
       
   271 
       
   272 Now, we define a strong induction principle. This induction principle allow us to avoid some terms during the induction. The bound variable The avoided terms ($c$)  *}
   159 
   273 
   160 lemma typing_induct_strong
   274 lemma typing_induct_strong
   161   [consumes 1, case_names t_Var t_App t_Lam t_Const t_Unit]:
   275   [consumes 1, case_names t_Var t_App t_Lam t_Const t_Unit]:
   162     fixes  P::"'a::fs_name \<Rightarrow> (name\<times>ty) list \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow>bool"
   276     fixes  P::"'a::fs_name \<Rightarrow> (name\<times>ty) list \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow>bool"
   163     and    x :: "'a::fs_name"
   277     and    x :: "'a::fs_name"
   164     assumes a: "\<Gamma> \<turnstile> e : T"
   278     assumes a: "\<Gamma> \<turnstile> e : T"
   165     and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
   279     and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
   166     and a2: "\<And>\<Gamma> e1 T1 T2 e2 c. \<lbrakk>\<And>c. P c \<Gamma> e1 (T1\<rightarrow>T2); \<And>c. P c \<Gamma> e2 T1\<rbrakk> 
   280     and a2: "\<And>\<Gamma> e\<^isub>1 T\<^isub>1 T\<^isub>2 e\<^isub>2 c. \<lbrakk>\<And>c. P c \<Gamma> e\<^isub>1 (T\<^isub>1\<rightarrow>T\<^isub>2); \<And>c. P c \<Gamma> e\<^isub>2 T\<^isub>1\<rbrakk> 
   167              \<Longrightarrow> P c \<Gamma> (App e1 e2) T2"
   281              \<Longrightarrow> P c \<Gamma> (App e\<^isub>1 e\<^isub>2) T\<^isub>2"
   168     and a3: "\<And>x \<Gamma> T1 t T2 c.\<lbrakk>x\<sharp>(\<Gamma>,c); \<And>c. P c ((x,T1)#\<Gamma>) t T2\<rbrakk>
   282     and a3: "\<And>x \<Gamma> T\<^isub>1 t T\<^isub>2 c.\<lbrakk>x\<sharp>(\<Gamma>,c); \<And>c. P c ((x,T\<^isub>1)#\<Gamma>) t T\<^isub>2\<rbrakk>
   169              \<Longrightarrow> P c \<Gamma> (Lam [x].t) (T1\<rightarrow>T2)"
   283              \<Longrightarrow> P c \<Gamma> (Lam [x].t) (T\<^isub>1\<rightarrow>T\<^isub>2)"
   170     and a4: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> (Const n) TBase"
   284     and a4: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> (Const n) TBase"
   171     and a5: "\<And>\<Gamma> c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> Unit TUnit"
   285     and a5: "\<And>\<Gamma> c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> Unit TUnit"
   172     shows "P c \<Gamma> e T"
   286     shows "P c \<Gamma> e T"
   173 proof -
   287 proof -
   174   from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) (pi\<bullet>T)"
   288   from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) (pi\<bullet>T)"
   177     have "valid \<Gamma>" by fact
   291     have "valid \<Gamma>" by fact
   178     then have "valid (pi\<bullet>\<Gamma>)" by (simp only: eqvt)
   292     then have "valid (pi\<bullet>\<Gamma>)" by (simp only: eqvt)
   179     moreover
   293     moreover
   180     have "(x,T)\<in>set \<Gamma>" by fact
   294     have "(x,T)\<in>set \<Gamma>" by fact
   181     then have "pi\<bullet>(x,T)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])  
   295     then have "pi\<bullet>(x,T)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])  
   182     then have "(pi\<bullet>x,T)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: set_eqvt)
   296     then have "(pi\<bullet>x,T)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: eqvt)
   183     ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) (pi\<bullet>T)" using a1 by simp
   297     ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) (pi\<bullet>T)" using a1 by simp
   184   next
   298   next
   185     case (t_App \<Gamma> e1 T1 T2 e2 pi c)
   299     case (t_App \<Gamma> e\<^isub>1 T\<^isub>1 T\<^isub>2 e\<^isub>2 pi c)
   186     thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e1 e2)) (pi\<bullet>T2)" using a2 
   300     thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e\<^isub>1 e\<^isub>2)) (pi\<bullet>T\<^isub>2)" using a2 
   187       by (simp only: eqvt) (blast)
   301       by (simp only: eqvt) (blast)
   188   next
   302   next
   189     case (t_Lam x \<Gamma> T1 t T2 pi c)
   303     case (t_Lam x \<Gamma> T\<^isub>1 t T\<^isub>2 pi c)
   190     obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>\<Gamma>,pi\<bullet>t,c)" by (erule exists_fresh[OF fs_name1])
   304     obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>\<Gamma>,pi\<bullet>t,c)" by (erule exists_fresh[OF fs_name1])
   191     let ?sw = "[(pi\<bullet>x,y)]"
   305     let ?sw = "[(pi\<bullet>x,y)]"
   192     let ?pi' = "?sw@pi"
   306     let ?pi' = "?sw@pi"
   193     have f0: "x\<sharp>\<Gamma>" by fact
   307     have f0: "x\<sharp>\<Gamma>" by fact
   194     have f1: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f0 by (simp add: fresh_bij)
   308     have f1: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f0 by (simp add: fresh_bij)
   195     have f2: "y\<sharp>?pi'\<bullet>\<Gamma>" by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
   309     have f2: "y\<sharp>?pi'\<bullet>\<Gamma>" by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
   196       have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>T2)" by fact
   310       have ih1: "\<And>c. P c (?pi'\<bullet>((x,T\<^isub>1)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>T\<^isub>2)" by fact
   197     then have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T1\<rightarrow>T2)" using fs f2 a3
   311     then have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T\<^isub>1\<rightarrow>T\<^isub>2)" using fs f2 a3
   198       by (simp add: calc_atm)
   312       by (simp add: calc_atm)
   199     then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) (T1\<rightarrow>T2)" 
   313     then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) (T\<^isub>1\<rightarrow>T\<^isub>2)" 
   200       by (simp del: append_Cons add: calc_atm pt_name2)
   314       by (simp del: append_Cons add: calc_atm pt_name2)
   201     moreover have "(?sw\<bullet>pi\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)"
   315     moreover have "(?sw\<bullet>pi\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)"
   202       by (rule perm_fresh_fresh) (simp_all add: fs f1)
   316       by (rule perm_fresh_fresh) (simp_all add: fs f1)
   203     moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) = Lam [(pi\<bullet>x)].(pi\<bullet>t)"
   317     moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) = Lam [(pi\<bullet>x)].(pi\<bullet>t)"
   204       by (rule perm_fresh_fresh) (simp_all add: fs f1 fresh_atm abs_fresh)
   318       by (rule perm_fresh_fresh) (simp_all add: fs f1 fresh_atm abs_fresh)
   205     ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (pi\<bullet>T1\<rightarrow>T2)" by simp
   319     ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (pi\<bullet>T\<^isub>1\<rightarrow>T\<^isub>2)" by simp
   206   next
   320   next
   207     case (t_Const \<Gamma> n pi c)
   321     case (t_Const \<Gamma> n pi c)
   208     thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (pi\<bullet>TBase)" using a4 by (simp, blast intro: valid_eqvt)
   322     thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (pi\<bullet>TBase)" using a4 by (simp, blast intro: valid_eqvt)
   209   next
   323   next
   210     case (t_Unit \<Gamma> pi c)
   324     case (t_Unit \<Gamma> pi c)
   212   qed 
   326   qed 
   213   then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) (([]::name prm)\<bullet>T)" by blast
   327   then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) (([]::name prm)\<bullet>T)" by blast
   214   then show "P c \<Gamma> e T" by simp
   328   then show "P c \<Gamma> e T" by simp
   215 qed
   329 qed
   216 
   330 
   217 text {* capture-avoiding substitution *}
   331 text {* 
       
   332 \subsection{Capture-avoiding substitutions}
       
   333 
       
   334 In this section we define parallel substitution. The usual substitution will be derived as a special case of parallel substitution. But first we define a function to lookup for the term corresponding to a type in an association list. Note that if the term does not appear in the list then we return a variable of that name.\\
       
   335 Should we return Some or None and put that in a library ?
       
   336  *}
       
   337 
   218 
   338 
   219 fun
   339 fun
   220   lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm"   
   340   lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm"   
   221 where
   341 where
   222   "lookup [] X        = Var X"
   342   "lookup [] X        = Var X"
   223   "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
   343   "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
   224 
   344 
   225 lemma lookup_eqvt:
   345 lemma lookup_eqvt[eqvt]:
   226   fixes pi::"name prm"
   346   fixes pi::"name prm"
   227   and   \<theta>::"(name\<times>trm) list"
   347   and   \<theta>::"(name\<times>trm) list"
   228   and   X::"name"
   348   and   X::"name"
   229   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
   349   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
   230 by (induct \<theta>)
   350 by (induct \<theta>) (auto simp add: perm_bij)
   231    (auto simp add: perm_bij)
       
   232 
   351 
   233 lemma lookup_fresh:
   352 lemma lookup_fresh:
   234   fixes z::"name"
   353   fixes z::"name"
   235   assumes "z\<sharp>\<theta>" "z\<sharp>x"
   354   assumes "z\<sharp>\<theta>" "z\<sharp>x"
   236   shows "z \<sharp>lookup \<theta> x"
   355   shows "z\<sharp> lookup \<theta> x"
   237 using assms 
   356 using assms 
   238 by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)
   357 by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)
   239 
   358 
   240 lemma lookup_fresh':
   359 lemma lookup_fresh':
   241   assumes "z\<sharp>\<theta>"
   360   assumes "z\<sharp>\<theta>"
   242   shows "lookup \<theta> z = Var z"
   361   shows "lookup \<theta> z = Var z"
   243 using assms 
   362 using assms 
   244 by (induct rule: lookup.induct)
   363 by (induct rule: lookup.induct)
   245    (auto simp add: fresh_list_cons fresh_prod fresh_atm)
   364    (auto simp add: fresh_list_cons fresh_prod fresh_atm)
   246 
   365 
       
   366 text {* \subsubsection{Parallel substitution} *}
       
   367 
   247 consts
   368 consts
   248   psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [60,100] 100)
   369   psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [60,100] 100)
   249  
   370  
   250 nominal_primrec
   371 nominal_primrec
   251   "\<theta><(Var x)> = (lookup \<theta> x)"
   372   "\<theta><(Var x)> = (lookup \<theta> x)"
   252   "\<theta><(App t1 t2)> = App (\<theta><t1>) (\<theta><t2>)"
   373   "\<theta><(App t\<^isub>1 t\<^isub>2)> = App (\<theta><t\<^isub>1>) (\<theta><t\<^isub>2>)"
   253   "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
   374   "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
   254   "\<theta><(Const n)> = Const n"
   375   "\<theta><(Const n)> = Const n"
   255   "\<theta><(Unit)> = Unit"
   376   "\<theta><(Unit)> = Unit"
   256 apply(finite_guess add: fs_name1 lookup_eqvt)+
   377 apply(finite_guess)+
   257 apply(perm_full_simp)
       
   258 apply(simp add: fs_name1)
       
   259 apply(rule TrueI)+
   378 apply(rule TrueI)+
   260 apply(simp add: abs_fresh)+
   379 apply(simp add: abs_fresh)+
   261 apply(fresh_guess add: fs_name1 lookup_eqvt)+
   380 apply(fresh_guess)+
   262 done
   381 done
       
   382 
       
   383 
       
   384 text {* \subsubsection{Substitution} 
       
   385 
       
   386 The substitution function is defined just as a special case of parallel substitution. 
       
   387 
       
   388 *}
   263 
   389 
   264 abbreviation 
   390 abbreviation 
   265  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
   391  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
   266 where
   392 where
   267   "t[x::=t']  \<equiv> ([(x,t')])<t>" 
   393   "t[x::=t']  \<equiv> ([(x,t')])<t>" 
   268 
   394 
   269 lemma subst[simp]:
   395 lemma subst[simp]:
   270   shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
   396   shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
   271   and   "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
   397   and   "(App t\<^isub>1 t\<^isub>2)[y::=t'] = App (t\<^isub>1[y::=t']) (t\<^isub>2[y::=t'])"
   272   and   "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
   398   and   "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
   273   and   "Const n[y::=t'] = Const n"
   399   and   "Const n[y::=t'] = Const n"
   274   and   "Unit [y::=t'] = Unit"
   400   and   "Unit [y::=t'] = Unit"
   275   by (simp_all add: fresh_list_cons fresh_list_nil)
   401   by (simp_all add: fresh_list_cons fresh_list_nil)
   276 
   402 
   279   and   t::"trm"
   405   and   t::"trm"
   280   shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
   406   shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
   281   by (nominal_induct t avoiding: x t' rule: trm.induct)
   407   by (nominal_induct t avoiding: x t' rule: trm.induct)
   282      (perm_simp add: fresh_bij)+
   408      (perm_simp add: fresh_bij)+
   283 
   409 
       
   410 text {* \subsubsection{Lemmas about freshness and substitutions} *}
       
   411 
   284 lemma subst_rename: 
   412 lemma subst_rename: 
   285   fixes c::"name"
   413   fixes c::"name"
   286   and   t1::"trm"
   414   and   t1::"trm"
   287   assumes a: "c\<sharp>t1"
   415   assumes a: "c\<sharp>t\<^isub>1"
   288   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
   416   shows "t\<^isub>1[a::=t\<^isub>2] = ([(c,a)]\<bullet>t\<^isub>1)[c::=t\<^isub>2]"
   289   using a
   417   using a
   290   apply(nominal_induct t1 avoiding: a c t2 rule: trm.induct)
   418   apply(nominal_induct t\<^isub>1 avoiding: a c t\<^isub>2 rule: trm.induct)
   291   apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+
   419   apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+
   292   done
   420   done
   293 
   421 
   294 lemma fresh_psubst: 
   422 lemma fresh_psubst: 
   295   fixes z::"name"
   423   fixes z::"name"
   302 
   430 
   303 lemma fresh_subst'':
   431 lemma fresh_subst'':
   304   fixes z::"name"
   432   fixes z::"name"
   305   and   t1::"trm"
   433   and   t1::"trm"
   306   and   t2::"trm"
   434   and   t2::"trm"
   307   assumes "z\<sharp>t2"
   435   assumes "z\<sharp>t\<^isub>2"
   308   shows "z\<sharp>t1[z::=t2]"
   436   shows "z\<sharp>t\<^isub>1[z::=t\<^isub>2]"
   309 using assms 
   437 using assms 
   310 by (nominal_induct t1 avoiding: t2 z rule: trm.induct)
   438 by (nominal_induct t\<^isub>1 avoiding: t\<^isub>2 z rule: trm.induct)
   311    (auto simp add: abs_fresh fresh_nat fresh_atm)
   439    (auto simp add: abs_fresh fresh_nat fresh_atm)
   312 
   440 
   313 lemma fresh_subst':
   441 lemma fresh_subst':
   314   fixes z::"name"
   442   fixes z::"name"
   315   and   t1::"trm"
   443   and   t1::"trm"
   316   and   t2::"trm"
   444   and   t2::"trm"
   317   assumes "z\<sharp>[y].t1" "z\<sharp>t2"
   445   assumes "z\<sharp>[y].t\<^isub>1" "z\<sharp>t\<^isub>2"
   318   shows "z\<sharp>t1[y::=t2]"
   446   shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
   319 using assms 
   447 using assms 
   320 by (nominal_induct t1 avoiding: y t2 z rule: trm.induct)
   448 by (nominal_induct t\<^isub>1 avoiding: y t\<^isub>2 z rule: trm.induct)
   321    (auto simp add: abs_fresh fresh_nat fresh_atm)
   449    (auto simp add: abs_fresh fresh_nat fresh_atm)
   322 
   450 
   323 lemma fresh_subst:
   451 lemma fresh_subst:
   324   fixes z::"name"
   452   fixes z::"name"
   325   and   t1::"trm"
   453   and   t1::"trm"
   326   and   t2::"trm"
   454   and   t2::"trm"
   327   assumes "z\<sharp>t1" "z\<sharp>t2"
   455   assumes "z\<sharp>t\<^isub>1" "z\<sharp>t\<^isub>2"
   328   shows "z\<sharp>t1[y::=t2]"
   456   shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
   329 using assms fresh_subst'
   457 using assms fresh_subst'
   330 by (auto simp add: abs_fresh) 
   458 by (auto simp add: abs_fresh) 
   331 
   459 
   332 lemma fresh_psubst_simpl:
   460 lemma fresh_psubst_simpl:
   333   assumes "x\<sharp>t"
   461   assumes "x\<sharp>t"
   344     by (simp add: fresh_list_cons fresh_prod)
   472     by (simp add: fresh_list_cons fresh_prod)
   345   moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp
   473   moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp
   346   ultimately show "(x,u)#\<theta><Lam [y].t> = \<theta><Lam [y].t>" by auto
   474   ultimately show "(x,u)#\<theta><Lam [y].t> = \<theta><Lam [y].t>" by auto
   347 qed (auto simp add: fresh_atm abs_fresh)
   475 qed (auto simp add: fresh_atm abs_fresh)
   348 
   476 
   349 text {* Equivalence (defined) *}
       
   350 
       
   351 inductive2
       
   352   equiv_def :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ == _ : _" [60,60] 60) 
       
   353 where
       
   354   Q_Refl[intro]:  "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t == t : T"
       
   355 | Q_Symm[intro]:  "\<Gamma> \<turnstile> t == s : T \<Longrightarrow> \<Gamma> \<turnstile> s == t : T"
       
   356 | Q_Trans[intro]: "\<lbrakk>\<Gamma> \<turnstile> s == t : T; \<Gamma> \<turnstile> t == u : T\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> s == u : T"
       
   357 | Q_Abs[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s2 ==  Lam [x]. t2 : T1 \<rightarrow> T2"
       
   358 | Q_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> s1 == t1 : T1 \<rightarrow> T2 ; \<Gamma> \<turnstile> s2 == t2 : T1\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> App s1 s2 == App t1 t2 : T2"
       
   359 | Q_Beta[intro]:  "\<lbrakk>x\<sharp>(\<Gamma>,s2,t2); (x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2 ; \<Gamma> \<turnstile> s2 == t2 : T1\<rbrakk> 
       
   360                    \<Longrightarrow>  \<Gamma> \<turnstile> App (Lam [x]. s12) s2 ==  t12[x::=t2] : T2"
       
   361 | Q_Ext[intro]:   "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T1)#\<Gamma> \<turnstile> App s (Var x) == App t (Var x) : T2\<rbrakk> 
       
   362                    \<Longrightarrow> \<Gamma> \<turnstile> s == t : T1 \<rightarrow> T2"
       
   363 
       
   364 lemma equiv_def_valid:
       
   365   assumes "\<Gamma> \<turnstile> t == s : T"
       
   366   shows "valid \<Gamma>"
       
   367 using assms by (induct,auto elim:typing_valid)
       
   368 
       
   369 lemma equiv_def_eqvt[eqvt]:
       
   370   fixes pi::"name prm"
       
   371   assumes a: "\<Gamma> \<turnstile> s == t : T"
       
   372   shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) == (pi\<bullet>t) : (pi\<bullet>T)"
       
   373 using a
       
   374 apply(induct)
       
   375 apply(auto intro: typing_eqvt valid_eqvt simp add: fresh_bij subst_eqvt simp del: perm_ty)
       
   376 apply(rule_tac x="pi\<bullet>x" in Q_Ext)
       
   377 apply(simp add: fresh_bij)+
       
   378 done
       
   379 
       
   380 lemma equiv_def_strong_induct
       
   381   [consumes 1, case_names Q_Refl Q_Symm Q_Trans Q_Abs Q_App Q_Beta Q_Ext]:
       
   382   fixes c::"'a::fs_name"
       
   383   assumes a0: "\<Gamma> \<turnstile> s == t : T" 
       
   384   and     a1: "\<And>\<Gamma> t T c.  \<Gamma> \<turnstile> t : T  \<Longrightarrow> P c \<Gamma> t t T"
       
   385   and     a2: "\<And>\<Gamma> t s T c. \<lbrakk>\<And>d. P d \<Gamma> t s T\<rbrakk> \<Longrightarrow>  P c \<Gamma> s t T"
       
   386   and     a3: "\<And>\<Gamma> s t T u c. \<lbrakk>\<And>d. P d \<Gamma> s t T; \<And>d. P d \<Gamma> t u T\<rbrakk> 
       
   387                \<Longrightarrow> P c \<Gamma> s u T"
       
   388   and     a4: "\<And>x \<Gamma> T1 s2 t2 T2 c. \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>c; \<And>d. P d ((x,T1)#\<Gamma>) s2 t2 T2\<rbrakk>
       
   389                \<Longrightarrow> P c \<Gamma> (Lam [x].s2) (Lam [x].t2) (T1\<rightarrow>T2)"
       
   390   and     a5: "\<And>\<Gamma> s1 t1 T1 T2 s2 t2 c. \<lbrakk>\<And>d. P d \<Gamma> s1 t1 (T1\<rightarrow>T2); \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> 
       
   391                \<Longrightarrow> P c \<Gamma> (App s1 s2) (App t1 t2) T2"
       
   392   and     a6: "\<And>x \<Gamma> T1 s12 t12 T2 s2 t2 c.
       
   393                \<lbrakk>x\<sharp>(\<Gamma>,s2,t2); x\<sharp>c; \<And>d. P d ((x,T1)#\<Gamma>) s12 t12 T2; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> 
       
   394                \<Longrightarrow> P c \<Gamma> (App (Lam [x].s12) s2) (t12[x::=t2]) T2"
       
   395   and     a7: "\<And>x \<Gamma> s t T1 T2 c.
       
   396                \<lbrakk>x\<sharp>(\<Gamma>,s,t); \<And>d. P d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk>
       
   397                \<Longrightarrow> P c \<Gamma> s t (T1\<rightarrow>T2)"
       
   398  shows "P c \<Gamma>  s t T"
       
   399 proof -
       
   400   from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" 
       
   401     proof(induct)
       
   402       case (Q_Refl \<Gamma> t T pi c)
       
   403       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) (pi\<bullet>T)" using a1 by (simp only: eqvt)
       
   404     next
       
   405       case (Q_Symm \<Gamma> t s T pi c)
       
   406       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" using a2 by (simp only: equiv_def_eqvt)
       
   407     next
       
   408       case (Q_Trans \<Gamma> s t T u pi c)
       
   409       then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) (pi\<bullet>T)" using a3 by (blast intro: equiv_def_eqvt)
       
   410     next
       
   411       case (Q_App \<Gamma> s1 t1 T1 T2 s2 t2 pi c)
       
   412       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s1 s2) (pi\<bullet>App t1 t2) (pi\<bullet>T2)" using a5 
       
   413 	by (simp only: eqvt) (blast)
       
   414     next
       
   415       case (Q_Ext x \<Gamma> s t T1 T2 pi c)
       
   416       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T1\<rightarrow>T2)"  
       
   417 	by (auto intro!: a7 simp add: fresh_bij)
       
   418     next
       
   419       case (Q_Abs x \<Gamma> T1 s2 t2 T2 pi c)
       
   420       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1])
       
   421       let ?sw="[(pi\<bullet>x,y)]"
       
   422       let ?pi'="?sw@pi"
       
   423       have f1: "x\<sharp>\<Gamma>" by fact
       
   424       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij)
       
   425       have f3: "y\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
       
   426       have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) (?pi'\<bullet>T2)" by fact
       
   427       then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T2" by (simp add: calc_atm)
       
   428       then have "P c  (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>Lam [x].s2) (?pi'\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" using a4 f3 fs
       
   429 	by (simp add: calc_atm)
       
   430       then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" 
       
   431 	by (simp del: append_Cons add: calc_atm pt_name2)
       
   432       moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
       
   433 	by (rule perm_fresh_fresh) (simp_all add: fs f2)
       
   434       moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>s2))) = Lam [(pi\<bullet>x)].(pi\<bullet>s2)" 
       
   435 	by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh)
       
   436       moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t2))) = Lam [(pi\<bullet>x)].(pi\<bullet>t2)" 
       
   437 	by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh)
       
   438       ultimately have "P c (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" by simp
       
   439       then show  "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Lam [x].s2) (pi\<bullet>Lam [x].t2) (pi\<bullet>T1\<rightarrow>T2)" by simp 
       
   440     next 
       
   441       case (Q_Beta x \<Gamma> s2 t2 T1 s12 t12 T2 pi c) 
       
   442       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s12,pi\<bullet>t12,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" 
       
   443 	by (rule exists_fresh[OF fs_name1])
       
   444       let ?sw="[(pi\<bullet>x,y)]"
       
   445       let ?pi'="?sw@pi"
       
   446       have f1: "x\<sharp>(\<Gamma>,s2,t2)" by fact 
       
   447       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s2,t2))" using f1 by (simp add: fresh_bij)
       
   448       have f3: "y\<sharp>(?pi'\<bullet>(\<Gamma>,s2,t2))" using f1 
       
   449 	by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp fresh_prod)
       
   450       have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T2)" by fact
       
   451       then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T2)" by (simp add: calc_atm)
       
   452       moreover
       
   453       have ih2: "\<And>c. P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s2) (?pi'\<bullet>t2) (?pi'\<bullet>T1)" by fact
       
   454       ultimately have "P c  (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(App (Lam [x].s12) s2)) (?pi'\<bullet>(t12[x::=t2])) (?pi'\<bullet>T2)" 
       
   455 	using a6 f3 fs by (force simp add: subst_eqvt calc_atm del: perm_ty)
       
   456       then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2))) 
       
   457 	(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])) T2" 
       
   458 	by (simp del: append_Cons add: calc_atm pt_name2 subst_eqvt)
       
   459       moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
       
   460 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified])
       
   461       moreover have "(?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2))) = App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)" 
       
   462 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified] abs_fresh)
       
   463       moreover have "(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])) = ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])" 
       
   464 	by (rule perm_fresh_fresh) 
       
   465 	   (simp_all add: fs[simplified] f2[simplified] fresh_subst fresh_subst'')
       
   466       ultimately have "P c (pi\<bullet>\<Gamma>) (App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)) ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)]) T2"
       
   467 	by simp
       
   468       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App (Lam [x].s12) s2) (pi\<bullet>t12[x::=t2]) (pi\<bullet>T2)" by (simp add: subst_eqvt)
       
   469     qed
       
   470   then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>T)" by blast
       
   471   then show "P c \<Gamma> s t T" by simp
       
   472 qed
       
   473 
       
   474 text {* Weak head reduction *}
       
   475 
       
   476 inductive2
       
   477   whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) 
       
   478 where
       
   479   QAR_Beta[intro]: "App (Lam [x]. t12) t2 \<leadsto> t12[x::=t2]"
       
   480 | QAR_App[intro]: "t1 \<leadsto> t1' \<Longrightarrow> App t1 t2 \<leadsto> App t1' t2"
       
   481 
       
   482 declare trm.inject  [simp add]
       
   483 declare ty.inject  [simp add]
       
   484 
       
   485 inductive_cases2 whr_Gen[elim]: "t \<leadsto> t'"
       
   486 inductive_cases2 whr_Lam[elim]: "Lam [x].t \<leadsto> t'"
       
   487 inductive_cases2 whr_App_Lam[elim]: "App (Lam [x].t12) t2 \<leadsto> t"
       
   488 inductive_cases2 whr_Var[elim]: "Var x \<leadsto> t"
       
   489 inductive_cases2 whr_Const[elim]: "Const n \<leadsto> t"
       
   490 inductive_cases2 whr_App[elim]: "App p q \<leadsto> t"
       
   491 inductive_cases2 whr_Const_Right[elim]: "t \<leadsto> Const n"
       
   492 inductive_cases2 whr_Var_Right[elim]: "t \<leadsto> Var x"
       
   493 inductive_cases2 whr_App_Right[elim]: "t \<leadsto> App p q"
       
   494 
       
   495 declare trm.inject  [simp del]
       
   496 declare ty.inject  [simp del]
       
   497 
       
   498 text {* Weak head normalization *}
       
   499 
       
   500 abbreviation 
       
   501  nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100)
       
   502 where
       
   503   "t\<leadsto>|  \<equiv> \<not>(\<exists> u. t \<leadsto> u)" 
       
   504 
       
   505 inductive2
       
   506   whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 
       
   507 where
       
   508   QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u"
       
   509 | QAN_Normal[intro]: "t\<leadsto>|  \<Longrightarrow> t \<Down> t"
       
   510 
       
   511 lemma whr_eqvt:
       
   512   fixes pi::"name prm"
       
   513   assumes a: "t \<leadsto> t'"
       
   514   shows "(pi\<bullet>t) \<leadsto> (pi\<bullet>t')"
       
   515 using a
       
   516 by (induct) (auto simp add: subst_eqvt fresh_bij)
       
   517 
       
   518 lemma whn_eqvt[eqvt]:
       
   519   fixes pi::"name prm"
       
   520   assumes a: "t \<Down> t'"
       
   521   shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')"
       
   522 using a
       
   523 apply(induct)
       
   524 apply(rule QAN_Reduce)
       
   525 apply(rule whr_eqvt)
       
   526 apply(assumption)+
       
   527 apply(rule QAN_Normal)
       
   528 apply(auto)
       
   529 apply(drule_tac pi="rev pi" in whr_eqvt)
       
   530 apply(perm_simp)
       
   531 done
       
   532 
       
   533 text {* Algorithmic term equivalence and algorithmic path equivalence *}
       
   534 
       
   535 inductive2
       
   536   alg_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ <=> _ : _" [60,60] 60) 
       
   537 and
       
   538   alg_path_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60] 60) 
       
   539 where
       
   540   QAT_Base[intro]:  "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : TBase"
       
   541 | QAT_Arrow[intro]: "\<lbrakk>x\<sharp>\<Gamma>; x\<sharp>s; x\<sharp>t; (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2\<rbrakk> 
       
   542                      \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T1 \<rightarrow> T2"
       
   543 | QAT_One[intro]:   "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : TUnit"
       
   544 | QAP_Var[intro]:   "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T"
       
   545 | QAP_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T1 \<rightarrow> T2; \<Gamma> \<turnstile> s <=> t : T1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T2"
       
   546 | QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
       
   547 
       
   548 lemma alg_equiv_alg_path_equiv_eqvt[eqvt]:
       
   549   fixes pi::"name prm"
       
   550   shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : (pi\<bullet>T)" 
       
   551   and   "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>p) \<leftrightarrow> (pi\<bullet>q) : (pi\<bullet>T)"
       
   552 apply(induct rule: alg_equiv_alg_path_equiv.inducts)
       
   553 apply(auto intro: whn_eqvt simp add: fresh_bij valid_eqvt)
       
   554 apply(rule_tac x="pi\<bullet>x" in  QAT_Arrow)
       
   555 apply(auto simp add: fresh_bij)
       
   556 apply(rule QAP_Var)
       
   557 apply(simp add: valid_eqvt)
       
   558 apply(simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
       
   559 apply(perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst])
       
   560 done
       
   561 
       
   562 lemma alg_equiv_alg_path_equiv_strong_induct
       
   563   [case_names QAT_Base QAT_Arrow QAT_One QAP_Var QAP_App QAP_Const]:
       
   564   fixes c::"'a::fs_name"
       
   565   assumes a1: "\<And>s p t q \<Gamma> c. \<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase; \<And>d. P2 d \<Gamma> p q TBase\<rbrakk> 
       
   566                \<Longrightarrow> P1 c \<Gamma> s t TBase"
       
   567   and     a2: "\<And>x \<Gamma> s t T1 T2 c.
       
   568                \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>s; x\<sharp>t; x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2;
       
   569                \<And>d. P1 d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk>
       
   570                \<Longrightarrow> P1 c \<Gamma> s t (T1\<rightarrow>T2)"
       
   571   and     a3: "\<And>\<Gamma> s t c. valid \<Gamma> \<Longrightarrow> P1 c \<Gamma> s t TUnit"
       
   572   and     a4: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P2 c \<Gamma> (Var x) (Var x) T"
       
   573   and     a5: "\<And>\<Gamma> p q T1 T2 s t c.
       
   574                \<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2; \<And>d. P2 d \<Gamma> p q (T1\<rightarrow>T2); \<Gamma> \<turnstile> s <=> t : T1; \<And>d. P1 d \<Gamma> s t T1\<rbrakk>
       
   575                \<Longrightarrow> P2 c \<Gamma> (App p s) (App q t) T2"
       
   576   and     a6: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P2 c \<Gamma> (Const n) (Const n) TBase"
       
   577   shows "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow>P1 c \<Gamma> s t T) \<and> (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c \<Gamma>' s' t' T')"
       
   578 proof -
       
   579   have "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow> (\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T)) \<and> 
       
   580         (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> (\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>') (pi\<bullet>s') (pi\<bullet>t') T'))"
       
   581   proof(induct rule: alg_equiv_alg_path_equiv.induct)
       
   582     case (QAT_Base s q t p \<Gamma>)
       
   583     then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TBase"
       
   584       apply(auto)
       
   585       apply(rule_tac p="pi\<bullet>q" and q="pi\<bullet>p" in  a1)
       
   586       apply(simp_all add: whn_eqvt alg_equiv_alg_path_equiv_eqvt[simplified])
       
   587       done
       
   588   next
       
   589     case (QAT_Arrow x \<Gamma> s t T1 T2)
       
   590     show ?case
       
   591     proof (rule allI, rule allI)
       
   592       fix c::"'a::fs_name" and pi::"name prm"
       
   593       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>s,pi\<bullet>t,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1])
       
   594       let ?sw="[(pi\<bullet>x,y)]"
       
   595       let ?pi'="?sw@pi"
       
   596       have f0: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
       
   597       then have f1: "x\<sharp>(\<Gamma>,s,t)" by simp
       
   598       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s,t))" using f1 by (simp add: fresh_bij)
       
   599       have f3: "y\<sharp>?pi'\<bullet>(\<Gamma>,s,t)" using f1 
       
   600 	by (simp only: pt_name2 fresh_left, auto simp add: perm_pi_simp calc_atm)
       
   601       then have f3': "y\<sharp>?pi'\<bullet>\<Gamma>" "y\<sharp>?pi'\<bullet>s" "y\<sharp>?pi'\<bullet>t" by (auto simp add: fresh_prod)
       
   602       have pr1: "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact
       
   603       then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>(App s (Var x))) <=> (?pi'\<bullet>(App t (Var x))) : (?pi'\<bullet>T2)" 
       
   604 	by (rule alg_equiv_alg_path_equiv_eqvt)
       
   605       then have "(y,T1)#(?pi'\<bullet>\<Gamma>) \<turnstile> (App (?pi'\<bullet>s) (Var y)) <=> (App (?pi'\<bullet>t) (Var y)) : T2" 
       
   606 	by (simp add: calc_atm)
       
   607       moreover    
       
   608       have ih1: "\<forall>c (pi::name prm).  P1 c (pi\<bullet>((x,T1)#\<Gamma>)) (pi\<bullet>App s (Var x)) (pi\<bullet>App t (Var x)) T2"
       
   609 	by fact
       
   610       then have "\<And>c.  P1 c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>App s (Var x)) (?pi'\<bullet>App t (Var x)) T2"
       
   611 	by auto
       
   612       then have "\<And>c.  P1 c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (App (?pi'\<bullet>s) (Var y)) (App (?pi'\<bullet>t) (Var y)) T2"
       
   613 	by (simp add: calc_atm)     
       
   614       ultimately have "P1 c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s) (?pi'\<bullet>t) (T1\<rightarrow>T2)" using a2 f3' fs by simp
       
   615       then have "P1 c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>pi\<bullet>s) (?sw\<bullet>pi\<bullet>t) (T1\<rightarrow>T2)" 
       
   616 	by (simp del: append_Cons add: calc_atm pt_name2)
       
   617       moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
       
   618 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified])
       
   619       moreover have "(?sw\<bullet>(pi\<bullet>s)) = (pi\<bullet>s)" 
       
   620 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified])
       
   621       moreover have "(?sw\<bullet>(pi\<bullet>t)) = (pi\<bullet>t)" 
       
   622 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified])
       
   623       ultimately show "P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T1\<rightarrow>T2)" by (simp)
       
   624     qed
       
   625   next
       
   626     case (QAT_One \<Gamma> s t)
       
   627     then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TUnit"
       
   628       by (auto intro!: a3 simp add: valid_eqvt)
       
   629   next
       
   630     case (QAP_Var \<Gamma> x T)
       
   631     then show "\<forall>c (pi::name prm). P2 c (pi \<bullet> \<Gamma>) (pi \<bullet> Var x) (pi \<bullet> Var x) T"
       
   632       apply(auto intro!: a4 simp add: valid_eqvt)
       
   633       apply(simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
       
   634       apply(perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst])
       
   635       done
       
   636   next
       
   637     case (QAP_App \<Gamma> p q T1 T2 s t)
       
   638     then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>App p s) (pi\<bullet>App q t) T2"
       
   639       by (auto intro!: a5 simp add: alg_equiv_alg_path_equiv_eqvt[simplified])
       
   640   next
       
   641     case (QAP_Const \<Gamma> n)
       
   642     then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>Const n) (pi\<bullet>Const n) TBase"
       
   643       by (auto intro!: a6 simp add: valid_eqvt)
       
   644   qed
       
   645   then have "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow> P1 c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) T) \<and> 
       
   646              (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c (([]::name prm)\<bullet>\<Gamma>') (([]::name prm)\<bullet>s') (([]::name prm)\<bullet>t') T')"
       
   647     by blast
       
   648   then show ?thesis by simp
       
   649 qed
       
   650 
       
   651 (* post-processing of the strong induction principle proved above; *) 
       
   652 (* the code extracts the strong_inducts-version from strong_induct *)
       
   653 setup {*
       
   654   PureThy.add_thmss
       
   655     [(("alg_equiv_alg_path_equiv_strong_inducts",
       
   656       ProjectRule.projects (ProofContext.init (the_context())) [1,2]
       
   657         (thm "alg_equiv_alg_path_equiv_strong_induct")), [])] #> snd
       
   658 *}
       
   659 
       
   660 declare trm.inject  [simp add]
       
   661 declare ty.inject  [simp add]
       
   662 
       
   663 inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'"
       
   664 
       
   665 inductive_cases2 alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s<=>t : TBase"
       
   666 inductive_cases2 alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s<=>t : T1 \<rightarrow> T2"
       
   667 
       
   668 inductive_cases2 alg_path_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
       
   669 inductive_cases2 alg_path_equiv_Unit_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
       
   670 inductive_cases2 alg_path_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : T1 \<rightarrow> T2"
       
   671 
       
   672 inductive_cases2 alg_path_equiv_Var_left_inv_auto[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
       
   673 inductive_cases2 alg_path_equiv_Var_left_inv_auto'[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
       
   674 inductive_cases2 alg_path_equiv_Var_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
       
   675 inductive_cases2 alg_path_equiv_Var_right_inv_auto'[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
       
   676 inductive_cases2 alg_path_equiv_Const_left_inv_auto[elim]: "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
       
   677 inductive_cases2 alg_path_equiv_Const_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
       
   678 inductive_cases2 alg_path_equiv_App_left_inv_auto[elim]: "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
       
   679 inductive_cases2 alg_path_equiv_App_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
       
   680 inductive_cases2 alg_path_equiv_Lam_left_inv_auto[elim]: "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
       
   681 inductive_cases2 alg_path_equiv_Lam_right_inv_auto[elim]: "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
       
   682 
       
   683 declare trm.inject [simp del]
       
   684 declare ty.inject [simp del]
       
   685 
       
   686 text {* Subcontext. *}
       
   687 
       
   688 abbreviation
       
   689   "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [55,55] 55)
       
   690 where
       
   691   "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2) \<and> valid \<Gamma>2"
       
   692 
       
   693 lemma alg_equiv_valid:
       
   694   shows  "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> valid \<Gamma>" and  "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
       
   695 by (induct rule : alg_equiv_alg_path_equiv.inducts, auto)
       
   696 
       
   697 lemma algorithmic_monotonicity:
       
   698   fixes \<Gamma>':: "(name\<times>ty) list"
       
   699   shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s <=> t : T"
       
   700   and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
       
   701 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts)
       
   702   case (QAT_Arrow x \<Gamma> s t T1 T2 \<Gamma>')
       
   703   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
       
   704   have h2:"\<Gamma>\<lless>\<Gamma>'" by fact
       
   705   have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T1)#\<Gamma> \<lless> \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact
       
   706   have "x\<sharp>\<Gamma>'" by fact
       
   707   then have sub:"(x,T1)#\<Gamma> \<lless> (x,T1)#\<Gamma>'" using h2 by auto
       
   708   then have "(x,T1)#\<Gamma>' \<turnstile> App s (Var x) <=> App t (Var x) : T2" using ih by auto
       
   709   then show "\<Gamma>' \<turnstile> s <=> t : T1\<rightarrow>T2" using sub fs by auto
       
   710 qed (auto)
       
   711 
       
   712 text {* Logical equivalence. *}
       
   713 
       
   714 function log_equiv :: "((name\<times>ty) list \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)"   
       
   715                       ("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) 
       
   716 where    
       
   717    "\<Gamma> \<turnstile> s is t : TUnit = valid \<Gamma>"
       
   718  | "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s <=> t : TBase"
       
   719  | "\<Gamma> \<turnstile> s is t : (T1 \<rightarrow> T2) =  
       
   720            (valid \<Gamma> \<and> (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T2)))"
       
   721 apply (auto simp add: ty.inject)
       
   722 apply (subgoal_tac "(\<exists>T1 T2. b=T1 \<rightarrow> T2) \<or> b=TUnit \<or> b=TBase" )
       
   723 apply (force)
       
   724 apply (rule ty_cases)
       
   725 done
       
   726 
       
   727 termination
       
   728 apply(relation "measure (\<lambda>(_,_,_,T). size T)")
       
   729 apply(auto)
       
   730 done
       
   731 
       
   732 lemma log_equiv_valid: 
       
   733   assumes "\<Gamma> \<turnstile> s is t : T"
       
   734   shows "valid \<Gamma>"
       
   735 using assms 
       
   736 by (induct rule: log_equiv.induct,auto elim: alg_equiv_valid)
       
   737 
       
   738 lemma logical_monotonicity :
       
   739  fixes T::ty
       
   740  assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma>\<lless>\<Gamma>'" 
       
   741  shows "\<Gamma>' \<turnstile> s is t : T"
       
   742 using assms
       
   743 proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct)
       
   744   case (2 \<Gamma> s t \<Gamma>')
       
   745   then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto
       
   746 next
       
   747   case (3 \<Gamma> s t T1 T2 \<Gamma>')
       
   748   have h1:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact
       
   749   have h2:"\<Gamma>\<lless>\<Gamma>'" by fact
       
   750   {
       
   751     fix \<Gamma>'' s' t'
       
   752     assume "\<Gamma>'\<lless>\<Gamma>''" "\<Gamma>'' \<turnstile> s' is t' : T1"
       
   753     then have "\<Gamma>'' \<turnstile> (App s s') is (App t t') : T2" using h1 h2 by auto
       
   754   }
       
   755   then show "\<Gamma>' \<turnstile> s is t : T1\<rightarrow>T2" using h2 by auto
       
   756 qed (auto)
       
   757   
       
   758 lemma forget: 
   477 lemma forget: 
   759   fixes x::"name"
   478   fixes x::"name"
   760   and   L::"trm"
   479   and   L::"trm"
   761   assumes a: "x\<sharp>L" 
   480   assumes a: "x\<sharp>L" 
   762   shows "L[x::=P] = L"
   481   shows "L[x::=P] = L"
   764 by (nominal_induct L avoiding: x P rule: trm.induct)
   483 by (nominal_induct L avoiding: x P rule: trm.induct)
   765    (auto simp add: fresh_atm abs_fresh)
   484    (auto simp add: fresh_atm abs_fresh)
   766 
   485 
   767 lemma subst_fun_eq:
   486 lemma subst_fun_eq:
   768   fixes u::trm
   487   fixes u::trm
   769   assumes h:"[x].t1 = [y].t2"
   488   assumes h:"[x].t\<^isub>1 = [y].t\<^isub>2"
   770   shows "t1[x::=u] = t2[y::=u]"
   489   shows "t\<^isub>1[x::=u] = t\<^isub>2[y::=u]"
   771 proof -
   490 proof -
   772   { 
   491   { 
   773     assume "x=y" and "t1=t2"
   492     assume "x=y" and "t\<^isub>1=t\<^isub>2"
   774     then have ?thesis using h by simp
   493     then have ?thesis using h by simp
   775   }
   494   }
   776   moreover 
   495   moreover 
   777   {
   496   {
   778     assume h1:"x \<noteq> y" and h2:"t1=[(x,y)] \<bullet> t2" and h3:"x \<sharp> t2"
   497     assume h1:"x \<noteq> y" and h2:"t\<^isub>1=[(x,y)] \<bullet> t\<^isub>2" and h3:"x \<sharp> t\<^isub>2"
   779     then have "([(x,y)] \<bullet> t2)[x::=u] = t2[y::=u]" by (simp add: subst_rename)
   498     then have "([(x,y)] \<bullet> t\<^isub>2)[x::=u] = t\<^isub>2[y::=u]" by (simp add: subst_rename)
   780     then have ?thesis using h2 by simp 
   499     then have ?thesis using h2 by simp 
   781   }
   500   }
   782   ultimately show ?thesis using alpha h by blast
   501   ultimately show ?thesis using alpha h by blast
   783 qed
   502 qed
   784 
   503 
   785 lemma psubst_empty[simp]:
   504 lemma psubst_empty[simp]:
   786   shows "[]<t> = t"
   505   shows "[]<t> = t"
   787   by (nominal_induct t rule: trm.induct) (auto simp add: fresh_list_nil)
   506   by (nominal_induct t rule: trm.induct) (auto simp add: fresh_list_nil)
   788 
   507 
   789 lemma psubst_subst_psubst:
   508 lemma psubst_subst_psubst:
   790   assumes h:"c \<sharp> \<theta>"
   509   assumes h:"c\<sharp>\<theta>"
   791   shows "\<theta><t>[c::=s] = (c,s)#\<theta><t>"
   510   shows "\<theta><t>[c::=s] = (c,s)#\<theta><t>"
   792   using h
   511   using h
   793 by (nominal_induct t avoiding: \<theta> c s rule: trm.induct)
   512 by (nominal_induct t avoiding: \<theta> c s rule: trm.induct)
   794    (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
   513    (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
   795 
   514 
   828   ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" by auto
   547   ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" by auto
   829   moreover have "Lam [n].(\<theta><t>[x::=\<theta><u>]) = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs fresh_psubst by auto
   548   moreover have "Lam [n].(\<theta><t>[x::=\<theta><u>]) = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs fresh_psubst by auto
   830   ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs by auto
   549   ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs by auto
   831   then show "\<theta><(Lam [n].t)[x::=u]> = \<theta><Lam [n].t>[x::=\<theta><u>]" using fs by auto
   550   then show "\<theta><(Lam [n].t)[x::=u]> = \<theta><Lam [n].t>[x::=\<theta><u>]" using fs by auto
   832 qed (auto)
   551 qed (auto)
       
   552 
       
   553 text {* 
       
   554 \section{Equivalence}
       
   555 \subsection{Definition of the equivalence relation}
       
   556  *}
       
   557 
       
   558 (*<*)
       
   559 inductive2
       
   560   equiv_def :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<equiv> _ : _" [60,60] 60) 
       
   561 where
       
   562   Q_Refl[intro]:  "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<equiv> t : T"
       
   563 | Q_Symm[intro]:  "\<Gamma> \<turnstile> t \<equiv> s : T \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"
       
   564 | Q_Trans[intro]: "\<lbrakk>\<Gamma> \<turnstile> s \<equiv> t : T; \<Gamma> \<turnstile> t \<equiv> u : T\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> s \<equiv> u : T"
       
   565 | Q_Abs[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s\<^isub>2 \<equiv>  Lam [x]. t\<^isub>2 : T\<^isub>1 \<rightarrow> T\<^isub>2"
       
   566 | Q_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> s\<^isub>1 \<equiv> t\<^isub>1 : T\<^isub>1 \<rightarrow> T\<^isub>2 ; \<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> App s\<^isub>1 s\<^isub>2 \<equiv> App t\<^isub>1 t\<^isub>2 : T\<^isub>2"
       
   567 | Q_Beta[intro]:  "\<lbrakk>x\<sharp>(\<Gamma>,s\<^isub>2,t\<^isub>2); (x,T\<^isub>1)#\<Gamma> \<turnstile> s12 \<equiv> t12 : T\<^isub>2 ; \<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1\<rbrakk> 
       
   568                    \<Longrightarrow>  \<Gamma> \<turnstile> App (Lam [x]. s12) s\<^isub>2 \<equiv>  t12[x::=t\<^isub>2] : T\<^isub>2"
       
   569 | Q_Ext[intro]:   "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2\<rbrakk> 
       
   570                    \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
       
   571 (*>*)
       
   572 
       
   573 text {* 
       
   574 \begin{center}
       
   575 \isastyle
       
   576 @{thm[mode=Rule] Q_Refl[no_vars]}{\sc{Q\_Refl}}\qquad
       
   577 @{thm[mode=Rule] Q_Symm[no_vars]}{\sc{Q\_Symm}}\\
       
   578 @{thm[mode=Rule] Q_Trans[no_vars]}{\sc{Q\_Trans}}\\
       
   579 @{thm[mode=Rule] Q_App[no_vars]}{\sc{Q\_App}}\\
       
   580 @{thm[mode=Rule] Q_Abs[no_vars]}{\sc{Q\_Abs}}\\
       
   581 @{thm[mode=Rule] Q_Beta[no_vars]}{\sc{Q\_Beta}}\\
       
   582 @{thm[mode=Rule] Q_Ext[no_vars]}{\sc{Q\_Ext}}\\
       
   583 \end{center}
       
   584 *}
       
   585 
       
   586 text {* It is now a tradition, we derive the lemma about validity, and we generate the equivariance lemma. *}
       
   587 
       
   588 lemma equiv_def_valid:
       
   589   assumes "\<Gamma> \<turnstile> t \<equiv> s : T"
       
   590   shows "valid \<Gamma>"
       
   591 using assms by (induct,auto elim:typing_valid)
       
   592 
       
   593 nominal_inductive equiv_def
       
   594 
       
   595 text{*
       
   596 \subsection{Strong induction principle for the equivalence relation}
       
   597 *}
       
   598 
       
   599 lemma equiv_def_strong_induct
       
   600   [consumes 1, case_names Q_Refl Q_Symm Q_Trans Q_Abs Q_App Q_Beta Q_Ext]:
       
   601   fixes c::"'a::fs_name"
       
   602   assumes a0: "\<Gamma> \<turnstile> s \<equiv> t : T" 
       
   603   and     a1: "\<And>\<Gamma> t T c.  \<Gamma> \<turnstile> t : T  \<Longrightarrow> P c \<Gamma> t t T"
       
   604   and     a2: "\<And>\<Gamma> t s T c. \<lbrakk>\<And>d. P d \<Gamma> t s T\<rbrakk> \<Longrightarrow>  P c \<Gamma> s t T"
       
   605   and     a3: "\<And>\<Gamma> s t T u c. \<lbrakk>\<And>d. P d \<Gamma> s t T; \<And>d. P d \<Gamma> t u T\<rbrakk> 
       
   606                \<Longrightarrow> P c \<Gamma> s u T"
       
   607   and     a4: "\<And>x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 c. \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>c; \<And>d. P d ((x,T\<^isub>1)#\<Gamma>) s\<^isub>2 t\<^isub>2 T\<^isub>2\<rbrakk>
       
   608                \<Longrightarrow> P c \<Gamma> (Lam [x].s\<^isub>2) (Lam [x].t\<^isub>2) (T\<^isub>1\<rightarrow>T\<^isub>2)"
       
   609   and     a5: "\<And>\<Gamma> s\<^isub>1 t\<^isub>1 T\<^isub>1 T\<^isub>2 s\<^isub>2 t\<^isub>2 c. \<lbrakk>\<And>d. P d \<Gamma> s\<^isub>1 t\<^isub>1 (T\<^isub>1\<rightarrow>T\<^isub>2); \<And>d. P d \<Gamma> s\<^isub>2 t\<^isub>2 T\<^isub>1\<rbrakk> 
       
   610                \<Longrightarrow> P c \<Gamma> (App s\<^isub>1 s\<^isub>2) (App t\<^isub>1 t\<^isub>2) T\<^isub>2"
       
   611   and     a6: "\<And>x \<Gamma> T\<^isub>1 s12 t12 T\<^isub>2 s\<^isub>2 t\<^isub>2 c.
       
   612                \<lbrakk>x\<sharp>(\<Gamma>,s\<^isub>2,t\<^isub>2); x\<sharp>c; \<And>d. P d ((x,T\<^isub>1)#\<Gamma>) s12 t12 T\<^isub>2; \<And>d. P d \<Gamma> s\<^isub>2 t\<^isub>2 T\<^isub>1\<rbrakk> 
       
   613                \<Longrightarrow> P c \<Gamma> (App (Lam [x].s12) s\<^isub>2) (t12[x::=t\<^isub>2]) T\<^isub>2"
       
   614   and     a7: "\<And>x \<Gamma> s t T\<^isub>1 T\<^isub>2 c.
       
   615                \<lbrakk>x\<sharp>(\<Gamma>,s,t); \<And>d. P d ((x,T\<^isub>1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T\<^isub>2\<rbrakk>
       
   616                \<Longrightarrow> P c \<Gamma> s t (T\<^isub>1\<rightarrow>T\<^isub>2)"
       
   617  shows "P c \<Gamma>  s t T"
       
   618 proof -
       
   619   from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" 
       
   620     proof(induct)
       
   621       case (Q_Refl \<Gamma> t T pi c)
       
   622       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) (pi\<bullet>T)" using a1 by (simp only: eqvt)
       
   623     next
       
   624       case (Q_Symm \<Gamma> t s T pi c)
       
   625       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" using a2 by (simp only: equiv_def_eqvt)
       
   626     next
       
   627       case (Q_Trans \<Gamma> s t T u pi c)
       
   628       then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) (pi\<bullet>T)" using a3 by (blast intro: equiv_def_eqvt)
       
   629     next
       
   630       case (Q_App \<Gamma> s\<^isub>1 t\<^isub>1 T\<^isub>1 T\<^isub>2 s\<^isub>2 t\<^isub>2 pi c)
       
   631       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s\<^isub>1 s\<^isub>2) (pi\<bullet>App t\<^isub>1 t\<^isub>2) (pi\<bullet>T\<^isub>2)" using a5 
       
   632 	by (simp only: eqvt) (blast)
       
   633     next
       
   634       case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>2 pi c)
       
   635       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T\<^isub>1\<rightarrow>T\<^isub>2)"  
       
   636 	by (auto intro!: a7 simp add: fresh_bij)
       
   637     next
       
   638       case (Q_Abs x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 pi c)
       
   639       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s\<^isub>2,pi\<bullet>t\<^isub>2,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1])
       
   640       let ?sw="[(pi\<bullet>x,y)]"
       
   641       let ?pi'="?sw@pi"
       
   642       have f1: "x\<sharp>\<Gamma>" by fact
       
   643       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij)
       
   644       have f3: "y\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp)
       
   645       have ih1: "\<And>c. P c (?pi'\<bullet>((x,T\<^isub>1)#\<Gamma>)) (?pi'\<bullet>s\<^isub>2) (?pi'\<bullet>t\<^isub>2) (?pi'\<bullet>T\<^isub>2)" by fact
       
   646       then have "\<And>c. P c ((y,T\<^isub>1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s\<^isub>2) (?pi'\<bullet>t\<^isub>2) T\<^isub>2" by (simp add: calc_atm)
       
   647       then have "P c  (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>Lam [x].s\<^isub>2) (?pi'\<bullet>Lam [x].t\<^isub>2) (T\<^isub>1\<rightarrow>T\<^isub>2)" using a4 f3 fs
       
   648 	by (simp add: calc_atm)
       
   649       then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>s\<^isub>2)) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>t\<^isub>2)) (T\<^isub>1\<rightarrow>T\<^isub>2)" 
       
   650 	by (simp del: append_Cons add: calc_atm pt_name2)
       
   651       moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
       
   652 	by (rule perm_fresh_fresh) (simp_all add: fs f2)
       
   653       moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>s\<^isub>2))) = Lam [(pi\<bullet>x)].(pi\<bullet>s\<^isub>2)" 
       
   654 	by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh)
       
   655       moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t\<^isub>2))) = Lam [(pi\<bullet>x)].(pi\<bullet>t\<^isub>2)" 
       
   656 	by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh)
       
   657       ultimately have "P c (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>x)].(pi\<bullet>s\<^isub>2)) (Lam [(pi\<bullet>x)].(pi\<bullet>t\<^isub>2)) (T\<^isub>1\<rightarrow>T\<^isub>2)" by simp
       
   658       then show  "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Lam [x].s\<^isub>2) (pi\<bullet>Lam [x].t\<^isub>2) (pi\<bullet>T\<^isub>1\<rightarrow>T\<^isub>2)" by simp 
       
   659     next 
       
   660       case (Q_Beta x \<Gamma> s\<^isub>2 t\<^isub>2 T\<^isub>1 s12 t12 T\<^isub>2 pi c) 
       
   661       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s12,pi\<bullet>t12,pi\<bullet>s\<^isub>2,pi\<bullet>t\<^isub>2,pi\<bullet>\<Gamma>,c)" 
       
   662 	by (rule exists_fresh[OF fs_name1])
       
   663       let ?sw="[(pi\<bullet>x,y)]"
       
   664       let ?pi'="?sw@pi"
       
   665       have f1: "x\<sharp>(\<Gamma>,s\<^isub>2,t\<^isub>2)" by fact 
       
   666       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s\<^isub>2,t\<^isub>2))" using f1 by (simp add: fresh_bij)
       
   667       have f3: "y\<sharp>(?pi'\<bullet>(\<Gamma>,s\<^isub>2,t\<^isub>2))" using f1 
       
   668 	by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp fresh_prod)
       
   669       have ih1: "\<And>c. P c (?pi'\<bullet>((x,T\<^isub>1)#\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T\<^isub>2)" by fact
       
   670       then have "\<And>c. P c ((y,T\<^isub>1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T\<^isub>2)" by (simp add: calc_atm)
       
   671       moreover
       
   672       have ih2: "\<And>c. P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s\<^isub>2) (?pi'\<bullet>t\<^isub>2) (?pi'\<bullet>T\<^isub>1)" by fact
       
   673       ultimately have "P c  (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(App (Lam [x].s12) s\<^isub>2)) (?pi'\<bullet>(t12[x::=t\<^isub>2])) (?pi'\<bullet>T\<^isub>2)" 
       
   674 	using a6 f3 fs by (force simp add: subst_eqvt calc_atm del: perm_ty)
       
   675       then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s\<^isub>2))) 
       
   676 	(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t\<^isub>2)])) T\<^isub>2" 
       
   677 	by (simp del: append_Cons add: calc_atm pt_name2 subst_eqvt)
       
   678       moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
       
   679 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified])
       
   680       moreover have "(?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s\<^isub>2))) = App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s\<^isub>2)" 
       
   681 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified] abs_fresh)
       
   682       moreover have "(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t\<^isub>2)])) = ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t\<^isub>2)])" 
       
   683 	by (rule perm_fresh_fresh) 
       
   684 	   (simp_all add: fs[simplified] f2[simplified] fresh_subst fresh_subst'')
       
   685       ultimately have "P c (pi\<bullet>\<Gamma>) (App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s\<^isub>2)) ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t\<^isub>2)]) T\<^isub>2"
       
   686 	by simp
       
   687       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App (Lam [x].s12) s\<^isub>2) (pi\<bullet>t12[x::=t\<^isub>2]) (pi\<bullet>T\<^isub>2)" by (simp add: subst_eqvt)
       
   688     qed
       
   689   then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>T)" by blast
       
   690   then show "P c \<Gamma> s t T" by simp
       
   691 qed
       
   692 
       
   693 
       
   694 text {* \section{Type-driven equivalence algorithm} 
       
   695 
       
   696 We follow the original presentation. The algorithm is described using inference rules only.
       
   697 
       
   698 *}
       
   699 
       
   700 text {* \subsection{Weak head reduction} *}
       
   701 
       
   702 (*<*)
       
   703 inductive2
       
   704   whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) 
       
   705 where
       
   706   QAR_Beta[intro]: "App (Lam [x]. t12) t\<^isub>2 \<leadsto> t12[x::=t\<^isub>2]"
       
   707 | QAR_App[intro]: "t1 \<leadsto> t1' \<Longrightarrow> App t1 t\<^isub>2 \<leadsto> App t1' t\<^isub>2"
       
   708 (*>*)
       
   709 
       
   710 text {* 
       
   711 \begin{figure}
       
   712 \begin{center}
       
   713 \isastyle
       
   714 @{thm[mode=Rule] QAR_Beta[no_vars]}{\sc{QAR\_Beta}} \qquad
       
   715 @{thm[mode=Rule] QAR_App[no_vars]}{\sc{QAR\_App}}
       
   716 \end{center}
       
   717 \end{figure}
       
   718 *}
       
   719 
       
   720 text {* \subsubsection{Inversion lemma for weak head reduction} *}
       
   721 
       
   722 declare trm.inject  [simp add]
       
   723 declare ty.inject  [simp add]
       
   724 
       
   725 inductive_cases2 whr_Gen[elim]: "t \<leadsto> t'"
       
   726 inductive_cases2 whr_Lam[elim]: "Lam [x].t \<leadsto> t'"
       
   727 inductive_cases2 whr_App_Lam[elim]: "App (Lam [x].t12) t2 \<leadsto> t"
       
   728 inductive_cases2 whr_Var[elim]: "Var x \<leadsto> t"
       
   729 inductive_cases2 whr_Const[elim]: "Const n \<leadsto> t"
       
   730 inductive_cases2 whr_App[elim]: "App p q \<leadsto> t"
       
   731 inductive_cases2 whr_Const_Right[elim]: "t \<leadsto> Const n"
       
   732 inductive_cases2 whr_Var_Right[elim]: "t \<leadsto> Var x"
       
   733 inductive_cases2 whr_App_Right[elim]: "t \<leadsto> App p q"
       
   734 
       
   735 declare trm.inject  [simp del]
       
   736 declare ty.inject  [simp del]
       
   737 
       
   738 nominal_inductive whr_def
       
   739 
       
   740 text {* 
       
   741 \subsection{Weak head normalization} 
       
   742 \subsubsection{Definition of the normal form}
       
   743 *}
       
   744 
       
   745 abbreviation 
       
   746  nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100)
       
   747 where
       
   748   "t\<leadsto>|  \<equiv> \<not>(\<exists> u. t \<leadsto> u)" 
       
   749 
       
   750 text{* \subsubsection{Definition of weak head normal form} *}
       
   751 
       
   752 (*<*)
       
   753 inductive2
       
   754   whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 
       
   755 where
       
   756   QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u"
       
   757 | QAN_Normal[intro]: "t\<leadsto>|  \<Longrightarrow> t \<Down> t"
       
   758 
       
   759 (*>*)
       
   760 
       
   761 text {* 
       
   762 \begin{center}
       
   763 @{thm[mode=Rule] QAN_Reduce[no_vars]}{\sc{QAN\_Reduce}}\qquad
       
   764 @{thm[mode=Rule] QAN_Normal[no_vars]}{\sc{QAN\_Normal}}
       
   765 \end{center}
       
   766 *}
       
   767 
       
   768 lemma whn_eqvt[eqvt]:
       
   769   fixes pi::"name prm"
       
   770   assumes a: "t \<Down> t'"
       
   771   shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')"
       
   772 using a
       
   773 apply(induct)
       
   774 apply(rule QAN_Reduce)
       
   775 apply(rule whr_def_eqvt)
       
   776 apply(assumption)+
       
   777 apply(rule QAN_Normal)
       
   778 apply(auto)
       
   779 apply(drule_tac pi="rev pi" in whr_def_eqvt)
       
   780 apply(perm_simp)
       
   781 done
       
   782 
       
   783 text {* \subsection{Algorithmic term equivalence and algorithmic path equivalence} *}
       
   784 
       
   785 (*<*)
       
   786 inductive2
       
   787   alg_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60] 60) 
       
   788 and
       
   789   alg_path_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60] 60) 
       
   790 where
       
   791   QAT_Base[intro]:  "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
       
   792 | QAT_Arrow[intro]: "\<lbrakk>x\<sharp>\<Gamma>; x\<sharp>s; x\<sharp>t; (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2\<rbrakk> 
       
   793                      \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
       
   794 | QAT_One[intro]:   "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TUnit"
       
   795 | QAP_Var[intro]:   "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T"
       
   796 | QAP_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2"
       
   797 | QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
       
   798 (*>*)
       
   799 
       
   800 text {* 
       
   801 \begin{center}
       
   802 @{thm[mode=Rule] QAT_Base[no_vars]}{\sc{QAT\_Base}}\\
       
   803 @{thm[mode=Rule] QAT_Arrow[no_vars]}{\sc{QAT\_Arrow}}\\
       
   804 @{thm[mode=Rule] QAP_Var[no_vars]}{\sc{QAP\_Var}}\\
       
   805 @{thm[mode=Rule] QAP_App[no_vars]}{\sc{QAP\_App}}\\
       
   806 @{thm[mode=Rule] QAP_Const[no_vars]}{\sc{QAP\_Const}}\\
       
   807 \end{center}
       
   808 *}
       
   809 
       
   810 text {* Again we generate the equivariance lemma. *}
       
   811 
       
   812 nominal_inductive  alg_equiv
       
   813 
       
   814 text {* \subsubsection{Strong induction principle for algorithmic term and path equivalences} *}
       
   815 
       
   816 lemma alg_equiv_alg_path_equiv_strong_induct
       
   817   [case_names QAT_Base QAT_Arrow QAT_One QAP_Var QAP_App QAP_Const]:
       
   818   fixes c::"'a::fs_name"
       
   819   assumes a1: "\<And>s p t q \<Gamma> c. \<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase; \<And>d. P2 d \<Gamma> p q TBase\<rbrakk> 
       
   820                \<Longrightarrow> P1 c \<Gamma> s t TBase"
       
   821   and     a2: "\<And>x \<Gamma> s t T\<^isub>1 T\<^isub>2 c.
       
   822                \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>s; x\<sharp>t; x\<sharp>c; (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2;
       
   823                \<And>d. P1 d ((x,T\<^isub>1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T\<^isub>2\<rbrakk>
       
   824                \<Longrightarrow> P1 c \<Gamma> s t (T\<^isub>1\<rightarrow>T\<^isub>2)"
       
   825   and     a3: "\<And>\<Gamma> s t c. valid \<Gamma> \<Longrightarrow> P1 c \<Gamma> s t TUnit"
       
   826   and     a4: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P2 c \<Gamma> (Var x) (Var x) T"
       
   827   and     a5: "\<And>\<Gamma> p q T\<^isub>1 T\<^isub>2 s t c.
       
   828                \<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2; \<And>d. P2 d \<Gamma> p q (T\<^isub>1\<rightarrow>T\<^isub>2); \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1; \<And>d. P1 d \<Gamma> s t T\<^isub>1\<rbrakk>
       
   829                \<Longrightarrow> P2 c \<Gamma> (App p s) (App q t) T\<^isub>2"
       
   830   and     a6: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P2 c \<Gamma> (Const n) (Const n) TBase"
       
   831   shows "(\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<longrightarrow>P1 c \<Gamma> s t T) \<and> (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c \<Gamma>' s' t' T')"
       
   832 proof -
       
   833   have "(\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<longrightarrow> (\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T)) \<and> 
       
   834         (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> (\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>') (pi\<bullet>s') (pi\<bullet>t') T'))"
       
   835   proof(induct rule: alg_equiv_alg_path_equiv.induct)
       
   836     case (QAT_Base s q t p \<Gamma>)
       
   837     then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TBase"
       
   838       apply(auto)
       
   839       apply(rule_tac p="pi\<bullet>q" and q="pi\<bullet>p" in  a1)
       
   840       apply(simp_all add: eqvt[simplified])
       
   841       done
       
   842   next
       
   843     case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2)
       
   844     show ?case
       
   845     proof (rule allI, rule allI)
       
   846       fix c::"'a::fs_name" and pi::"name prm"
       
   847       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>s,pi\<bullet>t,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1])
       
   848       let ?sw="[(pi\<bullet>x,y)]"
       
   849       let ?pi'="?sw@pi"
       
   850       have f0: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
       
   851       then have f1: "x\<sharp>(\<Gamma>,s,t)" by simp
       
   852       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s,t))" using f1 by (simp add: fresh_bij)
       
   853       have f3: "y\<sharp>?pi'\<bullet>(\<Gamma>,s,t)" using f1 
       
   854 	by (simp only: pt_name2 fresh_left, auto simp add: perm_pi_simp calc_atm)
       
   855       then have f3': "y\<sharp>?pi'\<bullet>\<Gamma>" "y\<sharp>?pi'\<bullet>s" "y\<sharp>?pi'\<bullet>t" by (auto simp add: fresh_prod)
       
   856       have pr1: "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
       
   857       then have "?pi'\<bullet> ((x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2)" using perm_bool by simp
       
   858       then have "(?pi'\<bullet>((x,T\<^isub>1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>(App s (Var x))) \<Leftrightarrow> (?pi'\<bullet>(App t (Var x))) : (?pi'\<bullet>T\<^isub>2)" 
       
   859 	by (auto simp add: eqvt)
       
   860       then have "(y,T\<^isub>1)#(?pi'\<bullet>\<Gamma>) \<turnstile> (App (?pi'\<bullet>s) (Var y)) \<Leftrightarrow> (App (?pi'\<bullet>t) (Var y)) : T\<^isub>2" 
       
   861 	by (simp add: calc_atm)
       
   862       moreover    
       
   863       have ih1: "\<forall>c (pi::name prm).  P1 c (pi\<bullet>((x,T\<^isub>1)#\<Gamma>)) (pi\<bullet>App s (Var x)) (pi\<bullet>App t (Var x)) T\<^isub>2"
       
   864 	by fact
       
   865       then have "\<And>c.  P1 c (?pi'\<bullet>((x,T\<^isub>1)#\<Gamma>)) (?pi'\<bullet>App s (Var x)) (?pi'\<bullet>App t (Var x)) T\<^isub>2"
       
   866 	by auto
       
   867       then have "\<And>c.  P1 c ((y,T\<^isub>1)#(?pi'\<bullet>\<Gamma>)) (App (?pi'\<bullet>s) (Var y)) (App (?pi'\<bullet>t) (Var y)) T\<^isub>2"
       
   868 	by (simp add: calc_atm)     
       
   869       ultimately have "P1 c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s) (?pi'\<bullet>t) (T\<^isub>1\<rightarrow>T\<^isub>2)" using a2 f3' fs by simp
       
   870       then have "P1 c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>pi\<bullet>s) (?sw\<bullet>pi\<bullet>t) (T\<^isub>1\<rightarrow>T\<^isub>2)" 
       
   871 	by (simp del: append_Cons add: calc_atm pt_name2)
       
   872       moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
       
   873 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified])
       
   874       moreover have "(?sw\<bullet>(pi\<bullet>s)) = (pi\<bullet>s)" 
       
   875 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified])
       
   876       moreover have "(?sw\<bullet>(pi\<bullet>t)) = (pi\<bullet>t)" 
       
   877 	by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified])
       
   878       ultimately show "P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T\<^isub>1\<rightarrow>T\<^isub>2)" by (simp)
       
   879     qed
       
   880   next
       
   881     case (QAT_One \<Gamma> s t)
       
   882     then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TUnit"
       
   883       by (auto intro!: a3 simp add: valid_eqvt)
       
   884   next
       
   885     case (QAP_Var \<Gamma> x T)
       
   886     then show "\<forall>c (pi::name prm). P2 c (pi \<bullet> \<Gamma>) (pi \<bullet> Var x) (pi \<bullet> Var x) T"
       
   887       apply(auto intro!: a4 simp add: valid_eqvt)
       
   888       apply(simp add: set_eqvt[symmetric])
       
   889       apply(perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst])
       
   890       done
       
   891   next
       
   892     case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t)
       
   893     then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>App p s) (pi\<bullet>App q t) T\<^isub>2"
       
   894       by (auto intro!: a5 simp add: eqvt[simplified])
       
   895   next
       
   896     case (QAP_Const \<Gamma> n)
       
   897     then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>Const n) (pi\<bullet>Const n) TBase"
       
   898       by (auto intro!: a6 simp add: eqvt)
       
   899   qed
       
   900   then have "(\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<longrightarrow> P1 c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) T) \<and> 
       
   901              (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c (([]::name prm)\<bullet>\<Gamma>') (([]::name prm)\<bullet>s') (([]::name prm)\<bullet>t') T')"
       
   902     by blast
       
   903   then show ?thesis by simp
       
   904 qed
       
   905 
       
   906 (* post-processing of the strong induction principle proved above; *) 
       
   907 (* the code extracts the strong_inducts-version from strong_induct *)
       
   908 (*<*)
       
   909 setup {*
       
   910   PureThy.add_thmss
       
   911     [(("alg_equiv_alg_path_equiv_strong_inducts",
       
   912       ProjectRule.projects (ProofContext.init (the_context())) [1,2]
       
   913         (thm "alg_equiv_alg_path_equiv_strong_induct")), [])] #> snd
       
   914 *}
       
   915 (*>*)
       
   916 
       
   917 lemma alg_equiv_valid:
       
   918   shows  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" and  "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
       
   919 by (induct rule : alg_equiv_alg_path_equiv.inducts, auto)
       
   920 
       
   921 text{* \subsubsection{Inversion lemmas for algorithmic term and path equivalences} *}
       
   922 
       
   923 declare trm.inject  [simp add]
       
   924 declare ty.inject  [simp add]
       
   925 
       
   926 inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'"
       
   927 
       
   928 inductive_cases2 alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
       
   929 inductive_cases2 alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
       
   930 
       
   931 inductive_cases2 alg_path_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
       
   932 inductive_cases2 alg_path_equiv_Unit_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
       
   933 inductive_cases2 alg_path_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
       
   934 
       
   935 inductive_cases2 alg_path_equiv_Var_left_inv_auto[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
       
   936 inductive_cases2 alg_path_equiv_Var_left_inv_auto'[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
       
   937 inductive_cases2 alg_path_equiv_Var_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
       
   938 inductive_cases2 alg_path_equiv_Var_right_inv_auto'[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
       
   939 inductive_cases2 alg_path_equiv_Const_left_inv_auto[elim]: "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
       
   940 inductive_cases2 alg_path_equiv_Const_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
       
   941 inductive_cases2 alg_path_equiv_App_left_inv_auto[elim]: "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
       
   942 inductive_cases2 alg_path_equiv_App_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
       
   943 inductive_cases2 alg_path_equiv_Lam_left_inv_auto[elim]: "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
       
   944 inductive_cases2 alg_path_equiv_Lam_right_inv_auto[elim]: "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
       
   945 
       
   946 declare trm.inject [simp del]
       
   947 declare ty.inject [simp del]
       
   948 
       
   949 text {* \section{Completeness of the algorithm} *}
       
   950 
       
   951 lemma algorithmic_monotonicity:
       
   952   fixes \<Gamma>':: "(name\<times>ty) list"
       
   953   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
       
   954   and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
       
   955 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts)
       
   956  case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
       
   957   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
       
   958   have h2:"\<Gamma>\<lless>\<Gamma>'" by fact
       
   959   have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<lless> \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
       
   960   have "x\<sharp>\<Gamma>'" by fact
       
   961   then have sub:"(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'" using h2 by auto
       
   962   then have "(x,T\<^isub>1)#\<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" using ih by auto
       
   963   then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using sub fs by auto
       
   964 qed (auto)
       
   965 
       
   966 lemma valid_monotonicity[elim]:
       
   967  assumes "\<Gamma> \<lless> \<Gamma>'" and "x\<sharp>\<Gamma>'"
       
   968  shows "(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'"
       
   969 using assms by auto
       
   970 
       
   971 lemma algorithmic_monotonicity_auto:
       
   972   fixes \<Gamma>':: "(name\<times>ty) list"
       
   973   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
       
   974   and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
       
   975 by (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts, auto simp add: valid_monotonicity)
   833  
   976  
   834 lemma fresh_subst_fresh:
   977 text {* \subsection{Definition of the logical relation} *}
   835     assumes "a\<sharp>e"
   978 
   836     shows "a\<sharp>t[a::=e]"
   979 function log_equiv :: "((name\<times>ty) list \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)"   
       
   980                       ("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) 
       
   981 where    
       
   982    "\<Gamma> \<turnstile> s is t : TUnit = valid \<Gamma>"
       
   983  | "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
       
   984  | "\<Gamma> \<turnstile> s is t : (T\<^isub>1 \<rightarrow> T\<^isub>2) =  
       
   985            (valid \<Gamma> \<and> (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2)))"
       
   986 apply (auto simp add: ty.inject)
       
   987 apply (subgoal_tac "(\<exists>T\<^isub>1 T\<^isub>2. b=T\<^isub>1 \<rightarrow> T\<^isub>2) \<or> b=TUnit \<or> b=TBase" )
       
   988 apply (force)
       
   989 apply (rule ty_cases)
       
   990 done
       
   991 
       
   992 termination
       
   993 apply(relation "measure (\<lambda>(_,_,_,T). size T)")
       
   994 apply(auto)
       
   995 done
       
   996 
       
   997 lemma log_equiv_valid: 
       
   998   assumes "\<Gamma> \<turnstile> s is t : T"
       
   999   shows "valid \<Gamma>"
   837 using assms 
  1000 using assms 
   838 by (nominal_induct t avoiding: a e rule: trm.induct)
  1001 by (induct rule: log_equiv.induct,auto elim: alg_equiv_valid)
   839    (auto simp add: fresh_atm abs_fresh fresh_nat) 
  1002 
       
  1003 text {* \subsubsection{Monotonicity of the logical equivalence relation} *}
       
  1004 
       
  1005 lemma logical_monotonicity :
       
  1006  fixes T::ty
       
  1007  assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma>\<lless>\<Gamma>'" 
       
  1008  shows "\<Gamma>' \<turnstile> s is t : T"
       
  1009 using assms
       
  1010 proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct)
       
  1011   case (2 \<Gamma> s t \<Gamma>')
       
  1012   then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto
       
  1013 next
       
  1014   case (3 \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
       
  1015   then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by force 
       
  1016 qed (auto)
       
  1017 
       
  1018 text {* If two terms are path equivalent then they are in normal form. *}
   840 
  1019 
   841 lemma path_equiv_implies_nf:
  1020 lemma path_equiv_implies_nf:
   842   assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
  1021   assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
   843   shows "s \<leadsto>|" and "t \<leadsto>|"
  1022   shows "s \<leadsto>|" and "t \<leadsto>|"
   844 using assms
  1023 using assms
   845 by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto)
  1024 by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto)
   846 
  1025 
   847 lemma path_equiv_implies_nf:
       
   848   shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> True"
       
   849     and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> s \<leadsto>|"
       
   850         "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> t \<leadsto>|"
       
   851 by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto)
       
   852 
       
   853 lemma main_lemma:
  1026 lemma main_lemma:
   854   shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T" and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T"
  1027   shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T" and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T"
   855 proof (nominal_induct T arbitrary: \<Gamma> s t p q rule:ty.induct)
  1028 proof (nominal_induct T arbitrary: \<Gamma> s t p q rule:ty.induct)
   856   case (Arrow T1 T2)
  1029   case (Arrow T\<^isub>1 T\<^isub>2)
   857   { 
  1030   { 
   858     case (1 \<Gamma> s t)
  1031     case (1 \<Gamma> s t)
   859     have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T2 \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T2" by fact
  1032     have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>2" by fact
   860     have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T1" by fact
  1033     have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^isub>1" by fact
   861     have h:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact
  1034     have h:"\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
   862     obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1])
  1035     obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1])
   863     have "valid \<Gamma>" using h log_equiv_valid by auto
  1036     have "valid \<Gamma>" using h log_equiv_valid by auto
   864     then have v:"valid ((x,T1)#\<Gamma>)" using fs by auto
  1037     then have v:"valid ((x,T\<^isub>1)#\<Gamma>)" using fs by auto
   865     then have "(x,T1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T1" by auto
  1038     then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T\<^isub>1" by auto
   866     then have "(x,T1)#\<Gamma> \<turnstile> Var x is Var x : T1" using ih2 by auto
  1039     then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x is Var x : T\<^isub>1" using ih2 by auto
   867     then have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T2" using h v by auto
  1040     then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T\<^isub>2" using h v by auto
   868     then have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" using ih1 by auto
  1041     then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" using ih1 by auto
   869     then show "\<Gamma> \<turnstile> s <=> t : T1\<rightarrow>T2" using fs by (auto simp add: fresh_prod)
  1042     then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
   870   next
  1043   next
   871     case (2 \<Gamma> p q)
  1044     case (2 \<Gamma> p q)
   872     have h:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2" by fact
  1045     have h:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
   873     have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T2" by fact
  1046     have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^isub>2" by fact
   874     have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T1 \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T1" by fact
  1047     have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" by fact
   875     {
  1048     {
   876       fix \<Gamma>' s t
  1049       fix \<Gamma>' s t
   877       assume "\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T1"
  1050       assume "\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^isub>1"
   878       then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T1 \<rightarrow> T2" using h algorithmic_monotonicity by auto
  1051       then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2" using h algorithmic_monotonicity by auto
   879       moreover have "\<Gamma>' \<turnstile> s <=> t : T1" using ih2 hl by auto
  1052       moreover have "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" using ih2 hl by auto
   880       ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T2" by auto
  1053       ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2" by auto
   881       then have "\<Gamma>' \<turnstile> App p s is App q t : T2" using ih1 by auto
  1054       then have "\<Gamma>' \<turnstile> App p s is App q t : T\<^isub>2" using ih1 by auto
   882     }
  1055     }
   883     moreover have "valid \<Gamma>" using h alg_equiv_valid by auto
  1056     moreover have "valid \<Gamma>" using h alg_equiv_valid by auto
   884     ultimately show "\<Gamma> \<turnstile> p is q : T1\<rightarrow>T2"  by auto
  1057     ultimately show "\<Gamma> \<turnstile> p is q : T\<^isub>1\<rightarrow>T\<^isub>2"  by auto
   885   }
  1058   }
   886 next
  1059 next
   887   case TBase
  1060   case TBase
   888   { case 2
  1061   { case 2
   889     have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact
  1062     have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact
   890     then have "s \<leadsto>|" and "t \<leadsto>|" using path_equiv_implies_nf by auto
  1063     then have "s \<leadsto>|" and "t \<leadsto>|" using path_equiv_implies_nf by auto
   891     then have "s \<Down> s" and "t \<Down> t" by auto
  1064     then have "s \<Down> s" and "t \<Down> t" by auto
   892     then have "\<Gamma> \<turnstile> s <=> t : TBase" using h by auto
  1065     then have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" using h by auto
   893     then show "\<Gamma> \<turnstile> s is t : TBase" by auto
  1066     then show "\<Gamma> \<turnstile> s is t : TBase" by auto
   894   }
  1067   }
   895 qed (auto elim:alg_equiv_valid)
  1068 qed (auto elim:alg_equiv_valid)
   896 
  1069 
   897 corollary corollary_main:
  1070 corollary corollary_main:
   898   assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
  1071   assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
   899   shows "\<Gamma> \<turnstile> s <=> t : T"
  1072   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
   900 using a main_lemma by blast
  1073 using a main_lemma by blast
   901 
  1074 
   902 lemma algorithmic_symmetry_aux:
  1075 lemma algorithmic_symmetry:
   903   shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> \<Gamma> \<turnstile> t <=> s : T" 
  1076   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T" 
   904   and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T"
  1077   and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T"
   905 by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto)
  1078 by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto)
   906 
       
   907 lemma algorithmic_symmetry:
       
   908   assumes a: "\<Gamma> \<turnstile> s <=> t : T"
       
   909   shows "\<Gamma> \<turnstile> t <=> s : T"
       
   910 using a by (simp add: algorithmic_symmetry_aux)
       
   911 
       
   912 lemma algorithmic_path_symmetry:
       
   913   assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
       
   914   shows "\<Gamma> \<turnstile> t \<leftrightarrow> s : T"
       
   915 using a by (simp add: algorithmic_symmetry_aux)
       
   916 
  1079 
   917 lemma red_unicity : 
  1080 lemma red_unicity : 
   918   assumes a: "x \<leadsto> a" 
  1081   assumes a: "x \<leadsto> a" 
   919   and     b: "x \<leadsto> b"
  1082   and     b: "x \<leadsto> b"
   920   shows "a=b"
  1083   shows "a=b"
   941   then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto
  1104   then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto
   942   then have "t=t'" using h red_unicity by auto
  1105   then have "t=t'" using h red_unicity by auto
   943   then show "a=b" using ih hl by auto
  1106   then show "a=b" using ih hl by auto
   944 qed (auto)
  1107 qed (auto)
   945 
  1108 
   946 lemma Q_eqvt :
  1109 nominal_inductive alg_equiv
   947   fixes pi:: "name prm"
  1110 
   948   shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : T"
       
   949   and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) \<leftrightarrow> (pi\<bullet>t) : T"
       
   950 using assms
       
   951 proof (induct rule:alg_equiv_alg_path_equiv.inducts)
       
   952   case (QAP_Var \<Gamma> x T)
       
   953   then have "pi\<bullet>(x,T) \<in> (pi\<bullet>(set \<Gamma>))" using in_eqvt by blast
       
   954   then have "(pi\<bullet>x,T) \<in> (set (pi\<bullet>\<Gamma>))" using set_eqvt perm_ty by auto
       
   955   moreover have "valid \<Gamma>" by fact
       
   956   ultimately show ?case using valid_eqvt by auto
       
   957 next
       
   958   case (QAT_Arrow x \<Gamma> s t T1 T2)
       
   959   then have h:"((pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>))" "((pi\<bullet>x)\<sharp>(pi\<bullet>s))" "((pi\<bullet>x)\<sharp>(pi\<bullet>t))"  using fresh_bij by auto
       
   960   have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> pi \<bullet> (App s (Var x)) <=> pi \<bullet> (App t (Var x)) : T2" by fact
       
   961   then have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" by auto
       
   962   moreover have "pi\<bullet>((x,T1)#\<Gamma>) = (pi\<bullet>x,pi\<bullet>T1)#(pi\<bullet>\<Gamma>)" by auto
       
   963   ultimately have "((pi\<bullet>x,T1)#(pi\<bullet>\<Gamma>))  \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" 
       
   964     using perm_ty by auto
       
   965   then show ?case using h by auto
       
   966 qed (auto elim:whn_eqvt valid_eqvt)
       
   967  
       
   968 (* FIXME this lemma should not be here I am reinventing the wheel I guess *)
  1111 (* FIXME this lemma should not be here I am reinventing the wheel I guess *)
   969 
  1112 (*<*)
   970 lemma perm_basic[simp]:
  1113 lemma perm_basic[simp]:
   971  fixes x y::"name"
  1114  fixes x y::"name"
   972 shows "[(x,y)]\<bullet>y = x"
  1115 shows "[(x,y)]\<bullet>y = x"
   973 using assms using calc_atm by perm_simp
  1116 using assms using calc_atm by perm_simp
       
  1117 (*>*)
       
  1118 
       
  1119 text{* \subsection{Strong inversion lemma for algorithmic equivalence} *}
   974 
  1120 
   975 lemma Q_Arrow_strong_inversion:
  1121 lemma Q_Arrow_strong_inversion:
   976   assumes fs:"x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" and h:"\<Gamma> \<turnstile> t <=> u : T1\<rightarrow>T2"
  1122   assumes fs:"x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" and h:"\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2"
   977   shows "(x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> App u (Var x) : T2"
  1123   shows "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2"
   978 proof -
  1124 proof -
   979   obtain y where  fs2:"y\<sharp>\<Gamma>" "y\<sharp>u" "y\<sharp>t" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" 
  1125   obtain y where  fs2:"y\<sharp>\<Gamma>" "y\<sharp>u" "y\<sharp>t" and "(y,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^isub>2" 
   980     using h by auto
  1126     using h by auto
   981   then have "([(x,y)]\<bullet>((y,T1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) <=> [(x,y)]\<bullet> App u (Var y) : T2" 
  1127   then have "([(x,y)]\<bullet>((y,T\<^isub>1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) \<Leftrightarrow> [(x,y)]\<bullet> App u (Var y) : T\<^isub>2" 
   982     using Q_eqvt by blast
  1128     using  alg_equiv_eqvt[simplified] by blast
   983   then show ?thesis using fs fs2 by (perm_simp)
  1129   then show ?thesis using fs fs2 by (perm_simp)
   984 qed
  1130 qed
   985 
  1131 
   986 lemma fresh_context: 
  1132 text{* 
   987   fixes  \<Gamma> :: "(name\<times>ty) list"
  1133 For the \texttt{algorithmic\_transitivity} lemma we need a unicity property.
   988   and    a :: "name"
  1134 But one has to be cautious, because this unicity property is true only for algorithmic path. 
   989   assumes "a\<sharp>\<Gamma>"
  1135 Indeed the following lemma is \textbf{false}:\\
   990   shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
  1136 \begin{center}
   991 using assms by(induct \<Gamma>, auto simp add: fresh_prod fresh_list_cons fresh_atm)
  1137 @{prop "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"}
   992 
  1138 \end{center}
   993 lemma type_unicity_in_context:
  1139 Here is the counter example :\\
   994   fixes  \<Gamma> :: "(name\<times>ty)list"
  1140 \begin{center}
   995   and    pi:: "name prm"
  1141 @{prop "\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase"} and @{prop "\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit"}
   996   and    a :: "name"
  1142 \end{center}
   997   and    \<tau> :: "ty"
  1143 *}
   998   assumes "valid \<Gamma>" and "(x,T1) \<in> set \<Gamma>" and "(x,T2) \<in> set \<Gamma>"
  1144 
   999   shows "T1=T2"
  1145 (*
  1000 using assms by (induct \<Gamma>, auto dest!: fresh_context)
       
  1001 
       
  1002 (* 
       
  1003 
       
  1004 Warning: This lemma is false.
       
  1005 
       
  1006 lemma algorithmic_type_unicity:
  1146 lemma algorithmic_type_unicity:
  1007   shows "\<lbrakk> \<Gamma> \<turnstile> s <=> t : T ; \<Gamma> \<turnstile> s <=> u : T' \<rbrakk> \<Longrightarrow> T = T'"
  1147   shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
  1008   and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
  1148   and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
  1009 
  1149 
  1010 Here is the counter example : 
  1150 Here is the counter example : 
  1011 \<Gamma> \<turnstile> Const n <=> Const n : Tbase and \<Gamma> \<turnstile> Const n <=> Const n : TUnit
  1151 \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase and \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit
  1012 
  1152 
  1013 *)
  1153 *)
  1014 
  1154 
  1015 lemma algorithmic_path_type_unicity:
  1155 lemma algorithmic_path_type_unicity:
  1016   shows "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
  1156   shows "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
  1020   have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact
  1160   have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact
  1021   then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto
  1161   then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto
  1022   moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact
  1162   moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact
  1023   ultimately show "T=T'" using type_unicity_in_context by auto
  1163   ultimately show "T=T'" using type_unicity_in_context by auto
  1024 next
  1164 next
  1025   case (QAP_App \<Gamma> p q T1 T2 s t u T2')
  1165   case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u T\<^isub>2')
  1026   have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T1\<rightarrow>T2 = T" by fact
  1166   have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
  1027   have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T2'" by fact
  1167   have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2'" by fact
  1028   then obtain r t T1' where "u = App r t"  "\<Gamma> \<turnstile> p \<leftrightarrow> r : T1' \<rightarrow> T2'" by auto
  1168   then obtain r t T\<^isub>1' where "u = App r t"  "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
  1029   then have "T1\<rightarrow>T2 = T1' \<rightarrow> T2'" by auto
  1169   then have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
  1030   then show "T2=T2'" using ty.inject by auto
  1170   then show "T\<^isub>2=T\<^isub>2'" using ty.inject by auto
  1031 qed (auto)
  1171 qed (auto)
  1032 
  1172 
  1033 lemma algorithmic_transitivity:
  1173 lemma algorithmic_transitivity:
  1034   shows "\<lbrakk> \<Gamma> \<turnstile> s <=> t : T ; \<Gamma> \<turnstile> t <=> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s <=> u : T"
  1174   shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<Leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T"
  1035   and  "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T"
  1175   and  "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T"
  1036 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv_strong_inducts)
  1176 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv_strong_inducts)
  1037   case (QAT_Base s p t q \<Gamma> u)
  1177   case (QAT_Base s p t q \<Gamma> u)
  1038   have h:"s \<Down> p" "t \<Down> q" by fact
  1178   have h:"s \<Down> p" "t \<Down> q" by fact
  1039   have ih:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : TBase" by fact
  1179   have ih:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : TBase" by fact
  1040   have "\<Gamma> \<turnstile> t <=> u : TBase" by fact
  1180   have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : TBase" by fact
  1041   then obtain r q' where hl:"t \<Down> q'" "u \<Down> r" "\<Gamma> \<turnstile> q' \<leftrightarrow> r : TBase" by auto
  1181   then obtain r q' where hl:"t \<Down> q'" "u \<Down> r" "\<Gamma> \<turnstile> q' \<leftrightarrow> r : TBase" by auto
  1042   moreover have eq:"q=q'" using nf_unicity hl h by auto
  1182   moreover have eq:"q=q'" using nf_unicity hl h by auto
  1043   ultimately have "\<Gamma> \<turnstile> p \<leftrightarrow> r : TBase" using ih by auto
  1183   ultimately have "\<Gamma> \<turnstile> p \<leftrightarrow> r : TBase" using ih by auto
  1044   then show "\<Gamma> \<turnstile> s <=> u : TBase" using hl h by auto
  1184   then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : TBase" using hl h by auto
  1045 next
  1185 next
  1046   case (QAT_Arrow  x \<Gamma> s t T1 T2 u)
  1186   case (QAT_Arrow  x \<Gamma> s t T\<^isub>1 T\<^isub>2 u)
  1047   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
  1187   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
  1048   moreover have h:"\<Gamma> \<turnstile> t <=> u : T1\<rightarrow>T2" by fact
  1188   moreover have h:"\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
  1049   moreover then obtain y where "y\<sharp>\<Gamma>" "y\<sharp>t" "y\<sharp>u" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" 
  1189   moreover then obtain y where "y\<sharp>\<Gamma>" "y\<sharp>t" "y\<sharp>u" and "(y,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^isub>2" 
  1050     by auto
  1190     by auto
  1051   moreover have fs2:"x\<sharp>u" by fact
  1191   moreover have fs2:"x\<sharp>u" by fact
  1052   ultimately have "(x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> App u (Var x) : T2" using Q_Arrow_strong_inversion by blast
  1192   ultimately have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" using Q_Arrow_strong_inversion by blast
  1053   moreover have ih:"\<And> v. (x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> v : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> v : T2" 
  1193   moreover have ih:"\<And> v. (x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> v : T\<^isub>2 \<Longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> v : T\<^isub>2" 
  1054     by fact
  1194     by fact
  1055   ultimately have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App u (Var x) : T2" by auto
  1195   ultimately have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by auto
  1056   then show "\<Gamma> \<turnstile> s <=> u : T1\<rightarrow>T2" using fs fs2 by auto
  1196   then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" using fs fs2 by auto
  1057 next
  1197 next
  1058   case (QAP_App \<Gamma> p q T1 T2 s t u)
  1198   case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u)
  1059   have h1:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2" by fact
  1199   have h1:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
  1060   have ih1:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : T1\<rightarrow>T2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : T1\<rightarrow>T2" by fact
  1200   have ih1:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
  1061   have "\<Gamma> \<turnstile> s <=> t : T1" by fact
  1201   have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" by fact
  1062   have ih2:"\<And>u. \<Gamma> \<turnstile> t <=> u : T1 \<Longrightarrow> \<Gamma> \<turnstile> s <=> u : T1" by fact
  1202   have ih2:"\<And>u. \<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1" by fact
  1063   have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T2" by fact
  1203   have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T\<^isub>2" by fact
  1064   then obtain r T1' v where ha:"\<Gamma> \<turnstile> q \<leftrightarrow> r : T1'\<rightarrow>T2" and hb:"\<Gamma> \<turnstile> t <=> v : T1'" and eq:"u = App r v" 
  1204   then obtain r T\<^isub>1' v where ha:"\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^isub>1'\<rightarrow>T\<^isub>2" and hb:"\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^isub>1'" and eq:"u = App r v" 
  1065     by auto
  1205     by auto
  1066   moreover have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T1\<rightarrow>T2" using h1 algorithmic_path_symmetry by auto
  1206   moreover have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T\<^isub>1\<rightarrow>T\<^isub>2" using h1 algorithmic_symmetry by auto
  1067   ultimately have "T1'\<rightarrow>T2 = T1\<rightarrow>T2" using algorithmic_path_type_unicity by auto
  1207   ultimately have "T\<^isub>1'\<rightarrow>T\<^isub>2 = T\<^isub>1\<rightarrow>T\<^isub>2" using algorithmic_path_type_unicity by auto
  1068   then have "T1' = T1" using ty.inject by auto
  1208   then have "T\<^isub>1' = T\<^isub>1" using ty.inject by auto
  1069   then have "\<Gamma> \<turnstile> s <=> v : T1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T1\<rightarrow>T2" using ih1 ih2 ha hb by auto
  1209   then have "\<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^isub>1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1\<rightarrow>T\<^isub>2" using ih1 ih2 ha hb by auto
  1070   then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T2" using eq by auto
  1210   then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2" using eq by auto
  1071 qed (auto)
  1211 qed (auto)
  1072 
  1212 
  1073 lemma algorithmic_weak_head_closure:
  1213 lemma algorithmic_weak_head_closure:
  1074   shows "\<lbrakk>\<Gamma> \<turnstile> s <=> t : T ; s' \<leadsto> s; t' \<leadsto> t\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' <=> t' : T"
  1214   shows "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; s' \<leadsto> s; t' \<leadsto> t\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' \<Leftrightarrow> t' : T"
  1075 by (nominal_induct \<Gamma> s t T avoiding: s' t'  
  1215 by (nominal_induct \<Gamma> s t T avoiding: s' t'  
  1076     rule: alg_equiv_alg_path_equiv_strong_inducts(1) [of _ _ _ _ "%a b c d e. True"])
  1216     rule: alg_equiv_alg_path_equiv_strong_inducts(1) [of _ _ _ _ "%a b c d e. True"])
  1077    (auto)
  1217    (auto)
  1078 
  1218 
  1079 lemma logical_symmetry:
  1219 lemma logical_symmetry:
  1088 using assms
  1228 using assms
  1089 proof (nominal_induct arbitrary: \<Gamma> s t u  rule:ty.induct)
  1229 proof (nominal_induct arbitrary: \<Gamma> s t u  rule:ty.induct)
  1090   case TBase
  1230   case TBase
  1091   then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim:  algorithmic_transitivity)
  1231   then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim:  algorithmic_transitivity)
  1092 next 
  1232 next 
  1093   case (Arrow T1 T2 \<Gamma> s t u)
  1233   case (Arrow T\<^isub>1 T\<^isub>2 \<Gamma> s t u)
  1094   have h1:"\<Gamma> \<turnstile> s is t : T1 \<rightarrow> T2" by fact
  1234   have h1:"\<Gamma> \<turnstile> s is t : T\<^isub>1 \<rightarrow> T\<^isub>2" by fact
  1095   have h2:"\<Gamma> \<turnstile> t is u : T1 \<rightarrow> T2" by fact
  1235   have h2:"\<Gamma> \<turnstile> t is u : T\<^isub>1 \<rightarrow> T\<^isub>2" by fact
  1096   have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T1; \<Gamma> \<turnstile> t is u : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T1" by fact
  1236   have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>1; \<Gamma> \<turnstile> t is u : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^isub>1" by fact
  1097   have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T2; \<Gamma> \<turnstile> t is u : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T2" by fact
  1237   have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>2; \<Gamma> \<turnstile> t is u : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^isub>2" by fact
  1098   {
  1238   {
  1099     fix \<Gamma>' s' u'
  1239     fix \<Gamma>' s' u'
  1100     assume hsub:"\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T1"
  1240     assume hsub:"\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^isub>1"
  1101     then have "\<Gamma>' \<turnstile> u' is s' : T1" using logical_symmetry by blast
  1241     then have "\<Gamma>' \<turnstile> u' is s' : T\<^isub>1" using logical_symmetry by blast
  1102     then have "\<Gamma>' \<turnstile> u' is u' : T1" using ih1 hl by blast
  1242     then have "\<Gamma>' \<turnstile> u' is u' : T\<^isub>1" using ih1 hl by blast
  1103     then have "\<Gamma>' \<turnstile> App t u' is App u u' : T2" using h2 hsub by auto
  1243     then have "\<Gamma>' \<turnstile> App t u' is App u u' : T\<^isub>2" using h2 hsub by auto
  1104     moreover have "\<Gamma>' \<turnstile>  App s s' is App t u' : T2" using h1 hsub hl by auto
  1244     moreover have "\<Gamma>' \<turnstile>  App s s' is App t u' : T\<^isub>2" using h1 hsub hl by auto
  1105     ultimately have "\<Gamma>' \<turnstile>  App s s' is App u u' : T2" using ih2 by blast
  1245     ultimately have "\<Gamma>' \<turnstile>  App s s' is App u u' : T\<^isub>2" using ih2 by blast
  1106   }
  1246   }
  1107   moreover have "valid \<Gamma>" using h1 alg_equiv_valid by auto
  1247   moreover have "valid \<Gamma>" using h1 alg_equiv_valid by auto
  1108   ultimately show "\<Gamma> \<turnstile> s is u : T1 \<rightarrow> T2" by auto
  1248   ultimately show "\<Gamma> \<turnstile> s is u : T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
  1109 qed (auto)
  1249 qed (auto)
  1110 
  1250 
  1111 lemma logical_weak_head_closure:
  1251 lemma logical_weak_head_closure:
  1112   assumes a: "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" "t' \<leadsto> t"
  1252   assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" "t' \<leadsto> t"
  1113   shows "\<Gamma> \<turnstile> s' is t' : T"
  1253   shows "\<Gamma> \<turnstile> s' is t' : T"
  1114 using a
  1254 using assms algorithmic_weak_head_closure 
  1115 apply(nominal_induct arbitrary: \<Gamma> s t s' t' rule:ty.induct)
  1255 by (nominal_induct arbitrary: \<Gamma> s t s' t' rule:ty.induct) (auto, blast)
  1116 apply(auto simp add: algorithmic_weak_head_closure)
       
  1117 apply(blast)
       
  1118 done
       
  1119 
  1256 
  1120 lemma logical_weak_head_closure':
  1257 lemma logical_weak_head_closure':
  1121   assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" 
  1258   assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" 
  1122   shows "\<Gamma> \<turnstile> s' is t : T"
  1259   shows "\<Gamma> \<turnstile> s' is t : T"
  1123 using assms
  1260 using assms
  1125   case (TBase  \<Gamma> s t s')
  1262   case (TBase  \<Gamma> s t s')
  1126   then show ?case by force
  1263   then show ?case by force
  1127 next
  1264 next
  1128   case (TUnit \<Gamma> s t s')
  1265   case (TUnit \<Gamma> s t s')
  1129   then show ?case by auto
  1266   then show ?case by auto
  1130 next
  1267 next 
  1131   case (Arrow T1 T2 \<Gamma> s t s')
  1268   case (Arrow T\<^isub>1 T\<^isub>2 \<Gamma> s t s')
  1132   have h1:"s' \<leadsto> s" by fact
  1269   have h1:"s' \<leadsto> s" by fact
  1133   have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T2" by fact
  1270   have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T\<^isub>2" by fact
  1134   have h2:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact
  1271   have h2:"\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
  1135   then have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T2)" by auto
  1272   then have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2)" by auto
  1136   {
  1273   {
  1137     fix \<Gamma>' s2 t2
  1274     fix \<Gamma>' s\<^isub>2 t\<^isub>2
  1138     assume "\<Gamma>\<lless>\<Gamma>'" and "\<Gamma>' \<turnstile> s2 is t2 : T1"
  1275     assume "\<Gamma>\<lless>\<Gamma>'" and "\<Gamma>' \<turnstile> s\<^isub>2 is t\<^isub>2 : T\<^isub>1"
  1139     then have "\<Gamma>' \<turnstile> (App s s2) is (App t t2) : T2" using hb by auto
  1276     then have "\<Gamma>' \<turnstile> (App s s\<^isub>2) is (App t t\<^isub>2) : T\<^isub>2" using hb by auto
  1140     moreover have "(App s' s2)  \<leadsto> (App s s2)" using h1 by auto  
  1277     moreover have "(App s' s\<^isub>2)  \<leadsto> (App s s\<^isub>2)" using h1 by auto  
  1141     ultimately have "\<Gamma>' \<turnstile> App s' s2 is App t t2 : T2" using ih by auto
  1278     ultimately have "\<Gamma>' \<turnstile> App s' s\<^isub>2 is App t t\<^isub>2 : T\<^isub>2" using ih by auto
  1142   }
  1279   }
  1143   moreover have "valid \<Gamma>" using h2 log_equiv_valid by auto
  1280   moreover have "valid \<Gamma>" using h2 log_equiv_valid by auto
  1144   ultimately show "\<Gamma> \<turnstile> s' is t : T1\<rightarrow>T2" by auto
  1281   ultimately show "\<Gamma> \<turnstile> s' is t : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
  1145 qed
  1282 qed 
  1146 
  1283 
  1147 abbreviation 
  1284 abbreviation 
  1148  log_equiv_subst :: "(name\<times>ty) list \<Rightarrow> (name\<times>trm) list \<Rightarrow>  (name\<times>trm) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool"  
  1285  log_equiv_subst :: "(name\<times>ty) list \<Rightarrow> (name\<times>trm) list \<Rightarrow>  (name\<times>trm) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool"  
  1149                      ("_ \<turnstile> _ is _ over _" [60,60] 60) 
  1286                      ("_ \<turnstile> _ is _ over _" [60,60] 60) 
  1150 where
  1287 where
  1198 theorem fundamental_theorem:
  1335 theorem fundamental_theorem:
  1199   assumes "\<Gamma> \<turnstile> t : T" "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>"
  1336   assumes "\<Gamma> \<turnstile> t : T" "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>"
  1200   shows "\<Gamma>' \<turnstile> \<gamma><t> is \<theta><t> : T"   
  1337   shows "\<Gamma>' \<turnstile> \<gamma><t> is \<theta><t> : T"   
  1201 using assms
  1338 using assms
  1202 proof (nominal_induct avoiding:\<Gamma>' \<gamma> \<theta>  rule: typing_induct_strong)
  1339 proof (nominal_induct avoiding:\<Gamma>' \<gamma> \<theta>  rule: typing_induct_strong)
  1203 case (t_Lam x \<Gamma> T1 t2 T2 \<Gamma>' \<gamma> \<theta>)
  1340 case (t_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Gamma>' \<gamma> \<theta>)
  1204 have fs:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" "x\<sharp>\<Gamma>" by fact
  1341 have fs:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" "x\<sharp>\<Gamma>" by fact
  1205 have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
  1342 have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
  1206 have ih:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t2> is \<theta><t2> : T2" by fact
  1343 have ih:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T\<^isub>1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t\<^isub>2> is \<theta><t\<^isub>2> : T\<^isub>2" by fact
  1207 {
  1344 {
  1208   fix \<Gamma>'' s' t'
  1345   fix \<Gamma>'' s' t'
  1209   assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1"
  1346   assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1"
  1210   then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using logical_subst_monotonicity h by blast
  1347   then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using logical_subst_monotonicity h by blast
  1211   then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast
  1348   then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
  1212   then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><t2> is (x,t')#\<theta><t2> : T2" using ih by auto
  1349   then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><t\<^isub>2> is (x,t')#\<theta><t\<^isub>2> : T\<^isub>2" using ih by auto
  1213   then have "\<Gamma>''\<turnstile>\<gamma><t2>[x::=s'] is \<theta><t2>[x::=t'] : T2" using psubst_subst_psubst fs by simp
  1350   then have "\<Gamma>''\<turnstile>\<gamma><t\<^isub>2>[x::=s'] is \<theta><t\<^isub>2>[x::=t'] : T\<^isub>2" using psubst_subst_psubst fs by simp
  1214   moreover have "App (Lam [x].\<gamma><t2>) s' \<leadsto> \<gamma><t2>[x::=s']" by auto
  1351   moreover have "App (Lam [x].\<gamma><t\<^isub>2>) s' \<leadsto> \<gamma><t\<^isub>2>[x::=s']" by auto
  1215   moreover have "App (Lam [x].\<theta><t2>) t' \<leadsto> \<theta><t2>[x::=t']" by auto
  1352   moreover have "App (Lam [x].\<theta><t\<^isub>2>) t' \<leadsto> \<theta><t\<^isub>2>[x::=t']" by auto
  1216   ultimately have "\<Gamma>''\<turnstile> App (Lam [x].\<gamma><t2>) s' is App (Lam [x].\<theta><t2>) t' : T2" 
  1353   ultimately have "\<Gamma>''\<turnstile> App (Lam [x].\<gamma><t\<^isub>2>) s' is App (Lam [x].\<theta><t\<^isub>2>) t' : T\<^isub>2" 
  1217     using logical_weak_head_closure by auto
  1354     using logical_weak_head_closure by auto
  1218 }
  1355 }
  1219 moreover have "valid \<Gamma>'" using h by auto
  1356 moreover have "valid \<Gamma>'" using h by auto
  1220 ultimately show "\<Gamma>' \<turnstile> \<gamma><Lam [x].t2> is \<theta><Lam [x].t2> : T1\<rightarrow>T2" using fs by auto 
  1357 ultimately show "\<Gamma>' \<turnstile> \<gamma><Lam [x].t\<^isub>2> is \<theta><Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by auto 
  1221 qed (auto)
  1358 qed (auto)
  1222 
  1359 
  1223 theorem fundamental_theorem_2:
  1360 theorem fundamental_theorem_2:
  1224   assumes h1: "\<Gamma> \<turnstile> s == t : T" 
  1361   assumes h1: "\<Gamma> \<turnstile> s \<equiv> t : T" 
  1225   and     h2: "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>"
  1362   and     h2: "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>"
  1226   shows "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T"
  1363   shows "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T"
  1227 using h1 h2
  1364 using h1 h2
  1228 proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<gamma> \<theta> rule: equiv_def_strong_induct)
  1365 proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<gamma> \<theta> rule: equiv_def_strong_induct)
  1229   case (Q_Refl \<Gamma> t T \<Gamma>' \<gamma> \<theta>)
  1366   case (Q_Refl \<Gamma> t T \<Gamma>' \<gamma> \<theta>)
  1243   then have "\<Gamma>' \<turnstile> \<theta> is \<theta> over \<Gamma>" using logical_pseudo_reflexivity by auto
  1380   then have "\<Gamma>' \<turnstile> \<theta> is \<theta> over \<Gamma>" using logical_pseudo_reflexivity by auto
  1244   then have "\<Gamma>' \<turnstile> \<theta><t> is \<theta><u> : T" using ih2 by auto
  1381   then have "\<Gamma>' \<turnstile> \<theta><t> is \<theta><u> : T" using ih2 by auto
  1245   moreover have "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" using ih1 h by auto
  1382   moreover have "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" using ih1 h by auto
  1246   ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><u> : T" using logical_transitivity by blast
  1383   ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><u> : T" using logical_transitivity by blast
  1247 next
  1384 next
  1248   case (Q_Abs x \<Gamma> T1 s2 t2 T2 \<Gamma>' \<gamma> \<theta>)
  1385   case (Q_Abs x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 \<Gamma>' \<gamma> \<theta>)
  1249   have fs:"x\<sharp>\<Gamma>" by fact
  1386   have fs:"x\<sharp>\<Gamma>" by fact
  1250   have fs2: "x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact 
  1387   have fs2: "x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact 
  1251   have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
  1388   have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
  1252   have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T2" by fact
  1389   have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T\<^isub>1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s\<^isub>2> is \<theta><t\<^isub>2> : T\<^isub>2" by fact
  1253   {
  1390   {
  1254     fix \<Gamma>'' s' t'
  1391     fix \<Gamma>'' s' t'
  1255     assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1"
  1392     assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1"
  1256     then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast
  1393     then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast
  1257     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast
  1394     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
  1258     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><s2> is (x,t')#\<theta><t2> : T2" using ih by blast
  1395     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><s\<^isub>2> is (x,t')#\<theta><t\<^isub>2> : T\<^isub>2" using ih by blast
  1259     then have "\<Gamma>''\<turnstile> \<gamma><s2>[x::=s'] is \<theta><t2>[x::=t'] : T2" using fs2 psubst_subst_psubst by auto
  1396     then have "\<Gamma>''\<turnstile> \<gamma><s\<^isub>2>[x::=s'] is \<theta><t\<^isub>2>[x::=t'] : T\<^isub>2" using fs2 psubst_subst_psubst by auto
  1260     moreover have "App (Lam [x]. \<gamma><s2>) s' \<leadsto>  \<gamma><s2>[x::=s']" 
  1397     moreover have "App (Lam [x]. \<gamma><s\<^isub>2>) s' \<leadsto>  \<gamma><s\<^isub>2>[x::=s']" 
  1261               and "App (Lam [x].\<theta><t2>) t' \<leadsto> \<theta><t2>[x::=t']" by auto
  1398               and "App (Lam [x].\<theta><t\<^isub>2>) t' \<leadsto> \<theta><t\<^isub>2>[x::=t']" by auto
  1262     ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<gamma><s2>) s' is App (Lam [x].\<theta><t2>) t' : T2" 
  1399     ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<gamma><s\<^isub>2>) s' is App (Lam [x].\<theta><t\<^isub>2>) t' : T\<^isub>2" 
  1263       using logical_weak_head_closure by auto
  1400       using logical_weak_head_closure by auto
  1264   }
  1401   }
  1265   moreover have "valid \<Gamma>'" using h2 by auto
  1402   moreover have "valid \<Gamma>'" using h2 by auto
  1266   ultimately have "\<Gamma>' \<turnstile> Lam [x].\<gamma><s2> is Lam [x].\<theta><t2> : T1\<rightarrow>T2" by auto
  1403   ultimately have "\<Gamma>' \<turnstile> Lam [x].\<gamma><s\<^isub>2> is Lam [x].\<theta><t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
  1267   then show "\<Gamma>' \<turnstile> \<gamma><Lam [x].s2> is \<theta><Lam [x].t2> : T1\<rightarrow>T2" using fs2 by auto
  1404   then show "\<Gamma>' \<turnstile> \<gamma><Lam [x].s\<^isub>2> is \<theta><Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs2 by auto
  1268 next
  1405 next
  1269   case (Q_App \<Gamma> s1 t1 T1 T2 s2 t2 \<Gamma>' \<gamma> \<theta>)
  1406   case (Q_App \<Gamma> s\<^isub>1 t\<^isub>1 T\<^isub>1 T\<^isub>2 s\<^isub>2 t\<^isub>2 \<Gamma>' \<gamma> \<theta>)
  1270   then show "\<Gamma>' \<turnstile> \<gamma><App s1 s2> is \<theta><App t1 t2> : T2" by auto 
  1407   then show "\<Gamma>' \<turnstile> \<gamma><App s\<^isub>1 s\<^isub>2> is \<theta><App t\<^isub>1 t\<^isub>2> : T\<^isub>2" by auto 
  1271 next
  1408 next
  1272   case (Q_Beta x \<Gamma> T1 s12 t12 T2 s2 t2 \<Gamma>' \<gamma> \<theta>)
  1409   case (Q_Beta x \<Gamma> T\<^isub>1 s12 t12 T\<^isub>2 s\<^isub>2 t\<^isub>2 \<Gamma>' \<gamma> \<theta>)
  1273   have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
  1410   have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
  1274   have fs:"x\<sharp>\<Gamma>" by fact
  1411   have fs:"x\<sharp>\<Gamma>" by fact
  1275   have fs2:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact 
  1412   have fs2:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact 
  1276   have ih1:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T1" by fact
  1413   have ih1:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s\<^isub>2> is \<theta><t\<^isub>2> : T\<^isub>1" by fact
  1277   have ih2:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s12> is \<theta><t12> : T2" by fact
  1414   have ih2:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T\<^isub>1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s12> is \<theta><t12> : T\<^isub>2" by fact
  1278   have "\<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T1" using ih1 h by auto
  1415   have "\<Gamma>' \<turnstile> \<gamma><s\<^isub>2> is \<theta><t\<^isub>2> : T\<^isub>1" using ih1 h by auto
  1279   then have "\<Gamma>' \<turnstile> (x,\<gamma><s2>)#\<gamma> is (x,\<theta><t2>)#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext h fs by blast
  1416   then have "\<Gamma>' \<turnstile> (x,\<gamma><s\<^isub>2>)#\<gamma> is (x,\<theta><t\<^isub>2>)#\<theta> over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext h fs by blast
  1280   then have "\<Gamma>' \<turnstile> (x,\<gamma><s2>)#\<gamma><s12> is (x,\<theta><t2>)#\<theta><t12> : T2" using ih2 by auto
  1417   then have "\<Gamma>' \<turnstile> (x,\<gamma><s\<^isub>2>)#\<gamma><s12> is (x,\<theta><t\<^isub>2>)#\<theta><t12> : T\<^isub>2" using ih2 by auto
  1281   then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><s2>] is \<theta><t12>[x::=\<theta><t2>] : T2" using fs2 psubst_subst_psubst by auto
  1418   then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><s\<^isub>2>] is \<theta><t12>[x::=\<theta><t\<^isub>2>] : T\<^isub>2" using fs2 psubst_subst_psubst by auto
  1282   then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><s2>] is \<theta><t12[x::=t2]> : T2" using fs2 psubst_subst_propagate by auto
  1419   then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><s\<^isub>2>] is \<theta><t12[x::=t\<^isub>2]> : T\<^isub>2" using fs2 psubst_subst_propagate by auto
  1283   moreover have "App (Lam [x].\<gamma><s12>) (\<gamma><s2>) \<leadsto> \<gamma><s12>[x::=\<gamma><s2>]" by auto 
  1420   moreover have "App (Lam [x].\<gamma><s12>) (\<gamma><s\<^isub>2>) \<leadsto> \<gamma><s12>[x::=\<gamma><s\<^isub>2>]" by auto 
  1284   ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<gamma><s12>) (\<gamma><s2>) is \<theta><t12[x::=t2]> : T2" 
  1421   ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<gamma><s12>) (\<gamma><s\<^isub>2>) is \<theta><t12[x::=t\<^isub>2]> : T\<^isub>2" 
  1285     using logical_weak_head_closure' by auto
  1422     using logical_weak_head_closure' by auto
  1286   then show "\<Gamma>' \<turnstile> \<gamma><App (Lam [x].s12) s2> is \<theta><t12[x::=t2]> : T2" using fs2 by simp
  1423   then show "\<Gamma>' \<turnstile> \<gamma><App (Lam [x].s12) s\<^isub>2> is \<theta><t12[x::=t\<^isub>2]> : T\<^isub>2" using fs2 by simp
  1287 next
  1424 next
  1288   case (Q_Ext x \<Gamma> s t T1 T2 \<Gamma>' \<gamma> \<theta>)
  1425   case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>' \<gamma> \<theta>)
  1289   have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
  1426   have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
  1290   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
  1427   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
  1291   have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><App s (Var x)> is \<theta><App t (Var x)> : T2" 
  1428   have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T\<^isub>1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><App s (Var x)> is \<theta><App t (Var x)> : T\<^isub>2" 
  1292     by fact
  1429     by fact
  1293    {
  1430    {
  1294     fix \<Gamma>'' s' t'
  1431     fix \<Gamma>'' s' t'
  1295     assume hsub:"\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1"
  1432     assume hsub:"\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1"
  1296     then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast
  1433     then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast
  1297     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast
  1434     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
  1298     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><App s (Var x)>  is (x,t')#\<theta><App t (Var x)> : T2" using ih by blast
  1435     then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><App s (Var x)>  is (x,t')#\<theta><App t (Var x)> : T\<^isub>2" using ih by blast
  1299     then have "\<Gamma>'' \<turnstile> App (((x,s')#\<gamma>)<s>) (((x,s')#\<gamma>)<(Var x)>) is App ((x,t')#\<theta><t>) ((x,t')#\<theta><(Var x)>) : T2"
  1436     then have "\<Gamma>'' \<turnstile> App (((x,s')#\<gamma>)<s>) (((x,s')#\<gamma>)<(Var x)>) is App ((x,t')#\<theta><t>) ((x,t')#\<theta><(Var x)>) : T\<^isub>2"
  1300       by auto
  1437       by auto
  1301     then have "\<Gamma>'' \<turnstile> App ((x,s')#\<gamma><s>) s'  is App ((x,t')#\<theta><t>) t' : T2" by auto
  1438     then have "\<Gamma>'' \<turnstile> App ((x,s')#\<gamma><s>) s'  is App ((x,t')#\<theta><t>) t' : T\<^isub>2" by auto
  1302     then have "\<Gamma>'' \<turnstile> App (\<gamma><s>) s' is App (\<theta><t>) t' : T2" using fs fresh_psubst_simpl by auto
  1439     then have "\<Gamma>'' \<turnstile> App (\<gamma><s>) s' is App (\<theta><t>) t' : T\<^isub>2" using fs fresh_psubst_simpl by auto
  1303   }
  1440   }
  1304   moreover have "valid \<Gamma>'" using h2 by auto
  1441   moreover have "valid \<Gamma>'" using h2 by auto
  1305   ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T1\<rightarrow>T2" by auto
  1442   ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
  1306 qed
  1443 qed
  1307 
  1444 
       
  1445 
  1308 theorem completeness:
  1446 theorem completeness:
  1309   assumes "\<Gamma> \<turnstile> s == t : T"
  1447   assumes "\<Gamma> \<turnstile> s \<equiv> t : T"
  1310   shows "\<Gamma> \<turnstile> s <=> t : T"
  1448   shows   "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
  1311 using assms
  1449 using assms
  1312 proof -
  1450 proof -
  1313   {
  1451   {
  1314     fix x T
  1452     fix x T
  1315     assume "(x,T) \<in> set \<Gamma>" "valid \<Gamma>"
  1453     assume "(x,T) \<in> set \<Gamma>" "valid \<Gamma>"
  1317   }
  1455   }
  1318   moreover have "valid \<Gamma>" using equiv_def_valid assms by auto
  1456   moreover have "valid \<Gamma>" using equiv_def_valid assms by auto
  1319   ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto 
  1457   ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto 
  1320   then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 assms by blast
  1458   then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 assms by blast
  1321   then have "\<Gamma> \<turnstile> s is t : T" by simp
  1459   then have "\<Gamma> \<turnstile> s is t : T" by simp
  1322   then show  "\<Gamma> \<turnstile> s <=> t : T" using main_lemma by simp
  1460   then show  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma by simp
  1323 qed
  1461 qed
  1324 
  1462 
  1325 (* Soundness is left as an exercise - like in the book - for the avid formalist 
  1463 text{*
  1326 
  1464 \section{About soundness}
  1327 theorem soundness:
  1465 *}
  1328   shows "\<lbrakk>\<Gamma> \<turnstile> s <=> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T"
  1466 
  1329   and   "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T"
  1467 text {* We leave soundness as an exercise - like in the book :-) \\ 
  1330 
  1468  @{prop[mode=IfThen] "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} \\
  1331 *)
  1469  @{prop "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} 
       
  1470 *}
  1332 
  1471 
  1333 end
  1472 end
  1334 
  1473