# HG changeset patch # User huffman # Date 1267294367 28800 # Node ID deaf221c4a59f61dfc4de2f37c946918a3bd9155 # Parent d63655b8836905a1d14cf74865a7ad2707bc0053 moved proofs of dist_les and dist_eqs to domain_constructors.ML diff -r d63655b88369 -r deaf221c4a59 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 08:30:11 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 10:12:47 2010 -0800 @@ -21,6 +21,8 @@ con_rews : thm list, inverts : thm list, injects : thm list, + dist_les : thm list, + dist_eqs : thm list, sel_rews : thm list } * theory; end; @@ -508,6 +510,48 @@ in map (fn c => pgterm mk_eq c (K tacs)) cons' end; end; + (* prove distinctness of constructors *) + local + fun map_dist (f : 'a -> 'a -> 'b) (xs : 'a list) : 'b list = + flat (map_index (fn (i, x) => map (f x) (nth_drop i xs)) xs); + fun prime (Free (n, T)) = Free (n^"'", T) + | prime t = t; + fun iff_disj (t, []) = mk_not t + | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts); + fun iff_disj2 (t, [], us) = mk_not t + | iff_disj2 (t, ts, []) = mk_not t + | iff_disj2 (t, ts, us) = + mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us)); + fun dist_le (con1, args1) (con2, args2) = + let + val vs1 = vars_of args1; + val vs2 = map prime (vars_of args2); + val zs1 = map snd (filter_out (fst o fst) (args1 ~~ vs1)); + val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2)); + val rhss = map mk_undef zs1; + val goal = mk_trp (iff_disj (lhs, rhss)); + val rule1 = iso_locale RS @{thm iso.abs_below}; + val rules = rule1 :: @{thms con_below_iff_rules}; + val tacs = [simp_tac (HOL_ss addsimps rules) 1]; + in prove thy con_betas goal (K tacs) end; + fun dist_eq (con1, args1) (con2, args2) = + let + val vs1 = vars_of args1; + val vs2 = map prime (vars_of args2); + val zs1 = map snd (filter_out (fst o fst) (args1 ~~ vs1)); + val zs2 = map snd (filter_out (fst o fst) (args2 ~~ vs2)); + val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2)); + val rhss1 = map mk_undef zs1; + val rhss2 = map mk_undef zs2; + val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2)); + val rule1 = iso_locale RS @{thm iso.abs_eq}; + val rules = rule1 :: @{thms con_eq_iff_rules}; + val tacs = [simp_tac (HOL_ss addsimps rules) 1]; + in prove thy con_betas goal (K tacs) end; + in + val dist_les = map_dist dist_le spec'; + val dist_eqs = map_dist dist_eq spec'; + end; val result = { @@ -518,7 +562,9 @@ con_compacts = con_compacts, con_rews = con_rews, inverts = inverts, - injects = injects + injects = injects, + dist_les = dist_les, + dist_eqs = dist_eqs }; in (result, thy) @@ -721,6 +767,8 @@ con_rews = #con_rews con_result, inverts = #inverts con_result, injects = #injects con_result, + dist_les = #dist_les con_result, + dist_eqs = #dist_eqs con_result, sel_rews = sel_thms }; in (result, thy) diff -r d63655b88369 -r deaf221c4a59 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 08:30:11 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 10:12:47 2010 -0800 @@ -199,7 +199,7 @@ val con_appls = #con_betas result; val {exhaust, casedist, ...} = result; -val {con_compacts, con_rews, inverts, injects, ...} = result; +val {con_compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result; val {sel_rews, ...} = result; @@ -374,64 +374,6 @@ val pat_rews = pat_stricts @ pat_apps; end; -val _ = trace " Proving dist_les..."; -val dist_les = - let - fun dist (con1, args1) (con2, args2) = - let - fun iff_disj (t, []) = HOLogic.mk_not t - | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts; - val lhs = con_app con1 args1 << con_app con2 args2; - val rhss = map (fn x => %:x === UU) (nonlazy args1); - val goal = mk_trp (iff_disj (lhs, rhss)); - val rule1 = iso_locale RS @{thm iso.abs_below}; - val rules = rule1 :: @{thms con_below_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; - - fun distinct (con1, _, args1) (con2, _, args2) = - let - val arg1 = (con1, args1); - val arg2 = - (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) - (args2, Name.variant_list (map vname args1) (map vname args2))); - in [dist arg1 arg2, dist arg2 arg1] end; - fun distincts [] = [] - | distincts (c::cs) = maps (distinct c) cs @ distincts cs; - in distincts cons end; - -val _ = trace " Proving dist_eqs..."; -val dist_eqs = - let - fun dist (con1, args1) (con2, args2) = - let - fun iff_disj (t, [], us) = HOLogic.mk_not t - | iff_disj (t, ts, []) = HOLogic.mk_not t - | iff_disj (t, ts, us) = - let - val disj1 = foldr1 HOLogic.mk_disj ts; - val disj2 = foldr1 HOLogic.mk_disj us; - in t === HOLogic.mk_conj (disj1, disj2) end; - val lhs = con_app con1 args1 === con_app con2 args2; - val rhss1 = map (fn x => %:x === UU) (nonlazy args1); - val rhss2 = map (fn x => %:x === UU) (nonlazy args2); - val goal = mk_trp (iff_disj (lhs, rhss1, rhss2)); - val rule1 = iso_locale RS @{thm iso.abs_eq}; - val rules = rule1 :: @{thms con_eq_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; - - fun distinct (con1, _, args1) (con2, _, args2) = - let - val arg1 = (con1, args1); - val arg2 = - (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) - (args2, Name.variant_list (map vname args1) (map vname args2))); - in [dist arg1 arg2, dist arg2 arg1] end; - fun distincts [] = [] - | distincts (c::cs) = maps (distinct c) cs @ distincts cs; - in distincts cons end; - (* ----- theorems concerning one induction step ----------------------------- *) val copy_strict =