diff --git a/src/1/TypeBase.sig b/src/1/TypeBase.sig index fd9fe81933..8c95b79532 100644 --- a/src/1/TypeBase.sig +++ b/src/1/TypeBase.sig @@ -31,6 +31,7 @@ sig val case_cong_of : hol_type -> thm val case_def_of : hol_type -> thm val case_eq_of : hol_type -> thm + val constant_case_of : hol_type -> thm val nchotomy_of : hol_type -> thm val distinct_of : hol_type -> thm val fields_of : hol_type -> (string * rcd_fieldinfo) list diff --git a/src/1/TypeBase.sml b/src/1/TypeBase.sml index d3083c5667..37deefddd2 100644 --- a/src/1/TypeBase.sml +++ b/src/1/TypeBase.sml @@ -71,6 +71,7 @@ val bool_info = case_def = boolTheory.bool_case_thm, nchotomy = boolTheory.BOOL_CASES_AX }, + constant_case = boolTheory.bool_case_CONST, case_cong = boolTheory.COND_CONG, distinct = SOME (CONJUNCT1 boolTheory.BOOL_EQ_DISTINCT), nchotomy = boolTheory.BOOL_CASES_AX, @@ -146,32 +147,33 @@ fun pfetch s ty = ("unable to find "^ Lib.quote (print_sp_type ty)^" in the TypeBase"); -fun axiom_of ty = TypeBasePure.axiom_of (pfetch "axiom_of" ty) -fun induction_of ty = TypeBasePure.induction_of (pfetch "induction_of" ty) -fun constructors_of ty = TypeBasePure.constructors_of (pfetch "constructors_of" ty) -fun destructors_of ty = TypeBasePure.destructors_of (pfetch "destructors_of" ty) -fun recognizers_of ty = TypeBasePure.recognizers_of (pfetch "recognizers_of" ty) -fun case_const_of ty = TypeBasePure.case_const_of (pfetch "case_const_of" ty) -fun case_cong_of ty = TypeBasePure.case_cong_of (pfetch "case_cong_of" ty) -fun case_def_of ty = TypeBasePure.case_def_of (pfetch "case_def_of" ty) -fun case_eq_of ty = TypeBasePure.case_eq_of (pfetch "case_eq_of" ty) -fun nchotomy_of ty = TypeBasePure.nchotomy_of (pfetch "nchotomy_of" ty) -fun fields_of ty = TypeBasePure.fields_of (pfetch "fields_of" ty) -fun accessors_of ty = TypeBasePure.accessors_of (pfetch "accessors_of" ty) -fun updates_of ty = TypeBasePure.updates_of (pfetch "updates_of" ty) -fun simpls_of ty = TypeBasePure.simpls_of (pfetch "simpls_of" ty) -fun axiom_of0 ty = TypeBasePure.axiom_of0 (pfetch "axiom_of" ty) -fun induction_of0 ty = TypeBasePure.induction_of0 (pfetch "induction_of0" ty) - -fun distinct_of ty = valOf2 ty "distinct_of" +fun axiom_of ty = TypeBasePure.axiom_of (pfetch "axiom_of" ty) +fun induction_of ty = TypeBasePure.induction_of (pfetch "induction_of" ty) +fun constructors_of ty = TypeBasePure.constructors_of (pfetch "constructors_of" ty) +fun destructors_of ty = TypeBasePure.destructors_of (pfetch "destructors_of" ty) +fun recognizers_of ty = TypeBasePure.recognizers_of (pfetch "recognizers_of" ty) +fun case_const_of ty = TypeBasePure.case_const_of (pfetch "case_const_of" ty) +fun case_cong_of ty = TypeBasePure.case_cong_of (pfetch "case_cong_of" ty) +fun case_def_of ty = TypeBasePure.case_def_of (pfetch "case_def_of" ty) +fun case_eq_of ty = TypeBasePure.case_eq_of (pfetch "case_eq_of" ty) +fun constant_case_of ty = TypeBasePure.constant_case_of (pfetch "case_eq_of" ty) +fun nchotomy_of ty = TypeBasePure.nchotomy_of (pfetch "nchotomy_of" ty) +fun fields_of ty = TypeBasePure.fields_of (pfetch "fields_of" ty) +fun accessors_of ty = TypeBasePure.accessors_of (pfetch "accessors_of" ty) +fun updates_of ty = TypeBasePure.updates_of (pfetch "updates_of" ty) +fun simpls_of ty = TypeBasePure.simpls_of (pfetch "simpls_of" ty) +fun axiom_of0 ty = TypeBasePure.axiom_of0 (pfetch "axiom_of" ty) +fun induction_of0 ty = TypeBasePure.induction_of0 (pfetch "induction_of0" ty) + +fun distinct_of ty = valOf2 ty "distinct_of" (TypeBasePure.distinct_of (pfetch "distinct_of" ty)) -fun one_one_of ty = valOf2 ty "one_one_of" +fun one_one_of ty = valOf2 ty "one_one_of" (TypeBasePure.one_one_of (pfetch "one_one_of" ty)) -fun size_of0 ty = TypeBasePure.size_of0 (pfetch "size_of0" ty) -fun encode_of0 ty = TypeBasePure.encode_of0 (pfetch "encode_of0" ty) -fun size_of ty = valOf2 ty "size_of" +fun size_of0 ty = TypeBasePure.size_of0 (pfetch "size_of0" ty) +fun encode_of0 ty = TypeBasePure.encode_of0 (pfetch "encode_of0" ty) +fun size_of ty = valOf2 ty "size_of" (TypeBasePure.size_of (pfetch "size_of" ty)) -fun encode_of ty = valOf2 ty "encode_of" +fun encode_of ty = valOf2 ty "encode_of" (TypeBasePure.encode_of (pfetch "encode_of" ty)) diff --git a/src/1/TypeBasePure.sig b/src/1/TypeBasePure.sig index 7b0a2e972a..c3aab7584d 100644 --- a/src/1/TypeBasePure.sig +++ b/src/1/TypeBasePure.sig @@ -16,23 +16,24 @@ sig datatype shared_thm = ORIG of thm | COPY of (string * string) * thm type mk_datatype_record = - {ax : shared_thm, - induction : 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, - lift : term option, - one_one : thm option, - distinct : thm option, - fields : (string * rcd_fieldinfo) list, - accessors : thm list, - updates : thm list, - destructors : thm list, - recognizers : thm list} + {ax : shared_thm, + induction : shared_thm, + case_def : thm, + case_cong : thm, + case_eq : thm, + case_elim : thm, + constant_case : thm, + nchotomy : thm, + size : (term * shared_thm) option, + encode : (term * shared_thm) option, + lift : term option, + one_one : thm option, + distinct : thm option, + fields : (string * rcd_fieldinfo) list, + accessors : thm list, + updates : thm list, + destructors : thm list, + recognizers : thm list} val mk_datatype_info_no_simpls : mk_datatype_record -> tyinfo val gen_std_rewrs : tyinfo -> thm list @@ -63,6 +64,7 @@ sig val case_def_of : tyinfo -> thm val case_eq_of : tyinfo -> thm val case_elim_of : tyinfo -> thm + val constant_case_of : tyinfo -> thm val nchotomy_of : tyinfo -> thm val distinct_of : tyinfo -> thm option val one_one_of : tyinfo -> thm option diff --git a/src/1/TypeBasePure.sml b/src/1/TypeBasePure.sml index 0e61f0cc51..7543e4bf23 100644 --- a/src/1/TypeBasePure.sml +++ b/src/1/TypeBasePure.sml @@ -27,23 +27,24 @@ datatype shared_thm | COPY of (string * string) * thm; type mk_datatype_record = - {ax : shared_thm, - induction : 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, - lift : term option, - one_one : thm option, - distinct : thm option, - fields : (string * rcd_fieldinfo) list, - accessors : thm list, - updates : thm list, - destructors : thm list, - recognizers : thm list} + {ax : shared_thm, + induction : shared_thm, + case_def : thm, + case_cong : thm, + case_eq : thm, + case_elim : thm, + constant_case : thm, + nchotomy : thm, + size : (term * shared_thm) option, + encode : (term * shared_thm) option, + lift : term option, + one_one : thm option, + distinct : thm option, + fields : (string * rcd_fieldinfo) list, + accessors : thm list, + updates : thm list, + destructors : thm list, + recognizers : thm list} fun thm_of (ORIG x) = x | thm_of (COPY (s,x)) = x; @@ -53,59 +54,61 @@ fun thm_of (ORIG x) = x (*---------------------------------------------------------------------------*) type dtyinfo = - {ty : hol_type, - axiom : shared_thm, - induction : shared_thm, - case_def : thm, - case_eq : thm, - case_elim : thm, - case_cong : thm, - nchotomy : thm, - case_const : term, - constructors : term list, - destructors : thm list, - recognizers : thm list, - size : (term * shared_thm) option, - encode : (term * shared_thm) option, - lift : term option, - distinct : thm option, - one_one : thm option, - fields : (string * rcd_fieldinfo) list, - accessors : thm list, - updates : thm list, - simpls : simpfrag, - extra : ThyDataSexp.t list} ; + {ty : hol_type, + axiom : shared_thm, + induction : shared_thm, + case_def : thm, + case_eq : thm, + case_elim : thm, + constant_case : thm, + case_cong : thm, + nchotomy : thm, + case_const : term, + constructors : term list, + destructors : thm list, + recognizers : thm list, + size : (term * shared_thm) option, + encode : (term * shared_thm) option, + lift : term option, + distinct : thm option, + one_one : thm option, + fields : (string * rcd_fieldinfo) list, + accessors : thm list, + updates : thm list, + simpls : simpfrag, + extra : ThyDataSexp.t list} ; open FunctionalRecordUpdate -fun gcons_mkUp z = makeUpdate22 z +fun gcons_mkUp z = makeUpdate23 z fun update_DTY z = let 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 = + constant_case 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, - case_elim = case_elim, constructors = constructors, + case_elim = case_elim, constant_case = constant_case, 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_elim - case_eq case_def case_const case_cong axiom accessors = + fields extra encode distinct destructors constructors constant_case + 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, - case_elim = case_elim, constructors = constructors, destructors = destructors, + case_elim = case_elim, constant_case = constant_case, + 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, - 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 case_elim + case_elim, constant_case, 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 case_elim constant_case constructors destructors distinct encode extra fields induction lift nchotomy one_one recognizers simpls size ty updates in @@ -186,6 +189,10 @@ 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 constant_case_of (DFACTS {constant_case, ...}) = constant_case + | constant_case_of (NFACTS (ty,_)) = + raise ERR "constant_case_of" (dollarty ty^" is not a datatype"); + fun extra_of (DFACTS{extra,...}) = extra | extra_of (NFACTS(_, {extra,...})) = extra @@ -363,42 +370,44 @@ val defn_const = fun mk_datatype_info_no_simpls rcd = let - val {ax,case_def,case_eq,case_elim,case_cong,induction, - nchotomy,size,encode,lift,one_one, - fields, accessors, updates, distinct, + val {ax,case_def,case_eq,case_elim,constant_case, + case_cong,induction,nchotomy,size,encode,lift, + one_one, fields, accessors, updates, distinct, destructors,recognizers} = rcd val (ty,ty_names,constructors) = basic_info case_def in DFACTS - {ty = ty, - constructors = constructors, - destructors = destructors, - recognizers = recognizers, - 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, - one_one = one_one, - distinct = distinct, - fields = fields, - accessors = accessors, - updates = updates, - simpls = {rewrs = [], convs = []}, - size = size, - encode = encode, - lift = lift, - axiom = ax, - extra = []} + {ty = ty, + constructors = constructors, + destructors = destructors, + recognizers = recognizers, + case_const = defn_const case_def, + case_def = case_def, + case_eq = case_eq, + case_elim = case_elim, + constant_case = constant_case, + case_cong = case_cong, + induction = induction, + nchotomy = nchotomy, + one_one = one_one, + distinct = distinct, + fields = fields, + accessors = accessors, + updates = updates, + simpls = {rewrs = [], convs = []}, + size = size, + encode = encode, + lift = lift, + axiom = ax, + extra = []} end fun gen_std_rewrs tyi = let val D = case distinct_of tyi of NONE => [] | SOME x => CONJUNCTS x val inj = case one_one_of tyi of NONE => [] | SOME th => [th] - val c = D @ map GSYM D @ inj + val const_case = [constant_case_of tyi] handle HOL_ERR _ => [] + val c = D @ map GSYM D @ inj @ const_case in case_def_of tyi :: c handle HOL_ERR _ => c end @@ -415,6 +424,8 @@ local fun mk_ti (n,ax,ind) prove_case_eq_thm {case_def = cdef, nchotomy = nch}, case_elim = prove_case_ho_elim_thm {case_def = cdef, nchotomy = nch}, + constant_case = + prove_case_const_thm {case_def = cdef, nchotomy = nch}, one_one=oo, distinct=d,size=NONE, encode=NONE, lift=NONE, fields=[], accessors=[],updates=[], recognizers=[],destructors=[]} @@ -443,6 +454,8 @@ fun gen_datatype_info {ax, ind, case_defs} = prove_case_eq_thm {case_def = cased1, nchotomy = nch1}, case_elim = prove_case_ho_elim_thm {case_def = cased1, nchotomy = nch1}, + constant_case = + prove_case_const_thm {case_def = cased1, nchotomy = nch1}, size=NONE, encode=NONE, lift=NONE, fields=[], accessors=[],updates=[], one_one=hd one_ones, distinct=hd distincts, @@ -477,7 +490,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, - case_elim, fields, accessors, updates,recognizers,destructors,extra} + case_elim,constant_case,fields, accessors, updates,recognizers, + destructors,extra} = recd val ty_namestring = name_pair (ty_name_of d) in @@ -546,6 +560,11 @@ fun pp_tyinfo tyi = pp_thm case_elim ) >> add_break(1,0) >> + block CONSISTENT 1 ( + add_string "Case-const constant case:" >> add_break (1,0) >> + pp_thm constant_case + ) >> 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 >> @@ -1089,6 +1108,7 @@ fun dtyiToSEXPs (dtyi : dtyinfo) = field "case_def" (Thm (#case_def dtyi)) @ field "case_eq" (Thm (#case_eq dtyi)) @ field "case_elim" (Thm (#case_elim dtyi)) @ + field "constant_case" (Thm (#constant_case dtyi)) @ field "case_cong" (Thm (#case_cong dtyi)) @ field "case_const" (Term (#case_const dtyi)) @ field "constructors" (List (map Term (#constructors dtyi))) @ @@ -1155,6 +1175,7 @@ fun fromSEXP0 s = Sym "case_def", Thm case_def, Sym "case_eq", Thm case_eq, Sym "case_elim", Thm case_elim, + Sym "constant_case", Thm constant_case, Sym "case_cong", Thm case_cong, Sym "case_const", Term case_const, Sym "constructors", List clist, @@ -1174,8 +1195,8 @@ fun fromSEXP0 s = (SOME ( DFACTS {ty = typ, axiom = ORIG axiom, induction = ORIG induction, case_def = case_def, case_eq = case_eq, - case_elim = case_elim, case_cong = case_cong, - case_const = case_const, + case_elim = case_elim, constant_case = constant_case, + case_cong = case_cong, case_const = case_const, constructors = H "constructors" (map tm) clist, destructors = H "destructors" (map thm) dlist, recognizers = H "recognizers" (map thm) rlist, diff --git a/src/coretypes/pairScript.sml b/src/coretypes/pairScript.sml index 8e9a0f1e2d..9d6e3ade2e 100644 --- a/src/coretypes/pairScript.sml +++ b/src/coretypes/pairScript.sml @@ -688,6 +688,10 @@ val pair_case_ho_elim = Q.store_thm( Q.ISPEC_THEN ‘p’ STRUCT_CASES_TAC pair_CASES THEN SRW_TAC[][pair_CASE_def, FST, SND, PAIR_EQ]); +Theorem pair_case_CONST = Prim_rec.prove_case_const_thm + { case_def = pair_case_thm, + nchotomy=ABS_PAIR_THM}; + val _ = TypeBase.export [ TypeBasePure.mk_datatype_info_no_simpls { ax=TypeBasePure.ORIG pair_Axiom, @@ -695,6 +699,7 @@ val _ = TypeBase.export [ case_cong=pair_case_cong, case_eq = pair_case_eq, case_elim = pair_case_ho_elim, + constant_case = pair_case_CONST, induction=TypeBasePure.ORIG pair_induction, nchotomy=ABS_PAIR_THM, size=NONE, diff --git a/src/datatype/Datatype.sml b/src/datatype/Datatype.sml index ab7c9ae7fe..d125058645 100644 --- a/src/datatype/Datatype.sml +++ b/src/datatype/Datatype.sml @@ -708,6 +708,7 @@ fun persistent_tyinfo tyinfos = save_thm(name "_induction", induction_of tyi); save_thm(name "_case_cong", case_cong_of tyi); save_thm(name "_case_eq", case_eq_of tyi); + save_thm(name "_case_CONST", constant_case_of tyi); () end in diff --git a/src/datatype/EnumType.sml b/src/datatype/EnumType.sml index 7fb2cee877..b877a32c01 100644 --- a/src/datatype/EnumType.sml +++ b/src/datatype/EnumType.sml @@ -387,6 +387,8 @@ fun enum_type_to_tyinfo (ty, clist) = let 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}, + constant_case = + Prim_rec.prove_case_const_thm{case_def = case_def, nchotomy = nchotomy}, nchotomy = nchotomy, size = size, encode = NONE,