src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
changeset 54701 4ed7454aebde
parent 54691 506312c293f5
child 54742 7a86358a3c0b
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon Dec 09 09:44:57 2013 +0100
@@ -0,0 +1,131 @@
+(*  Title:      HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    Author:     Florian Haftmann, TU Muenchen
+    Copyright   2001-2013
+
+Code generation for freely generated types.
+*)
+
+signature CTR_SUGAR_CODE =
+sig
+  val add_ctr_code: string -> typ list -> (string * typ) list -> thm list -> thm list -> thm list ->
+    theory -> theory
+end;
+
+structure Ctr_Sugar_Code : CTR_SUGAR_CODE =
+struct
+
+open Ctr_Sugar_Util
+
+val eqN = "eq"
+val reflN = "refl"
+val simpsN = "simps"
+
+fun mk_case_certificate thy raw_thms =
+  let
+    val thms as thm1 :: _ = raw_thms
+      |> Conjunction.intr_balanced
+      |> Thm.unvarify_global
+      |> Conjunction.elim_balanced (length raw_thms)
+      |> map Simpdata.mk_meta_eq
+      |> map Drule.zero_var_indexes;
+    val params = Term.add_free_names (Thm.prop_of thm1) [];
+    val rhs = thm1
+      |> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
+      ||> fst o split_last |> list_comb;
+    val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
+    val assum = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs));
+  in
+    thms
+    |> Conjunction.intr_balanced
+    |> rewrite_rule [Thm.symmetric (Thm.assume assum)]
+    |> Thm.implies_intr assum
+    |> Thm.generalize ([], params) 0
+    |> Axclass.unoverload thy
+    |> Thm.varifyT_global
+  end;
+
+fun mk_free_ctr_equations fcT ctrs inject_thms distinct_thms thy =
+  let
+    fun mk_fcT_eq (t, u) = Const (@{const_name HOL.equal}, fcT --> fcT --> HOLogic.boolT) $ t $ u;
+    fun true_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term True});
+    fun false_eq tu = HOLogic.mk_eq (mk_fcT_eq tu, @{term False});
+
+    val monomorphic_prop_of = prop_of o Thm.unvarify_global o Drule.zero_var_indexes;
+
+    fun massage_inject (tp $ (eqv $ (_ $ t $ u) $ rhs)) = tp $ (eqv $ mk_fcT_eq (t, u) $ rhs);
+    fun massage_distinct (tp $ (_ $ (_ $ t $ u))) = [tp $ false_eq (t, u), tp $ false_eq (u, t)];
+
+    val triv_inject_goals =
+      map_filter (fn c as (_, T) =>
+          if T = fcT then SOME (HOLogic.mk_Trueprop (true_eq (Const c, Const c))) else NONE)
+        ctrs;
+    val inject_goals = map (massage_inject o monomorphic_prop_of) inject_thms;
+    val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;
+    val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));
+
+    val simp_ctxt =
+      Simplifier.global_context thy HOL_basic_ss
+        addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
+
+    fun prove goal =
+      Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt)))
+      |> Simpdata.mk_eq;
+  in
+    (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
+  end;
+
+fun add_equality fcT fcT_name As ctrs inject_thms distinct_thms =
+  let
+    fun add_def lthy =
+      let
+        fun mk_side const_name =
+          Const (const_name, fcT --> fcT --> HOLogic.boolT) $ Free ("x", fcT) $ Free ("y", fcT);
+        val spec =
+          mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
+          |> Syntax.check_term lthy;
+        val ((_, (_, raw_def)), lthy') =
+          Specification.definition (NONE, (Attrib.empty_binding, spec)) lthy;
+        val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); (* FIXME? *)
+        val def = singleton (Proof_Context.export lthy' ctxt_thy) raw_def;
+      in
+        (def, lthy')
+      end;
+
+    fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms);
+
+    val qualify =
+      Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;
+  in
+    Class.instantiation ([fcT_name], map dest_TFree As, [HOLogic.class_equal])
+    #> add_def
+    #-> Class.prove_instantiation_exit_result (map o Morphism.thm) (K tac) o single
+    #-> fold Code.del_eqn
+    #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms)
+    #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
+      [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
+        ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])])
+    #> snd
+  end;
+
+fun add_ctr_code fcT_name raw_As raw_ctrs inject_thms distinct_thms case_thms thy =
+  let
+    val As = map (perhaps (try Logic.unvarifyT_global)) raw_As;
+    val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs;
+    val fcT = Type (fcT_name, As);
+    val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
+  in
+    if can (Code.constrset_of_consts thy) unover_ctrs then
+      thy
+      |> Code.add_datatype ctrs
+      |> fold_rev Code.add_default_eqn case_thms
+      |> Code.add_case (mk_case_certificate thy case_thms)
+      |> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
+        ? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
+    else
+      thy
+  end;
+
+end;