# HG changeset patch # User traytel # Date 1394111694 -3600 # Node ID 8f20d09d294ef51c6da55f60a5d3f6e0231a6eed # Parent 800e155d051a115ef947af20634b20f27a8e248a move special BNFs used for composition only to BNF_Comp; use local copy of identity function that gets unfolded later for ID diff -r 800e155d051a -r 8f20d09d294e src/HOL/BNF_Comp.thy --- a/src/HOL/BNF_Comp.thy Thu Mar 06 13:36:50 2014 +0100 +++ b/src/HOL/BNF_Comp.thy Thu Mar 06 14:14:54 2014 +0100 @@ -42,6 +42,17 @@ apply (rule Card_order_cprod) done +lemma csum_dup: "cinfinite r \ Card_order r \ p +c p' =o r +c r \ p +c p' =o r" +apply (erule ordIso_transitive) +apply (frule csum_absorb2') +apply (erule ordLeq_refl) +by simp + +lemma cprod_dup: "cinfinite r \ Card_order r \ p *c p' =o r *c r \ p *c p' =o r" +apply (erule ordIso_transitive) +apply (rule cprod_infinite) +by simp + lemma Union_image_insert: "\(f ` insert a B) = f a \ \(f ` B)" by simp @@ -128,22 +139,28 @@ end -definition id_bnf_comp :: "'a \ 'a" where "id_bnf_comp = (\x. x)" +bnf DEADID: 'a + map: "id :: 'a \ 'a" + bd: natLeq + rel: "op = :: 'a \ 'a \ bool" +by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) + +definition id_bnf_comp :: "'a \ 'a" where "id_bnf_comp \ (\x. x)" + +bnf ID: 'a + map: "id_bnf_comp :: ('a \ 'b) \ 'a \ 'b" + sets: "\x. {x}" + bd: natLeq + rel: "id_bnf_comp :: ('a \ 'b \ bool) \ 'a \ 'b \ bool" +unfolding id_bnf_comp_def +apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) +apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) +apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] +done lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV" unfolding id_bnf_comp_def by unfold_locales auto -lemma csum_dup: "cinfinite r \ Card_order r \ p +c p' =o r +c r \ p +c p' =o r" -apply (erule ordIso_transitive) -apply (frule csum_absorb2') -apply (erule ordLeq_refl) -by simp - -lemma cprod_dup: "cinfinite r \ Card_order r \ p *c p' =o r *c r \ p *c p' =o r" -apply (erule ordIso_transitive) -apply (rule cprod_infinite) -by simp - ML_file "Tools/BNF/bnf_comp_tactics.ML" ML_file "Tools/BNF/bnf_comp.ML" diff -r 800e155d051a -r 8f20d09d294e src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Thu Mar 06 13:36:50 2014 +0100 +++ b/src/HOL/Basic_BNFs.thy Thu Mar 06 14:14:54 2014 +0100 @@ -13,22 +13,6 @@ imports BNF_Def begin -bnf ID: 'a - map: "id :: ('a \ 'b) \ 'a \ 'b" - sets: "\x. {x}" - bd: natLeq - rel: "id :: ('a \ 'b \ bool) \ 'a \ 'b \ bool" -apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) -apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) -apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] -done - -bnf DEADID: 'a - map: "id :: 'a \ 'a" - bd: natLeq - rel: "op = :: 'a \ 'a \ bool" -by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) - definition setl :: "'a + 'b \ 'a set" where "setl x = (case x of Inl z => {z} | _ => {})" diff -r 800e155d051a -r 8f20d09d294e src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Thu Mar 06 13:36:50 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Thu Mar 06 14:14:54 2014 +0100 @@ -56,8 +56,8 @@ open BNF_Tactics open BNF_Comp_Tactics -val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID"); -val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID"); +val ID_bnf = the (bnf_of @{context} "BNF_Comp.ID"); +val DEADID_bnf = the (bnf_of @{context} "BNF_Comp.DEADID"); type comp_cache = (bnf * (typ list * typ list)) Typtab.table; @@ -109,6 +109,8 @@ fun mk_permuteN src dest = "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest); +val id_bnf_comp_def = @{thm id_bnf_comp_def} + (*copied from Envir.expand_term_free*) fun expand_term_const defs = let @@ -339,9 +341,9 @@ Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy; val phi = - Morphism.thm_morphism "BNF" (unfold_thms lthy' @{thms id_bnf_comp_def}) + Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def]) $> Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy') - @{thms id_bnf_comp_def[abs_def]} []); + [id_bnf_comp_def] []); val bnf'' = morph_bnf phi bnf'; in @@ -761,19 +763,21 @@ |> mk_Frees' "f" (map2 (curry op -->) As Bs) ||>> mk_Frees' "R" (map2 mk_pred2T As Bs) + val expand_id_bnf_comp_def = + expand_term_const [Thm.prop_of id_bnf_comp_def |> Logic.dest_equals] val map_unfolds = #map_unfolds unfold_set; val set_unfoldss = #set_unfoldss unfold_set; val rel_unfolds = #rel_unfolds unfold_set; - val expand_maps = + val expand_maps = expand_id_bnf_comp_def o fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds); val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss); - val expand_rels = + val expand_rels = expand_id_bnf_comp_def o fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds); - fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds; + fun unfold_maps ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: map_unfolds); fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss; - fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds; + fun unfold_rels ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: rel_unfolds); fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt; val repTA = mk_T_of_bnf Ds As bnf; @@ -854,7 +858,7 @@ val bnf_wits = map (fn (I, t) => fold Term.absdummy (map (nth As) I) - (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1)))) + (AbsA $ Term.list_comb (expand_id_bnf_comp_def t, map Bound (0 upto length I - 1)))) (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN