tweaked setup for datatype realizer
authorblanchet
Thu Sep 04 11:20:59 2014 +0200 (2014-09-04)
changeset 5818282478e6c60cb
parent 58181 6d527272f7b2
child 58183 285fbec02fb0
tweaked setup for datatype realizer
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Old_Datatype.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/local_interpretation.ML
src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 04 09:02:43 2014 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 04 11:20:59 2014 +0200
     1.3 @@ -188,6 +188,7 @@
     1.4  ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
     1.5  ML_file "Tools/BNF/bnf_lfp_size.ML"
     1.6  ML_file "Tools/Function/old_size.ML"
     1.7 +ML_file "Tools/Old_Datatype/old_datatype_realizer.ML"
     1.8  
     1.9  lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    1.10    by (cases b) auto
     2.1 --- a/src/HOL/Old_Datatype.thy	Thu Sep 04 09:02:43 2014 +0200
     2.2 +++ b/src/HOL/Old_Datatype.thy	Thu Sep 04 11:20:59 2014 +0200
     2.3 @@ -526,7 +526,4 @@
     2.4  ML_file "Tools/inductive_realizer.ML"
     2.5  setup InductiveRealizer.setup
     2.6  
     2.7 -ML_file "Tools/Old_Datatype/old_datatype_realizer.ML"
     2.8 -setup Old_Datatype_Realizer.setup
     2.9 -
    2.10  end
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 04 09:02:43 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 04 11:20:59 2014 +0200
     3.3 @@ -41,6 +41,8 @@
     3.4    val fp_sugars_of_global: theory -> fp_sugar list
     3.5    val fp_sugar_interpretation: (fp_sugar list -> theory -> theory) ->
     3.6      (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
     3.7 +  val interpret_fp_sugars: fp_sugar list -> local_theory -> local_theory
     3.8 +  val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
     3.9    val register_fp_sugars: fp_sugar list -> local_theory -> local_theory
    3.10  
    3.11    val co_induct_of: 'a list -> 'a
    3.12 @@ -229,13 +231,16 @@
    3.13    |> Sign.restore_naming thy;
    3.14  
    3.15  val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
    3.16 +val interpret_fp_sugars = FP_Sugar_Interpretation.data;
    3.17  
    3.18 -fun register_fp_sugars fp_sugars =
    3.19 +fun register_fp_sugars_raw fp_sugars =
    3.20    fold (fn fp_sugar as {T = Type (s, _), ...} =>
    3.21        Local_Theory.declaration {syntax = false, pervasive = true}
    3.22          (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
    3.23 -    fp_sugars
    3.24 -  #> FP_Sugar_Interpretation.data fp_sugars;
    3.25 +    fp_sugars;
    3.26 +
    3.27 +fun register_fp_sugars fp_sugars =
    3.28 +  register_fp_sugars fp_sugars #> interpret_fp_sugars fp_sugars;
    3.29  
    3.30  fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
    3.31      live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
    3.32 @@ -255,8 +260,9 @@
    3.33           rel_distincts = nth rel_distinctss kk}
    3.34          |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
    3.35    in
    3.36 -    fold interpret_bnf (#bnfs fp_res)
    3.37 -    #> register_fp_sugars fp_sugars
    3.38 +    register_fp_sugars_raw fp_sugars
    3.39 +    #> fold interpret_bnf (#bnfs fp_res)
    3.40 +    #> interpret_fp_sugars fp_sugars
    3.41    end;
    3.42  
    3.43  (* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
     4.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Sep 04 09:02:43 2014 +0200
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Sep 04 11:20:59 2014 +0200
     4.3 @@ -1025,7 +1025,7 @@
     4.4                       (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
     4.5                    I)
     4.6            |> Local_Theory.notes (anonymous_notes @ notes)
     4.7 -          (* for "datatype_realizer.ML": *)
     4.8 +          (* for "old_datatype_realizer.ML": *)
     4.9            |>> name_noted_thms fcT_name exhaustN;
    4.10  
    4.11          val ctr_sugar =
     5.1 --- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Thu Sep 04 09:02:43 2014 +0200
     5.2 +++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Thu Sep 04 11:20:59 2014 +0200
     5.3 @@ -42,11 +42,13 @@
     5.4      val (data, interps) = Interp.get thy;
     5.5      val unfinished = interps |> map (fn ((gf, _), xs) =>
     5.6        (g_or_f gf, if eq_list eq (xs, data) then [] else subtract eq xs data));
     5.7 -    val finished = interps |> map (fn (interp, _) => (interp, data));
     5.8 +    val finished = interps |> map (apsnd (K data));
     5.9    in
    5.10 -    if forall (null o #2) unfinished then NONE
    5.11 -    else SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
    5.12 -      |> lift_lthy (Interp.put (data, finished)))
    5.13 +    if forall (null o #2) unfinished then
    5.14 +      NONE
    5.15 +    else
    5.16 +      SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
    5.17 +        |> lift_lthy (Interp.put (data, finished)))
    5.18    end;
    5.19  
    5.20  fun consolidate lthy =
     6.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML	Thu Sep 04 09:02:43 2014 +0200
     6.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML	Thu Sep 04 11:20:59 2014 +0200
     6.3 @@ -8,7 +8,6 @@
     6.4  signature OLD_DATATYPE_REALIZER =
     6.5  sig
     6.6    val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
     6.7 -  val setup: theory -> theory
     6.8  end;
     6.9  
    6.10  structure Old_Datatype_Realizer : OLD_DATATYPE_REALIZER =
    6.11 @@ -158,9 +157,7 @@
    6.12  
    6.13    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    6.14  
    6.15 -
    6.16 -fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info)
    6.17 -    thy =
    6.18 +fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
    6.19    let
    6.20      val ctxt = Proof_Context.init_global thy;
    6.21      val cert = cterm_of thy;
    6.22 @@ -241,6 +238,6 @@
    6.23        |> fold_rev make_casedists infos
    6.24      end;
    6.25  
    6.26 -val setup = Old_Datatype_Data.interpretation add_dt_realizers;
    6.27 +val _ = Theory.setup (Old_Datatype_Data.interpretation add_dt_realizers);
    6.28  
    6.29  end;
     7.1 --- a/src/HOL/Transfer.thy	Thu Sep 04 09:02:43 2014 +0200
     7.2 +++ b/src/HOL/Transfer.thy	Thu Sep 04 11:20:59 2014 +0200
     7.3 @@ -9,8 +9,8 @@
     7.4  imports Hilbert_Choice Metis Option
     7.5  begin
     7.6  
     7.7 -(* We include Option here although it's not needed here. 
     7.8 -   By doing this, we avoid a diamond problem for BNF and 
     7.9 +(* We import Option here although it's not needed here.
    7.10 +   By doing this, we avoid a diamond problem for BNF and
    7.11     FP sugar interpretation defined in this file. *)
    7.12  
    7.13  subsection {* Relator for function space *}
    7.14 @@ -227,18 +227,18 @@
    7.15  
    7.16  subsection {* Equality restricted by a predicate *}
    7.17  
    7.18 -definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
    7.19 +definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    7.20    where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
    7.21  
    7.22 -lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id" 
    7.23 -unfolding eq_onp_def Grp_def by auto 
    7.24 +lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"
    7.25 +unfolding eq_onp_def Grp_def by auto
    7.26  
    7.27  lemma eq_onp_to_eq:
    7.28    assumes "eq_onp P x y"
    7.29    shows "x = y"
    7.30  using assms by (simp add: eq_onp_def)
    7.31  
    7.32 -lemma eq_onp_top_eq_eq: "eq_onp top = op=" 
    7.33 +lemma eq_onp_top_eq_eq: "eq_onp top = op="
    7.34  by (simp add: eq_onp_def)
    7.35  
    7.36  lemma eq_onp_same_args:
    7.37 @@ -298,10 +298,10 @@
    7.38  
    7.39  subsection {* Properties of relators *}
    7.40  
    7.41 -lemma left_total_eq[transfer_rule]: "left_total op=" 
    7.42 +lemma left_total_eq[transfer_rule]: "left_total op="
    7.43    unfolding left_total_def by blast
    7.44  
    7.45 -lemma left_unique_eq[transfer_rule]: "left_unique op=" 
    7.46 +lemma left_unique_eq[transfer_rule]: "left_unique op="
    7.47    unfolding left_unique_def by blast
    7.48  
    7.49  lemma right_total_eq [transfer_rule]: "right_total op="
    7.50 @@ -366,7 +366,7 @@
    7.51  
    7.52  end
    7.53  
    7.54 -ML_file "Tools/Transfer/transfer_bnf.ML" 
    7.55 +ML_file "Tools/Transfer/transfer_bnf.ML"
    7.56  
    7.57  declare pred_fun_def [simp]
    7.58  declare rel_fun_eq [relator_eq]
    7.59 @@ -486,13 +486,13 @@
    7.60    shows "((A ===> B) ===> op=) mono mono"
    7.61  unfolding mono_def[abs_def] by transfer_prover
    7.62  
    7.63 -lemma right_total_relcompp_transfer[transfer_rule]: 
    7.64 +lemma right_total_relcompp_transfer[transfer_rule]:
    7.65    assumes [transfer_rule]: "right_total B"
    7.66 -  shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) 
    7.67 +  shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=)
    7.68      (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO"
    7.69  unfolding OO_def[abs_def] by transfer_prover
    7.70  
    7.71 -lemma relcompp_transfer[transfer_rule]: 
    7.72 +lemma relcompp_transfer[transfer_rule]:
    7.73    assumes [transfer_rule]: "bi_total B"
    7.74    shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO"
    7.75  unfolding OO_def[abs_def] by transfer_prover
    7.76 @@ -507,13 +507,13 @@
    7.77    shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp"
    7.78  unfolding Domainp_iff[abs_def] by transfer_prover
    7.79  
    7.80 -lemma reflp_transfer[transfer_rule]: 
    7.81 +lemma reflp_transfer[transfer_rule]:
    7.82    "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp"
    7.83    "right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp"
    7.84    "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
    7.85    "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
    7.86    "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
    7.87 -using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def 
    7.88 +using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
    7.89  by fast+
    7.90  
    7.91  lemma right_unique_transfer [transfer_rule]: