src/HOL/BNF/Tools/bnf_wrap.ML
changeset 51380 cac8c9a636b6
parent 50214 67fb9a168d10
child 51551 88d1d19fb74f
equal deleted inserted replaced
51379:6dd83e007f56 51380:cac8c9a636b6
   165              SOME (std_disc_binding ctr)
   165              SOME (std_disc_binding ctr)
   166            else
   166            else
   167              SOME disc)) ks ms ctrs0;
   167              SOME disc)) ks ms ctrs0;
   168 
   168 
   169     val no_discs = map is_none disc_bindings;
   169     val no_discs = map is_none disc_bindings;
   170     val no_discs_at_all = forall I no_discs;
       
   171 
   170 
   172     fun std_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
   171     fun std_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
   173 
   172 
   174     val sel_bindingss =
   173     val sel_bindingss =
   175       pad_list [] n raw_sel_bindingss
   174       pad_list [] n raw_sel_bindingss
   238           fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
   237           fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
   239 
   238 
   240           fun alternate_disc k =
   239           fun alternate_disc k =
   241             Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
   240             Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
   242 
   241 
   243           fun mk_default T t =
       
   244             let
       
   245               val Ts0 = map TFree (Term.add_tfreesT (fastype_of t) []);
       
   246               val Ts = map TFree (Term.add_tfreesT T []);
       
   247             in Term.subst_atomic_types (Ts0 ~~ Ts) t end;
       
   248 
       
   249           fun mk_sel_case_args b proto_sels T =
   242           fun mk_sel_case_args b proto_sels T =
   250             map2 (fn Ts => fn k =>
   243             map2 (fn Ts => fn k =>
   251               (case AList.lookup (op =) proto_sels k of
   244               (case AList.lookup (op =) proto_sels k of
   252                 NONE =>
   245                 NONE =>
   253                 (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
   246                 (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
   254                   NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
   247                   NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
   255                 | SOME t => mk_default (Ts ---> T) t)
   248                 | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term no_defs_lthy)
   256               | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
   249               | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
   257 
   250 
   258           fun sel_spec b proto_sels =
   251           fun sel_spec b proto_sels =
   259             let
   252             let
   260               val _ =
   253               val _ =
   656   map2 (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])) goalss tacss
   649   map2 (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])) goalss tacss
   657   |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
   650   |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
   658 
   651 
   659 val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
   652 val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
   660   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
   653   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
   661   prepare_wrap_datatype Syntax.read_term;
   654   prepare_wrap_datatype Syntax.parse_term;
   662 
   655 
   663 fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
   656 fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
   664 
   657 
   665 val parse_bindings = parse_bracket_list Parse.binding;
   658 val parse_bindings = parse_bracket_list Parse.binding;
   666 val parse_bindingss = parse_bracket_list parse_bindings;
   659 val parse_bindingss = parse_bracket_list parse_bindings;