explicit type Name.binding for higher-specification elements;
authorwenzelm
Tue Sep 02 14:10:30 2008 +0200 (2008-09-02)
changeset 280804723eb2456ce
parent 28079 955c42c8a5e4
child 28081 d664b2c1dfe6
explicit type Name.binding for higher-specification elements;
simplified ProofContext.inferred_param;
src/Pure/Isar/obtain.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Sep 02 14:10:29 2008 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Sep 02 14:10:30 2008 +0200
     1.3 @@ -40,16 +40,16 @@
     1.4  signature OBTAIN =
     1.5  sig
     1.6    val thatN: string
     1.7 -  val obtain: string -> (string * string option * mixfix) list ->
     1.8 -    ((string * Attrib.src list) * (string * string list) list) list ->
     1.9 +  val obtain: string -> (Name.binding * string option * mixfix) list ->
    1.10 +    ((Name.binding * Attrib.src list) * (string * string list) list) list ->
    1.11      bool -> Proof.state -> Proof.state
    1.12 -  val obtain_i: string -> (string * typ option * mixfix) list ->
    1.13 -    ((string * attribute list) * (term * term list) list) list ->
    1.14 +  val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
    1.15 +    ((Name.binding * attribute list) * (term * term list) list) list ->
    1.16      bool -> Proof.state -> Proof.state
    1.17    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
    1.18      (cterm list * thm list) * Proof.context
    1.19 -  val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.20 -  val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.21 +  val guess: (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.22 +  val guess_i: (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
    1.23  end;
    1.24  
    1.25  structure Obtain: OBTAIN =
    1.26 @@ -122,7 +122,7 @@
    1.27      (*obtain vars*)
    1.28      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
    1.29      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    1.30 -    val xs = map #1 vars;
    1.31 +    val xs = map (Name.name_of o #1) vars;
    1.32  
    1.33      (*obtain asms*)
    1.34      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    1.35 @@ -151,18 +151,19 @@
    1.36      fun after_qed _ =
    1.37        Proof.local_qed (NONE, false)
    1.38        #> Seq.map (`Proof.the_fact #-> (fn rule =>
    1.39 -        Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
    1.40 +        Proof.fix_i vars
    1.41          #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
    1.42    in
    1.43      state
    1.44      |> Proof.enter_forward
    1.45 -    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
    1.46 +    |> Proof.have_i NONE (K Seq.single) [((Name.no_binding, []), [(obtain_prop, [])])] int
    1.47      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    1.48 -    |> Proof.fix_i [(thesisN, NONE, NoSyn)]
    1.49 -    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
    1.50 +    |> Proof.fix_i [(Name.binding thesisN, NONE, NoSyn)]
    1.51 +    |> Proof.assume_i
    1.52 +      [((Name.binding that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
    1.53      |> `Proof.the_facts
    1.54      ||> Proof.chain_facts chain_facts
    1.55 -    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false
    1.56 +    ||> Proof.show_i NONE after_qed [((Name.no_binding, []), [(thesis, [])])] false
    1.57      |-> Proof.refine_insert
    1.58    end;
    1.59  
    1.60 @@ -258,8 +259,10 @@
    1.61      val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
    1.62    in ((vars', rule''), ctxt') end;
    1.63  
    1.64 -fun inferred_type (x, _, mx) ctxt =
    1.65 -  let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
    1.66 +fun inferred_type (binding, _, mx) ctxt =
    1.67 +  let
    1.68 +    val x = Name.name_of binding;
    1.69 +    val (T, ctxt') = ProofContext.inferred_param x ctxt
    1.70    in ((x, T, mx), ctxt') end;
    1.71  
    1.72  fun polymorphic ctxt vars =
    1.73 @@ -291,9 +294,9 @@
    1.74        in
    1.75          state'
    1.76          |> Proof.map_context (K ctxt')
    1.77 -        |> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms)
    1.78 -        |> `Proof.context_of |-> (fn fix_ctxt =>
    1.79 -            Proof.assm_i (obtain_export fix_ctxt rule (map cert ts)) [(("", []), asms)])
    1.80 +        |> Proof.fix_i (map (fn ((x, T), mx) => (Name.binding x, SOME T, mx)) parms)
    1.81 +        |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
    1.82 +          (obtain_export fix_ctxt rule (map cert ts)) [((Name.no_binding, []), asms)])
    1.83          |> Proof.add_binds_i AutoBind.no_facts
    1.84        end;
    1.85  
    1.86 @@ -308,10 +311,10 @@
    1.87      state
    1.88      |> Proof.enter_forward
    1.89      |> Proof.begin_block
    1.90 -    |> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)]
    1.91 +    |> Proof.fix_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)]
    1.92      |> Proof.chain_facts chain_facts
    1.93      |> Proof.local_goal print_result (K I) (apsnd (rpair I))
    1.94 -      "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]
    1.95 +      "guess" before_qed after_qed [((Name.no_binding, []), [Logic.mk_term goal, goal])]
    1.96      |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
    1.97    end;
    1.98  
     2.1 --- a/src/Pure/Isar/specification.ML	Tue Sep 02 14:10:29 2008 +0200
     2.2 +++ b/src/Pure/Isar/specification.ML	Tue Sep 02 14:10:30 2008 +0200
     2.3 @@ -9,52 +9,53 @@
     2.4  signature SPECIFICATION =
     2.5  sig
     2.6    val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
     2.7 -  val check_specification: (string * typ option * mixfix) list ->
     2.8 -    ((string * Attrib.src list) * term list) list list -> Proof.context ->
     2.9 -    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.10 +  val check_specification: (Name.binding * typ option * mixfix) list ->
    2.11 +    ((Name.binding * Attrib.src list) * term list) list list -> Proof.context ->
    2.12 +    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
    2.13      Proof.context
    2.14 -  val read_specification: (string * string option * mixfix) list ->
    2.15 -    ((string * Attrib.src list) * string list) list list -> Proof.context ->
    2.16 -    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.17 +  val read_specification: (Name.binding * string option * mixfix) list ->
    2.18 +    ((Name.binding * Attrib.src list) * string list) list list -> Proof.context ->
    2.19 +    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
    2.20      Proof.context
    2.21 -  val check_free_specification: (string * typ option * mixfix) list ->
    2.22 -    ((string * Attrib.src list) * term list) list -> Proof.context ->
    2.23 -    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.24 +  val check_free_specification: (Name.binding * typ option * mixfix) list ->
    2.25 +    ((Name.binding * Attrib.src list) * term list) list -> Proof.context ->
    2.26 +    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
    2.27      Proof.context
    2.28 -  val read_free_specification: (string * string option * mixfix) list ->
    2.29 -    ((string * Attrib.src list) * string list) list -> Proof.context ->
    2.30 -    (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
    2.31 +  val read_free_specification: (Name.binding * string option * mixfix) list ->
    2.32 +    ((Name.binding * Attrib.src list) * string list) list -> Proof.context ->
    2.33 +    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
    2.34      Proof.context
    2.35 -  val axiomatization: (string * typ option * mixfix) list ->
    2.36 -    ((bstring * Attrib.src list) * term list) list -> local_theory ->
    2.37 -    (term list * (bstring * thm list) list) * local_theory
    2.38 -  val axiomatization_cmd: (string * string option * mixfix) list ->
    2.39 -    ((bstring * Attrib.src list) * string list) list -> local_theory ->
    2.40 -    (term list * (bstring * thm list) list) * local_theory
    2.41 +  val axiomatization: (Name.binding * typ option * mixfix) list ->
    2.42 +    ((Name.binding * Attrib.src list) * term list) list -> local_theory ->
    2.43 +    (term list * (string * thm list) list) * local_theory
    2.44 +  val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
    2.45 +    ((Name.binding * Attrib.src list) * string list) list -> local_theory ->
    2.46 +    (term list * (string * thm list) list) * local_theory
    2.47    val definition:
    2.48 -    (string * typ option * mixfix) option * ((string * Attrib.src list) * term) ->
    2.49 -    local_theory -> (term * (bstring * thm)) * local_theory
    2.50 +    (Name.binding * typ option * mixfix) option * ((Name.binding * Attrib.src list) * term) ->
    2.51 +    local_theory -> (term * (string * thm)) * local_theory
    2.52    val definition_cmd:
    2.53 -    (string * string option * mixfix) option * ((string * Attrib.src list) * string) ->
    2.54 -    local_theory -> (term * (bstring * thm)) * local_theory
    2.55 -  val abbreviation: Syntax.mode -> (string * typ option * mixfix) option * term ->
    2.56 +    (Name.binding * string option * mixfix) option * ((Name.binding * Attrib.src list) * string) ->
    2.57 +    local_theory -> (term * (string * thm)) * local_theory
    2.58 +  val abbreviation: Syntax.mode -> (Name.binding * typ option * mixfix) option * term ->
    2.59      local_theory -> local_theory
    2.60 -  val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string ->
    2.61 +  val abbreviation_cmd: Syntax.mode -> (Name.binding * string option * mixfix) option * string ->
    2.62      local_theory -> local_theory
    2.63    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    2.64    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    2.65 -  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    2.66 -    local_theory -> (bstring * thm list) list * local_theory
    2.67 +  val theorems: string ->
    2.68 +    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
    2.69 +    local_theory -> (string * thm list) list * local_theory
    2.70    val theorems_cmd: string ->
    2.71 -    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
    2.72 -    local_theory -> (bstring * thm list) list * local_theory
    2.73 +    ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
    2.74 +    local_theory -> (string * thm list) list * local_theory
    2.75    val theorem: string -> Method.text option ->
    2.76 -    (thm list list -> local_theory -> local_theory) ->
    2.77 -    string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
    2.78 +    (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
    2.79 +    Element.context_i Locale.element list -> Element.statement_i ->
    2.80      bool -> local_theory -> Proof.state
    2.81    val theorem_cmd: string -> Method.text option ->
    2.82 -    (thm list list -> local_theory -> local_theory) ->
    2.83 -    string * Attrib.src list -> Element.context Locale.element list -> Element.statement ->
    2.84 +    (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
    2.85 +    Element.context Locale.element list -> Element.statement ->
    2.86      bool -> local_theory -> Proof.state
    2.87    val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
    2.88  end;
    2.89 @@ -122,8 +123,8 @@
    2.90        |> flat |> burrow (Syntax.check_props params_ctxt);
    2.91      val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
    2.92  
    2.93 -    val vs = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
    2.94 -    val params = vs ~~ map #3 vars;
    2.95 +    val Ts = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
    2.96 +    val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
    2.97      val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
    2.98    in ((params, name_atts ~~ specs), specs_ctxt) end;
    2.99  
   2.100 @@ -149,7 +150,8 @@
   2.101      val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
   2.102      val _ =
   2.103        if not do_print then ()
   2.104 -      else print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) (map fst vars);
   2.105 +      else print_consts lthy' (member (op =) (fold Term.add_frees consts' []))
   2.106 +        (map (fn ((b, T), _) => (Name.name_of b, T)) vars);
   2.107    in ((consts, axioms), lthy') end;
   2.108  
   2.109  val axiomatization = gen_axioms false check_specification;
   2.110 @@ -163,21 +165,27 @@
   2.111      val (vars, [((raw_name, atts), [prop])]) =
   2.112        fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
   2.113      val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
   2.114 -    val name = Thm.def_name_optional x raw_name;
   2.115 -    val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
   2.116 -      if x = x' then mx
   2.117 -      else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
   2.118 -    val ((lhs, (_, th)), lthy2) = lthy
   2.119 -      |> LocalTheory.define Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
   2.120 -    val ((b, [th']), lthy3) = lthy2
   2.121 -      |> LocalTheory.note Thm.definitionK
   2.122 -          ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
   2.123 +    val name = Name.map_name (Thm.def_name_optional x) raw_name;
   2.124 +    val var =
   2.125 +      (case vars of
   2.126 +        [] => (Name.binding x, NoSyn)
   2.127 +      | [((b, _), mx)] =>
   2.128 +          let
   2.129 +            val y = Name.name_of b;
   2.130 +            val _ = x = y orelse
   2.131 +              error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
   2.132 +                Position.str_of (Name.pos_of b));
   2.133 +          in (b, mx) end);
   2.134 +    val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
   2.135 +        (var, ((Name.map_name (suffix "_raw") name, []), rhs));
   2.136 +    val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
   2.137 +        ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
   2.138  
   2.139      val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
   2.140      val _ =
   2.141        if not do_print then ()
   2.142        else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   2.143 -  in ((lhs, (b, th')), lthy3) end;
   2.144 +  in ((lhs, (def_name, th')), lthy3) end;
   2.145  
   2.146  val definition = gen_def false check_free_specification;
   2.147  val definition_cmd = gen_def true read_free_specification;
   2.148 @@ -191,12 +199,19 @@
   2.149        prep (the_list raw_var) [(("", []), [raw_prop])]
   2.150          (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
   2.151      val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
   2.152 -    val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
   2.153 -      if x = y then mx
   2.154 -      else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
   2.155 +    val var =
   2.156 +      (case vars of
   2.157 +        [] => (Name.binding x, NoSyn)
   2.158 +      | [((b, _), mx)] =>
   2.159 +          let
   2.160 +            val y = Name.name_of b;
   2.161 +            val _ = x = y orelse
   2.162 +              error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
   2.163 +                Position.str_of (Name.pos_of b));
   2.164 +          in (b, mx) end);
   2.165      val lthy' = lthy
   2.166        |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
   2.167 -      |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
   2.168 +      |> LocalTheory.abbrev mode (var, rhs) |> snd
   2.169        |> ProofContext.restore_syntax_mode lthy;
   2.170  
   2.171      val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
   2.172 @@ -249,11 +264,12 @@
   2.173        in ((prems, stmt, []), goal_ctxt) end
   2.174    | Element.Obtains obtains =>
   2.175        let
   2.176 -        val case_names = obtains |> map_index
   2.177 -          (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
   2.178 +        val case_names = obtains |> map_index (fn (i, (binding, _)) =>
   2.179 +          let val name = Name.name_of binding
   2.180 +          in if name = "" then string_of_int (i + 1) else name end);
   2.181          val constraints = obtains |> map (fn (_, (vars, _)) =>
   2.182            Locale.Elem (Element.Constrains
   2.183 -            (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))));
   2.184 +            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE))));
   2.185  
   2.186          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
   2.187          val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
   2.188 @@ -262,14 +278,15 @@
   2.189  
   2.190          fun assume_case ((name, (vars, _)), asms) ctxt' =
   2.191            let
   2.192 -            val xs = map fst vars;
   2.193 +            val bs = map fst vars;
   2.194 +            val xs = map Name.name_of bs;
   2.195              val props = map fst asms;
   2.196 -            val (parms, _) = ctxt'
   2.197 +            val (Ts, _) = ctxt'
   2.198                |> fold Variable.declare_term props
   2.199                |> fold_map ProofContext.inferred_param xs;
   2.200 -            val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
   2.201 +            val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
   2.202            in
   2.203 -            ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
   2.204 +            ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
   2.205              ctxt' |> Variable.auto_fixes asm
   2.206              |> ProofContext.add_assms_i Assumption.assume_export
   2.207                [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
   2.208 @@ -279,13 +296,13 @@
   2.209          val atts = map (Attrib.internal o K)
   2.210            [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
   2.211          val prems = subtract_prems loc_ctxt elems_ctxt;
   2.212 -        val stmt = [(("", atts), [(thesis, [])])];
   2.213 +        val stmt = [((Name.no_binding, atts), [(thesis, [])])];
   2.214  
   2.215          val (facts, goal_ctxt) = elems_ctxt
   2.216 -          |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
   2.217 +          |> (snd o ProofContext.add_fixes_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)])
   2.218            |> fold_map assume_case (obtains ~~ propp)
   2.219            |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
   2.220 -                [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
   2.221 +                [((Name.binding Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
   2.222        in ((prems, stmt, facts), goal_ctxt) end);
   2.223  
   2.224  structure TheoremHook = GenericDataFun
   2.225 @@ -323,14 +340,20 @@
   2.226          lthy
   2.227          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
   2.228          |> (fn (res, lthy') =>
   2.229 -          (ProofDisplay.theory_results lthy' ((kind, name), res);
   2.230 -            if name = "" andalso null atts then lthy'
   2.231 -            else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
   2.232 +          if Name.name_of name = "" andalso null atts then
   2.233 +            (ProofDisplay.theory_results lthy' ((kind, ""), res); lthy')
   2.234 +          else
   2.235 +            let
   2.236 +              val ([(res_name, _)], lthy'') = lthy'
   2.237 +                |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
   2.238 +              val _ = ProofDisplay.theory_results lthy' ((kind, res_name), res);
   2.239 +            in lthy'' end)
   2.240          |> after_qed results'
   2.241        end;
   2.242    in
   2.243      goal_ctxt
   2.244 -    |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])]
   2.245 +    |> ProofContext.note_thmss_i Thm.assumptionK
   2.246 +      [((Name.binding AutoBind.assmsN, []), [(prems, [])])]
   2.247      |> snd
   2.248      |> Proof.theorem_i before_qed after_qed' (map snd stmt)
   2.249      |> Proof.refine_insert facts