SeLFiE: some supports to reason goals with case distinctions

[yutakang]

@{term "case x of [] => y | w#ws ⇒ z"};
(*
  Const ("List.list.case_list", "'a ⇒ ('b ⇒ 'b list ⇒ 'a) ⇒ 'b list ⇒ 'a")
$ Free  ("y", "'a")
$ Abs   ("w", "'b", Abs ("ws", "'b list", Free ("z", "'a")))
$ Free  ("x", "'b list"):
*)

@{term "case x of [] => y | w#ws ⇒ w"};
(*
  Const ("List.list.case_list", "'a ⇒ ('a ⇒ 'a list ⇒ 'a) ⇒ 'a list ⇒ 'a")
$ Free  ("y", "'a")
$ Abs   ("w", "'a", Abs ("ws", "'a list", Bound 1))
$ Free  ("x", "'a list")
*)

@{term "case x of True => y | _ ⇒ z"}
(*
  Const ("Product_Type.bool.case_bool", "'a ⇒ 'a ⇒ bool ⇒ 'a")
$ Free  ("y", "'a")
$ Free  ("z", "'a")
$ Free  ("x", "bool")
*)

Probably we need a new language construct that takes a term (e.g. List.list.case_list) and tells us how many cases we should expect for this term (e.g. 2).

[yutakang]

So, probably we should tag each term or term occurrence with the number possible alternative cases: int option in Unique_Node.

[yutakang]

Na.. we already have Takes_N_Arguments and a case distinction in Isabelle/HOL is a function application.

So, we can just apply Takes_N_Arguments to, for example, List.list.case_list.

Maybe we need Takes_N_Minus_One_Arguments.

[yutakang]

Note that the bound term can be of a product type:

@{term "let (x1,  x2,  x3) = y in z"};
val it =
   Const ("HOL.Let", "'a × 'b × 'c ⇒ ('a × 'b × 'c ⇒ 'd) ⇒ 'd") $ Free ("y", "'a × 'b × 'c") $
     (Const ("Product_Type.prod.case_prod", "('a ⇒ 'b × 'c ⇒ 'd) ⇒ 'a × 'b × 'c ⇒ 'd") $
       Abs ("x1", "'a",
         Const ("Product_Type.prod.case_prod", "('b ⇒ 'c ⇒ 'd) ⇒ 'b × 'c ⇒ 'd") $
           Abs ("x2", "'b", Abs ("x3", "'c", Free ("z", "'d"))))):
   term

[yutakang]

But it looks like only variables and contents of product types are permitted.

In that case, we can use the type of HOL.Let as a hint.

But still, we have to be able to talk about "how many Abs appears below/above this. Maybe recursion helps?

[yutakang]

Another problem is that x in let x = y in z is not really a term, but a string in Abs ("x", "'a", Free ("z", "'b")).

x may appear as a bound variable Bound n, though.

[yutakang]

Probably we need more supports to deal with Abs and Bound

For example, Bound_Is_Introduced_By_Let (x), for which probably we have the same problem: we have to be able to talk about "how many Abs appears below/above this. Maybe recursion helps?

[yutakang]

We need an atomic assertion to detect case_

[yutakang]

done in 1f0001f10b2abf08745eba27e3195f823c0b272a.