1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 02 16:52:21 2004 +0200
1.3 @@ -0,0 +1,462 @@
1.4 +(* Title: HOL/Induct/QuoNestedDataType
1.5 + ID: $Id$
1.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 + Copyright 2004 University of Cambridge
1.8 +
1.9 +*)
1.10 +
1.11 +header{*Quotienting a Free Algebra Involving Nested Recursion*}
1.12 +
1.13 +theory QuoNestedDataType = Main:
1.14 +
1.15 +subsection{*Defining the Free Algebra*}
1.16 +
1.17 +text{*Messages with encryption and decryption as free constructors.*}
1.18 +datatype
1.19 + freeExp = VAR nat
1.20 + | PLUS freeExp freeExp
1.21 + | FNCALL nat "freeExp list"
1.22 +
1.23 +text{*The equivalence relation, which makes PLUS associative.*}
1.24 +consts exprel :: "(freeExp * freeExp) set"
1.25 +
1.26 +syntax
1.27 + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "~~" 50)
1.28 +syntax (xsymbols)
1.29 + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
1.30 +syntax (HTML output)
1.31 + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
1.32 +translations
1.33 + "X \<sim> Y" == "(X,Y) \<in> exprel"
1.34 +
1.35 +text{*The first rule is the desired equation. The next three rules
1.36 +make the equations applicable to subterms. The last two rules are symmetry
1.37 +and transitivity.*}
1.38 +inductive "exprel"
1.39 + intros
1.40 + ASSOC: "PLUS X (PLUS Y Z) \<sim> PLUS (PLUS X Y) Z"
1.41 + VAR: "VAR N \<sim> VAR N"
1.42 + PLUS: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> PLUS X Y \<sim> PLUS X' Y'"
1.43 + FNCALL: "(Xs,Xs') \<in> listrel exprel \<Longrightarrow> FNCALL F Xs \<sim> FNCALL F Xs'"
1.44 + SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
1.45 + TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
1.46 + monos listrel_mono
1.47 +
1.48 +
1.49 +text{*Proving that it is an equivalence relation*}
1.50 +
1.51 +lemma exprel_refl_conj: "X \<sim> X & (Xs,Xs) \<in> listrel(exprel)"
1.52 +apply (induct X and Xs)
1.53 +apply (blast intro: exprel.intros listrel.intros)+
1.54 +done
1.55 +
1.56 +lemmas exprel_refl = exprel_refl_conj [THEN conjunct1]
1.57 +lemmas list_exprel_refl = exprel_refl_conj [THEN conjunct2]
1.58 +
1.59 +theorem equiv_exprel: "equiv UNIV exprel"
1.60 +proof (simp add: equiv_def, intro conjI)
1.61 + show "reflexive exprel" by (simp add: refl_def exprel_refl)
1.62 + show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
1.63 + show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
1.64 +qed
1.65 +
1.66 +theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"
1.67 +by (insert equiv_listrel [OF equiv_exprel], simp)
1.68 +
1.69 +
1.70 +lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []"
1.71 +apply (rule exprel.intros)
1.72 +apply (rule listrel.intros)
1.73 +done
1.74 +
1.75 +lemma FNCALL_Cons:
1.76 + "\<lbrakk>X \<sim> X'; (Xs,Xs') \<in> listrel(exprel)\<rbrakk>
1.77 + \<Longrightarrow> FNCALL F (X#Xs) \<sim> FNCALL F (X'#Xs')"
1.78 +by (blast intro: exprel.intros listrel.intros)
1.79 +
1.80 +
1.81 +
1.82 +subsection{*Some Functions on the Free Algebra*}
1.83 +
1.84 +subsubsection{*The Set of Variables*}
1.85 +
1.86 +text{*A function to return the set of variables present in a message. It will
1.87 +be lifted to the initial algrebra, to serve as an example of that process.
1.88 +Note that the "free" refers to the free datatype rather than to the concept
1.89 +of a free variable.*}
1.90 +consts
1.91 + freevars :: "freeExp \<Rightarrow> nat set"
1.92 + freevars_list :: "freeExp list \<Rightarrow> nat set"
1.93 +
1.94 +primrec
1.95 + "freevars (VAR N) = {N}"
1.96 + "freevars (PLUS X Y) = freevars X \<union> freevars Y"
1.97 + "freevars (FNCALL F Xs) = freevars_list Xs"
1.98 +
1.99 + "freevars_list [] = {}"
1.100 + "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
1.101 +
1.102 +text{*This theorem lets us prove that the vars function respects the
1.103 +equivalence relation. It also helps us prove that Variable
1.104 + (the abstract constructor) is injective*}
1.105 +theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V"
1.106 +apply (erule exprel.induct)
1.107 +apply (erule_tac [4] listrel.induct)
1.108 +apply (simp_all add: Un_assoc)
1.109 +done
1.110 +
1.111 +
1.112 +
1.113 +subsubsection{*Functions for Freeness*}
1.114 +
1.115 +text{*A discriminator function to distinguish vars, sums and function calls*}
1.116 +consts freediscrim :: "freeExp \<Rightarrow> int"
1.117 +primrec
1.118 + "freediscrim (VAR N) = 0"
1.119 + "freediscrim (PLUS X Y) = 1"
1.120 + "freediscrim (FNCALL F Xs) = 2"
1.121 +
1.122 +theorem exprel_imp_eq_freediscrim:
1.123 + "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
1.124 +by (erule exprel.induct, auto)
1.125 +
1.126 +
1.127 +text{*This function, which returns the function name, is used to
1.128 +prove part of the injectivity property for FnCall.*}
1.129 +consts freefun :: "freeExp \<Rightarrow> nat"
1.130 +
1.131 +primrec
1.132 + "freefun (VAR N) = 0"
1.133 + "freefun (PLUS X Y) = 0"
1.134 + "freefun (FNCALL F Xs) = F"
1.135 +
1.136 +theorem exprel_imp_eq_freefun:
1.137 + "U \<sim> V \<Longrightarrow> freefun U = freefun V"
1.138 +by (erule exprel.induct, simp_all add: listrel.intros)
1.139 +
1.140 +
1.141 +text{*This function, which returns the list of function arguments, is used to
1.142 +prove part of the injectivity property for FnCall.*}
1.143 +consts freeargs :: "freeExp \<Rightarrow> freeExp list"
1.144 +primrec
1.145 + "freeargs (VAR N) = []"
1.146 + "freeargs (PLUS X Y) = []"
1.147 + "freeargs (FNCALL F Xs) = Xs"
1.148 +
1.149 +theorem exprel_imp_eqv_freeargs:
1.150 + "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
1.151 +apply (erule exprel.induct)
1.152 +apply (erule_tac [4] listrel.induct)
1.153 +apply (simp_all add: listrel.intros)
1.154 +apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])
1.155 +apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]])
1.156 +done
1.157 +
1.158 +
1.159 +
1.160 +subsection{*The Initial Algebra: A Quotiented Message Type*}
1.161 +
1.162 +
1.163 +typedef (Exp) exp = "UNIV//exprel"
1.164 + by (auto simp add: quotient_def)
1.165 +
1.166 +text{*The abstract message constructors*}
1.167 +
1.168 +constdefs
1.169 + Var :: "nat \<Rightarrow> exp"
1.170 + "Var N == Abs_Exp(exprel``{VAR N})"
1.171 +
1.172 + Plus :: "[exp,exp] \<Rightarrow> exp"
1.173 + "Plus X Y ==
1.174 + Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})"
1.175 +
1.176 + FnCall :: "[nat, exp list] \<Rightarrow> exp"
1.177 + "FnCall F Xs ==
1.178 + Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"
1.179 +
1.180 +
1.181 +text{*Reduces equality of equivalence classes to the @{term exprel} relation:
1.182 + @{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"} *}
1.183 +lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I]
1.184 +
1.185 +declare equiv_exprel_iff [simp]
1.186 +
1.187 +
1.188 +text{*All equivalence classes belong to set of representatives*}
1.189 +lemma [simp]: "exprel``{U} \<in> Exp"
1.190 +by (auto simp add: Exp_def quotient_def intro: exprel_refl)
1.191 +
1.192 +lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp"
1.193 +apply (rule inj_on_inverseI)
1.194 +apply (erule Abs_Exp_inverse)
1.195 +done
1.196 +
1.197 +text{*Reduces equality on abstractions to equality on representatives*}
1.198 +declare inj_on_Abs_Exp [THEN inj_on_iff, simp]
1.199 +
1.200 +declare Abs_Exp_inverse [simp]
1.201 +
1.202 +
1.203 +text{*Case analysis on the representation of a exp as an equivalence class.*}
1.204 +lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]:
1.205 + "(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P"
1.206 +apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE])
1.207 +apply (drule arg_cong [where f=Abs_Exp])
1.208 +apply (auto simp add: Rep_Exp_inverse intro: exprel_refl)
1.209 +done
1.210 +
1.211 +
1.212 +subsection{*Every list of abstract expressions can be expressed in terms of a
1.213 + list of concrete expressions*}
1.214 +
1.215 +constdefs Abs_ExpList :: "freeExp list => exp list"
1.216 + "Abs_ExpList Xs == map (%U. Abs_Exp(exprel``{U})) Xs"
1.217 +
1.218 +lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []"
1.219 +by (simp add: Abs_ExpList_def)
1.220 +
1.221 +lemma Abs_ExpList_Cons [simp]:
1.222 + "Abs_ExpList (X#Xs) == Abs_Exp (exprel``{X}) # Abs_ExpList Xs"
1.223 +by (simp add: Abs_ExpList_def)
1.224 +
1.225 +lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us"
1.226 +apply (induct z)
1.227 +apply (rule_tac [2] z=a in eq_Abs_Exp)
1.228 +apply (auto simp add: Abs_ExpList_def intro: exprel_refl)
1.229 +done
1.230 +
1.231 +lemma eq_Abs_ExpList [case_names Abs_ExpList]:
1.232 + "(!!Us. z = Abs_ExpList Us ==> P) ==> P"
1.233 +by (rule exE [OF ExpList_rep], blast)
1.234 +
1.235 +
1.236 +subsubsection{*Characteristic Equations for the Abstract Constructors*}
1.237 +
1.238 +lemma Plus: "Plus (Abs_Exp(exprel``{U})) (Abs_Exp(exprel``{V})) =
1.239 + Abs_Exp (exprel``{PLUS U V})"
1.240 +proof -
1.241 + have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel"
1.242 + by (simp add: congruent2_def exprel.PLUS)
1.243 + thus ?thesis
1.244 + by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])
1.245 +qed
1.246 +
1.247 +text{*It is not clear what to do with FnCall: it's argument is an abstraction
1.248 +of an @{typ "exp list"}. Is it just Nil or Cons? What seems to work best is to
1.249 +regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class*}
1.250 +
1.251 +text{*This theorem is easily proved but never used. There's no obvious way
1.252 +even to state the analogous result, @{text FnCall_Cons}.*}
1.253 +lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})"
1.254 + by (simp add: FnCall_def)
1.255 +
1.256 +lemma FnCall_respects:
1.257 + "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
1.258 + by (simp add: congruent_def exprel.FNCALL)
1.259 +
1.260 +lemma FnCall_sing:
1.261 + "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"
1.262 +proof -
1.263 + have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel"
1.264 + by (simp add: congruent_def FNCALL_Cons listrel.intros)
1.265 + thus ?thesis
1.266 + by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel])
1.267 +qed
1.268 +
1.269 +lemma listset_Rep_Exp_Abs_Exp:
1.270 + "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
1.271 +by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def)
1.272 +
1.273 +lemma FnCall:
1.274 + "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
1.275 +proof -
1.276 + have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
1.277 + by (simp add: congruent_def exprel.FNCALL)
1.278 + thus ?thesis
1.279 + by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]
1.280 + listset_Rep_Exp_Abs_Exp)
1.281 +qed
1.282 +
1.283 +
1.284 +text{*Establishing this equation is the point of the whole exercise*}
1.285 +theorem Plus_assoc: "Plus X (Plus Y Z) = Plus (Plus X Y) Z"
1.286 +by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC)
1.287 +
1.288 +
1.289 +
1.290 +subsection{*The Abstract Function to Return the Set of Variables*}
1.291 +
1.292 +constdefs
1.293 + vars :: "exp \<Rightarrow> nat set"
1.294 + "vars X == \<Union>U \<in> Rep_Exp X. freevars U"
1.295 +
1.296 +lemma vars_respects: "freevars respects exprel"
1.297 +by (simp add: congruent_def exprel_imp_eq_freevars)
1.298 +
1.299 +text{*The extension of the function @{term vars} to lists*}
1.300 +consts vars_list :: "exp list \<Rightarrow> nat set"
1.301 +primrec
1.302 + "vars_list [] = {}"
1.303 + "vars_list(E#Es) = vars E \<union> vars_list Es"
1.304 +
1.305 +
1.306 +text{*Now prove the three equations for @{term vars}*}
1.307 +
1.308 +lemma vars_Variable [simp]: "vars (Var N) = {N}"
1.309 +by (simp add: vars_def Var_def
1.310 + UN_equiv_class [OF equiv_exprel vars_respects])
1.311 +
1.312 +lemma vars_Plus [simp]: "vars (Plus X Y) = vars X \<union> vars Y"
1.313 +apply (cases X, cases Y)
1.314 +apply (simp add: vars_def Plus
1.315 + UN_equiv_class [OF equiv_exprel vars_respects])
1.316 +done
1.317 +
1.318 +lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs"
1.319 +apply (cases Xs rule: eq_Abs_ExpList)
1.320 +apply (simp add: FnCall)
1.321 +apply (induct_tac Us)
1.322 +apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects])
1.323 +done
1.324 +
1.325 +lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}"
1.326 +by simp
1.327 +
1.328 +lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X \<union> vars_list Xs"
1.329 +by simp
1.330 +
1.331 +
1.332 +subsection{*Injectivity Properties of Some Constructors*}
1.333 +
1.334 +lemma VAR_imp_eq: "VAR m \<sim> VAR n \<Longrightarrow> m = n"
1.335 +by (drule exprel_imp_eq_freevars, simp)
1.336 +
1.337 +text{*Can also be proved using the function @{term vars}*}
1.338 +lemma Var_Var_eq [iff]: "(Var m = Var n) = (m = n)"
1.339 +by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq)
1.340 +
1.341 +lemma VAR_neqv_PLUS: "VAR m \<sim> PLUS X Y \<Longrightarrow> False"
1.342 +by (drule exprel_imp_eq_freediscrim, simp)
1.343 +
1.344 +theorem Var_neq_Plus [iff]: "Var N \<noteq> Plus X Y"
1.345 +apply (cases X, cases Y)
1.346 +apply (simp add: Var_def Plus)
1.347 +apply (blast dest: VAR_neqv_PLUS)
1.348 +done
1.349 +
1.350 +theorem Var_neq_FnCall [iff]: "Var N \<noteq> FnCall F Xs"
1.351 +apply (cases Xs rule: eq_Abs_ExpList)
1.352 +apply (auto simp add: FnCall Var_def)
1.353 +apply (drule exprel_imp_eq_freediscrim, simp)
1.354 +done
1.355 +
1.356 +subsection{*Injectivity of @{term FnCall}*}
1.357 +
1.358 +constdefs
1.359 + fun :: "exp \<Rightarrow> nat"
1.360 + "fun X == contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
1.361 +
1.362 +lemma fun_respects: "(%U. {freefun U}) respects exprel"
1.363 +by (simp add: congruent_def exprel_imp_eq_freefun)
1.364 +
1.365 +lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"
1.366 +apply (cases Xs rule: eq_Abs_ExpList)
1.367 +apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects])
1.368 +done
1.369 +
1.370 +constdefs
1.371 + args :: "exp \<Rightarrow> exp list"
1.372 + "args X == contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
1.373 +
1.374 +text{*This result can probably be generalized to arbitrary equivalence
1.375 +relations, but with little benefit here.*}
1.376 +lemma Abs_ExpList_eq:
1.377 + "(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)"
1.378 +by (erule listrel.induct, simp_all)
1.379 +
1.380 +lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
1.381 +by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs)
1.382 +
1.383 +lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"
1.384 +apply (cases Xs rule: eq_Abs_ExpList)
1.385 +apply (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects])
1.386 +done
1.387 +
1.388 +
1.389 +lemma FnCall_FnCall_eq [iff]:
1.390 + "(FnCall F Xs = FnCall F' Xs') = (F=F' & Xs=Xs')"
1.391 +proof
1.392 + assume "FnCall F Xs = FnCall F' Xs'"
1.393 + hence "fun (FnCall F Xs) = fun (FnCall F' Xs')"
1.394 + and "args (FnCall F Xs) = args (FnCall F' Xs')" by auto
1.395 + thus "F=F' & Xs=Xs'" by simp
1.396 +next
1.397 + assume "F=F' & Xs=Xs'" thus "FnCall F Xs = FnCall F' Xs'" by simp
1.398 +qed
1.399 +
1.400 +
1.401 +subsection{*The Abstract Discriminator*}
1.402 +text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
1.403 +function in order to prove discrimination theorems.*}
1.404 +
1.405 +constdefs
1.406 + discrim :: "exp \<Rightarrow> int"
1.407 + "discrim X == contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
1.408 +
1.409 +lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
1.410 +by (simp add: congruent_def exprel_imp_eq_freediscrim)
1.411 +
1.412 +text{*Now prove the four equations for @{term discrim}*}
1.413 +
1.414 +lemma discrim_Var [simp]: "discrim (Var N) = 0"
1.415 +by (simp add: discrim_def Var_def
1.416 + UN_equiv_class [OF equiv_exprel discrim_respects])
1.417 +
1.418 +lemma discrim_Plus [simp]: "discrim (Plus X Y) = 1"
1.419 +apply (cases X, cases Y)
1.420 +apply (simp add: discrim_def Plus
1.421 + UN_equiv_class [OF equiv_exprel discrim_respects])
1.422 +done
1.423 +
1.424 +lemma discrim_FnCall [simp]: "discrim (FnCall F Xs) = 2"
1.425 +apply (rule_tac z=Xs in eq_Abs_ExpList)
1.426 +apply (simp add: discrim_def FnCall
1.427 + UN_equiv_class [OF equiv_exprel discrim_respects])
1.428 +done
1.429 +
1.430 +
1.431 +text{*The structural induction rule for the abstract type*}
1.432 +theorem exp_induct:
1.433 + assumes V: "\<And>nat. P1 (Var nat)"
1.434 + and P: "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)"
1.435 + and F: "\<And>nat list. P2 list \<Longrightarrow> P1 (FnCall nat list)"
1.436 + and Nil: "P2 []"
1.437 + and Cons: "\<And>exp list. \<lbrakk>P1 exp; P2 list\<rbrakk> \<Longrightarrow> P2 (exp # list)"
1.438 + shows "P1 exp & P2 list"
1.439 +proof (cases exp, rule eq_Abs_ExpList [of list], clarify)
1.440 + fix U Us
1.441 + show "P1 (Abs_Exp (exprel `` {U})) \<and>
1.442 + P2 (Abs_ExpList Us)"
1.443 + proof (induct U and Us)
1.444 + case (VAR nat)
1.445 + with V show ?case by (simp add: Var_def)
1.446 + next
1.447 + case (PLUS X Y)
1.448 + with P [of "Abs_Exp (exprel `` {X})" "Abs_Exp (exprel `` {Y})"]
1.449 + show ?case by (simp add: Plus)
1.450 + next
1.451 + case (FNCALL nat list)
1.452 + with F [of "Abs_ExpList list"]
1.453 + show ?case by (simp add: FnCall)
1.454 + next
1.455 + case Nil_freeExp
1.456 + with Nil show ?case by simp
1.457 + next
1.458 + case Cons_freeExp
1.459 + with Cons
1.460 + show ?case by simp
1.461 + qed
1.462 +qed
1.463 +
1.464 +end
1.465 +