move special BNFs used for composition only to BNF_Comp;
authortraytel
Thu Mar 06 14:14:54 2014 +0100 (2014-03-06)
changeset 559358f20d09d294e
parent 55934 800e155d051a
child 55936 f6591f8c629d
move special BNFs used for composition only to BNF_Comp;
use local copy of identity function that gets unfolded later for ID
src/HOL/BNF_Comp.thy
src/HOL/Basic_BNFs.thy
src/HOL/Tools/BNF/bnf_comp.ML
     1.1 --- a/src/HOL/BNF_Comp.thy	Thu Mar 06 13:36:50 2014 +0100
     1.2 +++ b/src/HOL/BNF_Comp.thy	Thu Mar 06 14:14:54 2014 +0100
     1.3 @@ -42,6 +42,17 @@
     1.4  apply (rule Card_order_cprod)
     1.5  done
     1.6  
     1.7 +lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
     1.8 +apply (erule ordIso_transitive)
     1.9 +apply (frule csum_absorb2')
    1.10 +apply (erule ordLeq_refl)
    1.11 +by simp
    1.12 +
    1.13 +lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
    1.14 +apply (erule ordIso_transitive)
    1.15 +apply (rule cprod_infinite)
    1.16 +by simp
    1.17 +
    1.18  lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
    1.19  by simp
    1.20  
    1.21 @@ -128,22 +139,28 @@
    1.22  
    1.23  end
    1.24  
    1.25 -definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp = (\<lambda>x. x)"
    1.26 +bnf DEADID: 'a
    1.27 +  map: "id :: 'a \<Rightarrow> 'a"
    1.28 +  bd: natLeq
    1.29 +  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.30 +by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
    1.31 +
    1.32 +definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
    1.33 +
    1.34 +bnf ID: 'a
    1.35 +  map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.36 +  sets: "\<lambda>x. {x}"
    1.37 +  bd: natLeq
    1.38 +  rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    1.39 +unfolding id_bnf_comp_def
    1.40 +apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    1.41 +apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    1.42 +apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    1.43 +done
    1.44  
    1.45  lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
    1.46    unfolding id_bnf_comp_def by unfold_locales auto
    1.47  
    1.48 -lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
    1.49 -apply (erule ordIso_transitive)
    1.50 -apply (frule csum_absorb2')
    1.51 -apply (erule ordLeq_refl)
    1.52 -by simp
    1.53 -
    1.54 -lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
    1.55 -apply (erule ordIso_transitive)
    1.56 -apply (rule cprod_infinite)
    1.57 -by simp
    1.58 -
    1.59  ML_file "Tools/BNF/bnf_comp_tactics.ML"
    1.60  ML_file "Tools/BNF/bnf_comp.ML"
    1.61  
     2.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:50 2014 +0100
     2.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 14:14:54 2014 +0100
     2.3 @@ -13,22 +13,6 @@
     2.4  imports BNF_Def
     2.5  begin
     2.6  
     2.7 -bnf ID: 'a
     2.8 -  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     2.9 -  sets: "\<lambda>x. {x}"
    2.10 -  bd: natLeq
    2.11 -  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    2.12 -apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
    2.13 -apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
    2.14 -apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
    2.15 -done
    2.16 -
    2.17 -bnf DEADID: 'a
    2.18 -  map: "id :: 'a \<Rightarrow> 'a"
    2.19 -  bd: natLeq
    2.20 -  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.21 -by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
    2.22 -
    2.23  definition setl :: "'a + 'b \<Rightarrow> 'a set" where
    2.24  "setl x = (case x of Inl z => {z} | _ => {})"
    2.25  
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 13:36:50 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 14:14:54 2014 +0100
     3.3 @@ -56,8 +56,8 @@
     3.4  open BNF_Tactics
     3.5  open BNF_Comp_Tactics
     3.6  
     3.7 -val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
     3.8 -val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
     3.9 +val ID_bnf = the (bnf_of @{context} "BNF_Comp.ID");
    3.10 +val DEADID_bnf = the (bnf_of @{context} "BNF_Comp.DEADID");
    3.11  
    3.12  type comp_cache = (bnf * (typ list * typ list)) Typtab.table;
    3.13  
    3.14 @@ -109,6 +109,8 @@
    3.15  fun mk_permuteN src dest =
    3.16    "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
    3.17  
    3.18 +val id_bnf_comp_def = @{thm id_bnf_comp_def}
    3.19 +
    3.20  (*copied from Envir.expand_term_free*)
    3.21  fun expand_term_const defs =
    3.22    let
    3.23 @@ -339,9 +341,9 @@
    3.24          Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
    3.25  
    3.26      val phi =
    3.27 -      Morphism.thm_morphism "BNF" (unfold_thms lthy' @{thms id_bnf_comp_def})
    3.28 +      Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
    3.29        $> Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy')
    3.30 -        @{thms id_bnf_comp_def[abs_def]} []);
    3.31 +        [id_bnf_comp_def] []);
    3.32  
    3.33      val bnf'' = morph_bnf phi bnf';
    3.34    in
    3.35 @@ -761,19 +763,21 @@
    3.36        |> mk_Frees' "f" (map2 (curry op -->) As Bs)
    3.37        ||>> mk_Frees' "R" (map2 mk_pred2T As Bs)
    3.38  
    3.39 +    val expand_id_bnf_comp_def =
    3.40 +      expand_term_const [Thm.prop_of id_bnf_comp_def |> Logic.dest_equals]
    3.41      val map_unfolds = #map_unfolds unfold_set;
    3.42      val set_unfoldss = #set_unfoldss unfold_set;
    3.43      val rel_unfolds = #rel_unfolds unfold_set;
    3.44  
    3.45 -    val expand_maps =
    3.46 +    val expand_maps = expand_id_bnf_comp_def o
    3.47        fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds);
    3.48      val expand_sets =
    3.49        fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss);
    3.50 -    val expand_rels =
    3.51 +    val expand_rels = expand_id_bnf_comp_def o
    3.52        fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds);
    3.53 -    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) map_unfolds;
    3.54 +    fun unfold_maps ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: map_unfolds);
    3.55      fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss;
    3.56 -    fun unfold_rels ctxt = unfold_thms ctxt rel_unfolds;
    3.57 +    fun unfold_rels ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: rel_unfolds);
    3.58      fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
    3.59  
    3.60      val repTA = mk_T_of_bnf Ds As bnf;
    3.61 @@ -854,7 +858,7 @@
    3.62  
    3.63      val bnf_wits = map (fn (I, t) =>
    3.64          fold Term.absdummy (map (nth As) I)
    3.65 -          (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
    3.66 +          (AbsA $ Term.list_comb (expand_id_bnf_comp_def t, map Bound (0 upto length I - 1))))
    3.67        (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
    3.68  
    3.69      fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN