15172

1 
(* Title: HOL/Induct/QuoNestedDataType


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 2004 University of Cambridge


5 


6 
*)


7 


8 
header{*Quotienting a Free Algebra Involving Nested Recursion*}


9 

16417

10 
theory QuoNestedDataType imports Main begin

15172

11 


12 
subsection{*Defining the Free Algebra*}


13 


14 
text{*Messages with encryption and decryption as free constructors.*}


15 
datatype


16 
freeExp = VAR nat


17 
 PLUS freeExp freeExp


18 
 FNCALL nat "freeExp list"


19 


20 
text{*The equivalence relation, which makes PLUS associative.*}


21 
consts exprel :: "(freeExp * freeExp) set"


22 


23 
syntax


24 
"_exprel" :: "[freeExp, freeExp] => bool" (infixl "~~" 50)


25 
syntax (xsymbols)


26 
"_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)


27 
syntax (HTML output)


28 
"_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)


29 
translations


30 
"X \<sim> Y" == "(X,Y) \<in> exprel"


31 


32 
text{*The first rule is the desired equation. The next three rules


33 
make the equations applicable to subterms. The last two rules are symmetry


34 
and transitivity.*}


35 
inductive "exprel"


36 
intros


37 
ASSOC: "PLUS X (PLUS Y Z) \<sim> PLUS (PLUS X Y) Z"


38 
VAR: "VAR N \<sim> VAR N"


39 
PLUS: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> PLUS X Y \<sim> PLUS X' Y'"


40 
FNCALL: "(Xs,Xs') \<in> listrel exprel \<Longrightarrow> FNCALL F Xs \<sim> FNCALL F Xs'"


41 
SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"


42 
TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"


43 
monos listrel_mono


44 


45 


46 
text{*Proving that it is an equivalence relation*}


47 


48 
lemma exprel_refl_conj: "X \<sim> X & (Xs,Xs) \<in> listrel(exprel)"


49 
apply (induct X and Xs)


50 
apply (blast intro: exprel.intros listrel.intros)+


51 
done


52 


53 
lemmas exprel_refl = exprel_refl_conj [THEN conjunct1]


54 
lemmas list_exprel_refl = exprel_refl_conj [THEN conjunct2]


55 


56 
theorem equiv_exprel: "equiv UNIV exprel"


57 
proof (simp add: equiv_def, intro conjI)


58 
show "reflexive exprel" by (simp add: refl_def exprel_refl)


59 
show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)


60 
show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)


61 
qed


62 


63 
theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"


64 
by (insert equiv_listrel [OF equiv_exprel], simp)


65 


66 


67 
lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []"


68 
apply (rule exprel.intros)


69 
apply (rule listrel.intros)


70 
done


71 


72 
lemma FNCALL_Cons:


73 
"\<lbrakk>X \<sim> X'; (Xs,Xs') \<in> listrel(exprel)\<rbrakk>


74 
\<Longrightarrow> FNCALL F (X#Xs) \<sim> FNCALL F (X'#Xs')"


75 
by (blast intro: exprel.intros listrel.intros)


76 


77 


78 


79 
subsection{*Some Functions on the Free Algebra*}


80 


81 
subsubsection{*The Set of Variables*}


82 


83 
text{*A function to return the set of variables present in a message. It will


84 
be lifted to the initial algrebra, to serve as an example of that process.


85 
Note that the "free" refers to the free datatype rather than to the concept


86 
of a free variable.*}


87 
consts


88 
freevars :: "freeExp \<Rightarrow> nat set"


89 
freevars_list :: "freeExp list \<Rightarrow> nat set"


90 


91 
primrec


92 
"freevars (VAR N) = {N}"


93 
"freevars (PLUS X Y) = freevars X \<union> freevars Y"


94 
"freevars (FNCALL F Xs) = freevars_list Xs"


95 


96 
"freevars_list [] = {}"


97 
"freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"


98 


99 
text{*This theorem lets us prove that the vars function respects the


100 
equivalence relation. It also helps us prove that Variable


101 
(the abstract constructor) is injective*}


102 
theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V"


103 
apply (erule exprel.induct)


104 
apply (erule_tac [4] listrel.induct)


105 
apply (simp_all add: Un_assoc)


106 
done


107 


108 


109 


110 
subsubsection{*Functions for Freeness*}


111 


112 
text{*A discriminator function to distinguish vars, sums and function calls*}


113 
consts freediscrim :: "freeExp \<Rightarrow> int"


114 
primrec


115 
"freediscrim (VAR N) = 0"


116 
"freediscrim (PLUS X Y) = 1"


117 
"freediscrim (FNCALL F Xs) = 2"


118 


119 
theorem exprel_imp_eq_freediscrim:


120 
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"


121 
by (erule exprel.induct, auto)


122 


123 


124 
text{*This function, which returns the function name, is used to


125 
prove part of the injectivity property for FnCall.*}


126 
consts freefun :: "freeExp \<Rightarrow> nat"


127 


128 
primrec


129 
"freefun (VAR N) = 0"


130 
"freefun (PLUS X Y) = 0"


131 
"freefun (FNCALL F Xs) = F"


132 


133 
theorem exprel_imp_eq_freefun:


134 
"U \<sim> V \<Longrightarrow> freefun U = freefun V"


135 
by (erule exprel.induct, simp_all add: listrel.intros)


136 


137 


138 
text{*This function, which returns the list of function arguments, is used to


139 
prove part of the injectivity property for FnCall.*}


140 
consts freeargs :: "freeExp \<Rightarrow> freeExp list"


141 
primrec


142 
"freeargs (VAR N) = []"


143 
"freeargs (PLUS X Y) = []"


144 
"freeargs (FNCALL F Xs) = Xs"


145 


146 
theorem exprel_imp_eqv_freeargs:


147 
"U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"


148 
apply (erule exprel.induct)


149 
apply (erule_tac [4] listrel.induct)


150 
apply (simp_all add: listrel.intros)


151 
apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])


152 
apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]])


153 
done


154 


155 


156 


157 
subsection{*The Initial Algebra: A Quotiented Message Type*}


158 


159 


160 
typedef (Exp) exp = "UNIV//exprel"


161 
by (auto simp add: quotient_def)


162 


163 
text{*The abstract message constructors*}


164 


165 
constdefs


166 
Var :: "nat \<Rightarrow> exp"


167 
"Var N == Abs_Exp(exprel``{VAR N})"


168 


169 
Plus :: "[exp,exp] \<Rightarrow> exp"


170 
"Plus X Y ==


171 
Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})"


172 


173 
FnCall :: "[nat, exp list] \<Rightarrow> exp"


174 
"FnCall F Xs ==


175 
Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"


176 


177 


178 
text{*Reduces equality of equivalence classes to the @{term exprel} relation:


179 
@{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"} *}


180 
lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I]


181 


182 
declare equiv_exprel_iff [simp]


183 


184 


185 
text{*All equivalence classes belong to set of representatives*}


186 
lemma [simp]: "exprel``{U} \<in> Exp"


187 
by (auto simp add: Exp_def quotient_def intro: exprel_refl)


188 


189 
lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp"


190 
apply (rule inj_on_inverseI)


191 
apply (erule Abs_Exp_inverse)


192 
done


193 


194 
text{*Reduces equality on abstractions to equality on representatives*}


195 
declare inj_on_Abs_Exp [THEN inj_on_iff, simp]


196 


197 
declare Abs_Exp_inverse [simp]


198 


199 


200 
text{*Case analysis on the representation of a exp as an equivalence class.*}


201 
lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]:


202 
"(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P"


203 
apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE])


204 
apply (drule arg_cong [where f=Abs_Exp])


205 
apply (auto simp add: Rep_Exp_inverse intro: exprel_refl)


206 
done


207 


208 


209 
subsection{*Every list of abstract expressions can be expressed in terms of a


210 
list of concrete expressions*}


211 


212 
constdefs Abs_ExpList :: "freeExp list => exp list"


213 
"Abs_ExpList Xs == map (%U. Abs_Exp(exprel``{U})) Xs"


214 


215 
lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []"


216 
by (simp add: Abs_ExpList_def)


217 


218 
lemma Abs_ExpList_Cons [simp]:


219 
"Abs_ExpList (X#Xs) == Abs_Exp (exprel``{X}) # Abs_ExpList Xs"


220 
by (simp add: Abs_ExpList_def)


221 


222 
lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us"


223 
apply (induct z)


224 
apply (rule_tac [2] z=a in eq_Abs_Exp)


225 
apply (auto simp add: Abs_ExpList_def intro: exprel_refl)


226 
done


227 


228 
lemma eq_Abs_ExpList [case_names Abs_ExpList]:


229 
"(!!Us. z = Abs_ExpList Us ==> P) ==> P"


230 
by (rule exE [OF ExpList_rep], blast)


231 


232 


233 
subsubsection{*Characteristic Equations for the Abstract Constructors*}


234 


235 
lemma Plus: "Plus (Abs_Exp(exprel``{U})) (Abs_Exp(exprel``{V})) =


236 
Abs_Exp (exprel``{PLUS U V})"


237 
proof 


238 
have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel"


239 
by (simp add: congruent2_def exprel.PLUS)


240 
thus ?thesis


241 
by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])


242 
qed


243 


244 
text{*It is not clear what to do with FnCall: it's argument is an abstraction


245 
of an @{typ "exp list"}. Is it just Nil or Cons? What seems to work best is to


246 
regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class*}


247 


248 
text{*This theorem is easily proved but never used. There's no obvious way


249 
even to state the analogous result, @{text FnCall_Cons}.*}


250 
lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})"


251 
by (simp add: FnCall_def)


252 


253 
lemma FnCall_respects:


254 
"(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"


255 
by (simp add: congruent_def exprel.FNCALL)


256 


257 
lemma FnCall_sing:


258 
"FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"


259 
proof 


260 
have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel"


261 
by (simp add: congruent_def FNCALL_Cons listrel.intros)


262 
thus ?thesis


263 
by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel])


264 
qed


265 


266 
lemma listset_Rep_Exp_Abs_Exp:


267 
"listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";


268 
by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def)


269 


270 
lemma FnCall:


271 
"FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"


272 
proof 


273 
have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"


274 
by (simp add: congruent_def exprel.FNCALL)


275 
thus ?thesis


276 
by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]


277 
listset_Rep_Exp_Abs_Exp)


278 
qed


279 


280 


281 
text{*Establishing this equation is the point of the whole exercise*}


282 
theorem Plus_assoc: "Plus X (Plus Y Z) = Plus (Plus X Y) Z"


283 
by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC)


284 


285 


286 


287 
subsection{*The Abstract Function to Return the Set of Variables*}


288 


289 
constdefs


290 
vars :: "exp \<Rightarrow> nat set"


291 
"vars X == \<Union>U \<in> Rep_Exp X. freevars U"


292 


293 
lemma vars_respects: "freevars respects exprel"


294 
by (simp add: congruent_def exprel_imp_eq_freevars)


295 


296 
text{*The extension of the function @{term vars} to lists*}


297 
consts vars_list :: "exp list \<Rightarrow> nat set"


298 
primrec


299 
"vars_list [] = {}"


300 
"vars_list(E#Es) = vars E \<union> vars_list Es"


301 


302 


303 
text{*Now prove the three equations for @{term vars}*}


304 


305 
lemma vars_Variable [simp]: "vars (Var N) = {N}"


306 
by (simp add: vars_def Var_def


307 
UN_equiv_class [OF equiv_exprel vars_respects])


308 


309 
lemma vars_Plus [simp]: "vars (Plus X Y) = vars X \<union> vars Y"


310 
apply (cases X, cases Y)


311 
apply (simp add: vars_def Plus


312 
UN_equiv_class [OF equiv_exprel vars_respects])


313 
done


314 


315 
lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs"


316 
apply (cases Xs rule: eq_Abs_ExpList)


317 
apply (simp add: FnCall)


318 
apply (induct_tac Us)


319 
apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects])


320 
done


321 


322 
lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}"


323 
by simp


324 


325 
lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X \<union> vars_list Xs"


326 
by simp


327 


328 


329 
subsection{*Injectivity Properties of Some Constructors*}


330 


331 
lemma VAR_imp_eq: "VAR m \<sim> VAR n \<Longrightarrow> m = n"


332 
by (drule exprel_imp_eq_freevars, simp)


333 


334 
text{*Can also be proved using the function @{term vars}*}


335 
lemma Var_Var_eq [iff]: "(Var m = Var n) = (m = n)"


336 
by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq)


337 


338 
lemma VAR_neqv_PLUS: "VAR m \<sim> PLUS X Y \<Longrightarrow> False"


339 
by (drule exprel_imp_eq_freediscrim, simp)


340 


341 
theorem Var_neq_Plus [iff]: "Var N \<noteq> Plus X Y"


342 
apply (cases X, cases Y)


343 
apply (simp add: Var_def Plus)


344 
apply (blast dest: VAR_neqv_PLUS)


345 
done


346 


347 
theorem Var_neq_FnCall [iff]: "Var N \<noteq> FnCall F Xs"


348 
apply (cases Xs rule: eq_Abs_ExpList)


349 
apply (auto simp add: FnCall Var_def)


350 
apply (drule exprel_imp_eq_freediscrim, simp)


351 
done


352 


353 
subsection{*Injectivity of @{term FnCall}*}


354 


355 
constdefs


356 
fun :: "exp \<Rightarrow> nat"


357 
"fun X == contents (\<Union>U \<in> Rep_Exp X. {freefun U})"


358 


359 
lemma fun_respects: "(%U. {freefun U}) respects exprel"


360 
by (simp add: congruent_def exprel_imp_eq_freefun)


361 


362 
lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"


363 
apply (cases Xs rule: eq_Abs_ExpList)


364 
apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects])


365 
done


366 


367 
constdefs


368 
args :: "exp \<Rightarrow> exp list"


369 
"args X == contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"


370 


371 
text{*This result can probably be generalized to arbitrary equivalence


372 
relations, but with little benefit here.*}


373 
lemma Abs_ExpList_eq:


374 
"(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)"


375 
by (erule listrel.induct, simp_all)


376 


377 
lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"


378 
by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs)


379 


380 
lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"


381 
apply (cases Xs rule: eq_Abs_ExpList)


382 
apply (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects])


383 
done


384 


385 


386 
lemma FnCall_FnCall_eq [iff]:


387 
"(FnCall F Xs = FnCall F' Xs') = (F=F' & Xs=Xs')"


388 
proof


389 
assume "FnCall F Xs = FnCall F' Xs'"


390 
hence "fun (FnCall F Xs) = fun (FnCall F' Xs')"


391 
and "args (FnCall F Xs) = args (FnCall F' Xs')" by auto


392 
thus "F=F' & Xs=Xs'" by simp


393 
next


394 
assume "F=F' & Xs=Xs'" thus "FnCall F Xs = FnCall F' Xs'" by simp


395 
qed


396 


397 


398 
subsection{*The Abstract Discriminator*}


399 
text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this


400 
function in order to prove discrimination theorems.*}


401 


402 
constdefs


403 
discrim :: "exp \<Rightarrow> int"


404 
"discrim X == contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"


405 


406 
lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"


407 
by (simp add: congruent_def exprel_imp_eq_freediscrim)


408 


409 
text{*Now prove the four equations for @{term discrim}*}


410 


411 
lemma discrim_Var [simp]: "discrim (Var N) = 0"


412 
by (simp add: discrim_def Var_def


413 
UN_equiv_class [OF equiv_exprel discrim_respects])


414 


415 
lemma discrim_Plus [simp]: "discrim (Plus X Y) = 1"


416 
apply (cases X, cases Y)


417 
apply (simp add: discrim_def Plus


418 
UN_equiv_class [OF equiv_exprel discrim_respects])


419 
done


420 


421 
lemma discrim_FnCall [simp]: "discrim (FnCall F Xs) = 2"


422 
apply (rule_tac z=Xs in eq_Abs_ExpList)


423 
apply (simp add: discrim_def FnCall


424 
UN_equiv_class [OF equiv_exprel discrim_respects])


425 
done


426 


427 


428 
text{*The structural induction rule for the abstract type*}


429 
theorem exp_induct:


430 
assumes V: "\<And>nat. P1 (Var nat)"


431 
and P: "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)"


432 
and F: "\<And>nat list. P2 list \<Longrightarrow> P1 (FnCall nat list)"


433 
and Nil: "P2 []"


434 
and Cons: "\<And>exp list. \<lbrakk>P1 exp; P2 list\<rbrakk> \<Longrightarrow> P2 (exp # list)"


435 
shows "P1 exp & P2 list"


436 
proof (cases exp, rule eq_Abs_ExpList [of list], clarify)


437 
fix U Us


438 
show "P1 (Abs_Exp (exprel `` {U})) \<and>


439 
P2 (Abs_ExpList Us)"


440 
proof (induct U and Us)


441 
case (VAR nat)


442 
with V show ?case by (simp add: Var_def)


443 
next


444 
case (PLUS X Y)


445 
with P [of "Abs_Exp (exprel `` {X})" "Abs_Exp (exprel `` {Y})"]


446 
show ?case by (simp add: Plus)


447 
next


448 
case (FNCALL nat list)


449 
with F [of "Abs_ExpList list"]


450 
show ?case by (simp add: FnCall)


451 
next


452 
case Nil_freeExp


453 
with Nil show ?case by simp


454 
next


455 
case Cons_freeExp


456 
with Cons


457 
show ?case by simp


458 
qed


459 
qed


460 


461 
end


462 
