Theory QuoNestedDataType

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

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 (rule equivI)
show "refl exprel" by (simp add: refl_on_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)"
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

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
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"

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 [] = []"

lemma Abs_ExpList_Cons [simp]:
"Abs_ExpList (X#Xs) = Abs_Exp (exprel{X}) # Abs_ExpList Xs"

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 []})"

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}"
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