src/HOL/Induct/QuoNestedDataType.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*  Title:      HOL/Induct/QuoNestedDataType.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 header{*Quotienting a Free Algebra Involving Nested Recursion*}
     7 
     8 theory QuoNestedDataType imports Main begin
     9 
    10 subsection{*Defining the Free Algebra*}
    11 
    12 text{*Messages with encryption and decryption as free constructors.*}
    13 datatype
    14      freeExp = VAR  nat
    15              | PLUS  freeExp freeExp
    16              | FNCALL  nat "freeExp list"
    17 
    18 datatype_compat freeExp
    19 
    20 text{*The equivalence relation, which makes PLUS associative.*}
    21 
    22 text{*The first rule is the desired equation. The next three rules
    23 make the equations applicable to subterms. The last two rules are symmetry
    24 and transitivity.*}
    25 inductive_set
    26   exprel :: "(freeExp * freeExp) set"
    27   and exp_rel :: "[freeExp, freeExp] => bool"  (infixl "\<sim>" 50)
    28   where
    29     "X \<sim> Y == (X,Y) \<in> exprel"
    30   | ASSOC: "PLUS X (PLUS Y Z) \<sim> PLUS (PLUS X Y) Z"
    31   | VAR: "VAR N \<sim> VAR N"
    32   | PLUS: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> PLUS X Y \<sim> PLUS X' Y'"
    33   | FNCALL: "(Xs,Xs') \<in> listrel exprel \<Longrightarrow> FNCALL F Xs \<sim> FNCALL F Xs'"
    34   | SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
    35   | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
    36   monos listrel_mono
    37 
    38 
    39 text{*Proving that it is an equivalence relation*}
    40 
    41 lemma exprel_refl: "X \<sim> X"
    42   and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)"
    43   by (induct X and Xs rule: compat_freeExp.induct compat_freeExp_list.induct)
    44     (blast intro: exprel.intros listrel.intros)+
    45 
    46 theorem equiv_exprel: "equiv UNIV exprel"
    47 proof -
    48   have "refl exprel" by (simp add: refl_on_def exprel_refl)
    49   moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
    50   moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
    51   ultimately show ?thesis by (simp add: equiv_def)
    52 qed
    53 
    54 theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"
    55   using equiv_listrel [OF equiv_exprel] by simp
    56 
    57 
    58 lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []"
    59 apply (rule exprel.intros) 
    60 apply (rule listrel.intros) 
    61 done
    62 
    63 lemma FNCALL_Cons:
    64      "\<lbrakk>X \<sim> X'; (Xs,Xs') \<in> listrel(exprel)\<rbrakk>
    65       \<Longrightarrow> FNCALL F (X#Xs) \<sim> FNCALL F (X'#Xs')"
    66 by (blast intro: exprel.intros listrel.intros) 
    67 
    68 
    69 
    70 subsection{*Some Functions on the Free Algebra*}
    71 
    72 subsubsection{*The Set of Variables*}
    73 
    74 text{*A function to return the set of variables present in a message.  It will
    75 be lifted to the initial algrebra, to serve as an example of that process.
    76 Note that the "free" refers to the free datatype rather than to the concept
    77 of a free variable.*}
    78 primrec freevars :: "freeExp \<Rightarrow> nat set" 
    79   and freevars_list :: "freeExp list \<Rightarrow> nat set" where
    80   "freevars (VAR N) = {N}"
    81 | "freevars (PLUS X Y) = freevars X \<union> freevars Y"
    82 | "freevars (FNCALL F Xs) = freevars_list Xs"
    83 
    84 | "freevars_list [] = {}"
    85 | "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
    86 
    87 text{*This theorem lets us prove that the vars function respects the
    88 equivalence relation.  It also helps us prove that Variable
    89   (the abstract constructor) is injective*}
    90 theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V"
    91 apply (induct set: exprel) 
    92 apply (erule_tac [4] listrel.induct) 
    93 apply (simp_all add: Un_assoc)
    94 done
    95 
    96 
    97 
    98 subsubsection{*Functions for Freeness*}
    99 
   100 text{*A discriminator function to distinguish vars, sums and function calls*}
   101 primrec freediscrim :: "freeExp \<Rightarrow> int" where
   102   "freediscrim (VAR N) = 0"
   103 | "freediscrim (PLUS X Y) = 1"
   104 | "freediscrim (FNCALL F Xs) = 2"
   105 
   106 theorem exprel_imp_eq_freediscrim:
   107      "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
   108   by (induct set: exprel) auto
   109 
   110 
   111 text{*This function, which returns the function name, is used to
   112 prove part of the injectivity property for FnCall.*}
   113 primrec freefun :: "freeExp \<Rightarrow> nat" where
   114   "freefun (VAR N) = 0"
   115 | "freefun (PLUS X Y) = 0"
   116 | "freefun (FNCALL F Xs) = F"
   117 
   118 theorem exprel_imp_eq_freefun:
   119      "U \<sim> V \<Longrightarrow> freefun U = freefun V"
   120   by (induct set: exprel) (simp_all add: listrel.intros)
   121 
   122 
   123 text{*This function, which returns the list of function arguments, is used to
   124 prove part of the injectivity property for FnCall.*}
   125 primrec freeargs :: "freeExp \<Rightarrow> freeExp list" where
   126   "freeargs (VAR N) = []"
   127 | "freeargs (PLUS X Y) = []"
   128 | "freeargs (FNCALL F Xs) = Xs"
   129 
   130 theorem exprel_imp_eqv_freeargs:
   131   assumes "U \<sim> V"
   132   shows "(freeargs U, freeargs V) \<in> listrel exprel"
   133 proof -
   134   from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE)
   135   from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE)
   136   from assms show ?thesis
   137     apply induct
   138     apply (erule_tac [4] listrel.induct) 
   139     apply (simp_all add: listrel.intros)
   140     apply (blast intro: symD [OF sym])
   141     apply (blast intro: transD [OF trans])
   142     done
   143 qed
   144 
   145 
   146 subsection{*The Initial Algebra: A Quotiented Message Type*}
   147 
   148 definition "Exp = UNIV//exprel"
   149 
   150 typedef exp = Exp
   151   morphisms Rep_Exp Abs_Exp
   152   unfolding Exp_def by (auto simp add: quotient_def)
   153 
   154 text{*The abstract message constructors*}
   155 
   156 definition
   157   Var :: "nat \<Rightarrow> exp" where
   158   "Var N = Abs_Exp(exprel``{VAR N})"
   159 
   160 definition
   161   Plus :: "[exp,exp] \<Rightarrow> exp" where
   162    "Plus X Y =
   163        Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})"
   164 
   165 definition
   166   FnCall :: "[nat, exp list] \<Rightarrow> exp" where
   167    "FnCall F Xs =
   168        Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"
   169 
   170 
   171 text{*Reduces equality of equivalence classes to the @{term exprel} relation:
   172   @{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"} *}
   173 lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I]
   174 
   175 declare equiv_exprel_iff [simp]
   176 
   177 
   178 text{*All equivalence classes belong to set of representatives*}
   179 lemma [simp]: "exprel``{U} \<in> Exp"
   180 by (auto simp add: Exp_def quotient_def intro: exprel_refl)
   181 
   182 lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp"
   183 apply (rule inj_on_inverseI)
   184 apply (erule Abs_Exp_inverse)
   185 done
   186 
   187 text{*Reduces equality on abstractions to equality on representatives*}
   188 declare inj_on_Abs_Exp [THEN inj_on_iff, simp]
   189 
   190 declare Abs_Exp_inverse [simp]
   191 
   192 
   193 text{*Case analysis on the representation of a exp as an equivalence class.*}
   194 lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]:
   195      "(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P"
   196 apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE])
   197 apply (drule arg_cong [where f=Abs_Exp])
   198 apply (auto simp add: Rep_Exp_inverse intro: exprel_refl)
   199 done
   200 
   201 
   202 subsection{*Every list of abstract expressions can be expressed in terms of a
   203   list of concrete expressions*}
   204 
   205 definition
   206   Abs_ExpList :: "freeExp list => exp list" where
   207   "Abs_ExpList Xs = map (%U. Abs_Exp(exprel``{U})) Xs"
   208 
   209 lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []"
   210 by (simp add: Abs_ExpList_def)
   211 
   212 lemma Abs_ExpList_Cons [simp]:
   213      "Abs_ExpList (X#Xs) == Abs_Exp (exprel``{X}) # Abs_ExpList Xs"
   214 by (simp add: Abs_ExpList_def)
   215 
   216 lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us"
   217 apply (induct z)
   218 apply (rename_tac [2] a b)
   219 apply (rule_tac [2] z=a in eq_Abs_Exp)
   220 apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl)
   221 done
   222 
   223 lemma eq_Abs_ExpList [case_names Abs_ExpList]:
   224      "(!!Us. z = Abs_ExpList Us ==> P) ==> P"
   225 by (rule exE [OF ExpList_rep], blast) 
   226 
   227 
   228 subsubsection{*Characteristic Equations for the Abstract Constructors*}
   229 
   230 lemma Plus: "Plus (Abs_Exp(exprel``{U})) (Abs_Exp(exprel``{V})) = 
   231              Abs_Exp (exprel``{PLUS U V})"
   232 proof -
   233   have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel"
   234     by (auto simp add: congruent2_def exprel.PLUS)
   235   thus ?thesis
   236     by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])
   237 qed
   238 
   239 text{*It is not clear what to do with FnCall: it's argument is an abstraction
   240 of an @{typ "exp list"}. Is it just Nil or Cons? What seems to work best is to
   241 regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class*}
   242 
   243 text{*This theorem is easily proved but never used. There's no obvious way
   244 even to state the analogous result, @{text FnCall_Cons}.*}
   245 lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})"
   246   by (simp add: FnCall_def)
   247 
   248 lemma FnCall_respects: 
   249      "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
   250   by (auto simp add: congruent_def exprel.FNCALL)
   251 
   252 lemma FnCall_sing:
   253      "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"
   254 proof -
   255   have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel"
   256     by (auto simp add: congruent_def FNCALL_Cons listrel.intros)
   257   thus ?thesis
   258     by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel])
   259 qed
   260 
   261 lemma listset_Rep_Exp_Abs_Exp:
   262      "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}"
   263   by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def)
   264 
   265 lemma FnCall:
   266      "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
   267 proof -
   268   have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
   269     by (auto simp add: congruent_def exprel.FNCALL)
   270   thus ?thesis
   271     by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]
   272                   listset_Rep_Exp_Abs_Exp)
   273 qed
   274 
   275 
   276 text{*Establishing this equation is the point of the whole exercise*}
   277 theorem Plus_assoc: "Plus X (Plus Y Z) = Plus (Plus X Y) Z"
   278 by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC)
   279 
   280 
   281 
   282 subsection{*The Abstract Function to Return the Set of Variables*}
   283 
   284 definition
   285   vars :: "exp \<Rightarrow> nat set" where
   286   "vars X = (\<Union>U \<in> Rep_Exp X. freevars U)"
   287 
   288 lemma vars_respects: "freevars respects exprel"
   289 by (auto simp add: congruent_def exprel_imp_eq_freevars) 
   290 
   291 text{*The extension of the function @{term vars} to lists*}
   292 primrec vars_list :: "exp list \<Rightarrow> nat set" where
   293   "vars_list []    = {}"
   294 | "vars_list(E#Es) = vars E \<union> vars_list Es"
   295 
   296 
   297 text{*Now prove the three equations for @{term vars}*}
   298 
   299 lemma vars_Variable [simp]: "vars (Var N) = {N}"
   300 by (simp add: vars_def Var_def 
   301               UN_equiv_class [OF equiv_exprel vars_respects]) 
   302  
   303 lemma vars_Plus [simp]: "vars (Plus X Y) = vars X \<union> vars Y"
   304 apply (cases X, cases Y) 
   305 apply (simp add: vars_def Plus 
   306                  UN_equiv_class [OF equiv_exprel vars_respects]) 
   307 done
   308 
   309 lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs"
   310 apply (cases Xs rule: eq_Abs_ExpList) 
   311 apply (simp add: FnCall)
   312 apply (induct_tac Us)
   313 apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects])
   314 done
   315 
   316 lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}" 
   317 by simp
   318 
   319 lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X \<union> vars_list Xs"
   320 by simp
   321 
   322 
   323 subsection{*Injectivity Properties of Some Constructors*}
   324 
   325 lemma VAR_imp_eq: "VAR m \<sim> VAR n \<Longrightarrow> m = n"
   326 by (drule exprel_imp_eq_freevars, simp)
   327 
   328 text{*Can also be proved using the function @{term vars}*}
   329 lemma Var_Var_eq [iff]: "(Var m = Var n) = (m = n)"
   330 by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq)
   331 
   332 lemma VAR_neqv_PLUS: "VAR m \<sim> PLUS X Y \<Longrightarrow> False"
   333 by (drule exprel_imp_eq_freediscrim, simp)
   334 
   335 theorem Var_neq_Plus [iff]: "Var N \<noteq> Plus X Y"
   336 apply (cases X, cases Y) 
   337 apply (simp add: Var_def Plus) 
   338 apply (blast dest: VAR_neqv_PLUS) 
   339 done
   340 
   341 theorem Var_neq_FnCall [iff]: "Var N \<noteq> FnCall F Xs"
   342 apply (cases Xs rule: eq_Abs_ExpList) 
   343 apply (auto simp add: FnCall Var_def)
   344 apply (drule exprel_imp_eq_freediscrim, simp)
   345 done
   346 
   347 subsection{*Injectivity of @{term FnCall}*}
   348 
   349 definition
   350   "fun" :: "exp \<Rightarrow> nat" where
   351   "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
   352 
   353 lemma fun_respects: "(%U. {freefun U}) respects exprel"
   354 by (auto simp add: congruent_def exprel_imp_eq_freefun) 
   355 
   356 lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"
   357 apply (cases Xs rule: eq_Abs_ExpList) 
   358 apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects])
   359 done
   360 
   361 definition
   362   args :: "exp \<Rightarrow> exp list" where
   363   "args X = the_elem (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
   364 
   365 text{*This result can probably be generalized to arbitrary equivalence
   366 relations, but with little benefit here.*}
   367 lemma Abs_ExpList_eq:
   368      "(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)"
   369   by (induct set: listrel) simp_all
   370 
   371 lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
   372 by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 
   373 
   374 lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"
   375 apply (cases Xs rule: eq_Abs_ExpList) 
   376 apply (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects])
   377 done
   378 
   379 
   380 lemma FnCall_FnCall_eq [iff]:
   381      "(FnCall F Xs = FnCall F' Xs') = (F=F' & Xs=Xs')" 
   382 proof
   383   assume "FnCall F Xs = FnCall F' Xs'"
   384   hence "fun (FnCall F Xs) = fun (FnCall F' Xs')" 
   385     and "args (FnCall F Xs) = args (FnCall F' Xs')" by auto
   386   thus "F=F' & Xs=Xs'" by simp
   387 next
   388   assume "F=F' & Xs=Xs'" thus "FnCall F Xs = FnCall F' Xs'" by simp
   389 qed
   390 
   391 
   392 subsection{*The Abstract Discriminator*}
   393 text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
   394 function in order to prove discrimination theorems.*}
   395 
   396 definition
   397   discrim :: "exp \<Rightarrow> int" where
   398   "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
   399 
   400 lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
   401 by (auto simp add: congruent_def exprel_imp_eq_freediscrim) 
   402 
   403 text{*Now prove the four equations for @{term discrim}*}
   404 
   405 lemma discrim_Var [simp]: "discrim (Var N) = 0"
   406 by (simp add: discrim_def Var_def 
   407               UN_equiv_class [OF equiv_exprel discrim_respects]) 
   408 
   409 lemma discrim_Plus [simp]: "discrim (Plus X Y) = 1"
   410 apply (cases X, cases Y) 
   411 apply (simp add: discrim_def Plus 
   412                  UN_equiv_class [OF equiv_exprel discrim_respects]) 
   413 done
   414 
   415 lemma discrim_FnCall [simp]: "discrim (FnCall F Xs) = 2"
   416 apply (rule_tac z=Xs in eq_Abs_ExpList) 
   417 apply (simp add: discrim_def FnCall
   418                  UN_equiv_class [OF equiv_exprel discrim_respects]) 
   419 done
   420 
   421 
   422 text{*The structural induction rule for the abstract type*}
   423 theorem exp_inducts:
   424   assumes V:    "\<And>nat. P1 (Var nat)"
   425       and P:    "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)"
   426       and F:    "\<And>nat list. P2 list \<Longrightarrow> P1 (FnCall nat list)"
   427       and Nil:  "P2 []"
   428       and Cons: "\<And>exp list. \<lbrakk>P1 exp; P2 list\<rbrakk> \<Longrightarrow> P2 (exp # list)"
   429   shows "P1 exp" and "P2 list"
   430 proof -
   431   obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp)
   432   obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList)
   433   have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)"
   434   proof (induct U and Us rule: compat_freeExp.induct compat_freeExp_list.induct)
   435     case (VAR nat)
   436     with V show ?case by (simp add: Var_def) 
   437   next
   438     case (PLUS X Y)
   439     with P [of "Abs_Exp (exprel `` {X})" "Abs_Exp (exprel `` {Y})"]
   440     show ?case by (simp add: Plus) 
   441   next
   442     case (FNCALL nat list)
   443     with F [of "Abs_ExpList list"]
   444     show ?case by (simp add: FnCall) 
   445   next
   446     case Nil_freeExp
   447     with Nil show ?case by simp
   448   next
   449     case Cons_freeExp
   450     with Cons show ?case by simp
   451   qed
   452   with exp and list show "P1 exp" and "P2 list" by (simp_all only:)
   453 qed
   454 
   455 end