How to define a termination order for the function with fmmap_keys?











up vote
2
down vote

favorite












I'm trying to define a supremum operation for a datatype based on fmap:



datatype t = A | B | C "(nat, t) fmap"

abbreviation
"supc f xs ys ≡
fmmap_keys
(λk x. f x (the (fmlookup ys k)))
(fmfilter (λk. k |∈| fmdom ys) xs)"

fun sup_t (infixl "⊔" 65) where
"A ⊔ _ = A"
| "B ⊔ B = B"
| "B ⊔ _ = A"
| "C xs ⊔ C ys = C (supc (⊔) xs ys)"
| "C xs ⊔ _ = A"


And get the error:



Unfinished subgoals:
(a, 1, <):
1. ⋀ys x. size (the (fmlookup ys x)) < Suc (∑x∈fset (fset_of_fmap ys). Suc (case x of (a, x) ⇒ size x))
(a, 1, <=):
1. ⋀ys x. size (the (fmlookup ys x)) ≤ Suc (∑x∈fset (fset_of_fmap ys). Suc (case x of (a, x) ⇒ size x))
(a, 2, <):
1. ⋀xs xa. size xa < Suc (∑x∈fset (fset_of_fmap xs). Suc (case x of (a, x) ⇒ size x))
(a, 2, <=):
1. ⋀xs xa. size xa ≤ Suc (∑x∈fset (fset_of_fmap xs). Suc (case x of (a, x) ⇒ size x))
(a, 3, <):
1. False
Calls:
a) (C xs, C ys) ~> (xa, the (fmlookup ys x))
Measures:
1) λp. size (snd p)
2) λp. size (fst p)
3) size
Result matrix:
1 2 3
a: ? ? <=

Could not find lexicographic termination order.


If I simplify the function passed as the first argument to fmmap_keys, then the error disappears:



abbreviation
"supc f xs ys ≡
fmmap_keys
(λk x. x)
(fmfilter (λk. k |∈| fmdom ys) xs)"


So I guess, that the error is caused by a complex recursive call of sup_t. The only possible source of non-termination is structures of the form C («[x ↦ C (...)]»). But an external C is removed on each recursive call so the function should terminate.



Could you suggest how to fix this error or redefine supc?





UPDATE



Here is an alternative definition:



abbreviation
"supc f xs ys ≡
fmap_of_list (map
(λ(k, x). (k, f x (the (fmlookup ys k))))
(sorted_list_of_fmap (fmfilter (λk. k |∈| fmdom ys) xs)))"

function sup_t (infixl "⊔" 65) where
"A ⊔ _ = A"
| "B ⊔ x = (if x = B then B else A)"
| "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"
by pat_completeness auto
termination
apply auto


I have to prove the following subgoal:



⋀a b. sup_t_dom (a, b)


How to unfold sup_t_dom?










share|improve this question




























    up vote
    2
    down vote

    favorite












    I'm trying to define a supremum operation for a datatype based on fmap:



    datatype t = A | B | C "(nat, t) fmap"

    abbreviation
    "supc f xs ys ≡
    fmmap_keys
    (λk x. f x (the (fmlookup ys k)))
    (fmfilter (λk. k |∈| fmdom ys) xs)"

    fun sup_t (infixl "⊔" 65) where
    "A ⊔ _ = A"
    | "B ⊔ B = B"
    | "B ⊔ _ = A"
    | "C xs ⊔ C ys = C (supc (⊔) xs ys)"
    | "C xs ⊔ _ = A"


    And get the error:



    Unfinished subgoals:
    (a, 1, <):
    1. ⋀ys x. size (the (fmlookup ys x)) < Suc (∑x∈fset (fset_of_fmap ys). Suc (case x of (a, x) ⇒ size x))
    (a, 1, <=):
    1. ⋀ys x. size (the (fmlookup ys x)) ≤ Suc (∑x∈fset (fset_of_fmap ys). Suc (case x of (a, x) ⇒ size x))
    (a, 2, <):
    1. ⋀xs xa. size xa < Suc (∑x∈fset (fset_of_fmap xs). Suc (case x of (a, x) ⇒ size x))
    (a, 2, <=):
    1. ⋀xs xa. size xa ≤ Suc (∑x∈fset (fset_of_fmap xs). Suc (case x of (a, x) ⇒ size x))
    (a, 3, <):
    1. False
    Calls:
    a) (C xs, C ys) ~> (xa, the (fmlookup ys x))
    Measures:
    1) λp. size (snd p)
    2) λp. size (fst p)
    3) size
    Result matrix:
    1 2 3
    a: ? ? <=

    Could not find lexicographic termination order.


    If I simplify the function passed as the first argument to fmmap_keys, then the error disappears:



    abbreviation
    "supc f xs ys ≡
    fmmap_keys
    (λk x. x)
    (fmfilter (λk. k |∈| fmdom ys) xs)"


    So I guess, that the error is caused by a complex recursive call of sup_t. The only possible source of non-termination is structures of the form C («[x ↦ C (...)]»). But an external C is removed on each recursive call so the function should terminate.



    Could you suggest how to fix this error or redefine supc?





    UPDATE



    Here is an alternative definition:



    abbreviation
    "supc f xs ys ≡
    fmap_of_list (map
    (λ(k, x). (k, f x (the (fmlookup ys k))))
    (sorted_list_of_fmap (fmfilter (λk. k |∈| fmdom ys) xs)))"

    function sup_t (infixl "⊔" 65) where
    "A ⊔ _ = A"
    | "B ⊔ x = (if x = B then B else A)"
    | "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"
    by pat_completeness auto
    termination
    apply auto


    I have to prove the following subgoal:



    ⋀a b. sup_t_dom (a, b)


    How to unfold sup_t_dom?










    share|improve this question


























      up vote
      2
      down vote

      favorite









      up vote
      2
      down vote

      favorite











      I'm trying to define a supremum operation for a datatype based on fmap:



      datatype t = A | B | C "(nat, t) fmap"

      abbreviation
      "supc f xs ys ≡
      fmmap_keys
      (λk x. f x (the (fmlookup ys k)))
      (fmfilter (λk. k |∈| fmdom ys) xs)"

      fun sup_t (infixl "⊔" 65) where
      "A ⊔ _ = A"
      | "B ⊔ B = B"
      | "B ⊔ _ = A"
      | "C xs ⊔ C ys = C (supc (⊔) xs ys)"
      | "C xs ⊔ _ = A"


      And get the error:



      Unfinished subgoals:
      (a, 1, <):
      1. ⋀ys x. size (the (fmlookup ys x)) < Suc (∑x∈fset (fset_of_fmap ys). Suc (case x of (a, x) ⇒ size x))
      (a, 1, <=):
      1. ⋀ys x. size (the (fmlookup ys x)) ≤ Suc (∑x∈fset (fset_of_fmap ys). Suc (case x of (a, x) ⇒ size x))
      (a, 2, <):
      1. ⋀xs xa. size xa < Suc (∑x∈fset (fset_of_fmap xs). Suc (case x of (a, x) ⇒ size x))
      (a, 2, <=):
      1. ⋀xs xa. size xa ≤ Suc (∑x∈fset (fset_of_fmap xs). Suc (case x of (a, x) ⇒ size x))
      (a, 3, <):
      1. False
      Calls:
      a) (C xs, C ys) ~> (xa, the (fmlookup ys x))
      Measures:
      1) λp. size (snd p)
      2) λp. size (fst p)
      3) size
      Result matrix:
      1 2 3
      a: ? ? <=

      Could not find lexicographic termination order.


      If I simplify the function passed as the first argument to fmmap_keys, then the error disappears:



      abbreviation
      "supc f xs ys ≡
      fmmap_keys
      (λk x. x)
      (fmfilter (λk. k |∈| fmdom ys) xs)"


      So I guess, that the error is caused by a complex recursive call of sup_t. The only possible source of non-termination is structures of the form C («[x ↦ C (...)]»). But an external C is removed on each recursive call so the function should terminate.



      Could you suggest how to fix this error or redefine supc?





      UPDATE



      Here is an alternative definition:



      abbreviation
      "supc f xs ys ≡
      fmap_of_list (map
      (λ(k, x). (k, f x (the (fmlookup ys k))))
      (sorted_list_of_fmap (fmfilter (λk. k |∈| fmdom ys) xs)))"

      function sup_t (infixl "⊔" 65) where
      "A ⊔ _ = A"
      | "B ⊔ x = (if x = B then B else A)"
      | "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"
      by pat_completeness auto
      termination
      apply auto


      I have to prove the following subgoal:



      ⋀a b. sup_t_dom (a, b)


      How to unfold sup_t_dom?










      share|improve this question















      I'm trying to define a supremum operation for a datatype based on fmap:



      datatype t = A | B | C "(nat, t) fmap"

      abbreviation
      "supc f xs ys ≡
      fmmap_keys
      (λk x. f x (the (fmlookup ys k)))
      (fmfilter (λk. k |∈| fmdom ys) xs)"

      fun sup_t (infixl "⊔" 65) where
      "A ⊔ _ = A"
      | "B ⊔ B = B"
      | "B ⊔ _ = A"
      | "C xs ⊔ C ys = C (supc (⊔) xs ys)"
      | "C xs ⊔ _ = A"


      And get the error:



      Unfinished subgoals:
      (a, 1, <):
      1. ⋀ys x. size (the (fmlookup ys x)) < Suc (∑x∈fset (fset_of_fmap ys). Suc (case x of (a, x) ⇒ size x))
      (a, 1, <=):
      1. ⋀ys x. size (the (fmlookup ys x)) ≤ Suc (∑x∈fset (fset_of_fmap ys). Suc (case x of (a, x) ⇒ size x))
      (a, 2, <):
      1. ⋀xs xa. size xa < Suc (∑x∈fset (fset_of_fmap xs). Suc (case x of (a, x) ⇒ size x))
      (a, 2, <=):
      1. ⋀xs xa. size xa ≤ Suc (∑x∈fset (fset_of_fmap xs). Suc (case x of (a, x) ⇒ size x))
      (a, 3, <):
      1. False
      Calls:
      a) (C xs, C ys) ~> (xa, the (fmlookup ys x))
      Measures:
      1) λp. size (snd p)
      2) λp. size (fst p)
      3) size
      Result matrix:
      1 2 3
      a: ? ? <=

      Could not find lexicographic termination order.


      If I simplify the function passed as the first argument to fmmap_keys, then the error disappears:



      abbreviation
      "supc f xs ys ≡
      fmmap_keys
      (λk x. x)
      (fmfilter (λk. k |∈| fmdom ys) xs)"


      So I guess, that the error is caused by a complex recursive call of sup_t. The only possible source of non-termination is structures of the form C («[x ↦ C (...)]»). But an external C is removed on each recursive call so the function should terminate.



      Could you suggest how to fix this error or redefine supc?





      UPDATE



      Here is an alternative definition:



      abbreviation
      "supc f xs ys ≡
      fmap_of_list (map
      (λ(k, x). (k, f x (the (fmlookup ys k))))
      (sorted_list_of_fmap (fmfilter (λk. k |∈| fmdom ys) xs)))"

      function sup_t (infixl "⊔" 65) where
      "A ⊔ _ = A"
      | "B ⊔ x = (if x = B then B else A)"
      | "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"
      by pat_completeness auto
      termination
      apply auto


      I have to prove the following subgoal:



      ⋀a b. sup_t_dom (a, b)


      How to unfold sup_t_dom?







      isabelle






      share|improve this question















      share|improve this question













      share|improve this question




      share|improve this question








      edited Nov 10 at 4:30

























      asked Nov 9 at 14:22









      Denis

      318219




      318219
























          1 Answer
          1






          active

          oldest

          votes

















          up vote
          2
          down vote



          accepted
          +50










          Please find a potentially viable solution in the code listing below.





          Background



          The issue that you have encountered is described partially in the document "Defining Recursive Functions in Isabelle/HOL" written by Alexander Krauss (also known as "Tutorial on Function Definitions" in Isabelle documentation) and more comprehensively in the PhD thesis "Automating Recursive Definitions and Termination Proofs in Higher-Order Logic" that was also written by Alexander Krauss. In particular, see Chapter 4 in the tutorial and section 3.3 in the thesis.





          Size of t



          From the aforementioned references, it is possible to infer that one way to prove the termination of sup_t is to provide a suitable measure function. In this case, it is apparent that a measure function that is associated with the size of the datatype might be suitable for the application. Unfortunately, t is a nested type and (in this particular case) the default function size does not seem to capture the recursive nature of the datatype - this is not always the case (see section 3.3.2 in the thesis).



          As the first step, I provided a new size function for t. The definition is based on the total number of Cs contained within x::t (the definition should be easy to modify to suit your needs for other applications).





          Measure and Termination



          I found that the measure function (λ(xs, ys). size ys) is suitable to prove the termination of sup_t. Also, this measure function is used in Isabelle to prove the termination of sup_t if it is declared with the command fun. However, in this case, it was not possible to prove that the arguments of recursive calls indeed decrease with respect to the relation that was established by the measure automatically. However, it would be sufficient to show that "size (the (fmlookup x k)) < size (C x)".



          Unfortunately, the function supc (as stated in your question) is not self-certifying with respect to the property that the first argument that is passed to (λk x. f x (the (fmlookup ys k))) is in the domain of ys. Therefore, the (fmlookup ys k) can take the value the None. Given that this issue seems to be nearly orthogonal to the main topic of the question, I decided not to investigate it further and made an amendment to the function supc to ensure that it is guaranteed to return an element of t (you may want to prove explicitly that the function specified below is identical in its behaviour to the one that you provided in your question or, otherwise, provide a better alternative that would be self-certifying):



          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"


          After this modification, the previous goal "size (the (fmlookup x k)) < size (C x)" was changed to "(k |∈| fmdom ys) ⟹ size (the (fmlookup x k)) < size (C x)", which could be easily proven (see lemma measure_cond). If this lemma is declared as an introduction rule then the termination of sup_t can be proven automatically if it is declared with the command fun.





          Remarks



          The main reason why I decided to investigate this issue and provide an answer is that I knew very little about some of the main topics of the question and wanted to learn them. In fact, in my own work, I have never encountered a function for which termination needed to be proven manually. Furthermore, I have never used the theory Finite_Map (at least, not explicitly). Thus, I also wanted to learn about this theory and the associated datatype. As a result, my answer may be suboptimal due to the lack of experience/knowledge in these areas. Of course, if you also have doubts about whether the solution that I proposed here is optimal for the application, it may be worth trying to ask the question on the mailing list. In all honesty, I would also like to know if there is a better solution.





          theory termination_problem
          imports
          Complex_Main
          "HOL-Library.Finite_Map"
          begin

          declare [[show_types]]
          declare [[show_sorts]]
          declare [[show_consts]]
          declare [[show_main_goal]]
          declare [[show_hyps]]

          datatype (plugins del: "size") t = A | B | C "(nat, t) fmap"

          abbreviation "tcf ≡ (λ v::(nat × nat). (λ r::nat. snd v + r))"

          interpretation tcf: comp_fun_commute tcf
          proof
          fix x y
          show "tcf y ∘ tcf x = tcf x ∘ tcf y"
          proof -
          fix z
          have "(tcf y ∘ tcf x) z = snd y + snd x + z" by auto
          also have "(tcf x ∘ tcf y) z = snd y + snd x + z" by auto
          ultimately have "(tcf y ∘ tcf x) z = (tcf x ∘ tcf y) z" by auto
          then show "(tcf y ∘ tcf x) = (tcf x ∘ tcf y)" by auto
          qed
          qed

          instantiation t :: size
          begin

          primrec t_size :: "t ⇒ nat" where
          AR: "t_size A = 0" |
          BR: "t_size B = 0" |
          CR: "t_size (C x) =
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"

          definition size_t where
          size_t_def: "size_t = t_size"

          instance ..

          end

          lemma ffold_rec_exp:
          assumes "k |∈| fmdom x"
          and "ky = (k, the (fmlookup (fmmap t_size x) k))"
          shows "ffold tcf 0 (fset_of_fmap (fmmap t_size x)) =
          tcf ky (ffold tcf 0 ((fset_of_fmap (fmmap t_size x)) |-| {|ky|}))"
          using assms tcf.ffold_rec by auto

          lemma elem_le_ffold:
          assumes "k |∈| fmdom x"
          shows "t_size (the (fmlookup x k)) <
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"
          using ffold_rec_exp assms by auto

          lemma measure_cond [intro]:
          assumes "k |∈| fmdom x"
          shows "size (the (fmlookup x k)) < size (C x)"
          using assms elem_le_ffold size_t_def by auto

          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"

          fun sup_t (infixl "⊔" 65) where
          "A ⊔ _ = A"
          | "B ⊔ x = (if x = B then B else A)"
          | "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"

          (*Examples*)

          abbreviation "list_1 ≡ fmap_of_list [(1::nat, B)]"
          abbreviation "list_2 ≡ fmap_of_list [(1::nat, A), (2::nat, A)]"
          value "(C list_1) ⊔ (C list_2)"

          abbreviation "list_3 ≡ fmap_of_list [(1::nat, B), (3::nat, A)]"
          abbreviation "list_4 ≡ fmap_of_list [(2::nat, A), (4::nat, B)]"
          value "(C list_3) ⊔ (C list_4)"

          abbreviation "list_5 ≡ fmap_of_list [(1::nat, B), (2::nat, B)]"
          abbreviation "list_6 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_5) ⊔ (C list_6)"

          abbreviation "list_7 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_8 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_7) ⊔ (C list_8)"

          abbreviation "list_9 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_10 ≡ fmap_of_list [(2::nat, C list_6), (3::nat, B)]"
          value "(C list_9) ⊔ (C list_10)"

          end





          share|improve this answer























          • Many thanks for a very detailed answer!
            – Denis
            Nov 12 at 16:46










          • This time, while answering your question, I have also acquired a substantial amount of new knowledge: thank you for providing an interesting question.
            – xanonec
            Nov 12 at 17:35






          • 1




            I have made minor amendments: it is not necessary to prove termination explicitly if measure_cond is declared as an introduction rule.
            – xanonec
            Nov 13 at 15:01











          Your Answer






          StackExchange.ifUsing("editor", function () {
          StackExchange.using("externalEditor", function () {
          StackExchange.using("snippets", function () {
          StackExchange.snippets.init();
          });
          });
          }, "code-snippets");

          StackExchange.ready(function() {
          var channelOptions = {
          tags: "".split(" "),
          id: "1"
          };
          initTagRenderer("".split(" "), "".split(" "), channelOptions);

          StackExchange.using("externalEditor", function() {
          // Have to fire editor after snippets, if snippets enabled
          if (StackExchange.settings.snippets.snippetsEnabled) {
          StackExchange.using("snippets", function() {
          createEditor();
          });
          }
          else {
          createEditor();
          }
          });

          function createEditor() {
          StackExchange.prepareEditor({
          heartbeatType: 'answer',
          convertImagesToLinks: true,
          noModals: true,
          showLowRepImageUploadWarning: true,
          reputationToPostImages: 10,
          bindNavPrevention: true,
          postfix: "",
          imageUploader: {
          brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
          contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
          allowUrls: true
          },
          onDemand: true,
          discardSelector: ".discard-answer"
          ,immediatelyShowMarkdownHelp:true
          });


          }
          });














           

          draft saved


          draft discarded


















          StackExchange.ready(
          function () {
          StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53227525%2fhow-to-define-a-termination-order-for-the-function-with-fmmap-keys%23new-answer', 'question_page');
          }
          );

          Post as a guest















          Required, but never shown

























          1 Answer
          1






          active

          oldest

          votes








          1 Answer
          1






          active

          oldest

          votes









          active

          oldest

          votes






          active

          oldest

          votes








          up vote
          2
          down vote



          accepted
          +50










          Please find a potentially viable solution in the code listing below.





          Background



          The issue that you have encountered is described partially in the document "Defining Recursive Functions in Isabelle/HOL" written by Alexander Krauss (also known as "Tutorial on Function Definitions" in Isabelle documentation) and more comprehensively in the PhD thesis "Automating Recursive Definitions and Termination Proofs in Higher-Order Logic" that was also written by Alexander Krauss. In particular, see Chapter 4 in the tutorial and section 3.3 in the thesis.





          Size of t



          From the aforementioned references, it is possible to infer that one way to prove the termination of sup_t is to provide a suitable measure function. In this case, it is apparent that a measure function that is associated with the size of the datatype might be suitable for the application. Unfortunately, t is a nested type and (in this particular case) the default function size does not seem to capture the recursive nature of the datatype - this is not always the case (see section 3.3.2 in the thesis).



          As the first step, I provided a new size function for t. The definition is based on the total number of Cs contained within x::t (the definition should be easy to modify to suit your needs for other applications).





          Measure and Termination



          I found that the measure function (λ(xs, ys). size ys) is suitable to prove the termination of sup_t. Also, this measure function is used in Isabelle to prove the termination of sup_t if it is declared with the command fun. However, in this case, it was not possible to prove that the arguments of recursive calls indeed decrease with respect to the relation that was established by the measure automatically. However, it would be sufficient to show that "size (the (fmlookup x k)) < size (C x)".



          Unfortunately, the function supc (as stated in your question) is not self-certifying with respect to the property that the first argument that is passed to (λk x. f x (the (fmlookup ys k))) is in the domain of ys. Therefore, the (fmlookup ys k) can take the value the None. Given that this issue seems to be nearly orthogonal to the main topic of the question, I decided not to investigate it further and made an amendment to the function supc to ensure that it is guaranteed to return an element of t (you may want to prove explicitly that the function specified below is identical in its behaviour to the one that you provided in your question or, otherwise, provide a better alternative that would be self-certifying):



          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"


          After this modification, the previous goal "size (the (fmlookup x k)) < size (C x)" was changed to "(k |∈| fmdom ys) ⟹ size (the (fmlookup x k)) < size (C x)", which could be easily proven (see lemma measure_cond). If this lemma is declared as an introduction rule then the termination of sup_t can be proven automatically if it is declared with the command fun.





          Remarks



          The main reason why I decided to investigate this issue and provide an answer is that I knew very little about some of the main topics of the question and wanted to learn them. In fact, in my own work, I have never encountered a function for which termination needed to be proven manually. Furthermore, I have never used the theory Finite_Map (at least, not explicitly). Thus, I also wanted to learn about this theory and the associated datatype. As a result, my answer may be suboptimal due to the lack of experience/knowledge in these areas. Of course, if you also have doubts about whether the solution that I proposed here is optimal for the application, it may be worth trying to ask the question on the mailing list. In all honesty, I would also like to know if there is a better solution.





          theory termination_problem
          imports
          Complex_Main
          "HOL-Library.Finite_Map"
          begin

          declare [[show_types]]
          declare [[show_sorts]]
          declare [[show_consts]]
          declare [[show_main_goal]]
          declare [[show_hyps]]

          datatype (plugins del: "size") t = A | B | C "(nat, t) fmap"

          abbreviation "tcf ≡ (λ v::(nat × nat). (λ r::nat. snd v + r))"

          interpretation tcf: comp_fun_commute tcf
          proof
          fix x y
          show "tcf y ∘ tcf x = tcf x ∘ tcf y"
          proof -
          fix z
          have "(tcf y ∘ tcf x) z = snd y + snd x + z" by auto
          also have "(tcf x ∘ tcf y) z = snd y + snd x + z" by auto
          ultimately have "(tcf y ∘ tcf x) z = (tcf x ∘ tcf y) z" by auto
          then show "(tcf y ∘ tcf x) = (tcf x ∘ tcf y)" by auto
          qed
          qed

          instantiation t :: size
          begin

          primrec t_size :: "t ⇒ nat" where
          AR: "t_size A = 0" |
          BR: "t_size B = 0" |
          CR: "t_size (C x) =
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"

          definition size_t where
          size_t_def: "size_t = t_size"

          instance ..

          end

          lemma ffold_rec_exp:
          assumes "k |∈| fmdom x"
          and "ky = (k, the (fmlookup (fmmap t_size x) k))"
          shows "ffold tcf 0 (fset_of_fmap (fmmap t_size x)) =
          tcf ky (ffold tcf 0 ((fset_of_fmap (fmmap t_size x)) |-| {|ky|}))"
          using assms tcf.ffold_rec by auto

          lemma elem_le_ffold:
          assumes "k |∈| fmdom x"
          shows "t_size (the (fmlookup x k)) <
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"
          using ffold_rec_exp assms by auto

          lemma measure_cond [intro]:
          assumes "k |∈| fmdom x"
          shows "size (the (fmlookup x k)) < size (C x)"
          using assms elem_le_ffold size_t_def by auto

          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"

          fun sup_t (infixl "⊔" 65) where
          "A ⊔ _ = A"
          | "B ⊔ x = (if x = B then B else A)"
          | "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"

          (*Examples*)

          abbreviation "list_1 ≡ fmap_of_list [(1::nat, B)]"
          abbreviation "list_2 ≡ fmap_of_list [(1::nat, A), (2::nat, A)]"
          value "(C list_1) ⊔ (C list_2)"

          abbreviation "list_3 ≡ fmap_of_list [(1::nat, B), (3::nat, A)]"
          abbreviation "list_4 ≡ fmap_of_list [(2::nat, A), (4::nat, B)]"
          value "(C list_3) ⊔ (C list_4)"

          abbreviation "list_5 ≡ fmap_of_list [(1::nat, B), (2::nat, B)]"
          abbreviation "list_6 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_5) ⊔ (C list_6)"

          abbreviation "list_7 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_8 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_7) ⊔ (C list_8)"

          abbreviation "list_9 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_10 ≡ fmap_of_list [(2::nat, C list_6), (3::nat, B)]"
          value "(C list_9) ⊔ (C list_10)"

          end





          share|improve this answer























          • Many thanks for a very detailed answer!
            – Denis
            Nov 12 at 16:46










          • This time, while answering your question, I have also acquired a substantial amount of new knowledge: thank you for providing an interesting question.
            – xanonec
            Nov 12 at 17:35






          • 1




            I have made minor amendments: it is not necessary to prove termination explicitly if measure_cond is declared as an introduction rule.
            – xanonec
            Nov 13 at 15:01















          up vote
          2
          down vote



          accepted
          +50










          Please find a potentially viable solution in the code listing below.





          Background



          The issue that you have encountered is described partially in the document "Defining Recursive Functions in Isabelle/HOL" written by Alexander Krauss (also known as "Tutorial on Function Definitions" in Isabelle documentation) and more comprehensively in the PhD thesis "Automating Recursive Definitions and Termination Proofs in Higher-Order Logic" that was also written by Alexander Krauss. In particular, see Chapter 4 in the tutorial and section 3.3 in the thesis.





          Size of t



          From the aforementioned references, it is possible to infer that one way to prove the termination of sup_t is to provide a suitable measure function. In this case, it is apparent that a measure function that is associated with the size of the datatype might be suitable for the application. Unfortunately, t is a nested type and (in this particular case) the default function size does not seem to capture the recursive nature of the datatype - this is not always the case (see section 3.3.2 in the thesis).



          As the first step, I provided a new size function for t. The definition is based on the total number of Cs contained within x::t (the definition should be easy to modify to suit your needs for other applications).





          Measure and Termination



          I found that the measure function (λ(xs, ys). size ys) is suitable to prove the termination of sup_t. Also, this measure function is used in Isabelle to prove the termination of sup_t if it is declared with the command fun. However, in this case, it was not possible to prove that the arguments of recursive calls indeed decrease with respect to the relation that was established by the measure automatically. However, it would be sufficient to show that "size (the (fmlookup x k)) < size (C x)".



          Unfortunately, the function supc (as stated in your question) is not self-certifying with respect to the property that the first argument that is passed to (λk x. f x (the (fmlookup ys k))) is in the domain of ys. Therefore, the (fmlookup ys k) can take the value the None. Given that this issue seems to be nearly orthogonal to the main topic of the question, I decided not to investigate it further and made an amendment to the function supc to ensure that it is guaranteed to return an element of t (you may want to prove explicitly that the function specified below is identical in its behaviour to the one that you provided in your question or, otherwise, provide a better alternative that would be self-certifying):



          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"


          After this modification, the previous goal "size (the (fmlookup x k)) < size (C x)" was changed to "(k |∈| fmdom ys) ⟹ size (the (fmlookup x k)) < size (C x)", which could be easily proven (see lemma measure_cond). If this lemma is declared as an introduction rule then the termination of sup_t can be proven automatically if it is declared with the command fun.





          Remarks



          The main reason why I decided to investigate this issue and provide an answer is that I knew very little about some of the main topics of the question and wanted to learn them. In fact, in my own work, I have never encountered a function for which termination needed to be proven manually. Furthermore, I have never used the theory Finite_Map (at least, not explicitly). Thus, I also wanted to learn about this theory and the associated datatype. As a result, my answer may be suboptimal due to the lack of experience/knowledge in these areas. Of course, if you also have doubts about whether the solution that I proposed here is optimal for the application, it may be worth trying to ask the question on the mailing list. In all honesty, I would also like to know if there is a better solution.





          theory termination_problem
          imports
          Complex_Main
          "HOL-Library.Finite_Map"
          begin

          declare [[show_types]]
          declare [[show_sorts]]
          declare [[show_consts]]
          declare [[show_main_goal]]
          declare [[show_hyps]]

          datatype (plugins del: "size") t = A | B | C "(nat, t) fmap"

          abbreviation "tcf ≡ (λ v::(nat × nat). (λ r::nat. snd v + r))"

          interpretation tcf: comp_fun_commute tcf
          proof
          fix x y
          show "tcf y ∘ tcf x = tcf x ∘ tcf y"
          proof -
          fix z
          have "(tcf y ∘ tcf x) z = snd y + snd x + z" by auto
          also have "(tcf x ∘ tcf y) z = snd y + snd x + z" by auto
          ultimately have "(tcf y ∘ tcf x) z = (tcf x ∘ tcf y) z" by auto
          then show "(tcf y ∘ tcf x) = (tcf x ∘ tcf y)" by auto
          qed
          qed

          instantiation t :: size
          begin

          primrec t_size :: "t ⇒ nat" where
          AR: "t_size A = 0" |
          BR: "t_size B = 0" |
          CR: "t_size (C x) =
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"

          definition size_t where
          size_t_def: "size_t = t_size"

          instance ..

          end

          lemma ffold_rec_exp:
          assumes "k |∈| fmdom x"
          and "ky = (k, the (fmlookup (fmmap t_size x) k))"
          shows "ffold tcf 0 (fset_of_fmap (fmmap t_size x)) =
          tcf ky (ffold tcf 0 ((fset_of_fmap (fmmap t_size x)) |-| {|ky|}))"
          using assms tcf.ffold_rec by auto

          lemma elem_le_ffold:
          assumes "k |∈| fmdom x"
          shows "t_size (the (fmlookup x k)) <
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"
          using ffold_rec_exp assms by auto

          lemma measure_cond [intro]:
          assumes "k |∈| fmdom x"
          shows "size (the (fmlookup x k)) < size (C x)"
          using assms elem_le_ffold size_t_def by auto

          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"

          fun sup_t (infixl "⊔" 65) where
          "A ⊔ _ = A"
          | "B ⊔ x = (if x = B then B else A)"
          | "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"

          (*Examples*)

          abbreviation "list_1 ≡ fmap_of_list [(1::nat, B)]"
          abbreviation "list_2 ≡ fmap_of_list [(1::nat, A), (2::nat, A)]"
          value "(C list_1) ⊔ (C list_2)"

          abbreviation "list_3 ≡ fmap_of_list [(1::nat, B), (3::nat, A)]"
          abbreviation "list_4 ≡ fmap_of_list [(2::nat, A), (4::nat, B)]"
          value "(C list_3) ⊔ (C list_4)"

          abbreviation "list_5 ≡ fmap_of_list [(1::nat, B), (2::nat, B)]"
          abbreviation "list_6 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_5) ⊔ (C list_6)"

          abbreviation "list_7 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_8 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_7) ⊔ (C list_8)"

          abbreviation "list_9 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_10 ≡ fmap_of_list [(2::nat, C list_6), (3::nat, B)]"
          value "(C list_9) ⊔ (C list_10)"

          end





          share|improve this answer























          • Many thanks for a very detailed answer!
            – Denis
            Nov 12 at 16:46










          • This time, while answering your question, I have also acquired a substantial amount of new knowledge: thank you for providing an interesting question.
            – xanonec
            Nov 12 at 17:35






          • 1




            I have made minor amendments: it is not necessary to prove termination explicitly if measure_cond is declared as an introduction rule.
            – xanonec
            Nov 13 at 15:01













          up vote
          2
          down vote



          accepted
          +50







          up vote
          2
          down vote



          accepted
          +50




          +50




          Please find a potentially viable solution in the code listing below.





          Background



          The issue that you have encountered is described partially in the document "Defining Recursive Functions in Isabelle/HOL" written by Alexander Krauss (also known as "Tutorial on Function Definitions" in Isabelle documentation) and more comprehensively in the PhD thesis "Automating Recursive Definitions and Termination Proofs in Higher-Order Logic" that was also written by Alexander Krauss. In particular, see Chapter 4 in the tutorial and section 3.3 in the thesis.





          Size of t



          From the aforementioned references, it is possible to infer that one way to prove the termination of sup_t is to provide a suitable measure function. In this case, it is apparent that a measure function that is associated with the size of the datatype might be suitable for the application. Unfortunately, t is a nested type and (in this particular case) the default function size does not seem to capture the recursive nature of the datatype - this is not always the case (see section 3.3.2 in the thesis).



          As the first step, I provided a new size function for t. The definition is based on the total number of Cs contained within x::t (the definition should be easy to modify to suit your needs for other applications).





          Measure and Termination



          I found that the measure function (λ(xs, ys). size ys) is suitable to prove the termination of sup_t. Also, this measure function is used in Isabelle to prove the termination of sup_t if it is declared with the command fun. However, in this case, it was not possible to prove that the arguments of recursive calls indeed decrease with respect to the relation that was established by the measure automatically. However, it would be sufficient to show that "size (the (fmlookup x k)) < size (C x)".



          Unfortunately, the function supc (as stated in your question) is not self-certifying with respect to the property that the first argument that is passed to (λk x. f x (the (fmlookup ys k))) is in the domain of ys. Therefore, the (fmlookup ys k) can take the value the None. Given that this issue seems to be nearly orthogonal to the main topic of the question, I decided not to investigate it further and made an amendment to the function supc to ensure that it is guaranteed to return an element of t (you may want to prove explicitly that the function specified below is identical in its behaviour to the one that you provided in your question or, otherwise, provide a better alternative that would be self-certifying):



          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"


          After this modification, the previous goal "size (the (fmlookup x k)) < size (C x)" was changed to "(k |∈| fmdom ys) ⟹ size (the (fmlookup x k)) < size (C x)", which could be easily proven (see lemma measure_cond). If this lemma is declared as an introduction rule then the termination of sup_t can be proven automatically if it is declared with the command fun.





          Remarks



          The main reason why I decided to investigate this issue and provide an answer is that I knew very little about some of the main topics of the question and wanted to learn them. In fact, in my own work, I have never encountered a function for which termination needed to be proven manually. Furthermore, I have never used the theory Finite_Map (at least, not explicitly). Thus, I also wanted to learn about this theory and the associated datatype. As a result, my answer may be suboptimal due to the lack of experience/knowledge in these areas. Of course, if you also have doubts about whether the solution that I proposed here is optimal for the application, it may be worth trying to ask the question on the mailing list. In all honesty, I would also like to know if there is a better solution.





          theory termination_problem
          imports
          Complex_Main
          "HOL-Library.Finite_Map"
          begin

          declare [[show_types]]
          declare [[show_sorts]]
          declare [[show_consts]]
          declare [[show_main_goal]]
          declare [[show_hyps]]

          datatype (plugins del: "size") t = A | B | C "(nat, t) fmap"

          abbreviation "tcf ≡ (λ v::(nat × nat). (λ r::nat. snd v + r))"

          interpretation tcf: comp_fun_commute tcf
          proof
          fix x y
          show "tcf y ∘ tcf x = tcf x ∘ tcf y"
          proof -
          fix z
          have "(tcf y ∘ tcf x) z = snd y + snd x + z" by auto
          also have "(tcf x ∘ tcf y) z = snd y + snd x + z" by auto
          ultimately have "(tcf y ∘ tcf x) z = (tcf x ∘ tcf y) z" by auto
          then show "(tcf y ∘ tcf x) = (tcf x ∘ tcf y)" by auto
          qed
          qed

          instantiation t :: size
          begin

          primrec t_size :: "t ⇒ nat" where
          AR: "t_size A = 0" |
          BR: "t_size B = 0" |
          CR: "t_size (C x) =
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"

          definition size_t where
          size_t_def: "size_t = t_size"

          instance ..

          end

          lemma ffold_rec_exp:
          assumes "k |∈| fmdom x"
          and "ky = (k, the (fmlookup (fmmap t_size x) k))"
          shows "ffold tcf 0 (fset_of_fmap (fmmap t_size x)) =
          tcf ky (ffold tcf 0 ((fset_of_fmap (fmmap t_size x)) |-| {|ky|}))"
          using assms tcf.ffold_rec by auto

          lemma elem_le_ffold:
          assumes "k |∈| fmdom x"
          shows "t_size (the (fmlookup x k)) <
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"
          using ffold_rec_exp assms by auto

          lemma measure_cond [intro]:
          assumes "k |∈| fmdom x"
          shows "size (the (fmlookup x k)) < size (C x)"
          using assms elem_le_ffold size_t_def by auto

          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"

          fun sup_t (infixl "⊔" 65) where
          "A ⊔ _ = A"
          | "B ⊔ x = (if x = B then B else A)"
          | "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"

          (*Examples*)

          abbreviation "list_1 ≡ fmap_of_list [(1::nat, B)]"
          abbreviation "list_2 ≡ fmap_of_list [(1::nat, A), (2::nat, A)]"
          value "(C list_1) ⊔ (C list_2)"

          abbreviation "list_3 ≡ fmap_of_list [(1::nat, B), (3::nat, A)]"
          abbreviation "list_4 ≡ fmap_of_list [(2::nat, A), (4::nat, B)]"
          value "(C list_3) ⊔ (C list_4)"

          abbreviation "list_5 ≡ fmap_of_list [(1::nat, B), (2::nat, B)]"
          abbreviation "list_6 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_5) ⊔ (C list_6)"

          abbreviation "list_7 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_8 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_7) ⊔ (C list_8)"

          abbreviation "list_9 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_10 ≡ fmap_of_list [(2::nat, C list_6), (3::nat, B)]"
          value "(C list_9) ⊔ (C list_10)"

          end





          share|improve this answer














          Please find a potentially viable solution in the code listing below.





          Background



          The issue that you have encountered is described partially in the document "Defining Recursive Functions in Isabelle/HOL" written by Alexander Krauss (also known as "Tutorial on Function Definitions" in Isabelle documentation) and more comprehensively in the PhD thesis "Automating Recursive Definitions and Termination Proofs in Higher-Order Logic" that was also written by Alexander Krauss. In particular, see Chapter 4 in the tutorial and section 3.3 in the thesis.





          Size of t



          From the aforementioned references, it is possible to infer that one way to prove the termination of sup_t is to provide a suitable measure function. In this case, it is apparent that a measure function that is associated with the size of the datatype might be suitable for the application. Unfortunately, t is a nested type and (in this particular case) the default function size does not seem to capture the recursive nature of the datatype - this is not always the case (see section 3.3.2 in the thesis).



          As the first step, I provided a new size function for t. The definition is based on the total number of Cs contained within x::t (the definition should be easy to modify to suit your needs for other applications).





          Measure and Termination



          I found that the measure function (λ(xs, ys). size ys) is suitable to prove the termination of sup_t. Also, this measure function is used in Isabelle to prove the termination of sup_t if it is declared with the command fun. However, in this case, it was not possible to prove that the arguments of recursive calls indeed decrease with respect to the relation that was established by the measure automatically. However, it would be sufficient to show that "size (the (fmlookup x k)) < size (C x)".



          Unfortunately, the function supc (as stated in your question) is not self-certifying with respect to the property that the first argument that is passed to (λk x. f x (the (fmlookup ys k))) is in the domain of ys. Therefore, the (fmlookup ys k) can take the value the None. Given that this issue seems to be nearly orthogonal to the main topic of the question, I decided not to investigate it further and made an amendment to the function supc to ensure that it is guaranteed to return an element of t (you may want to prove explicitly that the function specified below is identical in its behaviour to the one that you provided in your question or, otherwise, provide a better alternative that would be self-certifying):



          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"


          After this modification, the previous goal "size (the (fmlookup x k)) < size (C x)" was changed to "(k |∈| fmdom ys) ⟹ size (the (fmlookup x k)) < size (C x)", which could be easily proven (see lemma measure_cond). If this lemma is declared as an introduction rule then the termination of sup_t can be proven automatically if it is declared with the command fun.





          Remarks



          The main reason why I decided to investigate this issue and provide an answer is that I knew very little about some of the main topics of the question and wanted to learn them. In fact, in my own work, I have never encountered a function for which termination needed to be proven manually. Furthermore, I have never used the theory Finite_Map (at least, not explicitly). Thus, I also wanted to learn about this theory and the associated datatype. As a result, my answer may be suboptimal due to the lack of experience/knowledge in these areas. Of course, if you also have doubts about whether the solution that I proposed here is optimal for the application, it may be worth trying to ask the question on the mailing list. In all honesty, I would also like to know if there is a better solution.





          theory termination_problem
          imports
          Complex_Main
          "HOL-Library.Finite_Map"
          begin

          declare [[show_types]]
          declare [[show_sorts]]
          declare [[show_consts]]
          declare [[show_main_goal]]
          declare [[show_hyps]]

          datatype (plugins del: "size") t = A | B | C "(nat, t) fmap"

          abbreviation "tcf ≡ (λ v::(nat × nat). (λ r::nat. snd v + r))"

          interpretation tcf: comp_fun_commute tcf
          proof
          fix x y
          show "tcf y ∘ tcf x = tcf x ∘ tcf y"
          proof -
          fix z
          have "(tcf y ∘ tcf x) z = snd y + snd x + z" by auto
          also have "(tcf x ∘ tcf y) z = snd y + snd x + z" by auto
          ultimately have "(tcf y ∘ tcf x) z = (tcf x ∘ tcf y) z" by auto
          then show "(tcf y ∘ tcf x) = (tcf x ∘ tcf y)" by auto
          qed
          qed

          instantiation t :: size
          begin

          primrec t_size :: "t ⇒ nat" where
          AR: "t_size A = 0" |
          BR: "t_size B = 0" |
          CR: "t_size (C x) =
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"

          definition size_t where
          size_t_def: "size_t = t_size"

          instance ..

          end

          lemma ffold_rec_exp:
          assumes "k |∈| fmdom x"
          and "ky = (k, the (fmlookup (fmmap t_size x) k))"
          shows "ffold tcf 0 (fset_of_fmap (fmmap t_size x)) =
          tcf ky (ffold tcf 0 ((fset_of_fmap (fmmap t_size x)) |-| {|ky|}))"
          using assms tcf.ffold_rec by auto

          lemma elem_le_ffold:
          assumes "k |∈| fmdom x"
          shows "t_size (the (fmlookup x k)) <
          (Suc 0) + ffold tcf 0 (fset_of_fmap (fmmap t_size x))"
          using ffold_rec_exp assms by auto

          lemma measure_cond [intro]:
          assumes "k |∈| fmdom x"
          shows "size (the (fmlookup x k)) < size (C x)"
          using assms elem_le_ffold size_t_def by auto

          abbreviation
          "supc f xs ys ≡
          fmmap_keys
          (λk x. if (k |∈| fmdom ys) then (f x (the (fmlookup ys k))) else A)
          (fmfilter (λk. k |∈| fmdom ys) xs)"

          fun sup_t (infixl "⊔" 65) where
          "A ⊔ _ = A"
          | "B ⊔ x = (if x = B then B else A)"
          | "C xs ⊔ x = (case x of C ys ⇒ C (supc sup_t xs ys) | _ ⇒ A)"

          (*Examples*)

          abbreviation "list_1 ≡ fmap_of_list [(1::nat, B)]"
          abbreviation "list_2 ≡ fmap_of_list [(1::nat, A), (2::nat, A)]"
          value "(C list_1) ⊔ (C list_2)"

          abbreviation "list_3 ≡ fmap_of_list [(1::nat, B), (3::nat, A)]"
          abbreviation "list_4 ≡ fmap_of_list [(2::nat, A), (4::nat, B)]"
          value "(C list_3) ⊔ (C list_4)"

          abbreviation "list_5 ≡ fmap_of_list [(1::nat, B), (2::nat, B)]"
          abbreviation "list_6 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_5) ⊔ (C list_6)"

          abbreviation "list_7 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_8 ≡ fmap_of_list [(2::nat, B), (4::nat, B)]"
          value "(C list_7) ⊔ (C list_8)"

          abbreviation "list_9 ≡
          fmap_of_list [(1::nat, B), (2::nat, C list_5), (3::nat, A)]"
          abbreviation "list_10 ≡ fmap_of_list [(2::nat, C list_6), (3::nat, B)]"
          value "(C list_9) ⊔ (C list_10)"

          end






          share|improve this answer














          share|improve this answer



          share|improve this answer








          edited Nov 17 at 21:33

























          answered Nov 10 at 22:51









          xanonec

          45717




          45717












          • Many thanks for a very detailed answer!
            – Denis
            Nov 12 at 16:46










          • This time, while answering your question, I have also acquired a substantial amount of new knowledge: thank you for providing an interesting question.
            – xanonec
            Nov 12 at 17:35






          • 1




            I have made minor amendments: it is not necessary to prove termination explicitly if measure_cond is declared as an introduction rule.
            – xanonec
            Nov 13 at 15:01


















          • Many thanks for a very detailed answer!
            – Denis
            Nov 12 at 16:46










          • This time, while answering your question, I have also acquired a substantial amount of new knowledge: thank you for providing an interesting question.
            – xanonec
            Nov 12 at 17:35






          • 1




            I have made minor amendments: it is not necessary to prove termination explicitly if measure_cond is declared as an introduction rule.
            – xanonec
            Nov 13 at 15:01
















          Many thanks for a very detailed answer!
          – Denis
          Nov 12 at 16:46




          Many thanks for a very detailed answer!
          – Denis
          Nov 12 at 16:46












          This time, while answering your question, I have also acquired a substantial amount of new knowledge: thank you for providing an interesting question.
          – xanonec
          Nov 12 at 17:35




          This time, while answering your question, I have also acquired a substantial amount of new knowledge: thank you for providing an interesting question.
          – xanonec
          Nov 12 at 17:35




          1




          1




          I have made minor amendments: it is not necessary to prove termination explicitly if measure_cond is declared as an introduction rule.
          – xanonec
          Nov 13 at 15:01




          I have made minor amendments: it is not necessary to prove termination explicitly if measure_cond is declared as an introduction rule.
          – xanonec
          Nov 13 at 15:01


















           

          draft saved


          draft discarded



















































           


          draft saved


          draft discarded














          StackExchange.ready(
          function () {
          StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53227525%2fhow-to-define-a-termination-order-for-the-function-with-fmmap-keys%23new-answer', 'question_page');
          }
          );

          Post as a guest















          Required, but never shown





















































          Required, but never shown














          Required, but never shown












          Required, but never shown







          Required, but never shown

































          Required, but never shown














          Required, but never shown












          Required, but never shown







          Required, but never shown







          Popular posts from this blog

          Bressuire

          Vorschmack

          Quarantine