Skip to content
Snippets Groups Projects
Select Git revision
  • 37a6062b7100bb93c20dee4415e96e608da20a5e
  • master default
  • JS-based-scroll-rendering
  • Paul_Marius_Level
  • Paul_Marius_2
  • Paul_Marius
  • Andi_Mark
  • be-UnityWebView
  • gitignoreFrameitServer
  • ZimmerBSc
  • Bugfix_StageLoading
  • stages
  • MAZIFAU_Experimental
  • tsc/coneworld
  • tsc/fact-interaction
  • marcel
  • MaZiFAU_TopSort
  • mergeHelper
  • zwischenSpeichern
  • tempAndrToMaster
  • SebBranch
  • 3.0
  • v2.1
  • v2.0
  • v1.0
25 results

MenueControl_mobile.cs

Blame
  • 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