text:
section\<open>Auxiliary results on arithmetic\<close>

theory Nat_Miscellanea
  imports
    Delta_System_Lemma.ZF_Library
begin

hide_const (open) Order.pred
notation add (infixl \<open>+\<^sub>\<omega>\<close> 65)
notation diff (infixl \<open>-\<^sub>\<omega>\<close> 65)

text\<open>Most of these results will get used at some point for the
calculation of arities.\<close>

lemmas nat_succI =  Ord_succ_mem_iff [THEN iffD2,OF nat_into_Ord]

lemma nat_succD : "m \<in> nat \<Longrightarrow>  succ(n) \<in> succ(m) \<Longrightarrow> n \<in> m"
  by (drule_tac j="succ(m)" in ltI,auto elim:ltD)

lemmas zero_in_succ = ltD [OF nat_0_le]

lemma in_n_in_nat :  "m \<in> nat \<Longrightarrow> n \<in> m \<Longrightarrow> n \<in> nat"
  by(drule ltI[of "n"],auto simp add: lt_nat_in_nat)

lemma ltI_neg : "x \<in> nat \<Longrightarrow> j \<le> x \<Longrightarrow> j \<noteq> x \<Longrightarrow> j < x"
  by (simp add: le_iff)

lemma succ_pred_eq  :  "m \<in> nat \<Longrightarrow> m \<noteq> 0  \<Longrightarrow> succ(pred(m)) = m"
  by (auto elim: natE)

lemma succ_ltI : "succ(j) < n \<Longrightarrow> j < n"
  by (simp add: succ_leE[OF leI])

lemmas succ_leD = succ_leE[OF leI]

lemma succpred_leI : "n \<in> nat \<Longrightarrow>  n \<le> succ(pred(n))"
  by (auto elim: natE)

lemma succpred_n0 : "succ(n) \<in> p \<Longrightarrow> p\<noteq>0"
  by (auto)

lemmas natEin = natE [OF lt_nat_in_nat]

lemmas Un_least_lt_iffn =  Un_least_lt_iff [OF nat_into_Ord nat_into_Ord]

lemma pred_type : "m \<in> nat \<Longrightarrow> n \<le> m \<Longrightarrow> n\<in>nat"
  by (rule leE,auto simp:in_n_in_nat ltD)

lemma pred_le : "m \<in> nat \<Longrightarrow> n \<le> succ(m) \<Longrightarrow> pred(n) \<le> m"
  by(rule_tac n="n" in natE,auto simp add:pred_type[of "succ(m)"])

lemma pred_le2 : "n\<in> nat \<Longrightarrow> m \<in> nat \<Longrightarrow> pred(n) \<le> m \<Longrightarrow> n \<le> succ(m)"
  by(subgoal_tac "n\<in>nat",rule_tac n="n" in natE,auto)

lemma Un_leD1 : "Ord(i)\<Longrightarrow> Ord(j)\<Longrightarrow> Ord(k)\<Longrightarrow>  i \<union> j \<le> k \<Longrightarrow> i \<le> k"
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct1]],simp_all)

lemma Un_leD2 : "Ord(i)\<Longrightarrow> Ord(j)\<Longrightarrow> Ord(k)\<Longrightarrow>  i \<union> j \<le>k \<Longrightarrow> j \<le> k"
  by (rule Un_least_lt_iff[THEN iffD1[THEN conjunct2]],simp_all)

lemma gt1 : "n \<in> nat \<Longrightarrow> i \<in> n \<Longrightarrow> i \<noteq> 0 \<Longrightarrow> i \<noteq> 1 \<Longrightarrow> 1<i"
  by(rule_tac n="i" in natE,erule in_n_in_nat,auto intro: Ord_0_lt)

lemma pred_mono : "m \<in> nat \<Longrightarrow> n \<le> m \<Longrightarrow> pred(n) \<le> pred(m)"
  by(rule_tac n="n" in natE,auto simp add:le_in_nat,erule_tac n="m" in natE,auto)

lemma succ_mono : "m \<in> nat \<Longrightarrow> n \<le> m \<Longrightarrow> succ(n) \<le> succ(m)"
  by auto

lemma union_abs1 :
  "\<lbrakk> i \<le> j \<rbrakk> \<Longrightarrow> i \<union> j = j"
  by (rule Un_absorb1,erule le_imp_subset)

lemma union_abs2 :
  "\<lbrakk> i \<le> j \<rbrakk> \<Longrightarrow> j \<union> i = j"
  by (rule Un_absorb2,erule le_imp_subset)

lemma ord_un_max : "Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i \<union> j = max(i,j)"
  using max_def union_abs1 not_lt_iff_le leI union_abs2
  by auto

lemma ord_max_ty : "Ord(i) \<Longrightarrow>Ord(j) \<Longrightarrow> Ord(max(i,j))"
  unfolding max_def by simp

lemmas ord_simp_union = ord_un_max ord_max_ty max_def

lemma le_succ : "x\<in>nat \<Longrightarrow> x\<le>succ(x)" by simp

lemma le_pred : "x\<in>nat \<Longrightarrow> pred(x)\<le>x"
  using pred_le[OF _ le_succ] pred_succ_eq
  by simp

lemma not_le_anti_sym : "x\<in>nat \<Longrightarrow> y \<in> nat \<Longrightarrow> \<not> x\<le>y \<Longrightarrow> \<not>y\<le>x \<Longrightarrow> y=x"
  using Ord_linear not_le_iff_lt ltD lt_trans
  by auto

lemma Un_le_compat : "o \<le> p \<Longrightarrow> q \<le> r \<Longrightarrow> Ord(o) \<Longrightarrow> Ord(p) \<Longrightarrow> Ord(q) \<Longrightarrow> Ord(r) \<Longrightarrow> o \<union> q \<le> p \<union> r"
  using le_trans[of q r "p\<union>r",OF _ Un_upper2_le] le_trans[of o p "p\<union>r",OF _ Un_upper1_le]
    ord_simp_union
  by auto

lemma Un_le : "p \<le> r \<Longrightarrow> q \<le> r \<Longrightarrow>
               Ord(p) \<Longrightarrow> Ord(q) \<Longrightarrow> Ord(r) \<Longrightarrow>
                p \<union> q \<le> r"
  using ord_simp_union by auto

lemma Un_leI3 : "o \<le> r \<Longrightarrow> p \<le> r \<Longrightarrow> q \<le> r \<Longrightarrow>
                Ord(o) \<Longrightarrow> Ord(p) \<Longrightarrow> Ord(q) \<Longrightarrow> Ord(r) \<Longrightarrow>
                o \<union> p \<union> q \<le> r"
  using ord_simp_union by auto

lemma diff_mono :
  assumes "m \<in> nat" "n\<in>nat" "p \<in> nat" "m < n" "p\<le>m"
  shows "m#-p < n#-p"
proof -
  from assms
  have "m#-p \<in> nat" "m#-p +\<^sub>\<omega>p = m"
    using add_diff_inverse2 by simp_all
  with assms
  show ?thesis
    using less_diff_conv[of n p "m #- p",THEN iffD2] by simp
qed

lemma pred_Un:
  "x \<in> nat \<Longrightarrow> y \<in> nat \<Longrightarrow> pred(succ(x) \<union> y) = x \<union> pred(y)"
  "x \<in> nat \<Longrightarrow> y \<in> nat \<Longrightarrow> pred(x \<union> succ(y)) = pred(x) \<union> y"
  using pred_Un_distrib pred_succ_eq by simp_all

lemma le_natI : "j \<le> n \<Longrightarrow> n \<in> nat \<Longrightarrow> j\<in>nat"
  by(drule ltD,rule in_n_in_nat,rule nat_succ_iff[THEN iffD2,of n],simp_all)

lemma le_natE : "n\<in>nat \<Longrightarrow> j < n \<Longrightarrow>  j\<in>n"
  by(rule ltE[of j n],simp+)

lemma leD : assumes "n\<in>nat" "j \<le> n"
  shows "j < n | j = n"
  using leE[OF \<open>j\<le>n\<close>,of "j<n | j = n"] by auto

lemma pred_nat_eq :
  assumes "n\<in>nat"
  shows "pred(n) = \<Union> n"
  using assms
proof(induct)
  case 0
  then show ?case by simp
next
  case (succ x)
  then show ?case using pred_succ_eq Ord_Union_succ_eq
    by simp
qed

subsection\<open>Some results in ordinal arithmetic\<close>
text\<open>The following results are auxiliary to the proof of
wellfoundedness of the relation \<^term>\<open>frecR\<close>\<close>

lemma max_cong :
  assumes "x \<le> y" "Ord(y)" "Ord(z)"
  shows "max(x,y) \<le> max(y,z)"
proof (cases "y \<le> z")
  case True
  then show ?thesis
    unfolding max_def using assms by simp
next
  case False
  then have "z \<le> y"  using assms not_le_iff_lt leI by simp
  then show ?thesis
    unfolding max_def using assms by simp
qed

lemma max_commutes :
  assumes "Ord(x)" "Ord(y)"
  shows "max(x,y) = max(y,x)"
  using assms Un_commute ord_simp_union(1) ord_simp_union(1)[symmetric] by auto

lemma max_cong2 :
  assumes "x \<le> y" "Ord(y)" "Ord(z)" "Ord(x)"
  shows "max(x,z) \<le> max(y,z)"
proof -
  from assms
  have " x \<union> z \<le> y \<union> z"
    using lt_Ord Ord_Un Un_mono[OF  le_imp_subset[OF \<open>x\<le>y\<close>]]  subset_imp_le by auto
  then show ?thesis
    using  ord_simp_union \<open>Ord(x)\<close> \<open>Ord(z)\<close> \<open>Ord(y)\<close> by simp
qed

lemma max_D1 :
  assumes "x = y" "w < z"  "Ord(x)"  "Ord(w)" "Ord(z)" "max(x,w) = max(y,z)"
  shows "z\<le>y"
proof -
  from assms
  have "w <  x \<union> w" using Un_upper2_lt[OF \<open>w<z\<close>] assms ord_simp_union by simp
  then
  have "w < x" using assms lt_Un_iff[of x w w] lt_not_refl by auto
  then
  have "y = y \<union> z" using assms max_commutes ord_simp_union assms leI by simp
  then
  show ?thesis using Un_leD2 assms by simp
qed

lemma max_D2 :
  assumes "w = y \<or> w = z" "x < y"  "Ord(x)"  "Ord(w)" "Ord(y)" "Ord(z)" "max(x,w) = max(y,z)"
  shows "x<w"
proof -
  from assms
  have "x < z \<union> y" using Un_upper2_lt[OF \<open>x<y\<close>] by simp
  then
  consider (a) "x < y" | (b) "x < w"
    using assms ord_simp_union by simp
  then show ?thesis proof (cases)
    case a
    consider (c) "w = y" | (d) "w = z"
      using assms by auto
    then show ?thesis proof (cases)
      case c
      with a show ?thesis by simp
    next
      case d
      with a
      show ?thesis
      proof (cases "y <w")
        case True
        then show ?thesis using lt_trans[OF \<open>x<y\<close>] by simp
      next
        case False
        then
        have "w \<le> y"
          using not_lt_iff_le[OF assms(5) assms(4)] by simp
        with \<open>w=z\<close>
        have "max(z,y) = y"  unfolding max_def using assms by simp
        with assms
        have "... = x \<union> w" using ord_simp_union max_commutes  by simp
        then show ?thesis using le_Un_iff assms by blast
      qed
    qed
  next
    case b
    then show ?thesis .
  qed
qed

lemma oadd_lt_mono2 :
  assumes  "Ord(n)" "Ord(\<alpha>)" "Ord(\<beta>)" "\<alpha> < \<beta>" "x < n" "y < n" "0 <n"
  shows "n ** \<alpha> + x < n **\<beta> + y"
proof -
  consider (0) "\<beta>=0" | (s) \<gamma> where  "Ord(\<gamma>)" "\<beta> = succ(\<gamma>)" | (l) "Limit(\<beta>)"
    using Ord_cases[OF \<open>Ord(\<beta>)\<close>,of ?thesis] by force
  then show ?thesis
  proof cases
    case 0
    then show ?thesis using \<open>\<alpha><\<beta>\<close> by auto
  next
    case s
    then
    have "\<alpha>\<le>\<gamma>" using \<open>\<alpha><\<beta>\<close> using leI by auto
    then
    have "n ** \<alpha> \<le> n ** \<gamma>" using omult_le_mono[OF _ \<open>\<alpha>\<le>\<gamma>\<close>] \<open>Ord(n)\<close> by simp
    then
    have "n ** \<alpha> + x < n ** \<gamma> + n" using oadd_lt_mono[OF _ \<open>x<n\<close>] by simp
    also
    have "... = n ** \<beta>" using \<open>\<beta>=succ(_)\<close> omult_succ \<open>Ord(\<beta>)\<close> \<open>Ord(n)\<close> by simp
    finally
    have "n ** \<alpha> + x < n ** \<beta>" by auto
    then
    show ?thesis using oadd_le_self \<open>Ord(\<beta>)\<close> lt_trans2 \<open>Ord(n)\<close> by auto
  next
    case l
    have "Ord(x)" using \<open>x<n\<close> lt_Ord by simp
    with l
    have "succ(\<alpha>) < \<beta>" using Limit_has_succ \<open>\<alpha><\<beta>\<close> by simp
    have "n ** \<alpha> + x < n ** \<alpha> + n"
      using oadd_lt_mono[OF le_refl[OF Ord_omult[OF _ \<open>Ord(\<alpha>)\<close>]] \<open>x<n\<close>] \<open>Ord(n)\<close> by simp
    also
    have "... = n ** succ(\<alpha>)" using omult_succ \<open>Ord(\<alpha>)\<close> \<open>Ord(n)\<close> by simp
    finally
    have "n ** \<alpha> + x < n ** succ(\<alpha>)" by simp
    with \<open>succ(\<alpha>) < \<beta>\<close>
    have "n ** \<alpha> + x < n ** \<beta>" using lt_trans omult_lt_mono \<open>Ord(n)\<close> \<open>0<n\<close>  by auto
    then show ?thesis using oadd_le_self \<open>Ord(\<beta>)\<close> lt_trans2 \<open>Ord(n)\<close> by auto
  qed
qed
end

author: isabelle-prover

repo: mirror-afp-devel


text:
(*  Title:      HOL/Hoare/HeapSyntax.thy
    Author:     Tobias Nipkow
    Copyright   2002 TUM
*)

theory HeapSyntax imports Hoare_Logic Heap begin

subsection "Field access and update"

syntax
  "_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
   ("_/'((_ \<rightarrow> _)')" [1000,0] 900)
  "_fassign"  :: "'a ref => id => 'v => 's com"
   ("(2_^._ :=/ _)" [70,1000,65] 61)
  "_faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
   ("_^._" [65,1000] 65)
translations
  "f(r \<rightarrow> v)" == "f(CONST addr r := v)"
  "p^.f := e" => "f := f(p \<rightarrow> e)"
  "p^.f" => "f(CONST addr p)"

declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp]

text "An example due to Suzuki:"

lemma "VARS v n
  {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
   distinct[w0,x0,y0,z0]}
  w^.v := (1::int); w^.n := x;
  x^.v := 2; x^.n := y;
  y^.v := 3; y^.n := z;
  z^.v := 4; x^.n := z
  {w^.n^.n^.v = 4}"
by vcg_simp

end

repo: jormungand


text:
theory prop_86
imports Main
        "$HIPSTER_HOME/IsaHipster"
begin
  datatype 'a list = Nil2 | Cons2 "'a" "'a list"
  datatype Nat = Z | S "Nat"
  fun equal2 :: "Nat => Nat => bool" where
  "equal2 (Z) (Z) = True"
  | "equal2 (Z) (S z) = False"
  | "equal2 (S x2) (Z) = False"
  | "equal2 (S x2) (S y2) = equal2 x2 y2"
  fun elem :: "Nat => Nat list => bool" where
  "elem x (Nil2) = False"
  | "elem x (Cons2 z xs) = (if equal2 x z then True else elem x xs)"
  fun lt :: "Nat => Nat => bool" where
  "lt x (Z) = False"
  | "lt (Z) (S z) = True"
  | "lt (S x2) (S z) = lt x2 z"
  fun ins :: "Nat => Nat list => Nat list" where
  "ins x (Nil2) = Cons2 x (Nil2)"
  | "ins x (Cons2 z xs) =
       (if lt x z then Cons2 x (Cons2 z xs) else Cons2 z (ins x xs))"

(*hipster lt equal2*)
lemma lemma_a [thy_expl]: "equal2 x2 y2 = equal2 y2 x2"
by (hipster_induct_schemes lt.simps equal2.simps)

lemma lemma_aa [thy_expl]: "lt x2 x2 = False"
by (hipster_induct_schemes lt.simps equal2.simps)

lemma lemma_ab [thy_expl]: "equal2 x2 x2 = True"
by (hipster_induct_schemes lt.simps equal2.simps)

lemma lemma_ac [thy_expl]: "lt x2 (S x2) = True"
by (hipster_induct_schemes lt.simps equal2.simps)

lemma lemma_ad [thy_expl]: "equal2 x2 (S x2) = False"
by (hipster_induct_schemes lt.simps equal2.simps)

lemma lemma_ae [thy_expl]: "lt (S x2) x2 = False"
by (hipster_induct_schemes lt.simps equal2.simps)

lemma lemma_af [thy_expl]: "lt x2 (S Z) = equal2 x2 Z"
by (hipster_induct_schemes lt.simps equal2.simps)

lemma lemma_t [thy_expl]: "lt x y \<Longrightarrow> equal2 x y = False"
by (hipster_induct_schemes lt.simps equal2.simps)

theorem x0 : "lt x y \<Longrightarrow> ((elem x (ins y xs)) \<longleftrightarrow> (elem x xs))"
by (hipster_induct_schemes elem.simps ins.simps lt.simps Nat.exhaust list.exhaust)

end

author: moajohansson

repo: IsaHipster


text:
theory PhiSem_Pointer_Mem
  imports Phi_System.PhiSem_Formalization_Tools "HOL-Library.Word"
begin

section \<open>Semantic\<close>

subsection \<open>Models\<close>

subsubsection \<open>Type\<close>

virtual_datatype \<phi>mem_ty = \<phi>empty_ty +
  T_pointer :: unit

context \<phi>mem_ty begin
abbreviation \<open>pointer \<equiv> T_pointer.mk ()\<close>
end

debt_axiomatization T_pointer :: \<open>unit type_entry\<close>
  where \<phi>mem_ty_ax: \<open>\<phi>mem_ty TY_CONS_OF T_pointer\<close>

interpretation \<phi>mem_ty TY_CONS_OF _ _ T_pointer using \<phi>mem_ty_ax .

subsubsection \<open>Value\<close>

paragraph \<open>Memory Address\<close>

consts addrspace_bits :: "nat" \<comment> \<open>The bit length of the memory address space, in unit of bits\<close>
specification (addrspace_bits) addrspace_bits_L0: "0 < addrspace_bits" by auto

typedecl addr_cap

instantiation addr_cap :: len begin
definition [simp]: "len_of_addr_cap (_::addr_cap itself) = addrspace_bits"
instance apply standard using addrspace_bits_L0 by simp
end

type_synonym size_t = \<open>addr_cap word\<close>
abbreviation to_size_t :: \<open>nat \<Rightarrow> size_t\<close> where \<open>to_size_t \<equiv> of_nat\<close>

declare [ [typedef_overloaded] ]

datatype segidx = Null | Segment nat \<comment> \<open>nonce\<close> (layout: TY)
  \<comment> \<open>The nonce itself is not an identifier, but (nonce \<times> layout) is.\<close>

hide_const (open) layout

datatype 'index memaddr = memaddr (segment: segidx) (index: 'index ) (infixl "|:" 60)

declare [ [typedef_overloaded = false] ]

declare memaddr.sel[iff]
hide_const (open) segment index

type_synonym logaddr = \<open>nat list memaddr\<close> (* the index of logaddr is non empty *)
type_synonym rawaddr = \<open>size_t memaddr\<close>

instantiation segidx :: zero begin
definition [simp]: "zero_segidx = Null"
instance ..
end

instantiation memaddr :: (zero) zero begin
definition "zero_memaddr = (0 |: 0)"
instance ..
end

lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
proof
  assume "finite (UNIV::int set)"
  moreover have "inj (\<lambda>i::int. 2 * i)"
    by (rule injI) simp
  ultimately have "surj (\<lambda>i::int. 2 * i)"
    by (rule finite_UNIV_inj_surj)
  thm finite_UNIV_inj_surj
  then obtain i :: int where "1 = 2 * i" by (rule surjE)
  then show False by (simp add: pos_zmult_eq_1_iff)
qed

lemma segidx_infinite[simp]:
  \<open>infinite (UNIV :: segidx set)\<close>
  using inj_on_finite[where A = \<open>UNIV::nat set\<close> and B = \<open>(UNIV :: segidx set)\<close>
        and f = \<open>\<lambda>n. Segment n undefined\<close>]
  by (meson infinite_UNIV_char_0 injI segidx.inject top_greatest)

lemma segidx_infinite_TY:
  \<open>infinite {a. segidx.layout a = TY}\<close>
  using inj_on_finite[where A = \<open>UNIV::nat set\<close> and B = \<open>{a. segidx.layout a = TY}\<close>
        and f = \<open>\<lambda>n. Segment n TY\<close>]
  using inj_def by fastforce

abbreviation shift_addr :: "'idx memaddr \<Rightarrow> ('idx::monoid_add) \<Rightarrow> 'idx memaddr" (infixl "||+" 60)
  where "shift_addr addr delta \<equiv> map_memaddr (\<lambda>x. x + delta) addr"

lemma mem_shift_shift[simp]: "a ||+ i ||+ j = a ||+ (i + j)" by (cases a) (simp add: add.assoc)

lemma memaddr_segment_shift[simp]:
  \<open>memaddr.segment (a ||+ i) = memaddr.segment a\<close>
  by (cases a, simp)

lemma memaddr_index_shift[simp]:
  \<open>memaddr.index (a ||+ i) = memaddr.index a + i\<close>
  by (cases a, simp)

lemma mem_shift_add_cancel[simp]:
  \<open>(a ||+ i) = (a ||+ j) \<longleftrightarrow> i = j\<close>
  for i :: \<open>'a::{monoid_add,cancel_semigroup_add}\<close>
  by (cases a, simp)

paragraph \<open>Model\<close>

virtual_datatype \<phi>mem_val :: "sep_magma" = \<phi>empty_val +
  V_pointer :: rawaddr

debt_axiomatization V_pointer :: \<open>rawaddr value_entry\<close>
  where \<phi>mem_val_ax: \<open>\<phi>mem_val VAL_CONS_OF V_pointer\<close>

interpretation \<phi>mem_val VAL_CONS_OF _ _ V_pointer using \<phi>mem_val_ax .

subsubsection \<open>Resource\<close>

type_synonym R_mem = \<open>(segidx \<rightharpoonup> VAL nosep)\<close>

resource_space \<phi>mem_res = \<phi>empty_res +
  R_mem :: R_mem

debt_axiomatization R_mem :: \<open>R_mem resource_entry\<close>
  where R_mem_ax: \<open>\<phi>mem_res R_mem\<close>

interpretation \<phi>mem_res R_mem using R_mem_ax .

subsection \<open>Semantics\<close>

datatype ('TY,'VAL) \<M> = \<M>
  (size_of:        \<open>'TY \<Rightarrow> nat\<close>)
  (valid_idx_step: \<open>'TY \<Rightarrow> nat \<Rightarrow> bool\<close>)
  (idx_step_type:  \<open>nat \<Rightarrow> 'TY \<Rightarrow> 'TY\<close>)
  (idx_step_value: \<open>nat \<Rightarrow> 'VAL \<Rightarrow> 'VAL\<close>)
  (idx_step_mod_value: \<open>nat \<Rightarrow> ('VAL \<Rightarrow> 'VAL) \<Rightarrow> 'VAL \<Rightarrow> 'VAL\<close>)
  (idx_step_offset: \<open>'TY \<Rightarrow> nat \<Rightarrow> nat\<close>)

hide_const (open) size_of valid_idx_step idx_step_type idx_step_value
  idx_step_mod_value idx_step_offset

locale mem_setting =
  std_ty  where CONS_OF   = TY_CONS_OF
            and TYPE'NAME = \<open>TYPE('TY_N)\<close>
            and TYPE'REP  = \<open>TYPE('TY)\<close>
+ std_val where CONS_OF   = VAL_CONS_OF
            and TYPE'TY   = \<open>TYPE('TY)\<close>
            and TYPE'NAME = \<open>TYPE('VAL_N)\<close>
            and TYPE'REP  = \<open>TYPE('VAL::nonsepable_semigroup)\<close>
+ std_res where TYPE'VAL  = \<open>TYPE('VAL)\<close>
            and TYPE'TY   = \<open>TYPE('TY)\<close>
            and TYPE'NAME = \<open>TYPE('RES_N)\<close>
            and TYPE'REP  = \<open>TYPE('RES::comm_monoid_mult)\<close>
  for TY_CONS_OF and VAL_CONS_OF
+ fixes TYPES :: \<open>(('TY_N \<Rightarrow> 'TY) \<times> ('VAL_N => 'VAL) \<times> ('RES_N => 'RES)) itself\<close>

fixes \<M> :: \<open>('TY,'VAL) \<M>\<close>
  assumes memobj_size_arr    : \<open>\<M>.size_of \<M> (\<tau>Array N T) = N * \<M>.size_of \<M> T\<close>
    and   memobj_size_step   : \<open>\<M>.valid_idx_step \<M> T i \<Longrightarrow> \<M>.size_of \<M> (idx_step_type i T) \<le> \<M>.size_of \<M> T\<close>
    and   idx_step_type_measure: \<open>\<M>.valid_idx_step \<M> T i \<Longrightarrow> type_measure (\<M>.idx_step_type \<M> i T) < type_measure T\<close>
    and   idx_step_type_tup  : \<open>i < length tys \<Longrightarrow> \<M>.idx_step_type \<M> i (\<tau>Tuple tys) = tys!i \<close>
    and   idx_step_type_arr  : \<open>i \<le> N \<Longrightarrow> \<M>.idx_step_type \<M> i (\<tau>Array N T) = T\<close>
    and   valid_idx_step_tup : \<open>\<M>.valid_idx_step \<M> (\<tau>Tuple tys) i \<longleftrightarrow> i < length tys\<close>
    and   valid_idx_step_arr : \<open>\<M>.valid_idx_step \<M> (\<tau>Array N T) i \<longleftrightarrow> i < N\<close>
    and   idx_step_value_welltyp: \<open>\<M>.valid_idx_step \<M> T i \<Longrightarrow> v \<in> Well_Type T \<Longrightarrow> \<M>.idx_step_value \<M> i v \<in> Well_Type (\<M>.idx_step_type \<M> i T)\<close>
    and   idx_step_value_tup : \<open>\<M>.idx_step_value \<M> i (V_tup.mk vs)   = vs!i\<close>
    and   idx_step_value_arr : \<open>\<M>.idx_step_value \<M> i (V_array.mk (T,vs)) = vs!i\<close>
    and   idx_step_mod_value : \<open>\<M>.valid_idx_step \<M> T i
                            \<Longrightarrow> \<M>.valid_idx_step \<M> T j
                            \<Longrightarrow> v \<in> Well_Type T
                            \<Longrightarrow> \<M>.idx_step_value \<M> i (\<M>.idx_step_mod_value \<M> j f v) =
                                  (if i = j then f (\<M>.idx_step_value \<M> j v) else \<M>.idx_step_value \<M> i v) \<close>
    and   idx_step_mod_value_welltyp: \<open>\<M>.valid_idx_step \<M> T i
                                   \<Longrightarrow> v \<in> Well_Type T
                                   \<Longrightarrow> f (\<M>.idx_step_value \<M> i v) \<in> Well_Type (\<M>.idx_step_type \<M> i T)
                                   \<Longrightarrow> \<M>.idx_step_mod_value \<M> i f v \<in> Well_Type T\<close>
    and   idx_step_mod_value_tup : \<open>\<M>.idx_step_mod_value \<M> i f (V_tup.mk vs) = V_tup.mk (vs[i := f (vs!i)])\<close>
    and   idx_step_mod_value_arr : \<open>\<M>.idx_step_mod_value \<M> i f (V_array.mk (T,vs)) = V_array.mk (T,vs[i := f (vs!i)])\<close>
    and   idx_step_offset_arr: \<open>\<M>.idx_step_offset \<M> (\<tau>Array N T) i = i * \<M>.size_of \<M> T\<close>
    and   idx_step_offset_size:\<open>\<M>.valid_idx_step \<M> T i \<Longrightarrow> \<M>.idx_step_offset \<M> T i + \<M>.size_of \<M> (\<M>.idx_step_type \<M> i T) \<le> \<M>.size_of \<M> T\<close>
    and   idx_step_offset_disj:\<open>\<M>.valid_idx_step \<M> T i \<Longrightarrow> \<M>.valid_idx_step \<M> T j \<Longrightarrow>
                                \<M>.idx_step_offset \<M> T i \<le> \<M>.idx_step_offset \<M> T j \<Longrightarrow>
                                \<M>.idx_step_offset \<M> T j < \<M>.idx_step_offset \<M> T i + \<M>.size_of \<M> (\<M>.idx_step_type \<M> i T) \<Longrightarrow>
                                i = j\<close>

end

repo: phi-system


text:
(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Trace_Schematic_Insts_Test
imports
  Lib.Trace_Schematic_Insts
begin

text \<open>
  Trace the schematic variables and types that a method instantiates.
  This only works for the variables already in the proof goal; new
  variables introduced by the traced method are not tracked.
\<close>

experiment begin
section \<open>Examples\<close>

text \<open>Schematic variables\<close>
lemma "\<lbrakk> \<forall>x. P x \<rbrakk> \<Longrightarrow> P x"
  apply (drule spec) \<comment> \<open>introduces schematic var "?x"\<close>
  apply (trace_schematic_insts \<open>assumption\<close>)
  done

definition foo :: "'a \<Rightarrow> bool"
  where "foo x = True"

lemma fooI1:
  "foo 0 \<Longrightarrow> foo x"
  by (simp add: foo_def)

lemma fooI2:
  "foo x \<Longrightarrow> foo 0"
  by (simp add: foo_def)

lemma fooI2':
  "foo x \<Longrightarrow> foo (0 :: nat)"
  by (erule fooI2)

text \<open>Schematic type variables\<close>
lemma "foo x \<Longrightarrow> foo y"
  apply (rule fooI1) \<comment> \<open>introduces schematic type "0 :: ?'a"\<close>
  apply (trace_schematic_insts \<open>erule fooI2'\<close>)
  done

text \<open>When backtracking, every recursive invocation is traced\<close>
lemma "\<lbrakk> \<forall>x. Q x \<longrightarrow> R x; \<forall>x. P x \<longrightarrow> Q x; P x; P y \<longrightarrow> R x \<rbrakk> \<Longrightarrow> R x"
  apply (drule spec)
  apply (drule spec)
  text \<open>For more clarity, methods can be named\<close>
  apply (trace_schematic_insts impE1 \<open>erule impE\<close>,
         trace_schematic_insts impE2 \<open>erule impE\<close>,
         (trace_schematic_insts "try assumption" \<open>assumption\<close>)+; fail)
  done

text \<open>Interactive example\<close>
ML \<open>
  fun trace_resolve_tac ctxt =
      Trace_Schematic_Insts.trace_schematic_insts_tac ctxt
        (Trace_Schematic_Insts.default_rule_report ctxt "demo title")
        (fn t => resolve_tac ctxt [t])
\<close>
lemma
  assumes Pf: "\<And>f (x :: nat). Q f \<Longrightarrow> P x \<Longrightarrow> P (f x)"
  assumes Q: "Q ((*) 2)"
  assumes P: "P a"
  shows "\<exists>x. P (x + a + a)"
  apply (tactic \<open>trace_resolve_tac @{context} @{thm exI} 1\<close>)
  apply (trace_schematic_insts \<open>subst add_0\<close>)

  \<comment>\<open>
    This picks *some* instantiation of `f` in @{thm Pf}. The first one is
    @{term "\<lambda>a. a"}, which isn't what we want.
  \<close>
  apply (tactic \<open>trace_resolve_tac @{context} @{thm Pf} 1\<close>)
   \<comment>\<open>
     This picks the *next* instantiation of `f`, in this case @{term "\<lambda>a. a + a"}
     Notice that the reporting callback gets called with the new instantiations!
   \<close>
   back

   apply (tactic \<open>
     Trace_Schematic_Insts.trace_schematic_insts_tac
       @{context}
       (Trace_Schematic_Insts.default_rule_report @{context} "demo title")
       (fn t => EqSubst.eqsubst_tac @{context} [0] [t])
       @{thm mult_2[symmetric]} 1
   \<close>)
   apply (tactic \<open>trace_resolve_tac @{context} @{thm Q} 1\<close>)
  apply (tactic \<open>trace_resolve_tac @{context} @{thm P} 1\<close>)
  done

section \<open>Tests\<close>

ML \<open>
fun trace_schematic_assert ctxt test_name tac expected_vars expected_tvars =
  let
    fun skip_dummy_state tac = fn st =>
        case Thm.prop_of st of
            Const (@{const_name Pure.prop}, _) $
              (Const (@{const_name Pure.term}, _) $ Const (@{const_name Pure.dummy_pattern}, _)) =>
              Seq.succeed st
          | _ => tac st

    fun check insts =
      if expected_vars = #terms insts andalso expected_tvars = #typs insts then () else
        error ("Trace_Schematic_Insts failed test: " ^ test_name)

  in Method.NO_CONTEXT_TACTIC ctxt
        (Trace_Schematic_Insts.trace_schematic_insts (SIMPLE_METHOD tac) check [])
     |> skip_dummy_state
  end
\<close>

text \<open>Schematic variables\<close>
lemma "\<lbrakk> \<forall>x. P x \<rbrakk> \<Longrightarrow> P x"
  apply (drule spec)
  apply (tactic \<open>let
      val alpha = TFree ("'a", @{sort type})
      val expected_vars = [(Var (("x", 0), alpha), Free ("x", alpha))]
      val expected_tvars = []
      in trace_schematic_assert @{context}
            "basic Var test" (assume_tac @{context} 1)
            expected_vars expected_tvars
      end\<close>)
  done

text \<open>Schematic type variables\<close>
lemma "foo x \<Longrightarrow> foo y"
  apply (rule fooI1)
  apply (tactic \<open>let
      val expected_vars = []
      val expected_tvars = [(TVar (("'a", 0), @{sort zero}), @{typ nat})]
      in trace_schematic_assert
            @{context}
            "basic TVar test"
            (eresolve_tac @{context} @{thms fooI2'} 1)
            expected_vars expected_tvars
      end\<close>)
  done

ML \<open>
fun trace_schematic_resolve_tac_assert ctxt test_name thm expected_rule_insts expected_proof_insts =
  let
    fun check rule_insts proof_insts =
        if expected_rule_insts = rule_insts andalso expected_proof_insts = proof_insts
        then ()
        else
          let
            val _ = tracing (@{make_string} (rule_insts, proof_insts))
          in error ("Trace_Schematic_Insts failed test: " ^ test_name) end
    fun tactic thm = resolve_tac ctxt [thm]
  in HEADGOAL (Trace_Schematic_Insts.trace_schematic_insts_tac ctxt check tactic thm)
  end
\<close>

text \<open>Simultaneous rule and goal instantiations\<close>
lemma "\<exists>a. foo (a :: nat)"
  apply (rule exI)
  apply (tactic \<open>
    let
      val a' = TVar (("'a", 0), @{sort type})
      val b' = TVar (("'b", 0), @{sort zero})
      val a'' = TVar (("'a", 2), @{sort type})
      val expected_rule_vars = [
        (Var (("x", 0), a'), Var(("x", 2), a''))
      ]
      val expected_rule_tvars = [
        (a', a''),
        (b', @{typ nat})
      ]
      val expected_goal_vars = [
        (Var (("a", 0), @{typ nat}), @{term "0 :: nat"})
      ]
    in
      trace_schematic_resolve_tac_assert
        @{context}
        "basic rule tracing"
        @{thm fooI2}
        {bounds = [], terms = expected_rule_vars, typs = expected_rule_tvars}
        {bounds = [], terms = expected_goal_vars, typs = []}
    end
  \<close>)
  by (simp add: foo_def)

text \<open>Rule instantiations with bound variables\<close>
lemma "\<And>X. X \<and> Y \<Longrightarrow> Y \<and> X"
  apply (tactic \<open>
    let
      val expected_rule_bounds = [("X", @{typ bool})]
      val expected_rule_vars = [
        (Var (("P", 0), @{typ bool}), @{term "\<lambda>X :: bool. Y :: bool"}),
        (Var (("Q", 0), @{typ bool}), @{term "\<lambda>X :: bool. X :: bool"})
      ]
    in
      trace_schematic_resolve_tac_assert
        @{context}
        "rule tracing with bound variables"
        @{thm conjI}
        {bounds = expected_rule_bounds, terms = expected_rule_vars, typs = []}
        {bounds = [], terms = [], typs = []}
    end
  \<close>)
  by simp+

text \<open>Rule instantiations with function terms\<close>
lemma "\<exists>f. \<forall>x. f x = x"
  apply (intro exI allI)
  apply (rule fun_cong)
  apply (tactic \<open>
    let
      val a' = TVar (("'a", 0), @{sort type})
      \<comment>\<open>
        New lambda abstraction gets an anonymous variable name. Usually rendered as
        @{term "\<lambda>x a. a"}.
      \<close>
      val lambda = Abs ("x", @{typ 'a}, Abs ("", @{typ 'a}, Bound 0))

      val expected_rule_bounds = [("x", @{typ 'a})]
      val expected_rule_vars = [
        (Var (("t", 0), a'), lambda)
      ]
      val expected_rule_typs = [
        (a', @{typ "'a \<Rightarrow> 'a"})
      ]
      val expected_goal_vars = [
        (Var (("f", 2), @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}), lambda)
      ]
    in
      trace_schematic_resolve_tac_assert
        @{context}
        "rule tracing with function term instantiations"
        @{thm refl}
        {bounds = expected_rule_bounds, terms = expected_rule_vars, typs = expected_rule_typs}
        {bounds = [], terms = expected_goal_vars, typs = []}
    end
  \<close>)
  done

end

end

author: NICTA


text:
(* Author: Bernhard Stöckl *)

theory CostFunctions
  imports Complex_Main JoinTree Selectivities
begin

section \<open>Cost Functions\<close>

subsection \<open>General Cost Functions\<close>

fun c_out :: "'a card \<Rightarrow> 'a selectivity \<Rightarrow> 'a joinTree \<Rightarrow> real" where
  "c_out _ _ (Relation _) = 0"
| "c_out cf f (Join l r) = card cf f (Join l r) + c_out cf f l + c_out cf f r"

fun c_nlj :: "'a card \<Rightarrow> 'a selectivity \<Rightarrow> 'a joinTree \<Rightarrow> real" where
  "c_nlj _ _ (Relation _) = 0"
| "c_nlj cf f (Join l r) = card cf f l * card cf f r + c_nlj cf f l + c_nlj cf f r"

fun c_hj :: "'a card \<Rightarrow> 'a selectivity \<Rightarrow> 'a joinTree \<Rightarrow> real" where
  "c_hj _ _ (Relation _) = 0"
| "c_hj cf f (Join l r) = 1.2 * card cf f l + c_hj cf f l + c_hj cf f r"

fun c_smj :: "'a card \<Rightarrow> 'a selectivity \<Rightarrow> 'a joinTree \<Rightarrow> real" where
  "c_smj _ _ (Relation _) = 0"
| "c_smj cf f (Join l r) = card cf f l * log 2 (card cf f l) + card cf f r * log 2 (card cf f r)
    + c_smj cf f l + c_smj cf f r"

subsection \<open>Cost functions that are considered by IKKBZ.\<close>

fun c_IKKBZ :: "('a \<Rightarrow> real \<Rightarrow> real) \<Rightarrow> 'a card \<Rightarrow> 'a selectivity \<Rightarrow> 'a joinTree \<Rightarrow> real" where
  "c_IKKBZ _ _ _ (Relation _) = 0"
| "c_IKKBZ h cf f (Join l (Relation rel)) = card cf f l * (h rel (cf rel)) + c_IKKBZ h cf f l"
| "c_IKKBZ _ _ _ (Join l r) = undefined"

text \<open>
  A list of relations defines a unique left-deep tree. This functions computes a cost function
  given by such a list representation of a tree according to the formula
  @{text "\<Sum>\<^sub>i\<^sub>=\<^sub>2\<^sup>n n\<^sub>{\<^sub>1\<^sub>,\<^sub>2\<^sub>,\<^sub>\<dots>\<^sub>i\<^sub>-\<^sub>1\<^sub>} h\<^sub>i(n\<^sub>i)"}
  where @{text "n\<^sub>{\<^sub>1\<^sub>,\<^sub>2\<^sub>,\<^sub>\<dots>\<^sub>i\<^sub>-\<^sub>1\<^sub>}"} = @{term "card subtree"} = @{term "ldeep_n f cf"} (list subtree)
  The input list is expected to be in reversed order for easier recursive processing
  i.e. the first element in xs is the rightmost element of the left-deep tree
\<close>

fun c_list' :: "'a selectivity \<Rightarrow> 'a card \<Rightarrow> ('a list \<Rightarrow> 'a \<Rightarrow> real) \<Rightarrow> 'a list \<Rightarrow> real" where
  "c_list' _ _ _ [] = 0"
| "c_list' _ _ _ [x] = 0"
| "c_list' f cf h (x#xs) = ldeep_n f cf xs * h xs x + c_list' f cf h xs"

text \<open>
  Equivalent definition which allows splitting the list at any point.
\<close>
fun c_list :: "('a \<Rightarrow> real) \<Rightarrow> 'a card \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> real" where
  "c_list _ _ _ _ [] = 0"
| "c_list _ _ h r [x] = (if x=r then 0 else h x)"
| "c_list sf cf h r (x#xs) = c_list sf cf h r xs + ldeep_T sf cf xs * c_list sf cf h r [x]"

text \<open>
  Maps the h function to a static version that doesn't require an input list.
\<close>
fun create_h_list :: "('a list \<Rightarrow> 'a \<Rightarrow> real) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> real" where
  "create_h_list _ [] = (\<lambda>_. 1)"
| "create_h_list h (x#xs) = (\<lambda>a. if a=x then h xs x else create_h_list h xs a)"

subsection \<open>Properties of Cost Functions\<close>

definition symmetric :: "('a joinTree \<Rightarrow> real) \<Rightarrow> bool" where
  "symmetric f = (\<forall>x y. f (Join x y) = f (Join y x))"

definition symmetric' :: "('a card \<Rightarrow> 'a selectivity \<Rightarrow> 'a joinTree \<Rightarrow> real) \<Rightarrow> bool" where
  "symmetric' f = (\<forall>x y cf sf. sel_symm sf \<longrightarrow> (f cf sf (Join x y) = f cf sf (Join y x)))"

text \<open>
  Uses reversed lists since the last joined relation should only appear once. Therefore, it should
  be the head of the list and by inductive reasoning the list should be reversed.
  Furthermore, the root must be the first relation in the sequence (last in the reverse) or it must
  not be contained at all.
\<close>
definition asi' :: "'a \<Rightarrow> ('a list \<Rightarrow> real) \<Rightarrow> bool" where
  "asi' r c = (\<exists>rank :: ('a list \<Rightarrow> real).
    (\<forall>A U V B. distinct (A@U@V@B) \<and> U \<noteq> [] \<and> V \<noteq> []
      \<and> (r \<notin> set (A@U@V@B) \<or> (take 1 (A@U@V@B) = [r] \<and> take 1 (A@V@U@B) = [r]))
      \<longrightarrow> (c (rev (A@U@V@B)) \<le> c (rev (A@V@U@B)) \<longleftrightarrow> rank (rev U) \<le> rank (rev V))))"

definition asi :: "('a list \<Rightarrow> real) \<Rightarrow> 'a \<Rightarrow> ('a list \<Rightarrow> real) \<Rightarrow> bool" where
  "asi rank r c = (\<forall>A U V B. distinct (A@U@V@B) \<and> U \<noteq> [] \<and> V \<noteq> []
      \<and> (r \<notin> set (A@U@V@B) \<or> (take 1 (A@U@V@B) = [r] \<and> take 1 (A@V@U@B) = [r]))
      \<longrightarrow> (c (rev (A@U@V@B)) \<le> c (rev (A@V@U@B)) \<longleftrightarrow> rank (rev U) \<le> rank (rev V)))"

(* alternative asi definition with slightly changed preconditions related for r *)
definition asi'' :: "('a list \<Rightarrow> real) \<Rightarrow> 'a \<Rightarrow> ('a list \<Rightarrow> real) \<Rightarrow> bool" where
  "asi'' rank r c = ((\<forall>A U V B. distinct (A@U@V@B) \<and> U \<noteq> [] \<and> V \<noteq> [] \<and> U \<noteq> [r] \<and> V \<noteq> [r]
    \<longrightarrow> (c (rev (A@U@V@B)) \<le> c (rev (A@V@U@B)) \<longleftrightarrow> rank (rev U) \<le> rank (rev V))))"

subsection \<open>Proofs\<close>
(** proofs that certain cost functions satisfy properties **)

lemma c_out_symm: "sel_symm f \<Longrightarrow> symmetric (c_out cf f)"
  by (simp add: symmetric_def list_sel_symm)

lemma c_nlj_symm: "symmetric (c_nlj cf f)"
  by (simp add: symmetric_def)

lemma c_smj_symm: "symmetric (c_smj cf f)"
  by (simp add: symmetric_def)

subsubsection \<open>Equivalence Proofs\<close>

theorem c_nlj_IKKBZ: "left_deep t \<Longrightarrow> c_nlj cf f t = c_IKKBZ (\<lambda>_. id) cf f t"
proof(induction t)
  case (Join l r)
  then show ?case by(cases r) auto
qed(simp)

theorem c_hj_IKKBZ: "left_deep t \<Longrightarrow> c_hj cf f t = c_IKKBZ (\<lambda>_ _. 1.2) cf f t"
proof(induction t)
  case ind: (Join l r)
  then show ?case by(cases r) auto
qed(simp)

lemma change_fun_order: "y\<noteq>rel
  \<Longrightarrow> (\<lambda>a b. if a=rel then g a b else (\<lambda>c d. if c=y then h c d else f c d) a b)
    = (\<lambda>a b. if a=y then h a b else (\<lambda>c d. if c=rel then g c d else f c d) a b)"
  by fastforce

lemma c_IKKBZ_fun_notelem:
  assumes "left_deep t"
      and "distinct_relations t"
      and "y \<notin> relations t"
      and "f' = (\<lambda>a b. if a=y then z b else f a b)"
    shows "c_IKKBZ f' cf sf t = c_IKKBZ f cf sf t"
using assms proof(induction t arbitrary: f' f z rule: left_deep.induct)
  case (2 l rel)
  then have 0: "rel \<noteq> y" by auto
  have "c_IKKBZ f' cf sf (Join l (Relation rel))
      = card cf sf l * (f' rel (cf rel)) + c_IKKBZ f' cf sf l" by simp
  also have "\<dots> = card cf sf l * (f' rel (cf rel)) + c_IKKBZ f cf sf l"
    using ldeep_trans distinct_trans_l 2 by fastforce
  also have "\<dots> = card cf sf l * (f rel (cf rel)) + c_IKKBZ f cf sf l"
    using "2.prems"(3,4) by fastforce
  also have "\<dots> = c_IKKBZ f cf sf (Join l (Relation rel))" using "2.prems"(1) by simp
  finally show ?case .
qed (auto)

lemma distinct_c_IKKBZ_ldeep_s_prepend:
  "\<lbrakk>distinct(ys@revorder t); left_deep t\<rbrakk>
    \<Longrightarrow> c_IKKBZ (\<lambda>a b. ldeep_s f (ys@revorder t) a * b) cf f t
      = c_IKKBZ (\<lambda>a b. ldeep_s f (revorder t) a * b) cf f t"
proof(induction t arbitrary: ys rule: left_deep.induct)
  case (2 l rr)
  let ?ylr = "ys @ revorder (Join l (Relation rr))"
  let ?lr = "revorder (Join l (Relation rr))"
  let ?h = "(\<lambda>a. (*) (ldeep_s f ?ylr a))"
  let ?h' = "(\<lambda>a. (*) (ldeep_s f ?lr a))"
  let ?h'' = "(\<lambda>a. (*) (ldeep_s f (revorder l) a))"
  have "?lr = [rr]@revorder l" by simp
  have 0: "distinct ?lr" using "2.prems"(1) by simp
  have "c_IKKBZ ?h cf f (Join l (Relation rr))
      = card cf f l * ((ldeep_s f ?ylr rr) * (cf rr)) + c_IKKBZ ?h cf f l"
    by simp
  also have "\<dots> = card cf f l * ((list_sel_aux' f (revorder l) rr) * (cf rr))
              + c_IKKBZ ?h cf f l"
    using "2.prems"(1) by (fastforce simp: distinct_ldeep_s_eq_aux)
  also have "\<dots> = card cf f l * (?h' rr (cf rr)) + c_IKKBZ ?h cf f l" by simp
  also have "\<dots> = card cf f l * (?h' rr (cf rr)) + c_IKKBZ ?h'' cf f l"
    using "2.IH"[of "ys@[rr]"] "2.prems" by simp
  also have "\<dots> = card cf f l * (?h' rr (cf rr)) + c_IKKBZ ?h' cf f l"
    using "2.IH"[of "[rr]"] "2.prems"(2) 0 by simp
  finally show ?case by simp
qed (auto)

lemma distinct_c_IKKBZ_ldeep_s_subtree:
  assumes "distinct_relations (Join l (Relation rel))"
      and "left_deep (Join l (Relation rel))"
    shows "c_IKKBZ (\<lambda>a b. ldeep_s f (revorder (Join l (Relation rel))) a * b) cf f l
          = c_IKKBZ (\<lambda>a b. ldeep_s f (revorder l) a * b) cf f l"
proof -
  have "distinct (revorder (Join l (Relation rel)))"
    using assms(1) by (simp add: distinct_rels_alt inorder_eq_mset)
  then have "distinct ([rel]@revorder l)" by simp
  then show ?thesis using distinct_c_IKKBZ_ldeep_s_prepend[of "[rel]" l] assms(2) by simp
qed

theorem c_out_IKKBZ:
  "\<lbrakk>distinct_relations t; reasonable_cards cf f t; left_deep t\<rbrakk>
    \<Longrightarrow> c_IKKBZ (\<lambda>a b. ldeep_s f (revorder t) a * b) cf f t = c_out cf f t"
proof(induction t)
  case ind: (Join l r)
  then show ?case
  proof(cases r)
    case (Relation rel)
    let ?s = "(\<lambda>a b. ldeep_s f (revorder (Join l r)) a * b)"
    let ?s' = "(\<lambda>a b. ldeep_s f (revorder l) a * b)"
    have "c_IKKBZ ?s cf f l = c_IKKBZ ?s' cf f l"
      using ind.prems distinct_c_IKKBZ_ldeep_s_subtree Relation by fast
    then have 0: "c_IKKBZ ?s cf f l = c_out cf f l"
      using ind ldeep_trans distinct_trans_l reasonable_trans by metis
    have "c_IKKBZ ?s cf f (Join l r) = card cf f l * (?s rel (cf rel)) + c_IKKBZ ?s cf f l"
      using Relation by simp
    also have "\<dots> = card cf f l * ((list_sel_aux' f (revorder l) rel) * (cf rel))
                + c_IKKBZ ?s cf f l"
      using Relation by simp
    also have "\<dots> = card cf f l * ((list_sel f (revorder l) [rel]) * (cf rel))
                + c_IKKBZ ?s cf f l"
      by (simp add: list_sel_sing_aux')
    also have "\<dots> = card cf f l * ((list_sel f (inorder l) [rel]) * (cf rel))
                + c_IKKBZ ?s cf f l"
      using mset_x_eq_list_sel_eq[of "revorder l"] by (simp add: revorder_eq_rev_inorder)
    also have "\<dots> = card cf f (Join l r) + c_IKKBZ ?s' cf f l"
      using distinct_c_IKKBZ_ldeep_s_subtree ind.prems Relation by fastforce
    also have "\<dots> = card cf f (Join l r) + c_out cf f l"
      using ind reasonable_trans distinct_trans_l ldeep_trans by metis
    finally show ?thesis using Relation by simp
  next
    case (Join lr rr)
    then show ?thesis using ind by simp
  qed
qed(simp)

theorem c_out_eq_c_list':
  "\<lbrakk>distinct_relations t; reasonable_cards cf f t; left_deep t\<rbrakk>
    \<Longrightarrow> c_list' f cf (\<lambda>xs x. (list_sel_aux' f xs x) * cf x) (revorder t) = c_out cf f t"
proof(induction t rule: left_deep.induct)
  case (2 l rr)
  let ?h = "\<lambda>xs x. list_sel_aux' f xs x * cf x"
  let ?ll = "revorder l"
  have 1: "distinct_relations l" using "2.prems" distinct_trans_l by simp
  have 2: "reasonable_cards cf f l" using "2.prems" reasonable_trans by blast
  have 3: "left_deep l" using "2.prems" by simp
  have "revorder (Join l (Relation rr)) = rr # ?ll" by simp
  then have "c_list' f cf ?h (revorder (Join l (Relation rr)))
        = ldeep_n f cf ?ll * ?h ?ll rr + c_list' f cf ?h ?ll"
    using joinTree_cases_ldeep[OF 3] by auto
  also have "\<dots> = card cf f l * ?h ?ll rr + c_list' f cf ?h ?ll"
    using ldeep_n_eq_card_subtree "2.prems" by auto
  also have "\<dots> = card cf f l * (list_sel_aux' f ?ll rr) * cf rr + c_list' f cf ?h ?ll"
    using mset_x_eq_list_sel_aux'_eq mset_rev by fastforce
  also have "\<dots> = card cf f (Join l (Relation rr)) + c_list' f cf ?h ?ll"
    unfolding card_join_alt by (simp add: list_sel_sing_aux')
  also have "\<dots> = card cf f (Join l (Relation rr)) + c_out cf f l" using "2.IH" 1 2 3 by simp
  finally show ?case by simp
qed (auto)

lemma rev_first_last_elem: "(rev (x#x'#xs')) = (r#rs) \<Longrightarrow> x \<in># mset rs"
  using  in_multiset_in_set last_in_set last_snoc rev_singleton_conv
  by (metis List.last.simps List.list.discI List.list.inject List.rev.simps(2))

lemma distinct_first_uneq_last: "distinct (x#x'#xs') \<Longrightarrow> rev (x#x'#xs') = r#rs \<Longrightarrow> r \<noteq> x"
  using rev_first_last_elem mset_rev set_mset_mset
  by (metis List.distinct.simps(2) count_eq_zero_iff distinct_count_atmost_1)

lemma distinct_create_eq_app:
  "\<lbrakk>distinct (ys@xs); x \<in># mset xs\<rbrakk> \<Longrightarrow> create_h_list h xs x = create_h_list h (ys@xs) x"
  by(induction ys) auto

lemma c_list_single_h_list_not_elem_prepend:
  "x \<notin> set ys
  \<Longrightarrow> c_list f cf (create_h_list h (ys@x#xs)) r [x] = c_list f cf (create_h_list h (x#xs)) r [x]"
  by(induction ys) auto

lemma c_list_single_f_list_not_elem_prepend:
  "x \<notin> set ys
  \<Longrightarrow> c_list (ldeep_s f (ys@x#xs)) cf h r [x] = c_list (ldeep_s f (x#xs)) cf h r [x]"
  by(induction ys) auto

lemma c_list_prepend_h_disjunct:
  assumes "distinct (ys@xs)"
  shows "c_list f cf (create_h_list h (ys@xs)) r xs = c_list f cf (create_h_list h xs) r xs"
using assms proof(induction xs arbitrary: ys)
  case (Cons x xs)
  then have 0: "distinct (ys @ [x] @ xs)" by simp
  then have 1: "distinct ([x] @ xs)" by simp
  let ?h = "create_h_list h (ys @ x # xs)"
  let ?h' = "create_h_list h xs"
  let ?h'' = "create_h_list h (x#xs)"
  have 2: "x \<notin> set ys" using Cons.prems by simp
  show ?case
  proof(cases "xs=[]")
    case True
    then show ?thesis
      using Cons distinct_create_eq_app in_multiset_in_set
      by (metis CostFunctions.c_list.simps(2) List.list.set_intros(1))
  next
    case False
    then obtain x' xs' where x'_def[simp]: "xs = x'#xs'" using List.list.exhaust_sel by auto
    then have "c_list f cf ?h r (x # xs)
        = c_list f cf ?h r xs + ldeep_T f cf xs * c_list f cf ?h r [x]" by simp
    also have "\<dots> = c_list f cf ?h' r xs + ldeep_T f cf xs * c_list f cf ?h r [x]"
      using Cons.IH[of "ys@[x]"] 0 by simp
    also have "\<dots> = c_list f cf ?h'' r xs + ldeep_T f cf xs * c_list f cf ?h r [x]"
      using Cons.IH[of "[x]"] 1 by simp
    also have "\<dots> = c_list f cf ?h'' r xs + ldeep_T f cf xs * c_list f cf ?h'' r [x]"
      using c_list_single_h_list_not_elem_prepend 2 by metis
    finally show ?thesis by simp
  qed
qed(simp)

lemma c_list_prepend_f_disjunct:
  assumes "distinct (ys@xs)"
  shows "c_list (ldeep_s f (ys@xs)) cf h r xs = c_list (ldeep_s f xs) cf h r xs"
using assms proof(induction xs arbitrary: ys)
  case (Cons x xs)
  then have 0: "distinct(ys @ [x] @ xs)" by simp
  then have 1: "distinct ([x] @ xs)" by simp
  let ?f = "ldeep_s f (ys @ x # xs)"
  let ?f' = "ldeep_s f xs"
  let ?f'' = "ldeep_s f (x#xs)"
  have 2: "x \<notin> set ys" using Cons.prems by simp
  show ?case
  proof(cases "xs=[]")
    case False
    then obtain x' xs' where x'_def[simp]: "xs = x'#xs'" using List.list.exhaust_sel by auto
    have "ldeep_T ?f cf xs = ldeep_T ?f' cf xs"
      using distinct_ldeep_T_prepend[of "ys@[x]" "xs" f cf] Cons.prems by simp
    then have 3: "ldeep_T ?f cf xs = ldeep_T ?f'' cf xs"
      using distinct_ldeep_T_prepend[of "[x]" "xs" f cf] Cons.prems 1 by simp
    have "c_list ?f cf h r (x # xs)
          = c_list ?f cf h r xs + ldeep_T ?f cf xs * c_list ?f cf h r [x]"
      by simp
    also have "\<dots> = c_list ?f' cf h r xs + ldeep_T ?f'' cf xs * c_list ?f cf h r [x]"
      using Cons.IH[of "ys@[x]"] 0 3 by simp
    also have "\<dots> = c_list ?f'' cf h r xs + ldeep_T ?f'' cf xs * c_list ?f cf h r [x]"
      using Cons.IH[of "[x]"] 1 by simp
    also have "\<dots> = c_list ?f'' cf h r xs + ldeep_T ?f'' cf xs * c_list ?f'' cf h r [x]"
      using c_list_single_f_list_not_elem_prepend 2 by metis
    finally show ?thesis by simp
  qed(simp)
qed(simp)

lemma c_list'_eq_c_list:
  assumes "distinct xs"
      and "rev xs = r # rs"
    shows "c_list (ldeep_s f xs) cf (create_h_list h xs) r xs = c_list' f cf h xs"
using assms proof(induction xs arbitrary: rs)
  case (Cons x xs)
  then show ?case
  proof(cases "xs=[]")
    case False
    then obtain x' xs' where x'_def[simp]: "xs = x'#xs'" using List.list.exhaust_sel by auto
    then have 0: "x \<noteq> r" using distinct_first_uneq_last Cons by fast
    have 1: "distinct xs" using Cons.prems(1) by simp
    have "\<exists>rs'. rev xs = r # rs'"
      using Cons.prems Nil_is_append_conv butlast_append
      by (metis List.append.right_neutral List.butlast.simps(2) List.list.distinct(1)
          List.rev.simps(2) \<open>\<And>thesis. (\<And>x' xs'. xs = x' # xs' \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>)
    then obtain rs' where 2: "rev xs = r # rs'" by blast
    let ?h = "create_h_list h (x # x' # xs')"
    let ?h' = "create_h_list h (x' # xs')"
    let ?f = "ldeep_s f (x'#xs')"
    let ?f' = "ldeep_s f (x#x'#xs')"
    have "c_list (ldeep_s f (x#xs)) cf (create_h_list h (x # xs)) r (x # xs)
        = c_list ?f' cf ?h r (x # x' # xs')"
      by simp
    also have "\<dots> = c_list ?f' cf ?h r (x' # xs')
            + ldeep_T ?f' cf (x' # xs') * c_list ?f' cf ?h r [x]"
      by simp
    also have "\<dots> = c_list ?f' cf ?h r (x' # xs') + ldeep_T ?f' cf (x' # xs') * h (x' # xs') x"
      using 0 by simp
    also have "\<dots> = c_list ?f' cf ?h r (x' # xs') + ldeep_T ?f cf (x' # xs') * h (x' # xs') x"
      using distinct_ldeep_T_prepend[of "[x]" "x'#xs'"] Cons.prems(1) by simp
    also have "\<dots> = c_list ?f' cf ?h r (x' # xs') + ldeep_n f cf (x' # xs') * h (x' # xs') x"
      using ldeep_T_eq_ldeep_n 1 by fastforce
    also have "\<dots> = c_list ?f cf ?h r (x' # xs') + ldeep_n f cf (x' # xs') * h (x' # xs') x"
      using c_list_prepend_f_disjunct[of "[x]" "x'#xs'"] Cons.prems(1) by simp
    also have "\<dots> = c_list ?f cf ?h' r (x' # xs') + ldeep_n f cf (x' # xs') * h (x' # xs') x"
      using c_list_prepend_h_disjunct[of "[x]" "x'#xs'"] Cons.prems by simp
    also have "\<dots> = c_list' f cf h (x' # xs') + ldeep_n f cf (x' # xs') * h (x' # xs') x"
      using Cons.IH 1 2 by simp
    also have "\<dots> = c_list' f cf h (x#x' # xs')"
      using Cons.prems x'_def 1 2 by simp
    finally show ?thesis by simp
  qed(simp)
qed(simp)

lemma clist_eq_if_cf_eq:
  "\<forall>x. set x \<subseteq> set xs \<longrightarrow> ldeep_T sf cf' x = ldeep_T sf cf x
    \<Longrightarrow> c_list sf cf' h r xs = c_list sf cf h r xs"
  by (induction sf cf' h r xs rule: c_list.induct) (auto simp: subset_insertI2)

lemma ldeep_s_h_eq_list_sel_aux'_h:
  "\<lbrakk>distinct xs; ys@x#zs = xs\<rbrakk>
    \<Longrightarrow> (\<lambda>a. ldeep_s f xs a * cf a) x  = (\<lambda>xs x. (list_sel_aux' f xs x) * cf x) zs x"
  by (fastforce simp: distinct_ldeep_s_eq_aux)

corollary ldeep_s_h_eq_list_sel_aux'_h':
  "\<lbrakk>distinct_relations t; ys@x#zs = revorder t\<rbrakk>
    \<Longrightarrow> (\<lambda>a. ldeep_s f (revorder t) a * cf a) x = (\<lambda>xs x. (list_sel_aux' f xs x) * cf x) zs x"
  by (fastforce simp: distinct_rels_alt ldeep_s_h_eq_list_sel_aux'_h)

lemma create_h_list_distinct_simp: "\<lbrakk>distinct xs; ys@x#zs = xs\<rbrakk> \<Longrightarrow> create_h_list h xs x = h zs x"
  by (induction xs arbitrary: ys) (force simp: append_eq_Cons_conv)+

lemma ldeep_s_h_eq_create_h_list:
  "\<lbrakk>distinct xs; ys@x#zs = xs\<rbrakk>
    \<Longrightarrow> (\<lambda>a. ldeep_s f xs a * cf a) x = create_h_list (\<lambda>xs x. (list_sel_aux' f xs x) * cf x) xs x"
  by (simp add: distinct_relations_def create_h_list_distinct_simp ldeep_s_h_eq_list_sel_aux'_h)

lemma ldeep_s_h_eq_create_h_list':
  "\<lbrakk>distinct_relations t; ys@x#zs = revorder t\<rbrakk>
    \<Longrightarrow> (\<lambda>a. ldeep_s f (revorder t) a * cf a) x
      = create_h_list (\<lambda>xs x. (list_sel_aux' f xs x) * cf x) (revorder t) x"
  by (simp add: distinct_rels_alt ldeep_s_h_eq_create_h_list)

corollary ldeep_s_h_eq_create_h_list'':
  "distinct_relations t \<Longrightarrow> \<forall>ys x zs. ys@x#zs = revorder t
    \<longrightarrow> (\<lambda>a. ldeep_s f (revorder t) a * cf a) x
      = create_h_list (\<lambda>xs x. (list_sel_aux' f xs x) * cf x) (revorder t) x"
  using ldeep_s_h_eq_create_h_list' by fast

lemma ldeep_s_h_eq_create_h_list''':
  "\<lbrakk>distinct_relations t; x \<in> relations t\<rbrakk>
    \<Longrightarrow> (\<lambda>a. ldeep_s f (revorder t) a * cf a) x
      = create_h_list (\<lambda>xs x. (list_sel_aux' f xs x) * cf x) (revorder t) x"
  using ldeep_s_eq_list_sel_aux'_split revorder_eq_set
  by (fastforce simp add: distinct_rels_alt ldeep_s_h_eq_create_h_list)

lemma cons2_if_2elems: "\<lbrakk>x \<in> set xs; y \<in> set xs; x \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>y z zs. xs = y # z # zs"
  using last.simps list.set_cases neq_Nil_conv by metis

theorem c_IKKBZ_eq_c_list:
  fixes t
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
      and "\<forall>x \<in> relations t. h1 x (cf x) = h2 x"
  shows "c_IKKBZ h1 cf f t = c_list (ldeep_s f xs) cf h2 (first_node t) xs"
using assms proof(induction t arbitrary: xs rule: left_deep.induct)
  case (2 l r)
  let ?r = "first_node (Join l (Relation r))"
  let ?xs = "revorder (Join l (Relation r))"
  let ?ys = "revorder l"
  let ?sf = "ldeep_s f ?xs"
  have h1_h2_l: "\<forall>x \<in> relations l. h1 x (cf x) = h2 x" using "2.prems"(4) by simp
  have "c_IKKBZ h1 cf f (Join l (Relation r)) = card cf f l * (h1 r (cf r)) + c_IKKBZ h1 cf f l"
    by simp
  then have "c_IKKBZ h1 cf f (Join l (Relation r))
          = card cf f l * (h1 r (cf r)) + c_list (ldeep_s f ?ys) cf h2 ?r ?ys"
    using "2.hyps" "2.prems"(2-3) distinct_trans_l[OF "2.prems"(1)] h1_h2_l by force
  then have ind: "c_IKKBZ h1 cf f (Join l (Relation r))
          = card cf f l * (h1 r (cf r)) + c_list ?sf cf h2 ?r ?ys"
    using c_list_prepend_f_disjunct "2.prems"(1) unfolding distinct_rels_alt
    by (metis revorder.simps(2))
  have 0: "?r \<in> set ?xs" using first_node_last_revorder[of l] by force
  moreover have 1: "r \<in> set ?xs" by simp
  moreover have "distinct ?xs" using "2.prems"(1) distinct_rels_alt by force
  ultimately have "?r \<noteq> r" using first_node_last_revorder[of l] by auto
  then obtain z zs where z_def: "?xs = r # z # zs" using cons2_if_2elems[OF 0 1] by auto
  then have "c_list ?sf cf h2 ?r ?xs
          = c_list ?sf cf h2 ?r ?ys + ldeep_T ?sf cf ?ys * c_list ?sf cf h2 ?r [r]"
    by simp
  also have "\<dots> = c_list ?sf cf h2 ?r ?ys + ldeep_T ?sf cf ?ys * (h1 r (cf r))"
    using \<open>?r \<noteq> r\<close> "2.prems"(4) by fastforce
  also have "\<dots> = c_list ?sf cf h2 ?r ?ys + card cf f l * (h1 r (cf r))"
    using "2.prems"(1,3) ldeep_T_eq_card distinct_rels_alt distinct_ldeep_T_prepend
    by (metis revorder.simps(2) ldeep_trans distinct_trans_l)
  finally show ?case using ind by simp
qed(auto)

lemma c_IKKBZ_eq_c_list_cout:
  fixes f cf t
  defines "xs \<equiv> revorder t"
  defines "h \<equiv> (\<lambda>a. ldeep_s f xs a * cf a)"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
  shows "c_IKKBZ (\<lambda>a b. ldeep_s f xs a * b) cf f t = c_list (ldeep_s f xs) cf h (first_node t) xs"
  using assms c_IKKBZ_eq_c_list by fast

lemma c_IKKBZ_eq_c_list_cout_hlist:
  fixes f cf t
  defines "h \<equiv> (\<lambda>xs x. (list_sel_aux' f xs x) * cf x)"
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
  shows "c_IKKBZ (\<lambda>a b. ldeep_s f xs a * b) cf f t
        = c_list (ldeep_s f xs) cf (create_h_list h xs) (first_node t) xs"
  using assms c_IKKBZ_eq_c_list ldeep_s_h_eq_create_h_list'''[OF assms(3)] by fastforce

theorem c_out_eq_c_list:
  fixes f cf t
  defines "xs \<equiv> revorder t"
  defines "h \<equiv> (\<lambda>a. ldeep_s f xs a * cf a)"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
  shows "c_list (ldeep_s f xs) cf h (first_node t) xs = c_out cf f t"
  using c_IKKBZ_eq_c_list_cout c_out_IKKBZ assms by fastforce

theorem c_out_eq_c_list_hlist:
  fixes f cf t
  defines "h \<equiv> (\<lambda>xs x. (list_sel_aux' f xs x) * cf x)"
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
    shows "c_list (ldeep_s f xs) cf (create_h_list h xs) (first_node t) xs = c_out cf f t"
  using c_IKKBZ_eq_c_list_cout_hlist c_out_IKKBZ assms by fastforce

(* alternative proof using c_list' *)
lemma c_out_eq_c_list_altproof:
  fixes f cf t
  defines "h \<equiv> (\<lambda>xs x. (list_sel_aux' f xs x) * cf x)"
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
    shows "c_list (ldeep_s f xs) cf (create_h_list h xs) (first_node t) xs = c_out cf f t"
proof -
  obtain rs where rs_def[simp]: "rev (revorder t) = (first_node t) # rs"
    unfolding revorder_eq_rev_inorder using first_node_first_inorder by auto
  have 0: "distinct (revorder t)" using assms(3) distinct_rels_alt by auto
  then have "c_list (ldeep_s f xs) cf (create_h_list h xs) (first_node t) xs
          = c_list' f cf h (revorder t)"
    using rs_def c_list'_eq_c_list xs_def by fast
  then show ?thesis using assms c_out_eq_c_list' by auto
qed

text \<open>
  Similarly, we can derive the equivalence for other cost functions like @{term c_nlj} and
  @{term c_hj} by using the equivalence of @{term c_IKKBZ} and @{term c_list}.
\<close>

lemma c_IKKBZ_eq_c_list_hj:
  fixes f cf t
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
    shows "c_IKKBZ (\<lambda>_ _. 1.2) cf f t = c_list (ldeep_s f xs) cf (\<lambda>_. 1.2) (first_node t) xs"
  using c_IKKBZ_eq_c_list assms by fast

corollary c_hj_eq_c_list:
  fixes f cf t
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
    shows "c_list (ldeep_s f xs) cf (\<lambda>_. 1.2) (first_node t) xs = c_hj cf f t"
  using c_IKKBZ_eq_c_list_hj c_hj_IKKBZ assms by fastforce

lemma c_IKKBZ_eq_c_list_nlj:
  fixes f cf t
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
    shows "c_IKKBZ (\<lambda>_. id) cf f t = c_list (ldeep_s f xs) cf cf (first_node t) xs"
  using c_IKKBZ_eq_c_list assms by fastforce

corollary c_nlj_eq_c_list:
  fixes f cf t
  defines "xs \<equiv> revorder t"
  assumes "distinct_relations t"
      and "reasonable_cards cf f t"
      and "left_deep t"
    shows "c_list (ldeep_s f xs) cf cf (first_node t) xs = c_nlj cf f t"
  using c_IKKBZ_eq_c_list_nlj c_nlj_IKKBZ assms by fastforce

lemma c_list_app:
  "c_list f cf h r (ys@xs) = c_list f cf h r xs + ldeep_T f cf xs * c_list f cf h r ys"
proof(induction ys)
  case (Cons y ys)
  then show ?case
  proof(cases "xs=[]")
    case True
    then show ?thesis using ldeep_T_empty by auto
  next
    case False
    then obtain x' xs' where x'_def[simp]: "xs = x'#xs'" using List.list.exhaust_sel by blast
    then have "c_list f cf h r (y#ys @ xs)
            = c_list f cf h r (ys@xs) + ldeep_T f cf (ys@xs) * c_list f cf h r [y]"
      by (metis CostFunctions.c_list.simps(3) Nil_is_append_conv neq_Nil_conv)
    also have "\<dots> = c_list f cf h r xs + ldeep_T f cf xs * c_list f cf h r ys
            + ldeep_T f cf (ys@xs) * c_list f cf h r [y]"
      using Cons.IH by simp
    also have "\<dots> = c_list f cf h r xs + ldeep_T f cf xs * c_list f cf h r ys
            + ldeep_T f cf ys * ldeep_T f cf xs * c_list f cf h r [y]"
      using ldeep_T_app by auto
    also have "\<dots> = c_list f cf h r xs + ldeep_T f cf xs * (c_list f cf h r ys
            + ldeep_T f cf ys * c_list f cf h r [y])"
      by argo
    also have "\<dots> = c_list f cf h r xs + ldeep_T f cf xs * (c_list f cf h r (y # ys))"
      using False neq_Nil_conv List.append.left_neutral
      by (metis CostFunctions.c_list.simps(3) calculation)
    finally show ?thesis by simp
  qed
qed(simp)

lemma create_h_list_pos:
  "\<lbrakk>sel_reasonable sf; \<forall>x \<in> set xs. cf x > 0\<rbrakk>
    \<Longrightarrow> (create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs) x > 0"
  by (induction xs) (auto simp: list_sel_aux'_reasonable)

lemma c_list_not_neg:
  assumes "sel_reasonable sf"
      and "\<forall>x \<in> set ys. cf x > 0"
      and "h = (\<lambda>a. ldeep_s sf xs a * cf a)"
    shows "c_list (ldeep_s sf xs) cf h r ys \<ge> 0"
using assms proof(induction ys arbitrary: xs)
  case ind: (Cons y ys)
  let ?sf = "ldeep_s sf xs"
  show ?case
  proof(cases ys)
    case Nil
    then show ?thesis using ind.prems by (simp add: ldeep_s_pos order_less_imp_le)
  next
    case (Cons y' ys')
    show ?thesis
    proof(cases "y=r")
      case True
      then show ?thesis using Cons ind by simp
    next
      case False
      have "c_list ?sf cf h r (y # ys) = c_list ?sf cf h r ys + ldeep_T ?sf cf ys * h y"
        using Cons False by simp
      then have "c_list ?sf cf h r (y # ys) \<ge> ldeep_T ?sf cf ys * h y"
        using ind by simp
      moreover have "ldeep_T ?sf cf ys * h y > 0"
        using ind.prems by (simp add: ldeep_T_pos ldeep_s_pos)
      ultimately show ?thesis by simp
    qed
  qed
qed(simp)

lemma c_list_not_neg_hlist:
  assumes "sel_reasonable sf"
      and "\<forall>x \<in> set xs. cf x > 0"
      and "\<forall>x \<in> set ys. cf x > 0"
      and "h = create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs"
    shows "c_list (ldeep_s sf xs) cf h r ys \<ge> 0"
using assms proof(induction ys arbitrary: xs)
  case ind: (Cons y ys)
  let ?sf = "ldeep_s sf xs"
  show ?case
  proof(cases ys)
    case Nil
    then show ?thesis
      using ind.prems by(cases "y=r")(auto simp: create_h_list_pos less_eq_real_def)
  next
    case (Cons y' ys')
    show ?thesis
    proof(cases "y=r")
      case True
      then show ?thesis using Cons ind by simp
    next
      case False
      have "c_list ?sf cf h r (y # ys) = c_list ?sf cf h r ys + ldeep_T ?sf cf ys * h y"
        using Cons False by simp
      then have "c_list ?sf cf h r (y # ys) \<ge> ldeep_T ?sf cf ys * h y"
        using ind by simp
      moreover have "ldeep_T ?sf cf ys * h y > 0"
        using create_h_list_pos[of sf xs cf y] ind.prems by (simp add: ldeep_T_pos)
      ultimately show ?thesis by simp
    qed
  qed
qed(simp)

lemma c_list_pos_if_h_pos:
  "\<lbrakk>sel_reasonable sf; \<forall>x \<in> set xs. cf x > 0; \<forall>x \<in> set xs. h x > 0; r \<notin> set xs; xs \<noteq> []\<rbrakk>
    \<Longrightarrow> c_list (ldeep_s sf ys) cf h r xs > 0"
proof(induction "ldeep_s sf ys" cf h r xs rule: c_list.induct)
  case (3 cf h r y x xs)
  have "ldeep_T (ldeep_s sf ys) cf (x#xs) > 0" using ldeep_T_pos[of "x#xs"] "3.prems"(1,2) by simp
  then have "ldeep_T (ldeep_s sf ys) cf (x#xs) * c_list (ldeep_s sf ys) cf h r [y] > 0"
    using 3 by auto
  moreover have "c_list (ldeep_s sf ys) cf h r (x#xs) > 0" using 3 by auto
  ultimately show ?case by simp
qed(auto)

lemma c_list_pos_r_not_elem:
  assumes "sel_reasonable sf"
      and "\<forall>x \<in> set ys. cf x > 0"
      and "ys \<noteq> []"
      and "r \<notin> set ys"
      and "h = (\<lambda>a. ldeep_s sf xs a * cf a)"
    shows "c_list (ldeep_s sf xs) cf h r ys > 0"
  using c_list_pos_if_h_pos ldeep_s_pos assms by fastforce

lemma c_list_pos_r_not_elem_hlist:
  assumes "sel_reasonable sf"
      and "\<forall>x \<in> set xs. cf x > 0"
      and "\<forall>x \<in> set ys. cf x > 0"
      and "ys \<noteq> []"
      and "r \<notin> set ys"
      and "h = create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs"
    shows "c_list (ldeep_s sf xs) cf h r ys > 0"
  using c_list_pos_if_h_pos create_h_list_pos[OF assms(1)] assms by fastforce

lemma c_list_pos_not_root:
  assumes "sel_reasonable sf"
      and "\<forall>x \<in> set ys. cf x > 0"
      and "ys \<noteq> []"
      and "ys \<noteq> [r]"
      and "distinct ys"
      and "h = (\<lambda>a. ldeep_s sf xs a * cf a)"
    shows "c_list (ldeep_s sf xs) cf h r ys > 0"
using assms proof(induction ys arbitrary: xs)
  case ind: (Cons y ys)
  let ?sf = "ldeep_s sf xs"
  show ?case
  proof(cases ys)
    case Nil
    then have "c_list ?sf cf h r (y # ys) = h y" using ind.prems(4) by simp
    then show ?thesis using ind.prems(1,2,6) by (simp add: ldeep_s_pos)
  next
    case (Cons y' ys')
    show ?thesis
    proof(cases "y=r")
      case True
      then have 0: "r \<notin> set ys" using ind.prems(5) by simp
      have "c_list ?sf cf h r (y # ys) = c_list ?sf cf h r ys"
        using Cons True by simp
      then show ?thesis using ind.prems(1,2,4,6) 0 True by (fastforce intro: c_list_pos_r_not_elem)
    next
      case False
      have "c_list ?sf cf h r (y # ys) = c_list ?sf cf h r ys + ldeep_T ?sf cf ys * h y"
        using Cons False by simp
      then have "c_list ?sf cf h r (y # ys) \<ge> ldeep_T ?sf cf ys * h y"
        using c_list_not_neg ind.prems(1,2,3,6) by fastforce
      moreover have "ldeep_T ?sf cf ys * h y > 0"
        using ind.prems(1,2,6) by (simp add: ldeep_T_pos ldeep_s_pos)
      ultimately show ?thesis by simp
    qed
  qed
qed(simp)

lemma c_list_pos_not_root_hlist:
  assumes "sel_reasonable sf"
      and "\<forall>x \<in> set xs. cf x > 0"
      and "\<forall>x \<in> set ys. cf x > 0"
      and "ys \<noteq> []"
      and "ys \<noteq> [r]"
      and "distinct ys"
      and "h = create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs"
    shows "c_list (ldeep_s sf xs) cf h r ys > 0"
using assms proof(induction ys arbitrary: xs)
  case ind: (Cons y ys)
  let ?sf = "ldeep_s sf xs"
  show ?case
  proof(cases ys)
    case Nil
    then have "c_list ?sf cf h r (y # ys) = h y" using ind.prems(5) by simp
    then show ?thesis using create_h_list_pos ind.prems(1,2,7) by fastforce
  next
    case (Cons y' ys')
    show ?thesis
    proof(cases "y=r")
      case True
      then have 0: "r \<notin> set ys" using ind.prems(6) by simp
      have "c_list ?sf cf h r (y # ys) = c_list ?sf cf h r ys"
        using Cons True by simp
      then show ?thesis
        using c_list_pos_r_not_elem_hlist[of sf xs cf ys r h] 0 ind.prems(1,2,3,7) Cons by auto
    next
      case False
      have "c_list ?sf cf h r (y # ys) = c_list ?sf cf h r ys + ldeep_T ?sf cf ys * h y"
        using Cons False by simp
      then have "c_list ?sf cf h r (y # ys) \<ge> ldeep_T ?sf cf ys * h y"
        using c_list_not_neg_hlist ind.prems(1,2,3,7) by fastforce
      moreover have "ldeep_T ?sf cf ys * h y > 0"
        using ind.prems(1,2,3,7) by (simp add: ldeep_T_pos create_h_list_pos)
      ultimately show ?thesis by simp
    qed
  qed
qed(simp)

lemma c_list_split_four:
  assumes "T = ldeep_T f cf"
      and "C = c_list f cf h r"
    shows "C (rev (A @ U @ V @ B)) = C (rev A) + T (rev A) * C (rev U)
            + T (rev A) * T (rev U) * C (rev V)
            + T (rev A) * T (rev U) * T (rev V) * C (rev B)"
proof -
  let ?T = "ldeep_T f cf"
  let ?C = "c_list f cf h r"
  have "?C (rev (A @ U @ V @ B))
      = ?C (rev A) + ?T (rev A) * ?C (rev (U @ V @ B))"
    using c_list_app[where ys="rev (U@V@B)"] by simp
  also have "\<dots> = ?C (rev A) + ?T (rev A) * (?C (rev U)
        + ?T (rev U) * ?C (rev (V@B)))"
    using c_list_app[where ys="rev (V@B)"] by simp
  also have "\<dots> = ?C (rev A) + ?T (rev A) * ?C (rev U)
        + ?T (rev A) * ?T (rev U) * ?C (rev (V@B))"
    by argo
  also have "\<dots> = ?C (rev A) + ?T (rev A) * ?C (rev U)
        + ?T (rev A) * ?T (rev U) * (?C (rev V)
        + ?T (rev V) * ?C (rev B))"
    using c_list_app by force
  finally have 0: "?C (rev (A @ U @ V @ B))
      = ?C (rev A) + ?T (rev A) * ?C (rev U)
        + ?T (rev A) * ?T (rev U) * ?C (rev V)
        + ?T (rev A) * ?T (rev U) * ?T (rev V) * ?C (rev B)"
    by argo
  then show ?thesis using assms by simp
qed

lemma c_list_A_pos_asi:
  assumes "c_list f cf h r (rev U) > 0"
      and "c_list f cf h r (rev V) > 0"
      and "ldeep_T f cf (rev A) > 0"
    shows "c_list f cf h r (rev (A @ U @ V @ B)) \<le> c_list f cf h r (rev (A @ V @ U @ B))
       \<longleftrightarrow> ((ldeep_T f cf (rev U) - 1) / c_list f cf h r (rev U)
          \<le> (ldeep_T f cf (rev V) - 1) / c_list f cf h r (rev V))"
proof -
  let ?T = "ldeep_T f cf"
  let ?C = "c_list f cf h r"
  let ?rank = "(\<lambda>l. (?T l - 1) / ?C l)"
  have 0: "?C (rev (A @ U @ V @ B))
      = ?C (rev A) + ?T (rev A) * ?C (rev U)
        + ?T (rev A) * ?T (rev U) * ?C (rev V)
        + ?T (rev A) * ?T (rev U) * ?T (rev V) * ?C (rev B)"
    using c_list_split_four by fastforce
  have "?C (rev (A @ V @ U @ B))
      = ?C (rev A) + ?T (rev A) * ?C (rev V)
        + ?T (rev A) * ?T (rev V) * ?C (rev U)
        + ?T (rev A) * ?T (rev V) * ?T (rev U) * ?C (rev B)"
    using c_list_split_four by fastforce
  then have "?C (rev (A@U@V@B)) - ?C (rev (A@V@U@B))
          = ?T (rev A) * (?C (rev V) * (?T (rev U) - 1) - ?C (rev U) * (?T (rev V) - 1))"
    using 0 by argo
  also have "\<dots> = ?T (rev A) *
              (?C (rev V) * (?T (rev U) - 1) * (?C (rev U) / ?C (rev U))
                - ?C (rev U) * (?T (rev V) - 1) * (?C (rev V) / ?C (rev V)))"
    using assms
    by (metis Groups.monoid_mult_class.mult.right_neutral divide_self_if less_numeral_extra(3))
  also have "\<dots> = ?T (rev A) * ?C (rev U) * ?C (rev V) * (?rank (rev U) - ?rank (rev V))"
    by argo
  finally have 1: "?C (rev (A@U@V@B)) - ?C (rev (A@V@U@B))
              = ?T (rev A) * ?C (rev U) * ?C (rev V) * (?rank (rev U) - ?rank (rev V))".
  then show ?thesis
  proof(cases "?C (rev (A@U@V@B)) \<le> ?C (rev (A@V@U@B))")
    case True
    then show ?thesis by (smt (verit) assms 1 mult_pos_pos)
  next
    case False
    then show ?thesis by (smt (z3) 1 assms mult_pos_pos zero_less_mult_pos)
  qed
qed

lemma c_list_asi_aux:
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "c = c_list f cf h r"
      and "f = (ldeep_s sf xs)"
      and "\<forall>ys. (ys \<noteq> [] \<and> r \<notin> set ys) \<longrightarrow> c ys > 0"
      and "distinct (A@U@V@B)"
      and "U \<noteq> []"
      and "V \<noteq> []"
      and "rank = (\<lambda>l. (ldeep_T f cf l - 1) / c l)"
      and "r \<notin> set (A@U@V@B) \<or> (take 1 (A@U@V@B) = [r] \<and> take 1 (A@V@U@B) = [r])"
    shows "(c (rev (A@U@V@B)) \<le> c (rev (A@V@U@B)) \<longleftrightarrow> rank (rev U) \<le> rank (rev V))"
proof (cases "r \<notin> set (A@U@V@B)")
  case True
  have 0: "ldeep_T f cf (rev A) > 0" using assms(1,2,4) ldeep_T_pos by fast
  have "r \<notin> set (rev U)" using True by simp
  then have 1: "c_list f cf h r (rev U) > 0"
    using c_list_pos_r_not_elem assms(1-5,7) by fastforce
  have "r \<notin> set (rev V)" using True by simp
  then have "c_list f cf h r (rev V) > 0"
    using c_list_pos_r_not_elem assms(1-5,8) by fastforce
  then show ?thesis using c_list_A_pos_asi 0 1 assms(3,9) by fast
next
  case False
  have 0: "ldeep_T f cf (rev A) > 0" using assms(1,2,4) ldeep_T_pos by fast
  have r_first: "take 1 (A@U@V@B) = [r] \<and> take 1 (A@V@U@B) = [r]"
    using assms(10) False by blast
  then have "take 1 A = [r]" using assms(6-8) distinct_change_order_first_elem by metis
  then have "r \<in> set A" by (metis List.list.set_intros(1) in_set_takeD)
  then have 1: "r \<notin> set (U@V@B)" using assms(6) by auto
  then have "r \<notin> set (rev U)" by simp
  then have 2: "c_list f cf h r (rev U) > 0"
    using c_list_pos_r_not_elem assms(1-5,7) by fastforce
  have "r \<notin> set (rev V)" using 1 by simp
  then have "c_list f cf h r (rev V) > 0"
    using c_list_pos_r_not_elem assms(1-5,8) by fastforce
  then show ?thesis using c_list_A_pos_asi 0 2 assms(3,9) by fast
qed

lemma c_list_pos_asi:
  fixes sf cf h r xs
  defines "f \<equiv> ldeep_s sf xs"
  defines "rank \<equiv> (\<lambda>l. (ldeep_T f cf l - 1) / c_list f cf h r l)"
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "\<forall>ys. (ys \<noteq> [] \<and> r \<notin> set ys) \<longrightarrow> c_list f cf h r ys > 0"
  shows "asi rank r (c_list f cf h r)"
  unfolding asi_def using c_list_asi_aux[OF assms(3,4)] assms(1,2,5) by simp

theorem c_list_asi:
  fixes sf cf h r xs
  defines "f \<equiv> ldeep_s sf xs"
  defines "rank \<equiv> (\<lambda>l. (ldeep_T f cf l - 1) / c_list f cf h r l)"
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "\<forall>x. h x > 0"
  shows "asi rank r (c_list f cf h r)"
  using c_list_pos_asi assms c_list_pos_if_h_pos[OF assms(3)] by fastforce

corollary c_out_asi:
  fixes sf cf r xs
  defines "f \<equiv> ldeep_s sf xs"
  defines "h \<equiv> (\<lambda>a. ldeep_s sf xs a * cf a)"
  defines "rank \<equiv> (\<lambda>l. (ldeep_T f cf l - 1) / c_list f cf h r l)"
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
  shows "asi rank r (c_list f cf h r)"
  using c_list_asi ldeep_s_pos assms by fastforce

(* old alternative proof that proofs asi property directly for this specific h *)
lemma c_out_asi_aux:
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "c = c_list f cf h r"
      and "f = (ldeep_s sf xs)"
      and "h = (\<lambda>a. ldeep_s sf xs a * cf a)"
      and "distinct (A@U@V@B)"
      and "U \<noteq> []"
      and "V \<noteq> []"
      and "rank = (\<lambda>l. (ldeep_T f cf l - 1) / c l)"
      and "r \<notin> set (A@U@V@B) \<or> (take 1 (A@U@V@B) = [r] \<and> take 1 (A@V@U@B) = [r])"
    shows "(c (rev (A@U@V@B)) \<le> c (rev (A@V@U@B)) \<longleftrightarrow> rank (rev U) \<le> rank (rev V))"
proof (cases "r \<notin> set (A@U@V@B)")
  case True
  have 0: "ldeep_T f cf (rev A) > 0" using assms(1,2,4) ldeep_T_pos by fast
  have "r \<notin> set (rev U)" using True by simp
  then have 1: "c_list f cf h r (rev U) > 0"
    using c_list_pos_r_not_elem assms(1,2,4,5,7) by fastforce
  have "r \<notin> set (rev V)" using True by simp
  then have "c_list f cf h r (rev V) > 0"
    using c_list_pos_r_not_elem assms(1,2,4,5,8) by fastforce
  then show ?thesis using c_list_A_pos_asi 0 1 assms(3,9) by fast
next
  case False
  have 0: "ldeep_T f cf (rev A) > 0" using assms(1,2,4) ldeep_T_pos by fast
  have r_first: "take 1 (A@U@V@B) = [r] \<and> take 1 (A@V@U@B) = [r]"
    using assms(10) False by blast
  then have "take 1 A = [r]" using assms(6-8) distinct_change_order_first_elem by metis
  then have "r \<in> set A" by (metis List.list.set_intros(1) in_set_takeD)
  then have 1: "r \<notin> set (U@V@B)" using assms(6) by auto
  then have "r \<notin> set (rev U)" by simp
  then have 2: "c_list f cf h r (rev U) > 0"
    using c_list_pos_r_not_elem assms(1,2,4,5,7) by fastforce
  have "r \<notin> set (rev V)" using 1 by simp
  then have "c_list f cf h r (rev V) > 0"
    using c_list_pos_r_not_elem assms(1,2,4,5,8) by fastforce
  then show ?thesis using c_list_A_pos_asi 0 2 assms(3,9) by fast
qed

lemma c_out_asi_aux_hlist:
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "c = c_list f cf h r"
      and "f = (ldeep_s sf xs)"
      and "h = create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs"
      and "distinct (A@U@V@B)"
      and "U \<noteq> []"
      and "V \<noteq> []"
      and "rank = (\<lambda>l. (ldeep_T f cf l - 1) / c l)"
      and "r \<notin> set (A@U@V@B) \<or> (take 1 (A@U@V@B) = [r] \<and> take 1 (A@V@U@B) = [r])"
    shows "(c (rev (A@U@V@B)) \<le> c (rev (A@V@U@B)) \<longleftrightarrow> rank (rev U) \<le> rank (rev V))"
proof (cases "r \<notin> set (A@U@V@B)")
  case True
  have 0: "ldeep_T f cf (rev A) > 0" using assms(1,2,4) ldeep_T_pos by fast
  have "r \<notin> set (rev U)" using True by simp
  then have 1: "c_list f cf h r (rev U) > 0"
    using c_list_pos_r_not_elem_hlist assms(1,2,4,5,7) by fastforce
  have "r \<notin> set (rev V)" using True by simp
  then have "c_list f cf h r (rev V) > 0"
    using c_list_pos_r_not_elem_hlist assms(1,2,4,5,8) by fastforce
  then show ?thesis using c_list_A_pos_asi 0 1 assms(3,9) by fast
next
  case False
  have 0: "ldeep_T f cf (rev A) > 0" using assms(1,2,4) ldeep_T_pos by fast
  have r_first: "take 1 (A@U@V@B) = [r] \<and> take 1 (A@V@U@B) = [r]"
    using assms(10) False by blast
  then have "take 1 A = [r]" using assms(6-8) distinct_change_order_first_elem by metis
  then have "r \<in> set A" by (metis List.list.set_intros(1) in_set_takeD)
  then have 1: "r \<notin> set (U@V@B)" using assms(6) by auto
  then have "r \<notin> set (rev U)" by simp
  then have 2: "c_list f cf h r (rev U) > 0"
    using c_list_pos_r_not_elem_hlist assms(1,2,4,5,7) by fastforce
  have "r \<notin> set (rev V)" using 1 by simp
  then have "c_list f cf h r (rev V) > 0"
    using c_list_pos_r_not_elem_hlist assms(1,2,4,5,8) by fastforce
  then show ?thesis using c_list_A_pos_asi 0 2 assms(3,9) by fast
qed

theorem c_out_asi_altproof:
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "c = c_list f cf h r"
      and "f = (ldeep_s sf xs)"
      and "h = (\<lambda>a. ldeep_s sf xs a * cf a)"
    shows "asi (\<lambda>l. (ldeep_T f cf l - 1) / c l) r (c_list f cf h r)"
  unfolding asi_def using c_out_asi_aux[OF assms] assms(3) by blast

theorem c_out_asi_hlist:
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "c = c_list f cf h r"
      and "f = (ldeep_s sf xs)"
      and "h = create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs"
    shows "asi (\<lambda>l. (ldeep_T f cf l - 1) / c l) r (c_list f cf h r)"
  unfolding asi_def using c_out_asi_aux_hlist[OF assms] assms(3) by blast

lemma asi_if_asi': "asi rank r c \<Longrightarrow> asi' r c"
  unfolding asi'_def asi_def by auto

corollary c_out_asi':
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "f = (ldeep_s sf xs)"
      and "h = (\<lambda>a. ldeep_s sf xs a * cf a)"
    shows "asi' r (c_list f cf h r)"
  using asi_if_asi' c_out_asi[OF assms(1,2)] assms(3,4) by fast

corollary c_out_asi'_hlist:
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "f = (ldeep_s sf xs)"
      and "h = create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs"
    shows "asi' r (c_list f cf h r)"
  using asi_if_asi' c_out_asi_hlist[OF assms(1,2)] assms(3,4) by fast

lemma c_out_asi''_aux:
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "c = c_list f cf h r"
      and "f = (ldeep_s sf xs)"
      and "h = create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs"
      and "distinct (A@U@V@B)"
      and "U \<noteq> []"
      and "V \<noteq> []"
      and "rank = (\<lambda>l. (ldeep_T f cf l - 1) / c l)"
      and "U \<noteq> [r]"
      and "V \<noteq> [r]"
    shows "(c (rev (A@U@V@B)) \<le> c (rev (A@V@U@B)) \<longleftrightarrow> rank (rev U) \<le> rank (rev V))"
proof (cases "r \<notin> set (A@U@V@B)")
  case True
  have 0: "ldeep_T f cf (rev A) > 0" using assms(1,2,4) ldeep_T_pos by fast
  have "r \<notin> set (rev U)" using True by simp
  then have 1: "c_list f cf h r (rev U) > 0"
    using c_list_pos_r_not_elem_hlist assms(1,2,4,5,7) by fastforce
  have "r \<notin> set (rev V)" using True by simp
  then have "c_list f cf h r (rev V) > 0"
    using c_list_pos_r_not_elem_hlist assms(1,2,4,5,8) by fastforce
  then show ?thesis using c_list_A_pos_asi 0 1 assms(3,9) by fast
next
  case False
  have 0: "ldeep_T f cf (rev A) > 0" using assms(1,2,4) ldeep_T_pos by fast
  have 2: "c_list f cf h r (rev U) > 0"
    using c_list_pos_not_root_hlist assms(1,2,4-7,10) by fastforce
  have "c_list f cf h r (rev V) > 0"
    using c_list_pos_not_root_hlist assms(1,2,4-6,8,11) by fastforce
  then show ?thesis using c_list_A_pos_asi 0 2 assms(3,9) by fast
qed

theorem c_out_asi'':
  assumes "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "c = c_list f cf h r"
      and "f = (ldeep_s sf xs)"
      and "h = create_h_list (\<lambda>xs x. (list_sel_aux' sf xs x) * cf x) xs"
    shows "asi'' (\<lambda>l. (ldeep_T f cf l - 1) / c l) r (c_list f cf h r)"
  unfolding asi''_def using c_out_asi''_aux[OF assms] assms(3) by blast

subsubsection \<open>Additional ASI Proofs\<close>

lemma asi_le_iff_notr:
  "\<lbrakk>asi rank r cost; U \<noteq> []; V \<noteq> []; r \<notin> set (A @ U @ V @ B); distinct (A @ U @ V @ B)\<rbrakk>
    \<Longrightarrow> rank (rev U) \<le> rank (rev V) \<longleftrightarrow> cost (rev (A@U@V@B)) \<le> cost (rev (A@V@U@B))"
  unfolding asi_def by blast

lemma asi_le_iff_rfst:
  "\<lbrakk>asi rank r cost; U \<noteq> []; V \<noteq> [];
    take 1 (A @ U @ V @ B) = [r]; take 1 (A @ V @ U @ B) = [r]; distinct (A @ U @ V @ B)\<rbrakk>
    \<Longrightarrow> rank (rev U) \<le> rank (rev V) \<longleftrightarrow> cost (rev (A@U@V@B)) \<le> cost (rev (A@V@U@B))"
  unfolding asi_def by blast

lemma asi_le_notr:
  "\<lbrakk>asi rank r cost; rank (rev U) \<le> rank (rev V); U\<noteq>[]; V\<noteq>[];
    distinct (A@U@V@B); r \<notin> set (A@U@V@B)\<rbrakk>
    \<Longrightarrow> cost (rev (A@U@V@B)) \<le> cost (rev (A@V@U@B))"
  unfolding asi_def by blast

lemma asi_le_rfst:
  "\<lbrakk>asi rank r cost; rank (rev U) \<le> rank (rev V); U\<noteq>[]; V\<noteq>[]; distinct (A@U@V@B);
    take 1 (A @ U @ V @ B) = [r]; take 1 (A @ V @ U @ B) = [r]\<rbrakk>
    \<Longrightarrow> cost (rev (A@U@V@B)) \<le> cost (rev (A@V@U@B))"
  unfolding asi_def by blast

lemma asi_eq_notr:
  assumes "asi rank r cost"
      and "rank (rev U) = rank (rev V)"
      and "U \<noteq> []"
      and "V \<noteq> []"
      and "r \<notin> set (A@U@V@B)"
      and "distinct (A @ U @ V @ B)"
    shows "cost (rev (A@U@V@B)) = cost (rev (A@V@U@B))"
proof -
  have 0: "distinct (A@V@U@B)" using assms(6) by auto
  have 1: "r \<notin> set (A@V@U@B)" using assms(5) by auto
  then show ?thesis
    using asi_le_iff_notr[OF assms(1,3-6)] asi_le_iff_notr[OF assms(1,4,3) 1 0] assms(2) by simp
qed

lemma asi_eq_notr':
  assumes "asi rank r cost"
      and "cost (rev (A@U@V@B)) = cost (rev (A@V@U@B))"
      and "U \<noteq> []"
      and "V \<noteq> []"
      and "r \<notin> set (A@U@V@B)"
      and "distinct (A @ U @ V @ B)"
    shows "rank (rev U) = rank (rev V)"
proof -
  have 0: "distinct (A@V@U@B)" using assms(6) by auto
  have 1: "r \<notin> set (A@V@U@B)" using assms(5) by auto
  show ?thesis
    using asi_le_iff_notr[OF assms(1,3-6)] asi_le_iff_notr[OF assms(1,4,3) 1 0] assms(2) by simp
qed

lemma asi_eq_iff_notr:
  "\<lbrakk>asi rank r cost; U \<noteq> []; V \<noteq> []; r \<notin> set (A@U@V@B); distinct (A@U@V@B)\<rbrakk>
    \<Longrightarrow> rank (rev U) = rank (rev V) \<longleftrightarrow> cost (rev (A@U@V@B)) = cost (rev (A@V@U@B))"
  using asi_eq_notr[of rank r cost] asi_eq_notr'[of rank r cost] by blast

lemma asi_eq_rfst:
  assumes "asi rank r cost"
      and "rank (rev U) = rank (rev V)"
      and "U \<noteq> []"
      and "V \<noteq> []"
      and "take 1 (A @ U @ V @ B) = [r]"
      and "take 1 (A @ V @ U @ B) = [r]"
      and "distinct (A @ U @ V @ B)"
    shows "cost (rev (A@U@V@B)) = cost (rev (A@V@U@B))"
proof -
  have 0: "distinct (A@V@U@B)" using assms(7) by auto
  show ?thesis
    using asi_le_iff_rfst[OF assms(1,3-7)] asi_le_iff_rfst[OF assms(1,4,3,6,5) 0] assms(2) by simp
qed

lemma asi_eq_rfst':
  assumes "asi rank r cost"
      and "cost (rev (A@U@V@B)) = cost (rev (A@V@U@B))"
      and "U \<noteq> []"
      and "V \<noteq> []"
      and "take 1 (A @ U @ V @ B) = [r]"
      and "take 1 (A @ V @ U @ B) = [r]"
      and "distinct (A @ U @ V @ B)"
    shows "rank (rev U) = rank (rev V)"
proof -
  have 0: "distinct (A@V@U@B)" using assms(7) by auto
  show ?thesis
    using asi_le_iff_rfst[OF assms(1,3-7)] asi_le_iff_rfst[OF assms(1,4,3,6,5) 0] assms(2) by simp
qed

lemma asi_eq_iff_rfst:
  "\<lbrakk>asi rank r cost; U \<noteq> []; V \<noteq> [];
    take 1 (A @ U @ V @ B) = [r]; take 1 (A @ V @ U @ B) = [r]; distinct (A @ U @ V @ B)\<rbrakk>
    \<Longrightarrow> rank (rev U) = rank (rev V) \<longleftrightarrow> cost (rev (A@U@V@B)) = cost (rev (A@V@U@B))"
  using asi_eq_rfst[of rank r cost] asi_eq_rfst'[of rank r cost] by blast

lemma asi_lt_iff_notr:
  assumes "asi rank r cost"
      and "U \<noteq> []" and "V \<noteq> []"
      and "r \<notin> set (A @ U @ V @ B)"
      and "distinct (A @ U @ V @ B)"
    shows "rank (rev U) < rank (rev V) \<longleftrightarrow> cost (rev (A@U@V@B)) < cost (rev (A@V@U@B))"
  using asi_le_iff_notr[OF assms] asi_eq_iff_notr[OF assms] by auto

lemma asi_lt_iff_rfst:
  assumes "asi rank r cost"
      and "U \<noteq> []" and "V \<noteq> []"
      and "take 1 (A @ U @ V @ B) = [r]"
      and "take 1 (A @ V @ U @ B) = [r]"
      and "distinct (A @ U @ V @ B)"
    shows "rank (rev U) < rank (rev V) \<longleftrightarrow> cost (rev (A@U@V@B)) < cost (rev (A@V@U@B))"
  using asi_le_iff_rfst[OF assms] asi_eq_iff_rfst[OF assms] by auto

lemma asi_lt_notr:
  "\<lbrakk>asi rank r cost; rank (rev U) < rank (rev V); U\<noteq>[]; V\<noteq>[];
    distinct (A@U@V@B); r \<notin> set (A@U@V@B)\<rbrakk>
    \<Longrightarrow> cost (rev (A@U@V@B)) < cost (rev (A@V@U@B))"
  using asi_lt_iff_notr by fastforce

lemma asi_lt_rfst:
  "\<lbrakk>asi rank r cost; rank (rev U) < rank (rev V); U\<noteq>[]; V\<noteq>[]; distinct (A@U@V@B);
    take 1 (A @ U @ V @ B) = [r]; take 1 (A @ V @ U @ B) = [r]\<rbrakk>
    \<Longrightarrow> cost (rev (A@U@V@B)) < cost (rev (A@V@U@B))"
  using asi_lt_iff_rfst by fastforce

lemma asi''_simp_iff:
  "\<lbrakk>asi'' rank r cost; U \<noteq> []; V \<noteq> []; U \<noteq> [r]; V \<noteq> [r]; distinct (A @ U @ V @ B)\<rbrakk>
    \<Longrightarrow> rank (rev U) \<le> rank (rev V) \<longleftrightarrow> cost (rev (A@U@V@B)) \<le> cost (rev (A@V@U@B))"
  unfolding asi''_def by blast

lemma asi''_simp:
  "\<lbrakk>asi'' rank r cost; rank (rev U) \<le> rank (rev V); U\<noteq>[]; V\<noteq>[]; distinct (A@U@V@B); U\<noteq>[r]; V\<noteq>[r]\<rbrakk>
    \<Longrightarrow> cost (rev (A@U@V@B)) \<le> cost (rev (A@V@U@B))"
  unfolding asi''_def by blast

end


text:
theory structured_proofs_in_Isar_HOL
imports Main "Saturation_Framework.Calculus"
begin
(* notes*)

(* deux ! pour entrer \<And> *)

(* section 2: Logic *)
(* section 2.1 : Propositional logic *)

(* introduction rules*)
lemma "A \<longrightarrow> A"
proof (rule impI)
  assume a: "A"
  show "A" by (rule a) (* ! ? what is (rule a ) *)
qed
(* Command "proof" automatically tries to select an introduction rule based on the goal
    and a predefined list of rules *)

(* in the following proof, "impI" is automatically applied *)
lemma "A \<longrightarrow> A"
proof
  assume a: A
  show A by (rule a)
qed

(*  Trivial proofs, in particular those by assumption, should be trivial to perform.
    Proof "." does just that (and a bit more). Thus naming of assumptions is often superfluous.*)

lemma "A \<longrightarrow> A"
proof
  assume a : "A"
  from \<open> A \<close> show "A" .
qed

(* To hide proofs by assumption further, "by (method)" first applies method and then tries
  to solve all remaining subgoals by assumption:*)

lemma "A \<longrightarrow> A \<and> A"
proof (rule impI)
  assume "A"
  from \<open>A\<close> \<open>A\<close> show "A \<and> A" by (rule conjI)
qed

(* Elimination rules *)
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume AB : "A \<and> B"
  show "B \<and> A"
  proof (rule conjE[OF AB])
    assume "A" "B"
    from \<open>B\<close> \<open>A\<close> show ?thesis by (rule conjI)
  qed
qed

(*
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume AB: "A \<and> B"
  from AB show "B \<and> A"
  proof
    assume "A" "B"
    show ?thesis ..
  qed
qed
*)

(*
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume "A \<and> B"
  from this show "B \<and> A"
  proof
    assume "A" "B"
    show ?thesis ..
  qed
qed
*)

(*
?thesis always stands for the "current goal"
*)

(* an alternative proff that operates purely by forward reasoning:*)
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume ab : "A \<and> B"
  from ab have a: "A" ..
  from ab have b: "B" ..
  from b a show "B \<and> A" ..
qed

(* with details*)
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof (rule impI)
  assume ab : "A \<and> B"
  from ab have a: "A" by (rule conjE)
  from ab have b: "B" by (rule conjE)
  from b a show "B \<and> A" by (rule conjI)
qed

lemma "\<not>(A \<or> B) \<longrightarrow> \<not>A \<or> \<not>B"
proof (rule impI)
  assume "\<not>(A \<or> B)"
  have "\<not>A"
  proof (rule notI)
    assume A
    from this have "A \<or> B" by (rule disjI1)
    from \<open>\<not>(A \<or> B)\<close> \<open>A \<or> B\<close> show False by (rule notE)
  qed
  from \<open>\<not>A\<close> show "\<not>A \<or> \<not>B" by (rule disjI1)
qed

lemma "\<not>(A \<and> B) \<longrightarrow> \<not>A \<or> \<not>B"
proof
  (* \<turnstile> A \<or> \<not>A *)
  have "A \<or> \<not>A"
  proof (rule ccontr)
    assume "\<not>(A \<or> \<not>A)"
    have "\<not>A"    (*   ! ! on ne peut pas utiliser from this have "\<not>A" car proof (rule notI)  *)
    proof (rule notI)
      assume "A"
      from this have "A \<or> \<not>A" by (rule disjI1)
      from \<open>\<not>(A \<or> \<not>A)\<close> \<open>A \<or> \<not>A\<close> show False by (rule notE)
    qed
    from \<open>\<not>A\<close> have "A \<or> \<not>A" by (rule disjI2)
    from \<open>\<not>(A \<or> \<not>A)\<close> \<open>A \<or> \<not>A\<close> show False by (rule notE)
  qed

  (* \<turnstile> A \<or> \<not>A   \<not>(A \<and> B), A \<turnstile> \<not>A \<or> \<not>B    \<not>(A \<and> B), B \<turnstile> \<not>A \<or> \<not>B
    -----------------------------------------
         \<not>(A \<and> B) \<turnstile> \<not>A \<or> \<not>B  *)
  assume "\<not>(A \<and> B)"
  from \<open>A \<or> \<not>A\<close> show "\<not>A \<or> \<not>B"
  proof (rule disjE)
    assume "A"
    have "\<not>B"
    proof (rule notI)
      assume "B"
      from \<open>A\<close> \<open>B\<close> have "A \<and> B" by (rule conjI)
      from \<open>\<not>(A \<and> B)\<close> \<open>A \<and> B\<close> show False by (rule notE)
    qed
    from \<open>\<not>B\<close> show ?thesis by (rule disjI2)
  next
    assume "\<not>A"
    from this show ?thesis by (rule disjI1)
  qed
qed

lemma "\<not>(A \<and> B) \<longrightarrow> \<not>A \<or> \<not>B"
proof (rule impI)
  assume H1 : "\<not>(A \<and> B)"
  show "\<not>A \<or> \<not>B"
  proof (rule ccontr)
    assume H2 : "\<not>(\<not>A \<or> \<not>B)"
    have "\<not>A"
    proof (rule notI)
      assume "A"
      have "\<not>B"
      proof (rule notI)
        assume "B"
        from \<open>A\<close> \<open>B\<close> have not_H1 : "A \<and> B" by (rule conjI)
        from H1 not_H1 show False by (rule notE)
      qed
      from \<open>\<not>B\<close> have not_H2 : "\<not>A \<or> \<not>B" by (rule disjI2)
      from H2 not_H2 show False by (rule notE)
    qed
    from \<open>\<not>A\<close> have not_H2_2 : "\<not>A \<or> \<not>B" by (rule disjI1)
    from H2 not_H2_2 show False by (rule notE)
  qed
qed

lemma "\<not>(A \<and> B) \<longrightarrow> \<not>A \<or> \<not>B"
proof (rule impI)
  assume H1 : "\<not>(A \<and> B)"
  show "\<not>A \<or> \<not>B"
  proof (rule ccontr)
    assume H2 : "\<not>(\<not>A \<or> \<not>B)"
    have "\<not>A"
    proof (rule notI)
      assume "A"
      have "\<not>B"
      proof (rule notI)
        assume "B"
        with \<open>A\<close> have "A \<and> B" by (rule conjI)   (*   with facts = from facts this  *)
        with H1 show False by (rule notE)
      qed
      then have not_H2 : "\<not>A \<or> \<not>B" by (rule disjI2)
      with H2 show False by (rule notE)
    qed
    then have not_H2_2 : "\<not>A \<or> \<not>B" by (rule disjI1)
    with H2 show False by (rule notE)
  qed
qed

lemma "A \<and> B \<Longrightarrow> B \<and> A"
proof (rule conjI)
  assume "A \<and> B" thus "B" by (rule conjE)  (* thus = then show = from this show *)
next
  assume "A \<and> B" thus "A" by (rule conjE)
qed

lemma "large_A \<and> large_B \<Longrightarrow> large_B \<and> large_A"
      (is "?AB \<Longrightarrow> ?B \<and> ?A")
proof (rule conjI)
  assume "?AB" thus "?B" by (rule conjE)
next
  assume "?AB" thus "?A" by (rule conjE)
qed

lemma
  assumes AB : "large_A \<and> large_B"
  shows "large_B \<and> large_A" (is "?B \<and> ?A")
proof (rule conjI)
  from AB show "?B" by (rule conjE)
next
  from AB show "?A" by (rule conjE)
qed

lemma
  assumes AB : "large_A \<and> large_B"
  shows "large_B \<and> large_A" (is "?B \<and> ?A")
  using AB
proof
  assume "?B" "?A" thus ?thesis by (rule conjI)
qed

lemma
  assumes AB : "A \<or> B"
  shows "B \<or> A"
proof-
  from AB show ?thesis
  proof (rule disjE)
    assume "A"
    then show ?thesis by (rule disjI2) (* then = from this *)
  next
    assume "B"
    then show ?thesis by (rule disjI1) (* then = from this *)
  qed
qed

(* section 2.4 Predicate calculus *)
lemma
  assumes P : "\<forall>x. P x"
  shows "\<forall>x. P (f x)"
proof (rule allI)
  fix x
  from P show "P (f x)" by (rule allE)
qed

lemma
  assumes Pf : "\<exists>x. P(f x)"
  shows "\<exists>y. P y"
proof -
  show ?thesis using Pf
  (* = from Pf show ?thesis *)
  proof (rule exE)
    fix x
    assume "P (f x)"
    then show ?thesis by (rule exI)
  qed
qed

lemma assumes Pf : "\<exists>x. P (f x)" shows "\<exists>y. P y"
proof -
  from Pf obtain x where "P (f x)" by (rule exE)
  thus ?thesis by (rule exI)
qed

(* a tautology *)
lemma
  assumes ex : "\<exists>x. \<forall>y. P x y"
  shows "\<forall>y. \<exists>x. P x y"
proof-
  from ex show ?thesis
  proof (rule exE)
    fix x
    assume "\<forall>y. P x y"
    show ?thesis
    proof (rule allI)
      fix y
      from \<open>\<forall>y. P x y\<close> have "P x y" by (rule allE)
      then show "\<exists>x. P x y" by (rule exI)
    qed
  qed
qed

lemma
  assumes ex : "\<exists>x. \<forall>y. P x y"
  shows "\<forall>y. \<exists>x. P x y"
proof(rule allI)
  from ex obtain x where "\<forall>y. P x y" by (rule exE)
  fix y
  from \<open>\<forall>y. P x y\<close> have "P x y" by (rule allE)
  then show "\<exists>x. P x y" by (rule exI)
qed

(* section 2.5 Making bigger steps *)
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
proof
  let ?S = "{ x. x \<notin> f x }"
  show "?S \<notin> range f "
  proof
    assume "?S \<in> range f"
    then obtain y where fy: "?S = f y" ..
    show False
    proof cases
      assume "y \<in> ?S"
      hence "y \<notin> f y" by simp
      hence "y \<notin> ?S" by (simp add:fy)
(*      from \<open>y \<in> ?S\<close>  \<open>y \<notin> ?S\<close> show False by autod*)
    from \<open>y \<in> ?S\<close>  \<open>y \<notin> ?S\<close> show False by contradiction
    next
      assume "y \<notin> ?S"
      hence "y \<in> f y" by simp
      hence "y \<in> ?S" by (simp add:fy)
(*      from \<open>y \<in> ?S\<close>  \<open>y \<notin> ?S\<close> show False by autod*)
    from \<open>y \<in> ?S\<close>  \<open>y \<notin> ?S\<close> show False by contradiction
    qed
  qed
qed

theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
  by best

lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
proof -
  { fix x y
    assume "A x y" "B x y"
    have "C x y" sorry}
  thus ?thesis by blast
qed

(* section 2.6 *)
(* Combining proof styles *)
lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
proof (rule impI)
  assume "A"
  show "(A \<longrightarrow> B) \<longrightarrow> B"
  proof (rule impI)
    assume "A \<longrightarrow> B"
    have "B \<Longrightarrow> B" by blast
    from \<open>A \<longrightarrow>B\<close> \<open>A\<close> this show "B" by (rule impE)
  qed
qed

lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
proof (rule impI)
  assume a: "A"
  show "(A \<longrightarrow> B) \<longrightarrow> B"
    apply(rule impI)
    apply(erule impE)
    apply(rule a)
    apply assumption
    done
qed

lemma "\<not>A \<or> A"
proof cases
  assume "A" thus ?thesis by (rule disjI2)
next
  assume "\<not>A" thus ?thesis by (rule disjI1)
qed

lemma "\<not>A \<or> A"
proof (cases "A")
  case True thus ?thesis by (rule disjI2)
next
  case False thus ?thesis by (rule disjI1)
qed

lemma "length(tl xs) = length xs - 1"
proof (cases xs)
  case Nil thus ?thesis by simp
next
  case Cons thus ?thesis by simp
qed

lemma "length(tl xs) = length xs - 1"
proof (cases xs)
  assume Nil: "xs = []"
  from this show ?thesis by simp
next
  fix x xs'
  assume Cons: " xs = x # xs'"
  thus ?thesis by simp
qed

(* Section 3.2 Structural induction *)
lemma "2 * (\<Sum>i::nat = 0..n. i) = n * (n + 1)" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix n
  assume "?P n"
  from this show "?P (Suc n)" by simp
qed

lemma "2 * (\<Sum>i::nat = 0..n. i) = (n::nat) * (n + 1)" (is "?P n")
proof (induction n)
  show "?P 0" by simp
next
  fix n
  assume "?P n"
  thus "?P (Suc n)" by simp
qed

lemma "2 * (\<Sum>i::nat = 0 .. n. i) = (n::nat) * (n + 1)"
proof (induction n)
  case 0 show ?case by simp
next
  case Suc thus ?case by simp
qed

lemma
  fixes n::nat
  shows "n < n * n + 1"
proof (7657
  case 0 show ?case by simp
next
  case (Suc i) thus "Suc i < Suc i * Suc i + 1" by simp
qed

(* Section 3.3 Induction formulae involving \<And> or \<Longrightarrow> *)
lemma
  assumes A : "(\<And>(n::nat). (\<And>(m::nat). m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
  shows "P (n::nat)" (is "?Q n")
proof (rule A)
  show "\<And>m. m < n \<Longrightarrow> P m"
  proof (induct n)
    show "\<And>m. m < 0 \<Longrightarrow> P m"
    proof-
      fix m
      show "m < 0 \<Longrightarrow> P m"
      proof -
        assume "m < 0"
        from this show "P m" by simp
      qed
    qed
  next
    show "\<And>n m. \<lbrakk>\<And>m. m < n \<Longrightarrow> P m; m < Suc n\<rbrakk> \<Longrightarrow> P m"
    proof -
      fix n
      fix m
      show "\<lbrakk>\<And>m. m < n \<Longrightarrow> P m; m < Suc n\<rbrakk> \<Longrightarrow> P m"
      proof -
        assume IH : "\<And>k. k < n \<Longrightarrow> P k"
        and "m < Suc n"
        show "P m"
        proof cases
          assume "m = n"
          show "P m"
          proof -   (* passer par \<And>k. k < m \<Longrightarrow> P k  *)
            from A IH have "P n" by simp
            from this \<open>m = n\<close> show "P m" by simp
            (* ou
            { fix k
              assume "k < m"
              have "P k"
              proof-
                from \<open>k < m\<close> \<open>m = n\<close> have "k < n" by simp
                from this IH show "P k" by simp
              qed
            }
            from this have "\<And>k. k < m \<Longrightarrow> P k" by simp
            from A this show "P m" by simp
          qed  *)
          qed
        next
          assume "m \<noteq> n"
          from this \<open>m < Suc n\<close> have "m < n" by arith
          from this IH show "P m" by simp
        qed
      qed
    qed
  qed
qed

(* 3.4 reflexive transitive closure of a relation *)

consts rtc :: "(’a * ’a) set \<Rightarrow> (’a * ’a) set"
refl: "(x,x) \<in> r*"
step: "[ (x,y) \<in> r; (y,z) \<in> r* ] \<Longrightarrow> (x,z) \<in> r*"

  (* les example qui ne marchent pas *)

(*
lemma "A \<longrightarrow> A"
proof
  assume "A"
  show "A" .  (* ? *)
qed
*)
(*
lemma "A \<longrightarrow> A \<and> A"
proof
  assume "A"
  show "A \<and> A" by (rule conjI)
qed
*)

(*
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume AB: "A \<and> B"
  from AB show "B \<and> A"
  proof
    assume "A" "B"
    show ?thesis ..
  qed
qed
*)

(*
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
  assume "A \<and> B"
  from this show "B \<and> A"
  proof
    assume "A" "B"
    show ?thesis ..
  qed
qed
*)

end

author: Qdake