Theory QuoNestedDataType

(*  Title:      HOL/Induct/QuoNestedDataType.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   2004  University of Cambridge
*)

section‹Quotienting a Free Algebra Involving Nested Recursion›

text ‹This is the development promised in Lawrence Paulson's paper ``Defining functions on equivalence classes''
\emph{ACM Transactions on Computational Logic} \textbf{7}:40 (2006), 658--675,
illustrating bare-bones quotient constructions. Any comparison using lifting and transfer
should be done in a separate theory.›

theory QuoNestedDataType imports Main begin

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"

datatype_compat freeExp

text‹The equivalence relation, which makes PLUS associative.›

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_set
  exprel :: "(freeExp * freeExp) set"
  and exp_rel :: "[freeExp, freeExp] => bool"  (infixl "∼" 50)
  where
    "X ∼ Y ≡ (X,Y) ∈ exprel"
  | ASSOC: "PLUS X (PLUS Y Z) ∼ PLUS (PLUS X Y) Z"
  | VAR: "VAR N ∼ VAR N"
  | PLUS: "⟦X ∼ X'; Y ∼ Y'⟧ ⟹ PLUS X Y ∼ PLUS X' Y'"
  | FNCALL: "(Xs,Xs') ∈ listrel exprel ⟹ FNCALL F Xs ∼ FNCALL F Xs'"
  | SYM:   "X ∼ Y ⟹ Y ∼ X"
  | TRANS: "⟦X ∼ Y; Y ∼ Z⟧ ⟹ X ∼ Z"
  monos listrel_mono


text‹Proving that it is an equivalence relation›

lemma exprel_refl: "X ∼ X"
  and list_exprel_refl: "(Xs,Xs) ∈ listrel(exprel)"
  by (induct X and Xs rule: compat_freeExp.induct compat_freeExp_list.induct)
    (blast intro: exprel.intros listrel.intros)+

theorem equiv_exprel: "equiv UNIV exprel"
proof -
  have "refl exprel" by (simp add: refl_on_def exprel_refl)
  moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
  moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
  ultimately show ?thesis by (simp add: equiv_def)
qed

theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"
  using equiv_listrel [OF equiv_exprel] by simp

lemma FNCALL_Cons:
  "⟦X ∼ X'; (Xs,Xs') ∈ listrel(exprel)⟧ ⟹ FNCALL F (X#Xs) ∼ 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 algebra, 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.›
primrec freevars :: "freeExp ⇒ nat set" and freevars_list :: "freeExp list ⇒ nat set"
  where
  "freevars (VAR N) = {N}"
| "freevars (PLUS X Y) = freevars X ∪ freevars Y"
| "freevars (FNCALL F Xs) = freevars_list Xs"

| "freevars_list [] = {}"
| "freevars_list (X # Xs) = freevars X ∪ 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 ∼ V ⟹ freevars U = freevars V"
proof (induct set: exprel)
  case (FNCALL Xs Xs' F)
  then show ?case
    by (induct rule: listrel.induct) auto
qed (simp_all add: Un_assoc)


subsubsection‹Functions for Freeness›

text‹A discriminator function to distinguish vars, sums and function calls›
primrec freediscrim :: "freeExp ⇒ int" where
  "freediscrim (VAR N) = 0"
| "freediscrim (PLUS X Y) = 1"
| "freediscrim (FNCALL F Xs) = 2"

theorem exprel_imp_eq_freediscrim:
     "U ∼ V ⟹ freediscrim U = freediscrim V"
  by (induct set: exprel) auto


text‹This function, which returns the function name, is used to
prove part of the injectivity property for FnCall.›
primrec freefun :: "freeExp ⇒ nat" where
  "freefun (VAR N) = 0"
| "freefun (PLUS X Y) = 0"
| "freefun (FNCALL F Xs) = F"

theorem exprel_imp_eq_freefun:
     "U ∼ V ⟹ freefun U = freefun V"
  by (induct set: exprel) (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.›
primrec freeargs :: "freeExp ⇒ freeExp list" where
  "freeargs (VAR N) = []"
| "freeargs (PLUS X Y) = []"
| "freeargs (FNCALL F Xs) = Xs"


theorem exprel_imp_eqv_freeargs:
  assumes "U ∼ V"
  shows "(freeargs U, freeargs V) ∈ listrel exprel"
  using assms
proof induction
  case (FNCALL Xs Xs' F)
  then show ?case
    by (simp add: listrel_iff_nth)
next
  case (SYM X Y)
  then show ?case
    by (meson equivE equiv_list_exprel symD)
next
  case (TRANS X Y Z)
  then show ?case
    by (meson equivE equiv_list_exprel transD)
qed (use listrel.simps in auto)


subsection‹The Initial Algebra: A Quotiented Message Type›

definition "Exp = UNIV//exprel"

typedef exp = Exp
  morphisms Rep_Exp Abs_Exp
  unfolding Exp_def by (auto simp add: quotient_def)

text‹The abstract message constructors›

definition
  Var :: "nat ⇒ exp" where
  "Var N = Abs_Exp(exprel``{VAR N})"

definition
  Plus :: "[exp,exp] ⇒ exp" where
   "Plus X Y =
       Abs_Exp (⋃U ∈ Rep_Exp X. ⋃V ∈ Rep_Exp Y. exprel``{PLUS U V})"

definition
  FnCall :: "[nat, exp list] ⇒ exp" where
   "FnCall F Xs =
       Abs_Exp (⋃Us ∈ 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) ∈ 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 exprel_in_Exp [simp]: "exprel``{U} ∈ Exp"
  by (simp add: Exp_def quotientI)

lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp"
  by (meson Abs_Exp_inject inj_onI)

text‹Reduces equality on abstractions to equality on representatives›
declare inj_on_Abs_Exp [THEN inj_on_eq_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"
  by (metis Abs_Exp_cases Exp_def quotientE)


subsection‹Every list of abstract expressions can be expressed in terms of a
  list of concrete expressions›

definition
  Abs_ExpList :: "freeExp list => exp list" where
  "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: "∃Us. z = Abs_ExpList Us"
  by (smt (verit, del_insts) Abs_ExpList_def eq_Abs_Exp ex_map_conv)


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 "(λU V. exprel``{PLUS U V}) respects2 exprel"
    by (auto 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, ‹FnCall_Cons›.›
lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})"
  by (simp add: FnCall_def)

lemma FnCall_respects: 
     "(λUs. exprel``{FNCALL F Us}) respects (listrel exprel)"
  by (auto simp add: congruent_def exprel.FNCALL)

lemma FnCall_sing:
     "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"
proof -
  have "(λU. exprel``{FNCALL F [U]}) respects exprel"
    by (auto 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 Us) (simp_all add: listrel_Cons Abs_ExpList_def)

lemma FnCall:
     "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
proof -
  have "(λUs. exprel``{FNCALL F Us}) respects (listrel exprel)"
    by (auto 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›

definition
  vars :: "exp ⇒ nat set" where "vars X ≡ (⋃U ∈ Rep_Exp X. freevars U)"

lemma vars_respects: "freevars respects exprel"
by (auto simp add: congruent_def exprel_imp_eq_freevars) 

text‹The extension of the function \<^term>‹vars› to lists›
primrec vars_list :: "exp list ⇒ nat set" where
  "vars_list []    = {}"
| "vars_list(E#Es) = vars E ∪ 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 ∪ vars Y"
proof -
  have "⋀U V. ⟦X = Abs_Exp (exprel``{U}); Y = Abs_Exp (exprel``{V})⟧
               ⟹ vars (Plus X Y) = vars X ∪ vars Y"
    by (simp add: vars_def Plus UN_equiv_class [OF equiv_exprel vars_respects]) 
  then show ?thesis
    by (meson eq_Abs_Exp)
qed

lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs"
proof -
  have "vars (Abs_Exp (exprel``{FNCALL F Us})) = vars_list (Abs_ExpList Us)" for Us
    by (induct Us) (auto simp: vars_def UN_equiv_class [OF equiv_exprel vars_respects])
  then show ?thesis
    by (metis ExpList_rep FnCall)
qed

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

lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X ∪ vars_list Xs"
  by simp


subsection‹Injectivity Properties of Some Constructors›

lemma VAR_imp_eq: "VAR m ∼ VAR n ⟹ 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 ∼ PLUS X Y ⟹ False"
  using exprel_imp_eq_freediscrim by force

theorem Var_neq_Plus [iff]: "Var N ≠ Plus X Y"
proof -
  have "⋀U V. ⟦X = Abs_Exp (exprel``{U}); Y = Abs_Exp (exprel``{V})⟧ ⟹ Var N ≠ Plus X Y"
    using Plus VAR_neqv_PLUS Var_def by force
  then show ?thesis
    by (meson eq_Abs_Exp)
qed

theorem Var_neq_FnCall [iff]: "Var N ≠ FnCall F Xs"
proof -
  have "⋀Us. Var N ≠ FnCall F (Abs_ExpList Us)"
    using FnCall Var_def exprel_imp_eq_freediscrim by fastforce
  then show ?thesis
    by (metis ExpList_rep)
qed

subsection‹Injectivity of \<^term>‹FnCall››

definition
  "fun" :: "exp ⇒ nat"
  where "fun X ≡ the_elem (⋃U ∈ Rep_Exp X. {freefun U})"

lemma fun_respects: "(λU. {freefun U}) respects exprel"
  by (auto simp add: congruent_def exprel_imp_eq_freefun) 

lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"
proof -
  have "⋀Us. fun (FnCall F (Abs_ExpList Us)) = F"
    using FnCall UN_equiv_class [OF equiv_exprel] fun_def fun_respects by fastforce
  then show ?thesis
    by (metis ExpList_rep)
qed

definition
  args :: "exp ⇒ exp list" where
  "args X = the_elem (⋃U ∈ 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) ∈ listrel exprel ⟹ Abs_ExpList (y) = Abs_ExpList (z)"
  by (induct set: listrel) simp_all

lemma args_respects: "(λU. {Abs_ExpList (freeargs U)}) respects exprel"
  by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) 

lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"
proof -
  have "⋀Us. Xs = Abs_ExpList Us ⟹ args (FnCall F Xs) = Xs"
    by (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects])
  then show ?thesis
    by (metis ExpList_rep)
qed

lemma FnCall_FnCall_eq [iff]: "(FnCall F Xs = FnCall F' Xs') ⟷ (F=F' ∧ Xs=Xs')"
  by (metis args_FnCall fun_FnCall) 


subsection‹The Abstract Discriminator›
text‹However, as ‹FnCall_Var_neq_Var› illustrates, we don't need this
function in order to prove discrimination theorems.›

definition
  discrim :: "exp ⇒ int" where
  "discrim X = the_elem (⋃U ∈ Rep_Exp X. {freediscrim U})"

lemma discrim_respects: "(λU. {freediscrim U}) respects exprel"
by (auto 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"
proof -
  have "⋀U V. ⟦X = Abs_Exp (exprel``{U}); Y = Abs_Exp (exprel``{V})⟧ ⟹ discrim (Plus X Y) = 1"
    by (simp add: discrim_def Plus  UN_equiv_class [OF equiv_exprel discrim_respects]) 
  then show ?thesis
    by (meson eq_Abs_Exp)
qed

lemma discrim_FnCall [simp]: "discrim (FnCall F Xs) = 2"
proof -
  have "discrim (FnCall F (Abs_ExpList Us)) = 2" for Us
    by (simp add: discrim_def FnCall UN_equiv_class [OF equiv_exprel discrim_respects]) 
  then show ?thesis
    by (metis ExpList_rep)
qed

text‹The structural induction rule for the abstract type›
theorem exp_inducts:
  assumes V:    "⋀nat. P1 (Var nat)"
      and P:    "⋀exp1 exp2. ⟦P1 exp1; P1 exp2⟧ ⟹ P1 (Plus exp1 exp2)"
      and F:    "⋀nat list. P2 list ⟹ P1 (FnCall nat list)"
      and Nil:  "P2 []"
      and Cons: "⋀exp list. ⟦P1 exp; P2 list⟧ ⟹ P2 (exp # list)"
  shows "P1 exp" and "P2 list"
proof -
  obtain U where exp: "exp = (Abs_Exp (exprel``{U}))" by (cases exp)
  obtain Us where list: "list = Abs_ExpList Us" by (metis ExpList_rep)
  have "P1 (Abs_Exp (exprel``{U}))" and "P2 (Abs_ExpList Us)"
  proof (induct U and Us rule: compat_freeExp.induct compat_freeExp_list.induct)
    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
  with exp and list show "P1 exp" and "P2 list" by (simp_all only:)
qed

end