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