Mercurial Mercurial > hg > nominal2 / 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.
Nominal/FSet.thy
changeset 1907 7b74cf843942
parent 1905 dbc9e88c44da
child 1909 9972dc5bd7ad
equal deleted inserted replaced
1905:dbc9e88c44da 1907:7b74cf843942 
   561 
   561 
   562 quotient_definition
 
   562 quotient_definition
 
   563   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
 
   563   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
 
   564   is "ffold_raw"
 
   564   is "ffold_raw"
 
   565 
   565 
   566 lemma funion_sym_pre:
 
       
   567   "xs @ ys \<approx> ys @ xs"
 
       
   568   by auto
 
       
   569 
       
   570 lemma set_cong: 
   566 lemma set_cong: 
   571   shows "(set x = set y) = (x \<approx> y)"
 
   567   shows "(set x = set y) = (x \<approx> y)"
 
   572   by auto
 
   568   by auto
 
   573 
   569 
   574 lemma inj_map_eq_iff:
 
   570 lemma inj_map_eq_iff:
 
   758 
   754 
   759 lemma funion_empty[simp]:
 
   755 lemma funion_empty[simp]:
 
   760   shows "S |\<union>| {||} = S"
 
   756   shows "S |\<union>| {||} = S"
 
   761   by (lifting append_Nil2)
 
   757   by (lifting append_Nil2)
 
   762 
   758 
   763 lemma funion_sym:
 
   759 thm sup.commute[where 'a="'a fset"]
 
   764   shows "S |\<union>| T = T |\<union>| S"
 
   760 
   765   by (lifting funion_sym_pre)
 
   761 thm sup.assoc[where 'a="'a fset"]
 
   766 
       
   767 lemma funion_assoc:
 
       
   768   shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
 
       
   769   by (lifting append_assoc)
 
       
   770 
   762 
   771 lemma singleton_union_left:
 
   763 lemma singleton_union_left:
 
   772   "{|a|} |\<union>| S = finsert a S"
 
   764   "{|a|} |\<union>| S = finsert a S"
 
   773   by simp
 
   765   by simp
 
   774 
   766 
   775 lemma singleton_union_right:
 
   767 lemma singleton_union_right:
 
   776   "S |\<union>| {|a|} = finsert a S"
 
   768   "S |\<union>| {|a|} = finsert a S"
 
   777   by (subst funion_sym) simp
 
   769   by (subst sup.commute) simp
 
   778 
   770 
   779 section {* Induction and Cases rules for finite sets *}
 
   771 section {* Induction and Cases rules for finite sets *}
 
   780 
   772 
   781 lemma fset_strong_cases:
 
   773 lemma fset_strong_cases:
 
   782   "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
 
   774   "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
nominal2