products/sources/formale Sprachen/Isabelle/HOL image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lattices_Big.thy   Sprache: SML

(riemann_scaf
 (IMP_integral_def_TCC1 0
  (IMP_integral_def_TCC1-1 nil 3420183209
   ("" (expand "connected?") (("" (propax) nil nil)) nil)
   ((connected? const-decl "bool" deriv_domain_def "analysis/")) nil))
 (IMP_integral_def_TCC2 0
  (IMP_integral_def_TCC2-1 nil 3420183209
   ("" (expand "not_one_element?")
    (("" (skosimp)
      (("" (case-replace "x!1=0")
        (("1" (inst + "1") (("1" (assertnil nil)) nil)
         ("2" (inst + "0") (("2" (assertnil nil)) nil))
        nil))
      nil))
    nil)
   ((real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
 (step_TCC1 0
  (step_TCC1-1 nil 3450779708
   ("" (expand "step?")
    (("" (expand "step_function?")
      (("" (expand "zeroed?")
        ((""
          (inst + "(# length := 2,
                     seq := (LAMBDA (ii: below(2)): if ii = 0 then a else b endif) #)")
          (("1" (expand "step_function_on?")
            (("1" (skosimp)
              (("1" (inst + "0") (("1" (skosimp) nil nil)) nil)) nil))
            nil)
           ("2" (skosimp) (("2" (assertnil nil)) nil)
           ("3" (skosimp) (("3" (assertnil nil)) nil)
           ("4" (skosimp) (("4" (assertnil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((step_function? const-decl "bool" step_fun_def "analysis/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (b formal-const-decl "{x: real | a < x}" riemann_scaf nil)
    (a formal-const-decl "real" riemann_scaf nil)
    (<= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (below type-eq-decl nil nat_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (> const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (partition type-eq-decl nil integral_def "analysis/")
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (step_function_on? const-decl "bool" step_fun_def "analysis/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (zeroed? const-decl "bool" riemann_scaf nil)
    (step? const-decl "bool" riemann_scaf nil))
   nil))
 (bounded_TCC1 0
  (bounded_TCC1-1 nil 3450779708
   ("" (expand "zeroed_bounded?")
    (("" (expand "bounded?")
      (("" (expand "zeroed?")
        (("" (expand "abs") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((bounded? const-decl "bool" sup_norm "measure_integration/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (zeroed? const-decl "bool" riemann_scaf nil)
    (zeroed_bounded? const-decl "bool" riemann_scaf nil))
   nil))
 (IMP_fun_preds_partial_TCC1 0
  (IMP_fun_preds_partial_TCC1-1 nil 3450779708
   ("" (expand "partial_order?")
    (("" (expand "preorder?")
      (("" (expand "restrict")
        (("" (split)
          (("1" (expand "reflexive?")
            (("1" (skosimp)
              (("1" (expand "<=") (("1" (propax) nil nil)) nil)) nil))
            nil)
           ("2" (expand "transitive?")
            (("2" (expand "<=")
              (("2" (skosimp*)
                (("2" (inst - "x!2")
                  (("2" (inst - "x!2") (("2" (assertnil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (expand "antisymmetric?")
            (("3" (expand "<=")
              (("3" (skosimp)
                (("3" (apply-extensionality 1 :hide? t)
                  (("3" (inst - "x!2")
                    (("3" (inst - "x!2") (("3" (assertnil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((preorder? const-decl "bool" orders nil)
    (<= const-decl "bool" real_fun_orders "reals/")
    (reflexive? const-decl "bool" relations nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (transitive? const-decl "bool" relations nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (step? const-decl "bool" riemann_scaf nil)
    (step nonempty-type-eq-decl nil riemann_scaf nil)
    (antisymmetric? const-decl "bool" relations nil)
    (restrict const-decl "R" restrict nil)
    (partial_order? const-decl "bool" orders nil))
   nil))
 (partition_to_finite_partition_TCC1 0
  (partition_to_finite_partition_TCC1-1 nil 3420272748
   ("" (grind) nil nilnil nil))
 (partition_to_finite_partition_TCC2 0
  (partition_to_finite_partition_TCC2-1 nil 3420272748
   ("" (grind) nil nilnil nil))
 (partition_to_finite_partition_TCC3 0
  (partition_to_finite_partition_TCC3-1 nil 3420272748
   ("" (skosimp)
    (("" (expand "finite_partition?")
      (("" (split)
        (("1" (expand "singleton" 1 1)
          (("1" (expand "singleton" 1 1)
            (("1" (expand "union")
              (("1" (expand "member")
                (("1" (expand "fullset")
                  (("1" (expand "partition?")
                    (("1" (split)
                      (("1" (apply-extensionality :hide? t)
                        (("1" (expand "Union")
                          (("1" (case "x!1)
                            (("1" (split)
                              (("1" (inst + "{x | x < a}"nil nil)
                               ("2" (inst + "{x | bnil nil))
                              nil)
                             ("2" (flatten)
                              (("2"
                                (case "a<=x!1")
                                (("1"
                                  (case "x!1<=b")
                                  (("1"
                                    (hide 1 2)
                                    (("1"
                                      (lemma
                                       "part_in"
                                       ("P"
                                        "P!1"
                                        "a"
                                        "a"
                                        "b"
                                        "b"
                                        "x"
                                        "x!1"))
                                      (("1"
                                        (assert)
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (expand "<=" (-1 -2))
                                            (("1"
                                              (split -1)
                                              (("1"
                                                (split -2)
                                                (("1"
                                                  (inst
                                                   +
                                                   "{x |
                              seq(P!1)(ii!1) < x AND
                               x < seq(P!1)(1 + ii!1)}")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (flatten)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (inst 4 "ii!1")
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (inst
                                                   +
                                                   "singleton[closed_interval[real](a, b)]
                             (seq(P!1)(1+ii!1))")
                                                  (("1"
                                                    (expand "extend")
                                                    (("1"
                                                      (expand
                                                       "singleton")
                                                      (("1"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (flatten)
                                                    (("2"
                                                      (inst 3 "1+ii!1")
                                                      (("2"
                                                        (expand
                                                         "extend")
                                                        (("2"
                                                          (hide 1 2 4)
                                                          (("2"
                                                            (apply-extensionality
                                                             1
                                                             :hide?
                                                             t)
                                                            (("1"
                                                              (expand
                                                               "singleton")
                                                              (("1"
                                                                (lift-if
                                                                 1)
                                                                (("1"
                                                                  (prop)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (skosimp)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (inst
                                                 +
                                                 "singleton[closed_interval[real](a, b)]
                             (seq(P!1)(ii!1))")
                                                (("1"
                                                  (expand "extend")
                                                  (("1"
                                                    (expand
                                                     "singleton")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (flatten)
                                                  (("2"
                                                    (hide 1 2 4)
                                                    (("2"
                                                      (inst + "ii!1")
                                                      (("2"
                                                        (apply-extensionality
                                                         1
                                                         :hide?
                                                         t)
                                                        (("2"
                                                          (expand
                                                           "extend")
                                                          (("2"
                                                            (expand
                                                             "singleton")
                                                            (("2"
                                                              (lift-if
                                                               1)
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (case-replace
                                                                   "x!2 = seq(P!1)(ii!1)")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (assertnil nil))
                                  nil)
                                 ("2" (assertnil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (typepred "x!1")
                          (("2" (typepred "y!1")
                            (("2" (split)
                              (("1"
                                (split)
                                (("1" (assertnil nil)
                                 ("2" (grind) nil nil)
                                 ("3"
                                  (skosimp)
                                  (("3" (grind) nil nil))
                                  nil)
                                 ("4" (grind) nil nil))
                                nil)
                               ("2"
                                (split -2)
                                (("1" (grind) nil nil)
                                 ("2" (assertnil nil)
                                 ("3" (grind) nil nil)
                                 ("4" (grind) nil nil))
                                nil)
                               ("3"
                                (skosimp)
                                (("3"
                                  (split -2)
                                  (("1" (grind) nil nil)
                                   ("2" (grind) nil nil)
                                   ("3" (grind) nil nil)
                                   ("4"
                                    (skosimp)
                                    (("4"
                                      (replace -1)
                                      (("4"
                                        (replace -2)
                                        (("4"
                                          (hide-all-but 2)
                                          (("4"
                                            (expand "disjoint?")
                                            (("4"
                                              (expand "intersection")
                                              (("4"
                                                (expand "empty?")
                                                (("4"
                                                  (expand "member")
                                                  (("4"
                                                    (skosimp)
                                                    (("4"
                                                      (expand
                                                       "singleton")
                                                      (("4"
                                                        (lemma
                                                         "part_not_in"
                                                         ("a"
                                                          "a"
                                                          "b"
                                                          "b"
                                                          "x"
                                                          "x!2"))
                                                        (("4"
                                                          (assert)
                                                          (("4"
                                                            (inst
                                                             -
                                                             "P!1")
                                                            (("4"
                                                              (inst
                                                               -
                                                               "i!2"
                                                               "i!1")
                                                              (("4"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("4"
                                (split)
                                (("1" (grind) nil nil)
                                 ("2" (grind) nil nil)
                                 ("3"
                                  (skosimp*)
                                  (("3"
                                    (replace -1)
                                    (("3"
                                      (replace -2)
                                      (("3"
                                        (hide-all-but 2)
                                        (("3"
                                          (expand "disjoint?")
                                          (("3"
                                            (expand "intersection")
                                            (("3"
                                              (expand "empty?")
                                              (("3"
                                                (expand "member")
                                                (("3"
                                                  (skosimp)
                                                  (("3"
                                                    (expand
                                                     "singleton")
                                                    (("3"
                                                      (lemma
                                                       "part_not_in"
                                                       ("a"
                                                        "a"
                                                        "b"
                                                        "b"
                                                        "x"
                                                        "x!2"))
                                                      (("3"
                                                        (assert)
                                                        (("3"
                                                          (inst
                                                           -
                                                           "P!1")
                                                          (("3"
                                                            (inst
                                                             -
                                                             "i!2"
                                                             "i!1")
                                                            (("3"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("4"
                                  (skosimp*)
                                  (("4"
                                    (lemma
                                     "parts_disjoint"
                                     ("a" "a" "b" "b"))
                                    (("4"
                                      (inst - "_" "P!1" "i!1" "i!2")
                                      (("4"
                                        (replace -2)
                                        (("4"
                                          (replace -3)
                                          (("4"
                                            (hide -2 -3)
                                            (("4"
                                              (expand "disjoint?")
                                              (("4"
                                                (expand "intersection")
                                                (("4"
                                                  (expand "empty?")
                                                  (("4"
                                                    (expand "member")
                                                    (("4"
                                                      (skosimp)
                                                      (("4"
                                                        (inst - "x!2")
                                                        (("4"
                                                          (assert)
                                                          (("4"
                                                            (replace
                                                             -1)
                                                            (("4"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (rewrite "finite_union")
          (("2" (hide 2)
            (("2" (rewrite "finite_union")
              (("1" (hide 2)
                (("1" (rewrite "is_finite_surj" + :dir rl)
                  (("1"
                    (inst + "length(P!1)-1"
                     "lambda (i: below(length(P!1) - 1)):
                         {x |
                              seq(P!1)(i) < x AND
                               x < seq(P!1)(1 + i)}")
                    (("1" (expand "surjective?")
                      (("1" (skosimp)
                        (("1" (typepred "y!1")
                          (("1" (skosimp)
                            (("1" (inst + "i!1")
                              (("1" (assertnil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp) (("2" (inst + "i!1"nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (rewrite "is_finite_surj" + :dir rl)
                  (("2"
                    (inst + "length(P!1)"
                     "lambda (i: below(length(P!1))):singleton[closed_interval[real](a, b)]
                              (seq(P!1)(i))")
                    (("1" (expand "surjective?")
                      (("1" (skosimp)
                        (("1" (typepred "y!1")
                          (("1" (skosimp)
                            (("1" (inst + "i!1")
                              (("1"
                                (expand "extend")
                                (("1"
                                  (apply-extensionality :hide? t)
                                  (("1"
                                    (replace -1 1 rl)
                                    (("1"
                                      (lift-if 1)
                                      (("1"
                                        (prop)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (replace -2)
                                            (("1"
                                              (expand "singleton")
                                              (("1" (assertnil nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
                                          (("2"
                                            (replace -2)
                                            (("2"
                                              (expand "singleton")
                                              (("2" (assertnil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (skosimp)
                                    (("2" (assertnil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp)
                      (("2" (inst + "i!1")
                        (("2" (expand "extend")
                          (("2" (apply-extensionality :hide? t)
                            (("1" (expand "singleton")
                              (("1"
                                (case-replace "x!1 = seq(P!1)(i!1)")
                                (("1" (assertnil nil)
                                 ("2" (assertnil nil))
                                nil))
                              nil)
                             ("2" (skosimp) (("2" (assertnil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty_union1 application-judgement "(nonempty?)" bounded_nats
     "orders/")
    (finite_partition? const-decl "bool" partitions
     "measure_integration/")
    (nonempty_finite_union1 application-judgement
     "non_empty_finite_set[T]" sigma_countable "sigma_set/")
    (finite_union judgement-tcc nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite_surj formula-decl nil finite_sets nil)
    (surjective? const-decl "bool" functions nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (singleton const-decl "(singleton?)" sets nil)
    (union const-decl "set" sets nil)
    (fullset const-decl "set" sets nil)
    (part_in formula-decl nil integral_def "analysis/")
    (finite_extend application-judgement "finite_set[T]"
     extend_set_props nil)
    (nonempty_extend application-judgement "(nonempty?[T])"
     extend_set_props nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil)
    (ii!1 skolem-const-decl "below(length(P!1) - 1)" riemann_scaf nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (singleton_is_closed application-judgement
     "closed[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (singleton_is_compact application-judgement
     "compact[real, (metric_induced_topology)]" convergence_aux
     "metric_space/")
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[real]" integral_def "analysis/")
    (singleton_is_null application-judgement "null_set" lebesgue_def
     nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" sigma_countable "sigma_set/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (set type-eq-decl nil sets nil) (Union const-decl "set" sets nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (< const-decl "bool" reals nil)
    (a formal-const-decl "real" riemann_scaf nil)
    (b formal-const-decl "{x: real | a < x}" riemann_scaf nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (> const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (partition type-eq-decl nil integral_def "analysis/")
    (singleton? const-decl "bool" sets nil)
    (TRUE const-decl "bool" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" sets nil)
    (part_not_in formula-decl nil integral_def "analysis/")
    (finite_intersection1 application-judgement "finite_set[real]"
     integral_def "analysis/")
    (intersection2_preserves_bounded application-judgement
     "(LAMBDA (S: set[T]):
   bounded?(S, restrict[[real, real], [T, T], boolean](<=)))"
     bounded_nats "orders/")
    (parts_disjoint formula-decl nil integral_def "analysis/")
    (intersection1_preserves_bounded application-judgement
     "(LAMBDA (S: set[T]):
   bounded?(S, restrict[[real, real], [T, T], boolean](<=)))"
     bounded_nats "orders/")
    (finite_intersection2 application-judgement "finite_set[real]"
     integral_def "analysis/")
    (partition? const-decl "bool" partitions "measure_integration/")
    (member const-decl "bool" sets nil))
   nil))
 (riemann_lebesgue_step_isf 0
  (riemann_lebesgue_step_isf-1 nil 3450826554
   ("" (skosimp)
    (("" (typepred "phi!1")
      (("" (expand "step?")
        (("" (flatten)
          ((""
            (lemma "step_function_integrable?"
             ("a" "a" "b" "b" "f" "phi!1"))
            (("" (expand "Integrable?")
              (("" (assert)
                (("" (hide -1)
                  (("" (expand "Integral")
                    ((""
                      (lemma "step_function_on_integral"
                       ("a" "a" "b" "b" "f" "phi!1"))
                      (("" (assert)
                        (("" (expand "step_function?")
                          (("" (skosimp)
                            (("" (inst - "P!1")
                              ((""
                                (assert)
                                ((""
                                  (replace -1)
                                  ((""
                                    (hide -1)
                                    ((""
                                      (expand "step_function_on?")
                                      ((""
                                        (typepred "P!1")
                                        ((""
                                          (case
                                           "forall (x:real): isf?(*[real](phi(singleton[real](x)),phi!1)) & isf_integral(*[real](phi(singleton[real](x)),phi!1))=0")
                                          (("1"
                                            (case
                                             "forall (ii: below(length(P!1) - 1)): isf?(*[real]( val_in(a, b, P!1, ii, phi!1),phi(open(seq(P!1)(ii), seq(P!1)(1 + ii))))) & isf_integral(*[real]( val_in(a, b, P!1, ii, phi!1),phi(open(seq(P!1)(ii), seq(P!1)(1 + ii)))))=P!1`seq(1 + ii) * val_in(a, b, P!1, ii, phi!1) -
                P!1`seq(ii) * val_in(a, b, P!1, ii, phi!1)")
                                            (("1"
                                              (name
                                               "FF"
                                               "LAMBDA (ii: below(length(P!1) - 1)):
               P!1`seq(1 + ii) * val_in(a, b, P!1, ii, phi!1) -
                P!1`seq(ii) * val_in(a, b, P!1, ii, phi!1)")
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (case
                                                   "FORALL (ii: below(length(P!1) - 1)):
        isf?(*[real]
                 (val_in(a, b, P!1, ii, phi!1),
                  phi(open(seq(P!1)(ii), seq(P!1)(1 + ii)))))
         &
         isf_integral(*[real]
                          (val_in(a, b, P!1, ii, phi!1),
                           phi(open(seq(P!1)(ii), seq(P!1)(1 + ii)))))
          = FF(ii)")
                                                  (("1"
                                                    (case
                                                     "forall (n:nat): n <= length(P!1) - 2 => isf?(*[real](phi({x:real | a <= x & x < seq(P!1)(n+1)}),phi!1)) & sigma(0,n,FF) = isf_integral(*[real](phi({x:real | a <= x & x < seq(P!1)(n+1)}),phi!1))")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "length(P!1)-2")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (replace -8)
                                                          (("1"
                                                            (flatten)
                                                            (("1"
                                                              (replace
                                                               -2)
                                                              (("1"
                                                                (hide
                                                                 -3
                                                                 -4
                                                                 -5
                                                                 -2)
                                                                (("1"
                                                                  (inst
                                                                   -2
                                                                   "b")
                                                                  (("1"
                                                                    (flatten)
                                                                    (("1"
                                                                      (lemma
                                                                       "isf_add"
                                                                       ("i1"
                                                                        "(*[real](phi({x: real | a <= x & x < b}), phi!1))"
                                                                        "i2"
                                                                        "(*[real](phi(singleton[real](b)), phi!1))"))
                                                                      (("1"
                                                                        (lemma
                                                                         "isf_integral_add"
                                                                         ("i1"
                                                                          "(*[real](phi({x: real | a <= x & x < b}), phi!1))"
                                                                          "i2"
                                                                          "(*[real](phi(singleton[real](b)), phi!1))"))
                                                                        (("1"
                                                                          (case-replace
                                                                           "((*[real](phi({x: real | a <= x & x < b}), phi!1)) +
                    (*[real](phi(singleton[real](b)), phi!1)))=phi!1")
                                                                          (("1"
                                                                            (replace
                                                                             -3)
                                                                            (("1"
                                                                              (replace
                                                                               -2
                                                                               1)
                                                                              (("1"
                                                                                (replace
                                                                                 -6)
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
                                                                             (-11
                                                                              1))
                                                                            (("2"
                                                                              (apply-extensionality
                                                                               :hide?
                                                                               t)
                                                                              (("2"
                                                                                (expand
                                                                                 "zeroed?")
                                                                                (("2"
                                                                                  (inst
                                                                                   -
                                                                                   "x!1")
                                                                                  (("2"
                                                                                    (grind)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (propax)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide 2)
                                                      (("2"
                                                        (name
                                                         "GG"
                                                         "lambda (n: below(length(P!1) - 1)): (*[real]
                            (phi({x: real | a <= x & x < seq(P!1)(n + 1)}),
                             phi!1))")
                                                        (("2"
                                                          (case
                                                           "FORALL (n: nat):
        n <= length(P!1) - 2 =>
         isf?(GG(n)) & sigma(0, n, FF) =
           isf_integral(GG(n))")
                                                          (("1"
                                                            (skosimp)
                                                            (("1"
                                                              (inst
                                                               -
                                                               "n!1")
                                                              (("1"
                                                                (expand
                                                                 "GG")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide 2)
                                                            (("2"
                                                              (hide -1)
                                                              (("2"
                                                                (induct
                                                                 "n")
                                                                (("1"
                                                                  (flatten)
                                                                  (("1"
                                                                    (expand
                                                                     "sigma")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (expand
                                                                         "GG")
                                                                        (("1"
                                                                          (inst
                                                                           -2
                                                                           "0")
                                                                          (("1"
                                                                            (inst
                                                                             -5
                                                                             "a")
                                                                            (("1"
                                                                              (flatten)
                                                                              (("1"
                                                                                (lemma
                                                                                 "isf_add"
                                                                                 ("i1"
                                                                                  "(*[real](phi(singleton[real](a)), phi!1))"
                                                                                  "i2"
                                                                                  "(*[real]
                (val_in(a, b, P!1, 0, phi!1),
                 phi(open(seq(P!1)(0), seq(P!1)(1 + 0)))))"))
                                                                                (("1"
                                                                                  (lemma
                                                                                   "isf_integral_add"
                                                                                   ("i1"
                                                                                    "(*[real](phi(singleton[real](a)), phi!1))"
                                                                                    "i2"
                                                                                    "(*[real]
                (val_in(a, b, P!1, 0, phi!1),
                 phi(open(seq(P!1)(0), seq(P!1)(1 + 0)))))"))
                                                                                  (("1"
                                                                                    (replace
                                                                                     -9)
                                                                                    (("1"
                                                                                      (replace
                                                                                       -5)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "+
")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "*")
                                                                                          (("1"
                                                                                            (case-replace
                                                                                             "(LAMBDA (x: real):
             phi(singleton[real](a))(x) * phi!1(x) +
              val_in(a, b, P!1, 0, phi!1) *
               phi(open(seq(P!1)(0), seq(P!1)(1)))(x))=(LAMBDA (x_1: real):
             phi({x: real | a <= x & x < seq(P!1)(1)})(x_1) * phi!1(x_1))")
                                                                                            (("1"
                                                                                              (replace
                                                                                               -3)
                                                                                              (("1"
                                                                                                (replace
                                                                                                 -2)
                                                                                                (("1"
                                                                                                  (propax)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (hide
                                                                                               2
                                                                                               -7)
                                                                                              (("2"
                                                                                                (apply-extensionality
                                                                                                 1
                                                                                                 :hide?
                                                                                                 t)
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "singleton")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "phi")
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "member")
                                                                                                      (("1"
                                                                                                        (case-replace
                                                                                                         "x!1=a")
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          (("1"
                                                                                                            (replace
                                                                                                             -11)
                                                                                                            (("1"
                                                                                                              (inst
                                                                                                               -13
                                                                                                               "0")
                                                                                                              (("1"
                                                                                                                (assert)
                                                                                                                (("1"
                                                                                                                  (expand
                                                                                                                   "val_in")
                                                                                                                  (("1"
                                                                                                                    (inst
                                                                                                                     -14
                                                                                                                     "0")
                                                                                                                    (("1"
                                                                                                                      (skosimp)
                                                                                                                      (("1"
                                                                                                                        (case-replace
                                                                                                                         "open(a, seq(P!1)(1))(a)")
                                                                                                                        (("1"
                                                                                                                          (hide-all-but
                                                                                                                           (-12
                                                                                                                            -14
                                                                                                                            -1))
                                                                                                                          (("1"
                                                                                                                            (grind)
                                                                                                                            nil
--> --------------------

--> maximum size reached

--> --------------------

[ Seitenstruktur0.74Drucken  etwas mehr zur Ethik  ]