diff -r c15eea8d20af -r 95371a8b17e1 LamEx.thy --- a/LamEx.thy Fri Dec 04 17:50:02 2009 +0100 +++ b/LamEx.thy Fri Dec 04 17:57:03 2009 +0100 @@ -250,50 +250,3 @@ apply(simp add: var_supp) done - - - - - - - - - - - -(* Construction Site code *) - - -fun - option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" -where - "option_map f (nSome x) = nSome (f x)" -| "option_map f nNone = nNone" - -fun - option_rel -where - "option_rel r (nSome x) (nSome y) = r x y" -| "option_rel r _ _ = False" - -declare [[map noption = (option_map, option_rel)]] - -lemma "option_map id = id" -sorry - -lemma option_Quotient: - assumes q: "Quotient R Abs Rep" - shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" - apply (unfold Quotient_def) - apply (auto) - using q - apply (unfold Quotient_def) - apply (case_tac "a :: 'b noption") - apply (simp) - apply (simp) - apply (case_tac "a :: 'b noption") - apply (simp only: option_map.simps) - apply (subst option_rel.simps) - (* Simp starts hanging so don't know how to continue *) - sorry -