Stream: Beginner Questions

Topic: refinement case assumotions in ISAP computation induction

view this post on Zulip Ruslan Shevchenko (Oct 29 2023 at 17:37):

Where are the refinement assumptions in the computation induction in structured ISAR proofs?

Let we have next minimum theory:

theory ComputationInductionExample
  imports Main
begin

datatype TpExpr = AnyTp
                 |
                  ScalarTp
                 |
                  ArrowTp TpExpr TpExpr
                 |
                  ErrorTp


fun isCorrect::"TpExpr ⇒ bool" where
  "isCorrect AnyTp = True"
| "isCorrect ScalarTp = True"
| "isCorrect (ArrowTp x y) =  ((isCorrect x)∧(isCorrect y))"
| "isCorrect ErrorTp = False"

fun lub::"TpExpr ⇒ TpExpr ⇒ TpExpr" where
  "lub ErrorTp y = ErrorTp"
| "lub x ErrorTp = ErrorTp"
| "lub (ArrowTp a1 b1) (ArrowTp a2 b2) = (
  if (isCorrect a1)∧(isCorrect b1)∧(isCorrect a2)∧(isCorrect b2)
  then (if (a1=a2) then (ArrowTp a1 (lub b1 b2)) else AnyTp)
  else AnyTp
 )"
| "lub (ArrowTp a1 b1) y = (if (isCorrect a1)∧(isCorrect b1) then AnyTp else ErrorTp)"
| "lub x (ArrowTp a2 b2) = (if (isCorrect a2)∧(isCorrect b2) then AnyTp else ErrorTp)"
| "lub ScalarTp ScalarTp = ScalarTp"
| "lub x y = AnyTp"

lemma lum_correct_forward: fixes x y :: TpExpr
  assumes "isCorrectTp x" and "isCorrectTp y"
  shows "isCorrectTp (lub x y)"
proof (induct x y  rule: lub.induct)
  case (1 y)
  then have "x=ErrorTp"
    (* where to get informatin that x=ErrorTp
       or that (isCorrectTp ErrorTp) is in assumptions
       for this case ?
    *)
    sorry
  thm lub.induct
  thm "1"
  thm "1.prems"
  (*  thm "1.IH". --  no IH. ?*)
  (*  thm "1.hyps"  --  no hyps ?*)
  thm assms
  thm this
next
  oops

end

I can't understand - when I am situated inside a case for computation induction, there somewhere should be information about the binding of x and y relative to the current case. (i.e. should be or. " x=ErrorTp". in context or "isCorrecctTp ErrorTp" in assms. But it is not. What I missing, and how to bind variables in assumptions with the current case?

Thanks!

view this post on Zulip Simon Roßkopf (Oct 29 2023 at 17:58):

Without trying to really understand your example: The "induct" proof method does not know about the assumptions of your lemma. If you add them explicitly and start your proof with using assms proof (induct x y rule: lub.induct) everything should work as expected

view this post on Zulip Ruslan Shevchenko (Oct 29 2023 at 18:07):

Thanks, it helped!

view this post on Zulip Wolfgang Jeltsch (Nov 17 2023 at 15:20):

Also note that using induction instead of induct gives you slightly nicer names for the case assumptions. See the Isabelle/Isar Reference Manual for details.

Last updated: Apr 27 2024 at 16:16 UTC