Theory QuoNestedDataType

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


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

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"

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) (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_Nil: "FNCALL F [] ∼ FNCALL F []"
apply (rule exprel.intros)
apply (rule listrel.intros)
done

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 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.*}

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"
apply (induct set: exprel)
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*}
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"
proof -
from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE)
from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE)
from assms show ?thesis
apply induct
apply (erule_tac [4] listrel.induct)
apply (simp_all add: listrel.intros)
apply (blast intro: symD [OF sym])
apply (blast intro: transD [OF trans])
done
qed


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 (\<Union>U ∈ Rep_Exp X. \<Union>V ∈ Rep_Exp Y. exprel``{PLUS U V})"


definition
FnCall :: "[nat, exp list] => exp" where
"FnCall F Xs =
Abs_Exp (\<Union>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 [simp]: "exprel``{U} ∈ 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*}


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"
apply (induct z)
apply (rule_tac [2] z=a in eq_Abs_Exp)
apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv 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 "(λ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, @{text 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 = (\<Union>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"
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 ∪ 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"
by (drule exprel_imp_eq_freediscrim, simp)

theorem Var_neq_Plus [iff]: "Var N ≠ 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 ≠ 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}*}

definition
"fun" :: "exp => nat" where
"fun X = the_elem (\<Union>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"
apply (cases Xs rule: eq_Abs_ExpList)
apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects])
done

definition
args :: "exp => exp list" where
"args X = the_elem (\<Union>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"
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.*}


definition
discrim :: "exp => int" where
"discrim X = the_elem (\<Union>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"
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_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 (rule eq_Abs_ExpList)
have "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
with exp and list show "P1 exp" and "P2 list" by (simp_all only:)
qed

end