Select Git revision
FunctionFact.cs.meta
pvs.mmt 16.29 KiB
namespace http://pvs.csl.sri.com/
import lfx http://gl.mathhub.info/MMT/LFX
import prel http://pvs.csl.sri.com/prelude
import rules scala://pvs.mmt.kwarc.info
import lf scala://lf.mmt.kwarc.info
theory BoundInclude =
rule rules?BoundIncludeRule
parameter_binder # 1 binding 2,… ## 1 [ 2,… ]
theory PVS : lfx:/Subtyping?LFSubtyped =
include lfx:/Records?LFRecords
include ?BoundInclude
// PVS Types and expressions
tp : type
// unknown_type : tp
expr : tp → type # expr 1 -100 ## 1 prec -1
tpjudg : {A} expr A → tp → type # 2 $ 3 ## 2 : 3
subtpjudg : tp → tp → type # 1 *< 2 ## 1 <: 2 // = [A,B] {x:expr A} x $ B
powertp : tp → type # ℘ 1 = [A] ⟨ tp | ([x] x *< A) ⟩
powertpissub : {A,B: ℘ A} expr B <* expr A
// Literals
NatLit : tp
StringLit : tp
RatLit : tp
// tuple types
// TODO make this flexary
pvssigma : {A} (expr A → tp) → tp # Σ 2
tuple_tp : tp → tp → tp # 1 × 2 = [A][B] Σ [x:expr A]B
tuple_expr : {A,B} expr A → expr B → expr A × B # < 3 , 4 >
proj : {A,B} expr A → expr NatLit → expr B # 3 _ 4
// Function types
// TODO : Make this flexary
pvspi : {A} (expr A → tp) → tp # Π 2
fun_type : tp → tp → tp # 1 ⟹ 2 = [A,B] Π [x: expr A] B
pvsapply : {A,f : expr A → tp} expr (Π f) → {a:expr A} expr (f a) # 3 @ 4 ## 3 .( 4 ) prec 1000
lambda : {A,f : expr A → tp} ({a:expr A}expr (f a)) → expr (Π f) # λ 3
simplambda : {A,B,f: expr A → expr B}expr (A ⟹ B) = [A,B,f] PVS?lambda A ([x] B) f ## λ 3
simpapply : {A,B,f: expr (A ⟹ B)} expr A → expr B = [A,B,f] pvsapply A ([x] B) f ## 3 .( 4 )
// Booleans
bool : tp
boolean : tp = bool
FALSE : expr bool
TRUE: expr bool
NOT @ ¬ : expr (bool ⟹ bool)
// ¬ = NOT
AND @ & @ ∧ : expr (bool × bool) ⟹ bool # 1 ∧ 2 prec -10
// & = AND # 1 & 2 prec -10
// ∧ = AND # 1 ∧ 2 prec -10
OR @ ∨ : expr (bool × bool) ⟹ bool # 1 ∨ 2 prec -15
// ∨ = OR # 1 ∨ 2 prec -15
IMPLIES @ => @ ⇒ : expr (bool × bool) ⟹ bool # 1 ⇒ 2 prec -20
// => = IMPLIES # 1 => 2 prec -20
// ⇒ = IMPLIES # 1 ⇒ 2 prec -20
WHEN : expr (bool × bool) ⟹ bool # 1 WHEN 2 prec -20
IFF @ <=> @ ⇔ : expr (bool × bool) ⟹ bool # 1 ⇔ 2 prec -25
// <=> = IFF # 1 <=> 2 prec -25
// ⇔ = IFF # 1 ⇔ 2 prec -25
// Different kinds of formulas
formkind: type
assumption : formkind
axiom : formkind
challenge : formkind
claim : formkind
conjecture : formkind
corollary : formkind
fact : formkind
formula : formkind
law : formkind
lemma : formkind
obligation : formkind
postulate : formkind
proposition : formkind
sublemma : formkind
theorem : formkind
internal_judgment : formkind
proof : expr bool → type # ⊦ 1 prec -500 role Judgment
= : {A:tp} expr ((A × A) ⟹ bool) # 2 ≐ 3 role Eq
proof_of_TRUE : ⊦ TRUE
// Predicate for non-empty types
nonempty : tp → expr bool
is_nonempty : {A} expr A → ⊦ nonempty A
// Quantifiers
// TODO : Make this flexary
forall : {A} (expr A → expr bool) → expr bool # ∀ 2 ## FORALL 2
exists : {A} (expr A → expr bool) → expr bool # ∃ 2 ## EXISTS 2
// Auxiliary constructors
// TypeCast : {A,B,k,f} expr A → (k ⊦ f) → expr B
# 5 asInstanceOf 2 via 6
expr_as_type : {A}{B:tp} expr A → tp # ASTYPE 3 ## 3 = [A,B,e] B
recursor : {A} (expr A → expr A) → expr A ## INDUCTIVE 2
// Cases in matching
case : type
caselist # 1/…
match : {A,C} expr A → case → expr C ## 3 ⇒ 4
selbind # sel| V1T,… | 2 ## 2
selection : {A} expr A → case → case ## 2 : 3
// Records
rectp : {r : {' '} } tp ## 1
recordexpr : {r : {' '} } {' '} → expr (rectp r) ## 2
fieldapp # 1 .@ 2 ## 1 . 2
setsub : {A} (expr (A ⟹ bool)) → tp # ⟨ 1 | 2 ⟩
enumtype # 1|…
// update expressions
update # 1 with 2 ## 1 where 2
recupdate # 1 app 3,… as 2
funupdate # 1 is 2
tupleupdate # 1 to 2
type_extension : tp → tp → tp // record types only ? vectors/vectors_3D_def
// Rules
setsubispredsub1 : {A,e} expr (setsub A e) <* ⟨ (expr A) | ([x] ⊦ (e @ x)) ⟩
setsubispredsub2 : {A,e} ⟨ (expr A) | ([x] ⊦ (e @ x)) ⟩ <* expr (setsub A e)
setsubissub1 : {A,e} setsub A e *< A
setsubissub2 : {A,e} expr (setsub A e) <* expr A
subtpissubtype : {A:tp,B:tp} (A *< B) → ((expr A) <* (expr B))
subtprefl : {A} A *< A
pisubtp : {A,B}{f : expr A → tp,g: expr B → tp}{p: (expr B <* expr A)}
({x : expr B}(expr (f x) <* expr (g x))) →
Π f *< Π g
pisubtype : {A,B}{f : expr A → tp,g: expr B → tp}{p: (expr B <* expr A)}
({x : expr B}((f x) *< (g x))) →
(expr (Π f) <* expr (Π g))
= [A,B][f,g][p][F] subtpissubtype (Π f) (Π g)
(pisubtp A B f g p
([x] subtpissubtype (f x) (g x) (F x))
) role ForwardRule
sigmasubtp : {A,B}{f : expr A → tp,g: expr B → tp}{p: (expr A <* expr B)}
({x : expr A}(expr (f x) <* expr (g x))) →
Σ f *< Σ g
sigmasubtype : {A,B}{f : expr A → tp,g: expr B → tp}{p: (expr A <* expr B)}
({x : expr A}((f x) *< (g x))) →
(expr (Σ f) <* expr (Σ g))
= [A,B][f,g][p][F] subtpissubtype (Σ f) (Σ g)
(sigmasubtp A B f g p
([x] subtpissubtype (f x) (g x) (F x))
) role ForwardRule
rule lf?TermIrrelevanceRule (proof)
rule rules?NatLiterals
rule rules?StringLiterals
rule rules?RationalLiterals
rule rules?CurryingPiRule
rule rules?CurryingLambdaRule
// rule rules?CurryingRule
rule rules?CurryingEqualityPiRule
rule rules?CurryingEqualityLambdaRule
// rule rules?CurryingApplyRule
rule rules?NatLitSubtype
rule rules?PVSHOAS
rule rules?PVSNotation
// theory Prelude : ?PVS =
BoundInclude `prel:?transpose
BoundInclude `prel:?quantifier_props
BoundInclude `prel:?operator_defs
BoundInclude `prel:?numbers
BoundInclude `prel:?notequal
BoundInclude `prel:?if_def
BoundInclude `prel:?extend_bool
BoundInclude `prel:?equality_props
BoundInclude `prel:?equalities
BoundInclude `prel:?defined_types
BoundInclude `prel:?booleans
BoundInclude `prel:?boolean_props
BoundInclude `prel:?K_conversion
BoundInclude `prel:?K_props
BoundInclude `prel:?epsilons
BoundInclude `prel:?exists1
BoundInclude `prel:?functions
BoundInclude `prel:?function_inverse_def
BoundInclude `prel:?function_inverse
BoundInclude `prel:?functions_alt
BoundInclude `prel:?identity
BoundInclude `prel:?identity_props
BoundInclude `prel:?if_props
BoundInclude `prel:?number_fields
BoundInclude `prel:?relations
BoundInclude `prel:?orders
BoundInclude `prel:?measure_induction
BoundInclude `prel:?orders_alt
BoundInclude `prel:?reals
BoundInclude `prel:?extra_tegies
BoundInclude `prel:?rationals
BoundInclude `prel:?integers
BoundInclude `prel:?int_types
BoundInclude `prel:?bounded_int_inductions
BoundInclude `prel:?naturalnumbers
BoundInclude `prel:?nat_types
BoundInclude `prel:?euclidean_division
BoundInclude `prel:?empty_bv
BoundInclude `prel:?divides
BoundInclude `prel:?character
BoundInclude `prel:?bounded_nat_inductions
BoundInclude `prel:?bit
BoundInclude `prel:?bv
BoundInclude `prel:?bv_caret
BoundInclude `prel:?bv_concat_def
BoundInclude `prel:?bv_extend_defs
BoundInclude `prel:?nat_fun_props
BoundInclude `prel:?ordstruct_adt
BoundInclude `prel:?ordinals
BoundInclude `prel:?character_adt
BoundInclude `prel:?character_adt_reduce
BoundInclude `prel:?lex2
BoundInclude `prel:?lift_adt
BoundInclude `prel:?lift
BoundInclude `prel:?PartialFunctionDefinitions
BoundInclude `prel:?PartialFunctionComposition
BoundInclude `prel:?lift_adt_map
BoundInclude `prel:?lift_adt_reduce
BoundInclude `prel:?list_adt
BoundInclude `prel:?list
BoundInclude `prel:?list_adt_map
BoundInclude `prel:?list_adt_reduce
BoundInclude `prel:?list_props
BoundInclude `prel:?disjointness
BoundInclude `prel:?more_map_props
BoundInclude `prel:?ordstruct
BoundInclude `prel:?ordstruct_adt_reduce
BoundInclude `prel:?rational_props
BoundInclude `prel:?real_axioms
BoundInclude `prel:?real_types
BoundInclude `prel:?real_defs
BoundInclude `prel:?extra_real_props
BoundInclude `prel:?floor_ceil
BoundInclude `prel:?exponentiation
BoundInclude `prel:?exp2
BoundInclude `prel:?finite_sequences
BoundInclude `prel:?bv_nat
BoundInclude `prel:?bv_int_defs
BoundInclude `prel:?mod
BoundInclude `prel:?bv_arith_nat_defs
BoundInclude `prel:?bv_arithmetic_defs
BoundInclude `prel:?modulo_arithmetic
BoundInclude `prel:?list2finseq
BoundInclude `prel:?real_props
BoundInclude `prel:?restrict
BoundInclude `prel:?extend
BoundInclude `prel:?extend_props
BoundInclude `prel:?extend_func_props
BoundInclude `prel:?extend_order_props
BoundInclude `prel:?restrict_order_props
BoundInclude `prel:?restrict_props
BoundInclude `prel:?sequences
BoundInclude `prel:?seq_functions
BoundInclude `prel:?sets
BoundInclude `prel:?function_image
BoundInclude `prel:?function_inverse_alt
BoundInclude `prel:?function_props
BoundInclude `prel:?function_props2
BoundInclude `prel:?function_props_alt
BoundInclude `prel:?indexed_sets
BoundInclude `prel:?mucalculus
BoundInclude `prel:?ctlops
BoundInclude `prel:?fairctlops
BoundInclude `prel:?relation_defs
BoundInclude `prel:?relation_props
BoundInclude `prel:?relation_props2
BoundInclude `prel:?EquivalenceClosure
BoundInclude `prel:?QuotientDefinition
BoundInclude `prel:?bounded_real_defs
BoundInclude `prel:?bounded_real_defs_alt
BoundInclude `prel:?min_nat
BoundInclude `prel:?finite_sets
BoundInclude `prel:?function_image_aux
BoundInclude `prel:?function_iterate
BoundInclude `prel:?infinite_sets_def
BoundInclude `prel:?list2set
BoundInclude `prel:?filters
BoundInclude `prel:?Fairctlops
BoundInclude `prel:?more_finseq
BoundInclude `prel:?relation_converse_props
BoundInclude `prel:?KernelDefinition
BoundInclude `prel:?QuotientKernelProperties
BoundInclude `prel:?QuotientSubDefinition
BoundInclude `prel:?QuotientExtensionProperties
BoundInclude `prel:?QuotientDistributive
BoundInclude `prel:?QuotientIteration
BoundInclude `prel:?extend_set_props
BoundInclude `prel:?integer_props
BoundInclude `prel:?restrict_set_props
BoundInclude `prel:?map_props
BoundInclude `prel:?sets_lemmas
BoundInclude `prel:?finite_sets_of_sets
BoundInclude `prel:?stdlang
BoundInclude `prel:?strings
BoundInclude `prel:?stdexc
BoundInclude `prel:?stdcatch
BoundInclude `prel:?stdprog
BoundInclude `prel:?stdglobal
BoundInclude `prel:?stdpvs
BoundInclude `prel:?stdpvsio
BoundInclude `prel:?stdstr
BoundInclude `prel:?stdmath
BoundInclude `prel:?stdio
BoundInclude `prel:?stdfmap
BoundInclude `prel:?stdindent
BoundInclude `prel:?stdsys
BoundInclude `prel:?stdtokenizer
BoundInclude `prel:?subrange_inductions
BoundInclude `prel:?subrange_type
BoundInclude `prel:?union_adt
BoundInclude `prel:?union
BoundInclude `prel:?union_adt_map
BoundInclude `prel:?union_adt_reduce
BoundInclude `prel:?wf_induction
BoundInclude `prel:?xor_def
BoundInclude `prel:?bv_bitwise
theory Prelude : ?PVS =
include prel:?transpose
include prel:?quantifier_props
include prel:?operator_defs
include prel:?numbers
include prel:?notequal
include prel:?if_def
include prel:?extend_bool
include prel:?equality_props
include prel:?equalities
include prel:?defined_types
include prel:?booleans
include prel:?boolean_props
include prel:?K_conversion
include prel:?K_props
include prel:?epsilons
include prel:?exists1
include prel:?functions
include prel:?function_inverse_def
include prel:?function_inverse
include prel:?functions_alt
include prel:?identity
include prel:?identity_props
include prel:?if_props
include prel:?number_fields
include prel:?relations
include prel:?orders
include prel:?measure_induction
include prel:?orders_alt
include prel:?reals
include prel:?extra_tegies
include prel:?rationals
include prel:?integers
include prel:?int_types
include prel:?bounded_int_inductions
include prel:?naturalnumbers
include prel:?nat_types
include prel:?euclidean_division
include prel:?empty_bv
include prel:?divides
include prel:?character
include prel:?bounded_nat_inductions
include prel:?bit
include prel:?bv
include prel:?bv_caret
include prel:?bv_concat_def
include prel:?bv_extend_defs
include prel:?nat_fun_props
include prel:?ordstruct_adt
include prel:?ordinals
include prel:?character_adt
include prel:?character_adt_reduce
include prel:?lex2
include prel:?lift_adt
include prel:?lift
include prel:?PartialFunctionDefinitions
include prel:?PartialFunctionComposition
include prel:?lift_adt_map
include prel:?lift_adt_reduce
include prel:?list_adt
include prel:?list
include prel:?list_adt_map
include prel:?list_adt_reduce
include prel:?list_props
include prel:?disjointness
include prel:?more_map_props
include prel:?ordstruct
include prel:?ordstruct_adt_reduce
include prel:?rational_props
include prel:?real_axioms
include prel:?real_types
include prel:?real_defs
include prel:?extra_real_props
include prel:?floor_ceil
include prel:?exponentiation
include prel:?exp2
include prel:?finite_sequences
include prel:?bv_nat
include prel:?bv_int_defs
include prel:?mod
include prel:?bv_arith_nat_defs
include prel:?bv_arithmetic_defs
include prel:?modulo_arithmetic
include prel:?list2finseq
include prel:?real_props
include prel:?restrict
include prel:?extend
include prel:?extend_props
include prel:?extend_func_props
include prel:?extend_order_props
include prel:?restrict_order_props
include prel:?restrict_props
include prel:?sequences
include prel:?seq_functions
include prel:?sets
include prel:?function_image
include prel:?function_inverse_alt
include prel:?function_props
include prel:?function_props2
include prel:?function_props_alt
include prel:?indexed_sets
include prel:?mucalculus
include prel:?ctlops
include prel:?fairctlops
include prel:?relation_defs
include prel:?relation_props
include prel:?relation_props2
include prel:?EquivalenceClosure
include prel:?QuotientDefinition
include prel:?bounded_real_defs
include prel:?bounded_real_defs_alt
include prel:?min_nat
include prel:?finite_sets
include prel:?function_image_aux
include prel:?function_iterate
include prel:?infinite_sets_def
include prel:?list2set
include prel:?filters
include prel:?Fairctlops
include prel:?more_finseq
include prel:?relation_converse_props
include prel:?KernelDefinition
include prel:?QuotientKernelProperties
include prel:?QuotientSubDefinition
include prel:?QuotientExtensionProperties
include prel:?QuotientDistributive
include prel:?QuotientIteration
include prel:?extend_set_props
include prel:?integer_props
include prel:?restrict_set_props
include prel:?map_props
include prel:?sets_lemmas
include prel:?finite_sets_of_sets
include prel:?stdlang
include prel:?strings
include prel:?stdexc
include prel:?stdcatch
include prel:?stdprog
include prel:?stdglobal
include prel:?stdpvs
include prel:?stdpvsio
include prel:?stdstr
include prel:?stdmath
include prel:?stdio
include prel:?stdfmap
include prel:?stdindent
include prel:?stdsys
include prel:?stdtokenizer
include prel:?subrange_inductions
include prel:?subrange_type
include prel:?union_adt
include prel:?union
include prel:?union_adt_map
include prel:?union_adt_reduce
include prel:?wf_induction
include prel:?xor_def
include prel:?bv_bitwise