author  narboux 
Tue, 06 Mar 2007 16:40:32 +0100  
changeset 22421  51a18dd1ea86 
parent 22418  49e2d9744ae1 
child 22492  43545e640877 
permissions  rwrr 
22073  1 
(* "$Id$" *) 
2 
(* *) 

22082  3 
(* Formalisation of the chapter on Logical Relations *) 
4 
(* and a Case Study in Equivalence Checking *) 

5 
(* by Karl Crary from the book on Advanced Topics in *) 

6 
(* Types and Programming Languages, MIT Press 2005 *) 

7 

8 
(* The formalisation was done by Julien Narboux and *) 

9 
(* Christian Urban *) 

22073  10 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

11 
(*<*) 
22073  12 
theory Crary 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

13 
imports "../Nominal" 
22073  14 
begin 
15 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

16 
(* We put this def here because of some incompatibility of LatexSugar and Nominal *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

17 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

18 
syntax (Rule output) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

19 
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

20 
("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

21 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

22 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

23 
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

24 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

25 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

26 
("\<^raw:\mbox{>_\<^raw:}\\>/ _") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

27 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

28 
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

29 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

30 
syntax (IfThen output) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

31 
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

32 
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

33 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 
22421  34 
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

35 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

36 
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

37 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

38 
syntax (IfThenNoBox output) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

39 
"==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

40 
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

41 
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

42 
("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

43 
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

44 
"_asm" :: "prop \<Rightarrow> asms" ("_") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

45 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

46 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

47 
(*>*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

48 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

49 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

50 
\section{Definition of the language} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

51 
\subsection{Definition of the terms and types} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

52 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

53 
First we define the type of atom names which will be used for binders. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

54 
Each atom type is infinitely many atoms and equality is decidable. *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

55 

22073  56 
atom_decl name 
57 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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. *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

59 

22073  60 
nominal_datatype ty = TBase 
61 
 TUnit 

62 
 Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) 

63 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

64 
text {* The datatype of terms contains a binder. The notation @{text "\<guillemotleft>name\<guillemotright> trm"} means that the name is bound inside trm. *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

65 

22073  66 
nominal_datatype trm = Unit 
67 
 Var "name" 

68 
 Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) 

69 
 App "trm" "trm" 

70 
 Const "nat" 

71 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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. *} 
22073  73 

74 
lemma perm_ty[simp]: 

75 
fixes T::"ty" 

76 
and pi::"name prm" 

77 
shows "pi\<bullet>T = T" 

78 
by (induct T rule: ty.induct_weak) (simp_all) 

79 

80 
lemma fresh_ty[simp]: 

81 
fixes x::"name" 

82 
and T::"ty" 

83 
shows "x\<sharp>T" 

84 
by (simp add: fresh_def supp_def) 

85 

86 
lemma ty_cases: 

87 
fixes T::ty 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

88 
shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase" 
22082  89 
by (induct T rule:ty.induct_weak) (auto) 
22073  90 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

91 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

92 
\subsection{Size functions} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

93 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

94 
We define size functions for types and terms. As Isabelle allows overloading we can use the same notation for both functions. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

95 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

97 
*} 
22073  98 

99 
instance ty :: size .. 

100 

101 
nominal_primrec 

102 
"size (TBase) = 1" 

103 
"size (TUnit) = 1" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

104 
"size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2" 
22073  105 
by (rule TrueI)+ 
106 

107 
instance trm :: size .. 

108 

109 
nominal_primrec 

110 
"size (Unit) = 1" 

111 
"size (Var x) = 1" 

112 
"size (Lam [x].t) = size t + 1" 

113 
"size (App t1 t2) = size t1 + size t2" 

114 
"size (Const n) = 1" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

115 
apply(finite_guess)+ 
22073  116 
apply(rule TrueI)+ 
117 
apply(simp add: fresh_nat)+ 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

118 
apply(fresh_guess)+ 
22073  119 
done 
120 

121 
lemma ty_size_greater_zero[simp]: 

122 
fixes T::"ty" 

123 
shows "size T > 0" 

124 
by (nominal_induct rule:ty.induct) (simp_all) 

125 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

126 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

127 
\subsection{Typing} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

128 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

129 
\subsubsection{Typing contexts} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

130 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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. 
22073  132 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

133 
\paragraph{Definition of the Validity of contexts}\strut\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

134 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

135 
First we define what valid contexts are. Informally a context is valid is it does not contains twice the same variable. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

136 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

137 
We use the following two inference rules: *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

138 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

139 
(*<*) 
22073  140 
inductive2 
141 
valid :: "(name \<times> 'a::pt_name) list \<Rightarrow> bool" 

142 
where 

22082  143 
v_nil[intro]: "valid []" 
22073  144 
 v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

145 
(*>*) 
22073  146 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

147 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

148 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

149 
\isastyle 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

150 
@{thm[mode=Rule] v_nil[no_vars]}{\sc{v\_nil}} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

151 
\qquad 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

152 
@{thm[mode=Rule] v_cons[no_vars]}{\sc{v\_cons}} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

153 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

154 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

155 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

156 
text{* We generate the equivariance lemma for the relation \texttt{valid}. *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

157 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

158 
nominal_inductive valid 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

159 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

160 
text{* We obtain a lemma called \texttt{valid\_eqvt}: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

161 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

162 
@{thm[mode=IfThen] valid_eqvt} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

163 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

164 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

165 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

166 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

168 
*} 
22073  169 

170 
inductive_cases2 

171 
valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)" 

172 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

173 
text{* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

174 
The generated theorem is the following: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

175 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

176 
@{thm "valid_cons_elim_auto"[no_vars] } 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

177 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

178 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

179 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

180 
text{* \paragraph{Lemmas about valid contexts} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

181 
Now, we can prove two useful lemmas about valid contexts. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

182 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

183 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

184 
lemma fresh_context: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

185 
fixes \<Gamma> :: "(name\<times>ty) list" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

186 
and a :: "name" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

187 
assumes "a\<sharp>\<Gamma>" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

188 
shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

189 
using assms by (induct \<Gamma>, auto simp add: fresh_prod fresh_list_cons fresh_atm) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

190 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

191 
lemma type_unicity_in_context: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

192 
fixes \<Gamma> :: "(name\<times>ty)list" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

193 
and pi:: "name prm" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

194 
and a :: "name" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

195 
and \<tau> :: "ty" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

196 
assumes "valid \<Gamma>" and "(x,T\<^isub>1) \<in> set \<Gamma>" and "(x,T\<^isub>2) \<in> set \<Gamma>" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

197 
shows "T\<^isub>1=T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

198 
using assms by (induct \<Gamma>, auto dest!: fresh_context) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

199 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

200 
text {* \paragraph{Definition of subcontexts} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

201 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

203 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

204 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

205 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

206 
abbreviation 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

207 
"sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [55,55] 55) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

208 
where 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

210 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

211 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

212 
\subsubsection{Definition of the typing relation} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

213 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

214 
Now, we can define the typing judgements for terms. The rules are given in figure~\ref{typing}. *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

215 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

216 
(*<*) 
22073  217 

218 
inductive2 

219 
typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 

220 
where 

221 
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
22073  224 
 t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase" 
225 
 t_Unit[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

226 
(*>*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

227 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

228 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

229 
\begin{figure} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

230 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

231 
\isastyle %smaller fonts 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

232 
@{thm[mode=Rule] t_Var[no_vars]}{\sc{t\_Var}}\qquad 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

233 
@{thm[mode=Rule] t_App[no_vars]}{\sc{t\_App}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

234 
@{thm[mode=Rule] t_Lam[no_vars]}{\sc{t\_Lam}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

235 
@{thm[mode=Rule] t_Const[no_vars]}{\sc{t\_Const}} \qquad 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

236 
@{thm[mode=Rule] t_Unit[no_vars]}{\sc{t\_Unit}} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

237 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

238 
\caption{Typing rules\label{typing}} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

239 
\end{figure} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

240 
*} 
22073  241 

242 
lemma typing_valid: 

243 
assumes "\<Gamma> \<turnstile> t : T" 

244 
shows "valid \<Gamma>" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

245 
using assms by (induct)(auto) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

246 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

247 
nominal_inductive typing 
22073  248 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

249 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

250 
\subsubsection{Inversion lemmas for the typing relation} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

251 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

252 
We generate some inversion lemmas for 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

253 
the typing judgment and add them as elimination rules for the automatic tactics. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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'. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

255 
*} 
22073  256 

257 
declare trm.inject [simp add] 

258 
declare ty.inject [simp add] 

259 

260 
inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T" 

261 
inductive_cases2 t_Var_elim_auto[elim]: "\<Gamma> \<turnstile> Var x : T" 

262 
inductive_cases2 t_App_elim_auto[elim]: "\<Gamma> \<turnstile> App x y : T" 

263 
inductive_cases2 t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T" 

264 
inductive_cases2 t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit" 

265 

266 
declare trm.inject [simp del] 

267 
declare ty.inject [simp del] 

268 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

269 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

270 
\subsubsection{Strong induction principle} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

271 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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$) *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

273 

22073  274 
lemma typing_induct_strong 
275 
[consumes 1, case_names t_Var t_App t_Lam t_Const t_Unit]: 

276 
fixes P::"'a::fs_name \<Rightarrow> (name\<times>ty) list \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow>bool" 

277 
and x :: "'a::fs_name" 

278 
assumes a: "\<Gamma> \<turnstile> e : 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" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

281 
\<Longrightarrow> P c \<Gamma> (App e\<^isub>1 e\<^isub>2) T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

283 
\<Longrightarrow> P c \<Gamma> (Lam [x].t) (T\<^isub>1\<rightarrow>T\<^isub>2)" 
22073  284 
and a4: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> (Const n) TBase" 
285 
and a5: "\<And>\<Gamma> c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> Unit TUnit" 

286 
shows "P c \<Gamma> e T" 

287 
proof  

22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

288 
from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) (pi\<bullet>T)" 
22073  289 
proof (induct) 
290 
case (t_Var \<Gamma> x T pi c) 

291 
have "valid \<Gamma>" by fact 

22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

292 
then have "valid (pi\<bullet>\<Gamma>)" by (simp only: eqvt) 
22073  293 
moreover 
294 
have "(x,T)\<in>set \<Gamma>" by fact 

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]) 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

296 
then have "(pi\<bullet>x,T)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: eqvt) 
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

297 
ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) (pi\<bullet>T)" using a1 by simp 
22073  298 
next 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

299 
case (t_App \<Gamma> e\<^isub>1 T\<^isub>1 T\<^isub>2 e\<^isub>2 pi c) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

300 
thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e\<^isub>1 e\<^isub>2)) (pi\<bullet>T\<^isub>2)" using a2 
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

301 
by (simp only: eqvt) (blast) 
22073  302 
next 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

303 
case (t_Lam x \<Gamma> T\<^isub>1 t T\<^isub>2 pi c) 
22073  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]) 
305 
let ?sw = "[(pi\<bullet>x,y)]" 

306 
let ?pi' = "?sw@pi" 

307 
have f0: "x\<sharp>\<Gamma>" by fact 

308 
have f1: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f0 by (simp add: fresh_bij) 

309 
have f2: "y\<sharp>?pi'\<bullet>\<Gamma>" by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

310 
have ih1: "\<And>c. P c (?pi'\<bullet>((x,T\<^isub>1)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>T\<^isub>2)" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

311 
then have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T\<^isub>1\<rightarrow>T\<^isub>2)" using fs f2 a3 
22073  312 
by (simp add: calc_atm) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)" 
22073  314 
by (simp del: append_Cons add: calc_atm pt_name2) 
315 
moreover have "(?sw\<bullet>pi\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" 

316 
by (rule perm_fresh_fresh) (simp_all add: fs f1) 

317 
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) = Lam [(pi\<bullet>x)].(pi\<bullet>t)" 

318 
by (rule perm_fresh_fresh) (simp_all add: fs f1 fresh_atm abs_fresh) 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

319 
ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (pi\<bullet>T\<^isub>1\<rightarrow>T\<^isub>2)" by simp 
22073  320 
next 
321 
case (t_Const \<Gamma> n pi c) 

22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

322 
thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (pi\<bullet>TBase)" using a4 by (simp, blast intro: valid_eqvt) 
22073  323 
next 
324 
case (t_Unit \<Gamma> pi c) 

22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

325 
thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Unit) (pi\<bullet>TUnit)" using a5 by (simp, blast intro: valid_eqvt) 
22073  326 
qed 
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

327 
then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) (([]::name prm)\<bullet>T)" by blast 
22073  328 
then show "P c \<Gamma> e T" by simp 
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

329 
qed 
22073  330 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

331 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

332 
\subsection{Captureavoiding substitutions} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

333 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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.\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

335 
Should we return Some or None and put that in a library ? 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

336 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

337 

22073  338 

339 
fun 

340 
lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm" 

341 
where 

342 
"lookup [] X = Var X" 

343 
"lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)" 

344 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

345 
lemma lookup_eqvt[eqvt]: 
22073  346 
fixes pi::"name prm" 
347 
and \<theta>::"(name\<times>trm) list" 

348 
and X::"name" 

349 
shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

350 
by (induct \<theta>) (auto simp add: perm_bij) 
22073  351 

352 
lemma lookup_fresh: 

353 
fixes z::"name" 

354 
assumes "z\<sharp>\<theta>" "z\<sharp>x" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

355 
shows "z\<sharp> lookup \<theta> x" 
22073  356 
using assms 
357 
by (induct rule: lookup.induct) (auto simp add: fresh_list_cons) 

358 

359 
lemma lookup_fresh': 

360 
assumes "z\<sharp>\<theta>" 

361 
shows "lookup \<theta> z = Var z" 

362 
using assms 

363 
by (induct rule: lookup.induct) 

364 
(auto simp add: fresh_list_cons fresh_prod fresh_atm) 

365 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

366 
text {* \subsubsection{Parallel substitution} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

367 

22073  368 
consts 
369 
psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [60,100] 100) 

370 

371 
nominal_primrec 

372 
"\<theta><(Var x)> = (lookup \<theta> x)" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

373 
"\<theta><(App t\<^isub>1 t\<^isub>2)> = App (\<theta><t\<^isub>1>) (\<theta><t\<^isub>2>)" 
22073  374 
"x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)" 
375 
"\<theta><(Const n)> = Const n" 

376 
"\<theta><(Unit)> = Unit" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

377 
apply(finite_guess)+ 
22073  378 
apply(rule TrueI)+ 
379 
apply(simp add: abs_fresh)+ 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

380 
apply(fresh_guess)+ 
22073  381 
done 
382 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

383 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

384 
text {* \subsubsection{Substitution} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

385 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

386 
The substitution function is defined just as a special case of parallel substitution. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

387 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

388 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

389 

22073  390 
abbreviation 
391 
subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100) 

392 
where 

393 
"t[x::=t'] \<equiv> ([(x,t')])<t>" 

394 

395 
lemma subst[simp]: 

396 
shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

397 
and "(App t\<^isub>1 t\<^isub>2)[y::=t'] = App (t\<^isub>1[y::=t']) (t\<^isub>2[y::=t'])" 
22073  398 
and "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" 
399 
and "Const n[y::=t'] = Const n" 

400 
and "Unit [y::=t'] = Unit" 

401 
by (simp_all add: fresh_list_cons fresh_list_nil) 

402 

22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset

403 
lemma subst_eqvt[eqvt]: 
22073  404 
fixes pi::"name prm" 
405 
and t::"trm" 

406 
shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]" 

407 
by (nominal_induct t avoiding: x t' rule: trm.induct) 

408 
(perm_simp add: fresh_bij)+ 

409 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

410 
text {* \subsubsection{Lemmas about freshness and substitutions} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

411 

22073  412 
lemma subst_rename: 
413 
fixes c::"name" 

414 
and t1::"trm" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

415 
assumes a: "c\<sharp>t\<^isub>1" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

416 
shows "t\<^isub>1[a::=t\<^isub>2] = ([(c,a)]\<bullet>t\<^isub>1)[c::=t\<^isub>2]" 
22073  417 
using a 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

418 
apply(nominal_induct t\<^isub>1 avoiding: a c t\<^isub>2 rule: trm.induct) 
22073  419 
apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+ 
420 
done 

421 

422 
lemma fresh_psubst: 

423 
fixes z::"name" 

424 
and t::"trm" 

425 
assumes "z\<sharp>t" "z\<sharp>\<theta>" 

426 
shows "z\<sharp>(\<theta><t>)" 

427 
using assms 

428 
by (nominal_induct t avoiding: z \<theta> t rule: trm.induct) 

429 
(auto simp add: abs_fresh lookup_fresh) 

430 

431 
lemma fresh_subst'': 

432 
fixes z::"name" 

433 
and t1::"trm" 

434 
and t2::"trm" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

435 
assumes "z\<sharp>t\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

436 
shows "z\<sharp>t\<^isub>1[z::=t\<^isub>2]" 
22073  437 
using assms 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

438 
by (nominal_induct t\<^isub>1 avoiding: t\<^isub>2 z rule: trm.induct) 
22073  439 
(auto simp add: abs_fresh fresh_nat fresh_atm) 
440 

441 
lemma fresh_subst': 

442 
fixes z::"name" 

443 
and t1::"trm" 

444 
and t2::"trm" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

445 
assumes "z\<sharp>[y].t\<^isub>1" "z\<sharp>t\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

446 
shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]" 
22073  447 
using assms 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

448 
by (nominal_induct t\<^isub>1 avoiding: y t\<^isub>2 z rule: trm.induct) 
22073  449 
(auto simp add: abs_fresh fresh_nat fresh_atm) 
450 

451 
lemma fresh_subst: 

452 
fixes z::"name" 

453 
and t1::"trm" 

454 
and t2::"trm" 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

455 
assumes "z\<sharp>t\<^isub>1" "z\<sharp>t\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

456 
shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]" 
22073  457 
using assms fresh_subst' 
458 
by (auto simp add: abs_fresh) 

459 

460 
lemma fresh_psubst_simpl: 

461 
assumes "x\<sharp>t" 

462 
shows "(x,u)#\<theta><t> = \<theta><t>" 

463 
using assms 

464 
proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct) 

465 
case (Lam y t x u) 

466 
have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact 

467 
moreover have "x\<sharp> Lam [y].t" by fact 

468 
ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm) 

469 
moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact 

470 
ultimately have "(x,u)#\<theta><t> = \<theta><t>" by auto 

471 
moreover have "(x,u)#\<theta><Lam [y].t> = Lam [y]. ((x,u)#\<theta><t>)" using fs 

472 
by (simp add: fresh_list_cons fresh_prod) 

473 
moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp 

474 
ultimately show "(x,u)#\<theta><Lam [y].t> = \<theta><Lam [y].t>" by auto 

475 
qed (auto simp add: fresh_atm abs_fresh) 

476 

477 
lemma forget: 

478 
fixes x::"name" 

479 
and L::"trm" 

480 
assumes a: "x\<sharp>L" 

481 
shows "L[x::=P] = L" 

482 
using a 

22082  483 
by (nominal_induct L avoiding: x P rule: trm.induct) 
484 
(auto simp add: fresh_atm abs_fresh) 

22073  485 

486 
lemma subst_fun_eq: 

487 
fixes u::trm 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

488 
assumes h:"[x].t\<^isub>1 = [y].t\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

489 
shows "t\<^isub>1[x::=u] = t\<^isub>2[y::=u]" 
22073  490 
proof  
491 
{ 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

492 
assume "x=y" and "t\<^isub>1=t\<^isub>2" 
22073  493 
then have ?thesis using h by simp 
494 
} 

495 
moreover 

496 
{ 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

497 
assume h1:"x \<noteq> y" and h2:"t\<^isub>1=[(x,y)] \<bullet> t\<^isub>2" and h3:"x \<sharp> t\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

498 
then have "([(x,y)] \<bullet> t\<^isub>2)[x::=u] = t\<^isub>2[y::=u]" by (simp add: subst_rename) 
22073  499 
then have ?thesis using h2 by simp 
500 
} 

501 
ultimately show ?thesis using alpha h by blast 

502 
qed 

503 

504 
lemma psubst_empty[simp]: 

505 
shows "[]<t> = t" 

506 
by (nominal_induct t rule: trm.induct) (auto simp add: fresh_list_nil) 

507 

508 
lemma psubst_subst_psubst: 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

509 
assumes h:"c\<sharp>\<theta>" 
22073  510 
shows "\<theta><t>[c::=s] = (c,s)#\<theta><t>" 
511 
using h 

22082  512 
by (nominal_induct t avoiding: \<theta> c s rule: trm.induct) 
513 
(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst) 

22073  514 

515 
lemma subst_fresh_simpl: 

22082  516 
assumes a: "x\<sharp>\<theta>" 
22073  517 
shows "\<theta><Var x> = Var x" 
22082  518 
using a 
519 
by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm) 

22073  520 

521 
lemma psubst_subst_propagate: 

522 
assumes "x\<sharp>\<theta>" 

523 
shows "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" 

524 
using assms 

525 
proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct) 

526 
case (Var n x u \<theta>) 

527 
{ assume "x=n" 

528 
moreover have "x\<sharp>\<theta>" by fact 

529 
ultimately have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using subst_fresh_simpl by auto 

530 
} 

531 
moreover 

532 
{ assume h:"x\<noteq>n" 

533 
then have "x\<sharp>Var n" by (auto simp add: fresh_atm) 

534 
moreover have "x\<sharp>\<theta>" by fact 

535 
ultimately have "x\<sharp>\<theta><Var n>" using fresh_psubst by blast 

536 
then have " \<theta><Var n>[x::=\<theta><u>] = \<theta><Var n>" using forget by auto 

537 
then have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using h by auto 

538 
} 

539 
ultimately show ?case by auto 

540 
next 

541 
case (Lam n t x u \<theta>) 

542 
have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact 

543 
have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact 

544 
have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto 

545 
then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto 

546 
moreover have "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" using ih fs by blast 

547 
ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" 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 

549 
ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><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 

551 
qed (auto) 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

552 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

553 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

554 
\section{Equivalence} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

555 
\subsection{Definition of the equivalence relation} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

556 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

557 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

558 
(*<*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

559 
inductive2 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

560 
equiv_def :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<equiv> _ : _" [60,60] 60) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

561 
where 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

562 
Q_Refl[intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<equiv> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

563 
 Q_Symm[intro]: "\<Gamma> \<turnstile> t \<equiv> s : T \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

568 
\<Longrightarrow> \<Gamma> \<turnstile> App (Lam [x]. s12) s\<^isub>2 \<equiv> t12[x::=t\<^isub>2] : T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

570 
\<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

571 
(*>*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

572 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

573 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

574 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

575 
\isastyle 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

576 
@{thm[mode=Rule] Q_Refl[no_vars]}{\sc{Q\_Refl}}\qquad 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

577 
@{thm[mode=Rule] Q_Symm[no_vars]}{\sc{Q\_Symm}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

578 
@{thm[mode=Rule] Q_Trans[no_vars]}{\sc{Q\_Trans}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

579 
@{thm[mode=Rule] Q_App[no_vars]}{\sc{Q\_App}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

580 
@{thm[mode=Rule] Q_Abs[no_vars]}{\sc{Q\_Abs}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

581 
@{thm[mode=Rule] Q_Beta[no_vars]}{\sc{Q\_Beta}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

582 
@{thm[mode=Rule] Q_Ext[no_vars]}{\sc{Q\_Ext}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

583 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

584 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

585 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

586 
text {* It is now a tradition, we derive the lemma about validity, and we generate the equivariance lemma. *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

587 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

588 
lemma equiv_def_valid: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

589 
assumes "\<Gamma> \<turnstile> t \<equiv> s : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

590 
shows "valid \<Gamma>" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

591 
using assms by (induct,auto elim:typing_valid) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

592 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

593 
nominal_inductive equiv_def 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

594 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

595 
text{* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

596 
\subsection{Strong induction principle for the equivalence relation} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

597 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

598 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

599 
lemma equiv_def_strong_induct 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

600 
[consumes 1, case_names Q_Refl Q_Symm Q_Trans Q_Abs Q_App Q_Beta Q_Ext]: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

601 
fixes c::"'a::fs_name" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

602 
assumes a0: "\<Gamma> \<turnstile> s \<equiv> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

603 
and a1: "\<And>\<Gamma> t T c. \<Gamma> \<turnstile> t : T \<Longrightarrow> P c \<Gamma> t t T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

606 
\<Longrightarrow> P c \<Gamma> s u T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

608 
\<Longrightarrow> P c \<Gamma> (Lam [x].s\<^isub>2) (Lam [x].t\<^isub>2) (T\<^isub>1\<rightarrow>T\<^isub>2)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

610 
\<Longrightarrow> P c \<Gamma> (App s\<^isub>1 s\<^isub>2) (App t\<^isub>1 t\<^isub>2) T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

611 
and a6: "\<And>x \<Gamma> T\<^isub>1 s12 t12 T\<^isub>2 s\<^isub>2 t\<^isub>2 c. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

613 
\<Longrightarrow> P c \<Gamma> (App (Lam [x].s12) s\<^isub>2) (t12[x::=t\<^isub>2]) T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

614 
and a7: "\<And>x \<Gamma> s t T\<^isub>1 T\<^isub>2 c. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

616 
\<Longrightarrow> P c \<Gamma> s t (T\<^isub>1\<rightarrow>T\<^isub>2)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

617 
shows "P c \<Gamma> s t T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

618 
proof  
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

619 
from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

620 
proof(induct) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

621 
case (Q_Refl \<Gamma> t T pi c) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

622 
then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) (pi\<bullet>T)" using a1 by (simp only: eqvt) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

623 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

624 
case (Q_Symm \<Gamma> t s T pi c) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

626 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

627 
case (Q_Trans \<Gamma> s t T u pi c) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

629 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

632 
by (simp only: eqvt) (blast) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

633 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

634 
case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>2 pi c) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

635 
then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T\<^isub>1\<rightarrow>T\<^isub>2)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

636 
by (auto intro!: a7 simp add: fresh_bij) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

637 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

638 
case (Q_Abs x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 pi c) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

640 
let ?sw="[(pi\<bullet>x,y)]" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

641 
let ?pi'="?sw@pi" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

642 
have f1: "x\<sharp>\<Gamma>" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

643 
have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

644 
have f3: "y\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

648 
by (simp add: calc_atm) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

650 
by (simp del: append_Cons add: calc_atm pt_name2) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

651 
moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

652 
by (rule perm_fresh_fresh) (simp_all add: fs f2) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

653 
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>s\<^isub>2))) = Lam [(pi\<bullet>x)].(pi\<bullet>s\<^isub>2)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

654 
by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

655 
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t\<^isub>2))) = Lam [(pi\<bullet>x)].(pi\<bullet>t\<^isub>2)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

656 
by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

659 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

660 
case (Q_Beta x \<Gamma> s\<^isub>2 t\<^isub>2 T\<^isub>1 s12 t12 T\<^isub>2 pi c) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

662 
by (rule exists_fresh[OF fs_name1]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

663 
let ?sw="[(pi\<bullet>x,y)]" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

664 
let ?pi'="?sw@pi" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

665 
have f1: "x\<sharp>(\<Gamma>,s\<^isub>2,t\<^isub>2)" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

666 
have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s\<^isub>2,t\<^isub>2))" using f1 by (simp add: fresh_bij) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

667 
have f3: "y\<sharp>(?pi'\<bullet>(\<Gamma>,s\<^isub>2,t\<^isub>2))" using f1 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

668 
by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp fresh_prod) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

671 
moreover 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

674 
using a6 f3 fs by (force simp add: subst_eqvt calc_atm del: perm_ty) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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))) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

676 
(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t\<^isub>2)])) T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

677 
by (simp del: append_Cons add: calc_atm pt_name2 subst_eqvt) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

678 
moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

679 
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

681 
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified] abs_fresh) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)])" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

683 
by (rule perm_fresh_fresh) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

684 
(simp_all add: fs[simplified] f2[simplified] fresh_subst fresh_subst'') 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

686 
by simp 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

688 
qed 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

689 
then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>T)" by blast 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

690 
then show "P c \<Gamma> s t T" by simp 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

691 
qed 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

692 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

693 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

694 
text {* \section{Typedriven equivalence algorithm} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

695 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

696 
We follow the original presentation. The algorithm is described using inference rules only. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

697 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

698 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

699 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

700 
text {* \subsection{Weak head reduction} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

701 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

702 
(*<*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

703 
inductive2 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

704 
whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

705 
where 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

706 
QAR_Beta[intro]: "App (Lam [x]. t12) t\<^isub>2 \<leadsto> t12[x::=t\<^isub>2]" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

707 
 QAR_App[intro]: "t1 \<leadsto> t1' \<Longrightarrow> App t1 t\<^isub>2 \<leadsto> App t1' t\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

708 
(*>*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

709 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

710 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

711 
\begin{figure} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

712 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

713 
\isastyle 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

714 
@{thm[mode=Rule] QAR_Beta[no_vars]}{\sc{QAR\_Beta}} \qquad 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

715 
@{thm[mode=Rule] QAR_App[no_vars]}{\sc{QAR\_App}} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

716 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

717 
\end{figure} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

718 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

719 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

720 
text {* \subsubsection{Inversion lemma for weak head reduction} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

721 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

722 
declare trm.inject [simp add] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

723 
declare ty.inject [simp add] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

724 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

725 
inductive_cases2 whr_Gen[elim]: "t \<leadsto> t'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

726 
inductive_cases2 whr_Lam[elim]: "Lam [x].t \<leadsto> t'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

727 
inductive_cases2 whr_App_Lam[elim]: "App (Lam [x].t12) t2 \<leadsto> t" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

728 
inductive_cases2 whr_Var[elim]: "Var x \<leadsto> t" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

729 
inductive_cases2 whr_Const[elim]: "Const n \<leadsto> t" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

730 
inductive_cases2 whr_App[elim]: "App p q \<leadsto> t" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

731 
inductive_cases2 whr_Const_Right[elim]: "t \<leadsto> Const n" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

732 
inductive_cases2 whr_Var_Right[elim]: "t \<leadsto> Var x" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

733 
inductive_cases2 whr_App_Right[elim]: "t \<leadsto> App p q" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

734 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

735 
declare trm.inject [simp del] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

736 
declare ty.inject [simp del] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

737 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

738 
nominal_inductive whr_def 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

739 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

740 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

741 
\subsection{Weak head normalization} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

742 
\subsubsection{Definition of the normal form} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

743 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

744 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

745 
abbreviation 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

746 
nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>" [100] 100) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

747 
where 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

748 
"t\<leadsto> \<equiv> \<not>(\<exists> u. t \<leadsto> u)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

749 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

750 
text{* \subsubsection{Definition of weak head normal form} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

751 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

752 
(*<*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

753 
inductive2 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

754 
whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

755 
where 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

756 
QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

757 
 QAN_Normal[intro]: "t\<leadsto> \<Longrightarrow> t \<Down> t" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

758 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

759 
(*>*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

760 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

761 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

762 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

763 
@{thm[mode=Rule] QAN_Reduce[no_vars]}{\sc{QAN\_Reduce}}\qquad 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

764 
@{thm[mode=Rule] QAN_Normal[no_vars]}{\sc{QAN\_Normal}} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

765 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

766 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

767 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

768 
lemma whn_eqvt[eqvt]: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

769 
fixes pi::"name prm" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

770 
assumes a: "t \<Down> t'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

771 
shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

772 
using a 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

773 
apply(induct) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

774 
apply(rule QAN_Reduce) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

775 
apply(rule whr_def_eqvt) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

776 
apply(assumption)+ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

777 
apply(rule QAN_Normal) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

778 
apply(auto) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

779 
apply(drule_tac pi="rev pi" in whr_def_eqvt) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

780 
apply(perm_simp) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

781 
done 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

782 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

783 
text {* \subsection{Algorithmic term equivalence and algorithmic path equivalence} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

784 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

785 
(*<*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

786 
inductive2 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

787 
alg_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60] 60) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

788 
and 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

789 
alg_path_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60] 60) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

790 
where 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

793 
\<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1 \<rightarrow> T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

794 
 QAT_One[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TUnit" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

795 
 QAP_Var[intro]: "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

797 
 QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

798 
(*>*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

799 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

800 
text {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

801 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

802 
@{thm[mode=Rule] QAT_Base[no_vars]}{\sc{QAT\_Base}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

803 
@{thm[mode=Rule] QAT_Arrow[no_vars]}{\sc{QAT\_Arrow}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

804 
@{thm[mode=Rule] QAP_Var[no_vars]}{\sc{QAP\_Var}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

805 
@{thm[mode=Rule] QAP_App[no_vars]}{\sc{QAP\_App}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

806 
@{thm[mode=Rule] QAP_Const[no_vars]}{\sc{QAP\_Const}}\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

807 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

808 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

809 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

810 
text {* Again we generate the equivariance lemma. *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

811 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

812 
nominal_inductive alg_equiv 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

813 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

814 
text {* \subsubsection{Strong induction principle for algorithmic term and path equivalences} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

815 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

816 
lemma alg_equiv_alg_path_equiv_strong_induct 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

817 
[case_names QAT_Base QAT_Arrow QAT_One QAP_Var QAP_App QAP_Const]: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

818 
fixes c::"'a::fs_name" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

820 
\<Longrightarrow> P1 c \<Gamma> s t TBase" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

821 
and a2: "\<And>x \<Gamma> s t T\<^isub>1 T\<^isub>2 c. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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; 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

823 
\<And>d. P1 d ((x,T\<^isub>1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T\<^isub>2\<rbrakk> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

824 
\<Longrightarrow> P1 c \<Gamma> s t (T\<^isub>1\<rightarrow>T\<^isub>2)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

825 
and a3: "\<And>\<Gamma> s t c. valid \<Gamma> \<Longrightarrow> P1 c \<Gamma> s t TUnit" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

827 
and a5: "\<And>\<Gamma> p q T\<^isub>1 T\<^isub>2 s t c. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

829 
\<Longrightarrow> P2 c \<Gamma> (App p s) (App q t) T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

830 
and a6: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P2 c \<Gamma> (Const n) (Const n) TBase" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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')" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

832 
proof  
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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'))" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

835 
proof(induct rule: alg_equiv_alg_path_equiv.induct) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

836 
case (QAT_Base s q t p \<Gamma>) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

837 
then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TBase" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

838 
apply(auto) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

839 
apply(rule_tac p="pi\<bullet>q" and q="pi\<bullet>p" in a1) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

840 
apply(simp_all add: eqvt[simplified]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

841 
done 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

842 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

843 
case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

844 
show ?case 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

845 
proof (rule allI, rule allI) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

846 
fix c::"'a::fs_name" and pi::"name prm" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

848 
let ?sw="[(pi\<bullet>x,y)]" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

849 
let ?pi'="?sw@pi" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

850 
have f0: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

851 
then have f1: "x\<sharp>(\<Gamma>,s,t)" by simp 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

852 
have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s,t))" using f1 by (simp add: fresh_bij) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

853 
have f3: "y\<sharp>?pi'\<bullet>(\<Gamma>,s,t)" using f1 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

854 
by (simp only: pt_name2 fresh_left, auto simp add: perm_pi_simp calc_atm) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

856 
have pr1: "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

859 
by (auto simp add: eqvt) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

861 
by (simp add: calc_atm) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

862 
moreover 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

864 
by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

866 
by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

868 
by (simp add: calc_atm) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

871 
by (simp del: append_Cons add: calc_atm pt_name2) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

872 
moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

873 
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

874 
moreover have "(?sw\<bullet>(pi\<bullet>s)) = (pi\<bullet>s)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

875 
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

876 
moreover have "(?sw\<bullet>(pi\<bullet>t)) = (pi\<bullet>t)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

877 
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

878 
ultimately show "P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T\<^isub>1\<rightarrow>T\<^isub>2)" by (simp) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

879 
qed 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

880 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

881 
case (QAT_One \<Gamma> s t) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

882 
then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TUnit" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

883 
by (auto intro!: a3 simp add: valid_eqvt) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

884 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

885 
case (QAP_Var \<Gamma> x T) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

886 
then show "\<forall>c (pi::name prm). P2 c (pi \<bullet> \<Gamma>) (pi \<bullet> Var x) (pi \<bullet> Var x) T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

887 
apply(auto intro!: a4 simp add: valid_eqvt) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

888 
apply(simp add: set_eqvt[symmetric]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

889 
apply(perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

890 
done 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

891 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

892 
case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

894 
by (auto intro!: a5 simp add: eqvt[simplified]) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

895 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

896 
case (QAP_Const \<Gamma> n) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

897 
then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>Const n) (pi\<bullet>Const n) TBase" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

898 
by (auto intro!: a6 simp add: eqvt) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

899 
qed 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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> 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

901 
(\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c (([]::name prm)\<bullet>\<Gamma>') (([]::name prm)\<bullet>s') (([]::name prm)\<bullet>t') T')" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

902 
by blast 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

903 
then show ?thesis by simp 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

904 
qed 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

905 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

906 
(* postprocessing of the strong induction principle proved above; *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

907 
(* the code extracts the strong_inductsversion from strong_induct *) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

908 
(*<*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

909 
setup {* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

910 
PureThy.add_thmss 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

911 
[(("alg_equiv_alg_path_equiv_strong_inducts", 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

912 
ProjectRule.projects (ProofContext.init (the_context())) [1,2] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

913 
(thm "alg_equiv_alg_path_equiv_strong_induct")), [])] #> snd 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

914 
*} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

915 
(*>*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

916 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

917 
lemma alg_equiv_valid: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

918 
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

919 
by (induct rule : alg_equiv_alg_path_equiv.inducts, auto) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

920 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

921 
text{* \subsubsection{Inversion lemmas for algorithmic term and path equivalences} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

922 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

923 
declare trm.inject [simp add] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

924 
declare ty.inject [simp add] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

925 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

926 
inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

927 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

928 
inductive_cases2 alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

929 
inductive_cases2 alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

930 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

931 
inductive_cases2 alg_path_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

932 
inductive_cases2 alg_path_equiv_Unit_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

933 
inductive_cases2 alg_path_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

934 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

935 
inductive_cases2 alg_path_equiv_Var_left_inv_auto[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

936 
inductive_cases2 alg_path_equiv_Var_left_inv_auto'[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

937 
inductive_cases2 alg_path_equiv_Var_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

938 
inductive_cases2 alg_path_equiv_Var_right_inv_auto'[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

939 
inductive_cases2 alg_path_equiv_Const_left_inv_auto[elim]: "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

940 
inductive_cases2 alg_path_equiv_Const_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

941 
inductive_cases2 alg_path_equiv_App_left_inv_auto[elim]: "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

942 
inductive_cases2 alg_path_equiv_App_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

943 
inductive_cases2 alg_path_equiv_Lam_left_inv_auto[elim]: "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

944 
inductive_cases2 alg_path_equiv_Lam_right_inv_auto[elim]: "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

945 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

946 
declare trm.inject [simp del] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

947 
declare ty.inject [simp del] 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

948 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

949 
text {* \section{Completeness of the algorithm} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

950 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

951 
lemma algorithmic_monotonicity: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

952 
fixes \<Gamma>':: "(name\<times>ty) list" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

953 
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

954 
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

955 
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

956 
case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>') 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

957 
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

958 
have h2:"\<Gamma>\<lless>\<Gamma>'" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

960 
have "x\<sharp>\<Gamma>'" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

961 
then have sub:"(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'" using h2 by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

963 
then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using sub fs by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

964 
qed (auto) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

965 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

966 
lemma valid_monotonicity[elim]: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

967 
assumes "\<Gamma> \<lless> \<Gamma>'" and "x\<sharp>\<Gamma>'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

968 
shows "(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

969 
using assms by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

970 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

971 
lemma algorithmic_monotonicity_auto: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

972 
fixes \<Gamma>':: "(name\<times>ty) list" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

973 
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

974 
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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) 
22073  976 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

977 
text {* \subsection{Definition of the logical relation} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

978 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

979 
function log_equiv :: "((name\<times>ty) list \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

980 
("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

981 
where 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

982 
"\<Gamma> \<turnstile> s is t : TUnit = valid \<Gamma>" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

983 
 "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

984 
 "\<Gamma> \<turnstile> s is t : (T\<^isub>1 \<rightarrow> T\<^isub>2) = 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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)))" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

986 
apply (auto simp add: ty.inject) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" ) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

988 
apply (force) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

989 
apply (rule ty_cases) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

990 
done 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

991 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

992 
termination 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

993 
apply(relation "measure (\<lambda>(_,_,_,T). size T)") 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

994 
apply(auto) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

995 
done 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

996 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

997 
lemma log_equiv_valid: 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

998 
assumes "\<Gamma> \<turnstile> s is t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

999 
shows "valid \<Gamma>" 
22073  1000 
using assms 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1001 
by (induct rule: log_equiv.induct,auto elim: alg_equiv_valid) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1002 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1003 
text {* \subsubsection{Monotonicity of the logical equivalence relation} *} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1004 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1005 
lemma logical_monotonicity : 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1006 
fixes T::ty 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1007 
assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma>\<lless>\<Gamma>'" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1008 
shows "\<Gamma>' \<turnstile> s is t : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1009 
using assms 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1010 
proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1011 
case (2 \<Gamma> s t \<Gamma>') 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1012 
then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1013 
next 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1014 
case (3 \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>') 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1015 
then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by force 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1016 
qed (auto) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1017 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1018 
text {* If two terms are path equivalent then they are in normal form. *} 
22073  1019 

1020 
lemma path_equiv_implies_nf: 

1021 
assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" 

1022 
shows "s \<leadsto>" and "t \<leadsto>" 

1023 
using assms 

22082  1024 
by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto) 
22073  1025 

1026 
lemma main_lemma: 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
22073  1028 
proof (nominal_induct T arbitrary: \<Gamma> s t p q rule:ty.induct) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1029 
case (Arrow T\<^isub>1 T\<^isub>2) 
22073  1030 
{ 
1031 
case (1 \<Gamma> s t) 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1034 
have h:"\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by fact 
22073  1035 
obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1]) 
1036 
have "valid \<Gamma>" using h log_equiv_valid by auto 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1037 
then have v:"valid ((x,T\<^isub>1)#\<Gamma>)" using fs by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1038 
then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T\<^isub>1" by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1039 
then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x is Var x : T\<^isub>1" using ih2 by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1042 
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod) 
22073  1043 
next 
1044 
case (2 \<Gamma> p q) 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1045 
have h:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
22073  1048 
{ 
1049 
fix \<Gamma>' s t 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1050 
assume "\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^isub>1" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1051 
then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2" using h algorithmic_monotonicity by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1052 
moreover have "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" using ih2 hl by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1053 
ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2" by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1054 
then have "\<Gamma>' \<turnstile> App p s is App q t : T\<^isub>2" using ih1 by auto 
22073  1055 
} 
1056 
moreover have "valid \<Gamma>" using h alg_equiv_valid by auto 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1057 
ultimately show "\<Gamma> \<turnstile> p is q : T\<^isub>1\<rightarrow>T\<^isub>2" by auto 
22073  1058 
} 
1059 
next 

1060 
case TBase 

1061 
{ case 2 

1062 
have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact 

1063 
then have "s \<leadsto>" and "t \<leadsto>" using path_equiv_implies_nf by auto 

1064 
then have "s \<Down> s" and "t \<Down> t" by auto 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1065 
then have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" using h by auto 
22073  1066 
then show "\<Gamma> \<turnstile> s is t : TBase" by auto 
1067 
} 

1068 
qed (auto elim:alg_equiv_valid) 

1069 

1070 
corollary corollary_main: 

22082  1071 
assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1072 
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" 
22082  1073 
using a main_lemma by blast 
22073  1074 

1075 
lemma algorithmic_symmetry: 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1076 
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1077 
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1078 
by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto) 
22073  1079 

1080 
lemma red_unicity : 

22082  1081 
assumes a: "x \<leadsto> a" 
1082 
and b: "x \<leadsto> b" 

22073  1083 
shows "a=b" 
22082  1084 
using a b 
22073  1085 
apply (induct arbitrary: b) 
1086 
apply (erule whr_App_Lam) 

1087 
apply (clarify) 

1088 
apply (rule subst_fun_eq) 

22082  1089 
apply (simp) 
22073  1090 
apply (force) 
1091 
apply (erule whr_App) 

1092 
apply (blast)+ 

1093 
done 

1094 

1095 
lemma nf_unicity : 

1096 
assumes "x \<Down> a" "x \<Down> b" 

1097 
shows "a=b" 

1098 
using assms 

1099 
proof (induct arbitrary: b) 

1100 
case (QAN_Reduce x t a b) 

1101 
have h:"x \<leadsto> t" "t \<Down> a" by fact 

1102 
have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact 

1103 
have "x \<Down> b" by fact 

1104 
then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto 

1105 
then have "t=t'" using h red_unicity by auto 

1106 
then show "a=b" using ih hl by auto 

1107 
qed (auto) 

1108 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1109 
nominal_inductive alg_equiv 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1110 

22073  1111 
(* FIXME this lemma should not be here I am reinventing the wheel I guess *) 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1112 
(*<*) 
22073  1113 
lemma perm_basic[simp]: 
22082  1114 
fixes x y::"name" 
22073  1115 
shows "[(x,y)]\<bullet>y = x" 
1116 
using assms using calc_atm by perm_simp 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1117 
(*>*) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1118 

49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1119 
text{* \subsection{Strong inversion lemma for algorithmic equivalence} *} 
22073  1120 

1121 
lemma Q_Arrow_strong_inversion: 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1123 
shows "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" 
22073  1124 
proof  
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
22082  1126 
using h by auto 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1128 
using alg_equiv_eqvt[simplified] by blast 
22082  1129 
then show ?thesis using fs fs2 by (perm_simp) 
22073  1130 
qed 
1131 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1132 
text{* 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1133 
For the \texttt{algorithmic\_transitivity} lemma we need a unicity property. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1134 
But one has to be cautious, because this unicity property is true only for algorithmic path. 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1135 
Indeed the following lemma is \textbf{false}:\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1136 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1137 
@{prop "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1138 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1139 
Here is the counter example :\\ 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1140 
\begin{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1141 
@{prop "\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase"} and @{prop "\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit"} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1142 
\end{center} 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1143 
*} 
22073  1144 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1145 
(* 
22073  1146 
lemma algorithmic_type_unicity: 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1147 
shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" 
22073  1148 
and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" 
1149 

1150 
Here is the counter example : 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1151 
\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase and \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit 
22073  1152 

1153 
*) 

1154 

1155 
lemma algorithmic_path_type_unicity: 

1156 
shows "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" 

22082  1157 
proof (induct arbitrary: u T' 
1158 
rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _ "%a b c d . True" ]) 

22073  1159 
case (QAP_Var \<Gamma> x T u T') 
1160 
have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact 

1161 
then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto 

1162 
moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact 

1163 
ultimately show "T=T'" using type_unicity_in_context by auto 

1164 
next 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1165 
case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u T\<^isub>2') 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1166 
have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1167 
have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2'" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1169 
then have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1170 
then show "T\<^isub>2=T\<^isub>2'" using ty.inject by auto 
22073  1171 
qed (auto) 
1172 

1173 
lemma algorithmic_transitivity: 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1174 
shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<Leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T" 
22073  1175 
and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T" 
1176 
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv_strong_inducts) 

1177 
case (QAT_Base s p t q \<Gamma> u) 

1178 
have h:"s \<Down> p" "t \<Down> q" by fact 

1179 
have ih:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : TBase" by fact 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1180 
have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : TBase" by fact 
22073  1181 
then obtain r q' where hl:"t \<Down> q'" "u \<Down> r" "\<Gamma> \<turnstile> q' \<leftrightarrow> r : TBase" by auto 
1182 
moreover have eq:"q=q'" using nf_unicity hl h by auto 

1183 
ultimately have "\<Gamma> \<turnstile> p \<leftrightarrow> r : TBase" using ih by auto 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1184 
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : TBase" using hl h by auto 
22073  1185 
next 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1186 
case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 u) 
22073  1187 
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1188 
moreover have h:"\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
22082  1190 
by auto 
22073  1191 
moreover have fs2:"x\<sharp>u" by fact 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
22082  1194 
by fact 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1195 
ultimately have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1196 
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" using fs fs2 by auto 
22073  1197 
next 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1198 
case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1199 
have h1:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1201 
have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1202 
have ih2:"\<And>u. \<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1203 
have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T\<^isub>2" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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" 
22082  1205 
by auto 
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1206 
moreover have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T\<^isub>1\<rightarrow>T\<^isub>2" using h1 algorithmic_symmetry by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1207 
ultimately have "T\<^isub>1'\<rightarrow>T\<^isub>2 = T\<^isub>1\<rightarrow>T\<^isub>2" using algorithmic_path_type_unicity by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1208 
then have "T\<^isub>1' = T\<^isub>1" using ty.inject by auto 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1210 
then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2" using eq by auto 
22073  1211 
qed (auto) 
1212 

1213 
lemma algorithmic_weak_head_closure: 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1214 
shows "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; s' \<leadsto> s; t' \<leadsto> t\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' \<Leftrightarrow> t' : T" 
22073  1215 
by (nominal_induct \<Gamma> s t T avoiding: s' t' 
1216 
rule: alg_equiv_alg_path_equiv_strong_inducts(1) [of _ _ _ _ "%a b c d e. True"]) 

1217 
(auto) 

1218 

1219 
lemma logical_symmetry: 

22082  1220 
assumes a: "\<Gamma> \<turnstile> s is t : T" 
22073  1221 
shows "\<Gamma> \<turnstile> t is s : T" 
22082  1222 
using a 
1223 
by (nominal_induct arbitrary: \<Gamma> s t rule:ty.induct) (auto simp add: algorithmic_symmetry) 

22073  1224 

1225 
lemma logical_transitivity: 

1226 
assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" 

1227 
shows "\<Gamma> \<turnstile> s is u : T" 

1228 
using assms 

1229 
proof (nominal_induct arbitrary: \<Gamma> s t u rule:ty.induct) 

1230 
case TBase 

1231 
then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim: algorithmic_transitivity) 

1232 
next 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1233 
case (Arrow T\<^isub>1 T\<^isub>2 \<Gamma> s t u) 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1234 
have h1:"\<Gamma> \<turnstile> s is t : T\<^isub>1 \<rightarrow> T\<^isub>2" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1235 
have h2:"\<Gamma> \<turnstile> t is u : T\<^isub>1 \<rightarrow> T\<^isub>2" by fact 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

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 
22073  1238 
{ 
1239 
fix \<Gamma>' s' u' 

22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1240 
assume hsub:"\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^isub>1" 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1241 
then have "\<Gamma>' \<turnstile> u' is s' : T\<^isub>1" using logical_symmetry by blast 
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset

1242 
then have "\<Gamma>' \<turnstile> u' is u' : T\<^isub>1" using ih1 hl by blast 
