summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Mon, 01 Mar 2010 16:58:16 -0800 | |

changeset 35490 | 63f8121c6585 |

parent 35489 | dd02201d95b6 |

child 35491 | 92e0028a46f2 |

generate take_take rules

src/HOLCF/Representable.thy | file | annotate | diff | comparison | revisions | |

src/HOLCF/Tools/Domain/domain_isomorphism.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOLCF/Representable.thy Mon Mar 01 16:36:25 2010 -0800 +++ b/src/HOLCF/Representable.thy Mon Mar 01 16:58:16 2010 -0800 @@ -187,6 +187,26 @@ shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)" by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) +lemma deflation_chain_min: + assumes chain: "chain d" + assumes defl: "\<And>i. deflation (d i)" + shows "d i\<cdot>(d j\<cdot>x) = d (min i j)\<cdot>x" +proof (rule linorder_le_cases) + assume "i \<le> j" + with chain have "d i \<sqsubseteq> d j" by (rule chain_mono) + then have "d i\<cdot>(d j\<cdot>x) = d i\<cdot>x" + by (rule deflation_below_comp1 [OF defl defl]) + moreover from `i \<le> j` have "min i j = i" by simp + ultimately show ?thesis by simp +next + assume "j \<le> i" + with chain have "d j \<sqsubseteq> d i" by (rule chain_mono) + then have "d i\<cdot>(d j\<cdot>x) = d j\<cdot>x" + by (rule deflation_below_comp2 [OF defl defl]) + moreover from `j \<le> i` have "min i j = j" by simp + ultimately show ?thesis by simp +qed + subsection {* Proving a subtype is representable *}

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 01 16:36:25 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Mar 01 16:58:16 2010 -0800 @@ -463,6 +463,18 @@ val (take_strict_thms, thy) = fold_map prove_take_strict (take_consts ~~ dnames) thy; + (* prove take/take rules *) + fun prove_take_take ((chain_take, deflation_take), dname) thy = + let + val take_take_thm = + @{thm deflation_chain_min} OF [chain_take, deflation_take]; + in + add_qualified_thm "take_take" (dname, take_take_thm) thy + end; + val (take_take_thms, thy) = + fold_map prove_take_take + (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy; + val result = { take_consts = take_consts,