<commit_before>(*  Title:      Codatatype_Examples/Process.thy
    Author:     <NAME>, TU Muenchen
    Copyright   2012

Processes.
*)

header {* Processes *}

theory Process
imports "../Codatatype"
begin

codata 'a process =
  isAction: Action (prefOf: 'a) (contOf: "'a process") |
  isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")

(* Read: prefix of, continuation of, choice 1 of, choice 2 of *)

section {* Customization *}

subsection {* Basic properties *}

declare
  process.inject[simp]
  process.distinct[simp]
  process.discs[simp]
  process.sels[simp]
  process.collapse[simp]
  pre_process.pred_unfold[simp]

lemmas process_exhaust =
  process.exhaust[elim, case_names Action Choice]

(* Constructors versus discriminators *)
theorem isAction_isChoice:
"isAction p \<or> isChoice p"
by (rule process.disc_exhaust) auto

theorem not_isAction_isChoice: "\<not> (isAction p \<and> isChoice p)"
by (cases rule: process_exhaust[of p]) auto


subsection{* Coinduction *}

theorem process_coind[elim, consumes 1, case_names iss Action Choice, induct pred: "HOL.eq"]:
assumes phi: "\<phi> p p'" and
iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> \<phi> p p'" and
Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
shows "p = p'"
proof(intro mp[OF process.pred_coinduct, of \<phi>, OF _ phi], clarify)
  fix p p'  assume \<phi>: "\<phi> p p'"
  show "pre_process_pred (op =) \<phi> (process_unf p) (process_unf p')"
  proof(cases rule: process_exhaust[of p])
    case (Action a q) note p = Action
    hence "isAction p'" using iss[OF \<phi>] by (cases rule: process_exhaust[of p'], auto)
    then obtain a' q' where p': "p' = Action a' q'" by (cases rule: process_exhaust[of p'], auto)
    have 0: "a = a' \<and> \<phi> q q'" using Act[OF \<phi>[unfolded p p']] .
    have unf: "process_unf p = Inl (a,q)" "process_unf p' = Inl (a',q')"
    unfolding p p' Action_def process.unf_fld by simp_all
    show ?thesis using 0 unfolding unf by simp
  next
    case (Choice p1 p2) note p = Choice
    hence "isChoice p'" using iss[OF \<phi>] by (cases rule: process_exhaust[of p'], auto)
    then obtain p1' p2' where p': "p' = Choice p1' p2'"
    by (cases rule: process_exhaust[of p'], auto)
    have 0: "\<phi> p1 p1' \<and> \<phi> p2 p2'" using Ch[OF \<phi>[unfolded p p']] .
    have unf: "process_unf p = Inr (p1,p2)" "process_unf p' = Inr (p1',p2')"
    unfolding p p' Choice_def process.unf_fld by simp_all
    show ?thesis using 0 unfolding unf by simp
  qed
qed

(* Stronger coinduction, up to equality: *)
theorem process_coind_upto[elim, consumes 1, case_names iss Action Choice]:
assumes phi: "\<phi> p p'" and
iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> (\<phi> p p' \<or> p = p')" and
Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
shows "p = p'"
proof(intro mp[OF process.pred_coinduct_upto, of \<phi>, OF _ phi], clarify)
  fix p p'  assume \<phi>: "\<phi> p p'"
  show "pre_process_pred (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_unf p) (process_unf p')"
  proof(cases rule: process_exhaust[of p])
    case (Action a q) note p = Action
    hence "isAction p'" using iss[OF \<phi>] by (cases rule: process_exhaust[of p'], auto)
    then obtain a' q' where p': "p' = Action a' q'" by (cases rule: process_exhaust[of p'], auto)
    have 0: "a = a' \<and> (\<phi> q q' \<or> q = q')" using Act[OF \<phi>[unfolded p p']] .
    have unf: "process_unf p = Inl (a,q)" "process_unf p' = Inl (a',q')"
    unfolding p p' Action_def process.unf_fld by simp_all
    show ?thesis using 0 unfolding unf by simp
  next
    case (Choice p1 p2) note p = Choice
    hence "isChoice p'" using iss[OF \<phi>] by (cases rule: process_exhaust[of p'], auto)
    then obtain p1' p2' where p': "p' = Choice p1' p2'"
    by (cases rule: process_exhaust[of p'], auto)
    have 0: "(\<phi> p1 p1' \<or> p1 = p1') \<and> (\<phi> p2 p2' \<or> p2 = p2')" using Ch[OF \<phi>[unfolded p p']] .
    have unf: "process_unf p = Inr (p1,p2)" "process_unf p' = Inr (p1',p2')"
    unfolding p p' Choice_def process.unf_fld by simp_all
    show ?thesis using 0 unfolding unf by simp
  qed
qed


subsection {* Coiteration *}


section{* Coinductive definition of the notion of trace *}

(* Say we have a type of streams: *)<commit_msg>adapted example<commit_after>(*  Title:      Codatatype_Examples/Process.thy
    Author:     <NAME>, TU Muenchen
    Copyright   2012

Processes.
*)

header {* Processes *}

theory Process
imports "../Codatatype"
begin

codata 'a process =
  isAction: Action (prefOf: 'a) (contOf: "'a process") |
  isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")

(* Read: prefix of, continuation of, choice 1 of, choice 2 of *)

section {* Customization *}

subsection {* Basic properties *}

declare pre_process.pred_unfold[simp]

(* Constructors versus discriminators *)
theorem isAction_isChoice:
"isAction p \<or> isChoice p"
by (rule process.disc_exhaust) auto

theorem not_isAction_isChoice: "\<not> (isAction p \<and> isChoice p)"
by (cases rule: process.exhaust[of p]) auto


subsection{* Coinduction *}

theorem process_coind[elim, consumes 1, case_names iss Action Choice, induct pred: "HOL.eq"]:
assumes phi: "\<phi> p p'" and
iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> \<phi> p p'" and
Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
shows "p = p'"
proof(intro mp[OF process.pred_coinduct, of \<phi>, OF _ phi], clarify)
  fix p p'  assume \<phi>: "\<phi> p p'"
  show "pre_process_pred (op =) \<phi> (process_unf p) (process_unf p')"
  proof(cases rule: process.exhaust[of p])
    case (Action a q) note p = Action
    hence "isAction p'" using iss[OF \<phi>] by (cases rule: process.exhaust[of p'], auto)
    then obtain a' q' where p': "p' = Action a' q'" by (cases rule: process.exhaust[of p'], auto)
    have 0: "a = a' \<and> \<phi> q q'" using Act[OF \<phi>[unfolded p p']] .
    have unf: "process_unf p = Inl (a,q)" "process_unf p' = Inl (a',q')"
    unfolding p p' Action_def process.unf_fld by simp_all
    show ?thesis using 0 unfolding unf by simp
  next
    case (Choice p1 p2) note p = Choice
    hence "isChoice p'" using iss[OF \<phi>] by (cases rule: process.exhaust[of p'], auto)
    then obtain p1' p2' where p': "p' = Choice p1' p2'"
    by (cases rule: process.exhaust[of p'], auto)
    have 0: "\<phi> p1 p1' \<and> \<phi> p2 p2'" using Ch[OF \<phi>[unfolded p p']] .
    have unf: "process_unf p = Inr (p1,p2)" "process_unf p' = Inr (p1',p2')"
    unfolding p p' Choice_def process.unf_fld by simp_all
    show ?thesis using 0 unfolding unf by simp
  qed
qed

(* Stronger coinduction, up to equality: *)
theorem process_coind_upto[elim, consumes 1, case_names iss Action Choice]:
assumes phi: "\<phi> p p'" and
iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> (\<phi> p p' \<or> p = p')" and
Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
shows "p = p'"
proof(intro mp[OF process.pred_coinduct_upto, of \<phi>, OF _ phi], clarify)
  fix p p'  assume \<phi>: "\<phi> p p'"
  show "pre_process_pred (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_unf p) (process_unf p')"
  proof(cases rule: process.exhaust[of p])
    case (Action a q) note p = Action
    hence "isAction p'" using iss[OF \<phi>] by (cases rule: process.exhaust[of p'], auto)
    then obtain a' q' where p': "p' = Action a' q'" by (cases rule: process.exhaust[of p'], auto)
    have 0: "a = a' \<and> (\<phi> q q' \<or> q = q')" using Act[OF \<phi>[unfolded p p']] .
    have unf: "process_unf p = Inl (a,q)" "process_unf p' = Inl (a',q')"
    unfolding p p' Action_def process.unf_fld by simp_all
    show ?thesis using 0 unfolding unf by simp
  next
    case (Choice p1 p2) note p = Choice
    hence "isChoice p'" using iss[OF \<phi>] by (cases rule: process.exhaust[of p'], auto)
    then obtain p1' p2' where p': "p' = Choice p1' p2'"
    by (cases rule: process.exhaust[of p'], auto)
    have 0: "(\<phi> p1 p1' \<or> p1 = p1') \<and> (\<phi> p2 p2' \<or> p2 = p2')" using Ch[OF \<phi>[unfolded p p']] .
    have unf: "process_unf p = Inr (p1,p2)" "process_unf p' = Inr (p1',p2')"
    unfolding p p' Choice_def process.unf_fld by simp_all
    show ?thesis using 0 unfolding unf by simp
  qed
qed


subsection {* Coiteration *}


section{* Coinductive definition of the notion of trace *}

(* Say we have a type of streams: *)
{'fraction_non_alphanumeric': 0.16969243912857754, 'fraction_numerical': 0.010679196924391286, 'mean_word_length': 3.640733399405352, 'pattern_counts': {'":': 0, '<': 151, '<?xml version=': 0, '>': 151, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5094121', 'n_tokens_mistral': 3777, 'n_tokens_neox': 3559, 'n_words': 1302}