(*  Title:      HOL/Induct/QuoNestedDataType

     ID:         $Id$

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     Copyright   2004  University of Cambridge

 *)

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

 theory QuoNestedDataType = Main:

 subsection{*Defining the Free Algebra*}

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

 datatype

      freeExp = VAR  nat

 	     | PLUS  freeExp freeExp

 	     | FNCALL  nat "freeExp list"

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

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

 syntax

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

 syntax (xsymbols)

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

 syntax (HTML output)

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

 translations

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

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

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

 and transitivity.*}

 inductive "exprel"

   intros 

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

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

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

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

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

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

   monos listrel_mono

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

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

 apply (induct X and Xs)

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

 done

 lemmas exprel_refl = exprel_refl_conj [THEN conjunct1]

 lemmas list_exprel_refl = exprel_refl_conj [THEN conjunct2]

 theorem equiv_exprel: "equiv UNIV exprel"

 proof (simp add: equiv_def, intro conjI)

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

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

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

 qed

 theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"

 by (insert equiv_listrel [OF equiv_exprel], simp)

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

 apply (rule exprel.intros) 

 apply (rule listrel.intros) 

 done

 lemma FNCALL_Cons:

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

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

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

 subsection{*Some Functions on the Free Algebra*}

 subsubsection{*The Set of Variables*}

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

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

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

 of a free variable.*}

 consts

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

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

 primrec

    "freevars (VAR N) = {N}"

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

    "freevars (FNCALL F Xs) = freevars_list Xs"

    "freevars_list [] = {}"

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

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

 equivalence relation.  It also helps us prove that Variable

   (the abstract constructor) is injective*}

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

 apply (erule exprel.induct) 

 apply (erule_tac [4] listrel.induct) 

 apply (simp_all add: Un_assoc)

 done

 subsubsection{*Functions for Freeness*}

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

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

 primrec

    "freediscrim (VAR N) = 0"

    "freediscrim (PLUS X Y) = 1"

    "freediscrim (FNCALL F Xs) = 2"

 theorem exprel_imp_eq_freediscrim:

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

 by (erule exprel.induct, auto)

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

 prove part of the injectivity property for FnCall.*}

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

 primrec

    "freefun (VAR N) = 0"

    "freefun (PLUS X Y) = 0"

    "freefun (FNCALL F Xs) = F"

 theorem exprel_imp_eq_freefun:

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

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

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

 prove part of the injectivity property for FnCall.*}

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

 primrec

    "freeargs (VAR N) = []"

    "freeargs (PLUS X Y) = []"

    "freeargs (FNCALL F Xs) = Xs"

 theorem exprel_imp_eqv_freeargs:

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

 apply (erule exprel.induct)  

 apply (erule_tac [4] listrel.induct) 

 apply (simp_all add: listrel.intros)

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

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

 done

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

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

     by (auto simp add: quotient_def)

 text{*The abstract message constructors*}

 constdefs

   Var :: "nat \<Rightarrow> exp"

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

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

    "Plus X Y ==

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

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

    "FnCall F Xs ==

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

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

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

 lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I]

 declare equiv_exprel_iff [simp]

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

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

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

 lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp"

 apply (rule inj_on_inverseI)

 apply (erule Abs_Exp_inverse)

 done

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

 declare inj_on_Abs_Exp [THEN inj_on_iff, simp]

 declare Abs_Exp_inverse [simp]

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

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

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

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

 apply (drule arg_cong [where f=Abs_Exp])

 apply (auto simp add: Rep_Exp_inverse intro: exprel_refl)

 done

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

   list of concrete expressions*}

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

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

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

 by (simp add: Abs_ExpList_def)

 lemma Abs_ExpList_Cons [simp]:

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

 by (simp add: Abs_ExpList_def)

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

 apply (induct z)

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

 apply (auto simp add: Abs_ExpList_def intro: exprel_refl)

 done

 lemma eq_Abs_ExpList [case_names Abs_ExpList]:

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

 by (rule exE [OF ExpList_rep], blast) 

 subsubsection{*Characteristic Equations for the Abstract Constructors*}

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

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

 proof -

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

     by (simp add: congruent2_def exprel.PLUS)

   thus ?thesis

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

 qed

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

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

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

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

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

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

   by (simp add: FnCall_def)

 lemma FnCall_respects: 

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

   by (simp add: congruent_def exprel.FNCALL)

 lemma FnCall_sing:

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

 proof -

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

     by (simp add: congruent_def FNCALL_Cons listrel.intros)

   thus ?thesis

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

 qed

 lemma listset_Rep_Exp_Abs_Exp:

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

 by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def)

 lemma FnCall:

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

 proof -

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

     by (simp add: congruent_def exprel.FNCALL)

   thus ?thesis

     by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]

                   listset_Rep_Exp_Abs_Exp)

 qed

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

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

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

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

 constdefs

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

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

 lemma vars_respects: "freevars respects exprel"

 by (simp add: congruent_def exprel_imp_eq_freevars) 

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

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

 primrec

    "vars_list []    = {}"

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

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

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

 by (simp add: vars_def Var_def 

               UN_equiv_class [OF equiv_exprel vars_respects]) 

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

 apply (cases X, cases Y) 

 apply (simp add: vars_def Plus 

                  UN_equiv_class [OF equiv_exprel vars_respects]) 

 done

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

 apply (cases Xs rule: eq_Abs_ExpList) 

 apply (simp add: FnCall)

 apply (induct_tac Us) 

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

 done

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

 by simp

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

 by simp

 subsection{*Injectivity Properties of Some Constructors*}

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

 by (drule exprel_imp_eq_freevars, simp)

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

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

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

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

 by (drule exprel_imp_eq_freediscrim, simp)

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

 apply (cases X, cases Y) 

 apply (simp add: Var_def Plus) 

 apply (blast dest: VAR_neqv_PLUS) 

 done

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

 apply (cases Xs rule: eq_Abs_ExpList) 

 apply (auto simp add: FnCall Var_def)

 apply (drule exprel_imp_eq_freediscrim, simp)

 done

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

 constdefs

   fun :: "exp \<Rightarrow> nat"

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

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

 by (simp add: congruent_def exprel_imp_eq_freefun) 

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

 apply (cases Xs rule: eq_Abs_ExpList) 

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

 done

 constdefs

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

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

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

 relations, but with little benefit here.*}

 lemma Abs_ExpList_eq:

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

 by (erule listrel.induct, simp_all)

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

 by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 

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

 apply (cases Xs rule: eq_Abs_ExpList) 

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

 done

 lemma FnCall_FnCall_eq [iff]:

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

 proof

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

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

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

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

 next

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

 qed

 subsection{*The Abstract Discriminator*}

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

 function in order to prove discrimination theorems.*}

 constdefs

   discrim :: "exp \<Rightarrow> int"

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

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

 by (simp add: congruent_def exprel_imp_eq_freediscrim) 

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

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

 by (simp add: discrim_def Var_def 

               UN_equiv_class [OF equiv_exprel discrim_respects]) 

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

 apply (cases X, cases Y) 

 apply (simp add: discrim_def Plus 

                  UN_equiv_class [OF equiv_exprel discrim_respects]) 

 done

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

 apply (rule_tac z=Xs in eq_Abs_ExpList) 

 apply (simp add: discrim_def FnCall

                  UN_equiv_class [OF equiv_exprel discrim_respects]) 

 done

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

 theorem exp_induct:

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

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

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

       and Nil:  "P2 []"

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

   shows "P1 exp & P2 list"

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

   fix U Us

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

         P2 (Abs_ExpList Us)"

   proof (induct U and Us)

     case (VAR nat) 

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

   next

     case (PLUS X Y)

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

     show ?case by (simp add: Plus) 

   next

     case (FNCALL nat list)

     with F [of "Abs_ExpList list"]

     show ?case by (simp add: FnCall) 

   next

     case Nil_freeExp

     with Nil show ?case by simp

   next

     case Cons_freeExp

      with Cons

     show ?case by simp

   qed

 qed

 end