Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add transfer rule for constant List.lists
authorhuffman
Mon, 14 May 2012 17:28:07 +0200
changeset 47923 ba9df9685e7c
parent 47922 bba52dffab2b
child 47924 4e951258204b
add transfer rule for constant List.lists
src/HOL/Library/Quotient_List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Quotient_List.thy	Mon May 14 17:09:11 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Mon May 14 17:28:07 2012 +0200
@@ -176,6 +176,15 @@
   "(list_all2 A ===> set_rel A) set set"
   unfolding set_def by transfer_prover
 
+lemma lists_transfer [transfer_rule]:
+  "(set_rel A ===> set_rel (list_all2 A)) lists lists"
+  apply (rule fun_relI, rule set_relI)
+  apply (erule lists.induct, simp)
+  apply (simp only: set_rel_def list_all2_Cons1, metis lists.Cons)
+  apply (erule lists.induct, simp)
+  apply (simp only: set_rel_def list_all2_Cons2, metis lists.Cons)
+  done
+
 subsection {* Setup for lifting package *}
 
 lemma Quotient_list[quot_map]:
isabelle