src/HOL/List.thy
changeset 56525 b5b6ad5dc2ae
parent 56520 3373f5d1e074
child 56527 907f04603177
equal deleted inserted replaced
56524:f4ba736040fa 56525:b5b6ad5dc2ae
  6576   by (simp add: wf_iff_acyclic_if_finite)
  6576   by (simp add: wf_iff_acyclic_if_finite)
  6577 
  6577 
  6578 
  6578 
  6579 subsection {* Setup for Lifting/Transfer *}
  6579 subsection {* Setup for Lifting/Transfer *}
  6580 
  6580 
  6581 subsubsection {* Relator and predicator properties *}
       
  6582 
       
  6583 lemma list_all2_eq'[relator_eq]:
       
  6584   "list_all2 (op =) = (op =)"
       
  6585 by (rule ext)+ (simp add: list_all2_eq)
       
  6586 
       
  6587 lemma list_all2_mono'[relator_mono]:
       
  6588   assumes "A \<le> B"
       
  6589   shows "(list_all2 A) \<le> (list_all2 B)"
       
  6590 using assms by (auto intro: list_all2_mono)
       
  6591 
       
  6592 lemma list_all2_OO[relator_distr]: "list_all2 A OO list_all2 B = list_all2 (A OO B)"
       
  6593 proof (intro ext iffI)
       
  6594   fix xs ys
       
  6595   assume "list_all2 (A OO B) xs ys"
       
  6596   thus "(list_all2 A OO list_all2 B) xs ys"
       
  6597     unfolding OO_def
       
  6598     by (induct, simp, simp add: list_all2_Cons1 list_all2_Cons2, fast)
       
  6599 next
       
  6600   fix xs ys
       
  6601   assume "(list_all2 A OO list_all2 B) xs ys"
       
  6602   then obtain zs where "list_all2 A xs zs" and "list_all2 B zs ys" ..
       
  6603   thus "list_all2 (A OO B) xs ys"
       
  6604     by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
       
  6605 qed
       
  6606 
       
  6607 lemma Domainp_list[relator_domain]:
       
  6608   "Domainp (list_all2 A) = (list_all (Domainp A))"
       
  6609 proof -
       
  6610   {
       
  6611     fix x
       
  6612     have *: "\<And>x. (\<exists>y. A x y) = Domainp A x" unfolding Domainp_iff by blast
       
  6613     have "(\<exists>y. (list_all2 A x y)) = list_all (Domainp A) x"
       
  6614     by (induction x) (simp_all add: * list_all2_Cons1)
       
  6615   }
       
  6616   then show ?thesis
       
  6617   unfolding Domainp_iff[abs_def]
       
  6618   by (auto iff: fun_eq_iff)
       
  6619 qed 
       
  6620 
       
  6621 lemma left_total_list_all2[transfer_rule]:
       
  6622   "left_total R \<Longrightarrow> left_total (list_all2 R)"
       
  6623   unfolding left_total_def
       
  6624   apply safe
       
  6625   apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
       
  6626 done
       
  6627 
       
  6628 lemma left_unique_list_all2 [transfer_rule]:
       
  6629   "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
       
  6630   unfolding left_unique_def
       
  6631   apply (subst (2) all_comm, subst (1) all_comm)
       
  6632   apply (rule allI, rename_tac zs, induct_tac zs)
       
  6633   apply (auto simp add: list_all2_Cons2)
       
  6634   done
       
  6635 
       
  6636 lemma right_total_list_all2 [transfer_rule]:
       
  6637   "right_total R \<Longrightarrow> right_total (list_all2 R)"
       
  6638   unfolding right_total_def
       
  6639   by (rule allI, induct_tac y, simp, simp add: list_all2_Cons2)
       
  6640 
       
  6641 lemma right_unique_list_all2 [transfer_rule]:
       
  6642   "right_unique R \<Longrightarrow> right_unique (list_all2 R)"
       
  6643   unfolding right_unique_def
       
  6644   apply (rule allI, rename_tac xs, induct_tac xs)
       
  6645   apply (auto simp add: list_all2_Cons1)
       
  6646   done
       
  6647 
       
  6648 lemma bi_total_list_all2 [transfer_rule]:
       
  6649   "bi_total A \<Longrightarrow> bi_total (list_all2 A)"
       
  6650   unfolding bi_total_def
       
  6651   apply safe
       
  6652   apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
       
  6653   apply (rename_tac ys, induct_tac ys, simp, simp add: list_all2_Cons2)
       
  6654   done
       
  6655 
       
  6656 lemma bi_unique_list_all2 [transfer_rule]:
       
  6657   "bi_unique A \<Longrightarrow> bi_unique (list_all2 A)"
       
  6658   unfolding bi_unique_def
       
  6659   apply (rule conjI)
       
  6660   apply (rule allI, rename_tac xs, induct_tac xs)
       
  6661   apply (simp, force simp add: list_all2_Cons1)
       
  6662   apply (subst (2) all_comm, subst (1) all_comm)
       
  6663   apply (rule allI, rename_tac xs, induct_tac xs)
       
  6664   apply (simp, force simp add: list_all2_Cons2)
       
  6665   done
       
  6666 
       
  6667 lemma list_relator_eq_onp [relator_eq_onp]:
       
  6668   "list_all2 (eq_onp P) = eq_onp (list_all P)"
       
  6669   apply (simp add: fun_eq_iff list_all2_iff list_all_iff eq_onp_def Ball_def) 
       
  6670   apply (intro allI) 
       
  6671   apply (induct_tac rule: list_induct2') 
       
  6672   apply simp_all 
       
  6673   apply fastforce
       
  6674 done
       
  6675 
       
  6676 subsubsection {* Quotient theorem for the Lifting package *}
       
  6677 
       
  6678 lemma Quotient_list[quot_map]:
       
  6679   assumes "Quotient R Abs Rep T"
       
  6680   shows "Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"
       
  6681 proof (unfold Quotient_alt_def, intro conjI allI impI)
       
  6682   from assms have 1: "\<And>x y. T x y \<Longrightarrow> Abs x = y"
       
  6683     unfolding Quotient_alt_def by simp
       
  6684   fix xs ys assume "list_all2 T xs ys" thus "map Abs xs = ys"
       
  6685     by (induct, simp, simp add: 1)
       
  6686 next
       
  6687   from assms have 2: "\<And>x. T (Rep x) x"
       
  6688     unfolding Quotient_alt_def by simp
       
  6689   fix xs show "list_all2 T (map Rep xs) xs"
       
  6690     by (induct xs, simp, simp add: 2)
       
  6691 next
       
  6692   from assms have 3: "\<And>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y"
       
  6693     unfolding Quotient_alt_def by simp
       
  6694   fix xs ys show "list_all2 R xs ys \<longleftrightarrow> list_all2 T xs (map Abs xs) \<and>
       
  6695     list_all2 T ys (map Abs ys) \<and> map Abs xs = map Abs ys"
       
  6696     by (induct xs ys rule: list_induct2', simp_all, metis 3)
       
  6697 qed
       
  6698 
       
  6699 subsubsection {* Transfer rules for the Transfer package *}
  6581 subsubsection {* Transfer rules for the Transfer package *}
  6700 
  6582 
  6701 context
  6583 context
  6702 begin
  6584 begin
  6703 interpretation lifting_syntax .
  6585 interpretation lifting_syntax .