src/HOL/Isar_examples/MultisetOrder.thy
changeset 7530 505f6f8e9dcf
parent 7527 9e2dddd8b81f
child 7565 bfa85f429629
equal deleted inserted replaced
7529:fa534e4f7e49 7530:505f6f8e9dcf
     8 HOL/Induct/Multiset).  Pen-and-paper proof by Wilfried Buchholz.
     8 HOL/Induct/Multiset).  Pen-and-paper proof by Wilfried Buchholz.
     9 *)
     9 *)
    10 
    10 
    11 
    11 
    12 theory MultisetOrder = Multiset:;
    12 theory MultisetOrder = Multiset:;
    13 
       
    14 (* FIXME *)
       
    15 theorems [intro!!] = disjI1 disjI2;
       
    16 
    13 
    17 
    14 
    18 lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
    15 lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
    19     (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
    16     (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
    20     (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"
    17     (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)"