Theory Refine_Misc

header {* \isaheader{Miscellanneous Lemmas and Tools} *}
theory Refine_Misc
imports 
  "../Automatic_Refinement/Automatic_Refinement"
  Refine_Mono_Prover
begin

subsection {* Uncategorized Lemmas *}
lemma all_nat_split_at: "∀i::'a::linorder<k. P i ==> P k ==> ∀i>k. P i 
  ==> ∀i. P i"
  by (metis linorder_neq_iff)

subsection {* Well-Foundedness *}

lemma wf_no_infinite_down_chainI:
  assumes "!!f. [|!!i. (f (Suc i), f i)∈r|] ==> False"
  shows "wf r"
  by (metis assms wf_iff_no_infinite_down_chain)

text {* This lemma transfers well-foundedness over a simulation relation. *}
lemma sim_wf:
  assumes WF: "wf (S'¯)"
  assumes STARTR: "(x0,x0')∈R"
  assumes SIM: "!!s s' t. [| (s,s')∈R; (s,t)∈S; (x0',s')∈S'⇧* |] 
    ==> ∃t'. (s',t')∈S' ∧ (t,t')∈R"
  assumes CLOSED: "Domain S  ⊆ S⇧*``{x0}"
  shows "wf (S¯)"
proof (rule wf_no_infinite_down_chainI, simp)
  txt {*
    Informal proof:
    Assume there is an infinite chain in @{text "S"}.
    Due to the closedness property of @{text "S"}, it can be extended to 
    start at @{text x0}.
    Now, we inductively construct an infinite chain in @{text "S'"}, such that
    each element of the new chain is in relation with the corresponding 
    element of the original chain:
      The first element is @{text "x0'"}. 
      For any element @{text "i+1"}, the simulation property yields the next
      element.
    This chain contradicts well-foundedness of @{text "S'"}.
    *}

  fix f
  assume CHAIN: "!!i. (f i, f (Suc i))∈S"
  txt {* Extend to start with @{text "x0"} *}
  obtain f' where CHAIN': "!!i. (f' i, f' (Suc i))∈S" and [simp]: "f' 0 = x0"
  proof -
    {
      fix x
      assume S: "x = f 0"
      from CHAIN have "f 0 ∈ Domain S" by auto
      with CLOSED have "(x0,x)∈S⇧*" by (auto simp: S)
      then obtain g k where G0: "g 0 = x0" and X: "x = g k" 
        and CH: "(∀i<k. (g i, g (Suc i))∈S)"
      proof induct
        case base thus ?case by force
      next
        case (step y z) show ?case proof (rule step.hyps(3))
          fix g k 
          assume "g 0 = x0" and "y = g k" 
            and "∀i<k. (g i, g (Suc i))∈S"
          thus ?case using `(y,z)∈S`
            by (rule_tac step.prems[where g="g(Suc k := z)" and k="Suc k"])
              auto
        qed
      qed
      def f'≡"λi. if i<k then g i else f (i-k)"
      have "∃f'. f' 0 = x0 ∧ (∀i. (f' i, f' (Suc i))∈S)"
        apply (rule_tac x=f' in exI)
        apply (unfold f'_def)
        apply (rule conjI)
        using S X G0 apply (auto) []
        apply (rule_tac k=k in all_nat_split_at)
        apply (auto)
        apply (simp add: CH)
        apply (subgoal_tac "k = Suc i")
        apply (simp add: S[symmetric] CH X)
        apply simp
        apply (simp add: CHAIN)
        apply (subgoal_tac "Suc i - k = Suc (i-k)")
        using CHAIN apply simp
        apply simp
        done
    }
    then obtain f' where "∀i. (f' i,f' (Suc i))∈S" and "f' 0 = x0" by blast
    thus ?thesis by (blast intro!: that)
  qed

  txt {* Construct chain in @{text "S'"}*}
  def g'≡"rec_nat x0' (λi x. SOME x'. 
          (x,x')∈S' ∧ (f' (Suc i),x')∈R ∧ (x0', x')∈S'⇧* )"
  {
    fix i
    note [simp] = g'_def
    have "(g' i, g' (Suc i))∈S' ∧ (f' (Suc i),g' (Suc i))∈R 
      ∧ (x0',g' (Suc i))∈S'⇧*"
    proof (induct i)
      case 0 
      from SIM[OF STARTR] CHAIN'[of 0] obtain t' where 
        "(x0',t')∈S'" and "(f' (Suc 0),t')∈R" by auto
      moreover hence "(x0',t')∈S'⇧*" by auto
      ultimately show ?case
        by (auto intro: someI2 simp: STARTR)
    next
      case (Suc i)
      with SIM[OF _ CHAIN'[of "Suc i"]] 
      obtain t' where LS: "(g' (Suc i),t')∈S'" and "(f' (Suc (Suc i)),t')∈R"
        by auto
      moreover from LS Suc have "(x0', t')∈S'⇧*" by auto
      ultimately show ?case
        apply simp
        apply (rule_tac a="t'" in someI2)
        apply auto
        done
    qed
  } hence S'CHAIN: "∀i. (g' i, g'(Suc i))∈S'" by simp
  txt {* This contradicts well-foundedness *}
  with WF show False 
    by (erule_tac wf_no_infinite_down_chainE[where f=g']) simp
qed

text {* Well-founded relation that approximates a finite set from below. *}
definition "finite_psupset S ≡ { (Q',Q). Q⊂Q' ∧ Q' ⊆ S }"
lemma finite_psupset_wf[simp, intro]: "finite S ==> wf (finite_psupset S)"
  unfolding finite_psupset_def by (blast intro: wf_bounded_supset)

subsection {* Monotonicity and Orderings *}

lemma mono_const[simp, intro!]: "mono (λ_. c)" by (auto intro: monoI)
lemma mono_if: "[|mono S1; mono S2|] ==>
  mono (λF s. if b s then S1 F s else S2 F s)"
  apply rule
  apply (rule le_funI)
  apply (auto dest: monoD[THEN le_funD])
  done

lemma mono_infI: "mono f ==> mono g ==> mono (inf f g)"
  unfolding inf_fun_def
  apply (rule monoI)
  apply (metis inf_mono monoD)
  done

lemma mono_infI': 
  "mono f ==> mono g ==> mono (λx. inf (f x) (g x) :: 'b::lattice)"
  by (rule mono_infI[unfolded inf_fun_def])

lemma mono_infArg: 
  fixes f :: "'a::lattice => 'b::order"
  shows "mono f ==> mono (λx. f (inf x X))"
  apply (rule monoI)
  apply (erule monoD)
  apply (metis inf_mono order_refl) 
  done

lemma mono_Sup:
  fixes f :: "'a::complete_lattice => 'b::complete_lattice"
  shows "mono f ==> Sup (f`S) ≤ f (Sup S)"
  apply (rule Sup_least)
  apply (erule imageE)
  apply simp
  apply (erule monoD)
  apply (erule Sup_upper)
  done

lemma mono_SupI:
  fixes f :: "'a::complete_lattice => 'b::complete_lattice"
  assumes "mono f"
  assumes "S'⊆f`S"
  shows "Sup S' ≤ f (Sup S)"
  by (metis Sup_subset_mono assms mono_Sup order_trans)

lemma mono_Inf:
  fixes f :: "'a::complete_lattice => 'b::complete_lattice"
  shows "mono f ==> f (Inf S) ≤ Inf (f`S)"
  apply (rule Inf_greatest)
  apply (erule imageE)
  apply simp
  apply (erule monoD)
  apply (erule Inf_lower)
  done

lemma mono_funpow: "mono (f::'a::order => 'a) ==> mono (f^^i)"
  apply (induct i)
  apply (auto intro!: monoI) 
  apply (auto dest: monoD)
  done

lemma mono_id[simp, intro!]:
  "mono id"
  "mono (λx. x)"
  by (auto intro: monoI)

declare SUP_insert[simp]

lemma (in semilattice_inf) le_infD1:
  "a ≤ inf b c ==> a ≤ b" by (rule le_infE)
lemma (in semilattice_inf) le_infD2:
  "a ≤ inf b c ==> a ≤ c" by (rule le_infE)
lemma (in semilattice_inf) inf_leI:
  "[| !!x. [| x≤a; x≤b |] ==> x≤c |] ==> inf a b ≤ c"
  by (metis inf_le1 inf_le2)

lemma top_Sup: "(top::'a::complete_lattice)∈A ==> Sup A = top"
  by (metis Sup_upper top_le)
lemma bot_Inf: "(bot::'a::complete_lattice)∈A ==> Inf A = bot"
  by (metis Inf_lower le_bot)

lemma mono_compD: "mono f ==> x≤y ==> f o x ≤ f o y"
  apply (rule le_funI)
  apply (auto dest: monoD le_funD)
  done


subsubsection {* Galois Connections *}
locale galois_connection =
  fixes α::"'a::complete_lattice => 'b::complete_lattice" and γ
  assumes galois: "c ≤ γ(a) <-> α(c) ≤ a"
begin
  lemma αγ_defl: "α(γ(x)) ≤ x"
  proof -
    have "γ x ≤ γ x" by simp
    with galois show "α(γ(x)) ≤ x" by blast
  qed
  lemma γα_infl: "x ≤ γ(α(x))"
  proof -
    have "α x ≤ α x" by simp
    with galois show "x ≤ γ(α(x))" by blast
  qed
    
  lemma α_mono: "mono α"
  proof 
    fix x::'a and y::'a
    assume "x≤y"
    also note γα_infl[of y]
    finally show "α x ≤ α y" by (simp add: galois)
  qed

  lemma γ_mono: "mono γ"
    by rule (metis αγ_defl galois inf_absorb1 le_infE)

  lemma dist_γ[simp]: 
    "γ (inf a b) = inf (γ a) (γ b)"
    apply (rule order_antisym)
    apply (rule mono_inf[OF γ_mono])
    apply (simp add: galois)
    apply (simp add: galois[symmetric])
    done

  lemma dist_α[simp]: 
    "α (sup a b) = sup (α a) (α b)"
    by (metis (no_types) α_mono galois mono_sup order_antisym 
      sup_ge1 sup_ge2 sup_least)

end

subsubsection {* Fixed Points *}
lemma mono_lfp_eqI:
  assumes MONO: "mono f"
  assumes FIXP: "f a ≤ a"
  assumes LEAST: "!!x. f x = x ==> a≤x"
  shows "lfp f = a"
  apply (rule antisym)
  apply (rule lfp_lowerbound)
  apply (rule FIXP)
  by (metis LEAST MONO lfp_unfold)

lemma mono_gfp_eqI:
  assumes MONO: "mono f"
  assumes FIXP: "a ≤ f a"
  assumes GREATEST: "!!x. f x = x ==> x≤a"
  shows "gfp f = a"
  apply (rule antisym)
  apply (metis GREATEST MONO gfp_unfold)
  apply (rule gfp_upperbound)
  apply (rule FIXP)
  done

lemma lfp_le_gfp: "mono f ==> lfp f ≤ gfp f"
  by (metis gfp_upperbound lfp_lemma3)

lemma lfp_le_gfp': "mono f ==> lfp f x ≤ gfp f x"
  by (rule le_funD[OF lfp_le_gfp])

subsubsection {* Connecting Complete Lattices and 
  Chain-Complete Partial Orders *}
(* Note: Also connected by subclass now. However, we need both directions
  of embedding*)
lemma (in complete_lattice) is_ccpo: "class.ccpo Sup (op ≤) (op <)"
  apply unfold_locales
  apply (erule Sup_upper)
  apply (erule Sup_least)
  done

lemma (in complete_lattice) is_dual_ccpo: "class.ccpo Inf (op ≥) (op >)"
  apply unfold_locales
  apply (rule less_le_not_le)
  apply (rule order_refl)
  apply (erule (1) order_trans)
  apply (erule (1) antisym)
  apply (erule Inf_lower)
  apply (erule Inf_greatest)
  done
  
  
lemma ccpo_mono_simp: "monotone (op ≤) (op ≤) f <-> mono f"
  unfolding monotone_def mono_def by simp
lemma ccpo_monoI: "mono f ==> monotone (op ≤) (op ≤) f" 
  by (simp add: ccpo_mono_simp) 
lemma ccpo_monoD: "monotone (op ≤) (op ≤) f ==> mono f" 
  by (simp add: ccpo_mono_simp) 

lemma dual_ccpo_mono_simp: "monotone (op ≥) (op ≥) f <-> mono f"
  unfolding monotone_def mono_def by auto
lemma dual_ccpo_monoI: "mono f ==> monotone (op ≥) (op ≥) f" 
  by (simp add: dual_ccpo_mono_simp) 
lemma dual_ccpo_monoD: "monotone (op ≥) (op ≥) f ==> mono f" 
  by (simp add: dual_ccpo_mono_simp) 

lemma ccpo_lfp_simp: "!!f. mono f ==> ccpo.fixp Sup op ≤ f = lfp f"
  apply (rule antisym)
  defer
  apply (rule lfp_lowerbound)
  apply (drule ccpo.fixp_unfold[OF is_ccpo ccpo_monoI, symmetric])
  apply simp

  apply (rule ccpo.fixp_lowerbound[OF is_ccpo ccpo_monoI], assumption)
  apply (simp add: lfp_unfold[symmetric])
  done

lemma ccpo_gfp_simp: "!!f. mono f ==> ccpo.fixp Inf op ≥ f = gfp f"
  apply (rule antisym)
  apply (rule gfp_upperbound)
  apply (drule ccpo.fixp_unfold[OF is_dual_ccpo dual_ccpo_monoI, symmetric])
  apply simp

  apply (rule ccpo.fixp_lowerbound[OF is_dual_ccpo dual_ccpo_monoI], assumption)
  apply (simp add: gfp_unfold[symmetric])
  done

abbreviation "chain_admissible P ≡ ccpo.admissible Sup op ≤ P"
abbreviation "is_chain ≡ Complete_Partial_Order.chain (op ≤)"
lemmas chain_admissibleI[intro?] = ccpo.admissibleI[where lub=Sup and ord="op ≤"]


abbreviation "dual_chain_admissible P ≡ ccpo.admissible Inf (λx y. y≤x) P"
abbreviation "is_dual_chain ≡ Complete_Partial_Order.chain (λx y. y≤x)"
lemmas dual_chain_admissibleI[intro?] = 
  ccpo.admissibleI[where lub=Inf and ord="(λx y. y≤x)"]

lemma dual_chain_iff[simp]: "is_dual_chain C = is_chain C"
  unfolding chain_def
  apply auto
  done

lemmas chain_dualI = iffD1[OF dual_chain_iff]
lemmas dual_chainI = iffD2[OF dual_chain_iff]

lemma is_chain_empty[simp, intro!]: "is_chain {}"
  by (rule chainI) auto
lemma is_dual_chain_empty[simp, intro!]: "is_dual_chain {}"
  by (rule dual_chainI) auto

lemma point_chainI: "is_chain M ==> is_chain ((λf. f x)`M)"
  by (auto intro: chainI le_funI dest: chainD le_funD)


text {* We transfer the admissible induction lemmas to complete
  lattices. *}
lemma lfp_cadm_induct:
  "[|chain_admissible P; P (Sup {}); mono f; !!x. P x ==> P (f x)|] ==> P (lfp f)"
  by (simp only: ccpo_mono_simp[symmetric] ccpo_lfp_simp[symmetric])
     (rule ccpo.fixp_induct[OF is_ccpo])

lemma gfp_cadm_induct:
  "[|dual_chain_admissible P; P (Inf {}); mono f; !!x. P x ==> P (f x)|] ==> P (gfp f)"
  by (simp only: dual_ccpo_mono_simp[symmetric] ccpo_gfp_simp[symmetric])
     (rule ccpo.fixp_induct[OF is_dual_ccpo])

subsubsection {* Continuity and Kleene Fixed Point Theorem *}
definition "cont f ≡ ∀C. C≠{} --> f (Sup C) = Sup (f`C)"
definition "strict f ≡ f bot = bot"
definition "inf_distrib f ≡ strict f ∧ cont f"

lemma contI[intro?]: "[|!!C. C≠{} ==> f (Sup C) = Sup (f`C)|] ==> cont f" 
  unfolding cont_def by auto
lemma contD: "cont f ==> C≠{} ==> f (Sup C) = Sup (f`C)" 
  unfolding cont_def by auto
lemma contD': "cont f ==> C≠{} ==> f (Sup C) = SUPREMUM C f" 
  using contD by simp

lemma strictD[dest]: "strict f ==> f bot = bot" 
  unfolding strict_def by auto
-- "We only add this lemma to the simpset for functions on the same type. 
    Otherwise, the simplifier tries it much too often."
lemma strictD_simp[simp]: "strict f ==> f (bot::'a::bot) = (bot::'a)" 
  unfolding strict_def by auto

lemma strictI[intro?]: "f bot = bot ==> strict f"
  unfolding strict_def by auto

lemma inf_distribD[simp]: 
  "inf_distrib f ==> strict f"
  "inf_distrib f ==> cont f"
  unfolding inf_distrib_def by auto

lemma inf_distribI[intro?]: "[|strict f; cont f|] ==> inf_distrib f"
  unfolding inf_distrib_def by auto

lemma inf_distribD'[simp]:
  fixes f :: "'a::complete_lattice => 'b::complete_lattice"
  shows "inf_distrib f ==> f (Sup C) = Sup (f`C)"
  apply (cases "C={}")
  apply (auto dest: inf_distribD contD')
  done

lemma inf_distribI':
  fixes f :: "'a::complete_lattice => 'b::complete_lattice"
  assumes B: "!!C. f (Sup C) = Sup (f`C)"
  shows "inf_distrib f"
  apply (rule)
  apply (rule)
  apply (rule B[of "{}", simplified])
  apply (rule)
  apply (rule B)
  done
  
lemma cont_is_mono[simp]: 
  fixes f :: "'a::complete_lattice => 'b::complete_lattice"
  shows "cont f ==> mono f"
  apply (rule monoI)
  apply (drule_tac C="{x,y}" in contD)
  apply (auto simp: le_iff_sup)
  done

lemma inf_distrib_is_mono[simp]: 
  fixes f :: "'a::complete_lattice => 'b::complete_lattice"
  shows "inf_distrib f ==> mono f"
  by simp

text {* Only proven for complete lattices here. Also holds for CCPOs. *}
theorem kleene_lfp:
  fixes f:: "'a::complete_lattice => 'a"
  assumes CONT: "cont f"
  shows "lfp f = (SUP i. (f^^i) bot)"
proof (rule antisym)
  let ?K="{ (f^^i) bot | i . True}"
  note MONO=cont_is_mono[OF CONT]
  {
    fix i
    have "(f^^i) bot ≤ lfp f"
      apply (induct i)
      apply simp
      apply simp
      by (metis MONO lfp_unfold monoD)
  } thus "(SUP i. (f^^i) bot) ≤ lfp f" by (blast intro: SUP_least)
next
  show "lfp f ≤ (SUP i. (f^^i) bot)"
    apply (rule lfp_lowerbound)
    unfolding SUP_def
    apply (simp add: contD [OF CONT] del: Sup_image_eq)
    apply (rule Sup_subset_mono)
    apply (auto)
    apply (rule_tac x="Suc i" in range_eqI)
    apply auto
    done
qed


lemma (in galois_connection) dual_inf_dist_γ: "γ (Inf C) = Inf (γ`C)"
  apply (rule antisym)
  apply (rule Inf_greatest)
  apply clarify
  apply (rule monoD[OF γ_mono])
  apply (rule Inf_lower)
  apply simp

  apply (subst galois)
  apply (rule Inf_greatest)
  apply (subst galois[symmetric])
  apply (rule Inf_lower)
  apply simp
  done

lemma (in galois_connection) inf_dist_α: "inf_distrib α"
  apply (rule inf_distribI')
  apply (rule antisym)

  apply (subst galois[symmetric])
  apply (rule Sup_least)
  apply (subst galois)
  apply (rule Sup_upper)
  apply simp

  apply (rule Sup_least)
  apply clarify
  apply (rule monoD[OF α_mono])
  apply (rule Sup_upper)
  apply simp
  done

subsection {* Maps *}
subsubsection {* Key-Value Set *}
  
  lemma map_to_set_simps[simp]: 
    "map_to_set Map.empty = {}"
    "map_to_set [a\<mapsto>b] = {(a,b)}"
    "map_to_set (m|`K) = map_to_set m ∩ K×UNIV"
    "map_to_set (m(x:=None)) = map_to_set m - {x}×UNIV"
    "map_to_set (m(x\<mapsto>v)) = map_to_set m - {x}×UNIV ∪ {(x,v)}"
    "map_to_set m ∩ dom m×UNIV = map_to_set m"
    "m k = Some v ==> (k,v)∈map_to_set m"
    "single_valued (map_to_set m)"
    apply (simp_all)
    by (auto simp: map_to_set_def restrict_map_def split: split_if_asm
      intro: single_valuedI)
      
  lemma map_to_set_inj:     
    "(k,v)∈map_to_set m ==> (k,v')∈map_to_set m ==> v = v'"
    by (auto simp: map_to_set_def)


end