Skip to content

Add UNCURRY_EQ to AllCaseEqs, #1665

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
ordinarymath wants to merge 1 commit into
base: develop
Choose a base branch
from
Draft

Add UNCURRY_EQ to AllCaseEqs, #1665

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 2 additions & 0 deletions src/1/TypeBase.sig
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,8 @@ sig
val CaseEq : string -> thm
val CaseEqs : string list -> thm
val AllCaseEqs : unit -> thm
val add_CaseEqs : thm list -> unit
val add_CasePreds : thm list -> unit

val CasePred : string -> thm
val CasePreds : string list -> thm
Expand Down
9 changes: 7 additions & 2 deletions src/1/TypeBase.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -215,6 +215,8 @@ fun tyi_from_name s =

val CaseEq = TypeBasePure.case_eq_of o tyi_from_name
val CaseEqs = Drule.LIST_CONJ o map CaseEq
val additional_CaseEqs = ref ([]:thm list)
fun add_CaseEqs thms = ignore (additional_CaseEqs := thms @ (!additional_CaseEqs))
fun AllCaseEqs() =
let
fun foldthis(ty, tyi, acc) =
Expand All @@ -223,7 +225,7 @@ fun AllCaseEqs() =
| SOME th => if aconv (concl acc) boolSyntax.T then th
else CONJ th acc
in
TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())
CONJ (TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())) (Drule.LIST_CONJ (!additional_CaseEqs))
end

fun type_info_of ty = {case_def = case_def_of ty, nchotomy = nchotomy_of ty}
Expand All @@ -248,6 +250,9 @@ fun CasePred' tyinfo =
val CasePred = CasePred' o tyi_from_name

val CasePreds = Drule.LIST_CONJ o map CasePred
val additional_CasePreds = ref ([]:thm list)
fun add_CasePreds thms = ignore (additional_CasePreds := thms @ (!additional_CasePreds))

fun AllCasePreds() =
let
fun foldthis(ty, tyi, acc) =
Expand All @@ -256,7 +261,7 @@ fun AllCasePreds() =
| SOME th => if aconv (concl acc) boolSyntax.T then th
else CONJ th acc
in
TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())
CONJ (TypeBasePure.fold foldthis boolTheory.TRUTH (theTypeBase())) (Drule.LIST_CONJ (!additional_CasePreds))
end

(* ---------------------------------------------------------------------- *
Expand Down
7 changes: 7 additions & 0 deletions src/coretypes/pairScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -334,6 +334,13 @@ Proof
ASM_SIMP_TAC bool_ss [UNCURRY_DEF, PAIR_EQ]
QED

Theorem UNCURRY_PRED:
UNCURRY f x <=> ?a b. x = (a,b) /\ f a b
Proof
Q.SPEC_THEN ‘x’ STRIP_ASSUME_TAC pair_CASES >>
ASM_SIMP_TAC bool_ss [UNCURRY_DEF, PAIR_EQ]
QED

(* ------------------------------------------------------------------------- *)
(* pair_Axiom = |- !f. ?fn. !x y. fn (x,y) = f x y *)
(* ------------------------------------------------------------------------- *)
Expand Down
3 changes: 2 additions & 1 deletion src/coretypes/pairSimps.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,8 @@ open Lib Parse simpLib pairTheory PairedLambda;


val PAIR_ss = BasicProvers.thy_ssfrag "pair"

val _ = TypeBase.add_CaseEqs [UNCURRY_EQ]
val _ = TypeBase.add_CasePreds [UNCURRY_PRED]
val fvar = ``f:'a -> 'b -> bool``;
val paired_forall_ss =
conv_ss
Expand Down
Loading