# Theory CoinductiveLemmas

```theory CoinductiveLemmas imports Coinductive.Coinductive_List begin

lemma lSup_lappend:
"⟦Complete_Partial_Order.chain lprefix A; A ≠ {}⟧
⟹ lSup (lappend xs ` A) = lappend xs (lSup A)"
apply (induct xs; clarsimp)
defer
apply (subst image_image[symmetric, where f="λx. LCons _ x"])
apply (clarsimp simp: lSup_LCons)
apply (clarsimp simp: ccpo.admissible_def)
apply (rename_tac B)
apply (case_tac "lfinite (lSup B)")
defer
apply (rule lprefix_antisym)
apply (rule chain_lSup_lprefix)
apply (rule chainI)
apply (fastforce simp: lappend_inf)
apply clarsimp
apply (rule chain_lprefix_lSup)
apply (rule chainI)
apply (fastforce simp: lappend_inf)
apply (fastforce simp: lappend_inf)
apply (erule lfinite_rev_induct)
apply clarsimp
by (metis mcont_contD mcont_lappend2)

lemma lSup_lmap:
"⟦Complete_Partial_Order.chain lprefix A; A ≠ {}⟧
⟹ lSup ((lmap f) ` A) = lmap f (lSup A)"
by (metis mcont_contD mcont_lmap)

lemma lSup_lconcat:
"⟦Complete_Partial_Order.chain lprefix A; A ≠ {}⟧
⟹ lSup (lconcat ` A) = lconcat (lSup A)"
by (metis mcont_contD mcont_lconcat)

lemma cpo_llist_of_upt:
"Complete_Partial_Order.chain lprefix {x. ∃i. x = llist_of [0..<i]}"
apply (rule chainI)
apply clarsimp
apply (rename_tac i i')
apply (case_tac "i ≤ i'")
apply (simp (no_asm) add: prefix_def)
apply (rule_tac x="[i..<i']" in exI)
using le_Suc_ex upt_add_eq_append apply blast
apply (simp add: not_le)
apply (erule notE)
apply (drule less_imp_le)
apply (simp (no_asm) add: prefix_def)
apply (rule_tac x="[i'..<i]" in exI)
using le_Suc_ex upt_add_eq_append by blast

lemma iterates_Suc_is_lSup_upt:
"iterates Suc 0 = lSup {x. ∃i. x = llist_of [0..<i]}"
proof (coinduct rule : llist.coinduct
[where R="λx y. ltl x = lmap Suc x ∧ ltl y = lmap Suc y ∧ lnull x = lnull y
∧ lhd x = lhd y"])
case Eq_llist
then show ?case
apply (rule conjI)
apply (simp add: lmap_iterates)
apply (subst lSup_lmap[symmetric, OF cpo_llist_of_upt])
apply fastforce
apply clarsimp
apply (rule conjI)
apply (rule arg_cong[where f=lSup])
apply (rule equalityI; clarsimp simp: subset_iff image_def)
apply (metis Suc_pred lmap_llist_of map_Suc_upt)
apply (rename_tac i)
apply (rule_tac x="llist_of [0..<Suc i]" in bexI)
apply (metis ltl_llist_of map_Suc_upt tl_upt)
apply fastforce
apply (rule conjI)
apply fastforce
apply (simp add: lSup.code)
apply (rule conjI; clarsimp)
apply (metis lnull_llist_of neq0_conv not_less upt_eq_Nil_conv)
apply (rename_tac i)
apply (rule the_equality; clarsimp simp: image_def)
apply (rule_tac x="llist_of [0..<i]" in bexI, clarsimp)
apply fastforce
done
qed simp

abbreviation (input) flat :: "'a list llist ⇒ 'a llist" where
"flat xs ≡ lconcat (lmap llist_of xs)"

lemma flat_inf_llist_lSup:
"flat (inf_llist f) = lSup {x. ∃i. x = llist_of (concat (map f [0..<i]))}"
apply (clarsimp simp: Coinductive_List.inf_llist_def)
apply (subst iterates_Suc_is_lSup_upt)
apply clarsimp
apply (subst lSup_lmap[symmetric, OF cpo_llist_of_upt])
apply fastforce
apply (clarsimp simp: image_def)
apply (subst lSup_lmap[symmetric])
apply (rule chainI)
apply clarsimp
apply (metis (mono_tags, lifting) chain_def cpo_llist_of_upt lprefix_llist_of map_mono_prefix
mem_Collect_eq)
apply fastforce
apply (clarsimp simp add: lconcat_llist_of[symmetric])
apply (subst lmap_llist_of[symmetric])
apply (subst llist.map_comp[symmetric])
apply (subst lSup_lconcat[symmetric])
apply (rule chainI)
apply clarsimp
using cpo_llist_of_upt
apply (metis (no_types, opaque_lifting) le_Suc_ex less_imp_add_positive map_mono_prefix
not_less prefix_def upt_add_eq_append zero_le)
apply fastforce
apply (rule arg_cong[of _ _ lSup])
apply (fastforce simp: image_def)
done

lemma upper_subset_lSup_eq:
"⟦Complete_Partial_Order.chain lprefix B; A ⊆ B;
∀x∈B. ∃y∈A. lprefix x y⟧ ⟹ lSup B = lSup A"
apply (rule lprefix_antisym)
apply (rule chain_lSup_lprefix, simp)
apply (rename_tac xs)
apply (drule_tac x=xs in bspec, simp)
apply (meson chain_subset less_imp_le llist.lub_upper lprefix_trans)
apply (rule chain_lSup_lprefix)
using chain_subset apply blast
using llist.lub_upper by blast

lemma lmap_iterates_id:
"lmap (λz. x) (iterates Suc 0) = iterates id x"
apply coinduction
apply (simp add: lmap_iterates[symmetric] llist.map_comp)
done

end
```