Skip to content

Implement case_constant #1484

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 3 commits into
base: develop
Choose a base branch
from
Draft

Implement case_constant #1484

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ffa1256
Get TypeBasePure working
ordinarymath May 4, 2025
13180fd
fix TypeBase
ordinarymath May 12, 2025
0d6d135
Get coretypes to build + fix Datatype
ordinarymath May 12, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/1/TypeBase.sig
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
48 changes: 25 additions & 23 deletions src/1/TypeBase.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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))


Expand Down
36 changes: 19 additions & 17 deletions src/1/TypeBasePure.sig
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading
Loading