How to define the range lemma like star in Isabelle entry · Beginner Questions

Based on the repositoy in AFP, I plan to extend the library of regexp in Isabelle. Here I try to prove the range regexp in below which is similay to star.

The index of star could start from zero(empty list) to infinite. The range starts from nat m to nat n. But I have no idea that figure out a solution like lemma in_star_iff_concat(i.e. use the list to denote the procedure).

type_synonym 'a lang = "'a list set"

definition conc :: "'a lang ⇒ 'a lang ⇒ 'a lang" (infixr "@@" 75) where
"A @@ B = {xs@ys | xs ys. xs:A & ys:B}"

overloading lang_pow == "compow :: nat ⇒ 'a lang ⇒ 'a lang"
begin
  primrec lang_pow :: "nat ⇒ 'a lang ⇒ 'a lang" where
  "lang_pow 0 A = {[]}" |
  "lang_pow (Suc n) A = A @@ (lang_pow n A)"
end

definition lang_pow :: "nat ⇒ 'a lang ⇒ 'a lang" where
  lang_pow_code_def [code_abbrev]: "lang_pow = compow"

lemma [code]:
  "lang_pow (Suc n) A = A @@ (lang_pow n A)"
  "lang_pow 0 A = {[]}"
  by (simp_all add: lang_pow_code_def)


definition star :: "'a lang ⇒ 'a lang" where
"star A = (⋃n. A ^^ n)"


definition range :: "'a lang ⇒ nat ⇒ nat => 'a lang " where
"range A m n= (⋃i∈{m..n}. A ^^ i)"


lemma concat_in_star: "set ws ⊆ A ⟹ concat ws : star A"
  by(induct ws) simp_all


lemma in_star_iff_concat:
  "w ∈ star A = (∃ws. set ws ⊆ A ∧ w = concat ws)"
  (is "_ = (∃ws. ?R w ws)")
proof
  assume "w : star A" thus "∃ws. ?R w ws"
  proof induct
    case Nil have "?R [] []" by simp
    thus ?case ..
  next
    case (append u v)
    then obtain ws where "set ws ⊆ A ∧ v = concat ws" by blast
    with append have "?R (u@v) (u#ws)" by auto
    thus ?case ..
  qed
next
  assume "∃us. ?R w us" thus "w : star A"
  by (auto simp: concat_in_star)
qed

lemma try_range :"w : range A m n = (...)"
sorry

Lukas Stevens (May 22 2023 at 12:57):

You could use drop and take or state that w' ∈ A and w' = as @ w @ bs and length as = n /\ length w = m - n

Lukas Stevens (May 22 2023 at 13:27):

More concretely, w ∈ range A n m ⟺ (∃w' ∈ A. w' = as @ w @ bs ∧ length as = n ∧ length w = m - n)

Mathias Fleury (May 22 2023 at 13:37):

Hongjian Jiang (May 22 2023 at 19:04):

Hongjian Jiang (May 22 2023 at 19:13):

Sorry for that I am new comer in Isabelle. What is w' used for? If there is complete proof, that will be better to understand.

Hongjian Jiang (May 22 2023 at 19:24):

I try to prove such lemma here:

lemma "w : range1 A m n = (∃ws. set ws ⊆ A ∧ w = concat ws ∧ length ws ≤ n ∧ length ws ≥ m)"
  (is "_ = (∃ws. ?R w ws)")

Hongjian Jiang (May 22 2023 at 19:26):

where ∃ws. set ws ⊆ A ∧ w = concat ws ∧ length ws ≤ n ∧ m ≤ length ws ⟹ w ∈ range1 A m n was proved by below,

lemma concat_Suc_contains:"concat ws ∈ range1 A m n ⟹ concat ws ∈ range1 A m (Suc n)"
  apply(induct ws)
  apply simp
   apply (meson element_range1 le_Suc_eq)
  apply simp
  by (meson element_range1 le_Suc_eq)

lemma concat_n_times:"set ws ⊆ A ⟹ concat ws ∈ A ^^ length ws"
  apply(induct ws)
   apply simp
  apply simp
  done

lemma concat_in_range1: "set ws ⊆ A ∧ length ws ≥ m ∧ length ws ≤ n ⟹ concat ws : range1 A m n"
  apply(induct n)
  subgoal
   apply simp
    using zero_range1_empty apply fastforce
    done
  apply(case_tac "length ws ≤ n")
  subgoal for n apply simp
    by(simp add:concat_Suc_contains)
  subgoal for n apply simp apply(case_tac "length ws = (Suc n)")
     prefer 2
    subgoal
      apply simp
      done
    subgoal apply simp
      by (metis dual_order.refl element_range1 concat_n_times)
  done
  done

But w ∈ range1 A m n ⟹ ∃ws. set ws ⊆ A ∧ w = concat ws ∧ length ws ≤ n ∧ m ≤ length ws was still stuck.

Mathias Fleury (May 22 2023 at 20:24):

I gave it a try, and there is no Isabelle problem here, just a "how do you do this on paper"?

Hongjian Jiang (May 22 2023 at 20:29):

I can't figure out the proof of w ∈ range1 A m n ⟹ ∃ws. set ws ⊆ A ∧ w = concat ws ∧ length ws ≤ n ∧ m ≤ length ws, maybe induct on w. I am still trying.

Hongjian Jiang (May 22 2023 at 20:41):

lemma zero_range1_empty:"[] ∈ range1 A 0 n"
  apply(simp add:range1_def)
  apply(induct n)
   apply simp
  apply auto
  done

lemma element_range1:"b :range1 A m n = (∃i. i ≥ m ∧ i ≤ n ∧ b : A ^^ i)"
  apply(simp add:range1_def)
  using atLeastAtMost_iff by blast

lemma concat_Suc_contains:"concat ws ∈ range1 A m n ⟹ concat ws ∈ range1 A m (Suc n)"
  apply(induct ws)
  apply simp
   apply (meson element_range1 le_Suc_eq)
  apply simp
  by (meson element_range1 le_Suc_eq)

lemma concat_n_times:"set ws ⊆ A ⟹ concat ws ∈ A ^^ length ws"
  apply(induct ws)
   apply simp
  by simp

lemma concat_in_range1: "set ws ⊆ A ∧ length ws ≥ m ∧ length ws ≤ n ⟹ concat ws : range1 A m n"
  apply(induct n)
  subgoal
   apply simp
    using zero_range1_empty by fastforce
  apply(case_tac "length ws ≤ n")
  subgoal for n apply simp
    by(simp add:concat_Suc_contains)
  subgoal for n
    apply simp apply(case_tac "length ws = (Suc n)")
     prefer 2
    subgoal
      by simp
    subgoal apply simp
      by (metis dual_order.refl element_range1 concat_n_times)
  done
  done

lemma non_range1[simp]:"range1 A 0 0 = {[]}"
  apply(simp add:range1_def)
  done

lemma conc_range1[simp]:"range1 A 0 (Suc n) =  (range1 A 0 n) ∪ A ^^ (Suc n)"
  apply (simp add:range1_def)
  by (simp add: atLeast0_atMost_Suc inf_sup_aci(5))

lemma in_range_iff_concat:"w : range1 A m n = (∃ws. set ws ⊆ A ∧ w = concat ws ∧ length ws ≤ n ∧ length ws ≥ m)"
  (is "_ = (∃ws. ?R w ws)")
proof
  assume "w : range1 A m n" thus "∃ws. ?R w ws"
    sorry
next
  assume "∃us. ?R w us" thus "w : range1 A m n"
    apply auto
    by(simp add:concat_in_range1)
qed

Mathias Fleury (May 23 2023 at 04:54):

Unfolding range1 gives you a p such that p \in A^^p and m <= p and p <= n. Induction on p makes a lot more sense…

Hongjian Jiang (May 23 2023 at 07:34):

Hongjian Jiang (May 23 2023 at 07:43):

Sorry for the noob, what about the lemma " w ∈ A ^^ x ==> ∃ws. set ws ⊆ A ∧ w = concat ws ∧ length ws = x", when induct on p. It's very crucial.

Stream: Beginner Questions

Topic: How to define the range lemma like star in Isabelle entry

Hongjian Jiang (May 21 2023 at 19:54):