Search code examples
isabelleproof

Reasoning about overlapping inductive definitions in Isabelle


I would like to prove the following lemma in Isabelle:

lemma "T (Open # xs) ⟹ ¬ S (Open # xs) ⟹ count xs Close ≤ count xs Open"

Please find the definitions below:

datatype paren = Open | Close

inductive S where
  S_empty: "S []" |
  S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
  S_paren: "S xs ⟹ S (Open # xs @ [Close])"

inductive T where
  T_S: "T []" |
  T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
  T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
  T_left: "T xs ⟹ T (Open # xs)"

The lemma states that an unbalanced parentheses structure would result in a possibly unbalanced structure when removing an Open bracket.

I've been trying the techniques that are described in the book "A proof-assistant for Higher-order logic", but so far none of them work. In particular, I tried to use rule inversion and rule induction, sledgehammer and other techniques.

One of the problems is that I haven't yet learned about Isar proofs, which thus complicates the proof. I would prefer if you can orient me with plain apply commands.


Solution

  • Please find a proof below. It is not unlikely that it can be improved: I tried to follow the simplest route towards the proof and relied on sledgehammer to fill in the details.

    theory so_raoidii
    imports  Complex_Main
    
    begin
    
    datatype paren = Open | Close
    
    inductive S where
      S_empty: "S []" |
      S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
      S_paren: "S xs ⟹ S (Open # xs @ [Close])"
    
    inductive T where
      T_S: "T []" |
      T_append: "T xs ⟹ T ys ⟹ T (xs @ ys)" |
      T_paren: "T xs ⟹ T (Open # xs @ [Close])" |
      T_left: "T xs ⟹ T (Open # xs)"
    
    lemma count_list_lem: 
      "count_list xsa a = n ⟹ 
      count_list ysa a = m ⟹ 
      count_list (xsa @ ysa) a = n + m"
      apply(induction xsa arbitrary: ysa n m)
      apply auto
      done
    
    lemma T_to_count: "T xs ⟹ count_list xs Close ≤ count_list xs Open"
      apply(induction rule: T.induct)
      by (simp add: count_list_lem)+
    
    lemma T_to_S_count: "T xs ⟹ count_list xs Close = count_list xs Open ⟹ S xs"
      apply(induction rule: T.induct)
      apply(auto)
      apply(simp add: S_empty)
      apply(metis S_append T_to_count add.commute add_le_cancel_right count_list_lem 
            dual_order.antisym)
      apply(simp add: count_list_lem S_paren)
      using T_to_count by fastforce
    
    lemma "T (Open # xs) ⟹ 
          ¬ S (Open # xs) ⟹ 
          count_list xs Close ≤ count_list xs Open"
      apply(cases "T xs")
      apply(simp add: T_to_count)
      using T_to_S_count T_to_count by fastforce
    
    end