Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/NTP/Multiset.ML
changeset 5132 24f992a25adc
parent 5068 fb28eaa07e01
child 12218 6597093b77e7
equal deleted inserted replaced
5131:dd4ac220b8b4 5132:24f992a25adc 
    36 
    36 
    37 Goal "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
 
    37 Goal "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
 
    38 by (res_inst_tac [("M","M")] Multiset.induction 1);
 
    38 by (res_inst_tac [("M","M")] Multiset.induction 1);
 
    39  by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
 
    39  by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
 
    40 by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
 
    40 by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
 
    41 auto();
 
    41 by Auto_tac;
 
    42 qed "countm_props";
 
    42 qed "countm_props";
 
    43 
    43 
    44 Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
 
    44 Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
 
    45   by (res_inst_tac [("M","M")] Multiset.induction 1);
 
    45   by (res_inst_tac [("M","M")] Multiset.induction 1);
 
    46   by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
 
    46   by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
isabelle