Store higher-order case thm (disjunctive form) in TypeBase

This avoids generating it on the fly in AllCasePreds().

src/1/TypeBase.sml

@@ -70,6 +70,11 @@ val bool_info =
            case_def = boolTheory.bool_case_thm,
            nchotomy = boolTheory.BOOL_CASES_AX
          },
+       case_elim =
+         Prim_rec.prove_case_ho_elim_thm{
+           case_def = boolTheory.bool_case_thm,
+           nchotomy = boolTheory.BOOL_CASES_AX
+         },
        case_cong = boolTheory.COND_CONG,
        distinct = SOME (CONJUNCT1 boolTheory.BOOL_EQ_DISTINCT),
        nchotomy = boolTheory.BOOL_CASES_AX,
@@ -239,9 +244,7 @@ fun CasePred' tyinfo =
     let
       val id = mk_abs(mk_var ("x", bool), mk_var ("x", bool))
     in
-      {case_def = TypeBasePure.case_def_of tyinfo,
-       nchotomy = TypeBasePure.nchotomy_of tyinfo}
-      |> Prim_rec.prove_case_ho_elim_thm
+      case_elim_of tyinfo
       |> Drule.ISPEC id
       |> Conv.CONV_RULE (Conv.LHS_CONV Thm.BETA_CONV)
     end

src/1/TypeBasePure.sig

@@ -21,6 +21,7 @@ sig
          case_def  : thm,
          case_cong : thm,
          case_eq   : thm,
+         case_elim : thm,
          nchotomy  : thm,
          size      : (term * shared_thm) option,
          encode    : (term * shared_thm) option,
@@ -61,6 +62,7 @@ sig
    val case_cong_of    : tyinfo -> thm
    val case_def_of     : tyinfo -> thm
    val case_eq_of      : tyinfo -> thm
+   val case_elim_of    : tyinfo -> thm
    val nchotomy_of     : tyinfo -> thm
    val distinct_of     : tyinfo -> thm option
    val one_one_of      : tyinfo -> thm option

src/1/TypeBasePure.sml

@@ -32,6 +32,7 @@ datatype shared_thm
          case_def  : thm,
          case_cong : thm,
          case_eq   : thm,
+         case_elim : thm,
          nchotomy  : thm,
          size      : (term * shared_thm) option,
          encode    : (term * shared_thm) option,
@@ -57,6 +58,7 @@ type dtyinfo =
             induction    : shared_thm,
             case_def     : thm,
             case_eq      : thm,
+            case_elim    : thm,
             case_cong    : thm,
             nchotomy     : thm,
             case_const   : term,
@@ -75,35 +77,35 @@ type dtyinfo =
             extra        : ThyDataSexp.t list} ;
 
 open FunctionalRecordUpdate
-fun gcons_mkUp z = makeUpdate21 z
+fun gcons_mkUp z = makeUpdate22 z
 fun update_DTY z = let
-  fun from accessors axiom case_cong case_const case_def case_eq
+  fun from accessors axiom case_cong case_const case_def case_eq case_elim
            constructors destructors distinct encode extra fields induction lift
            nchotomy one_one recognizers simpls size ty updates =
     {accessors = accessors, axiom = axiom, case_cong = case_cong,
      case_const = case_const, case_def = case_def, case_eq = case_eq,
-     constructors = constructors, destructors = destructors,
-     distinct = distinct, encode = encode, extra = extra, fields = fields,
-     induction = induction, lift = lift, nchotomy = nchotomy,
-     one_one = one_one, recognizers = recognizers, simpls = simpls,
-     size = size, ty = ty, updates = updates}
+     case_elim = case_elim, constructors = constructors,
+     destructors = destructors, distinct = distinct, encode = encode,
+     extra = extra, fields = fields, induction = induction, lift = lift,
+     nchotomy = nchotomy, one_one = one_one, recognizers = recognizers,
+     simpls = simpls, size = size, ty = ty, updates = updates}
   (* fields in reverse order to above *)
   fun from' updates ty size simpls recognizers one_one nchotomy lift induction
-            fields extra encode distinct destructors constructors case_eq
-            case_def case_const case_cong axiom accessors =
+            fields extra encode distinct destructors constructors case_elim
+            case_eq case_def case_const case_cong axiom accessors =
     {accessors = accessors, axiom = axiom, case_cong = case_cong,
      case_const = case_const, case_def = case_def, case_eq = case_eq,
-     constructors = constructors, destructors = destructors,
+     case_elim = case_elim, constructors = constructors, destructors = destructors,
      distinct = distinct, encode = encode, extra = extra, fields = fields,
      induction = induction, lift = lift, nchotomy = nchotomy,
      one_one = one_one, recognizers = recognizers, simpls = simpls,
      size = size, ty = ty, updates = updates}
   (* first order *)
   fun to f {accessors, axiom, case_cong, case_const, case_def, case_eq,
-            constructors, destructors, distinct, encode, extra, fields,
+            case_elim, constructors, destructors, distinct, encode, extra, fields,
             induction, lift, nchotomy, one_one, recognizers, simpls, size, ty,
             updates} =
-    f accessors axiom case_cong case_const case_def case_eq
+    f accessors axiom case_cong case_const case_def case_eq case_elim
       constructors destructors distinct encode extra fields induction lift
       nchotomy one_one recognizers simpls size ty updates
 in
@@ -180,6 +182,10 @@ fun case_eq_of (DFACTS {case_eq, ...}) = case_eq
   | case_eq_of (NFACTS (ty,_)) =
        raise ERR "case_eq_of" (dollarty ty^" is not a datatype");
 
+fun case_elim_of (DFACTS {case_elim, ...}) = case_elim
+  | case_elim_of (NFACTS (ty,_)) =
+       raise ERR "case_elim_of" (dollarty ty^" is not a datatype");
+
 fun extra_of (DFACTS{extra,...}) = extra
   | extra_of (NFACTS(_, {extra,...})) = extra
 
@@ -357,7 +363,7 @@ val defn_const =
 
 fun mk_datatype_info_no_simpls rcd =
   let
-    val {ax,case_def,case_eq,case_cong,induction,
+    val {ax,case_def,case_eq,case_elim,case_cong,induction,
          nchotomy,size,encode,lift,one_one,
          fields, accessors, updates, distinct,
          destructors,recognizers} = rcd
@@ -371,6 +377,7 @@ fun mk_datatype_info_no_simpls rcd =
        case_const   = defn_const case_def,
        case_def     = case_def,
        case_eq      = case_eq,
+       case_elim    = case_elim,
        case_cong    = case_cong,
        induction    = induction,
        nchotomy     = nchotomy,
@@ -406,6 +413,8 @@ local fun mk_ti (n,ax,ind)
                       case_def=cdef,case_cong=ccong, nchotomy=nch,
                       case_eq =
                         prove_case_eq_thm {case_def = cdef, nchotomy = nch},
+                      case_elim =
+                        prove_case_ho_elim_thm {case_def = cdef, nchotomy = nch},
                       one_one=oo, distinct=d,size=NONE, encode=NONE,
                       lift=NONE, fields=[], accessors=[],updates=[],
                       recognizers=[],destructors=[]}
@@ -432,6 +441,8 @@ fun gen_datatype_info {ax, ind, case_defs} =
             case_def = cased1, case_cong = casec1, nchotomy = nch1,
             case_eq =
               prove_case_eq_thm {case_def = cased1, nchotomy = nch1},
+            case_elim =
+              prove_case_ho_elim_thm {case_def = cased1, nchotomy = nch1},
             size=NONE, encode=NONE, lift=NONE,
             fields=[], accessors=[],updates=[],
             one_one=hd one_ones, distinct=hd distincts,
@@ -466,7 +477,8 @@ fun pp_tyinfo tyi =
         let
           val {ty,constructors, case_const, case_def, case_cong, induction,
                nchotomy,one_one,distinct,simpls,size,encode,lift,axiom, case_eq,
-               fields, accessors, updates,recognizers,destructors,extra} = recd
+               case_elim, fields, accessors, updates,recognizers,destructors,extra}
+              = recd
           val ty_namestring = name_pair (ty_name_of d)
         in
           block CONSISTENT 0 (
@@ -529,6 +541,11 @@ fun pp_tyinfo tyi =
               pp_thm case_eq
             ) >> add_break(1,0) >>
 
+            block CONSISTENT 1 (
+              add_string "Case-const higher-order split:" >> add_break (1,0) >>
+              pp_thm case_elim
+            ) >> add_break(1,0) >>
+
             block CONSISTENT 1 (
               add_string "Extras: [" >> add_break(1,0) >>
               pr_list pp_sexp (add_string "," >> add_break(1,0)) extra >>
@@ -1071,6 +1088,7 @@ fun dtyiToSEXPs (dtyi : dtyinfo) =
     field "induction" (Thm (thm_of (#induction dtyi))) @
     field "case_def" (Thm (#case_def dtyi)) @
     field "case_eq" (Thm (#case_eq dtyi)) @
+    field "case_elim" (Thm (#case_elim dtyi)) @
     field "case_cong" (Thm (#case_cong dtyi)) @
     field "case_const" (Term (#case_const dtyi)) @
     field "constructors" (List (map Term (#constructors dtyi))) @
@@ -1136,6 +1154,7 @@ fun fromSEXP0 s =
               Sym "induction", Thm induction,
               Sym "case_def", Thm case_def,
               Sym "case_eq", Thm case_eq,
+              Sym "case_elim", Thm case_elim,
               Sym "case_cong", Thm case_cong,
               Sym "case_const", Term case_const,
               Sym "constructors", List clist,
@@ -1155,7 +1174,7 @@ fun fromSEXP0 s =
         (SOME (
             DFACTS {ty = typ, axiom = ORIG axiom, induction = ORIG induction,
                     case_def = case_def, case_eq = case_eq,
-                    case_cong = case_cong,
+                    case_elim = case_elim, case_cong = case_cong,
                     case_const = case_const,
                     constructors = H "constructors" (map tm) clist,
                     destructors = H "destructors" (map thm) dlist,

src/coalgebras/itreeScript.sml

@@ -322,6 +322,16 @@ Proof
   \\ fs [itree_CASE,itree_11,itree_distinct]
 QED
 
+Theorem itree_CASE_elim:
+  ∀f.
+  f(itree_CASE t ret div vis) <=>
+    (?r. t = Ret r /\ f(ret r)) \/
+    (t = Div /\ f(div)) \/
+    (?a g. t = Vis a g /\ f(vis a g))
+Proof
+  qspec_then `t` strip_assume_tac itree_cases \\ rw []
+  \\ fs [itree_CASE,itree_11,itree_distinct]
+QED
 
 (* itree unfold *)
 
@@ -559,6 +569,7 @@ val _ = TypeBase.export
       case_def = itree_CASE,
       case_cong = itree_CASE_cong,
       case_eq = itree_CASE_eq,
+      case_elim = itree_CASE_elim,
       nchotomy = itree_cases,
       size = NONE,
       encode = NONE,

src/coalgebras/itreeTauScript.sml

@@ -363,6 +363,16 @@ Proof
   \\ fs [itree_CASE,itree_11,itree_distinct]
 QED
 
+Theorem itree_CASE_elim:
+  ∀f.
+  f(itree_CASE t ret tau vis) <=>
+    (?r. t = Ret r /\ f(ret r)) \/
+    (?u. t = Tau u /\ f(tau u)) \/
+    (?a g. t = Vis a g /\ f(vis a g))
+Proof
+  qspec_then ‘t’ strip_assume_tac itree_cases \\ rw []
+  \\ fs [itree_CASE,itree_11,itree_distinct]
+QED
 
 (* itree unfold *)
 
@@ -573,6 +583,7 @@ val _ = TypeBase.export
       case_def = itree_CASE,
       case_cong = itree_CASE_cong,
       case_eq = itree_CASE_eq,
+      case_elim = itree_CASE_elim,
       nchotomy = itree_cases,
       size = NONE,
       encode = NONE,

src/coalgebras/llistScript.sml

@@ -2945,6 +2945,13 @@ Proof
   llist_CASE_TAC ``x:'a llist`` >> rw[]
 QED
 
+Theorem LLIST_CASE_ELIM:
+  ∀f'. f'(llist_CASE (x:'a llist) v f) <=>
+  x = [||] /\ f' v \/ ?a l. x = a:::l /\ f'(f a l)
+Proof
+  llist_CASE_TAC ``x:'a llist`` >> rw[FUN_EQ_THM]
+QED
+
 Theorem LLIST_DISTINCT:
   !a1 a0. [||] <> a0:::a1
 Proof
@@ -2985,6 +2992,7 @@ val _ = TypeBase.export
      case_def = llist_CASE_compute,
      case_cong = LLIST_CASE_CONG,
      case_eq = LLIST_CASE_EQ,
+     case_elim = LLIST_CASE_ELIM,
      nchotomy = llist_CASES,
      size = NONE,
      encode = NONE,

src/coalgebras/ltreeScript.sml

@@ -264,6 +264,12 @@ Proof
   \\ fs [Branch_11,ltree_CASE]
 QED
 
+Theorem ltree_CASE_elim:
+  ∀f'. f'(ltree_CASE t f) <=> ?a ts. t = Branch a ts /\ f'(f a ts)
+Proof
+  qspec_then `t` strip_assume_tac ltree_cases \\ rw []
+  \\ fs [Branch_11,ltree_CASE]
+QED
 
 (* ltree generator *)
 
@@ -642,6 +648,7 @@ val _ = TypeBase.export
       case_def = ltree_CASE,
       case_cong = ltree_CASE_cong,
       case_eq = ltree_CASE_eq,
+      case_elim = ltree_CASE_elim,
       nchotomy = ltree_cases,
       size = NONE,
       encode = NONE,

src/coretypes/pairScript.sml

@@ -569,12 +569,20 @@ val pair_case_eq = Q.store_thm(
   Q.ISPEC_THEN ‘p’ STRUCT_CASES_TAC pair_CASES THEN
   SRW_TAC[][pair_CASE_def, FST, SND, PAIR_EQ]);
 
+val pair_case_ho_elim = Q.store_thm(
+  "pair_case_ho_elim",
+  ‘!f'. f'(pair_CASE p f) = (?x y. p = (x,y) /\ f'(f x y))’,
+  strip_tac THEN
+  Q.ISPEC_THEN ‘p’ STRUCT_CASES_TAC pair_CASES THEN
+  SRW_TAC[][pair_CASE_def, FST, SND, PAIR_EQ]);
+
 val _ = TypeBase.export [
       TypeBasePure.mk_datatype_info_no_simpls {
         ax=TypeBasePure.ORIG pair_Axiom,
         case_def=pair_case_thm,
         case_cong=pair_case_cong,
         case_eq = pair_case_eq,
+        case_elim = pair_case_ho_elim,
         induction=TypeBasePure.ORIG pair_induction,
         nchotomy=ABS_PAIR_THM,
         size=NONE,

src/datatype/EnumType.sml

@@ -384,6 +384,8 @@ fun enum_type_to_tyinfo (ty, clist) = let
         case_cong = case_cong,
         case_eq =
           Prim_rec.prove_case_eq_thm{case_def = case_def, nchotomy = nchotomy},
+        case_elim =
+          Prim_rec.prove_case_ho_elim_thm{case_def = case_def, nchotomy = nchotomy},
         nchotomy = nchotomy,
         size = size,
         encode = NONE,