1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/ctr_sugar_code.ML Mon Dec 02 20:31:54 2013 +0100
1.3 @@ -0,0 +1,129 @@
1.4 +(* Title: HOL/Tools/ctr_sugar_code.ML
1.5 + Author: Jasmin Blanchette, TU Muenchen
1.6 + Author: Dmitriy Traytel, TU Muenchen
1.7 + Author: Stefan Berghofer, TU Muenchen
1.8 + Author: Florian Haftmann, TU Muenchen
1.9 + Copyright 2001-2013
1.10 +
1.11 +Code generation for freely generated types.
1.12 +*)
1.13 +
1.14 +signature CTR_SUGAR_CODE =
1.15 +sig
1.16 + val add_ctr_code: string -> typ list -> (string * typ) list -> thm list -> thm list -> thm list ->
1.17 + theory -> theory
1.18 +end;
1.19 +
1.20 +structure Ctr_Sugar_Code : CTR_SUGAR_CODE =
1.21 +struct
1.22 +
1.23 +open Ctr_Sugar_Util
1.24 +
1.25 +val eqN = "eq"
1.26 +val reflN = "refl"
1.27 +val simpsN = "simps"
1.28 +
1.29 +fun mk_case_certificate thy raw_thms =
1.30 + let
1.31 + val thms as thm1 :: _ = raw_thms
1.32 + |> Conjunction.intr_balanced
1.33 + |> Thm.unvarify_global
1.34 + |> Conjunction.elim_balanced (length raw_thms)
1.35 + |> map Simpdata.mk_meta_eq
1.36 + |> map Drule.zero_var_indexes;
1.37 + val params = Term.add_free_names (Thm.prop_of thm1) [];
1.38 + val rhs = thm1
1.39 + |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
1.40 + ||> fst o split_last |> list_comb;
1.41 + val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
1.42 + val assum = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
1.43 + in
1.44 + thms
1.45 + |> Conjunction.intr_balanced
1.46 + |> rewrite_rule [Thm.symmetric (Thm.assume assum)]
1.47 + |> Thm.implies_intr assum
1.48 + |> Thm.generalize ([], params) 0
1.49 + |> Axclass.unoverload thy
1.50 + |> Thm.varifyT_global
1.51 + end;
1.52 +
1.53 +fun mk_free_ctr_equations fcT ctrs inject_thms distinct_thms thy =
1.54 + let
1.55 + fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u;
1.56 + fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
1.57 + fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
1.58 +
1.59 + val monomorphic_prop_of = prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
1.60 +
1.61 + fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
1.62 + fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];
1.63 +
1.64 + val triv_inject_goals =
1.65 + map_filter (fn c as (_, T) =>
1.66 + if T = fcT then SOME (HOLogic.mk_Trueprop (true_eq (Const c, Const c))) else NONE)
1.67 + ctrs;
1.68 + val inject_goals = map (massage_inject o monomorphic_prop_of) inject_thms;
1.69 + val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;
1.70 + val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));
1.71 +
1.72 + val simp_ctxt =
1.73 + Simplifier.global_context thy HOL_basic_ss
1.74 + addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
1.75 +
1.76 + fun prove goal =
1.77 + Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt)))
1.78 + |> Simpdata.mk_eq;
1.79 + in
1.80 + (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
1.81 + end;
1.82 +
1.83 +fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =
1.84 + let
1.85 + fun add_def lthy =
1.86 + let
1.87 + fun mk_side const_name =
1.88 + Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);
1.89 + val spec =
1.90 + mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
1.91 + |> Syntax.check_term lthy;
1.92 + val ((_, (_, raw_def)), lthy') =
1.93 + Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
1.94 + val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
1.95 + val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def;
1.96 + in
1.97 + (def, lthy')
1.98 + end;
1.99 +
1.100 + fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
1.101 +
1.102 + val qualify =
1.103 + Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
1.104 + in
1.105 + Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
1.106 + #> add_def
1.107 + #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single
1.108 + #-> fold Code.del_eqn
1.109 + #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
1.110 + #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
1.111 + [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
1.112 + ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])])
1.113 + #> snd
1.114 + end;
1.115 +
1.116 +fun add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy =
1.117 + let
1.118 + val fcT = Type (fcT_name, As);
1.119 + val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
1.120 + in
1.121 + if can (Code.constrset_of_consts thy) unover_ctrs then
1.122 + thy
1.123 + |> Code.add_datatype ctrs
1.124 + |> fold_rev Code.add_default_eqn case_thms
1.125 + |> Code.add_case (mk_case_certificate thy case_thms)
1.126 + |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
1.127 + ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
1.128 + else
1.129 + thy
1.130 + end;
1.131 +
1.132 +end;