<commit_before>(*  Title:      HOLCF/ex/Stream_adm.thy
    ID:         $Id$
    Author:     <NAME>, <NAME>
*)

header {* Admissibility for streams *}

theory Stream_adm
imports "../ex/Stream" Continuity
begin

definition
  stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
  "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
                    (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))"

definition
  stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
  "stream_antiP F = (\<forall>P x. \<exists>Q i.
                (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
                (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
                (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))"

definition
  antitonP :: "'a set => bool" where
  "antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)"


(* ----------------------------------------------------------------------- *)

section "admissibility"

lemma flatstream_adm_lemma:
  assumes 1: "Porder.chain Y"
  assumes 2: "!i. P (Y i)"
  assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
  ==> P(lub (range Y)))"
  shows "P(lub (range Y))"
apply (rule increasing_chain_adm_lemma [OF 1 2])
apply (erule 3, assumption)
apply (erule thin_rl)
apply (rule allI)
apply (case_tac "!j. stream_finite (Y j)")
apply ( rule chain_incr)
apply ( rule allI)
apply ( drule spec)
apply ( safe)
apply ( rule exI)
apply ( rule slen_strict_mono)
apply (   erule spec)
apply (  assumption)
apply ( assumption)
apply (drule not_ex [THEN iffD1])
apply (subst slen_infinite)
apply (erule thin_rl)
apply (drule spec)
apply (unfold linorder_not_less)
apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]])
apply (simp)
done


(* should be without reference to stream length? *)
lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); 
 !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P"
apply (unfold adm_def)
apply (intro strip)
apply (erule (1) flatstream_adm_lemma)<commit_msg>Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification.<commit_after>(*  Title:      HOLCF/ex/Stream_adm.thy
    ID:         $Id$
    Author:     <NAME>, <NAME>
*)

header {* Admissibility for streams *}

theory Stream_adm
imports "../ex/Stream" Continuity
begin

definition
  stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
  "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
                    (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))"

definition
  stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
  "stream_antiP F = (\<forall>P x. \<exists>Q i.
                (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
                (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
                (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))"

definition
  antitonP :: "'a set => bool" where
  "antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)"


(* ----------------------------------------------------------------------- *)

section "admissibility"

lemma flatstream_adm_lemma:
  assumes 1: "Porder.chain Y"
  assumes 2: "!i. P (Y i)"
  assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
  ==> P(lub (range Y)))"
  shows "P(lub (range Y))"
apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2])
apply (erule 3, assumption)
apply (erule thin_rl)
apply (rule allI)
apply (case_tac "!j. stream_finite (Y j)")
apply ( rule chain_incr)
apply ( rule allI)
apply ( drule spec)
apply ( safe)
apply ( rule exI)
apply ( rule slen_strict_mono)
apply (   erule spec)
apply (  assumption)
apply ( assumption)
apply (drule not_ex [THEN iffD1])
apply (subst slen_infinite)
apply (erule thin_rl)
apply (drule spec)
apply (unfold linorder_not_less)
apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]])
apply (simp)
done


(* should be without reference to stream length? *)
lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); 
 !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P"
apply (unfold adm_def)
apply (intro strip)
apply (erule (1) flatstream_adm_lemma)
{'fraction_non_alphanumeric': 0.2016945649927671, 'fraction_numerical': 0.0037197768133911966, 'mean_word_length': 3.056999161777033, 'pattern_counts': {'":': 0, '<': 99, '<?xml version=': 0, '>': 99, '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': '4308234', 'n_tokens_mistral': 1891, 'n_tokens_neox': 1731, 'n_words': 569}