text:
(*  Title:      ZF/Finite.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

prove:  b \<in> Fin(A) \<Longrightarrow> inj(b,b) \<subseteq> surj(b,b)
*)

section\<open>Finite Powerset Operator and Finite Function Space\<close>

theory Finite imports Inductive Epsilon Nat begin

(*The natural numbers as a datatype*)
rep_datatype
  elimination    natE
  induction      nat_induct
  case_eqns      nat_case_0 nat_case_succ
  recursor_eqns  recursor_0 recursor_succ

consts
  Fin       :: "i\<Rightarrow>i"
  FiniteFun :: "[i,i]\<Rightarrow>i"         (\<open>(_ -||>/ _)\<close> [61, 60] 60)

inductive
  domains   "Fin(A)" \<subseteq> "Pow(A)"
  intros
    emptyI:  "0 \<in> Fin(A)"
    consI:   "\<lbrakk>a \<in> A;  b \<in> Fin(A)\<rbrakk> \<Longrightarrow> cons(a,b) \<in> Fin(A)"
  type_intros  empty_subsetI cons_subsetI PowI
  type_elims   PowD [elim_format]

inductive
  domains   "FiniteFun(A,B)" \<subseteq> "Fin(A*B)"
  intros
    emptyI:  "0 \<in> A -||> B"
    consI:   "\<lbrakk>a \<in> A;  b \<in> B;  h \<in> A -||> B;  a \<notin> domain(h)\<rbrakk>
              \<Longrightarrow> cons(\<langle>a,b\<rangle>,h) \<in> A -||> B"
  type_intros Fin.intros

subsection \<open>Finite Powerset Operator\<close>

lemma Fin_mono: "A<=B \<Longrightarrow> Fin(A) \<subseteq> Fin(B)"
  unfolding Fin.defs
apply (rule lfp_mono)
apply (rule Fin.bnd_mono)+
apply blast
done

(* @{term"A \<in> Fin(B) \<Longrightarrow> A \<subseteq> B"} *)
lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD]

(** Induction on finite sets **)

(*Discharging @{term"x\<notin>y"} entails extra work*)
lemma Fin_induct [case_names 0 cons, induct set: Fin]:
    "\<lbrakk>b \<in> Fin(A);
        P(0);
        \<And>x y. \<lbrakk>x \<in> A;  y \<in> Fin(A);  x\<notin>y;  P(y)\<rbrakk> \<Longrightarrow> P(cons(x,y))
\<rbrakk> \<Longrightarrow> P(b)"
apply (erule Fin.induct, simp)
apply (case_tac "a \<in> b")
 apply (erule cons_absorb [THEN ssubst], assumption) (*backtracking!*)
apply simp
done

(** Simplification for Fin **)
declare Fin.intros [simp]

lemma Fin_0: "Fin(0) = {0}"
by (blast intro: Fin.emptyI dest: FinD)

(*The union of two finite sets is finite.*)
lemma Fin_UnI [simp]: "\<lbrakk>b \<in> Fin(A);  c \<in> Fin(A)\<rbrakk> \<Longrightarrow> b \<union> c \<in> Fin(A)"
apply (erule Fin_induct)
apply (simp_all add: Un_cons)
done

(*The union of a set of finite sets is finite.*)
lemma Fin_UnionI: "C \<in> Fin(Fin(A)) \<Longrightarrow> \<Union>(C) \<in> Fin(A)"
by (erule Fin_induct, simp_all)

(*Every subset of a finite set is finite.*)
lemma Fin_subset_lemma [rule_format]: "b \<in> Fin(A) \<Longrightarrow> \<forall>z. z<=b \<longrightarrow> z \<in> Fin(A)"
apply (erule Fin_induct)
apply (simp add: subset_empty_iff)
apply (simp add: subset_cons_iff distrib_simps, safe)
apply (erule_tac b = z in cons_Diff [THEN subst], simp)
done

lemma Fin_subset: "\<lbrakk>c<=b;  b \<in> Fin(A)\<rbrakk> \<Longrightarrow> c \<in> Fin(A)"
by (blast intro: Fin_subset_lemma)

lemma Fin_IntI1 [intro,simp]: "b \<in> Fin(A) \<Longrightarrow> b \<inter> c \<in> Fin(A)"
by (blast intro: Fin_subset)

lemma Fin_IntI2 [intro,simp]: "c \<in> Fin(A) \<Longrightarrow> b \<inter> c \<in> Fin(A)"
by (blast intro: Fin_subset)

lemma Fin_0_induct_lemma [rule_format]:
    "\<lbrakk>c \<in> Fin(A);  b \<in> Fin(A); P(b);
        \<And>x y. \<lbrakk>x \<in> A;  y \<in> Fin(A);  x \<in> y;  P(y)\<rbrakk> \<Longrightarrow> P(y-{x})
\<rbrakk> \<Longrightarrow> c<=b \<longrightarrow> P(b-c)"
apply (erule Fin_induct, simp)
apply (subst Diff_cons)
apply (simp add: cons_subset_iff Diff_subset [THEN Fin_subset])
done

lemma Fin_0_induct:
    "\<lbrakk>b \<in> Fin(A);
        P(b);
        \<And>x y. \<lbrakk>x \<in> A;  y \<in> Fin(A);  x \<in> y;  P(y)\<rbrakk> \<Longrightarrow> P(y-{x})
\<rbrakk> \<Longrightarrow> P(0)"
apply (rule Diff_cancel [THEN subst])
apply (blast intro: Fin_0_induct_lemma)
done

(*Functions from a finite ordinal*)
lemma nat_fun_subset_Fin: "n \<in> nat \<Longrightarrow> n->A \<subseteq> Fin(nat*A)"
apply (induct_tac "n")
apply (simp add: subset_iff)
apply (simp add: succ_def mem_not_refl [THEN cons_fun_eq])
apply (fast intro!: Fin.consI)
done

subsection\<open>Finite Function Space\<close>

lemma FiniteFun_mono:
    "\<lbrakk>A<=C;  B<=D\<rbrakk> \<Longrightarrow> A -||> B  \<subseteq>  C -||> D"
  unfolding FiniteFun.defs
apply (rule lfp_mono)
apply (rule FiniteFun.bnd_mono)+
apply (intro Fin_mono Sigma_mono basic_monos, assumption+)
done

lemma FiniteFun_mono1: "A<=B \<Longrightarrow> A -||> A  \<subseteq>  B -||> B"
by (blast dest: FiniteFun_mono)

lemma FiniteFun_is_fun: "h \<in> A -||>B \<Longrightarrow> h \<in> domain(h) -> B"
apply (erule FiniteFun.induct, simp)
apply (simp add: fun_extend3)
done

lemma FiniteFun_domain_Fin: "h \<in> A -||>B \<Longrightarrow> domain(h) \<in> Fin(A)"
by (erule FiniteFun.induct, simp, simp)

lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type]

(*Every subset of a finite function is a finite function.*)
lemma FiniteFun_subset_lemma [rule_format]:
     "b \<in> A-||>B \<Longrightarrow> \<forall>z. z<=b \<longrightarrow> z \<in> A-||>B"
apply (erule FiniteFun.induct)
apply (simp add: subset_empty_iff FiniteFun.intros)
apply (simp add: subset_cons_iff distrib_simps, safe)
apply (erule_tac b = z in cons_Diff [THEN subst])
apply (drule spec [THEN mp], assumption)
apply (fast intro!: FiniteFun.intros)
done

lemma FiniteFun_subset: "\<lbrakk>c<=b;  b \<in> A-||>B\<rbrakk> \<Longrightarrow> c \<in> A-||>B"
by (blast intro: FiniteFun_subset_lemma)

(** Some further results by Sidi O. Ehmety **)

lemma fun_FiniteFunI [rule_format]: "A \<in> Fin(X) \<Longrightarrow> \<forall>f. f \<in> A->B \<longrightarrow> f \<in> A-||>B"
apply (erule Fin.induct)
 apply (simp add: FiniteFun.intros, clarify)
apply (case_tac "a \<in> b")
 apply (simp add: cons_absorb)
apply (subgoal_tac "restrict (f,b) \<in> b -||> B")
 prefer 2 apply (blast intro: restrict_type2)
apply (subst fun_cons_restrict_eq, assumption)
apply (simp add: restrict_def lam_def)
apply (blast intro: apply_funtype FiniteFun.intros
                    FiniteFun_mono [THEN [2] rev_subsetD])
done

lemma lam_FiniteFun: "A \<in> Fin(X) \<Longrightarrow> (\<lambda>x\<in>A. b(x)) \<in> A -||> {b(x). x \<in> A}"
by (blast intro: fun_FiniteFunI lam_funtype)

lemma FiniteFun_Collect_iff:
     "f \<in> FiniteFun(A, {y \<in> B. P(y)})
      \<longleftrightarrow> f \<in> FiniteFun(A,B) \<and> (\<forall>x\<in>domain(f). P(f`x))"
apply auto
apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD])
apply (blast dest: Pair_mem_PiD FiniteFun_is_fun)
apply (rule_tac A1="domain(f)" in
       subset_refl [THEN [2] FiniteFun_mono, THEN subsetD])
 apply (fast dest: FiniteFun_domain_Fin Fin.dom_subset [THEN subsetD])
apply (rule fun_FiniteFunI)
apply (erule FiniteFun_domain_Fin)
apply (rule_tac B = "range (f) " in fun_weaken_type)
 apply (blast dest: FiniteFun_is_fun range_of_fun range_type apply_equality)+
done

subsection\<open>The Contents of a Singleton Set\<close>

definition
  contents :: "i\<Rightarrow>i"  where
   "contents(X) \<equiv> THE x. X = {x}"

lemma contents_eq [simp]: "contents ({x}) = x"
by (simp add: contents_def)

end

repo: isabelle


text:
theory Abstract_Limits
  imports
    Abstract_Topology
begin

subsection\<open>nhdsin and atin\<close>

definition nhdsin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
  where "nhdsin X a =
           (if a \<in> topspace X then (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S) else bot)"

definition atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
  where "atin X a \<equiv> inf (nhdsin X a) (principal (topspace X - {a}))"

lemma nhdsin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> nhdsin X a = bot"
  and atin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> atin X a = bot"
  by (simp_all add: nhdsin_def atin_def)

lemma eventually_nhdsin:
  "eventually P (nhdsin X a) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
proof (cases "a \<in> topspace X")
  case True
  hence "nhdsin X a = (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S)"
    by (simp add: nhdsin_def)
  also have "eventually P \<dots> \<longleftrightarrow> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    using True by (subst eventually_INF_base) (auto simp: eventually_principal)
  finally show ?thesis using True by simp
qed auto

lemma eventually_atin:
  "eventually P (atin X a) \<longleftrightarrow> a \<notin> topspace X \<or>
             (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
proof (cases "a \<in> topspace X")
  case True
  hence "eventually P (atin X a) \<longleftrightarrow> (\<exists>S. openin X S \<and>
           a \<in> S \<and> (\<forall>x\<in>S. x \<in> topspace X \<and> x \<noteq> a \<longrightarrow> P x))"
    by (simp add: atin_def eventually_inf_principal eventually_nhdsin)
  also have "\<dots> \<longleftrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
    using openin_subset by (intro ex_cong) auto
  finally show ?thesis by (simp add: True)
qed auto

subsection\<open>Limits in a topological space\<close>

definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
  "limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"

lemma limitin_canonical_iff [simp]: "limitin euclidean f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
  by (auto simp: limitin_def tendsto_def)

lemma limitin_topspace: "limitin X f l F \<Longrightarrow> l \<in> topspace X"
  by (simp add: limitin_def)

lemma limitin_const_iff [simp]: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
  by (simp add: limitin_def)

lemma limitin_const: "limitin euclidean (\<lambda>a. l) l F"
  by simp

lemma limitin_eventually:
   "\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limitin X f l F"
  by (auto simp: limitin_def eventually_mono)

lemma limitin_subsequence:
   "\<lbrakk>strict_mono r; limitin X f l sequentially\<rbrakk> \<Longrightarrow> limitin X (f \<circ> r) l sequentially"
  unfolding limitin_def using eventually_subseq by fastforce

lemma limitin_subtopology:
  "limitin (subtopology X S) f l F
   \<longleftrightarrow> l \<in> S \<and> eventually (\<lambda>a. f a \<in> S) F \<and> limitin X f l F"  (is "?lhs = ?rhs")
proof (cases "l \<in> S \<inter> topspace X")
  case True
  show ?thesis
  proof
    assume L: ?lhs
    with True
    have "\<forall>\<^sub>F b in F. f b \<in> topspace X \<inter> S"
      by (metis (no_types) limitin_def openin_topspace topspace_subtopology)
    with L show ?rhs
      apply (clarsimp simp add: limitin_def eventually_mono openin_subtopology_alt)
      apply (drule_tac x="S \<inter> U" in spec, force simp: elim: eventually_mono)
      done
  next
    assume ?rhs
    then show ?lhs
      using eventually_elim2
      by (fastforce simp add: limitin_def openin_subtopology_alt)
  qed
qed (auto simp: limitin_def)

lemma limitin_canonical_iff_gen [simp]:
  assumes "open S"
  shows "limitin (top_of_set S) f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F \<and> l \<in> S"
  using assms by (auto simp: limitin_subtopology tendsto_def)

lemma limitin_sequentially:
   "limitin X S l sequentially \<longleftrightarrow>
     l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> (\<exists>N. \<forall>n. N \<le> n \<longrightarrow> S n \<in> U))"
  by (simp add: limitin_def eventually_sequentially)

lemma limitin_sequentially_offset:
   "limitin X f l sequentially \<Longrightarrow> limitin X (\<lambda>i. f (i + k)) l sequentially"
  unfolding limitin_sequentially
  by (metis add.commute le_add2 order_trans)

lemma limitin_sequentially_offset_rev:
  assumes "limitin X (\<lambda>i. f (i + k)) l sequentially"
  shows "limitin X f l sequentially"
proof -
  have "\<exists>N. \<forall>n\<ge>N. f n \<in> U" if U: "openin X U" "l \<in> U" for U
  proof -
    obtain N where "\<And>n. n\<ge>N \<Longrightarrow> f (n + k) \<in> U"
      using assms U unfolding limitin_sequentially by blast
    then have "\<forall>n\<ge>N+k. f n \<in> U"
      by (metis add_leD2 le_add_diff_inverse ordered_cancel_comm_monoid_diff_class.le_diff_conv2 add.commute)
    then show ?thesis ..
  qed
  with assms show ?thesis
    unfolding limitin_sequentially
    by simp
qed

lemma limitin_atin:
   "limitin Y f y (atin X x) \<longleftrightarrow>
        y \<in> topspace Y \<and>
        (x \<in> topspace X
        \<longrightarrow> (\<forall>V. openin Y V \<and> y \<in> V
                 \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> f ` (U - {x}) \<subseteq> V)))"
  by (auto simp: limitin_def eventually_atin image_subset_iff)

lemma limitin_atin_self:
   "limitin Y f (f a) (atin X a) \<longleftrightarrow>
        f a \<in> topspace Y \<and>
        (a \<in> topspace X
         \<longrightarrow> (\<forall>V. openin Y V \<and> f a \<in> V
                  \<longrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> f ` U \<subseteq> V)))"
  unfolding limitin_atin by fastforce

lemma limitin_trivial:
   "\<lbrakk>trivial_limit F; y \<in> topspace X\<rbrakk> \<Longrightarrow> limitin X f y F"
  by (simp add: limitin_def)

lemma limitin_transform_eventually:
   "\<lbrakk>eventually (\<lambda>x. f x = g x) F; limitin X f l F\<rbrakk> \<Longrightarrow> limitin X g l F"
  unfolding limitin_def using eventually_elim2 by fastforce

lemma continuous_map_limit:
  assumes "continuous_map X Y g" and f: "limitin X f l F"
  shows "limitin Y (g \<circ> f) (g l) F"
proof -
  have "g l \<in> topspace Y"
    by (meson assms continuous_map_def limitin_topspace)
  moreover
  have "\<And>U. \<lbrakk>\<forall>V. openin X V \<and> l \<in> V \<longrightarrow> (\<forall>\<^sub>F x in F. f x \<in> V); openin Y U; g l \<in> U\<rbrakk>
            \<Longrightarrow> \<forall>\<^sub>F x in F. g (f x) \<in> U"
    using assms eventually_mono
    by (fastforce simp: limitin_def dest!: openin_continuous_map_preimage)
  ultimately show ?thesis
    using f by (fastforce simp add: limitin_def)
qed

subsection\<open>Pointwise continuity in topological spaces\<close>

definition topcontinuous_at where
  "topcontinuous_at X Y f x \<longleftrightarrow>
     x \<in> topspace X \<and>
     (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
     (\<forall>V. openin Y V \<and> f x \<in> V
          \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. f y \<in> V)))"

lemma topcontinuous_at_atin:
   "topcontinuous_at X Y f x \<longleftrightarrow>
        x \<in> topspace X \<and>
        (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
        limitin Y f (f x) (atin X x)"
  unfolding topcontinuous_at_def
  by (fastforce simp add: limitin_atin)+

lemma continuous_map_eq_topcontinuous_at:
   "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. topcontinuous_at X Y f x)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: continuous_map_def topcontinuous_at_def)
next
  assume R: ?rhs
  then show ?lhs
    apply (auto simp: continuous_map_def topcontinuous_at_def)
    apply (subst openin_subopen, safe)
    apply (drule bspec, assumption)
    using openin_subset[of X] apply (auto simp: subset_iff dest!: spec)
    done
qed

lemma continuous_map_atin:
   "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. limitin Y f (f x) (atin X x))"
  by (auto simp: limitin_def topcontinuous_at_atin continuous_map_eq_topcontinuous_at)

lemma limitin_continuous_map:
   "\<lbrakk>continuous_map X Y f; a \<in> topspace X; f a = b\<rbrakk> \<Longrightarrow> limitin Y f b (atin X a)"
  by (auto simp: continuous_map_atin)

subsection\<open>Combining theorems for continuous functions into the reals\<close>

lemma continuous_map_canonical_const [continuous_intros]:
   "continuous_map X euclidean (\<lambda>x. c)"
  by simp

lemma continuous_map_real_mult [continuous_intros]:
   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * g x)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_pow [continuous_intros]:
   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x ^ n)"
  by (induction n) (auto simp: continuous_map_real_mult)

lemma continuous_map_real_mult_left:
   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. c * f x)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_mult_left_eq:
   "continuous_map X euclideanreal (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
proof (cases "c = 0")
  case False
  have "continuous_map X euclideanreal (\<lambda>x. c * f x) \<Longrightarrow> continuous_map X euclideanreal f"
    apply (frule continuous_map_real_mult_left [where c="inverse c"])
    apply (simp add: field_simps False)
    done
  with False show ?thesis
    using continuous_map_real_mult_left by blast
qed simp

lemma continuous_map_real_mult_right:
   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * c)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_mult_right_eq:
   "continuous_map X euclideanreal (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
  by (simp add: mult.commute flip: continuous_map_real_mult_left_eq)

lemma continuous_map_minus [continuous_intros]:
  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
  shows "continuous_map X euclidean f \<Longrightarrow> continuous_map X euclidean (\<lambda>x. - f x)"
  by (simp add: continuous_map_atin tendsto_minus)

lemma continuous_map_minus_eq [simp]:
  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
  shows "continuous_map X euclidean (\<lambda>x. - f x) \<longleftrightarrow> continuous_map X euclidean f"
  using continuous_map_minus add.inverse_inverse continuous_map_eq by fastforce

lemma continuous_map_add [continuous_intros]:
  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
  shows "\<lbrakk>continuous_map X euclidean f; continuous_map X euclidean g\<rbrakk> \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x + g x)"
  by (simp add: continuous_map_atin tendsto_add)

lemma continuous_map_diff [continuous_intros]:
  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
  shows "\<lbrakk>continuous_map X euclidean f; continuous_map X euclidean g\<rbrakk> \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x - g x)"
  by (simp add: continuous_map_atin tendsto_diff)

lemma continuous_map_norm [continuous_intros]:
  fixes f :: "'a\<Rightarrow>'b::real_normed_vector"
  shows "continuous_map X euclidean f \<Longrightarrow> continuous_map X euclidean (\<lambda>x. norm(f x))"
  by (simp add: continuous_map_atin tendsto_norm)

lemma continuous_map_real_abs [continuous_intros]:
   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. abs(f x))"
  by (simp add: continuous_map_atin tendsto_rabs)

lemma continuous_map_real_max [continuous_intros]:
   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. max (f x) (g x))"
  by (simp add: continuous_map_atin tendsto_max)

lemma continuous_map_real_min [continuous_intros]:
   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. min (f x) (g x))"
  by (simp add: continuous_map_atin tendsto_min)

lemma continuous_map_sum [continuous_intros]:
  fixes f :: "'a\<Rightarrow>'b\<Rightarrow>'c::real_normed_vector"
  shows "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclidean (\<lambda>x. f x i)\<rbrakk>
         \<Longrightarrow> continuous_map X euclidean (\<lambda>x. sum (f x) I)"
  by (simp add: continuous_map_atin tendsto_sum)

lemma continuous_map_prod [continuous_intros]:
   "\<lbrakk>finite I;
         \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
        \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. prod (f x) I)"
  by (simp add: continuous_map_atin tendsto_prod)

lemma continuous_map_real_inverse [continuous_intros]:
   "\<lbrakk>continuous_map X euclideanreal f; \<And>x. x \<in> topspace X \<Longrightarrow> f x \<noteq> 0\<rbrakk>
        \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. inverse(f x))"
  by (simp add: continuous_map_atin tendsto_inverse)

lemma continuous_map_real_divide [continuous_intros]:
   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g; \<And>x. x \<in> topspace X \<Longrightarrow> g x \<noteq> 0\<rbrakk>
   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x / g x)"
  by (simp add: continuous_map_atin tendsto_divide)

end


text:
(*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009-2011

Examples featuring Nitpick's monotonicity check.
*)

section \<open>Examples Featuring Nitpick's Monotonicity Check\<close>

theory Mono_Nits
imports Main
        (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" *)
        (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
begin

ML \<open>
open Nitpick_Util
open Nitpick_HOL
open Nitpick_Preproc

exception BUG

val thy = @{theory}
val ctxt = @{context}
val subst = []
val tac_timeout = seconds 1.0
val case_names = case_const_names ctxt
val defs = all_defs_of thy subst
val nondefs = all_nondefs_of ctxt subst
val def_tables = const_def_tables ctxt subst defs
val nondef_table = const_nondef_table nondefs
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
val psimp_table = const_psimp_table ctxt subst
val choice_spec_table = const_choice_spec_table ctxt subst
val intro_table = inductive_intro_table ctxt subst def_tables
val ground_thm_table = ground_theorem_table thy
val ersatz_table = ersatz_table ctxt
val hol_ctxt as {thy, ...} : hol_context =
  {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [], wfs = [],
   user_axioms = NONE, debug = false, whacks = [], binary_ints = SOME false,
   destroy_constrs = true, specialize = false, star_linear_preds = false,
   total_consts = NONE, needs = NONE, tac_timeout = tac_timeout, evals = [],
   case_names = case_names, def_tables = def_tables,
   nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table,
   psimp_table = psimp_table, choice_spec_table = choice_spec_table,
   intro_table = intro_table, ground_thm_table = ground_thm_table,
   ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
val binarize = false

fun is_mono t =
  Nitpick_Mono.formulas_monotonic hol_ctxt binarize @{typ 'a} ([t], [])

fun is_const t =
  let val T = fastype_of t in
    Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @{const False})
    |> is_mono
  end

fun mono t = is_mono t orelse raise BUG
fun nonmono t = not (is_mono t) orelse raise BUG
fun const t = is_const t orelse raise BUG
fun nonconst t = not (is_const t) orelse raise BUG
\<close>

ML \<open>Nitpick_Mono.trace := false\<close>

ML_val \<open>const @{term "A::('a\<Rightarrow>'b)"}\<close>
ML_val \<open>const @{term "(A::'a set) = A"}\<close>
ML_val \<open>const @{term "(A::'a set set) = A"}\<close>
ML_val \<open>const @{term "(\<lambda>x::'a set. a \<in> x)"}\<close>
ML_val \<open>const @{term "{{a::'a}} = C"}\<close>
ML_val \<open>const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"}\<close>
ML_val \<open>const @{term "A \<union> (B::'a set)"}\<close>
ML_val \<open>const @{term "\<lambda>A B x::'a. A x \<or> B x"}\<close>
ML_val \<open>const @{term "P (a::'a)"}\<close>
ML_val \<open>const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"}\<close>
ML_val \<open>const @{term "\<forall>A::'a set. a \<in> A"}\<close>
ML_val \<open>const @{term "\<forall>A::'a set. P A"}\<close>
ML_val \<open>const @{term "P \<or> Q"}\<close>
ML_val \<open>const @{term "A \<union> B = (C::'a set)"}\<close>
ML_val \<open>const @{term "(\<lambda>A B x::'a. A x \<or> B x) A B = C"}\<close>
ML_val \<open>const @{term "(if P then (A::'a set) else B) = C"}\<close>
ML_val \<open>const @{term "let A = (C::'a set) in A \<union> B"}\<close>
ML_val \<open>const @{term "THE x::'b. P x"}\<close>
ML_val \<open>const @{term "(\<lambda>x::'a. False)"}\<close>
ML_val \<open>const @{term "(\<lambda>x::'a. True)"}\<close>
ML_val \<open>const @{term "(\<lambda>x::'a. False) = (\<lambda>x::'a. False)"}\<close>
ML_val \<open>const @{term "(\<lambda>x::'a. True) = (\<lambda>x::'a. True)"}\<close>
ML_val \<open>const @{term "Let (a::'a) A"}\<close>
ML_val \<open>const @{term "A (a::'a)"}\<close>
ML_val \<open>const @{term "insert (a::'a) A = B"}\<close>
ML_val \<open>const @{term "- (A::'a set)"}\<close>
ML_val \<open>const @{term "finite (A::'a set)"}\<close>
ML_val \<open>const @{term "\<not> finite (A::'a set)"}\<close>
ML_val \<open>const @{term "finite (A::'a set set)"}\<close>
ML_val \<open>const @{term "\<lambda>a::'a. A a \<and> \<not> B a"}\<close>
ML_val \<open>const @{term "A < (B::'a set)"}\<close>
ML_val \<open>const @{term "A \<le> (B::'a set)"}\<close>
ML_val \<open>const @{term "[a::'a]"}\<close>
ML_val \<open>const @{term "[a::'a set]"}\<close>
ML_val \<open>const @{term "[A \<union> (B::'a set)]"}\<close>
ML_val \<open>const @{term "[A \<union> (B::'a set)] = [C]"}\<close>
ML_val \<open>const @{term "{(\<lambda>x::'a. x = a)} = C"}\<close>
ML_val \<open>const @{term "(\<lambda>a::'a. \<not> A a) = B"}\<close>
ML_val \<open>const @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> \<not> f a"}\<close>
ML_val \<open>const @{term "\<lambda>A B x::'a. A x \<and> B x \<and> A = B"}\<close>
ML_val \<open>const @{term "p = (\<lambda>(x::'a) (y::'a). P x \<or> \<not> Q y)"}\<close>
ML_val \<open>const @{term "p = (\<lambda>(x::'a) (y::'a). p x y :: bool)"}\<close>
ML_val \<open>const @{term "p = (\<lambda>A B x. A x \<and> \<not> B x) (\<lambda>x. True) (\<lambda>y. x \<noteq> y)"}\<close>
ML_val \<open>const @{term "p = (\<lambda>y. x \<noteq> y)"}\<close>
ML_val \<open>const @{term "(\<lambda>x. (p::'a\<Rightarrow>bool\<Rightarrow>bool) x False)"}\<close>
ML_val \<open>const @{term "(\<lambda>x y. (p::'a\<Rightarrow>'a\<Rightarrow>bool\<Rightarrow>bool) x y False)"}\<close>
ML_val \<open>const @{term "f = (\<lambda>x::'a. P x \<longrightarrow> Q x)"}\<close>
ML_val \<open>const @{term "\<forall>a::'a. P a"}\<close>

ML_val \<open>nonconst @{term "\<forall>P (a::'a). P a"}\<close>
ML_val \<open>nonconst @{term "THE x::'a. P x"}\<close>
ML_val \<open>nonconst @{term "SOME x::'a. P x"}\<close>
ML_val \<open>nonconst @{term "(\<lambda>A B x::'a. A x \<or> B x) = myunion"}\<close>
ML_val \<open>nonconst @{term "(\<lambda>x::'a. False) = (\<lambda>x::'a. True)"}\<close>
ML_val \<open>nonconst @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"}\<close>

ML_val \<open>mono @{prop "Q (\<forall>x::'a set. P x)"}\<close>
ML_val \<open>mono @{prop "P (a::'a)"}\<close>
ML_val \<open>mono @{prop "{a} = {b::'a}"}\<close>
ML_val \<open>mono @{prop "(\<lambda>x. x = a) = (\<lambda>y. y = (b::'a))"}\<close>
ML_val \<open>mono @{prop "(a::'a) \<in> P \<and> P \<union> P = P"}\<close>
ML_val \<open>mono @{prop "\<forall>F::'a set set. P"}\<close>
ML_val \<open>mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h)"}\<close>
ML_val \<open>mono @{prop "\<not> Q (\<forall>x::'a set. P x)"}\<close>
ML_val \<open>mono @{prop "\<not> (\<forall>x::'a. P x)"}\<close>
ML_val \<open>mono @{prop "myall P = (P = (\<lambda>x::'a. True))"}\<close>
ML_val \<open>mono @{prop "myall P = (P = (\<lambda>x::'a. False))"}\<close>
ML_val \<open>mono @{prop "\<forall>x::'a. P x"}\<close>
ML_val \<open>mono @{term "(\<lambda>A B x::'a. A x \<or> B x) \<noteq> myunion"}\<close>

ML_val \<open>nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"}\<close>
ML_val \<open>nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> a \<in> f \<and> a \<in> g \<longrightarrow> F h"}\<close>

ML \<open>
val preproc_timeout = seconds 5.0
val mono_timeout = seconds 1.0

fun is_forbidden_theorem name =
  length (Long_Name.explode name) <> 2 orelse
  String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
  String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
  String.isSuffix "_def" name orelse
  String.isSuffix "_raw" name

fun theorems_of thy =
  filter (fn (name, th) =>
             not (is_forbidden_theorem name) andalso
             Thm.theory_name_of_thm th = Context.theory_name thy)
         (Global_Theory.all_thms_of thy true)

fun check_formulas tsp =
  let
    fun is_type_actually_monotonic T =
      Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
    val free_Ts = fold Term.add_tfrees (op @ tsp) [] |> map TFree
    val (mono_free_Ts, nonmono_free_Ts) =
      Timeout.apply mono_timeout
          (List.partition is_type_actually_monotonic) free_Ts
  in
    if not (null mono_free_Ts) then "MONO"
    else if not (null nonmono_free_Ts) then "NONMONO"
    else "NIX"
  end
  handle Timeout.TIMEOUT _ => "TIMEOUT"
       | NOT_SUPPORTED _ => "UNSUP"
       | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"

fun check_theory thy =
  let
    val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
    val _ = File.write path ""
    fun check_theorem (name, th) =
      let
        val t = th |> Thm.prop_of |> Type.legacy_freeze |> close_form
        val neg_t = Logic.mk_implies (t, @{prop False})
        val (nondef_ts, def_ts, _, _, _, _) =
          Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
                              neg_t
        val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
      in File.append path (res ^ "\n"); writeln res end
      handle Timeout.TIMEOUT _ => ()
  in thy |> theorems_of |> List.app check_theorem end
\<close>

(*
ML_val {* check_theory @{theory AVL2} *}
ML_val {* check_theory @{theory Fun} *}
ML_val {* check_theory @{theory Huffman} *}
ML_val {* check_theory @{theory List} *}
ML_val {* check_theory @{theory Map} *}
ML_val {* check_theory @{theory Relation} *}
*)

ML \<open>getenv "ISABELLE_TMP"\<close>

end

repo: jormungand


text:
(* This Isabelle theory is produced using the TIP tool offered at the following website:
     https://github.com/tip-org/tools
   This file was originally provided as part of TIP benchmark at the following website:
     https://github.com/tip-org/benchmarks
   Yutaka Nagashima at CIIRC, CTU changed the TIP output theory file slightly
   to make it compatible with Isabelle2017.*)
  theory TIP_sort_MSortBUCount
  imports "../../Test_Base"
begin

datatype 'a list = nil2 | cons2 "'a" "'a list"

fun map :: "('a => 'b) => 'a list => 'b list" where
  "map f (nil2) = nil2"
| "map f (cons2 y xs) = cons2 (f y) (map f xs)"

fun lmerge :: "int list => int list => int list" where
  "lmerge (nil2) y = y"
| "lmerge (cons2 z x2) (nil2) = cons2 z x2"
| "lmerge (cons2 z x2) (cons2 x3 x4) =
     (if z <= x3 then cons2 z (lmerge x2 (cons2 x3 x4)) else
        cons2 x3 (lmerge (cons2 z x2) x4))"

fun pairwise :: "(int list) list => (int list) list" where
  "pairwise (nil2) = nil2"
| "pairwise (cons2 xs (nil2)) = cons2 xs (nil2)"
| "pairwise (cons2 xs (cons2 ys xss)) =
     cons2 (lmerge xs ys) (pairwise xss)"

(*fun did not finish the proof*)
function mergingbu :: "(int list) list => int list" where
  "mergingbu (nil2) = nil2"
| "mergingbu (cons2 xs (nil2)) = xs"
| "mergingbu (cons2 xs (cons2 z x2)) =
     mergingbu (pairwise (cons2 xs (cons2 z x2)))"
  by pat_completeness auto

fun msortbu :: "int list => int list" where
  "msortbu x = mergingbu (map (% (y :: int) => cons2 y (nil2)) x)"

fun count :: "'a => 'a list => int" where
  "count x (nil2) = 0"
| "count x (cons2 z ys) =
     (if (x = z) then 1 + (count x ys) else count x ys)"

theorem property0 :
  "((count x (msortbu xs)) = (count x xs))"
  oops

end

repo: PSL


text:
header {* Monotonic Boolean Transformers *}

theory Mono_Bool_Tran
imports
  "../LatticeProperties/Complete_Lattice_Prop"
  "../LatticeProperties/Conj_Disj"
begin

text{*
The type of monotonic transformers is the type associated to the set of monotonic
functions from a partially ordered set (poset) to itself. The type of monotonic
transformers with the pointwise extended order is also a poset.
The monotonic transformers with composition and identity
form a monoid, and the monoid operation is compatible with the order.

Gradually we extend the algebraic structure of monotonic transformers to
lattices, and complete lattices. We also introduce a dual operator
($(\mathsf{dual}\;f) p = - f (-p)$) on monotonic transformers over
a boolean algebra. However the monotonic transformers over a boolean
algebra are not closed to the pointwise extended negation operator.

Finally we introduce an iteration operator on monotonic transformers
over a complete lattice.
*}

notation
  bot ("\<bottom>") and
  top ("\<top>") and
  inf (infixl "\<sqinter>" 70) and
  sup (infixl "\<squnion>" 65) and
  Inf ("\<Sqinter>_" [900] 900) and
  Sup ("\<Squnion>_" [900] 900)

syntax (xsymbols)
  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)

lemma Inf_comp_fun:
  "\<Sqinter>M \<circ> f = (\<Sqinter>m\<in>M. m \<circ> f)"
  by (simp add: fun_eq_iff)

lemma INF_comp_fun:
  "(\<Sqinter>a\<in>A. g a) \<circ> f = (\<Sqinter>a\<in>A. g a \<circ> f)"
  by (simp add: fun_eq_iff)

lemma Sup_comp_fun:
  "\<Squnion>M \<circ> f = (\<Squnion>m\<in>M. m \<circ> f)"
  by (simp add: fun_eq_iff)

lemma SUP_comp_fun:
  "(\<Squnion>a\<in>A. g a) \<circ> f = (\<Squnion>a\<in>A. g a \<circ> f)"
  by (simp add: fun_eq_iff)

lemma (in order) mono_const [simp]:
  "mono (\<lambda>_. c)"
  by (auto intro: monoI)

lemma (in order) mono_id [simp]:
  "mono id"
  by (auto intro: order_class.monoI)

lemma (in order) mono_comp [simp]:
  "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (f \<circ> g)"
  by (auto intro!: monoI elim!: monoE order_class.monoE)

lemma (in bot) mono_bot [simp]:
  "mono \<bottom>"
  by (auto intro: monoI)

lemma (in top) mono_top [simp]:
  "mono \<top>"
  by (auto intro: monoI)

lemma (in semilattice_inf) mono_inf [simp]:
  assumes "mono f" and "mono g"
  shows "mono (f \<sqinter> g)"
proof
  fix a b
  assume "a \<le> b"
  have "f a \<sqinter> g a \<le> f a" by simp
  also from `mono f` `a \<le> b` have "\<dots> \<le> f b" by (auto elim: monoE)
  finally have *: "f a \<sqinter> g a \<le> f b" .
  have "f a \<sqinter> g a \<le> g a" by simp
  also from `mono g` `a \<le> b` have "\<dots> \<le> g b" by (auto elim: monoE)
  finally have **: "f a \<sqinter> g a \<le> g b" .
  from * ** show "(f \<sqinter> g) a \<le> (f \<sqinter> g) b" by auto
qed

lemma (in semilattice_sup) mono_sup [simp]:
  assumes "mono f" and "mono g"
  shows "mono (f \<squnion> g)"
proof
  fix a b
  assume "a \<le> b"
  from `mono f` `a \<le> b` have "f a \<le> f b" by (auto elim: monoE)
  also have "f b \<le> f b \<squnion> g b" by simp
  finally have *: "f a \<le> f b \<squnion> g b" .
  from `mono g` `a \<le> b` have "g a \<le> g b" by (auto elim: monoE)
  also have "g b \<le> f b \<squnion> g b" by simp
  finally have **: "g a \<le> f b \<squnion> g b" .
  from * ** show "(f \<squnion> g) a \<le> (f \<squnion> g) b" by auto
qed

lemma (in complete_lattice) mono_Inf [simp]:
  assumes "A \<subseteq> {f :: 'a \<Rightarrow> 'b:: complete_lattice. mono f}"
  shows "mono (\<Sqinter>A)"
proof
  fix a b
  assume "a \<le> b"
  { fix f
    assume "f \<in> A"
    with assms have "mono f" by auto
    with `a \<le> b` have "f a \<le> f b" by (auto elim: monoE)
  }
  then have "(\<Sqinter>f\<in>A. f a) \<le> (\<Sqinter>f\<in>A. f b)"
    by (auto intro: complete_lattice_class.INF_greatest complete_lattice_class.INF_lower2)
  then show "(\<Sqinter>A) a \<le> (\<Sqinter>A) b" by simp
qed

lemma (in complete_lattice) mono_Sup [simp]:
  assumes "A \<subseteq> {f :: 'a \<Rightarrow> 'b:: complete_lattice. mono f}"
  shows "mono (\<Squnion>A)"
proof
  fix a b
  assume "a \<le> b"
  { fix f
    assume "f \<in> A"
    with assms have "mono f" by auto
    with `a \<le> b` have "f a \<le> f b" by (auto elim: monoE)
  }
  then have "(\<Squnion>f\<in>A. f a) \<le> (\<Squnion>f\<in>A. f b)"
    by (auto intro: complete_lattice_class.SUP_least complete_lattice_class.SUP_upper2)
  then show "(\<Squnion>A) a \<le> (\<Squnion>A) b" by simp
qed

typedef 'a MonoTran = "{f::'a::order \<Rightarrow> 'a . mono f}"
proof
  show "id \<in> ?MonoTran" by simp
qed

setup_lifting type_definition_MonoTran

instantiation MonoTran :: (order) order
begin

lift_definition less_eq_MonoTran :: "'a MonoTran \<Rightarrow> 'a MonoTran \<Rightarrow> bool"
  is less_eq .

lift_definition less_MonoTran :: "'a MonoTran \<Rightarrow> 'a MonoTran \<Rightarrow> bool"
  is less .

instance
  by intro_classes (transfer, auto intro: order_antisym)+

end

instantiation MonoTran :: (order) monoid_mult
begin

lift_definition one_MonoTran :: "'a MonoTran"
  is id
  by (fact mono_id)

lift_definition times_MonoTran :: "'a MonoTran \<Rightarrow> 'a MonoTran \<Rightarrow> 'a MonoTran"
  is comp
  by (fact mono_comp)

instance
  by intro_classes (transfer, auto)+

end

instantiation MonoTran :: (order_bot) order_bot
begin

lift_definition bot_MonoTran :: "'a MonoTran"
  is \<bottom>
  by (fact mono_bot)

instance
  by intro_classes (transfer, simp)

end

instantiation MonoTran :: (order_top) order_top
begin

lift_definition top_MonoTran :: "'a MonoTran"
  is \<top>
  by (fact mono_top)

instance
  by intro_classes (transfer, simp)

end

instantiation MonoTran :: (lattice) lattice
begin

lift_definition inf_MonoTran :: "'a MonoTran \<Rightarrow> 'a MonoTran \<Rightarrow> 'a MonoTran"
  is inf
  by (fact mono_inf)

lift_definition sup_MonoTran :: "'a MonoTran \<Rightarrow> 'a MonoTran \<Rightarrow> 'a MonoTran"
  is sup
  by (fact mono_sup)

instance
  by intro_classes (transfer, simp)+

end

instance MonoTran :: (distrib_lattice) distrib_lattice
  by intro_classes (transfer, rule sup_inf_distrib1)

instantiation MonoTran :: (complete_lattice) complete_lattice
begin

lift_definition Inf_MonoTran :: "'a MonoTran set \<Rightarrow> 'a MonoTran"
  is Inf
  by (rule mono_Inf) auto

lift_definition Sup_MonoTran :: "'a MonoTran set \<Rightarrow> 'a MonoTran"
  is Sup
  by (rule mono_Sup) auto

instance
  by intro_classes (transfer, simp add: Inf_lower Sup_upper Inf_greatest Sup_least)+

end

context
begin

interpretation lifting_syntax .

lemma [transfer_rule]:
  "(rel_set A ===> (A ===> pcr_MonoTran HOL.eq) ===> pcr_MonoTran HOL.eq) SUPREMUM SUPREMUM"
  unfolding SUP_def [abs_def] by transfer_prover

end

instance MonoTran :: (complete_distrib_lattice) complete_distrib_lattice
  apply intro_classes
  apply transfer apply (simp add: inf_Sup sup_Inf)
  apply transfer apply (simp add: inf_Sup sup_Inf)
  done

definition
  "dual_fun (f::'a::boolean_algebra \<Rightarrow> 'a) = uminus \<circ> f \<circ> uminus"

lemma dual_fun_apply [simp]:
  "dual_fun f p = - f (- p)"
  by (simp add: dual_fun_def)

lemma mono_dual_fun [simp]:
  "mono f \<Longrightarrow> mono (dual_fun f)"
  apply (rule monoI)
  apply (erule monoE)
  apply auto
  done

lemma (in order) mono_inf_fun [simp]:
  fixes x :: "'b::semilattice_inf"
  shows "mono (inf x)"
  by (auto intro!: order_class.monoI semilattice_inf_class.inf_mono)

lemma (in order) mono_sup_fun [simp]:
  fixes x :: "'b::semilattice_sup"
  shows "mono (sup x)"
  by (auto intro!: order_class.monoI semilattice_sup_class.sup_mono)

lemma mono_comp_fun:
  fixes f :: "'a::order \<Rightarrow> 'b::order"
  shows "mono f \<Longrightarrow> mono (op \<circ> f)"
  by (rule monoI) (auto simp add: le_fun_def elim: monoE)

definition
  "Omega_fun f g = inf g \<circ> comp f"

lemma Omega_fun_apply [simp]:
  "Omega_fun f g h p = (g p \<sqinter> f (h p))"
  by (simp add: Omega_fun_def)

lemma mono_Omega_fun [simp]:
  "mono f \<Longrightarrow> mono (Omega_fun f g)"
  unfolding Omega_fun_def
  by (auto intro: mono_comp mono_comp_fun)

lemma mono_mono_Omega_fun [simp]:
  fixes f :: "'b::order \<Rightarrow> 'a::semilattice_inf" and g :: "'c::semilattice_inf \<Rightarrow> 'a"
  shows "mono f \<Longrightarrow> mono g \<Longrightarrow> mono_mono (Omega_fun f g)"
  apply (auto simp add: mono_mono_def Omega_fun_def)
  apply (rule mono_comp)
  apply (rule mono_inf_fun)
  apply (rule mono_comp_fun)
  apply assumption
  done

definition
  "omega_fun f = lfp (Omega_fun f id)"

definition
  "star_fun f = gfp (Omega_fun f id)"

lemma mono_omega_fun [simp]:
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
  assumes "mono f"
  shows "mono (omega_fun f)"
proof
  fix a b :: 'a
  assume "a \<le> b"
  from assms have "mono (lfp (Omega_fun f id))"
    by (auto intro: mono_mono_Omega_fun)
  with `a \<le> b` show "omega_fun f a \<le> omega_fun f b"
    by (auto simp add: omega_fun_def elim: monoE)
qed

lemma mono_star_fun [simp]:
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
  assumes "mono f"
  shows "mono (star_fun f)"
proof
  fix a b :: 'a
  assume "a \<le> b"
  from assms have "mono (gfp (Omega_fun f id))"
    by (auto intro: mono_mono_Omega_fun)
  with `a \<le> b` show "star_fun f a \<le> star_fun f b"
    by (auto simp add: star_fun_def elim: monoE)
qed

lemma lfp_omega_lowerbound:
  "mono f \<Longrightarrow> Omega_fun f g A \<le> A \<Longrightarrow> omega_fun f \<circ> g \<le> A"
  apply (simp add: omega_fun_def)
  apply (rule_tac P = "\<lambda> x . x \<circ> g \<le> A" and f = "Omega_fun f id" in lfp_ordinal_induct)
  apply simp_all
  apply (simp add: le_fun_def o_def inf_fun_def id_def Omega_fun_def)
  apply auto
  apply (rule_tac y = "f (A x) \<sqinter> g x" in order_trans)
  apply simp_all
  apply (rule_tac y = "f (S (g x))" in order_trans)
  apply simp_all
  apply (simp add: mono_def) apply (auto simp add: ac_simps)
  apply (unfold Sup_comp_fun)
  apply (rule SUP_least)
  by auto

lemma gfp_omega_upperbound:
  "mono f \<Longrightarrow> A \<le> Omega_fun f g A \<Longrightarrow> A \<le> star_fun f \<circ> g"
  apply (simp add: star_fun_def)
  apply (rule_tac P = "\<lambda> x . A \<le> x \<circ> g" and f = "Omega_fun f id" in gfp_ordinal_induct)
  apply simp_all
  apply (simp add: le_fun_def o_def inf_fun_def id_def Omega_fun_def)
  apply auto
  apply (rule_tac y = "f (A x) \<sqinter> g x" in order_trans)
  apply simp_all
  apply (rule_tac y = "f (A x)" in order_trans)
  apply simp_all
  apply (simp add: mono_def)
  apply (unfold Inf_comp_fun)
  apply (rule INF_greatest)
  by auto

lemma lfp_omega_greatest:
  assumes "\<And>u. Omega_fun f g u \<le> u \<Longrightarrow> A \<le> u"
  shows "A \<le> omega_fun f \<circ> g"
  apply (unfold omega_fun_def)
  apply (simp add: lfp_def)
  apply (unfold Inf_comp_fun)
  apply (rule INF_greatest)
  apply simp
  apply (rule assms)
  apply (simp add: le_fun_def)
  done

lemma gfp_star_least:
  assumes "\<And>u. u \<le> Omega_fun f g u \<Longrightarrow> u \<le> A"
  shows "star_fun f \<circ> g \<le> A"
  apply (unfold star_fun_def)
  apply (simp add: gfp_def)
  apply (unfold Sup_comp_fun)
  apply (rule SUP_least)
  apply simp
  apply (rule assms)
  apply (simp add: le_fun_def)
  done

lemma lfp_omega:
  "mono f \<Longrightarrow> omega_fun f \<circ> g = lfp (Omega_fun f g)"
  apply (rule antisym)
  apply (rule lfp_omega_lowerbound)
  apply simp_all
  apply (simp add: lfp_def)
  apply (rule Inf_greatest)
  apply safe
  apply (rule_tac y = "Omega_fun f g x" in order_trans)
  apply simp_all
  apply (rule_tac f = " Omega_fun f g" in monoD)
  apply simp_all
  apply (rule Inf_lower)
  apply simp
  apply (rule lfp_omega_greatest)
  apply (simp add: lfp_def)
  apply (rule Inf_lower)
  by simp

lemma gfp_star:
  "mono f \<Longrightarrow> star_fun f \<circ> g = gfp (Omega_fun f g)"
  apply (rule antisym)
  apply (rule gfp_star_least)
  apply (simp add: gfp_def)
  apply (rule Sup_upper, simp)
  apply (rule gfp_omega_upperbound)
  apply simp_all
  apply (simp add: gfp_def)
  apply (rule Sup_least)
  apply safe
  apply (rule_tac y = "Omega_fun f g x" in order_trans)
  apply simp_all
  apply (rule_tac f = " Omega_fun f g" in monoD)
  apply simp_all
  apply (rule Sup_upper)
  by simp

definition
  "assert_fun p q = (p \<sqinter> q :: 'a::semilattice_inf)"

lemma mono_assert_fun [simp]:
  "mono (assert_fun p)"
  apply (simp add: assert_fun_def mono_def, safe)
  by (rule_tac y = x in order_trans, simp_all)

lemma assert_fun_le_id [simp]: "assert_fun p \<le> id"
  by (simp add: assert_fun_def id_def le_fun_def)

lemma assert_fun_disjunctive [simp]: "assert_fun (p::'a::distrib_lattice) \<in> Apply.disjunctive"
  by (simp add: assert_fun_def Apply.disjunctive_def inf_sup_distrib)

definition
  "assertion_fun = range assert_fun"

lemma assert_cont:
  "(x :: 'a::boolean_algebra \<Rightarrow> 'a)  \<le> id \<Longrightarrow> x \<in> Apply.disjunctive \<Longrightarrow> x = assert_fun (x \<top>)"
  apply (rule antisym)
  apply (simp_all add: le_fun_def assert_fun_def, safe)
  apply (rule_tac f = x in  monoD, simp_all)
  apply (subgoal_tac "x top = sup (x xa) (x (-xa))")
  apply simp
  apply (subst inf_sup_distrib)
  apply simp
  apply (rule_tac y = "inf (- xa) xa" in order_trans)
  apply (simp del: compl_inf_bot)
  apply (rule_tac y = "x (- xa)" in order_trans)
  apply simp
  apply simp
  apply simp
  apply (cut_tac x = x and y = xa and z = "-xa" in Apply.disjunctiveD, simp)
  apply (subst (asm) sup_commute)
  apply (subst (asm) compl_sup_top)
  by simp

lemma assertion_fun_disj_less_one: "assertion_fun = Apply.disjunctive \<inter> {x::'a::boolean_algebra \<Rightarrow> 'a . x \<le> id}"
  apply safe
  apply (simp_all add: assertion_fun_def, auto simp add: image_def)
  apply (rule_tac x = "x \<top>" in exI)
  by (rule assert_cont, simp_all)

lemma assert_fun_dual: "((assert_fun p) o \<top>) \<sqinter> (dual_fun (assert_fun p)) = assert_fun p"
  by (simp add: fun_eq_iff inf_fun_def dual_fun_def o_def assert_fun_def top_fun_def inf_sup_distrib inf_compl_bot)

lemma assertion_fun_dual: "x \<in> assertion_fun \<Longrightarrow> (x o \<top>) \<sqinter> (dual_fun x) = x"
  by (simp add: assertion_fun_def, safe, simp add: assert_fun_dual)

lemma assertion_fun_MonoTran [simp]: "x \<in> assertion_fun \<Longrightarrow> mono x"
  by (unfold assertion_fun_def, auto)

lemma assertion_fun_le_one [simp]: "x \<in> assertion_fun \<Longrightarrow> x \<le> id"
  by (unfold assertion_fun_def, auto)

end

author: Josh-Tilles

repo: AFP

save_path: github-repos/isabelle/Josh-Tilles-AFP


text:
theory Timed_Automata
  imports Main
begin

chapter \<open>Basic Definitions and Semantics\<close>

section \<open>Time\<close>

class time = linordered_ab_group_add +
  assumes dense: "x < y \<Longrightarrow> \<exists>z. x < z \<and> z < y"
  assumes non_trivial: "\<exists> x. x \<noteq> 0"

begin

lemma non_trivial_neg: "\<exists> x. x < 0"
proof -
  from non_trivial obtain x where "x \<noteq> 0" by auto
  then show ?thesis
  proof (cases "x < 0", auto, goal_cases)
    case 1
    then have "x > 0" by auto
    then have "(-x) < 0" by auto
    then show ?case by blast
  qed
qed

end

datatype ('c, 't :: time) cconstraint =
  AND "('c, 't) cconstraint" "('c, 't) cconstraint" |
  LT 'c 't |
  LE 'c 't |
  EQ 'c 't |
  GT 'c 't |
  GE 'c 't

section \<open>Syntactic Definition\<close>

text \<open>
  For an informal description of timed automata we refer to Bengtsson and Yi \cite{BengtssonY03}.
  We define a timed automaton \<open>A\<close>
\<close>

type_synonym
  ('c, 'time, 's) invassn = "'s \<Rightarrow> ('c, 'time) cconstraint"

type_synonym
  ('a, 'c, 'time, 's) transition = "'s * ('c, 'time) cconstraint * 'a * 'c list * 's"

type_synonym
  ('a, 'c, 'time, 's) ta = "('a, 'c, 'time, 's) transition set * ('c, 'time, 's) invassn"

definition trans_of :: "('a, 'c, 'time, 's) ta \<Rightarrow> ('a, 'c, 'time, 's) transition set" where
  "trans_of \<equiv> fst"
definition inv_of  :: "('a, 'c, 'time, 's) ta \<Rightarrow> ('c, 'time, 's) invassn" where
  "inv_of \<equiv> snd"

abbreviation transition ::
  "('a, 'c, 'time, 's) ta \<Rightarrow> 's \<Rightarrow> ('c, 'time) cconstraint \<Rightarrow> 'a \<Rightarrow> 'c list \<Rightarrow> 's \<Rightarrow> bool"
("_ \<turnstile> _ \<longrightarrow>\<^bsup>_,_,_\<^esup> _" [61,61,61,61,61,61] 61) where
  "(A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l') \<equiv> (l,g,a,r,l') \<in> trans_of A"

subsection \<open>Collecting Information About Clocks\<close>

fun collect_clks :: "('c, 't :: time) cconstraint \<Rightarrow> 'c set"
where
  "collect_clks (AND cc1 cc2) = collect_clks cc1 \<union> collect_clks cc2" |
  "collect_clks (LT c _) = {c}" |
  "collect_clks (LE c _) = {c}" |
  "collect_clks (EQ c _) = {c}" |
  "collect_clks (GE c _) = {c}" |
  "collect_clks (GT c _) = {c}"

fun collect_clock_pairs :: "('c, 't :: time) cconstraint \<Rightarrow> ('c * 't) set"
where
  "collect_clock_pairs (LT x m) = {(x, m)}" |
  "collect_clock_pairs (LE x m) = {(x, m)}" |
  "collect_clock_pairs (EQ x m) = {(x, m)}" |
  "collect_clock_pairs (GE x m) = {(x, m)}" |
  "collect_clock_pairs (GT x m) = {(x, m)}" |
  "collect_clock_pairs (AND cc1 cc2) = (collect_clock_pairs cc1 \<union> collect_clock_pairs cc2)"

definition collect_clkt :: "('a, 'c, 't::time, 's) transition set \<Rightarrow> ('c *'t) set"
where
  "collect_clkt S = \<Union> {collect_clock_pairs (fst (snd t)) | t . t \<in> S}"

definition collect_clki :: "('c, 't :: time, 's) invassn \<Rightarrow> ('c *'t) set"
where
  "collect_clki I = \<Union> {collect_clock_pairs (I x) | x. True}"

definition clkp_set :: "('a, 'c, 't :: time, 's) ta \<Rightarrow> ('c *'t) set"
where
  "clkp_set A = collect_clki (inv_of A) \<union> collect_clkt (trans_of A)"

definition collect_clkvt :: "('a, 'c, 't::time, 's) transition set \<Rightarrow> 'c set"
where
  "collect_clkvt S = \<Union> {set ((fst o snd o snd o snd) t) | t . t \<in> S}"

abbreviation clk_set where "clk_set A \<equiv> fst ` clkp_set A \<union> collect_clkvt (trans_of A)"

(* We don not need this here but most other theories will make use of this predicate *)
inductive valid_abstraction
where
  "\<lbrakk>\<forall>(x,m) \<in> clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat>; collect_clkvt (trans_of A) \<subseteq> X; finite X\<rbrakk>
  \<Longrightarrow> valid_abstraction A X k"

section \<open>Operational Semantics\<close>

type_synonym ('c, 't) cval = "'c \<Rightarrow> 't"

definition cval_add :: "('c,'t) cval \<Rightarrow> 't::time \<Rightarrow> ('c,'t) cval" (infixr "\<oplus>" 64)
where
  "u \<oplus> d = (\<lambda> x. u x + d)"

inductive clock_val :: "('c, 't) cval \<Rightarrow> ('c, 't::time) cconstraint \<Rightarrow> bool" ("_ \<turnstile> _" [62, 62] 62)
where
  "\<lbrakk>u \<turnstile> cc1; u \<turnstile> cc2\<rbrakk> \<Longrightarrow> u \<turnstile> AND cc1 cc2" |
  "\<lbrakk>u c < d\<rbrakk> \<Longrightarrow> u \<turnstile> LT c d" |
  "\<lbrakk>u c \<le> d\<rbrakk> \<Longrightarrow> u \<turnstile> LE c d" |
  "\<lbrakk>u c = d\<rbrakk> \<Longrightarrow> u \<turnstile> EQ c d" |
  "\<lbrakk>u c \<ge> d\<rbrakk> \<Longrightarrow> u \<turnstile> GE c d" |
  "\<lbrakk>u c > d\<rbrakk> \<Longrightarrow> u \<turnstile> GT c d"

declare clock_val.intros[intro]

inductive_cases[elim!]: "u \<turnstile> AND cc1 cc2"
inductive_cases[elim!]: "u \<turnstile> LT c d"
inductive_cases[elim!]: "u \<turnstile> LE c d"
inductive_cases[elim!]: "u \<turnstile> EQ c d"
inductive_cases[elim!]: "u \<turnstile> GE c d"
inductive_cases[elim!]: "u \<turnstile> GT c d"

fun clock_set :: "'c list \<Rightarrow> 't::time \<Rightarrow> ('c,'t) cval \<Rightarrow> ('c,'t) cval"
where
  "clock_set [] _ u = u" |
  "clock_set (c#cs) t u = (clock_set cs t u)(c:=t)"

abbreviation clock_set_abbrv :: "'c list \<Rightarrow> 't::time \<Rightarrow> ('c,'t) cval \<Rightarrow> ('c,'t) cval"
("[_\<rightarrow>_]_" [65,65,65] 65)
where
  "[r \<rightarrow> t]u \<equiv> clock_set r t u"

inductive step_t ::
  "('a, 'c, 't, 's) ta \<Rightarrow> 's \<Rightarrow> ('c, 't) cval \<Rightarrow> ('t::time) \<Rightarrow> 's \<Rightarrow> ('c, 't) cval \<Rightarrow> bool"
("_ \<turnstile> \<langle>_, _\<rangle> \<rightarrow>\<^bsup>_\<^esup> \<langle>_, _\<rangle>" [61,61,61] 61)
where
  "\<lbrakk>u \<turnstile> inv_of A l; u \<oplus> d \<turnstile> inv_of A l; d \<ge> 0\<rbrakk> \<Longrightarrow> A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l, u \<oplus> d\<rangle>"

declare step_t.intros[intro!]

inductive_cases[elim!]: "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l',u'\<rangle>"

lemma step_t_determinacy1:
  "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l',u'\<rangle> \<Longrightarrow>  A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l'',u''\<rangle> \<Longrightarrow> l' = l''"
by auto

lemma step_t_determinacy2:
  "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l',u'\<rangle> \<Longrightarrow>  A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l'',u''\<rangle> \<Longrightarrow> u' = u''"
by auto

lemma step_t_cont1:
  "d \<ge> 0 \<Longrightarrow> e \<ge> 0 \<Longrightarrow> A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l',u'\<rangle> \<Longrightarrow> A \<turnstile> \<langle>l', u'\<rangle> \<rightarrow>\<^bsup>e\<^esup> \<langle>l'',u''\<rangle>
  \<Longrightarrow> A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d+e\<^esup> \<langle>l'',u''\<rangle>"
proof -
  assume A: "d \<ge> 0" "e \<ge> 0" "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l',u'\<rangle>" "A \<turnstile> \<langle>l', u'\<rangle> \<rightarrow>\<^bsup>e\<^esup> \<langle>l'',u''\<rangle>"
  hence "u' = (u \<oplus> d)" "u'' = (u' \<oplus> e)" by auto
  hence "u'' = (u \<oplus> (d + e))" unfolding cval_add_def by auto
  with A show ?thesis by auto
qed

inductive step_a ::
  "('a, 'c, 't, 's) ta \<Rightarrow> 's \<Rightarrow> ('c, ('t::time)) cval \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> ('c, 't) cval \<Rightarrow> bool"
("_ \<turnstile> \<langle>_, _\<rangle> \<rightarrow>\<^bsub>_\<^esub> \<langle>_, _\<rangle>" [61,61,61] 61)
where
  "\<lbrakk>A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'; u \<turnstile> g; u' \<turnstile> inv_of A l'; u' = [r \<rightarrow> 0]u\<rbrakk> \<Longrightarrow> (A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsub>a\<^esub> \<langle>l', u'\<rangle>)"

inductive step ::
  "('a, 'c, 't, 's) ta \<Rightarrow> 's \<Rightarrow> ('c, ('t::time)) cval \<Rightarrow> 's \<Rightarrow> ('c, 't) cval \<Rightarrow> bool"
("_ \<turnstile> \<langle>_, _\<rangle> \<rightarrow> \<langle>_,_\<rangle>" [61,61,61] 61)
where
  step_a: "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsub>a\<^esub> \<langle>l',u'\<rangle> \<Longrightarrow> (A \<turnstile> \<langle>l, u\<rangle> \<rightarrow> \<langle>l',u'\<rangle>)" |
  step_t: "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>\<^bsup>d\<^esup> \<langle>l',u'\<rangle> \<Longrightarrow> (A \<turnstile> \<langle>l, u\<rangle> \<rightarrow> \<langle>l',u'\<rangle>)"

inductive_cases[elim!]: "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow> \<langle>l',u'\<rangle>"

declare step.intros[intro]

inductive
  steps :: "('a, 'c, 't, 's) ta \<Rightarrow> 's \<Rightarrow> ('c, ('t::time)) cval \<Rightarrow> 's \<Rightarrow> ('c, 't) cval \<Rightarrow> bool"
("_ \<turnstile> \<langle>_, _\<rangle> \<rightarrow>* \<langle>_, _\<rangle>" [61,61,61] 61)
where
  refl: "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>* \<langle>l, u\<rangle>" |
  step: "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow> \<langle>l', u'\<rangle> \<Longrightarrow> A \<turnstile> \<langle>l', u'\<rangle> \<rightarrow>* \<langle>l'', u''\<rangle> \<Longrightarrow> A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>* \<langle>l'', u''\<rangle>"

declare steps.intros[intro]

section \<open>Zone Semantics\<close>

type_synonym ('c, 't) zone = "('c, 't) cval set"

definition zone_delay :: "('c, ('t::time)) zone \<Rightarrow> ('c, 't) zone"
("_\<^sup>\<up>" [71] 71)
where
  "Z\<^sup>\<up> = {u \<oplus> d|u d. u \<in> Z \<and> d \<ge> (0::'t)}"

definition zone_set :: "('c, 't::time) zone \<Rightarrow> 'c list \<Rightarrow> ('c, 't) zone"
("_\<^bsub>_ \<rightarrow> 0\<^esub>" [71] 71)
where
  "zone_set Z r = {[r \<rightarrow> (0::'t)]u | u . u \<in> Z}"

inductive step_z ::
  "('a, 'c, 't, 's) ta \<Rightarrow> 's \<Rightarrow> ('c, ('t::time)) zone \<Rightarrow> 's \<Rightarrow> ('c, 't) zone \<Rightarrow> bool"
("_ \<turnstile> \<langle>_, _\<rangle> \<leadsto> \<langle>_, _\<rangle>" [61,61,61] 61)
where
  step_t_z: "A \<turnstile> \<langle>l, Z\<rangle> \<leadsto> \<langle>l, (Z \<inter> {u. u \<turnstile> inv_of A l})\<^sup>\<up> \<inter> {u. u \<turnstile> inv_of A l}\<rangle>" |
  step_a_z: "\<lbrakk>A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'\<rbrakk>
              \<Longrightarrow> (A \<turnstile> \<langle>l, Z\<rangle> \<leadsto> \<langle>l', zone_set (Z \<inter> {u. u \<turnstile> g}) r \<inter> {u. u \<turnstile> inv_of A l'}\<rangle> )"

inductive_cases[elim!]: "A \<turnstile> \<langle>l, u\<rangle> \<leadsto> \<langle>l', u'\<rangle>"

declare step_z.intros[intro]

lemma step_z_sound:
  "A \<turnstile> \<langle>l, Z\<rangle> \<leadsto> \<langle>l',Z'\<rangle> \<Longrightarrow> (\<forall> u' \<in> Z'. \<exists> u \<in> Z.  A \<turnstile> \<langle>l, u\<rangle> \<rightarrow> \<langle>l',u'\<rangle>)"
proof (induction rule: step_z.induct, goal_cases)
  case 1 thus ?case unfolding zone_delay_def by blast
next
  case (2 A l g a r l' Z)
  show ?case
  proof
    fix u' assume "u' \<in> zone_set (Z \<inter> {u. u \<turnstile> g}) r \<inter> {u. u \<turnstile> inv_of A l'}"
    then obtain u where
      "u \<turnstile> g" "u' \<turnstile> inv_of A l'" "u' = [r\<rightarrow>0]u" "u \<in> Z"
    unfolding zone_set_def by auto
    with step_a.intros[OF 2 this(1-3)] show "\<exists>u\<in>Z. A \<turnstile> \<langle>l, u\<rangle> \<rightarrow> \<langle>l',u'\<rangle>" by fast
  qed
qed

text \<open>
  Corresponds to version in old papers --
  not strong enough for inductive proof over transitive closure relation.
\<close>
lemma step_z_complete1:
  "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow> \<langle>l', u'\<rangle> \<Longrightarrow> \<exists> Z. A \<turnstile> \<langle>l, {u}\<rangle> \<leadsto> \<langle>l', Z\<rangle> \<and> u' \<in> Z"
proof (induction rule: step.induct, goal_cases)
  case (1 A l u a l' u')
  then obtain g r
  where u': "u' = [r\<rightarrow>0]u" "A \<turnstile> l \<longrightarrow>\<^bsup>g,a,r\<^esup> l'" "u \<turnstile> g" "[r\<rightarrow>0]u \<turnstile> inv_of A l'"
  by (cases rule: step_a.cases) auto
  hence "{[r\<rightarrow>0]u} = zone_set ({u} \<inter> {u. u \<turnstile> g}) r \<inter> {u. u \<turnstile> inv_of A l'}"
  unfolding zone_set_def by blast
  with u'(1,2) show ?case by auto
next
  case (2 A l u d l' u')
  hence u': "u' = (u \<oplus> d)" "u \<turnstile> inv_of A l" "u \<oplus> d \<turnstile> inv_of A l" "0 \<le> d" and "l = l'" by auto
  hence "{u} = {u} \<inter> {u''. u'' \<turnstile> inv_of A l}" by fastforce
  with u'(1) have "{u'} = {u'' \<oplus> d |u''. u'' \<in> {u} \<inter> {u''. u'' \<turnstile> inv_of A l}}" by fastforce
  with u' have
    "u' \<in> {u'' \<oplus> d |u'' d. u'' \<in> {u} \<inter> {u. u \<turnstile> inv_of A l} \<and> 0 \<le> d} \<inter> {u. u \<turnstile> inv_of A l}"
  by fastforce
  thus ?case using \<open>l = l'\<close> step_t_z[unfolded zone_delay_def, of A l "{u}"] by blast
qed

text \<open>
  Easier proof.
\<close>
lemma step_z_complete2:
  "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow> \<langle>l', u'\<rangle> \<Longrightarrow> \<exists> Z. A \<turnstile> \<langle>l, {u}\<rangle> \<leadsto> \<langle>l', Z\<rangle> \<and> u' \<in> Z"
using step_z_complete by fast

inductive
  steps_z :: "('a, 'c, 't, 's) ta \<Rightarrow> 's \<Rightarrow> ('c, ('t::time)) zone \<Rightarrow> 's \<Rightarrow> ('c, 't) zone \<Rightarrow> bool"
("_ \<turnstile> \<langle>_, _\<rangle> \<leadsto>* \<langle>_, _\<rangle>" [61,61,61] 61)
where
  refl: "A \<turnstile> \<langle>l, Z\<rangle> \<leadsto>* \<langle>l, Z\<rangle>" |
  step: "A \<turnstile> \<langle>l, Z\<rangle> \<leadsto> \<langle>l', Z'\<rangle> \<Longrightarrow> A \<turnstile> \<langle>l', Z'\<rangle> \<leadsto>* \<langle>l'', Z''\<rangle> \<Longrightarrow> A \<turnstile> \<langle>l, Z\<rangle> \<leadsto>* \<langle>l'', Z''\<rangle>"

declare steps_z.intros[intro]

lemma steps_z_complete:
  "A \<turnstile> \<langle>l, u\<rangle> \<rightarrow>* \<langle>l', u'\<rangle> \<Longrightarrow> u \<in> Z \<Longrightarrow> \<exists> Z'. A \<turnstile> \<langle>l, Z\<rangle> \<leadsto>* \<langle>l', Z'\<rangle> \<and> u' \<in> Z'"
proof (induction arbitrary: Z rule: steps.induct)
  case refl thus ?case by auto
next
  case (step A l u l' u' l'' u'' Z)
  from step_z_complete[OF this(1,4)] obtain Z' where Z': "A \<turnstile> \<langle>l, Z\<rangle> \<leadsto> \<langle>l',Z'\<rangle>" "u' \<in> Z'" by auto
  then obtain Z'' where "A \<turnstile> \<langle>l', Z'\<rangle> \<leadsto>* \<langle>l'',Z''\<rangle>" "u'' \<in> Z''" using step by metis
  with Z' show ?case by blast
qed

end


text:
(*
    Author:     Vincent Trélat <vincent.trelat@depinfonancy.net>
*)

theory Utils
  imports Main "HOL-Library.Multiset"
begin

definition subset_mset_rel :: "('a multiset * 'a multiset) set" where
  "subset_mset_rel \<equiv> {(A,B). A <# B}"

primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
  "multiset_of [] = {#}" |
  "multiset_of (a # x) = multiset_of x + {# a #}"

lemma multiset_of_append [simp]:
  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
  by (induct xs arbitrary: ys) (auto simp: add_ac)

lemma triple_conjI:
  "\<lbrakk>P \<and> Q; R\<rbrakk> \<Longrightarrow> P \<and> Q \<and> R"
  by simp
end

author: VTrelat


text:
theory Cuadrado
imports Main
begin

text {* (cuadrado x) es el cuadrado de x. Por ejemplo,
     cuadrado 3 = 9
*}
definition cuadrado :: "int \<Rightarrow> int" where
  "cuadrado n = n*n"

value "cuadrado 3"
lemma "cuadrado 3 = 9" by (simp add: cuadrado_def)

end

author: jaalonso

repo: SLP

save_path: github-repos/isabelle/jaalonso-SLP