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