How IsaPlanner "accidentally" proves rev l = qrev l [] with best-first rippling:

This has actually nothing to do with the relaxed restrictions of rippling, but 
seems to be a unexpected side effect of caching and the same-check that we 
carry out to prune the search space. 

The proof-attempt of the step case starts of as normal as ever:

(1) rev(a::l) = qrev (a::l) []
    by rev_cons:
(2) (rev l) @ [a] = qrev (a::l) []
    by qrev_cons:
(3) (rev l) @ [a] = qrev l (a::[])

which is blocked but can be weak-fertilised to:
qrev l [] @ [a] = qrev l [a]

and triggers and attempt to prove a lemma that will fail. At some point best-first
search decides it's better to go back to the beginning, where we could have applied
qrev_cons first to state (1) instead of rev_cons. This gives

(4) rev(a::l) = qrev l (a::[])

Now, trying to apply rev_cons secondly (which is in fact pointless as it is a 
symmetric branch) is stopped as this would give us an identical copy of state (3) 
again. This rewrite is pruned by the same-check, and as a result state (4) instead 
becomes blocked. IsaPlanner fires a critic that tries to simplify the blocked state 
getting:

(rev l) @ [a] = qrev l [a], which is generalised to 

rev b @ c = qrev b c

Just what we happen to need! This lemma can be proved as usual, applied to the RHS 
of (4), followed by rev_cons and we're done. Seems like this proof is a bit of a 
lucky accident. If I would have pruned the entire symmetric branch (which I maybe 
should have done) and not left a blocked state this proof would indeed need the 
generalisation critic.

Below is IsaPlanner's output for this proof:


----------------------------------------------------------------------------
  Full Isar Script:
----------------------------------------------------------------------------

lemma auto_lemma_1: "rev b @ c = qrev b c"
proof (induct' "b")
  fix x :: "'a List"
  show "rev [] @ x = qrev [] x"
  by (simp (no_asm))
next
  fix x :: "'a List" and ba :: "'a List" and a :: "'a"
  assume a1[rule_format]: "ALL x. rev ba @ x = qrev ba x"
  have a4: "rev ba @ [a] @ x = rev ba @ (a # x)"
    by (rule auto_lemma_2)
  from a4  have a3: "rev ba @ [a] @ x = qrev ba (a # x)"
    by (subst a1[symmetric])
  from a3  have a2: "rev (a # ba) @ x = qrev ba (a # x)"
    by (subst BestF_L.rev.rev_cons)
  from a2  show "rev (a # ba) @ x = qrev (a # ba) x"
  by (subst BestF_L.qrev.qrev_cons)
qed

lemma auto_lemma_2: "b @ [a] @ c = b @ (a # c)"
proof (induct' "b")
  fix xa :: "'a" and x :: "'a List"
  show "[] @ [xa] @ x = [] @ (xa # x)"
  by (simp (no_asm))
next
  fix xa :: "'a" and x :: "'a List" and ba :: "'a List" and aa :: "'a"
  assume a2[rule_format]: "ALL x xa. ba @ [xa] @ x = ba @ (xa # x)"
  have a6: "aa # ba @ (xa # x) = (aa # ba) @ (xa # x)"
    by (simp (no_asm))
  from a6  have a5: "aa # ba @ [xa] @ x = (aa # ba) @ (xa # x)"
    by (subst a2)
  from a5  have a4: "aa # ba @ [xa] @ x = aa # ba @ (xa # x)"
    by (subst BestF_L.append.append_cons[symmetric])
  from a4  have a3: "(aa # ba @ [xa]) @ x = aa # ba @ (xa # x)"
    by (subst BestF_L.append.append_cons)
  from a3  have a2: "(aa # ba) @ [xa] @ x = aa # ba @ (xa # x)"
    by (subst BestF_L.append.append_cons)
  from a2  show "(aa # ba) @ [xa] @ x = (aa # ba) @ (xa # x)"
  by (subst BestF_L.append.append_cons)
qed

theorem "rev l = qrev l []"
proof (induct' "l")
  show "rev [] = qrev [] []"
  by (simp (no_asm))
next
  fix la :: "'a List" and a :: "'a"
  assume a[rule_format]: "rev la = qrev la []"
  have a3: "rev la @ [a] = qrev la [a]"
    by (rule auto_lemma_1)
  from a3  have a2: "rev (a # la) = qrev la [a]"
    by (simp (no_asm))
  from a2  show "rev (a # la) = qrev (a # la) []"
  by (subst BestF_L.qrev.qrev_cons)
qed
----------------------------------------------------------------------------


----------------------------------------------------------------------------
  Conjectures attempted:
----------------------------------------------------------------------------
Proved Lemmas: 
  auto_lemma_1: "rev ?b @ ?c = qrev ?b ?c"
  auto_lemma_2: "?b @ [?a] @ ?c = ?b @ (?a # ?c)"
 
Unprovable conjectures: 
  qrev ?b [] @ ?c = qrev ?b ?c
  qrev ?b [?a] @ ?c = qrev ?b [] @ (?a # ?c)
  qrev ?b [?a] @ ?c = qrev ?b (?a # ?c)
 
Non-theorems (false conjectures): 
  
----------------------------------------------------------------------------
 

----------------------------------------------------------------------------
  Full Hierarchical Proof Plan:
----------------------------------------------------------------------------
+[1] Solve using Induction, Bf-Rippling, and Conjecturing....
  +[1] induct' "l"...
    -[1] Solve the base case by simplification.
    +[1] Solve the step case using rippling....
      -[1] Start Rippling with state: 
           measure: 4
           aterm: rev [< op # a__ >] la__ = qrev [< op # a__ >] la__ []
      -[1] Ripple Step by subst BestF_L.qrev.qrev_cons
           rev (a__ # la__) = qrev la__ [a__]
           measure: 4
           aterm: rev [< op # a__ >] la__ = qrev la__ [< op # a__ >] []
      -[1] end rippling
      -[1] simp (no_asm)
    +[1] Proving the lemma: "rev b @ c = qrev b c"...
      +[1] Solve using Induction, Bf-Rippling, and Conjecturing....
        +[1] induct' "b"...
          -[1] Solve the base case by simplification.
          +[1] Solve the step case using rippling....
            -[1] Start Rippling with state: 
                 measure: 5
                 aterm: rev [< op # a__ >] ba__ @ \x__/ = qrev [< op # a__ >] ba__ \x__/
            -[1] Ripple Step by subst BestF_L.qrev.qrev_cons
                 rev (a__ # ba__) @ x__ = qrev ba__ (a__ # x__)
                 measure: 3
                 aterm: rev [< op # a__ >] ba__ @ \x__/ = qrev ba__ \a__ # x__/
            -[4] Ripple Step by subst BestF_L.rev.rev_cons
                 rev ba__ @ [a__] @ x__ = qrev ba__ (a__ # x__)
                 measure: 2
                 aterm: [< op @ >] (rev ba__) [< [a__] >] @ \x__/ = qrev ba__ \a__ # x__/
            -[1] end rippling
            -[2] Weak fertilisation
            -[1] Step case stuck
          +[1] Proving the lemma: "b @ [a] @ c = b @ (a # c)"...
            +[1] Solve using Induction, Bf-Rippling, and Conjecturing....
              +[1] induct' "b"...
                -[1] Solve the base case by simplification.
                +[1] Solve the step case using rippling....
                  -[1] Start Rippling with state: 
                       measure: 5
                       aterm: [< op # aa__ >] ba__ @ [\xa__/] @ \x__/ = [< op # aa__ >] ba__ @ (\xa__/ # \x__/)
                  -[1] Ripple Step by subst BestF_L.append.append_cons
                       (aa__ # ba__) @ [xa__] @ x__ = aa__ # ba__ @ (xa__ # x__)
                       measure: 4
                       aterm: [< op # aa__ >] ba__ @ [\xa__/] @ \x__/ = [< op # aa__ >] (ba__ @ (\xa__/ # \x__/))
                  -[1] Ripple Step by subst BestF_L.append.append_cons
                       (aa__ # ba__ @ [xa__]) @ x__ = aa__ # ba__ @ (xa__ # x__)
                       measure: 3
                       aterm: [< op # aa__ >] (ba__ @ [\xa__/]) @ \x__/ = [< op # aa__ >] (ba__ @ (\xa__/ # \x__/))
                  -[1] Ripple Step by subst BestF_L.append.append_cons
                       aa__ # ba__ @ [xa__] @ x__ = aa__ # ba__ @ (xa__ # x__)
                       measure: 2
                       aterm: [< op # aa__ >] (ba__ @ [\xa__/] @ \x__/) = [< op # aa__ >] (ba__ @ (\xa__/ # \x__/))
                  -[1] Ripple Step by subst BestF_L.append.append_cons[symmetric]
                       aa__ # ba__ @ [xa__] @ x__ = (aa__ # ba__) @ (xa__ # x__)
                       measure: 3
                       aterm: [< op # aa__ >] (ba__ @ [\xa__/] @ \x__/) = [< op # aa__ >] ba__ @ (\xa__/ # \x__/)
                  -[1] end rippling
                  -[1] Weak fertilisation
                  -[1] simp (no_asm)
                -[1] Qed
          -[1] rule auto_lemma_2
          -[1] Qed
    -[1] rule auto_lemma_1
    -[1] Qed
----------------------------------------------------------------------------