SeLFiE: some supports to reason goals with let bindings

[yutakang]

@{term "let x = 1 in x"};
(*
  Const ("HOL.Let", "'a ⇒ ('a ⇒ 'a) ⇒ 'a")
$ Const ("Groups.one_class.one", "'a")
$ Abs   ("x", "'a", Bound 0): term
*)

@{term "let x = 1 + y in x"};
(*
  Const ("HOL.Let", "'a ⇒ ('a ⇒ 'a) ⇒ 'a")
$(  Const ("Groups.plus_class.plus", "'a ⇒ 'a ⇒ 'a")
  $ Const ("Groups.one_class.one", "'a")
  $ Free ("y", "'a")
 )
$ Abs   ("x", "'a", Bound 0)
*)

@{term "let x = True ∧ False in x"};
(*
val it = 
  Const ("HOL.Let", "bool ⇒ (bool ⇒ bool) ⇒ bool")
$ ( Const ("HOL.conj", "bool ⇒ bool ⇒ bool")
  $ Const ("HOL.True", "bool")
  $ Const ("HOL.False", "bool")
  )
$ Abs ("x", "bool", Bound 0): term
*)

@{term "let x = y in z"};
(*
  Const ("HOL.Let", "'a ⇒ ('a ⇒ 'b) ⇒ 'b")
$ Free ("y", "'a")
$ Abs ("x", "'a", Free ("z", "'b")): term
*)

Probably we can introduce a syntactic sugar With_Let_X_Be_Y_In_Z (x, y, z).

Such syntactic sugar would be useful in Nearest_Neighbor.ML.

[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]

Not perfect, but it is done in 5ca65dc68272ccef97d9a3486ba5c876c84e6fc5 for now.