diff --git a/thys/Circus/Circus_Syntax.thy b/thys/Circus/Circus_Syntax.thy --- a/thys/Circus/Circus_Syntax.thy +++ b/thys/Circus/Circus_Syntax.thy @@ -1,372 +1,375 @@ section \Circus syntax\ theory Circus_Syntax imports Denotational_Semantics keywords "alphabet" "state" "channel" "nameset" "chanset" "schema" "action" and "circus_process" :: thy_defn begin abbreviation list_select::"['r \ 'a list] \ ('r \ 'a)" where "list_select Sel \ hd o Sel" abbreviation list_update::"[('a list \ 'a list) \ 'r \ 'r] \ ('a \ 'a) \ 'r \ 'r" where "list_update Upd \ \ e. Upd (\ l. (e (hd l))#(tl l))" abbreviation list_update_const::"[('a list \ 'a list) \ 'r \ 'r] \ 'a \ 'r relation" where "list_update_const Upd \ \ e. \ (A, A'). A' = Upd (\ l. e#(tl l)) A" abbreviation update_const::"[('a \ 'a) \ 'r \ 'r] \ 'a \ 'r relation" where "update_const Upd \ \ e. \ (A, A'). A' = Upd (\ _. e) A" syntax "_synt_assign" :: "id \ 'a \ 'b relation" ("_ := _") ML \ structure VARs_Data = Proof_Data ( type T = {State_vars: string list, Alpha_vars: string list} fun init _ : T = {State_vars = [], Alpha_vars = []} ) \ nonterminal circus_action and circus_schema syntax "_circus_action" :: "'a => circus_action" ("_") (* FIXME unused!? *) "_circus_schema" :: "'a => circus_schema" ("_") parse_translation \ let fun antiquote_tr ctxt = let val {State_vars=sv, Alpha_vars=av} = VARs_Data.get ctxt fun get_selector x = let val c = Consts.intern (Proof_Context.consts_of ctxt) x in if member (=) av x then SOME (Const ("Circus_Syntax.list_select", dummyT) $ (Syntax.const c)) else if member (=) sv x then SOME (Syntax.const c) else NONE end; fun get_update x = let val c = Consts.intern (Proof_Context.consts_of ctxt) x in if member (=) av x then SOME (Const ("Circus_Syntax.list_update_const", dummyT) $ (Syntax.const (c^Record.updateN))) else if member (=) sv x then SOME (Const ("Circus_Syntax.update_const", dummyT) $ (Syntax.const (c^Record.updateN))) else NONE end; fun print text = (fn x => let val _ = writeln text; in x end); val rel_op_type = @{typ "('a \ 'b \ bool) \ ('b \ 'c \ bool) \ 'a \ 'c \ bool"}; fun tr i (t as Free (x, _)) = (case get_selector x of SOME c => c $ Bound (i + 1) | NONE => (case try (unsuffix "'") x of SOME y => (case get_selector y of SOME c => c $ Bound i | NONE => t) | NONE => t)) | tr i (t as (Const ("_synt_assign", _) $ Free (x, _) $ r)) = (case get_update x of SOME c => c $ (tr i r) $ (Const ("Product_Type.Pair", dummyT) $ Bound (i + 1) $ Bound i) | NONE => t) (* | tr i (t as (Const (c, rel_op_type) $ l $ r)) = print c ((Syntax.const @{const_name case_prod} $ Abs ("B", dummyT, Abs ("B'", dummyT, Const (c, rel_op_type)))) $ tr i l $ tr i r) $ (Const ("Product_Type.Pair", dummyT) $ Bound (i + 1) $ Bound i)*) | tr i (t $ u) = tr i t $ tr i u | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t) | tr _ a = a; in tr 0 end; fun quote_tr ctxt [t] = Syntax.const @{const_name case_prod} $ Abs ("A", dummyT, Abs ("A'", dummyT, antiquote_tr ctxt (Term.incr_boundvars 2 t))) | quote_tr _ ts = raise TERM ("quote_tr", ts); in [(@{syntax_const "_circus_schema"}, quote_tr)] end \ ML \ fun get_fields (SOME ({fields, parent, ...}: Record.info)) thy = (case parent of SOME ( _,y) => fields @ get_fields (Record.get_info thy y) thy | NONE => fields) | get_fields NONE _ = [] val dummy = Term.dummy_pattern dummyT; fun mk_eq (l, r) = HOLogic.Trueprop $ ((HOLogic.eq_const dummyT) $ l $ r) fun add_datatype (params, binding) constr_specs thy = let val ([dt_name], thy') = thy |> BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting] [((binding, params, NoSyn), constr_specs)]; val constr_names = map fst (the_single (map (#3 o snd) (#descr (BNF_LFP_Compat.the_info thy' [BNF_LFP_Compat.Keep_Nesting] dt_name)))); fun constr (c, Ts) = (Const (c, dummyT), length Ts); val constrs = map #1 constr_specs ~~ map constr (constr_names ~~ map #2 constr_specs); in ((dt_name, constrs), thy') end; fun define_channels (params, binding) typesyn channels thy = case typesyn of NONE => let val dt_binding = Binding.suffix_name "_channels" binding; val constr_specs = map (fn (b, opt_T) => (b, the_list opt_T, NoSyn)) channels; val ((dt_name, constrs), thy1) = add_datatype (params, dt_binding) constr_specs thy; val T = Type (dt_name, []); val fun_name = "ev_eq" ^ "_" ^ Long_Name.base_name dt_name; val ev_equ = Free (fun_name, T --> T --> HOLogic.boolT); val eqs = map_product (fn (_, (c, n)) => (fn (_, (c1,n1)) => let val t = Term.list_comb (c, replicate n dummy); val t1 = Term.list_comb (c1, replicate n1 dummy); in (if c = c1 then mk_eq ((ev_equ $ t $ t1), @{term True}) else mk_eq ((ev_equ $ t $ t1), @{term False})) end)) constrs constrs; fun case_tac x ctxt = resolve_tac ctxt [Thm.instantiate' [] [SOME x] (#exhaust (BNF_LFP_Compat.the_info (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] dt_name))]; fun proof ctxt = (Class.intro_classes_tac ctxt [] THEN Subgoal.FOCUS (fn {context = ctxt', params = [(_, x)], ...} => (case_tac x ctxt') 1 THEN auto_tac ctxt') ctxt 1 THEN Subgoal.FOCUS (fn {context = ctxt', params = [(_, x), (_, y)], ...} => ((case_tac x ctxt') THEN_ALL_NEW (case_tac y ctxt')) 1 THEN auto_tac ctxt') ctxt 1); val thy2 = thy1 |> Class.instantiation ([dt_name], params, @{sort ev_eq}) - |> Local_Theory.subtarget (Function_Fun.add_fun [(Binding.name fun_name, NONE, NoSyn)] - (map (fn t => ((Binding.empty_atts, t), [], [])) eqs) Function_Fun.fun_config) + |> Local_Theory.begin_nested + |> snd + |> Function_Fun.add_fun [(Binding.name fun_name, NONE, NoSyn)] + (map (fn t => ((Binding.empty_atts, t), [], [])) eqs) Function_Fun.fun_config + |> Local_Theory.end_nested |> Class.prove_instantiation_exit (fn ctxt => proof ctxt); in ((dt_name, constrs), thy2) end | (SOME typn) => let val dt_binding = Binding.suffix_name "_channels" binding; val (dt_name, thy1) = thy |> Named_Target.theory_init |> (fn ctxt => Typedecl.abbrev (dt_binding, map fst params, NoSyn) (Proof_Context.read_typ ctxt typn) ctxt); val thy2 = thy1 |> Local_Theory.exit_global; in ((dt_name, []), thy2) end; fun define_chanset binding channel_constrs (name, chans) thy = let val constrs = filter (fn (b, _) => exists (fn a => a = Binding.name_of b) chans) channel_constrs; val bad_chans = filter_out (fn a => exists (fn (b, _) => a = Binding.name_of b) channel_constrs) chans; val _ = null bad_chans orelse error ("Bad elements " ^ commas_quote bad_chans ^ " in chanset: " ^ quote (Binding.print name)); val base_name = Binding.name_of name; val cs = map (fn (_, (c, n)) => Term.list_comb (c, replicate n (Const (@{const_name undefined}, dummyT)))) constrs; val chanset_eq = mk_eq ((Free (base_name, dummyT)), (HOLogic.mk_set dummyT cs)); in thy |> Named_Target.theory_init |> Specification.definition (SOME (Binding.qualify_name true binding base_name, NONE, NoSyn)) [] [] (Binding.empty_atts, chanset_eq) |> snd |> Local_Theory.exit_global end; fun define_nameset binding (rec_binding, alphabet) (ns_binding, names) thy = let val all_selectors = get_fields (Record.get_info thy (Sign.full_name thy rec_binding)) thy val bad_names = filter_out (fn a => exists (fn (b, _) => String.isSuffix a b) all_selectors) names; val _ = null bad_names orelse error ("Bad elements " ^ commas_quote bad_names ^ " in nameset: " ^ quote (Binding.print ns_binding)); val selectors = filter (fn (b, _) => exists (fn a => String.isSuffix a b) names) all_selectors; val updates = map (fn x => (fst x, ((suffix Record.updateN) o fst) x)) selectors; val selectors' = map (fn x => (fst x, Const(fst x, dummyT))) selectors; val updates' = map (fn (x, y) => (x, Const(y, dummyT))) updates; val l = map (fn (b, _) => Binding.name_of b) alphabet; val formulas = map2 (fn (nx, x) => fn (ny, y) => if (exists (fn b => String.isSuffix b nx) l) then Abs ("A", dummyT, (Const("Circus_Syntax.list_update", dummyT) $ x) $ (Abs ("_", dummyT, (Const("Circus_Syntax.list_select", dummyT) $ y) $ (Bound 1)))) else Abs ("A", dummyT, x $ (Abs ("_", dummyT, y $ (Bound 1))))) updates' selectors'; val base_name = Binding.name_of ns_binding; fun comp [a] = a $ (Bound 1) $ (Bound 0) | comp (a::l) = a $ (Bound 1) $ (comp l); val nameset_eq = mk_eq ((Free (base_name, dummyT)), (Abs ("_", dummyT, (Abs ("_", dummyT, comp formulas))))); in thy |> Named_Target.theory_init |> Specification.definition (SOME (Binding.qualify_name true binding base_name, NONE, NoSyn)) [] [] (Binding.empty_atts, nameset_eq) |> snd |> Local_Theory.exit_global end; fun define_schema binding (ex_binding, expr) (alph_bind, alpha, state) thy = let val fields_names = (map (fn (x, T) => (Binding.name_of x, T)) (alpha @ state)); val alpha' = (map (fn (x, T) => (Binding.name_of x, T)) alpha); val state' = (map (fn (x, T) => (Binding.name_of x, T)) state); val all_selectors = get_fields (Record.get_info thy (Sign.full_name thy alph_bind)) thy val base_name = Binding.name_of ex_binding; val ctxt = Proof_Context.init_global thy; val term = Syntax.read_term (ctxt |> VARs_Data.put ({State_vars=(map fst state'), Alpha_vars=(map fst alpha')}) |> Config.put Syntax.root @{nonterminal circus_schema}) expr; val sc_eq = mk_eq ((Free (base_name, dummyT)), term); in thy |> Named_Target.theory_init |> Specification.definition (SOME (Binding.qualify_name true binding base_name, NONE, NoSyn)) [] [] (Binding.empty_atts, sc_eq) |> snd |> Local_Theory.exit_global end; fun define_action binding (ex_binding, expr) alph_bind chan_bind thy = let val base_name = Binding.name_of ex_binding; val ctxt = Proof_Context.init_global thy; val actT = "Circus_Actions.action"; val action_eq = mk_eq ((Free (base_name, Type (actT, [(Proof_Context.read_type_name {proper=true, strict=false} ctxt (Sign.full_name thy chan_bind)), (Proof_Context.read_type_name {proper=true, strict=false} ctxt (Sign.full_name thy alph_bind))]))), (Syntax.parse_term ctxt expr)); in thy |> Named_Target.theory_init |> Specification.definition (SOME (Binding.qualify_name true binding base_name, NONE, NoSyn)) [] [] (Binding.empty_atts, action_eq) |> snd |> Local_Theory.exit_global end; fun define_expr binding (alph_bind, alpha, state) chan_bind (ex_binding, (is_schema, expr)) = if is_schema then define_schema binding (ex_binding, expr) (alph_bind, alpha, state) else define_action binding (ex_binding, expr) alph_bind chan_bind; fun prep_field prep_typ (b: binding, raw_T) ctxt = let val T = prep_typ ctxt raw_T; val ctxt' = Variable.declare_typ T ctxt; in ((b, T), ctxt') end; fun prep_constr prep_typ (b: binding, raw_T) ctxt = let val T = Option.map (prep_typ ctxt) raw_T; val ctxt' = fold Variable.declare_typ (the_list T) ctxt; in ((b, T), ctxt') end; fun gen_circus_process prep_constraint prep_typ (raw_params, binding) raw_alphabet raw_state (typesyn, raw_channels) namesets chansets exprs act thy = let val ctxt = Proof_Context.init_global thy; (* internalize arguments *) val params = map (prep_constraint ctxt) raw_params; val ctxt0 = fold (Variable.declare_typ o TFree) params ctxt; val (alphabet, ctxt1) = fold_map (prep_field prep_typ) raw_alphabet ctxt0; val (state, ctxt2) = fold_map (prep_field prep_typ) raw_state ctxt1; val (channels, ctxt3) = fold_map (prep_constr prep_typ) raw_channels ctxt2; val params' = map (Proof_Context.check_tfree ctxt3) params; (* type definitions *) val fields = map (fn (b, T) => (b, T, NoSyn)) (map (apsnd HOLogic.listT) alphabet @ state); val thy1 = thy |> not (null fields) ? Record.add_record {overloaded = false} (params', Binding.suffix_name "_alphabet" binding) NONE fields; val (channel_constrs, thy2) = if not (null channels) orelse is_some typesyn then apfst snd (define_channels (params', binding) typesyn channels thy1) else ([], thy1); val thy3 = thy2 |> not (null chansets) ? fold (define_chanset binding channel_constrs) chansets |> not (null namesets) ? fold (define_nameset binding ((Binding.suffix_name "_alphabet" binding), alphabet)) namesets |> not (null exprs) ? fold (define_expr binding ((Binding.suffix_name "_alphabet" binding), alphabet, state) (Binding.suffix_name "_channels" binding)) exprs |> define_action binding (binding, act) (Binding.suffix_name "_alphabet" binding) (Binding.suffix_name "_channels" binding); in thy3 end; fun circus_process x = gen_circus_process (K I) Syntax.check_typ x; fun circus_process_cmd x = gen_circus_process (apsnd o Typedecl.read_constraint) Syntax.read_typ x; local val fields = @{keyword "["} |-- Parse.enum1 "," (Parse.binding -- (@{keyword "::"} |-- Parse.!!! Parse.typ)) --| @{keyword "]"}; val constrs = (@{keyword "["} |-- Parse.enum1 "," (Parse.binding -- Scan.option Parse.typ) --| @{keyword "]"}) >> pair NONE || Parse.typ >> (fn b => (SOME b, [])); val names = @{keyword "["} |-- Parse.enum1 "," Parse.name --| @{keyword "]"}; in val _ = Outer_Syntax.command @{command_keyword circus_process} "Circus process specification" ((Parse.type_args_constrained -- Parse.binding --| @{keyword "="}) -- Scan.optional (@{keyword "alphabet"} |-- Parse.!!! (@{keyword "="} |-- fields)) [] -- Scan.optional (@{keyword "state"} |-- Parse.!!! (@{keyword "="} |-- fields)) [] -- Scan.optional (@{keyword "channel"} |-- Parse.!!! (@{keyword "="} |-- constrs)) (NONE, []) -- Scan.repeat (@{keyword "nameset"} |-- Parse.!!! ((Parse.binding --| @{keyword "="}) -- names)) -- Scan.repeat (@{keyword "chanset"} |-- Parse.!!! ((Parse.binding --| @{keyword "="}) -- names)) -- Scan.repeat ((@{keyword "schema"} |-- Parse.!!! ((Parse.binding --| @{keyword "="}) -- (Parse.term >> pair true))) || (@{keyword "action"} |-- Parse.!!! ((Parse.binding --| @{keyword "="}) -- (Parse.term >> pair false)))) -- (Parse.where_ |-- Parse.!!! Parse.term) >> (fn (((((((a, b), c), d), e), f), g), h) => Toplevel.theory (circus_process_cmd a b c d e f g h))); end; \ end diff --git a/thys/Deriving/Comparator_Generator/comparator_generator.ML b/thys/Deriving/Comparator_Generator/comparator_generator.ML --- a/thys/Deriving/Comparator_Generator/comparator_generator.ML +++ b/thys/Deriving/Comparator_Generator/comparator_generator.ML @@ -1,630 +1,641 @@ (* Title: Deriving class instances for datatypes Author: Christian Sternagel and René Thiemann Maintainer: Christian Sternagel and René Thiemann License: LGPL *) signature COMPARATOR_GENERATOR = sig type info = {map : term, (* take % x. x, if there is no map *) pcomp : term, (* partial comparator *) comp : term, (* full comparator *) comp_def : thm option, (* definition of comparator, important for nesting *) map_comp : thm option, (* compositionality of map, important for nesting *) partial_comp_thms : thm list, (* first eq, then sym, finally trans *) comp_thm : thm, (* comparator acomp \ \ \ comparator (full_comp acomp \) *) used_positions : bool list} (* registers @{term comparator_of :: "some_type :: linorder comparator"} where some_type must just be a type without type-arguments *) val register_comparator_of : string -> local_theory -> local_theory val register_foreign_comparator : typ -> (* type-constant without type-variables *) term -> (* comparator for type *) thm -> (* comparator thm for provided comparator *) local_theory -> local_theory val register_foreign_partial_and_full_comparator : string -> (* long type name *) term -> (* map function, should be \x. x, if there is no map *) term -> (* partial comparator of type ('a => order, 'b)ty => ('a,'b)ty => order, where 'a is used, 'b is unused *) term -> (* (full) comparator of type ('a \ 'a \ order) \ ('a,'b)ty \ ('a,'b)ty \ order, where 'a is used, 'b is unused *) thm option -> (* comp_def, should be full_comp = pcomp o map acomp ..., important for nesting *) thm option -> (* map compositionality, important for nesting *) thm -> (* partial eq thm for full comparator *) thm -> (* partial sym thm for full comparator *) thm -> (* partial trans thm for full comparator *) thm -> (* full thm: comparator a-comp => comparator (full_comp a-comp) *) bool list -> (*used positions*) local_theory -> local_theory datatype comparator_type = Linorder | BNF val generate_comparators_from_bnf_fp : string -> (* name of type *) local_theory -> ((term * thm list) list * (* partial comparators + simp-rules *) (term * thm) list) * (* non-partial comparator + def_rule *) local_theory val generate_comparator : comparator_type -> string -> (* name of type *) local_theory -> local_theory val get_info : Proof.context -> string -> info option (* ensures that the info will be available on later requests *) val ensure_info : comparator_type -> string -> local_theory -> local_theory end structure Comparator_Generator : COMPARATOR_GENERATOR = struct open Generator_Aux datatype comparator_type = BNF | Linorder val debug = false fun debug_out s = if debug then writeln s else () val orderT = @{typ order} fun compT T = T --> T --> orderT val orderify = map_atyps (fn T => T --> orderT) fun pcompT T = orderify T --> T --> orderT type info = {map : term, pcomp : term, comp : term, comp_def : thm option, map_comp : thm option, partial_comp_thms : thm list, comp_thm : thm, used_positions : bool list}; structure Data = Generic_Data ( type T = info Symtab.table; val empty = Symtab.empty; val extend = I; val merge = Symtab.merge (fn (info1 : info, info2 : info) => #comp info1 = #comp info2); ); fun add_info T info = Data.map (Symtab.update_new (T, info)) val get_info = Context.Proof #> Data.get #> Symtab.lookup fun the_info ctxt tyco = (case get_info ctxt tyco of SOME info => info | NONE => error ("no comparator information available for type " ^ quote tyco)) fun declare_info tyco m p c c_def m_comp p_thms c_thm used_pos = Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => add_info tyco {map = Morphism.term phi m, pcomp = Morphism.term phi p, comp = Morphism.term phi c, comp_def = Option.map (Morphism.thm phi) c_def, map_comp = Option.map (Morphism.thm phi) m_comp, partial_comp_thms = Morphism.fact phi p_thms, comp_thm = Morphism.thm phi c_thm, used_positions = used_pos}) val EQ = 0 val SYM = 1 val TRANS = 2 fun register_foreign_partial_and_full_comparator tyco m p c c_def m_comp eq_thm sym_thm trans_thm c_thm = declare_info tyco m p c c_def m_comp [eq_thm, sym_thm, trans_thm] c_thm fun mk_infer_const name ctxt c = infer_type ctxt (Const (name, dummyT) $ c) val mk_eq_comp = mk_infer_const @{const_name eq_comp} val mk_peq_comp = mk_infer_const @{const_name peq_comp} val mk_sym_comp = mk_infer_const @{const_name sym_comp} val mk_psym_comp = mk_infer_const @{const_name psym_comp} val mk_trans_comp = mk_infer_const @{const_name trans_comp} val mk_ptrans_comp = mk_infer_const @{const_name ptrans_comp} val mk_comp = mk_infer_const @{const_name comparator} fun default_comp T = absdummy T (absdummy T @{term Eq}) (*%_ _. Eq*) fun register_foreign_comparator T comp comp_thm lthy = let val tyco = (case T of Type (tyco, []) => tyco | _ => error "expected type constant") val eq = @{thm comp_to_peq_comp} OF [comp_thm] val sym = @{thm comp_to_psym_comp} OF [comp_thm] val trans = @{thm comp_to_ptrans_comp} OF [comp_thm] in register_foreign_partial_and_full_comparator tyco (HOLogic.id_const T) comp comp NONE NONE eq sym trans comp_thm [] lthy end fun register_comparator_of tyco lthy = let val T = Type (tyco, []) val comp = Const (@{const_name comparator_of}, compT T) val comp_thm = Thm.instantiate' [SOME (Thm.ctyp_of lthy T)] [] @{thm comparator_of} in register_foreign_comparator T comp comp_thm lthy end fun generate_comparators_from_bnf_fp tyco lthy = let val (tycos, Ts) = mutual_recursive_types tyco lthy val _ = map (fn tyco => "generating comparator for type " ^ quote tyco) tycos |> cat_lines |> writeln val (tfrees, used_tfrees) = type_parameters (hd Ts) lthy val used_positions = map (member (op =) used_tfrees o TFree) tfrees val cs = map (subT "comp") used_tfrees val comp_Ts = map compT used_tfrees val arg_comps = map Free (cs ~~ comp_Ts) val dep_tycos = fold (add_used_tycos lthy) tycos [] val XTys = Bnf_Access.bnf_types lthy tycos val inst_types = typ_subst_atomic (XTys ~~ Ts) val cTys = map (map (map inst_types)) (Bnf_Access.constr_argument_types lthy tycos) val map_simps = Bnf_Access.map_simps lthy tycos val case_simps = Bnf_Access.case_simps lthy tycos val maps = Bnf_Access.map_terms lthy tycos val map_comp_thms = Bnf_Access.map_comps lthy tycos val t_ixs = 0 upto (length Ts - 1) val compNs = (*TODO: clashes in presence of same type names in different theories*) map (Long_Name.base_name) tycos |> map (fn s => "comparator_" ^ s) fun gen_vars prefix = map (fn (i, pty) => Free (prefix ^ ints_to_subscript [i], pty)) (t_ixs ~~ Ts) (* primrec definitions of partial comparators *) fun mk_pcomp (tyco, T) = ("partial_comparator_" ^ Long_Name.base_name tyco, pcompT T) fun constr_terms lthy = Bnf_Access.constr_terms lthy #> map (apsnd (map freeify_tvars o fst o strip_type) o dest_Const) fun generate_pcomp_eqs lthy (tyco, T) = let val constrs = constr_terms lthy tyco fun comp_arg T x y = let val m = Generator_Aux.create_map default_comp (K o Free o mk_pcomp) () (K false) (#used_positions oo the_info) (#map oo the_info) (K o #pcomp oo the_info) tycos ((K o K) ()) T lthy val p = Generator_Aux.create_partial () (K false) (#used_positions oo the_info) (#map oo the_info) (K o #pcomp oo the_info) tycos ((K o K) ()) T lthy in p $ (m $ x) $ y |> infer_type lthy end fun generate_eq lthy (c_T as (cN, Ts)) = let val arg_Ts' = map orderify Ts val c = Const (cN, arg_Ts' ---> orderify T) val (y, (xs, ys)) = Name.variant "y" (Variable.names_of lthy) |>> Free o rpair T ||> (fn ctxt => Name.invent_names ctxt "x" (arg_Ts' @ Ts) |> map Free) ||> chop (length Ts) val k = find_index (curry (op =) c_T) constrs val cases = constrs |> map_index (fn (i, (_, Ts')) => if i < k then fold_rev absdummy Ts' @{term Gt} else if k < i then fold_rev absdummy Ts' @{term Lt} else @{term comp_lex} $ HOLogic.mk_list orderT (@{map 3} comp_arg Ts xs ys) |> lambdas ys) val lhs = Free (mk_pcomp (tyco, T)) $ list_comb (c, xs) $ y val rhs = list_comb (singleton (Bnf_Access.case_consts lthy) tyco, cases) $ y in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |> infer_type lthy end in map (generate_eq lthy) constrs end val eqs = map (generate_pcomp_eqs lthy) (tycos ~~ Ts) |> flat val bindings = tycos ~~ Ts |> map mk_pcomp |> map (fn (name, T) => (Binding.name name, SOME T, NoSyn)) - val ((pcomps, pcomp_simps), lthy) = Local_Theory.subtarget_result - (fn phi => fn (pcomps, _, pcomp_simps) => (map (Morphism.term phi) pcomps, map (Morphism.fact phi) pcomp_simps)) - (BNF_LFP_Rec_Sugar.primrec false [] bindings - (map (fn t => ((Binding.empty_atts, t), [], [])) eqs)) lthy + val ((pcomps, pcomp_simps), lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> (BNF_LFP_Rec_Sugar.primrec false [] bindings + (map (fn t => ((Binding.empty_atts, t), [], [])) eqs)) + |> Local_Theory.end_nested_result (fn phi => fn (pcomps, _, pcomp_simps) => (map (Morphism.term phi) pcomps, map (Morphism.fact phi) pcomp_simps)) (* definitions of comparators via partial comparators and maps *) fun generate_comp_def tyco lthy = let val cs = map (subT "comp") used_tfrees val arg_Ts = map compT used_tfrees val args = map Free (cs ~~ arg_Ts) val (pcomp, m) = AList.lookup (op =) (tycos ~~ (pcomps ~~ maps)) tyco |> the val ts = tfrees |> map TFree |> map (fn T => AList.lookup (op =) (used_tfrees ~~ args) T |> the_default (default_comp T)) val rhs = HOLogic.mk_comp (pcomp, list_comb (m, ts)) |> infer_type lthy val abs_def = lambdas args rhs val name = "comparator_" ^ Long_Name.base_name tyco val ((comp, (_, prethm)), lthy) = Local_Theory.define ((Binding.name name, NoSyn), (Binding.empty_atts, abs_def)) lthy val eq = Logic.mk_equals (list_comb (comp, args), rhs) val thm = Goal.prove lthy (map (fst o dest_Free) args) [] eq (K (unfold_tac lthy [prethm])) in Local_Theory.note ((Binding.name (name ^ "_def"), []), [thm]) lthy |>> the_single o snd |>> `(K comp) end - val ((comps, comp_defs), lthy) = Local_Theory.subtarget_result - (fn phi => fn (comps, comp_defs) => (map (Morphism.term phi) comps, map (Morphism.thm phi) comp_defs)) - (fold_map generate_comp_def tycos #>> split_list) lthy + val ((comps, comp_defs), lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map generate_comp_def tycos + |>> split_list + |> Local_Theory.end_nested_result + (fn phi => fn (comps, comp_defs) => (map (Morphism.term phi) comps, map (Morphism.thm phi) comp_defs)) (* alternative simp-rules for comparators *) val full_comps = map (list_comb o rpair arg_comps) comps fun generate_comp_simps (tyco, T) lthy = let val constrs = constr_terms lthy tyco fun comp_arg T x y = let fun create_comp (T as TFree _) = AList.lookup (op =) (used_tfrees ~~ arg_comps) T |> the_default (HOLogic.id_const dummyT) | create_comp (Type (tyco, Ts)) = (case AList.lookup (op =) (tycos ~~ comps) tyco of SOME c => list_comb (c, arg_comps) | NONE => let val {comp = c, used_positions = up, ...} = the_info lthy tyco val ts = (up ~~ Ts) |> map_filter (fn (b, T) => if b then SOME (create_comp T) else NONE) in list_comb (c, ts) end) | create_comp T = error ("unexpected schematic variable " ^ quote (Syntax.string_of_typ lthy T)) val comp = create_comp T in comp $ x $ y |> infer_type lthy end fun generate_eq_thm lthy (c_T as (_, Ts)) = let val (xs, ctxt) = Variable.names_of lthy |> fold_map (fn T => Name.variant "x" #>> Free o rpair T) Ts fun mk_const (c, Ts) = Const (c, Ts ---> T) val comp_const = AList.lookup (op =) (tycos ~~ comps) tyco |> the val lhs = list_comb (comp_const, arg_comps) $ list_comb (mk_const c_T, xs) val k = find_index (curry (op =) c_T) constrs fun mk_eq c ys rhs = let val y = list_comb (mk_const c, ys) val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs $ y, rhs)) in (ys, eq |> infer_type lthy) end val ((ys, eqs), _) = fold_map (fn (i, c as (_, Ts')) => fn ctxt => let val (ys, ctxt) = fold_map (fn T => Name.variant "y" #>> Free o rpair T) Ts' ctxt in (if i < k then mk_eq c ys @{term Gt} else if k < i then mk_eq c ys @{term Lt} else @{term comp_lex} $ HOLogic.mk_list orderT (@{map 3} comp_arg Ts xs ys) |> mk_eq c ys, ctxt) end) (tag_list 0 constrs) ctxt |> apfst (apfst flat o split_list) val dep_comp_defs = map_filter (#comp_def o the_info lthy) dep_tycos val dep_map_comps = map_filter (#map_comp o the_info lthy) dep_tycos val thms = prove_multi_future lthy (map (fst o dest_Free) (xs @ ys) @ cs) [] eqs (fn {context = ctxt, ...} => Goal.conjunction_tac 1 THEN unfold_tac ctxt (@{thms id_apply o_def} @ flat case_simps @ flat pcomp_simps @ dep_map_comps @ comp_defs @ dep_comp_defs @ flat map_simps)) in thms end val thms = map (generate_eq_thm lthy) constrs |> flat val simp_thms = map (Local_Defs.unfold lthy @{thms comp_lex_unfolds}) thms val name = "comparator_" ^ Long_Name.base_name tyco in lthy |> Local_Theory.note ((Binding.name (name ^ "_simps"), @{attributes [simp, code]}), simp_thms) |> snd |> (fn lthy => (thms, lthy)) end - val (comp_simps, lthy) = Local_Theory.subtarget_result - (fn phi => map (Morphism.fact phi)) - (fold_map generate_comp_simps (tycos ~~ Ts)) lthy + val (comp_simps, lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map generate_comp_simps (tycos ~~ Ts) + |> Local_Theory.end_nested_result (fn phi => map (Morphism.fact phi)) (* partial theorems *) val set_funs = Bnf_Access.set_terms lthy tycos val x_vars = gen_vars "x" val free_names = map (fst o dest_Free) (x_vars @ arg_comps) val xi_vars = map_index (fn (i, _) => map_index (fn (j, pty) => Free ("x" ^ ints_to_subscript [i, j], pty)) used_tfrees) Ts fun mk_eq_sym_trans_thm' mk_eq_sym_trans' = map_index (fn (i, ((set_funs, x), xis)) => let fun create_cond ((set_t, xi), c) = let val rhs = mk_eq_sym_trans' lthy c $ xi |> HOLogic.mk_Trueprop val lhs = HOLogic.mk_mem (xi, set_t $ x) |> HOLogic.mk_Trueprop in Logic.all xi (Logic.mk_implies (lhs, rhs)) end val used_sets = map (the o AList.lookup (op =) (map TFree tfrees ~~ set_funs)) used_tfrees val conds = map create_cond (used_sets ~~ xis ~~ arg_comps) val concl = mk_eq_sym_trans' lthy (nth full_comps i) $ x |> HOLogic.mk_Trueprop in Logic.list_implies (conds, concl) |> infer_type lthy end) (set_funs ~~ x_vars ~~ xi_vars) val induct_thms = Bnf_Access.induct_thms lthy tycos val set_simps = Bnf_Access.set_simps lthy tycos val case_thms = Bnf_Access.case_thms lthy tycos val distinct_thms = Bnf_Access.distinct_thms lthy tycos val inject_thms = Bnf_Access.inject_thms lthy tycos val rec_info = (the_info lthy, #used_positions, tycos) val split_IHs = split_IHs rec_info val unknown_value = false (* effect of choosing false / true not yet visible *) fun induct_tac ctxt f = ((DETERM o Induction.induction_tac ctxt false (map (fn x => [SOME (NONE, (x, unknown_value))]) x_vars) [] [] (SOME induct_thms) []) THEN_ALL_NEW (fn i => Subgoal.SUBPROOF (fn {context = ctxt, prems = prems, params = iparams, ...} => f (i - 1) ctxt prems iparams) ctxt i)) 1 fun recursor_tac kind = std_recursor_tac rec_info used_tfrees (fn info => nth (#partial_comp_thms info) kind) fun instantiate_IHs IHs pre_conds = map (fn IH => OF_option IH (replicate (Thm.nprems_of IH - length pre_conds) NONE @ map SOME pre_conds)) IHs fun get_v_i vs k = nth vs k |> snd |> SOME (* partial eq-theorem *) val _ = debug_out "Partial equality" val eq_thms' = mk_eq_sym_trans_thm' mk_peq_comp fun eq_solve_tac i ctxt IH_prems xs = let val (i, j) = ind_case_to_idxs cTys i val k = length IH_prems - length arg_comps val pre_conds = drop k IH_prems val IH = take k IH_prems val comp_simps = nth comp_simps i val case_thm = nth case_thms i val distinct_thms = nth distinct_thms i val inject_thms = nth inject_thms i val set_thms = nth set_simps i in (* after induction *) resolve_tac ctxt @{thms peq_compI} 1 THEN Subgoal.FOCUS (fn focus => let val y = #params focus |> hd val yt = y |> snd |> Thm.term_of val ctxt = #context focus val pre_cond = map (fn pre_cond => Local_Defs.unfold ctxt set_thms pre_cond) pre_conds val IH = instantiate_IHs IH pre_cond val xs_tys = map (fastype_of o Thm.term_of o snd) xs val IHs = split_IHs xs_tys IH fun sub_case_tac j' (ctxt, y_simp, _) = if j = j' then unfold_tac ctxt (y_simp @ comp_simps) THEN unfold_tac ctxt @{thms comp_lex_eq} THEN unfold_tac ctxt (@{thms in_set_simps} @ inject_thms @ @{thms refl_True}) THEN conjI_tac @{thms conj_weak_cong} ctxt xs (fn ctxt' => fn k => resolve_tac ctxt @{thms peq_compD} 1 THEN recursor_tac EQ pre_cond (nth xs_tys k) (nth IHs k) ctxt') else (* different constructors *) unfold_tac ctxt (y_simp @ distinct_thms @ comp_simps @ @{thms order.simps}) in mk_case_tac ctxt [[SOME yt]] case_thm sub_case_tac end ) ctxt 1 end val eq_thms' = prove_multi_future lthy free_names [] eq_thms' (fn {context = ctxt, ...} => induct_tac ctxt eq_solve_tac) val _ = debug_out (@{make_string} eq_thms') (* partial symmetry-theorem *) val _ = debug_out "Partial symmetry" val sym_thms' = mk_eq_sym_trans_thm' mk_psym_comp fun sym_solve_tac i ctxt IH_prems xs = let val (i, j) = ind_case_to_idxs cTys i val k = length IH_prems - length arg_comps val pre_conds = drop k IH_prems val IH = take k IH_prems val comp_simps = nth comp_simps i val case_thm = nth case_thms i val set_thms = nth set_simps i in (* after induction *) resolve_tac ctxt @{thms psym_compI} 1 THEN Subgoal.FOCUS (fn focus => let val y = #params focus |> hd val yt = y |> snd |> Thm.term_of val ctxt = #context focus val pre_cond = map (fn pre_cond => Local_Defs.unfold ctxt set_thms pre_cond) pre_conds val IH = instantiate_IHs IH pre_cond val xs_tys = map (fastype_of o Thm.term_of o snd) xs val IHs = split_IHs xs_tys IH fun sub_case_tac j' (ctxt, y_simp, ys) = if j = j' then unfold_tac ctxt (y_simp @ comp_simps) THEN resolve_tac ctxt @{thms comp_lex_sym} 1 THEN unfold_tac ctxt (@{thms length_nth_simps forall_finite}) THEN conjI_tac @{thms conjI} ctxt xs (fn ctxt' => fn k => resolve_tac ctxt' [infer_instantiate' ctxt' [NONE, get_v_i xs k, get_v_i ys k] @{thm psym_compD}] 1 THEN recursor_tac SYM pre_cond (nth xs_tys k) (nth IHs k) ctxt') else (* different constructors *) unfold_tac ctxt (y_simp @ comp_simps @ @{thms invert_order.simps}) in mk_case_tac ctxt [[SOME yt]] case_thm sub_case_tac end ) ctxt 1 end val sym_thms' = prove_multi_future lthy free_names [] sym_thms' (fn {context = ctxt, ...} => induct_tac ctxt sym_solve_tac) val _ = debug_out (@{make_string} sym_thms') (* partial transitivity-theorem *) val _ = debug_out "Partial transitivity" val trans_thms' = mk_eq_sym_trans_thm' mk_ptrans_comp fun trans_solve_tac i ctxt IH_prems xs = let val (i, j) = ind_case_to_idxs cTys i val k = length IH_prems - length arg_comps val pre_conds = drop k IH_prems val IH = take k IH_prems val comp_simps = nth comp_simps i val case_thm = nth case_thms i val set_thms = nth set_simps i in (* after induction *) resolve_tac ctxt @{thms ptrans_compI} 1 THEN Subgoal.FOCUS (fn focus => let val y = nth (#params focus) 0 val z = nth (#params focus) 1 val yt = y |> snd |> Thm.term_of val zt = z |> snd |> Thm.term_of val ctxt = #context focus val pre_cond = map (fn pre_cond => Local_Defs.unfold ctxt set_thms pre_cond) pre_conds val IH = instantiate_IHs IH pre_cond val xs_tys = map (fastype_of o Thm.term_of o snd) xs val IHs = split_IHs xs_tys IH fun sub_case_tac j' (ctxt, y_simp, ys) = let fun sub_case_tac' j'' (ctxt, z_simp, zs) = if j = j' andalso j = j'' then unfold_tac ctxt (y_simp @ z_simp @ comp_simps) THEN resolve_tac ctxt @{thms comp_lex_trans} 1 THEN unfold_tac ctxt (@{thms length_nth_simps forall_finite}) THEN conjI_tac @{thms conjI} ctxt xs (fn ctxt' => fn k => resolve_tac ctxt' [infer_instantiate' ctxt' [NONE, get_v_i xs k, get_v_i ys k, get_v_i zs k] @{thm ptrans_compD}] 1 THEN recursor_tac TRANS pre_cond (nth xs_tys k) (nth IHs k) ctxt') else (* different constructors *) unfold_tac ctxt (y_simp @ z_simp @ comp_simps @ @{thms trans_order_different}) in mk_case_tac ctxt [[SOME zt]] case_thm sub_case_tac' end in mk_case_tac ctxt [[SOME yt]] case_thm sub_case_tac end ) ctxt 1 end val trans_thms' = prove_multi_future lthy free_names [] trans_thms' (fn {context = ctxt, ...} => induct_tac ctxt trans_solve_tac) val _ = debug_out (@{make_string} trans_thms') (* total theorems *) fun mk_eq_sym_trans_thm mk_eq_sym_trans compI2 compE2 thms' = let val conds = map (fn c => mk_eq_sym_trans lthy c |> HOLogic.mk_Trueprop) arg_comps val thms = map (fn i => mk_eq_sym_trans lthy (nth full_comps i) |> HOLogic.mk_Trueprop |> (fn concl => Logic.list_implies (conds,concl))) t_ixs val thms = prove_multi_future lthy free_names [] thms (fn {context = ctxt, ...} => ALLGOALS Goal.conjunction_tac THEN Method.intros_tac ctxt (@{thm conjI} :: compI2 :: thms') [] THEN ALLGOALS (eresolve_tac ctxt [compE2])) in thms end val eq_thms = mk_eq_sym_trans_thm mk_eq_comp @{thm eq_compI2} @{thm eq_compD2} eq_thms' val sym_thms = mk_eq_sym_trans_thm mk_sym_comp @{thm sym_compI2} @{thm sym_compD2} sym_thms' val trans_thms = mk_eq_sym_trans_thm mk_trans_comp @{thm trans_compI2} @{thm trans_compD2} trans_thms' val _ = debug_out "full comparator thms" fun mk_comp_thm (i, ((e, s), t)) = let val conds = map (fn c => mk_comp lthy c |> HOLogic.mk_Trueprop) arg_comps fun from_comp thm i = thm OF replicate (Thm.prems_of thm |> length) (nth @{thms comparator_imp_eq_sym_trans} i) val nearly_thm = @{thm eq_sym_trans_imp_comparator} OF [from_comp e EQ, from_comp s SYM, from_comp t TRANS] val thm = mk_comp lthy (nth full_comps i) |> HOLogic.mk_Trueprop |> (fn concl => Logic.list_implies (conds, concl)) in Goal.prove_future lthy free_names [] thm (K (resolve_tac lthy [nearly_thm] 1 THEN ALLGOALS (assume_tac lthy))) end val comp_thms = map_index mk_comp_thm (eq_thms ~~ sym_thms ~~ trans_thms) val (_, lthy) = fold_map (fn (thm, cname) => Local_Theory.note ((Binding.name cname, []), [thm])) (comp_thms ~~ compNs) lthy val _ = debug_out (@{make_string} comp_thms) val pcomp_thms = map (fn ((e, s), t) => [e, s, t]) (eq_thms' ~~ sym_thms' ~~ trans_thms') val (_, lthy) = fold_map (fn (thms, cname) => Local_Theory.note ((Binding.name (cname ^ "_pointwise"), []), thms)) (pcomp_thms ~~ compNs) lthy in ((pcomps ~~ pcomp_simps, comps ~~ comp_defs), lthy) ||> fold (fn (((((((tyco, map), pcomp), comp), comp_def), map_comp), pcomp_thms), comp_thm) => declare_info tyco map pcomp comp (SOME comp_def) (SOME map_comp) pcomp_thms comp_thm used_positions) (tycos ~~ maps ~~ pcomps ~~ comps ~~ comp_defs ~~ map_comp_thms ~~ pcomp_thms ~~ comp_thms) end fun generate_comparator gen_type tyco lthy = let val _ = is_some (get_info lthy tyco) andalso error ("type " ^ quote tyco ^ " does already have a comparator") in case gen_type of BNF => generate_comparators_from_bnf_fp tyco lthy |> snd | Linorder => register_comparator_of tyco lthy end fun ensure_info gen_type tyco lthy = (case get_info lthy tyco of SOME _ => lthy | NONE => generate_comparator gen_type tyco lthy) fun generate_comparator_cmd tyco param = Named_Target.theory_map ( if param = "linorder" then generate_comparator Linorder tyco else if param = "" then generate_comparator BNF tyco else error ("unknown parameter, expecting no parameter for BNF-datatypes, " ^ "or \"linorder\" for types which are already in linorder")) val _ = Theory.setup (Derive_Manager.register_derive "comparator" "generate comparators for given types, options: (linorder) or ()" generate_comparator_cmd) end diff --git a/thys/Deriving/Equality_Generator/equality_generator.ML b/thys/Deriving/Equality_Generator/equality_generator.ML --- a/thys/Deriving/Equality_Generator/equality_generator.ML +++ b/thys/Deriving/Equality_Generator/equality_generator.ML @@ -1,505 +1,517 @@ (* Title: Deriving class instances for datatypes Author: Christian Sternagel and René Thiemann Maintainer: Christian Sternagel and René Thiemann License: LGPL *) signature EQUALITY_GENERATOR = sig type info = {map : term, (* take % x. x, if there is no map *) pequality : term, (* partial equality *) equality : term, (* full equality *) equality_def : thm option, (* definition of equality, important for nesting *) map_comp : thm option, (* compositionality of map, important for nesting *) partial_equality_thm : thm, (* partial version of equality thm *) equality_thm : thm, (* equality acomp \ \ \ equality (full_comp acomp \) *) used_positions : bool list} (* registers @{term equality_of :: "some_type :: linorder equality"} where some_type must just be a type without type-arguments *) val register_equality_of : string -> local_theory -> local_theory val register_foreign_equality : typ -> (* type-constant without type-variables *) term -> (* equality for type *) thm -> (* equality thm for provided equality *) local_theory -> local_theory val register_foreign_partial_and_full_equality : string -> (* long type name *) term -> (* map function, should be \x. x, if there is no map *) term -> (* partial equality of type ('a => order, 'b)ty => ('a,'b)ty => order, where 'a is used, 'b is unused *) term -> (* (full) equality of type ('a \ 'a \ order) \ ('a,'b)ty \ ('a,'b)ty \ order, where 'a is used, 'b is unused *) thm option -> (* comp_def, should be full_comp = pcomp o map acomp ..., important for nesting *) thm option -> (* map compositionality, important for nesting *) thm -> (* partial eq thm for full equality *) thm -> (* full thm: equality a-comp => equality (full_comp a-comp) *) bool list -> (*used positions*) local_theory -> local_theory datatype equality_type = EQ | BNF val generate_equalitys_from_bnf_fp : string -> (* name of type *) local_theory -> ((term * thm list) list * (* partial equalitys + simp-rules *) (term * thm) list) * (* non-partial equality + def_rule *) local_theory val generate_equality : equality_type -> string -> (* name of type *) local_theory -> local_theory val get_info : Proof.context -> string -> info option (* ensures that the info will be available on later requests *) val ensure_info : equality_type -> string -> local_theory -> local_theory end structure Equality_Generator : EQUALITY_GENERATOR = struct open Generator_Aux datatype equality_type = BNF | EQ val debug = false fun debug_out s = if debug then writeln s else () val boolT = @{typ bool} fun compT T = T --> T --> boolT val orderify = map_atyps (fn T => T --> boolT) fun pcompT T = orderify T --> T --> boolT type info = {map : term, pequality : term, equality : term, equality_def : thm option, map_comp : thm option, partial_equality_thm : thm, equality_thm : thm, used_positions : bool list}; structure Data = Generic_Data ( type T = info Symtab.table; val empty = Symtab.empty; val extend = I; val merge = Symtab.merge (fn (info1 : info, info2 : info) => #equality info1 = #equality info2); ); fun add_info T info = Data.map (Symtab.update_new (T, info)) val get_info = Context.Proof #> Data.get #> Symtab.lookup fun the_info ctxt tyco = (case get_info ctxt tyco of SOME info => info | NONE => error ("no equality information available for type " ^ quote tyco)) fun declare_info tyco m p c c_def m_comp p_thm c_thm used_pos = Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => add_info tyco {map = Morphism.term phi m, pequality = Morphism.term phi p, equality = Morphism.term phi c, equality_def = Option.map (Morphism.thm phi) c_def, map_comp = Option.map (Morphism.thm phi) m_comp, partial_equality_thm = Morphism.thm phi p_thm, equality_thm = Morphism.thm phi c_thm, used_positions = used_pos}) fun register_foreign_partial_and_full_equality tyco m p c c_def m_comp eq_thm c_thm = declare_info tyco m p c c_def m_comp eq_thm c_thm val mk_equality = mk_infer_const @{const_name equality} val mk_pequality = mk_infer_const @{const_name pequality} fun default_comp T = absdummy T (absdummy T @{term True}) (*%_ _. True*) fun register_foreign_equality T comp comp_thm lthy = let val tyco = (case T of Type (tyco, []) => tyco | _ => error "expected type constant with no arguments") val eq = @{thm equalityD2} OF [comp_thm] in register_foreign_partial_and_full_equality tyco (HOLogic.id_const T) comp comp NONE NONE eq comp_thm [] lthy end fun register_equality_of tyco lthy = let val (T,_) = typ_and_vs_of_typname (Proof_Context.theory_of lthy) tyco @{sort type} val comp = HOLogic.eq_const T val comp_thm = Thm.instantiate' [SOME (Thm.ctyp_of lthy T)] [] @{thm eq_equality} in register_foreign_equality T comp comp_thm lthy end fun generate_equalitys_from_bnf_fp tyco lthy = let val (tycos, Ts) = mutual_recursive_types tyco lthy val _ = map (fn tyco => "generating equality for type " ^ quote tyco) tycos |> cat_lines |> writeln val (tfrees, used_tfrees) = type_parameters (hd Ts) lthy val used_positions = map (member (op =) used_tfrees o TFree) tfrees val cs = map (subT "eq") used_tfrees val comp_Ts = map compT used_tfrees val arg_comps = map Free (cs ~~ comp_Ts) val dep_tycos = fold (add_used_tycos lthy) tycos [] val XTys = Bnf_Access.bnf_types lthy tycos val inst_types = typ_subst_atomic (XTys ~~ Ts) val cTys = map (map (map inst_types)) (Bnf_Access.constr_argument_types lthy tycos) val map_simps = Bnf_Access.map_simps lthy tycos val case_simps = Bnf_Access.case_simps lthy tycos val maps = Bnf_Access.map_terms lthy tycos val map_comp_thms = Bnf_Access.map_comps lthy tycos val t_ixs = 0 upto (length Ts - 1) val compNs = (*TODO: clashes in presence of same type names in different theories*) map (Long_Name.base_name) tycos |> map (fn s => "equality_" ^ s) fun gen_vars prefix = map (fn (i, pty) => Free (prefix ^ ints_to_subscript [i], pty)) (t_ixs ~~ Ts) (* primrec definitions of partial equalitys *) fun mk_pcomp (tyco, T) = ("partial_equality_" ^ Long_Name.base_name tyco, pcompT T) fun constr_terms lthy = Bnf_Access.constr_terms lthy #> map (apsnd (map freeify_tvars o fst o strip_type) o dest_Const) fun generate_pcomp_eqs lthy (tyco, T) = let val constrs = constr_terms lthy tyco fun comp_arg T x y = let val m = Generator_Aux.create_map default_comp (K o Free o mk_pcomp) () (K false) (#used_positions oo the_info) (#map oo the_info) (K o #pequality oo the_info) tycos ((K o K) ()) T lthy val p = Generator_Aux.create_partial () (K false) (#used_positions oo the_info) (#map oo the_info) (K o #pequality oo the_info) tycos ((K o K) ()) T lthy in p $ (m $ x) $ y |> infer_type lthy end fun generate_eq lthy (c_T as (cN, Ts)) = let val arg_Ts' = map orderify Ts val c = Const (cN, arg_Ts' ---> orderify T) val (y, (xs, ys)) = Name.variant "y" (Variable.names_of lthy) |>> Free o rpair T ||> (fn ctxt => Name.invent_names ctxt "x" (arg_Ts' @ Ts) |> map Free) ||> chop (length Ts) val k = find_index (curry (op =) c_T) constrs val cases = constrs |> map_index (fn (i, (_, Ts')) => if i < k then fold_rev absdummy Ts' @{term False} else if k < i then fold_rev absdummy Ts' @{term False} else @{term list_all_eq} $ HOLogic.mk_list boolT (@{map 3} comp_arg Ts xs ys) |> lambdas ys) val lhs = Free (mk_pcomp (tyco, T)) $ list_comb (c, xs) $ y val rhs = list_comb (singleton (Bnf_Access.case_consts lthy) tyco, cases) $ y in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |> infer_type lthy end in map (generate_eq lthy) constrs end val eqs = map (generate_pcomp_eqs lthy) (tycos ~~ Ts) |> flat val bindings = tycos ~~ Ts |> map mk_pcomp |> map (fn (name, T) => (Binding.name name, SOME T, NoSyn)) - val ((pcomps, pcomp_simps), lthy) = Local_Theory.subtarget_result - (fn phi => fn (pcomps, _, pcomp_simps) => (map (Morphism.term phi) pcomps, map (Morphism.fact phi) pcomp_simps)) - (BNF_LFP_Rec_Sugar.primrec false [] bindings - (map (fn t => ((Binding.empty_atts, t), [], [])) eqs)) lthy + val ((pcomps, pcomp_simps), lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> (BNF_LFP_Rec_Sugar.primrec false [] bindings + (map (fn t => ((Binding.empty_atts, t), [], [])) eqs)) + |> Local_Theory.end_nested_result + (fn phi => fn (pcomps, _, pcomp_simps) => (map (Morphism.term phi) pcomps, map (Morphism.fact phi) pcomp_simps)) (* definitions of equalitys via partial equalitys and maps *) fun generate_comp_def tyco lthy = let val cs = map (subT "eq") used_tfrees val arg_Ts = map compT used_tfrees val args = map Free (cs ~~ arg_Ts) val (pcomp, m) = AList.lookup (op =) (tycos ~~ (pcomps ~~ maps)) tyco |> the val ts = tfrees |> map TFree |> map (fn T => AList.lookup (op =) (used_tfrees ~~ args) T |> the_default (default_comp T)) val rhs = HOLogic.mk_comp (pcomp, list_comb (m, ts)) |> infer_type lthy val abs_def = lambdas args rhs val name = "equality_" ^ Long_Name.base_name tyco val ((comp, (_, prethm)), lthy) = Local_Theory.define ((Binding.name name, NoSyn), (Binding.empty_atts, abs_def)) lthy val eq = Logic.mk_equals (list_comb (comp, args), rhs) val thm = Goal.prove lthy (map (fst o dest_Free) args) [] eq (K (unfold_tac lthy [prethm])) in Local_Theory.note ((Binding.name (name ^ "_def"), []), [thm]) lthy |>> the_single o snd |>> `(K comp) end - val ((comps, comp_defs), lthy) = Local_Theory.subtarget_result - (fn phi => fn (comps, comp_defs) => (map (Morphism.term phi) comps, map (Morphism.thm phi) comp_defs)) - (fold_map generate_comp_def tycos #>> split_list) lthy + val ((comps, comp_defs), lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map generate_comp_def tycos + |>> split_list + |> Local_Theory.end_nested_result + (fn phi => fn (comps, comp_defs) => (map (Morphism.term phi) comps, map (Morphism.thm phi) comp_defs)) (* alternative simp-rules for equalitys *) val full_comps = map (list_comb o rpair arg_comps) comps fun generate_comp_simps (tyco, T) lthy = let val constrs = constr_terms lthy tyco fun comp_arg T x y = let fun create_comp (T as TFree _) = AList.lookup (op =) (used_tfrees ~~ arg_comps) T |> the_default (HOLogic.id_const dummyT) | create_comp (Type (tyco, Ts)) = (case AList.lookup (op =) (tycos ~~ comps) tyco of SOME c => list_comb (c, arg_comps) | NONE => let val {equality = c, used_positions = up, ...} = the_info lthy tyco val ts = (up ~~ Ts) |> map_filter (fn (b, T) => if b then SOME (create_comp T) else NONE) in list_comb (c, ts) end) | create_comp T = error ("unexpected schematic variable " ^ quote (Syntax.string_of_typ lthy T)) val comp = create_comp T in comp $ x $ y |> infer_type lthy end fun generate_eq_thm lthy (c_T as (_, Ts)) = let val (xs, ctxt) = Variable.names_of lthy |> fold_map (fn T => Name.variant "x" #>> Free o rpair T) Ts fun mk_const (c, Ts) = Const (c, Ts ---> T) val comp_const = AList.lookup (op =) (tycos ~~ comps) tyco |> the val lhs = list_comb (comp_const, arg_comps) $ list_comb (mk_const c_T, xs) val k = find_index (curry (op =) c_T) constrs fun mk_eq c ys rhs = let val y = list_comb (mk_const c, ys) val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs $ y, rhs)) in (ys, eq |> infer_type lthy) end val ((ys, eqs), _) = fold_map (fn (i, c as (_, Ts')) => fn ctxt => let val (ys, ctxt) = fold_map (fn T => Name.variant "y" #>> Free o rpair T) Ts' ctxt in (if i < k then mk_eq c ys @{term False} else if k < i then mk_eq c ys @{term False} else @{term list_all_eq} $ HOLogic.mk_list boolT (@{map 3} comp_arg Ts xs ys) |> mk_eq c ys, ctxt) end) (tag_list 0 constrs) ctxt |> apfst (apfst flat o split_list) val dep_comp_defs = map_filter (#equality_def o the_info lthy) dep_tycos val dep_map_comps = map_filter (#map_comp o the_info lthy) dep_tycos val thms = prove_multi_future lthy (map (fst o dest_Free) (xs @ ys) @ cs) [] eqs (fn {context = ctxt, ...} => Goal.conjunction_tac 1 THEN unfold_tac ctxt (@{thms id_apply o_def} @ flat case_simps @ flat pcomp_simps @ dep_map_comps @ comp_defs @ dep_comp_defs @ flat map_simps)) in thms end val thms = map (generate_eq_thm lthy) constrs |> flat val simp_thms = map (Local_Defs.unfold lthy @{thms list_all_eq_unfold}) thms val name = "equality_" ^ Long_Name.base_name tyco in lthy |> Local_Theory.note ((Binding.name (name ^ "_simps"), @{attributes [simp, code]}), simp_thms) |> snd |> (fn lthy => (thms, lthy)) end - val (comp_simps, lthy) = Local_Theory.subtarget_result - (fn phi => map (Morphism.fact phi)) - (fold_map generate_comp_simps (tycos ~~ Ts)) lthy + val (comp_simps, lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map generate_comp_simps (tycos ~~ Ts) + |> Local_Theory.end_nested_result (fn phi => map (Morphism.fact phi)) (* partial theorems *) val set_funs = Bnf_Access.set_terms lthy tycos val x_vars = gen_vars "x" val free_names = map (fst o dest_Free) (x_vars @ arg_comps) val xi_vars = map_index (fn (i, _) => map_index (fn (j, pty) => Free ("x" ^ ints_to_subscript [i, j], pty)) used_tfrees) Ts fun mk_eq_thm' mk_eq' = map_index (fn (i, ((set_funs, x), xis)) => let fun create_cond ((set_t, xi), c) = let val rhs = mk_eq' lthy c $ xi |> HOLogic.mk_Trueprop val lhs = HOLogic.mk_mem (xi, set_t $ x) |> HOLogic.mk_Trueprop in Logic.all xi (Logic.mk_implies (lhs, rhs)) end val used_sets = map (the o AList.lookup (op =) (map TFree tfrees ~~ set_funs)) used_tfrees val conds = map create_cond (used_sets ~~ xis ~~ arg_comps) val concl = mk_eq' lthy (nth full_comps i) $ x |> HOLogic.mk_Trueprop in Logic.list_implies (conds, concl) |> infer_type lthy end) (set_funs ~~ x_vars ~~ xi_vars) val induct_thms = Bnf_Access.induct_thms lthy tycos val set_simps = Bnf_Access.set_simps lthy tycos val case_thms = Bnf_Access.case_thms lthy tycos val distinct_thms = Bnf_Access.distinct_thms lthy tycos val inject_thms = Bnf_Access.inject_thms lthy tycos val rec_info = (the_info lthy, #used_positions, tycos) val split_IHs = split_IHs rec_info val unknown_value = false (* effect of choosing false / true not yet visible *) fun induct_tac ctxt f = ((DETERM o Induction.induction_tac ctxt false (map (fn x => [SOME (NONE, (x, unknown_value))]) x_vars) [] [] (SOME induct_thms) []) THEN_ALL_NEW (fn i => Subgoal.SUBPROOF (fn {context = ctxt, prems = prems, params = iparams, ...} => f (i - 1) ctxt prems iparams) ctxt i)) 1 val recursor_tac = std_recursor_tac rec_info used_tfrees (fn info => #partial_equality_thm info) fun instantiate_IHs IHs pre_conds = map (fn IH => OF_option IH (replicate (Thm.nprems_of IH - length pre_conds) NONE @ map SOME pre_conds)) IHs (* partial eq-theorem *) val _ = debug_out "Partial equality" val eq_thms' = mk_eq_thm' mk_pequality fun eq_solve_tac i ctxt IH_prems xs = let val (i, j) = ind_case_to_idxs cTys i val k = length IH_prems - length arg_comps val pre_conds = drop k IH_prems val IH = take k IH_prems val comp_simps = nth comp_simps i val case_thm = nth case_thms i val distinct_thms = nth distinct_thms i val inject_thms = nth inject_thms i val set_thms = nth set_simps i in (* after induction *) resolve_tac ctxt @{thms pequalityI} 1 THEN Subgoal.FOCUS (fn focus => let val y = #params focus |> hd val yt = y |> snd |> Thm.term_of val ctxt = #context focus val pre_cond = map (fn pre_cond => Local_Defs.unfold ctxt set_thms pre_cond) pre_conds val IH = instantiate_IHs IH pre_cond val xs_tys = map (fastype_of o Thm.term_of o snd) xs val IHs = split_IHs xs_tys IH fun sub_case_tac j' (ctxt, y_simp, _) = if j = j' then unfold_tac ctxt (y_simp @ comp_simps) THEN unfold_tac ctxt @{thms list_all_eq} THEN unfold_tac ctxt (@{thms in_set_simps} @ inject_thms @ @{thms refl_True}) THEN conjI_tac @{thms conj_weak_cong} ctxt xs (fn ctxt' => fn k => resolve_tac ctxt @{thms pequalityD} 1 THEN recursor_tac pre_cond (nth xs_tys k) (nth IHs k) ctxt') else (* different constructors *) unfold_tac ctxt (y_simp @ distinct_thms @ comp_simps @ @{thms bool.simps}) in mk_case_tac ctxt [[SOME yt]] case_thm sub_case_tac end ) ctxt 1 end val eq_thms' = prove_multi_future lthy free_names [] eq_thms' (fn {context = ctxt, ...} => induct_tac ctxt eq_solve_tac) val _ = debug_out (@{make_string} eq_thms') (* total theorems *) fun mk_eq_sym_trans_thm mk_eq_sym_trans compI2 compE2 thms' = let val conds = map (fn c => mk_eq_sym_trans lthy c |> HOLogic.mk_Trueprop) arg_comps val thms = map (fn i => mk_eq_sym_trans lthy (nth full_comps i) |> HOLogic.mk_Trueprop |> (fn concl => Logic.list_implies (conds,concl))) t_ixs val thms = prove_multi_future lthy free_names [] thms (fn {context = ctxt, ...} => ALLGOALS Goal.conjunction_tac THEN Method.intros_tac ctxt (@{thm conjI} :: compI2 :: thms') [] THEN ALLGOALS (eresolve_tac ctxt [compE2])) in thms end val eq_thms = mk_eq_sym_trans_thm mk_equality @{thm equalityI2} @{thm equalityD2} eq_thms' val _ = debug_out "full equality thms" fun mk_comp_thm (i, e) = let val conds = map (fn c => mk_equality lthy c |> HOLogic.mk_Trueprop) arg_comps val nearly_thm = e val thm = mk_equality lthy (nth full_comps i) |> HOLogic.mk_Trueprop |> (fn concl => Logic.list_implies (conds, concl)) in Goal.prove_future lthy free_names [] thm (K (resolve_tac lthy [nearly_thm] 1 THEN ALLGOALS (assume_tac lthy))) end val comp_thms = map_index mk_comp_thm eq_thms val (_, lthy) = fold_map (fn (thm, cname) => Local_Theory.note ((Binding.name cname, []), [thm])) (comp_thms ~~ compNs) lthy val _ = debug_out (@{make_string} comp_thms) val (_, lthy) = fold_map (fn (thm, cname) => Local_Theory.note ((Binding.name (cname ^ "_pointwise"), []), [thm])) (eq_thms' ~~ compNs) lthy in ((pcomps ~~ pcomp_simps, comps ~~ comp_defs), lthy) ||> fold (fn (((((((tyco, map), pcomp), comp), comp_def), map_comp) , peq_thm), comp_thm) => declare_info tyco map pcomp comp (SOME comp_def) (SOME map_comp) peq_thm comp_thm used_positions) (tycos ~~ maps ~~ pcomps ~~ comps ~~ comp_defs ~~ map_comp_thms ~~ eq_thms' ~~ comp_thms) end fun generate_equality gen_type tyco lthy = let val _ = is_some (get_info lthy tyco) andalso error ("type " ^ quote tyco ^ " does already have a equality") in case gen_type of BNF => generate_equalitys_from_bnf_fp tyco lthy |> snd | EQ => register_equality_of tyco lthy end fun ensure_info gen_type tyco lthy = (case get_info lthy tyco of SOME _ => lthy | NONE => generate_equality gen_type tyco lthy) fun generate_equality_cmd tyco param = Named_Target.theory_map ( if param = "eq" then generate_equality EQ tyco else if param = "" then generate_equality BNF tyco else error ("unknown parameter, expecting no parameter for BNF-datatypes, " ^ "or \"eq\" for types where the built-in equality \"=\" should be used.")) val _ = Theory.setup (Derive_Manager.register_derive "equality" "generate an equality function, options are () and (eq)" generate_equality_cmd) end diff --git a/thys/Deriving/Hash_Generator/hash_generator.ML b/thys/Deriving/Hash_Generator/hash_generator.ML --- a/thys/Deriving/Hash_Generator/hash_generator.ML +++ b/thys/Deriving/Hash_Generator/hash_generator.ML @@ -1,396 +1,411 @@ (* Title: Deriving class instances for datatypes Author: Christian Sternagel and René Thiemann Maintainer: Christian Sternagel and René Thiemann License: LGPL *) signature HASHCODE_GENERATOR = sig type info = {map : term, (* take % x. x, if there is no map *) phash : term, (* partial hash *) hash : term, (* full hash *) hash_def : thm option, (* definition of hash, important for nesting *) map_comp : thm option, (* hashositionality of map, important for nesting *) used_positions : bool list} (* registers some type which is already instance of hashcode class in hash generator where some type must just be a type without type-arguments *) val register_hash_of : string -> local_theory -> local_theory val register_foreign_hash : typ -> (* type-constant without type-variables *) term -> (* hash-function for type *) local_theory -> local_theory val register_foreign_partial_and_full_hash : string -> (* long type name *) term -> (* map function, should be \x. x, if there is no map *) term -> (* partial hash-function of type (hashcode, 'b)ty => hashcode, where 'a is used, 'b is unused *) term -> (* (full) hash-function of type ('a \ hashcode) \ ('a,'b)ty \ hashcode, where 'a is used, 'b is unused *) thm option -> (* hash_def, should be full_hash = phash o map ahash ..., important for nesting *) thm option -> (* map compositionality, important for nesting *) bool list -> (*used positions*) local_theory -> local_theory datatype hash_type = HASHCODE | BNF val generate_hashs_from_bnf_fp : string -> (* name of type *) local_theory -> ((term * thm list) list * (* partial hashs + simp-rules *) (term * thm) list) * (* non-partial hash + def_rule *) local_theory val generate_hash : hash_type -> string -> (* name of type *) local_theory -> local_theory (* construct hashcode instance for datatype *) val hashable_instance : string -> theory -> theory val get_info : Proof.context -> string -> info option (* ensures that the info will be available on later requests *) val ensure_info : hash_type -> string -> local_theory -> local_theory end structure Hashcode_Generator : HASHCODE_GENERATOR = struct open Generator_Aux datatype hash_type = BNF | HASHCODE val hash_name = @{const_name "hashcode"} val hashS = @{sort hashable} val hashT = @{typ hashcode} fun hashfunT T = T --> hashT val hashify = map_atyps (fn _ => hashT) fun phashfunT T = hashify T --> hashT val max_int = 2147483648 (* 2 ^^ 31 *) fun int_of_string s = fold (fn c => fn i => (1792318057 * i + Char.ord c) mod max_int) (String.explode s) 0 (* all numbers in int_of_string and create_factors are primes (31-bit) *) fun create_factor ty_name con_name i = (1444315237 * int_of_string ty_name + 1336760419 * int_of_string con_name + 2044890737 * (i + 1) ) mod max_int fun create_hashes ty_name con_name Ts = map (fn i => HOLogic.mk_number hashT (create_factor ty_name con_name i)) (0 upto length Ts) |> HOLogic.mk_list hashT fun create_def_size _ = 10 type info = {map : term, phash : term, hash : term, hash_def : thm option, map_comp : thm option, used_positions : bool list}; structure Data = Generic_Data ( type T = info Symtab.table; val empty = Symtab.empty; val extend = I; val merge = Symtab.merge (fn (info1 : info, info2 : info) => #hash info1 = #hash info2); ); fun add_info T info = Data.map (Symtab.update_new (T, info)) val get_info = Context.Proof #> Data.get #> Symtab.lookup fun the_info ctxt tyco = (case get_info ctxt tyco of SOME info => info | NONE => error ("no hash_code information available for type " ^ quote tyco)) fun declare_info tyco m p c c_def m_hash used_pos = Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => add_info tyco {map = Morphism.term phi m, phash = Morphism.term phi p, hash = Morphism.term phi c, hash_def = Option.map (Morphism.thm phi) c_def, map_comp = Option.map (Morphism.thm phi) m_hash, used_positions = used_pos}) fun register_foreign_partial_and_full_hash tyco m p c c_def m_hash eq_thm c_thm = declare_info tyco m p c c_def m_hash eq_thm c_thm fun default_hash T = absdummy T @{term "0 :: hashcode"} (*%_. 0*) fun register_foreign_hash T hash lthy = let val tyco = (case T of Type (tyco, []) => tyco | _ => error "expected type constant with no arguments") in register_foreign_partial_and_full_hash tyco (HOLogic.id_const T) hash hash NONE NONE [] lthy end fun register_hash_of tyco lthy = let val _ = is_class_instance (Proof_Context.theory_of lthy) tyco hashS orelse error ("type " ^ quote tyco ^ " is not an instance of class \"hashable\"") val (T,_) = typ_and_vs_of_typname (Proof_Context.theory_of lthy) tyco @{sort type} val hash = Const (hash_name, hashfunT T) in register_foreign_hash T hash lthy end fun generate_hashs_from_bnf_fp tyco lthy = let val (tycos, Ts) = mutual_recursive_types tyco lthy val _ = map (fn tyco => "generating hash-function for type " ^ quote tyco) tycos |> cat_lines |> writeln val (tfrees, used_tfrees) = type_parameters (hd Ts) lthy val used_positions = map (member (op =) used_tfrees o TFree) tfrees val cs = map (subT "h") used_tfrees val hash_Ts = map hashfunT used_tfrees val arg_hashs = map Free (cs ~~ hash_Ts) val dep_tycos = fold (add_used_tycos lthy) tycos [] val map_simps = Bnf_Access.map_simps lthy tycos val case_simps = Bnf_Access.case_simps lthy tycos val maps = Bnf_Access.map_terms lthy tycos val map_comp_thms = Bnf_Access.map_comps lthy tycos (* primrec definitions of partial hashs *) fun mk_phash (tyco, T) = ("partial_hash_code_" ^ Long_Name.base_name tyco, phashfunT T) fun constr_terms lthy = Bnf_Access.constr_terms lthy #> map (apsnd (map freeify_tvars o fst o strip_type) o dest_Const) fun generate_phash_eqs lthy (tyco, T) = let val constrs = constr_terms lthy tyco fun hash_arg T x = let val m = Generator_Aux.create_map default_hash (K o Free o mk_phash) () (K false) (#used_positions oo the_info) (#map oo the_info) (K o #phash oo the_info) tycos ((K o K) ()) T lthy val p = Generator_Aux.create_partial () (K false) (#used_positions oo the_info) (#map oo the_info) (K o #phash oo the_info) tycos ((K o K) ()) T lthy in p $ (m $ x) |> infer_type lthy end fun generate_eq lthy (cN, Ts) = let val arg_Ts' = map hashify Ts val c = Const (cN, arg_Ts' ---> hashify T) val xs = Name.invent_names (Variable.names_of lthy) "x" (arg_Ts') |> map Free val lhs = Free (mk_phash (tyco, T)) $ list_comb (c, xs) val rhs = @{term hash_combine} $ HOLogic.mk_list hashT (@{map 2} hash_arg Ts xs) $ create_hashes tyco cN Ts in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |> infer_type lthy end in map (generate_eq lthy) constrs end val eqs = map (generate_phash_eqs lthy) (tycos ~~ Ts) |> flat val bindings = tycos ~~ Ts |> map mk_phash |> map (fn (name, T) => (Binding.name name, SOME T, NoSyn)) - val ((phashs, phash_simps), lthy) = Local_Theory.subtarget_result - (fn phi => fn (phashs, _, phash_simps) => (map (Morphism.term phi) phashs, map (Morphism.fact phi) phash_simps)) - (BNF_LFP_Rec_Sugar.primrec false [] bindings - (map (fn t => ((Binding.empty_atts, t), [], [])) eqs)) lthy + val ((phashs, phash_simps), lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> BNF_LFP_Rec_Sugar.primrec false [] bindings + (map (fn t => ((Binding.empty_atts, t), [], [])) eqs) + |> Local_Theory.end_nested_result + (fn phi => fn (phashs, _, phash_simps) => (map (Morphism.term phi) phashs, map (Morphism.fact phi) phash_simps)) (* definitions of hashs via partial hashs and maps *) fun generate_hash_def tyco lthy = let val cs = map (subT "h") used_tfrees val arg_Ts = map hashfunT used_tfrees val args = map Free (cs ~~ arg_Ts) val (phash, m) = AList.lookup (op =) (tycos ~~ (phashs ~~ maps)) tyco |> the val ts = tfrees |> map TFree |> map (fn T => AList.lookup (op =) (used_tfrees ~~ args) T |> the_default (default_hash T)) val rhs = HOLogic.mk_comp (phash, list_comb (m, ts)) |> infer_type lthy val abs_def = lambdas args rhs val name = "hash_code_" ^ Long_Name.base_name tyco val ((hash, (_, prethm)), lthy) = Local_Theory.define ((Binding.name name, NoSyn), (Binding.empty_atts, abs_def)) lthy val eq = Logic.mk_equals (list_comb (hash, args), rhs) val thm = Goal.prove lthy (map (fst o dest_Free) args) [] eq (K (unfold_tac lthy [prethm])) in Local_Theory.note ((Binding.name (name ^ "_def"), []), [thm]) lthy |>> the_single o snd |>> `(K hash) end - val ((hashs, hash_defs), lthy) = Local_Theory.subtarget_result - (fn phi => fn (hashs, hash_defs) => (map (Morphism.term phi) hashs, map (Morphism.thm phi) hash_defs)) - (fold_map generate_hash_def tycos #>> split_list) lthy + val ((hashs, hash_defs), lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map generate_hash_def tycos + |>> split_list + |> Local_Theory.end_nested_result + (fn phi => fn (hashs, hash_defs) => (map (Morphism.term phi) hashs, map (Morphism.thm phi) hash_defs)) (* alternative simp-rules for hashs *) fun generate_hash_simps (tyco, T) lthy = let val constrs = constr_terms lthy tyco fun hash_arg T x = let fun create_hash (T as TFree _) = AList.lookup (op =) (used_tfrees ~~ arg_hashs) T |> the_default (HOLogic.id_const dummyT) | create_hash (Type (tyco, Ts)) = (case AList.lookup (op =) (tycos ~~ hashs) tyco of SOME c => list_comb (c, arg_hashs) | NONE => let val {hash = c, used_positions = up, ...} = the_info lthy tyco val ts = (up ~~ Ts) |> map_filter (fn (b, T) => if b then SOME (create_hash T) else NONE) in list_comb (c, ts) end) | create_hash T = error ("unexpected schematic variable " ^ quote (Syntax.string_of_typ lthy T)) val hash = create_hash T in hash $ x |> infer_type lthy end fun generate_eq_thm lthy (c_T as (cN, Ts)) = let val xs = Variable.names_of lthy |> fold_map (fn T => Name.variant "x" #>> Free o rpair T) Ts |> fst fun mk_const (c, Ts) = Const (c, Ts ---> T) val hash_const = AList.lookup (op =) (tycos ~~ hashs) tyco |> the val lhs = list_comb (hash_const, arg_hashs) $ list_comb (mk_const c_T, xs) val rhs = @{term hash_combine} $ HOLogic.mk_list hashT (@{map 2} hash_arg Ts xs) $ create_hashes tyco cN Ts val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |> infer_type lthy val dep_hash_defs = map_filter (#hash_def o the_info lthy) dep_tycos val dep_map_comps = map_filter (#map_comp o the_info lthy) dep_tycos val thms = prove_multi_future lthy (map (fst o dest_Free) xs @ cs) [] [eq] (fn {context = ctxt, ...} => Goal.conjunction_tac 1 THEN unfold_tac ctxt (@{thms id_apply o_def} @ flat case_simps @ flat phash_simps @ dep_map_comps @ hash_defs @ dep_hash_defs @ flat map_simps)) in thms end val thms = map (generate_eq_thm lthy) constrs |> flat val simp_thms = map (Local_Defs.unfold lthy @{thms hash_combine_unfold}) thms val name = "hash_code_" ^ Long_Name.base_name tyco in lthy |> Local_Theory.note ((Binding.name (name ^ "_simps"), @{attributes [simp, code]}), simp_thms) |> snd |> (fn lthy => (thms, lthy)) end - val lthy = Local_Theory.subtarget (fold_map generate_hash_simps (tycos ~~ Ts) #> snd) lthy + val lthy = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map generate_hash_simps (tycos ~~ Ts) + |> snd + |> Local_Theory.end_nested in ((phashs ~~ phash_simps, hashs ~~ hash_defs), lthy) ||> fold (fn (((((tyco, map), phash), hash), hash_def), map_comp) => declare_info tyco map phash hash (SOME hash_def) (SOME map_comp) used_positions) (tycos ~~ maps ~~ phashs ~~ hashs ~~ hash_defs ~~ map_comp_thms) end fun generate_hash gen_type tyco lthy = let val _ = is_some (get_info lthy tyco) andalso error ("type " ^ quote tyco ^ " does already have a hash") in case gen_type of BNF => generate_hashs_from_bnf_fp tyco lthy |> snd | HASHCODE => register_hash_of tyco lthy end fun ensure_info gen_type tyco lthy = (case get_info lthy tyco of SOME _ => lthy | NONE => generate_hash gen_type tyco lthy) fun dest_hash ctxt tname = (case get_info ctxt tname of SOME {hash = c, ...} => let val Ts = fastype_of c |> strip_type |> fst |> `((fn x => x - 1) o length) |> uncurry take in (c, Ts) end | NONE => error ("no hash info for type " ^ quote tname)) fun all_tys hash free_types = let val Ts = fastype_of hash |> strip_type |> fst |> List.last |> dest_Type |> snd in rename_types (Ts ~~ free_types) end fun mk_hash_rhs c Ts = list_comb (c, map (fn T => Const (hash_name, T)) Ts) fun mk_hash_def T rhs = Logic.mk_equals (Const (hash_name, hashfunT T), rhs) fun hashable_instance tname thy = let val _ = is_class_instance thy tname hashS andalso error ("type " ^ quote tname ^ " is already an instance of class \"hashcode\"") val _ = writeln ("deriving \"hashable\" instance for type " ^ quote tname) val thy = Named_Target.theory_map (ensure_info BNF tname) thy val {used_positions = us, ...} = the (get_info (Named_Target.theory_init thy) tname) val (_, xs) = typ_and_vs_of_used_typname tname us hashS val (_, (hashs_thm,lthy)) = Class.instantiation ([tname], xs, hashS) thy |> (fn ctxt => let val (c, Ts) = dest_hash ctxt tname val typ_mapping = all_tys c (map TFree xs) val hash_rhs = mk_hash_rhs c Ts val hash_def = mk_hash_def dummyT hash_rhs |> typ_mapping |> infer_type ctxt val ty = Term.fastype_of (snd (Logic.dest_equals hash_def)) |> Term.dest_Type |> snd |> hd val ty_it = Type (@{type_name itself}, [ty]) val hashs_rhs = lambda (Free ("x",ty_it)) (HOLogic.mk_number @{typ nat} (create_def_size tname)) val hashs_def = mk_def (ty_it --> @{typ nat}) @{const_name def_hashmap_size} hashs_rhs val basename = Long_Name.base_name tname in Generator_Aux.define_overloaded_generic ((Binding.name ("hashcode_" ^ basename ^ "_def"), @{attributes [code]}), hash_def) ctxt ||> define_overloaded ("def_hashmap_size_" ^ basename ^ "_def", hashs_def) end) in Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [] THEN unfold_tac ctxt [hashs_thm] THEN simp_tac ctxt 1 ) lthy end fun generate_hash_cmd tyco param = Named_Target.theory_map ( if param = "hashcode" then generate_hash HASHCODE tyco else if param = "" then generate_hash BNF tyco else error ("unknown parameter, expecting no parameter for BNF-datatypes, " ^ "or \"hashcode\" for types where the class-instance hashcode should be used.")) val _ = Theory.setup (Derive_Manager.register_derive "hash_code" "generate a hash function, options are () and (hashcode)" generate_hash_cmd #> Derive_Manager.register_derive "hashable" "register types in class hashable" (fn tyname => K (hashable_instance tyname))) end diff --git a/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy b/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy --- a/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy +++ b/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy @@ -1,1717 +1,1716 @@ (****************************************************************************** * Citadelle * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section\Dynamic Meta Embedding with Reflection\ theory Generator_dynamic_sequential imports Printer "../../isabelle_home/src/HOL/Isabelle_Main2" (*<*) keywords (* Toy language *) "Between" "Attributes" "Operations" "Constraints" "Role" "Ordered" "Subsets" "Union" "Redefines" "Derived" "Qualifier" "Existential" "Inv" "Pre" "Post" "self" "Nonunique" "Sequence_" (* Isabelle syntax *) "output_directory" "THEORY" "IMPORTS" "SECTION" "SORRY" "no_dirty" "deep" "shallow" "syntax_print" "skip_export" "generation_semantics" "flush_all" (* Isabelle semantics (parameterizing the semantics of Toy language) *) "design" "analysis" "oid_start" and (* Toy language *) "Enum" "Abstract_class" "Class" "Association" "Composition" "Aggregation" "Abstract_associationclass" "Associationclass" "Context" "End" "Instance" "BaseType" "State" "PrePost" (* Isabelle syntax *) "generation_syntax" :: thy_decl (*>*) begin text\In the ``dynamic'' solution: the exportation is automatically handled inside Isabelle/jEdit. Inputs are provided using the syntax of the Toy Language, and in output we basically have two options: \begin{itemize} \item The first is to generate an Isabelle file for inspection or debugging. The generated file can interactively be loaded in Isabelle/jEdit, or saved to the hard disk. This mode is called the ``deep exportation'' mode or shortly the ``deep'' mode. The aim is to maximally automate the process one is manually performing in @{file \Generator_static.thy\}. \item On the other hand, it is also possible to directly execute in Isabelle/jEdit the generated file from the random access memory. This mode corresponds to the ``shallow reflection'' mode or shortly ``shallow'' mode. \end{itemize} In both modes, the reflection is necessary since the main part used by both was defined at Isabelle side. As a consequence, experimentations in ``deep'' and ``shallow'' are performed without leaving the editing session, in the same as the one the meta-compiler is actually running.\ apply_code_printing_reflect \ val stdout_file = Unsynchronized.ref "" \ text\This variable is not used in this theory (only in @{file \Generator_static.thy\}), but needed for well typechecking the reflected SML code.\ code_reflect' open META functions (* executing the compiler as monadic combinators for deep and shallow *) fold_thy_deep fold_thy_shallow (* printing the HOL AST to (shallow Isabelle) string *) write_file (* manipulating the compiling environment *) compiler_env_config_reset_all compiler_env_config_update oidInit D_output_header_thy_update map2_ctxt_term check_export_code (* printing the TOY AST to (deep Isabelle) string *) isabelle_apply isabelle_of_compiler_env_config subsection\Interface Between the Reflected and the Native\ ML\ val To_string0 = META.meta_of_logic \ ML\ structure From = struct val string = META.SS_base o META.ST val binding = string o Binding.name_of (*fun term ctxt s = string (XML.content_of (YXML.parse_body (Syntax.string_of_term ctxt s)))*) val internal_oid = META.Oid o Code_Numeral.natural_of_integer val option = Option.map val list = List.map fun pair f1 f2 (x, y) = (f1 x, f2 y) fun pair3 f1 f2 f3 (x, y, z) = (f1 x, f2 y, f3 z) structure Pure = struct val indexname = pair string Code_Numeral.natural_of_integer val class = string val sort = list class fun typ e = (fn Type (s, l) => (META.Type o pair string (list typ)) (s, l) | TFree (s, s0) => (META.TFree o pair string sort) (s, s0) | TVar (i, s0) => (META.TVar o pair indexname sort) (i, s0) ) e fun term e = (fn Const (s, t) => (META.Const o pair string typ) (s, t) | Free (s, t) => (META.Free o pair string typ) (s, t) | Var (i, t) => (META.Var o pair indexname typ) (i, t) | Bound i => (META.Bound o Code_Numeral.natural_of_integer) i | Abs (s, ty, t) => (META.Abs o pair3 string typ term) (s, ty, t) | op $ (term1, term2) => (META.App o pair term term) (term1, term2) ) e end fun toy_ctxt_term thy expr = META.T_pure (Pure.term (Syntax.read_term (Proof_Context.init_global thy) expr)) end \ ML\fun List_mapi f = META.mapi (f o Code_Numeral.integer_of_natural)\ ML\ structure Ty' = struct fun check l_oid l = let val Mp = META.map_prod val Me = String.explode val Mi = String.implode val Ml = map in META.check_export_code (writeln o Mi) (warning o Mi) (fn s => writeln (Markup.markup (Markup.bad ()) (Mi s))) (error o To_string0) (Ml (Mp I Me) l_oid) ((META.SS_base o META.ST) l) end end \ subsection\Binding of the Reflected API to the Native API\ ML\ structure META_overload = struct val of_semi__typ = META.of_semi_typ To_string0 val of_semi__term = META.of_semi_terma To_string0 val of_semi__term' = META.of_semi_term To_string0 val fold = fold end \ ML\ structure Bind_Isabelle = struct fun To_binding s = Binding.make (s, Position.none) val To_sbinding = To_binding o To_string0 fun semi__method_simp g f = Method.Basic (fn ctxt => SIMPLE_METHOD (g (asm_full_simp_tac (f ctxt)))) val semi__method_simp_one = semi__method_simp (fn f => f 1) val semi__method_simp_all = semi__method_simp (CHANGED_PROP o PARALLEL_ALLGOALS) datatype semi__thm' = Thms_single' of thm | Thms_mult' of thm list fun semi__thm_attribute ctxt = let open META open META_overload val S = fn Thms_single' t => t val M = fn Thms_mult' t => t in fn Thm_thm s => Thms_single' (Proof_Context.get_thm ctxt (To_string0 s)) | Thm_thms s => Thms_mult' (Proof_Context.get_thms ctxt (To_string0 s)) | Thm_THEN (e1, e2) => (case (semi__thm_attribute ctxt e1, semi__thm_attribute ctxt e2) of (Thms_single' e1, Thms_single' e2) => Thms_single' (e1 RSN (1, e2)) | (Thms_mult' e1, Thms_mult' e2) => Thms_mult' (e1 RLN (1, e2))) | Thm_simplified (e1, e2) => Thms_single' (asm_full_simplify (clear_simpset ctxt addsimps [S (semi__thm_attribute ctxt e2)]) (S (semi__thm_attribute ctxt e1))) | Thm_OF (e1, e2) => Thms_single' ([S (semi__thm_attribute ctxt e2)] MRS (S (semi__thm_attribute ctxt e1))) | Thm_where (nth, l) => Thms_single' (Rule_Insts.where_rule ctxt (List.map (fn (var, expr) => (((To_string0 var, 0), Position.none), of_semi__term expr)) l) [] (S (semi__thm_attribute ctxt nth))) | Thm_symmetric e1 => let val e2 = S (semi__thm_attribute ctxt (Thm_thm (From.string "sym"))) in case semi__thm_attribute ctxt e1 of Thms_single' e1 => Thms_single' (e1 RSN (1, e2)) | Thms_mult' e1 => Thms_mult' (e1 RLN (1, [e2])) end | Thm_of (nth, l) => Thms_single' (Rule_Insts.of_rule ctxt (List.map (SOME o of_semi__term) l, []) [] (S (semi__thm_attribute ctxt nth))) end fun semi__thm_attribute_single ctxt s = case (semi__thm_attribute ctxt s) of Thms_single' t => t fun semi__thm_mult ctxt = let fun f thy = case (semi__thm_attribute ctxt thy) of Thms_mult' t => t | Thms_single' t => [t] in fn META.Thms_single thy => f thy | META.Thms_mult thy => f thy end fun semi__thm_mult_l ctxt l = List.concat (map (semi__thm_mult ctxt) l) fun semi__method_simp_only l ctxt = clear_simpset ctxt addsimps (semi__thm_mult_l ctxt l) fun semi__method_simp_add_del_split (l_add, l_del, l_split) ctxt = fold Splitter.add_split (semi__thm_mult_l ctxt l_split) (ctxt addsimps (semi__thm_mult_l ctxt l_add) delsimps (semi__thm_mult_l ctxt l_del)) fun semi__method expr = let open META open Method open META_overload in case expr of Method_rule o_s => Basic (fn ctxt => METHOD (HEADGOAL o Classical.rule_tac ctxt (case o_s of NONE => [] | SOME s => [semi__thm_attribute_single ctxt s]))) | Method_drule s => Basic (fn ctxt => drule ctxt 0 [semi__thm_attribute_single ctxt s]) | Method_erule s => Basic (fn ctxt => erule ctxt 0 [semi__thm_attribute_single ctxt s]) | Method_elim s => Basic (fn ctxt => elim ctxt [semi__thm_attribute_single ctxt s]) | Method_intro l => Basic (fn ctxt => intro ctxt (map (semi__thm_attribute_single ctxt) l)) | Method_subst (asm, l, s) => Basic (fn ctxt => SIMPLE_METHOD' ((if asm then EqSubst.eqsubst_asm_tac else EqSubst.eqsubst_tac) ctxt (map (fn s => case Int.fromString (To_string0 s) of SOME i => i) l) [semi__thm_attribute_single ctxt s])) | Method_insert l => Basic (fn ctxt => insert (semi__thm_mult_l ctxt l)) | Method_plus t => Combinator ( no_combinator_info , Repeat1 , [Combinator (no_combinator_info, Then, List.map semi__method t)]) | Method_option t => Combinator ( no_combinator_info , Try , [Combinator (no_combinator_info, Then, List.map semi__method t)]) | Method_or t => Combinator (no_combinator_info, Orelse, List.map semi__method t) | Method_one (Method_simp_only l) => semi__method_simp_one (semi__method_simp_only l) | Method_one (Method_simp_add_del_split l) => semi__method_simp_one (semi__method_simp_add_del_split l) | Method_all (Method_simp_only l) => semi__method_simp_all (semi__method_simp_only l) | Method_all (Method_simp_add_del_split l) => semi__method_simp_all (semi__method_simp_add_del_split l) | Method_auto_simp_add_split (l_simp, l_split) => Basic (fn ctxt => SIMPLE_METHOD (auto_tac (fold (fn (f, l) => fold f l) [(Simplifier.add_simp, semi__thm_mult_l ctxt l_simp) ,(Splitter.add_split, List.map (Proof_Context.get_thm ctxt o To_string0) l_split)] ctxt))) | Method_rename_tac l => Basic (K (SIMPLE_METHOD' (Tactic.rename_tac (List.map To_string0 l)))) | Method_case_tac e => Basic (fn ctxt => SIMPLE_METHOD' (Induct_Tacs.case_tac ctxt (of_semi__term e) [] NONE)) | Method_blast n => Basic (case n of NONE => SIMPLE_METHOD' o blast_tac | SOME lim => fn ctxt => SIMPLE_METHOD' (depth_tac ctxt (Code_Numeral.integer_of_natural lim))) | Method_clarify => Basic (fn ctxt => (SIMPLE_METHOD' (fn i => CHANGED_PROP (clarify_tac ctxt i)))) | Method_metis (l_opt, l) => Basic (fn ctxt => (METHOD oo Metis_Tactic.metis_method) ( (if l_opt = [] then NONE else SOME (map To_string0 l_opt), NONE) , map (semi__thm_attribute_single ctxt) l) ctxt) end fun then_tactic l = let open Method in (Combinator (no_combinator_info, Then, map semi__method l), (Position.none, Position.none)) end fun local_terminal_proof o_by = let open META in case o_by of Command_done => Proof.local_done_proof | Command_sorry => Proof.local_skip_proof true | Command_by l_apply => Proof.local_terminal_proof (then_tactic l_apply, NONE) end fun global_terminal_proof o_by = let open META in case o_by of Command_done => Proof.global_done_proof | Command_sorry => Proof.global_skip_proof true | Command_by l_apply => Proof.global_terminal_proof (then_tactic l_apply, NONE) end fun proof_show_gen f (thes, thes_when) st = st |> Proof.proof (SOME ( Method.Source [Token.make_string ("-", Position.none)] , (Position.none, Position.none))) |> Seq.the_result "" |> f |> Proof.show_cmd (thes_when = []) NONE (K I) [] (if thes_when = [] then [] else [(Binding.empty_atts, map (fn t => (t, [])) thes_when)]) [(Binding.empty_atts, [(thes, [])])] true |> snd val semi__command_state = let open META_overload in fn META.Command_apply_end l => (fn st => st |> Proof.apply_end (then_tactic l) |> Seq.the_result "") end val semi__command_proof = let open META_overload val thesis = "?thesis" fun proof_show f = proof_show_gen f (thesis, []) in fn META.Command_apply l => (fn st => st |> Proof.apply (then_tactic l) |> Seq.the_result "") | META.Command_using l => (fn st => let val ctxt = Proof.context_of st in Proof.using [map (fn s => ([ s], [])) (semi__thm_mult_l ctxt l)] st end) | META.Command_unfolding l => (fn st => let val ctxt = Proof.context_of st in Proof.unfolding [map (fn s => ([s], [])) (semi__thm_mult_l ctxt l)] st end) | META.Command_let (e1, e2) => proof_show (Proof.let_bind_cmd [([of_semi__term e1], of_semi__term e2)]) | META.Command_have (n, b, e, e_pr) => proof_show (fn st => st |> Proof.have_cmd true NONE (K I) [] [] [( (To_sbinding n, if b then [[Token.make_string ("simp", Position.none)]] else []) , [(of_semi__term e, [])])] true |> snd |> local_terminal_proof e_pr) | META.Command_fix_let (l, l_let, o_exp, _) => proof_show_gen ( fold (fn (e1, e2) => Proof.let_bind_cmd [([of_semi__term e1], of_semi__term e2)]) l_let o Proof.fix_cmd (List.map (fn i => (To_sbinding i, NONE, NoSyn)) l)) ( case o_exp of NONE => thesis | SOME (l_spec, _) => (String.concatWith (" \ ") (List.map of_semi__term l_spec)) , case o_exp of NONE => [] | SOME (_, l_when) => List.map of_semi__term l_when) end fun semi__theory in_theory in_local = let open META open META_overload in (*let val f = *)fn Theory_datatype (Datatype (n, l)) => in_local (BNF_FP_Def_Sugar.co_datatype_cmd BNF_Util.Least_FP BNF_LFP.construct_lfp (Ctr_Sugar.default_ctr_options_cmd, [( ( ( (([], To_sbinding n), NoSyn) , List.map (fn (n, l) => ( ( (To_binding "", To_sbinding n) , List.map (fn s => (To_binding "", of_semi__typ s)) l) , NoSyn)) l) , (To_binding "", To_binding "", To_binding "")) , [])])) | Theory_type_synonym (Type_synonym (n, v, l)) => in_theory (fn thy => let val s_bind = To_sbinding n in (snd o Typedecl.abbrev_global (s_bind, map To_string0 v, NoSyn) (Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end) | Theory_type_notation (Type_notation (n, e)) => in_local (Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))]) | Theory_instantiation (Instantiation (n, n_def, expr)) => in_theory (fn thy => let val name = To_string0 n val tycos = [ let val Term.Type (s, _) = (Isabelle_Typedecl.abbrev_cmd0 NONE thy name) in s end ] in thy |> Class.instantiation (tycos, [], Syntax.read_sort (Proof_Context.init_global thy) "object") |> fold_map (fn _ => fn thy => let val ((_, (_, ty)), thy) = Specification.definition_cmd NONE [] [] ((To_binding (To_string0 n_def ^ "_" ^ name ^ "_def"), []) , of_semi__term expr) false thy in (ty, thy) end) tycos |-> Class.prove_instantiation_exit_result (map o Morphism.thm) (fn ctxt => fn thms => Class.intro_classes_tac ctxt [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms)) |-> K I end) | Theory_overloading (Overloading (n_c, e_c, n, e)) => in_theory (fn thy => thy |> Overloading.overloading_cmd [(To_string0 n_c, of_semi__term e_c, true)] |> snd o Specification.definition_cmd NONE [] [] ((To_sbinding n, []), of_semi__term e) false |> Local_Theory.exit_global) | Theory_consts (Consts (n, ty, symb)) => in_theory (Sign.add_consts_cmd [( To_sbinding n , of_semi__typ ty , Mixfix (Input.string ("(_) " ^ To_string0 symb), [], 1000, Position.no_range))]) | Theory_definition def => in_local let val (def, e) = case def of Definition e => (NONE, e) | Definition_where1 (name, (abbrev, prio), e) => (SOME ( To_sbinding name , NONE , Mixfix (Input.string ("(1" ^ of_semi__term abbrev ^ ")"), [], Code_Numeral.integer_of_natural prio, Position.no_range)), e) | Definition_where2 (name, abbrev, e) => (SOME ( To_sbinding name , NONE , Mixfix (Input.string ("(" ^ of_semi__term abbrev ^ ")"), [], 1000, Position.no_range)), e) in (snd o Specification.definition_cmd def [] [] (Binding.empty_atts, of_semi__term e) false) end | Theory_lemmas (Lemmas_simp_thm (simp, s, l)) => in_local (fn lthy => (snd o Specification.theorems Thm.theoremK [((To_sbinding s, List.map (fn s => Attrib.check_src lthy [Token.make_string (s, Position.none)]) (if simp then ["simp", "code_unfold"] else [])), List.map (fn x => ([semi__thm_attribute_single lthy x], [])) l)] [] false) lthy) | Theory_lemmas (Lemmas_simp_thms (s, l)) => in_local (fn lthy => (snd o Specification.theorems Thm.theoremK [((To_sbinding s, List.map (fn s => Attrib.check_src lthy [Token.make_string (s, Position.none)]) ["simp", "code_unfold"]), List.map (fn x => (Proof_Context.get_thms lthy (To_string0 x), [])) l)] [] false) lthy) | Theory_lemma (Lemma (n, l_spec, l_apply, o_by)) => in_local (fn lthy => Specification.theorem_cmd true Thm.theoremK NONE (K I) Binding.empty_atts [] [] (Element.Shows [((To_sbinding n, []) ,[((String.concatWith (" \ ") (List.map of_semi__term l_spec)), [])])]) false lthy |> fold (semi__command_proof o META.Command_apply) l_apply |> global_terminal_proof o_by) | Theory_lemma (Lemma_assumes (n, l_spec, concl, l_apply, o_by)) => in_local (fn lthy => lthy |> Specification.theorem_cmd true Thm.theoremK NONE (K I) (To_sbinding n, []) [] (List.map (fn (n, (b, e)) => Element.Assumes [( ( To_sbinding n , if b then [[Token.make_string ("simp", Position.none)]] else []) , [(of_semi__term e, [])])]) l_spec) (Element.Shows [(Binding.empty_atts, [(of_semi__term concl, [])])]) false |> fold semi__command_proof l_apply |> (case map_filter (fn META.Command_let _ => SOME [] | META.Command_have _ => SOME [] | META.Command_fix_let (_, _, _, l) => SOME l | _ => NONE) (rev l_apply) of [] => global_terminal_proof o_by | _ :: l => let val arg = (NONE, true) in fn st => st |> local_terminal_proof o_by |> fold (fn l => fold semi__command_state l o Proof.local_qed arg) l |> Proof.global_qed arg end)) | Theory_axiomatization (Axiomatization (n, e)) => in_theory (#2 o Specification.axiomatization_cmd [] [] [] [((To_sbinding n, []), of_semi__term e)]) | Theory_section _ => in_theory I | Theory_text _ => in_theory I | Theory_ML (SML ml) => in_theory (Code_printing.reflect_ml (Input.source false (of_semi__term' ml) (Position.none, Position.none))) | Theory_setup (Setup ml) => in_theory (Isar_Cmd.setup (Input.source false (of_semi__term' ml) (Position.none, Position.none))) | Theory_thm (Thm thm) => in_local (fn lthy => let val () = writeln (Pretty.string_of (Proof_Context.pretty_fact lthy ("", List.map (semi__thm_attribute_single lthy) thm))) in lthy end) | Theory_interpretation (Interpretation (n, loc_n, loc_param, o_by)) => in_local (fn lthy => lthy |> Interpretation.interpretation_cmd ( [ ( (To_string0 loc_n, Position.none) , ( (To_string0 n, true) , (if loc_param = [] then Expression.Named [] else Expression.Positional (map (SOME o of_semi__term) loc_param), [])))] , []) |> global_terminal_proof o_by) (*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy) end*) end end structure Bind_META = struct open Bind_Isabelle fun all_meta aux ret = let open META open META_overload in fn META_semi_theories thy => ret o (case thy of Theories_one thy => semi__theory I Named_Target.theory_map thy | Theories_locale (data, l) => fn thy => thy |> ( Expression.add_locale_cmd (To_sbinding (META.holThyLocale_name data)) Binding.empty ([], []) (List.concat (map (fn (fixes, assumes) => List.concat [ map (fn (e,ty) => Element.Fixes [( To_binding (of_semi__term e) , SOME (of_semi__typ ty) , NoSyn)]) fixes , case assumes of NONE => [] | SOME (n, e) => [Element.Assumes [( (To_sbinding n, []) , [(of_semi__term e, [])])]]]) (META.holThyLocale_header data))) #> snd) |> fold (fold (semi__theory Local_Theory.background_theory (fn f => - \ \Note: This function is not equivalent to \<^ML>\Local_Theory.subtarget\.\ Local_Theory.new_group #> f #> Local_Theory.reset_group #> (fn lthy => #1 (Named_Target.switch NONE (Context.Proof lthy)) lthy |> Context.the_proof)))) l |> Local_Theory.exit_global) | META_boot_generation_syntax _ => ret o I | META_boot_setup_env _ => ret o I | META_all_meta_embedding meta => fn thy => aux (map2_ctxt_term (fn T_pure x => T_pure x | e => let fun aux e = case e of T_to_be_parsed (s, _) => SOME let val t = Syntax.read_term (Proof_Context.init_global thy) (To_string0 s) in (t, Term.add_frees t []) end | T_lambda (a, e) => Option.map (fn (e, l_free) => let val a = To_string0 a val (t, l_free) = case List.partition (fn (x, _) => x = a) l_free of ([], l_free) => (Term.TFree ("'a", ["HOL.type"]), l_free) | ([(_, t)], l_free) => (t, l_free) in (lambda (Term.Free (a, t)) e, l_free) end) (aux e) | _ => NONE in case aux e of NONE => error "nested pure expression not expected" | SOME (e, _) => META.T_pure (From.Pure.term e) end) meta) thy end end \ (*<*) subsection\Directives of Compilation for Target Languages\ ML\ structure Deep0 = struct fun apply_hs_code_identifiers ml_module thy = let fun mod_hs (fic, ml_module) = Code_Symbol.Module (fic, [("Haskell", SOME ml_module)]) in fold (Code_Target.set_identifiers o mod_hs) (map (fn x => (Context.theory_name x, ml_module)) (* list of .hs files that will be merged together in "ml_module" *) ( thy :: (* we over-approximate the set of compiler files *) Context.ancestors_of thy)) thy end val default_key = "" structure Export_code_env = struct structure Isabelle = struct val function = "write_file" val argument_main = "main" end structure Haskell = struct val function = "Function" val argument = "Argument" val main = "Main" structure Filename = struct fun hs_function ext = function ^ "." ^ ext fun hs_argument ext = argument ^ "." ^ ext fun hs_main ext = main ^ "." ^ ext end end structure OCaml = struct val make = "write" structure Filename = struct fun function ext = "function." ^ ext fun argument ext = "argument." ^ ext fun main_fic ext = "main." ^ ext fun makefile ext = make ^ "." ^ ext end end structure Scala = struct structure Filename = struct fun function ext = "Function." ^ ext fun argument ext = "Argument." ^ ext end end structure SML = struct val main = "Run" structure Filename = struct fun function ext = "Function." ^ ext fun argument ext = "Argument." ^ ext fun stdout ext = "Stdout." ^ ext fun main_fic ext = main ^ "." ^ ext end end datatype file_input = File | Directory end fun compile l cmd = let val (l, rc) = fold (fn cmd => (fn (l, 0) => let val {out, err, rc, ...} = Bash.process cmd in ((out, err) :: l, rc) end | x => x)) l ([], 0) val l = rev l in if rc = 0 then (l, Isabelle_System.bash_output cmd) else let val () = fold (fn (out, err) => K (warning err; writeln out)) l () in error "Compilation failed" end end val check = fold (fn (cmd, msg) => fn () => let val (out, rc) = Isabelle_System.bash_output cmd in if rc = 0 then () else ( writeln out ; error msg) end) val compiler = let open Export_code_env in [ let val ml_ext = "hs" in ( "Haskell", ml_ext, Directory, Haskell.Filename.hs_function , check [("ghc --version", "ghc is not installed (required for compiling a Haskell project)")] , (fn mk_fic => fn ml_module => fn mk_free => fn thy => File.write (mk_fic ("Main." ^ ml_ext)) (String.concatWith "; " [ "import qualified Unsafe.Coerce" , "import qualified " ^ Haskell.function , "import qualified " ^ Haskell.argument , "main :: IO ()" , "main = " ^ Haskell.function ^ "." ^ Isabelle.function ^ " (Unsafe.Coerce.unsafeCoerce " ^ Haskell.argument ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ ")"])) , fn tmp_export_code => fn tmp_file => compile [ "mv " ^ tmp_file ^ "/" ^ Haskell.Filename.hs_argument ml_ext ^ " " ^ Path.implode tmp_export_code , "cd " ^ Path.implode tmp_export_code ^ " && ghc -outputdir _build " ^ Haskell.Filename.hs_main ml_ext ] (Path.implode (Path.append tmp_export_code (Path.make [Haskell.main])))) end , let val ml_ext = "ml" in ( "OCaml", ml_ext, File, OCaml.Filename.function , check [("ocp-build -version", "ocp-build is not installed (required for compiling an OCaml project)") ,("ocamlopt -version", "ocamlopt is not installed (required for compiling an OCaml project)")] , fn mk_fic => fn ml_module => fn mk_free => fn thy => let val () = File.write (mk_fic (OCaml.Filename.makefile "ocp")) (String.concat [ "comp += \"-g\" link += \"-g\" " , "begin generated = true begin library \"nums\" end end " , "begin program \"", OCaml.make, "\" sort = true files = [ \"", OCaml.Filename.function ml_ext , "\" \"", OCaml.Filename.argument ml_ext , "\" \"", OCaml.Filename.main_fic ml_ext , "\" ]" , "requires = [\"nums\"] " , "end" ]) in File.write (mk_fic (OCaml.Filename.main_fic ml_ext)) ("let _ = Function." ^ ml_module ^ "." ^ Isabelle.function ^ " (Obj.magic (Argument." ^ ml_module ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ "))") end , fn tmp_export_code => fn tmp_file => compile [ "mv " ^ tmp_file ^ " " ^ Path.implode (Path.append tmp_export_code (Path.make [OCaml.Filename.argument ml_ext])) , "cd " ^ Path.implode tmp_export_code ^ " && ocp-build -init -scan -no-bytecode 2>&1" ] (Path.implode (Path.append tmp_export_code (Path.make [ "_obuild" , OCaml.make , OCaml.make ^ ".asm"])))) end , let val ml_ext = "scala" val ml_module = Unsynchronized.ref ("", "") in ( "Scala", ml_ext, File, Scala.Filename.function , check [("scala -e 0", "scala is not installed (required for compiling a Scala project)")] , (fn _ => fn ml_mod => fn mk_free => fn thy => ml_module := (ml_mod, mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list))) , fn tmp_export_code => fn tmp_file => let val l = File.read_lines (Path.explode tmp_file) val (ml_module, ml_main) = Unsynchronized.! ml_module val () = File.write_list (Path.append tmp_export_code (Path.make [Scala.Filename.argument ml_ext])) (List.map (fn s => s ^ "\n") ("object " ^ ml_module ^ " { def main (__ : Array [String]) = " ^ ml_module ^ "." ^ Isabelle.function ^ " (" ^ ml_module ^ "." ^ ml_main ^ ")" :: l @ ["}"])) in compile [] ("scala -nowarn " ^ Path.implode (Path.append tmp_export_code (Path.make [Scala.Filename.argument ml_ext]))) end) end , let val ml_ext_thy = "thy" val ml_ext_ml = "ML" in ( "SML", ml_ext_ml, File, SML.Filename.function , check [ let val isa = "isabelle" in ( Path.implode (Path.expand (Path.append (Path.variable "ISABELLE_HOME") (Path.make ["bin", isa]))) ^ " version" , isa ^ " is not installed (required for compiling a SML project)") end ] , fn mk_fic => fn ml_module => fn mk_free => fn thy => let val esc_star = "*" fun ml l = List.concat [ [ "ML{" ^ esc_star ] , map (fn s => s ^ ";") l , [ esc_star ^ "}"] ] val () = let val fic = mk_fic (SML.Filename.function ml_ext_ml) in (* replace ("\\" ^ "<") by ("\\\060") in 'fic' *) File.write_list fic (map (fn s => (if s = "" then "" else String.concatWith "\\" (map (fn s => let val l = String.size s in if l > 0 andalso String.sub (s,0) = #"<" then "\\060" ^ String.substring (s, 1, String.size s - 1) else s end) (String.fields (fn c => c = #"\\") s))) ^ "\n") (File.read_lines fic)) end in File.write_list (mk_fic (SML.Filename.main_fic ml_ext_thy)) (map (fn s => s ^ "\n") (List.concat [ [ "theory " ^ SML.main , "imports Main" , "begin" , "declare [[ML_print_depth = 500]]" (* any large number so that @{make_string} displays all the expression *) ] , ml [ "val stdout_file = Unsynchronized.ref (File.read (Path.make [\"" ^ SML.Filename.stdout ml_ext_ml ^ "\"]))" , "use \"" ^ SML.Filename.argument ml_ext_ml ^ "\"" ] , ml let val arg = "argument" in [ "val " ^ arg ^ " = XML.content_of (YXML.parse_body (@{make_string} (" ^ ml_module ^ "." ^ mk_free (Proof_Context.init_global thy) Isabelle.argument_main ([]: (string * string) list) ^ ")))" , "use \"" ^ SML.Filename.function ml_ext_ml ^ "\"" , "ML_Context.eval_source (ML_Compiler.verbose false ML_Compiler.flags) (Input.source false (\"let open " ^ ml_module ^ " in " ^ Isabelle.function ^ " (\" ^ " ^ arg ^ " ^ \") end\") (Position.none, Position.none) )" ] end , [ "end" ]])) end , fn tmp_export_code => fn tmp_file => let val stdout_file = Isabelle_System.create_tmp_path "stdout_file" "thy" val () = File.write (Path.append tmp_export_code (Path.make [SML.Filename.stdout ml_ext_ml])) (Path.implode (Path.expand stdout_file)) val (l, (_, exit_st)) = compile [ "mv " ^ tmp_file ^ " " ^ Path.implode (Path.append tmp_export_code (Path.make [SML.Filename.argument ml_ext_ml])) , "cd " ^ Path.implode tmp_export_code ^ " && echo 'use_thy \"" ^ SML.main ^ "\";' | " ^ Path.implode (Path.expand (Path.append (Path.variable "ISABELLE_HOME") (Path.make ["bin", "isabelle"]))) ^ " console" ] "true" val stdout = case try File.read stdout_file of SOME s => let val () = File.rm stdout_file in s end | NONE => "" in (l, (stdout, if List.exists (fn (err, _) => List.exists (fn "*** Error" => true | _ => false) (String.tokens (fn #"\n" => true | _ => false) err)) l then let val () = fold (fn (out, err) => K (warning err; writeln out)) l () in 1 end else exit_st)) end) end ] end structure Find = struct fun ext ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, ext, _, _, _, _, _) => ext fun export_mode ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, mode, _, _, _, _) => mode fun function ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, f, _, _, _) => f fun check_compil ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, build, _, _) => build fun init ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, _, build, _) => build fun build ml_compiler = case List.find (fn (ml_compiler0, _, _, _, _, _, _) => ml_compiler0 = ml_compiler) compiler of SOME (_, _, _, _, _, _, build) => build end end \ ML\ structure Deep = struct fun absolute_path filename thy = Path.implode (Path.append (Resources.master_directory thy) (Path.explode filename)) fun export_code_tmp_file seris g = fold (fn ((ml_compiler, ml_module), export_arg) => fn f => fn g => f (fn accu => let val tmp_name = Context.theory_name @{theory} in (if Deep0.Find.export_mode ml_compiler = Deep0.Export_code_env.Directory then Isabelle_System.with_tmp_dir tmp_name else Isabelle_System.with_tmp_file tmp_name (Deep0.Find.ext ml_compiler)) (fn filename => g (((((ml_compiler, ml_module), Path.implode filename), export_arg) :: accu))) end)) seris (fn f => f []) (g o rev) fun mk_path_export_code tmp_export_code ml_compiler i = Path.append tmp_export_code (Path.make [ml_compiler ^ Int.toString i]) fun export_code_cmd' seris tmp_export_code f_err filename_thy raw_cs thy = export_code_tmp_file seris (fn seris => let val mem_scala = List.exists (fn ((("Scala", _), _), _) => true | _ => false) seris val thy' (* FIXME unused *) = Isabelle_Code_Target.export_code_cmd false (if mem_scala then Deep0.Export_code_env.Isabelle.function :: raw_cs else raw_cs) ((map o apfst o apsnd) SOME seris) (let val v = Deep0.apply_hs_code_identifiers Deep0.Export_code_env.Haskell.argument thy in if mem_scala then Code_printing.apply_code_printing v else v end) in List_mapi (fn i => fn seri => case seri of (((ml_compiler, _), filename), _) => let val (l, (out, err)) = Deep0.Find.build ml_compiler (mk_path_export_code tmp_export_code ml_compiler i) filename val _ = f_err seri err in (l, out) end) seris end) fun mk_term ctxt s = fst (Scan.pass (Context.Proof ctxt) Args.term (Token.explode0 (Thy_Header.get_keywords' ctxt) s)) fun mk_free ctxt s l = let val t_s = mk_term ctxt s in if Term.is_Free t_s then s else let val l = (s, "") :: l in mk_free ctxt (fst (hd (Term.variant_frees t_s l))) l end end val list_all_eq = fn x0 :: xs => List.all (fn x1 => x0 = x1) xs end \ subsection\Saving the History of Meta Commands\ ML\ fun p_gen f g = f "[" "]" g (*|| f "{" "}" g*) || f "(" ")" g fun paren f = p_gen (fn s1 => fn s2 => fn f => Parse.$$$ s1 |-- f --| Parse.$$$ s2) f fun parse_l f = Parse.$$$ "[" |-- Parse.!!! (Parse.list f --| Parse.$$$ "]") fun parse_l' f = Parse.$$$ "[" |-- Parse.list f --| Parse.$$$ "]" fun parse_l1' f = Parse.$$$ "[" |-- Parse.list1 f --| Parse.$$$ "]" fun annot_ty f = Parse.$$$ "(" |-- f --| Parse.$$$ "::" -- Parse.binding --| Parse.$$$ ")" \ ML\ structure Generation_mode = struct datatype internal_deep = Internal_deep of (string * (string list (* imports *) * string (* import optional (bootstrap) *))) option * ((bstring (* compiler *) * bstring (* main module *) ) * Token.T list) list (* seri_args *) * bstring option (* filename_thy *) * Path.T (* tmp dir export_code *) * bool (* true: skip preview of code exportation *) datatype 'a generation_mode = Gen_deep of unit META.compiler_env_config_ext * internal_deep | Gen_shallow of unit META.compiler_env_config_ext * 'a (* theory init *) | Gen_syntax_print of int option structure Data_gen = Theory_Data (type T = theory generation_mode list Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.merge (K true)) val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) [] val parse_scheme = @{keyword "design"} >> K META.Gen_only_design || @{keyword "analysis"} >> K META.Gen_only_analysis val parse_sorry_mode = Scan.optional ( @{keyword "SORRY"} >> K (SOME META.Gen_sorry) || @{keyword "no_dirty"} >> K (SOME META.Gen_no_dirty)) NONE val parse_deep = Scan.optional (@{keyword "skip_export"} >> K true) false -- Scan.optional (((Parse.$$$ "(" -- @{keyword "THEORY"}) |-- Parse.name -- ((Parse.$$$ ")" -- Parse.$$$ "(" -- @{keyword "IMPORTS"}) |-- parse_l' Parse.name -- Parse.name) --| Parse.$$$ ")") >> SOME) NONE -- Scan.optional (@{keyword "SECTION"} >> K true) false -- parse_sorry_mode -- (* code_expr_inP *) parse_l1' (@{keyword "in"} |-- (Parse.name -- Scan.optional (@{keyword "module_name"} |-- Parse.name) "" -- code_expr_argsP)) -- Scan.optional ((Parse.$$$ "(" -- @{keyword "output_directory"}) |-- Parse.name --| Parse.$$$ ")" >> SOME) NONE val parse_semantics = let val z = 0 in Scan.optional (paren (@{keyword "generation_semantics"} |-- paren (parse_scheme -- Scan.optional ((Parse.$$$ "," -- @{keyword "oid_start"}) |-- Parse.nat) z))) (META.Gen_default, z) end val mode = let fun mk_env output_disable_thy output_header_thy oid_start design_analysis sorry_mode dirty = META.compiler_env_config_empty output_disable_thy (From.option (From.pair From.string (From.pair (From.list From.string) From.string)) output_header_thy) (META.oidInit (From.internal_oid oid_start)) design_analysis (sorry_mode, dirty) in @{keyword "deep"} |-- parse_semantics -- parse_deep >> (fn ( (design_analysis, oid_start) , ( ((((skip_exportation, output_header_thy), output_disable_thy), sorry_mode), seri_args) , filename_thy)) => fn ctxt => Gen_deep ( mk_env (not output_disable_thy) output_header_thy oid_start design_analysis sorry_mode (Config.get ctxt quick_and_dirty) , Internal_deep ( output_header_thy , seri_args , filename_thy , Isabelle_System.create_tmp_path "deep_export_code" "" , skip_exportation))) || @{keyword "shallow"} |-- parse_semantics -- parse_sorry_mode >> (fn ((design_analysis, oid_start), sorry_mode) => fn ctxt => Gen_shallow ( mk_env true NONE oid_start design_analysis sorry_mode (Config.get ctxt quick_and_dirty) , ())) || (@{keyword "syntax_print"} |-- Scan.optional (Parse.number >> SOME) NONE) >> (fn n => K (Gen_syntax_print (case n of NONE => NONE | SOME n => Int.fromString n))) end fun f_command l_mode = Toplevel.theory (fn thy => let val (l_mode, thy) = META.mapM (fn Gen_shallow (env, ()) => let val thy0 = thy in fn thy => (Gen_shallow (env, thy0), thy) end | Gen_syntax_print n => (fn thy => (Gen_syntax_print n, thy)) | Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)) => fn thy => let val _ = warning ("After closing Isabelle/jEdit, we may still need to remove this directory (by hand): " ^ Path.implode (Path.expand tmp_export_code)) val seri_args' = List_mapi (fn i => fn ((ml_compiler, ml_module), export_arg) => let val tmp_export_code = Deep.mk_path_export_code tmp_export_code ml_compiler i fun mk_fic s = Path.append tmp_export_code (Path.make [s]) val () = Deep0.Find.check_compil ml_compiler () val _ = Isabelle_System.make_directory tmp_export_code in ((( (ml_compiler, ml_module) , Path.implode (if Deep0.Find.export_mode ml_compiler = Deep0.Export_code_env.Directory then tmp_export_code else mk_fic (Deep0.Find.function ml_compiler (Deep0.Find.ext ml_compiler)))) , export_arg), mk_fic) end) seri_args val thy' (* FIXME unused *) = Isabelle_Code_Target.export_code_cmd (List.exists (fn (((("SML", _), _), _), _) => true | _ => false) seri_args') [Deep0.Export_code_env.Isabelle.function] (List.map ((apfst o apsnd) SOME o fst) seri_args') (Code_printing.apply_code_printing (Deep0.apply_hs_code_identifiers Deep0.Export_code_env.Haskell.function thy)) val () = fold (fn ((((ml_compiler, ml_module), _), _), mk_fic) => fn _ => Deep0.Find.init ml_compiler mk_fic ml_module Deep.mk_free thy) seri_args' () in (Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)), thy) end) let val ctxt = Proof_Context.init_global thy in map (fn f => f ctxt) l_mode end thy in Data_gen.map (Symtab.map_default (Deep0.default_key, l_mode) (fn _ => l_mode)) thy end) fun update_compiler_config f = Data_gen.map (Symtab.map_entry Deep0.default_key (fn l_mode => map (fn Gen_deep (env, d) => Gen_deep (META.compiler_env_config_update f env, d) | Gen_shallow (env, thy) => Gen_shallow (META.compiler_env_config_update f env, thy) | Gen_syntax_print n => Gen_syntax_print n) l_mode)) end \ subsection\Factoring All Meta Commands Together\ setup\ML_Antiquotation.inline @{binding mk_string} (Scan.succeed "(fn ctxt => fn x => ML_Pretty.string_of_polyml (ML_system_pretty (x, FixedInt.fromInt (Config.get ctxt (ML_Print_Depth.print_depth)))))") \ ML\ fun exec_deep (env, output_header_thy, seri_args, filename_thy, tmp_export_code, l_obj) thy0 = let open Generation_mode in let val of_arg = META.isabelle_of_compiler_env_config META.isabelle_apply I in let fun def s = Named_Target.theory_map (snd o Specification.definition_cmd NONE [] [] (Binding.empty_atts, s) false) in let val name_main = Deep.mk_free (Proof_Context.init_global thy0) Deep0.Export_code_env.Isabelle.argument_main [] in thy0 |> def (String.concatWith " " ( "(" (* polymorphism weakening needed by export_code *) ^ name_main ^ " :: (_ \ abr_string option) compiler_env_config_scheme)" :: "=" :: To_string0 (of_arg (META.compiler_env_config_more_map (fn () => (l_obj, From.option From.string (Option.map (fn filename_thy => Deep.absolute_path filename_thy thy0) filename_thy))) env)) :: [])) |> Deep.export_code_cmd' seri_args tmp_export_code (fn (((_, _), msg), _) => fn err => if err <> 0 then error msg else ()) filename_thy [name_main] |> (fn l => let val (l_warn, l) = (map fst l, map snd l) in if Deep.list_all_eq l then (List.concat l_warn, hd l) else error "There is an extracted language which does not produce a similar Isabelle content as the others" end) |> (fn (l_warn, s) => let val () = writeln (case (output_header_thy, filename_thy) of (SOME _, SOME _) => s | _ => String.concat (map ( (fn s => s ^ "\n") o Active.sendback_markup_command o trim_line) (String.tokens (fn c => c = #"\t") s))) in fold (fn (out, err) => K ( writeln (Markup.markup Markup.keyword2 err) ; case trim_line out of "" => () | out => writeln (Markup.markup Markup.keyword1 out))) l_warn () end) end end end end fun outer_syntax_command0 mk_string cmd_spec cmd_descr parser get_all_meta_embed = let open Generation_mode in Outer_Syntax.command cmd_spec cmd_descr (parser >> (fn name => Toplevel.theory (fn thy => let val (env, thy) = META.mapM let val get_all_meta_embed = get_all_meta_embed name in fn Gen_syntax_print n => (fn thy => let val _ = writeln (mk_string (Proof_Context.init_global (case n of NONE => thy | SOME n => Config.put_global ML_Print_Depth.print_depth n thy)) name) in (Gen_syntax_print n, thy) end) | Gen_deep (env, Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)) => (fn thy0 => let val l_obj = get_all_meta_embed thy0 in thy0 |> (if skip_exportation then K () else exec_deep ( META.d_output_header_thy_update (fn _ => NONE) env , output_header_thy , seri_args , NONE , tmp_export_code , l_obj)) |> K (Gen_deep ( META.fold_thy_deep l_obj env , Internal_deep ( output_header_thy , seri_args , filename_thy , tmp_export_code , skip_exportation)), thy0) end) | Gen_shallow (env, thy0) => fn thy => let fun aux (env, thy) x = META.fold_thy_shallow (fn f => f () handle ERROR e => ( warning "Shallow Backtracking: (true) Isabelle declarations occurring among the META-simulated ones are ignored (if any)" (* TODO automatically determine if there is such Isabelle declarations, for raising earlier a specific error message *) ; error e)) (fn _ => fn _ => thy0) (fn l => fn (env, thy) => Bind_META.all_meta (fn x => fn thy => aux (env, thy) [x]) (pair env) l thy) x (env, thy) val (env, thy) = aux (env, thy) (get_all_meta_embed thy) in (Gen_shallow (env, thy0), thy) end end (case Symtab.lookup (Data_gen.get thy) Deep0.default_key of SOME l => l | _ => [Gen_syntax_print NONE]) thy in Data_gen.map (Symtab.update (Deep0.default_key, env)) thy end))) end fun outer_syntax_command mk_string cmd_spec cmd_descr parser get_all_meta_embed = outer_syntax_command0 mk_string cmd_spec cmd_descr parser (fn a => fn thy => [get_all_meta_embed a thy]) \ subsection\Parameterizing the Semantics of Embedded Languages\ ML\ val () = let open Generation_mode in Outer_Syntax.command @{command_keyword generation_syntax} "set the generating list" (( mode >> (fn x => SOME [x]) || parse_l' mode >> SOME || @{keyword "deep"} -- @{keyword "flush_all"} >> K NONE) >> (fn SOME x => f_command x | NONE => Toplevel.theory (fn thy => let val l = case Symtab.lookup (Data_gen.get thy) Deep0.default_key of SOME l => l | _ => [] val l = List.concat (List.map (fn Gen_deep x => [x] | _ => []) l) val _ = case l of [] => warning "Nothing to perform." | _ => () val thy = fold (fn (env, Internal_deep (output_header_thy, seri_args, filename_thy, tmp_export_code, _)) => fn thy0 => thy0 |> let val (env, l_exec) = META.compiler_env_config_reset_all env in exec_deep (env, output_header_thy, seri_args, filename_thy, tmp_export_code, l_exec) end |> K thy0) l thy in thy end))) end \ subsection\Common Parser for Toy\ ML\ structure TOY_parse = struct datatype ('a, 'b) use_context = TOY_context_invariant of 'a | TOY_context_pre_post of 'b fun optional f = Scan.optional (f >> SOME) NONE val colon = Parse.$$$ ":" fun repeat2 scan = scan ::: Scan.repeat1 scan fun xml_unescape s = (XML.content_of (YXML.parse_body s), Position.none) |> Symbol_Pos.explode |> Symbol_Pos.implode |> From.string fun outer_syntax_command2 mk_string cmd_spec cmd_descr parser v_true v_false get_all_meta_embed = outer_syntax_command mk_string cmd_spec cmd_descr (optional (paren @{keyword "shallow"}) -- parser) (fn (is_shallow, use) => fn thy => get_all_meta_embed (if is_shallow = NONE then ( fn s => META.T_to_be_parsed ( From.string s , xml_unescape s) , v_true) else (From.toy_ctxt_term thy, v_false)) use) (* *) val ident_dot_dot = let val f = Parse.sym_ident >> (fn "\" => "\" | _ => Scan.fail "Syntax error") in f -- f end val ident_star = Parse.sym_ident (* "*" *) (* *) val unlimited_natural = ident_star >> (fn "*" => META.Mult_star | "\" => META.Mult_infinity | _ => Scan.fail "Syntax error") || Parse.number >> (fn s => META.Mult_nat (case Int.fromString s of SOME i => Code_Numeral.natural_of_integer i | NONE => Scan.fail "Syntax error")) val term_base = Parse.number >> (META.ToyDefInteger o From.string) || Parse.float_number >> (META.ToyDefReal o (From.pair From.string From.string o (fn s => case String.tokens (fn #"." => true | _ => false) s of [l1,l2] => (l1,l2) | _ => Scan.fail "Syntax error"))) || Parse.string >> (META.ToyDefString o From.string) val multiplicity = parse_l' (unlimited_natural -- optional (ident_dot_dot |-- unlimited_natural)) fun toy_term x = ( term_base >> META.ShallB_term || Parse.binding >> (META.ShallB_str o From.binding) || @{keyword "self"} |-- Parse.nat >> (fn n => META.ShallB_self (From.internal_oid n)) || paren (Parse.list toy_term) >> (* untyped, corresponds to Set, Sequence or Pair *) (* WARNING for Set: we are describing a finite set *) META.ShallB_list) x val name_object = optional (Parse.list1 Parse.binding --| colon) -- Parse.binding val type_object_weak = let val name_object = Parse.binding >> (fn s => (NONE, s)) in name_object -- Scan.repeat (Parse.$$$ "<" |-- Parse.list1 name_object) >> let val f = fn (_, s) => META.ToyTyCore_pre (From.binding s) in fn (s, l) => META.ToyTyObj (f s, map (map f) l) end end val type_object = name_object -- Scan.repeat (Parse.$$$ "<" |-- Parse.list1 name_object) >> let val f = fn (_, s) => META.ToyTyCore_pre (From.binding s) in fn (s, l) => META.ToyTyObj (f s, map (map f) l) end val category = multiplicity -- optional (@{keyword "Role"} |-- Parse.binding) -- Scan.repeat ( @{keyword "Ordered"} >> K META.Ordered0 || @{keyword "Subsets"} |-- Parse.binding >> K META.Subsets0 || @{keyword "Union"} >> K META.Union0 || @{keyword "Redefines"} |-- Parse.binding >> K META.Redefines0 || @{keyword "Derived"} -- Parse.$$$ "=" |-- Parse.term >> K META.Derived0 || @{keyword "Qualifier"} |-- Parse.term >> K META.Qualifier0 || @{keyword "Nonunique"} >> K META.Nonunique0 || @{keyword "Sequence_"} >> K META.Sequence) >> (fn ((l_mult, role), l) => META.Toy_multiplicity_ext (l_mult, From.option From.binding role, l, ())) val type_base = Parse.reserved "Void" >> K META.ToyTy_base_void || Parse.reserved "Boolean" >> K META.ToyTy_base_boolean || Parse.reserved "Integer" >> K META.ToyTy_base_integer || Parse.reserved "UnlimitedNatural" >> K META.ToyTy_base_unlimitednatural || Parse.reserved "Real" >> K META.ToyTy_base_real || Parse.reserved "String" >> K META.ToyTy_base_string fun use_type_gen type_object v = ((* collection *) Parse.reserved "Set" |-- use_type >> (fn l => META.ToyTy_collection (META.Toy_multiplicity_ext ([], NONE, [META.Set], ()), l)) || Parse.reserved "Sequence" |-- use_type >> (fn l => META.ToyTy_collection (META.Toy_multiplicity_ext ([], NONE, [META.Sequence], ()), l)) || category -- use_type >> META.ToyTy_collection (* pair *) || Parse.reserved "Pair" |-- ( use_type -- use_type || Parse.$$$ "(" |-- use_type --| Parse.$$$ "," -- use_type --| Parse.$$$ ")") >> META.ToyTy_pair (* base *) || type_base (* raw HOL *) || Parse.sym_ident (* "\" *) |-- Parse.typ --| Parse.sym_ident (* "\" *) >> (META.ToyTy_raw o xml_unescape) (* object type *) || type_object >> META.ToyTy_object || ((Parse.$$$ "(" |-- Parse.list ( (Parse.binding --| colon >> (From.option From.binding o SOME)) -- ( Parse.$$$ "(" |-- use_type --| Parse.$$$ ")" || use_type_gen type_object_weak) >> META.ToyTy_binding ) --| Parse.$$$ ")" >> (fn ty_arg => case rev ty_arg of [] => META.ToyTy_base_void | ty_arg => fold (fn x => fn acc => META.ToyTy_pair (x, acc)) (tl ty_arg) (hd ty_arg))) -- optional (colon |-- use_type)) >> (fn (ty_arg, ty_out) => case ty_out of NONE => ty_arg | SOME ty_out => META.ToyTy_arrow (ty_arg, ty_out)) || (Parse.$$$ "(" |-- use_type --| Parse.$$$ ")" >> (fn s => META.ToyTy_binding (NONE, s)))) v and use_type x = use_type_gen type_object x val use_prop = (optional (optional (Parse.binding >> From.binding) --| Parse.$$$ ":") >> (fn NONE => NONE | SOME x => x)) -- Parse.term --| optional (Parse.$$$ ";") >> (fn (n, e) => fn from_expr => META.ToyProp_ctxt (n, from_expr e)) (* *) val association_end = type_object -- category --| optional (Parse.$$$ ";") val association = optional @{keyword "Between"} |-- Scan.optional (repeat2 association_end) [] val invariant = optional @{keyword "Constraints"} |-- Scan.optional (@{keyword "Existential"} >> K true) false --| @{keyword "Inv"} -- use_prop structure Outer_syntax_Association = struct fun make ass_ty l = META.Toy_association_ext (ass_ty, META.ToyAssRel l, ()) end (* *) val context = Scan.repeat (( optional (@{keyword "Operations"} || Parse.$$$ "::") |-- Parse.binding -- use_type --| optional (Parse.$$$ "=" |-- Parse.term || Parse.term) -- Scan.repeat ( (@{keyword "Pre"} || @{keyword "Post"}) -- use_prop >> TOY_context_pre_post || invariant >> TOY_context_invariant) --| optional (Parse.$$$ ";")) >> (fn ((name_fun, ty), expr) => fn from_expr => META.Ctxt_pp (META.Toy_ctxt_pre_post_ext ( From.binding name_fun , ty , From.list (fn TOY_context_pre_post (pp, expr) => META.T_pp (if pp = "Pre" then META.ToyCtxtPre else META.ToyCtxtPost, expr from_expr) | TOY_context_invariant (b, expr) => META.T_invariant (META.T_inv (b, expr from_expr))) expr , ()))) || invariant >> (fn (b, expr) => fn from_expr => META.Ctxt_inv (META.T_inv (b, expr from_expr)))) val class = optional @{keyword "Attributes"} |-- Scan.repeat (Parse.binding --| colon -- use_type --| optional (Parse.$$$ ";")) -- context datatype use_classDefinition = TOY_class | TOY_class_abstract datatype ('a, 'b) use_classDefinition_content = TOY_class_content of 'a | TOY_class_synonym of 'b structure Outer_syntax_Class = struct fun make from_expr abstract ty_object attribute oper = META.Toy_class_raw_ext ( ty_object , From.list (From.pair From.binding I) attribute , From.list (fn f => f from_expr) oper , abstract , ()) end (* *) val term_object = parse_l ( optional ( Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ "," -- Parse.binding --| Parse.$$$ ")" --| (Parse.sym_ident >> (fn "|=" => Scan.succeed | _ => Scan.fail ""))) -- Parse.binding -- ( Parse.$$$ "=" |-- toy_term)) val list_attr' = term_object >> (fn res => (res, [] : binding list)) fun object_cast e = ( annot_ty term_object -- Scan.repeat ( (Parse.sym_ident >> (fn "->" => Scan.succeed | "\" => Scan.succeed | "\" => Scan.succeed | _ => Scan.fail "")) |-- ( Parse.reserved "toyAsType" |-- Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")" || Parse.binding)) >> (fn ((res, x), l) => (res, rev (x :: l)))) e val object_cast' = object_cast >> (fn (res, l) => (res, rev l)) fun get_toyinst l _ = META.ToyInstance (map (fn ((name,typ), (l_attr, is_cast)) => let val f = map (fn ((pre_post, attr), data) => ( From.option (From.pair From.binding From.binding) pre_post , ( From.binding attr , data))) val l_attr = fold (fn b => fn acc => META.ToyAttrCast (From.binding b, acc, [])) is_cast (META.ToyAttrNoCast (f l_attr)) in META.Toy_instance_single_ext (From.option From.binding name, From.option From.binding typ, l_attr, ()) end) l) val parse_instance = (Parse.binding >> SOME) -- optional (@{keyword "::"} |-- Parse.binding) --| @{keyword "="} -- (list_attr' || object_cast') (* *) datatype state_content = ST_l_attr of (((binding * binding) option * binding) * META.toy_data_shallow) list * binding list | ST_binding of binding val state_parse = parse_l' ( object_cast >> ST_l_attr || Parse.binding >> ST_binding) fun mk_state thy = map (fn ST_l_attr l => META.ToyDefCoreAdd (case get_toyinst (map (fn (l_i, l_ty) => ((NONE, SOME (hd l_ty)), (l_i, rev (tl l_ty)))) [l]) thy of META.ToyInstance [x] => x) | ST_binding b => META.ToyDefCoreBinding (From.binding b)) (* *) datatype state_pp_content = ST_PP_l_attr of state_content list | ST_PP_binding of binding val state_pp_parse = state_parse >> ST_PP_l_attr || Parse.binding >> ST_PP_binding fun mk_pp_state thy = fn ST_PP_l_attr l => META.ToyDefPPCoreAdd (mk_state thy l) | ST_PP_binding s => META.ToyDefPPCoreBinding (From.binding s) end \ subsection\Setup of Meta Commands for Toy: Enum\ ML\ val () = outer_syntax_command @{mk_string} @{command_keyword Enum} "" (Parse.binding -- parse_l1' Parse.binding) (fn (n1, n2) => K (META.META_enum (META.ToyEnum (From.binding n1, From.list From.binding n2)))) \ subsection\Setup of Meta Commands for Toy: (abstract) Class\ ML\ local open TOY_parse fun mk_classDefinition abstract cmd_spec = outer_syntax_command2 @{mk_string} cmd_spec "Class generation" ( Parse.binding --| Parse.$$$ "=" -- TOY_parse.type_base >> TOY_class_synonym || type_object -- class >> TOY_class_content) (curry META.META_class_raw META.Floor1) (curry META.META_class_raw META.Floor2) (fn (from_expr, META_class_raw) => fn TOY_class_content (ty_object, (attribute, oper)) => META_class_raw (Outer_syntax_Class.make from_expr (abstract = TOY_class_abstract) ty_object attribute oper) | TOY_class_synonym (n1, n2) => META.META_class_synonym (META.ToyClassSynonym (From.binding n1, n2))) in val () = mk_classDefinition TOY_class @{command_keyword Class} val () = mk_classDefinition TOY_class_abstract @{command_keyword Abstract_class} end \ subsection\Setup of Meta Commands for Toy: Association, Composition, Aggregation\ ML\ local open TOY_parse fun mk_associationDefinition ass_ty cmd_spec = outer_syntax_command @{mk_string} cmd_spec "" ( repeat2 association_end || optional Parse.binding |-- association) (fn l => fn _ => META.META_association (Outer_syntax_Association.make ass_ty l)) in val () = mk_associationDefinition META.ToyAssTy_association @{command_keyword Association} val () = mk_associationDefinition META.ToyAssTy_composition @{command_keyword Composition} val () = mk_associationDefinition META.ToyAssTy_aggregation @{command_keyword Aggregation} end \ subsection\Setup of Meta Commands for Toy: (abstract) Associationclass\ ML\ local open TOY_parse datatype use_associationClassDefinition = TOY_associationclass | TOY_associationclass_abstract fun mk_associationClassDefinition abstract cmd_spec = outer_syntax_command2 @{mk_string} cmd_spec "" ( type_object -- association -- class -- optional (Parse.reserved "aggregation" || Parse.reserved "composition")) (curry META.META_ass_class META.Floor1) (curry META.META_ass_class META.Floor2) (fn (from_expr, META_ass_class) => fn (((ty_object, l_ass), (attribute, oper)), assty) => META_ass_class (META.ToyAssClass ( Outer_syntax_Association.make (case assty of SOME "aggregation" => META.ToyAssTy_aggregation | SOME "composition" => META.ToyAssTy_composition | _ => META.ToyAssTy_association) l_ass , Outer_syntax_Class.make from_expr (abstract = TOY_associationclass_abstract) ty_object attribute oper))) in val () = mk_associationClassDefinition TOY_associationclass @{command_keyword Associationclass} val () = mk_associationClassDefinition TOY_associationclass_abstract @{command_keyword Abstract_associationclass} end \ subsection\Setup of Meta Commands for Toy: Context\ ML\ local open TOY_parse in val () = outer_syntax_command2 @{mk_string} @{command_keyword Context} "" (optional (Parse.list1 Parse.binding --| colon) -- Parse.binding -- context) (curry META.META_ctxt META.Floor1) (curry META.META_ctxt META.Floor2) (fn (from_expr, META_ctxt) => (fn ((l_param, name), l) => META_ctxt (META.Toy_ctxt_ext ( case l_param of NONE => [] | SOME l => From.list From.binding l , META.ToyTyObj (META.ToyTyCore_pre (From.binding name), []) , From.list (fn f => f from_expr) l , ())))) end \ subsection\Setup of Meta Commands for Toy: End\ ML\ val () = outer_syntax_command0 @{mk_string} @{command_keyword End} "Class generation" (Scan.optional ( Parse.$$$ "[" -- Parse.reserved "forced" -- Parse.$$$ "]" >> K true || Parse.$$$ "!" >> K true) false) (fn b => fn _ => if b then [META.META_flush_all META.ToyFlushAll] else []) \ subsection\Setup of Meta Commands for Toy: BaseType, Instance, State\ ML\ val () = outer_syntax_command @{mk_string} @{command_keyword BaseType} "" (parse_l' TOY_parse.term_base) (K o META.META_def_base_l o META.ToyDefBase) local open TOY_parse in val () = outer_syntax_command @{mk_string} @{command_keyword Instance} "" (Scan.optional (parse_instance -- Scan.repeat (optional @{keyword "and"} |-- parse_instance) >> (fn (x, xs) => x :: xs)) []) (META.META_instance oo get_toyinst) val () = outer_syntax_command @{mk_string} @{command_keyword State} "" (TOY_parse.optional (paren @{keyword "shallow"}) -- Parse.binding --| @{keyword "="} -- state_parse) (fn ((is_shallow, name), l) => fn thy => META.META_def_state ( if is_shallow = NONE then META.Floor1 else META.Floor2 , META.ToyDefSt (From.binding name, mk_state thy l))) end \ subsection\Setup of Meta Commands for Toy: PrePost\ ML\ local open TOY_parse in val () = outer_syntax_command @{mk_string} @{command_keyword PrePost} "" (TOY_parse.optional (paren @{keyword "shallow"}) -- TOY_parse.optional (Parse.binding --| @{keyword "="}) -- state_pp_parse -- TOY_parse.optional state_pp_parse) (fn (((is_shallow, n), s_pre), s_post) => fn thy => META.META_def_pre_post ( if is_shallow = NONE then META.Floor1 else META.Floor2 , META.ToyDefPP ( From.option From.binding n , mk_pp_state thy s_pre , From.option (mk_pp_state thy) s_post))) end (*val _ = print_depth 100*) \ (*>*) end diff --git a/thys/Nominal2/Nominal2.thy b/thys/Nominal2/Nominal2.thy --- a/thys/Nominal2/Nominal2.thy +++ b/thys/Nominal2/Nominal2.thy @@ -1,752 +1,757 @@ theory Nominal2 imports Nominal2_Base Nominal2_Abs Nominal2_FCB keywords "nominal_datatype" :: thy_defn and "nominal_function" "nominal_inductive" "nominal_termination" :: thy_goal_defn and "avoids" "binds" begin ML_file \nominal_dt_data.ML\ ML \open Nominal_Dt_Data\ ML_file \nominal_dt_rawfuns.ML\ ML \open Nominal_Dt_RawFuns\ ML_file \nominal_dt_alpha.ML\ ML \open Nominal_Dt_Alpha\ ML_file \nominal_dt_quot.ML\ ML \open Nominal_Dt_Quot\ (*****************************************) (* setup for induction principles method *) ML_file \nominal_induct.ML\ method_setup nominal_induct = \NominalInduct.nominal_induct_method\ \nominal induction\ (****************************************************) (* inductive definition involving nominal datatypes *) ML_file \nominal_inductive.ML\ (***************************************) (* forked code of the function package *) (* for defining nominal functions *) ML_file \nominal_function_common.ML\ ML_file \nominal_function_core.ML\ ML_file \nominal_mutual.ML\ ML_file \nominal_function.ML\ ML_file \nominal_termination.ML\ ML \ val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) val simp_attr = Attrib.internal (K Simplifier.simp_add) val induct_attr = Attrib.internal (K Induct.induct_simp_add) \ section\Interface for \nominal_datatype\\ ML \ fun get_cnstrs dts = map snd dts fun get_typed_cnstrs dts = flat (map (fn ((bn, _, _), constrs) => (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) fun get_cnstr_strs dts = map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) fun get_bn_fun_strs bn_funs = map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs \ text \Infrastructure for adding \_raw\ to types and terms\ ML \ fun add_raw s = s ^ "_raw" fun add_raws ss = map add_raw ss fun raw_bind bn = Binding.suffix_name "_raw" bn fun replace_str ss s = case (AList.lookup (op =) ss s) of SOME s' => s' | NONE => s fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) | replace_typ ty_ss T = T fun raw_dts ty_ss dts = let fun raw_dts_aux1 (bind, tys, _) = (raw_bind bind, map (replace_typ ty_ss) tys, NoSyn) fun raw_dts_aux2 ((bind, ty_args, _), constrs) = ((raw_bind bind, ty_args, NoSyn), map raw_dts_aux1 constrs) in map raw_dts_aux2 dts end fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T) | replace_aterm trm_ss trm = trm fun replace_term trm_ss ty_ss trm = trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) \ ML \ fun rawify_dts dts dts_env = raw_dts dts_env dts \ ML \ fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = let val bn_funs' = map (fn (bn, ty, _) => (raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs val bn_eqs' = map (fn (attr, trm) => ((attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm), [], [])) bn_eqs in (bn_funs', bn_eqs') end \ ML \ fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses = let fun rawify_bnds bnds = map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys) in (map o map o map) rawify_bclause bclauses end \ ML \ (* definition of the raw datatype *) fun define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy = let val thy = Local_Theory.exit_global lthy val thy_name = Context.theory_name thy val dt_names = map (fn ((s, _, _), _) => Binding.name_of s) dts val dt_full_names = map (Long_Name.qualify thy_name) dt_names val dt_full_names' = add_raws dt_full_names val dts_env = dt_full_names ~~ dt_full_names' val cnstr_full_names = map (Long_Name.qualify thy_name) cnstr_names val cnstr_full_names' = map (fn (x, y) => Long_Name.qualify thy_name (Long_Name.qualify (add_raw x) (add_raw y))) cnstr_tys val cnstrs_env = cnstr_full_names ~~ cnstr_full_names' val bn_fun_strs = get_bn_fun_strs bn_funs val bn_fun_strs' = add_raws bn_fun_strs val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' val bn_fun_full_env = map (apply2 (Long_Name.qualify thy_name)) (bn_fun_strs ~~ bn_fun_strs') val raw_dts = rawify_dts dts dts_env val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses val (raw_full_dt_names', thy1) = BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Kill_Type_Args] raw_dts thy val lthy1 = Named_Target.theory_init thy1 val dtinfos = map (Old_Datatype_Data.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' val raw_fp_sugars = map (the o BNF_FP_Def_Sugar.fp_sugar_of lthy1) raw_full_dt_names' val {descr, ...} = hd dtinfos val raw_ty_args = hd (Old_Datatype_Aux.get_rec_types descr) |> snd o dest_Type |> map dest_TFree val raw_schematic_ty_args = (snd o dest_Type o #T o hd) raw_fp_sugars val typ_subst = raw_schematic_ty_args ~~ map TFree raw_ty_args val freezeT = Term.typ_subst_atomic typ_subst val freeze = Term.subst_atomic_types typ_subst val raw_tys = map (freezeT o #T) raw_fp_sugars val raw_cns_info = all_dtyp_constrs_types descr val raw_all_cns = map (map freeze o #ctrs o #ctr_sugar o #fp_ctr_sugar) raw_fp_sugars val raw_inject_thms = flat (map #inject dtinfos) val raw_distinct_thms = flat (map #distinct dtinfos) val raw_induct_thm = (hd o #common_co_inducts o the o #fp_co_induct_sugar o hd) raw_fp_sugars val raw_induct_thms = map (the_single o #co_inducts o the o #fp_co_induct_sugar) raw_fp_sugars val raw_exhaust_thms = map #exhaust dtinfos val raw_size_trms = map HOLogic.size_const raw_tys val raw_size_thms = these (Option.map (#2 o #2) (BNF_LFP_Size.size_of lthy1 (hd raw_full_dt_names'))) val raw_result = RawDtInfo {raw_dt_names = raw_full_dt_names', raw_fp_sugars = raw_fp_sugars, raw_dts = raw_dts, raw_tys = raw_tys, raw_ty_args = raw_ty_args, raw_cns_info = raw_cns_info, raw_all_cns = raw_all_cns, raw_inject_thms = raw_inject_thms, raw_distinct_thms = raw_distinct_thms, raw_induct_thm = raw_induct_thm, raw_induct_thms = raw_induct_thms, raw_exhaust_thms = raw_exhaust_thms, raw_size_trms = raw_size_trms, raw_size_thms = raw_size_thms} in (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_result, lthy1) end \ ML \ fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = let val cnstr_names = get_cnstr_strs dts val cnstr_tys = get_typed_cnstrs dts val _ = trace_msg (K "Defining raw datatypes...") val (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_dt_info, lthy0) = define_raw_dts dts cnstr_names cnstr_tys bn_funs bn_eqs bclauses lthy val RawDtInfo {raw_dt_names, raw_tys, raw_ty_args, raw_fp_sugars, raw_all_cns, raw_inject_thms, raw_distinct_thms, raw_induct_thm, raw_induct_thms, raw_exhaust_thms, raw_size_trms, raw_size_thms, ...} = raw_dt_info val _ = trace_msg (K "Defining raw permutations...") val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) = define_raw_perms raw_dt_info lthy0 (* noting the raw permutations as eqvt theorems *) val lthy3 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a) val _ = trace_msg (K "Defining raw fv- and bn-functions...") val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_inducts, lthy3a) = define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy3 (* defining the permute_bn functions *) val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = define_raw_bn_perms raw_dt_info raw_bn_info lthy3a val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3c) = define_raw_fvs raw_dt_info raw_bn_info raw_bclauses lthy3b val _ = trace_msg (K "Defining alpha relations...") val (alpha_result, lthy4) = define_raw_alpha raw_dt_info raw_bn_info raw_bclauses raw_fvs lthy3c val _ = trace_msg (K "Proving distinct theorems...") val alpha_distincts = raw_prove_alpha_distincts lthy4 alpha_result raw_dt_info val _ = trace_msg (K "Proving eq-iff theorems...") val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_dt_info val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...") val raw_bn_eqvt = raw_prove_eqvt raw_bns raw_bn_inducts (raw_bn_defs @ raw_perm_simps) lthy4 - (* noting the raw_bn_eqvt lemmas in a temprorary theory *) - val lthy_tmp = Local_Theory.subtarget - (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) #> snd) lthy4 + (* noting the raw_bn_eqvt lemmas in a temporary theory *) + val lthy_tmp = + lthy4 + |> Local_Theory.begin_nested + |> snd + |> Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) + |> snd + |> Local_Theory.end_nested val raw_fv_eqvt = raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) lthy_tmp val raw_size_eqvt = let val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info in raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) lthy_tmp |> map (rewrite_rule lthy_tmp @{thms permute_nat_def[THEN eq_reflection]}) |> map (fn thm => thm RS @{thm sym}) end val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) val alpha_eqvt = let val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result in Nominal_Eqvt.raw_equivariance lthy5 (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros end val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt val _ = trace_msg (K "Proving equivalence of alpha...") val alpha_refl_thms = raw_prove_refl lthy5 alpha_result raw_induct_thm val alpha_sym_thms = raw_prove_sym lthy5 alpha_result alpha_eqvt_norm val alpha_trans_thms = raw_prove_trans lthy5 alpha_result (raw_distinct_thms @ raw_inject_thms) alpha_eqvt_norm val (alpha_equivp_thms, alpha_bn_equivp_thms) = raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms val _ = trace_msg (K "Proving alpha implies bn...") val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result val _ = trace_msg (K "Proving respectfulness...") val raw_funs_rsp_aux = raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp lthy5) raw_funs_rsp_aux fun match_const cnst th = (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o Thm.prop_of) th = fst (dest_Const cnst); fun find_matching_rsp cnst = hd (filter (fn th => match_const cnst th) raw_funs_rsp); val raw_fv_rsp = map find_matching_rsp raw_fvs; val raw_bn_rsp = map find_matching_rsp raw_bns; val raw_fv_bn_rsp = map find_matching_rsp raw_fv_bns; val raw_size_rsp = raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |> map (mk_funs_rsp lthy5) val raw_constrs_rsp = raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) val alpha_permute_rsp = map (mk_alpha_permute_rsp lthy5) alpha_eqvt val alpha_bn_rsp = raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps val _ = trace_msg (K "Defining the quotient types...") val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts val (qty_infos, lthy7) = let val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result in define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy5 end val qtys = map #qtyp qty_infos val qty_full_names = map (fst o dest_Type) qtys val qty_names = map Long_Name.base_name qty_full_names val _ = trace_msg (K "Defining the quotient constants...") val qconstrs_descrs = (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp)) val qbns_descr = map2 (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) bn_funs (raw_bns ~~ raw_bn_rsp) val qfvs_descr = map2 (fn n => fn (t, th) => ("fv_" ^ n, t, NoSyn, th)) qty_names (raw_fvs ~~ raw_fv_rsp) val qfv_bns_descr = map2 (fn (b, _, _) => fn (t, th) => ("fv_" ^ Variable.check_name b, t, NoSyn, th)) bn_funs (raw_fv_bns ~~ raw_fv_bn_rsp) val qalpha_bns_descr = let val AlphaResult {alpha_bn_trms, ...} = alpha_result in map2 (fn (b, _, _) => fn (t, th) => ("alpha_" ^ Variable.check_name b, t, NoSyn, th)) bn_funs (alpha_bn_trms ~~ alpha_bn_rsp) end val qperm_descr = map2 (fn n => fn (t, th) => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, th)) qty_names (raw_perm_funs ~~ (take (length raw_perm_funs) alpha_permute_rsp)) val qsize_descr = map2 (fn n => fn (t, th) => ("size_" ^ n, t, NoSyn, th)) qty_names (raw_size_trms ~~ (take (length raw_size_trms) raw_size_rsp)) val qperm_bn_descr = map2 (fn (b, _, _) => fn (t, th) => ("permute_" ^ Variable.check_name b, t, NoSyn, th)) bn_funs (raw_perm_bns ~~ raw_perm_bn_rsp) val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8) = lthy7 |> fold_map (define_qconsts qtys) qconstrs_descrs ||>> define_qconsts qtys qbns_descr ||>> define_qconsts qtys qfvs_descr ||>> define_qconsts qtys qfv_bns_descr ||>> define_qconsts qtys qalpha_bns_descr ||>> define_qconsts qtys qperm_bn_descr val lthy9 = define_qperms qtys qty_full_names raw_ty_args qperm_descr raw_perm_laws lthy8 val lthy9a = define_qsizes qtys qty_full_names raw_ty_args qsize_descr lthy9 val qtrms = (map o map) #qconst qconstrs_infos val qbns = map #qconst qbns_info val qfvs = map #qconst qfvs_info val qfv_bns = map #qconst qfv_bns_info val qalpha_bns = map #qconst qalpha_bns_info val qperm_bns = map #qconst qperm_bns_info val _ = trace_msg (K "Lifting of theorems...") val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_sel prod.case} val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = lthy9a |>>> lift_thms qtys [] alpha_distincts ||>>> lift_thms qtys eq_iff_simps alpha_eq_iff ||>>> lift_thms qtys [] raw_fv_defs ||>>> lift_thms qtys [] raw_bn_defs ||>>> lift_thms qtys [] raw_perm_simps ||>>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) ||>>> lift_thms qtys [] raw_bn_inducts ||>>> lift_thms qtys [] raw_size_eqvt ||>>> lift_thms qtys [] [raw_induct_thm] ||>>> lift_thms qtys [] raw_exhaust_thms ||>>> lift_thms qtys [] raw_size_thms ||>>> lift_thms qtys [] raw_perm_bn_simps ||>>> lift_thms qtys [] alpha_refl_thms ||>>> lift_thms qtys [] alpha_sym_thms ||>>> lift_thms qtys [] alpha_trans_thms val qinducts = Project_Rule.projections lthyB qinduct val _ = trace_msg (K "Proving supp lemmas and fs-instances...") val qsupports_thms = prove_supports lthyB qperm_simps (flat qtrms) (* finite supp lemmas *) val qfsupp_thms = prove_fsupp lthyB qtys qinduct qsupports_thms (* fs instances *) val lthyC = fs_instance qtys qty_full_names raw_ty_args qfsupp_thms lthyB val _ = trace_msg (K "Proving equality between fv and supp...") val qfv_supp_thms = prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC |> map Drule.eta_contraction_rule (* postprocessing of eq and fv theorems *) val qeq_iffs' = qeq_iffs |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps qfv_supp_thms)) |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]})) (* filters the theorems that are of the form "qfv = supp" *) val qfv_names = map (fst o dest_Const) qfvs fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Const (lhs, _) $ _)) = member (op =) qfv_names lhs | is_qfv_thm _ = false val qsupp_constrs = qfv_defs |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps (filter (is_qfv_thm o Thm.prop_of) qfv_supp_thms))) val transform_thm = @{lemma "x = y \ a \ x \ a \ y" by simp} val transform_thms = [ @{lemma "a \ (S \ T) \ a \ S \ a \ T" by simp}, @{lemma "a \ (S - T) \ a \ S \ a \ T" by simp}, @{lemma "(lhs = (a \ {})) \ lhs" by simp}, @{thm fresh_def[symmetric]}] val qfresh_constrs = qsupp_constrs |> map (fn thm => thm RS transform_thm) |> map (simplify (put_simpset HOL_basic_ss lthyC addsimps transform_thms)) (* proving that the qbn result is finite *) val qbn_finite_thms = prove_bns_finite qtys qbns qinduct qbn_defs lthyC (* proving that perm_bns preserve alpha *) val qperm_bn_alpha_thms = prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' qalpha_refl_thms lthyC (* proving the relationship of bn and permute_bn *) val qpermute_bn_thms = prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC val _ = trace_msg (K "Proving strong exhaust lemmas...") val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs' qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms val _ = trace_msg (K "Proving strong induct lemmas...") val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses (* noting the theorems *) (* generating the prefix for the theorem names *) val thms_name = the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name fun thms_suffix s = Binding.qualify_name true thms_name s val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms val (_, lthy9') = lthyC |> Local_Theory.declaration {syntax = false, pervasive = false} (K (fold register_info infos)) |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs') ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) ||>> Local_Theory.note ((thms_suffix "bn_inducts", []), qbn_inducts) ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", [eqvt_attr]), qfv_qbn_eqvts) ||>> Local_Theory.note ((thms_suffix "size", [simp_attr]), qsize_simps) ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct]) ||>> Local_Theory.note ((thms_suffix "inducts", [case_names_attr]), qinducts) ||>> Local_Theory.note ((thms_suffix "exhaust", [case_names_attr]), qexhausts) ||>> Local_Theory.note ((thms_suffix "strong_exhaust", [case_names_attr]), qstrong_exhaust_thms) ||>> Local_Theory.note ((thms_suffix "strong_induct", [case_names_attr]), qstrong_induct_thms) ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms) ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms) ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs) ||>> Local_Theory.note ((thms_suffix "fresh", [simp_attr]), qfresh_constrs) ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) ||>> Local_Theory.note ((thms_suffix "alpha_refl", []), qalpha_refl_thms) ||>> Local_Theory.note ((thms_suffix "alpha_sym", []), qalpha_sym_thms) ||>> Local_Theory.note ((thms_suffix "alpha_trans", []), qalpha_trans_thms) in lthy9' end \ section \Preparing and parsing of the specification\ ML \ (* adds the default sort @{sort fs} to nominal specifications *) fun augment_sort thy S = Sign.inter_sort thy (@{sort fs}, S) fun augment_sort_typ thy = map_type_tfree (fn (s, S) => TFree (s, augment_sort thy S)) \ ML \ (* generates the parsed datatypes and declares the constructors *) fun prepare_dts dt_strs thy = let fun prep_spec ((tname, tvs, mx), constrs) = ((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx'))) val (dts, spec_ctxt) = Old_Datatype.read_specs (map prep_spec dt_strs) thy fun augment ((tname, tvs, mx), constrs) = ((tname, map (apsnd (augment_sort thy)) tvs, mx), constrs |> map (fn (c, tys, mx') => (c, map (augment_sort_typ thy) tys, mx'))) val dts' = map augment dts fun mk_constr_trms ((tname, tvs, _), constrs) = let val ty = Type (Sign.full_name thy tname, map TFree tvs) in map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs end val constr_trms = flat (map mk_constr_trms dts') (* FIXME: local version *) (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *) val thy' = Sign.add_consts constr_trms (Proof_Context.theory_of spec_ctxt) in (dts', thy') end \ ML \ (* parsing the binding function specifications and *) (* declaring the function constants *) fun prepare_bn_funs bn_fun_strs bn_eq_strs thy = let val lthy = Named_Target.theory_init thy val ((bn_funs, bn_eqs), lthy') = Specification.read_multi_specs bn_fun_strs bn_eq_strs lthy fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) val bn_funs' = map prep_bn_fun bn_funs in (Local_Theory.exit_global lthy') |> Sign.add_consts bn_funs' |> pair (bn_funs', bn_eqs) end \ text \associates every SOME with the index in the list; drops NONEs\ ML \ fun indexify xs = let fun mapp _ [] = [] | mapp i (NONE :: xs) = mapp (i + 1) xs | mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs in mapp 0 xs end fun index_lookup xs x = case AList.lookup ((=)) xs x of SOME x => x | NONE => error ("Cannot find " ^ x ^ " as argument annotation."); \ ML \ fun prepare_bclauses dt_strs thy = let val annos_bclauses = get_cnstrs dt_strs |> (map o map) (fn (_, antys, _, bns) => (map fst antys, bns)) fun prep_binder env bn_str = case (Syntax.read_term_global thy bn_str) of Free (x, _) => (NONE, index_lookup env x) | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") fun prep_body env bn_str = index_lookup env bn_str fun prep_bclause env (mode, binders, bodies) = let val binders' = map (prep_binder env) binders val bodies' = map (prep_body env) bodies in BC (mode, binders', bodies') end fun prep_bclauses (annos, bclause_strs) = let val env = indexify annos (* for every label, associate the index *) in map (prep_bclause env) bclause_strs end in ((map o map) prep_bclauses annos_bclauses, thy) end \ text \ adds an empty binding clause for every argument that is not already part of a binding clause \ ML \ fun included i bcs = let fun incl (BC (_, bns, bds)) = member (op =) (map snd bns) i orelse member (=) bds i in exists incl bcs end \ ML \ fun complete dt_strs bclauses = let val args = get_cnstrs dt_strs |> (map o map) (fn (_, antys, _, _) => length antys) fun complt n bcs = let fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) in bcs @ (flat (map_range (add bcs) n)) end in (map2 o map2) complt args bclauses end \ ML \ fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = let (* this theory is used just for parsing *) val thy = Proof_Context.theory_of lthy val (((dts, (bn_funs, bn_eqs)), bclauses), _) = thy |> prepare_dts dt_strs ||>> prepare_bn_funs bn_fun_strs bn_eq_strs ||>> prepare_bclauses dt_strs val bclauses' = complete dt_strs bclauses in nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy end \ ML \ (* nominal datatype parser *) local fun triple1 ((x, y), z) = (x, y, z) fun triple2 ((x, y), z) = (y, x, z) fun tuple2 (((x, y), z), u) = (x, y, u, z) fun tuple3 ((x, y), (z, u)) = (x, y, z, u) in val opt_name = Scan.option (Parse.binding --| Args.colon) val anno_typ = Scan.option (Parse.name --| @{keyword "::"}) -- Parse.typ val bind_mode = @{keyword "binds"} |-- Scan.optional (Args.parens (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst val bind_clauses = Parse.enum "," (bind_mode -- Scan.repeat1 Parse.term -- (@{keyword "in"} |-- Scan.repeat1 Parse.name) >> triple1) val cnstr_parser = Parse.binding -- Scan.repeat anno_typ -- bind_clauses -- Parse.opt_mixfix >> tuple2 (* datatype parser *) val dt_parser = (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix >> triple2) -- (@{keyword "="} |-- Parse.enum1 "|" cnstr_parser) (* binding function parser *) val bnfun_parser = Scan.optional (@{keyword "binder"} |-- Parse_Spec.specification) ([], []) (* main parser *) val main_parser = opt_name -- Parse.and_list1 dt_parser -- bnfun_parser >> tuple3 end (* Command Keyword *) val _ = Outer_Syntax.local_theory @{command_keyword nominal_datatype} "declaration of nominal datatypes" (main_parser >> nominal_datatype2_cmd) \ end diff --git a/thys/Nominal2/nominal_dt_alpha.ML b/thys/Nominal2/nominal_dt_alpha.ML --- a/thys/Nominal2/nominal_dt_alpha.ML +++ b/thys/Nominal2/nominal_dt_alpha.ML @@ -1,875 +1,878 @@ (* Title: nominal_dt_alpha.ML Author: Cezary Kaliszyk Author: Christian Urban Definitions and proofs for the alpha-relations. *) signature NOMINAL_DT_ALPHA = sig val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list -> Proof.context -> alpha_result * local_theory val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> thm list * thm list val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> thm list -> thm list val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list val mk_funs_rsp: Proof.context -> thm -> thm val mk_alpha_permute_rsp: Proof.context -> thm -> thm end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = struct open Nominal_Permeq open Nominal_Dt_Data fun lookup xs x = the (AList.lookup (op=) xs x) fun group xs = AList.group (op=) xs (** definition of the inductive rules for alpha and alpha_bn **) (* construct the compound terms for prod_fv and prod_alpha *) fun mk_prod_fv (t1, t2) = let val ty1 = fastype_of t1 val ty2 = fastype_of t2 val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"} in Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2 end fun mk_prod_alpha (t1, t2) = let val ty1 = fastype_of t1 val ty2 = fastype_of t2 val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) val resT = [prodT, prodT] ---> @{typ "bool"} in Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 end (* generates the compound binder terms *) fun comb_binders lthy bmode args binders = let fun bind_set lthy args (NONE, i) = setify lthy (nth args i) | bind_set _ args (SOME bn, i) = bn $ (nth args i) fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) | bind_lst _ args (SOME bn, i) = bn $ (nth args i) val (combine_fn, bind_fn) = case bmode of Lst => (mk_append, bind_lst) | Set => (mk_union, bind_set) | Res => (mk_union, bind_set) in binders |> map (bind_fn lthy args) |> foldl1 combine_fn end (* produces the term for an alpha with abstraction *) fun mk_alpha_term bmode fv alpha args args' binders binders' = let val (alpha_name, binder_ty) = case bmode of Lst => (@{const_name "alpha_lst"}, @{typ "atom list"}) | Set => (@{const_name "alpha_set"}, @{typ "atom set"}) | Res => (@{const_name "alpha_res"}, @{typ "atom set"}) val ty = fastype_of args val pair_ty = HOLogic.mk_prodT (binder_ty, ty) val alpha_ty = [ty, ty] ---> @{typ "bool"} val fv_ty = ty --> @{typ "atom set"} val pair_lhs = HOLogic.mk_prod (binders, args) val pair_rhs = HOLogic.mk_prod (binders', args') in HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs) end (* for non-recursive binders we have to produce alpha_bn premises *) fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = case binder of (NONE, _) => [] | (SOME bn, i) => if member (op=) bodies i then [] else [lookup alpha_bn_map bn $ nth args i $ nth args' i] (* generate the premises for an alpha rule; mk_frees is used if no binders are present *) fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = let fun mk_frees i = let val arg = nth args i val arg' = nth args' i val ty = fastype_of arg in if nth is_rec i then fst (lookup alpha_map ty) $ arg $ arg' else HOLogic.mk_eq (arg, arg') end fun mk_alpha_fv i = let val ty = fastype_of (nth args i) in case AList.lookup (op=) alpha_map ty of NONE => (HOLogic.eq_const ty, supp_const ty) | SOME (alpha, fv) => (alpha, fv) end in case bclause of BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies | BC (bmode, binders, bodies) => let val (alphas, fvs) = split_list (map mk_alpha_fv bodies) val comp_fv = foldl1 mk_prod_fv fvs val comp_alpha = foldl1 mk_prod_alpha alphas val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) val comp_binders = comb_binders lthy bmode args binders val comp_binders' = comb_binders lthy bmode args' binders val alpha_prem = mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) in map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems) end end (* produces the introduction rule for an alpha rule *) fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) val alpha = fst (lookup alpha_map ty) val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses in Library.foldr Logic.mk_implies (flat prems, concl) end (* produces the premise of an alpha-bn rule; we only need to treat the case special where the binding clause is empty; - if the body is not included in the bn_info, then we either produce an equation or an alpha-premise - if the body is included in the bn_info, then we create either a recursive call to alpha-bn, or no premise *) fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause = let fun mk_alpha_bn_prem i = let val arg = nth args i val arg' = nth args' i val ty = fastype_of arg in case AList.lookup (op=) bn_args i of NONE => (case (AList.lookup (op=) alpha_map ty) of NONE => [HOLogic.mk_eq (arg, arg')] | SOME (alpha, _) => [alpha $ arg $ arg']) | SOME (NONE) => [] | SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg'] end in case bclause of BC (_, [], bodies) => map HOLogic.mk_Trueprop (flat (map mk_alpha_bn_prem bodies)) | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause end fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) val alpha_bn = lookup alpha_bn_map bn_trm val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses in Library.foldr Logic.mk_implies (flat prems, concl) end fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let val nth_constrs_info = nth constrs_info bn_n val nth_bclausess = nth bclausesss bn_n in map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy = let val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_names val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys val alpha_frees = map Free (alpha_names ~~ alpha_tys) val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs) val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val alpha_bn_names = map (prefix "alpha_") bn_names val alpha_bn_arg_tys = map (nth raw_tys) bn_tys val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) val alpha_bn_map = bns ~~ alpha_bn_frees val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) val all_alpha_intros = map (pair Binding.empty_atts) (flat alpha_intros @ flat alpha_bn_intros) - val (alpha_info, lthy') = lthy - |> Local_Theory.subtarget_result Inductive.transform_result - (Inductive.add_inductive + val (alpha_info, lthy') = + lthy + |> Local_Theory.begin_nested + |> snd + |> Inductive.add_inductive {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false} - all_alpha_names [] all_alpha_intros []) + all_alpha_names [] all_alpha_intros [] + |> Local_Theory.end_nested_result Inductive.transform_result; val phi = Proof_Context.export_morphism lthy' (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy); val alpha_info_global = Inductive.transform_result phi alpha_info; val all_alpha_trms = #preds alpha_info_global |> map Type.legacy_freeze (*FIXME*) val alpha_raw_induct = #raw_induct alpha_info_global val alpha_intros = #intrs alpha_info_global; val alpha_cases = #elims alpha_info_global; val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms val alpha_tys = map (domain_type o fastype_of) alpha_trms val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms val alpha_names = map (fst o dest_Const) alpha_trms val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms in (AlphaResult {alpha_names = alpha_names, alpha_trms = alpha_trms, alpha_tys = alpha_tys, alpha_bn_names = alpha_bn_names, alpha_bn_trms = alpha_bn_trms, alpha_bn_tys = alpha_bn_tys, alpha_intros = alpha_intros, alpha_cases = alpha_cases, alpha_raw_induct = alpha_raw_induct}, lthy') end (** induction proofs **) (* proof by structural induction over data types *) fun induct_prove tys props induct_thm cases_tac ctxt = let val (arg_names, ctxt') = Variable.variant_fixes (replicate (length tys) "x") ctxt val args = map2 (curry Free) arg_names tys val true_trms = replicate (length tys) (K @{term True}) fun apply_all x fs = map (fn f => f x) fs val goals = group (props @ (tys ~~ true_trms)) |> map snd |> map2 apply_all args |> map fold_conj |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop fun tac ctxt = HEADGOAL (DETERM o (resolve_tac ctxt [induct_thm]) THEN_ALL_NEW (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt]))) in Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map Old_Datatype_Aux.split_conj_thm |> flat |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end (* proof by rule induction over the alpha-definitions *) fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt = let val arg_tys = map (domain_type o fastype_of) alphas val ((arg_names1, arg_names2), ctxt') = ctxt |> Variable.variant_fixes (replicate (length alphas) "x") ||>> Variable.variant_fixes (replicate (length alphas) "y") val args1 = map2 (curry Free) arg_names1 arg_tys val args2 = map2 (curry Free) arg_names2 arg_tys val true_trms = replicate (length alphas) (K @{term True}) fun apply_all x fs = map (fn f => f x) fs val goals_rhs = group (props @ (alphas ~~ true_trms)) |> map snd |> map2 apply_all (args1 ~~ args2) |> map fold_conj fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2 val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2) val goals = (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs) |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop fun tac ctxt = HEADGOAL (DETERM o (resolve_tac ctxt [alpha_induct_thm]) THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt]) in Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map (fn th => th RS mp) |> map Old_Datatype_Aux.split_conj_thm |> flat |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end (** produces the distinctness theorems **) (* transforms the distinctness theorems of the constructors into "not-alphas" of the constructors *) fun mk_distinct_goal ty_trm_assoc neq = let val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = HOLogic.dest_not (HOLogic.dest_Trueprop neq) val ty_str = fst (dest_Type (domain_type ty_eq)) in Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |> HOLogic.mk_not |> HOLogic.mk_Trueprop end fun distinct_tac ctxt cases_thms distinct_thms = resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info val ty_trm_assoc = raw_dt_names ~~ alpha_names fun mk_alpha_distinct raw_distinct_trm = let val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm in Goal.prove ctxt [] [] goal (K (distinct_tac ctxt alpha_cases raw_distinct_thms 1)) end in map (mk_alpha_distinct o Thm.prop_of) raw_distinct_thms end (** produces the alpha_eq_iff simplification rules **) (* in case a theorem is of the form (Rel Const Const), it will be rewritten to ((Rel Const = Const) = True) *) fun mk_simp_rule thm = case Thm.prop_of thm of @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} | _ => thm fun alpha_eq_iff_tac ctxt dist_inj intros elims = SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' (resolve_tac ctxt @{thms iffI} THEN' RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) fun mk_alpha_eq_iff_goal thm = let val prop = Thm.prop_of thm; val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); fun list_conj l = foldr1 HOLogic.mk_conj l; in if hyps = [] then HOLogic.mk_Trueprop concl else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) end; fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; val goals = map mk_alpha_eq_iff_goal thms_imp; val tac = alpha_eq_iff_tac ctxt (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; in Variable.export ctxt' ctxt thms |> map mk_simp_rule end (** reflexivity proof for the alphas **) val exi_zero = @{lemma "P (0::perm) \ (\x. P x)" by auto} fun cases_tac intros ctxt = let val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv} val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt val bound_tac = EVERY' [ resolve_tac ctxt [exi_zero], resolve_tac ctxt @{thms alpha_refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] in resolve_tac ctxt intros THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac] end fun raw_prove_refl ctxt alpha_result raw_dt_induct = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} = alpha_result val props = map (fn (ty, c) => (ty, fn x => c $ x $ x)) ((alpha_tys ~~ alpha_trms) @ (alpha_bn_tys ~~ alpha_bn_trms)) in induct_prove alpha_tys props raw_dt_induct (cases_tac alpha_intros) ctxt end (** symmetry proof for the alphas **) val exi_neg = @{lemma "(\(p::perm). P p) \ (\q. P q \ Q (- q)) \ \p. Q p" by (erule exE, rule_tac x="-p" in exI, auto)} (* for premises that contain binders *) fun prem_bound_tac pred_names alpha_eqvt ctxt = let fun trans_prem_tac pred_names ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val prems' = map (transform_prem1 ctxt' pred_names) prems in resolve_tac ctxt' prems' 1 end) ctxt val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas} in EVERY' [ eresolve_tac ctxt [exi_neg], resolve_tac ctxt @{thms alpha_sym_eqvt}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' resolve_tac ctxt @{thms refl}, trans_prem_tac pred_names ctxt] end fun raw_prove_sym ctxt alpha_result alpha_eqvt = let val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, alpha_intros, alpha_raw_induct, ...} = alpha_result val alpha_trms = alpha_trms @ alpha_bn_trms val alpha_names = alpha_names @ alpha_bn_names val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms fun tac ctxt = resolve_tac ctxt alpha_intros THEN_ALL_NEW FIRST' [assume_tac ctxt, resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt, prem_bound_tac alpha_names alpha_eqvt ctxt] in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt end (** transitivity proof for alphas **) (* applies cases rules and resolves them with the last premise *) fun ecases_tac cases = Subgoal.FOCUS (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems])) fun aatac pred_names = SUBPROOF (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems))) (* instantiates exI with the permutation p + q *) val perm_inst_tac = Subgoal.FOCUS (fn {context = ctxt, params, ...} => let val (p, q) = apply2 snd (last2 params) val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q] val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} in HEADGOAL (resolve_tac ctxt [exi_inst]) end) fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = let val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv} in resolve_tac ctxt intros THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' TRY o EVERY' (* if binders are present *) [ eresolve_tac ctxt @{thms exE}, eresolve_tac ctxt @{thms exE}, perm_inst_tac ctxt, resolve_tac ctxt @{thms alpha_trans_eqvt}, assume_tac ctxt, aatac pred_names ctxt, eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' resolve_tac ctxt @{thms refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) end fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result val alpha_names = alpha_names @ alpha_bn_names fun all_cases ctxt = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt in EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms impI}, ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] end fun prep_trans_goal alpha_trm (arg1, arg2) = let val arg_ty = fastype_of arg1 val mid = alpha_trm $ arg2 $ (Bound 0) val rhs = alpha_trm $ arg1 $ (Bound 0) in HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) end fun raw_prove_trans ctxt alpha_result raw_dt_thms alpha_eqvt = let - val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, + val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val alpha_trms = alpha_trms @ alpha_bn_trms val props = map prep_trans_goal alpha_trms in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct (prove_trans_tac alpha_result raw_dt_thms alpha_eqvt) ctxt end (** proves the equivp predicate for all alphas **) val reflp_def' = @{lemma "reflp R == \x. R x x" by (simp add: reflp_def refl_on_def)} val symp_def' = @{lemma "symp R \ \x y . R x y --> R y x" by (simp add: symp_def sym_def)} val transp_def' = @{lemma "transp R \ \x y. R x y \ (\z. R y z \ R x z)" by (rule eq_reflection, auto simp add: trans_def transp_def)} fun raw_prove_equivp ctxt alpha_result refl symm trans = let val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result val refl' = map (fold_rule ctxt [reflp_def'] o atomize ctxt) refl val symm' = map (fold_rule ctxt [symp_def'] o atomize ctxt) symm val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans fun prep_goal t = HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) in Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN' RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans'])))) |> chop (length alpha_trms) end (* proves that alpha_raw implies alpha_bn *) fun raw_prove_bn_imp_tac alpha_result ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 ctxt' alpha_names) prems' in HEADGOAL (REPEAT_ALL_NEW (FIRST' [ resolve_tac ctxt' @{thms TrueI}, resolve_tac ctxt' @{thms conjI}, resolve_tac ctxt' prems', resolve_tac ctxt' prems'', resolve_tac ctxt' alpha_intros ])) end) ctxt fun raw_prove_bn_imp ctxt alpha_result = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val arg_ty = domain_type o fastype_of val ty_assoc = alpha_tys ~~ alpha_trms val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (raw_prove_bn_imp_tac alpha_result) ctxt end (* respectfulness for fv_raw / bn_raw *) fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val arg_ty = domain_type o fastype_of val ty_assoc = alpha_tys ~~ alpha_trms fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns val simpset = put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set_simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) in alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct (K (asm_full_simp_tac simpset)) ctxt end (* respectfulness for size *) fun raw_size_rsp_aux ctxt alpha_result simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = alpha_result fun mk_prop ty (x, y) = HOLogic.mk_eq (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) val simpset = put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv permute_prod_def prod.case prod.rec}) val tac = (TRY o REPEAT o eresolve_tac ctxt @{thms exE}) THEN' asm_full_simp_tac simpset in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt end (* respectfulness for constructors *) fun raw_constr_rsp_tac ctxt alpha_intros simps = let val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def} val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_conv prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps in asm_full_simp_tac pre_simpset THEN' REPEAT o (resolve_tac ctxt @{thms allI impI}) THEN' resolve_tac ctxt alpha_intros THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset) end fun raw_constrs_rsp ctxt alpha_result constrs simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result fun lookup ty = case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of NONE => HOLogic.eq_const ty | SOME alpha => alpha fun rel_fun_app (t1, t2) = Const (@{const_name "rel_fun"}, dummyT) $ t1 $ t2 fun prep_goal trm = trm |> strip_type o fastype_of |> (fn (tys, ty) => tys @ [ty]) |> map lookup |> foldr1 rel_fun_app |> (fn t => t $ trm $ trm) |> Syntax.check_term ctxt |> HOLogic.mk_Trueprop in map (fn constrs => Goal.prove_common ctxt NONE [] [] (map prep_goal constrs) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs end (* rsp lemmas for alpha_bn relations *) val rsp_equivp = @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> (=)) Q Q" by (simp only: rel_fun_def equivp_def, metis)} (* we have to reorder the alpha_bn_imps theorems in order to be in order with alpha_bn_trms *) fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps = let val AlphaResult {alpha_bn_trms, ...} = alpha_result fun mk_map thm = thm |> `Thm.prop_of |>> List.last o snd o strip_comb |>> HOLogic.dest_Trueprop |>> head_of |>> fst o dest_Const val alpha_bn_imps' = map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms fun mk_thm thm1 thm2 = (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) in map2 mk_thm alpha_bn_equivp alpha_bn_imps' end (* rsp for permute_bn functions *) val perm_bn_rsp = @{lemma "(\x y p. R x y \ R (f p x) (f p y)) \ ((=) ===> R ===> R) f f" by (simp add: rel_fun_def)} fun raw_prove_perm_bn_tac alpha_result simps ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems' in HEADGOAL (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems')) THEN' TRY o REPEAT_ALL_NEW (FIRST' [ resolve_tac ctxt' @{thms TrueI}, resolve_tac ctxt' @{thms conjI}, resolve_tac ctxt' @{thms refl}, resolve_tac ctxt' prems', resolve_tac ctxt' prems'', resolve_tac ctxt' alpha_intros ])) end) ctxt fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = alpha_result val perm_bn_ty = range_type o range_type o fastype_of val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms) val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) fun mk_prop t = let val alpha_trm = lookup ty_assoc (perm_bn_ty t) in (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y)) end val goals = map mk_prop perm_bns in alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct (raw_prove_perm_bn_tac alpha_result simps) ctxt |> Proof_Context.export ctxt' ctxt |> map (atomize ctxt) |> map single |> map (curry (op OF) perm_bn_rsp) end (* transformation of the natural rsp-lemmas into standard form *) val fun_rsp = @{lemma "(\x y. R x y \ f x = f y) \ (R ===> (=)) f f" by (simp add: rel_fun_def)} fun mk_funs_rsp ctxt thm = thm |> atomize ctxt |> single |> curry (op OF) fun_rsp val permute_rsp = @{lemma "(\x y p. R x y \ R (permute p x) (permute p y)) ==> ((=) ===> R ===> R) permute permute" by (simp add: rel_fun_def)} fun mk_alpha_permute_rsp ctxt thm = thm |> atomize ctxt |> single |> curry (op OF) permute_rsp end (* structure *) diff --git a/thys/Nominal2/nominal_dt_rawfuns.ML b/thys/Nominal2/nominal_dt_rawfuns.ML --- a/thys/Nominal2/nominal_dt_rawfuns.ML +++ b/thys/Nominal2/nominal_dt_rawfuns.ML @@ -1,542 +1,557 @@ (* Title: nominal_dt_rawfuns.ML Author: Cezary Kaliszyk Author: Christian Urban Definitions of the raw fv, fv_bn and permute functions. *) signature NOMINAL_DT_RAWFUNS = sig val get_all_binders: bclause list -> (term option * int) list val is_recursive_binder: bclause -> bool val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> Specification.multi_specs -> local_theory -> (term list * thm list * bn_info list * thm list * local_theory) val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> Proof.context -> term list * term list * thm list * thm list * local_theory val define_raw_bn_perms: raw_dt_info -> bn_info list -> local_theory -> (term list * thm list * local_theory) val define_raw_perms: raw_dt_info -> local_theory -> (term list * thm list * thm list) * local_theory val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list end structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = struct open Nominal_Permeq fun get_all_binders bclauses = bclauses |> map (fn (BC (_, binders, _)) => binders) |> flat |> remove_dups (op =) fun is_recursive_binder (BC (_, binders, bodies)) = case (inter (op =) (map snd binders) bodies) of nil => false | _ => true fun lookup xs x = the (AList.lookup (op=) xs x) (** functions that define the raw binding functions **) (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or appends of elements; in case of recursive calls it returns also the applied bn function *) fun strip_bn_fun ctxt args t = let fun aux t = case t of Const (@{const_name sup}, _) $ l $ r => aux l @ aux r | Const (@{const_name append}, _) $ l $ r => aux l @ aux r | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => (find_index (equal x) args, NONE) :: aux y | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y => (find_index (equal x) args, NONE) :: aux y | Const (@{const_name bot}, _) => [] | Const (@{const_name Nil}, _) => [] | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term ctxt t)) in aux t end (** definition of the raw binding functions **) fun prep_bn_info ctxt dt_names dts bn_funs eqs = let fun process_eq eq = let val (lhs, rhs) = eq |> HOLogic.dest_Trueprop |> HOLogic.dest_eq val (bn_fun, [cnstr]) = strip_comb lhs val (_, ty) = dest_Const bn_fun val (ty_name, _) = dest_Type (domain_type ty) val dt_index = find_index (fn x => x = ty_name) dt_names val (cnstr_head, cnstr_args) = strip_comb cnstr val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) val rhs_elements = strip_bn_fun ctxt cnstr_args rhs in ((bn_fun, dt_index), (cnstr_name, rhs_elements)) end (* order according to constructor names *) fun cntrs_order ((bn, dt_index), data) = let val dt = nth dts dt_index val cts = snd dt val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts in (bn, (bn, dt_index, order (op=) ct_names data)) end in eqs |> map process_eq |> AList.group (op=) (* eqs grouped according to bn_functions *) |> map cntrs_order (* inner data ordered according to constructors *) |> order (op=) bn_funs (* ordered according to bn_functions *) end fun define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy = if null raw_bn_funs then ([], [], [], [], lthy) else let val RawDtInfo {raw_dt_names, raw_dts, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info - val lthy1 = Local_Theory.subtarget (Function.add_function raw_bn_funs raw_bn_eqs - Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) - #> snd) lthy; + val lthy1 = + lthy + |> Local_Theory.begin_nested + |> snd + |> Function.add_function raw_bn_funs raw_bn_eqs + Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) + |> snd + |> Local_Theory.end_nested; val ({fs, simps, inducts, ...}, lthy2) = prove_termination_fun raw_size_thms lthy1 val raw_bn_induct = the inducts val raw_bn_eqs = the simps val raw_bn_info = prep_bn_info lthy raw_dt_names raw_dts fs (map Thm.prop_of raw_bn_eqs) in (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) end (** functions that construct the equations for fv and fv_bn **) fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = let fun mk_fv_body i = let val arg = nth args i val ty = fastype_of arg in case AList.lookup (op=) fv_map ty of NONE => mk_supp arg | SOME fv => fv $ arg end fun bind_set (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"}) | bind_set (SOME bn, i) = (bn $ (nth args i), if member (op=) bodies i then @{term "{}::atom set"} else lookup fv_bn_map bn $ (nth args i)) fun bind_lst (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"}) | bind_lst (SOME bn, i) = (bn $ (nth args i), if member (op=) bodies i then @{term "[]::atom list"} else lookup fv_bn_map bn $ (nth args i)) val (combine_fn, bind_fn) = case bmode of Lst => (fold_append, bind_lst) | Set => (fold_union, bind_set) | Res => (fold_union, bind_set) val t1 = map mk_fv_body bodies val (t2, t3) = binders |> map bind_fn |> split_list |> apply2 combine_fn in mk_union (mk_diff (fold_union t1, to_set t2), to_set t3) end (* in case of fv_bn we have to treat the case special, where an "empty" binding clause is given *) fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = let fun mk_fv_bn_body i = let val arg = nth args i val ty = fastype_of arg in case AList.lookup (op=) bn_args i of NONE => (case (AList.lookup (op=) fv_map ty) of NONE => mk_supp arg | SOME fv => fv $ arg) | SOME (NONE) => @{term "{}::atom set"} | SOME (SOME bn) => lookup fv_bn_map bn $ arg end in case bclause of BC (_, [], bodies) => fold_union (map mk_fv_bn_body bodies) | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause end fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val fv = lookup fv_map ty val lhs = fv $ list_comb (constr, args) val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses val rhs = fold_union rhs_trms in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val fv_bn = lookup fv_bn_map bn_trm val lhs = fv_bn $ list_comb (constr, args) val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses val rhs = fold_union rhs_trms in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let val nth_constrs_info = nth constrs_info bn_n val nth_bclausess = nth bclausesss bn_n in map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end fun define_raw_fvs raw_dt_info bn_info bclausesss lthy = let val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_dt_names val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys val fv_frees = map Free (fv_names ~~ fv_tys); val fv_map = raw_tys ~~ fv_frees val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val fv_bn_names = map (prefix "fv_") bn_names val fv_bn_arg_tys = map (nth raw_tys) bn_tys val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) val fv_bn_map = bns ~~ fv_bn_frees val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) raw_cns_info bclausesss val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_cns_info bclausesss) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat fv_eqs @ flat fv_bn_eqs) - val lthy' = Local_Theory.subtarget (Function.add_function all_fun_names all_fun_eqs - Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) - #> snd) lthy + val lthy' = + lthy + |> Local_Theory.begin_nested + |> snd + |> Function.add_function all_fun_names all_fun_eqs + Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) + |> snd + |> Local_Theory.end_nested; val ({fs, simps, inducts, ...}, lthy'') = prove_termination_fun raw_size_thms lthy' val morphism = Proof_Context.export_morphism lthy'' (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy) val simps_exp = map (Morphism.thm morphism) (the simps) val inducts_exp = map (Morphism.thm morphism) (the inducts) val (fvs', fv_bns') = chop (length fv_frees) fs (* grafting the types so that they coincide with the input into the function package *) val fvs'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fvs' fv_tys val fv_bns'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fv_bns' fv_bn_tys in (fvs'', fv_bns'', simps_exp, inducts_exp, lthy'') end (** definition of raw permute_bn functions **) fun mk_perm_bn_eq_rhs p perm_bn_map bn_args (i, arg) = case AList.lookup (op=) bn_args i of NONE => arg | SOME (NONE) => mk_perm p arg | SOME (SOME bn) => (lookup perm_bn_map bn) $ p $ arg fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) = let val p = Free ("p", @{typ perm}) val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val perm_bn = lookup perm_bn_map bn_trm val lhs = perm_bn $ p $ list_comb (constr, args) val rhs = list_comb (constr, map_index (mk_perm_bn_eq_rhs p perm_bn_map bn_args) args) in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end fun mk_perm_bn_eqs lthy perm_bn_map cns_info (bn_trm, bn_n, bn_argss) = let val nth_cns_info = nth cns_info bn_n in map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info end fun define_raw_bn_perms raw_dt_info bn_info lthy = if null bn_info then ([], [], lthy) else let val RawDtInfo {raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val perm_bn_names = map (prefix "permute_") bn_names val perm_bn_arg_tys = map (nth raw_tys) bn_tys val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys) val perm_bn_map = bns ~~ perm_bn_frees val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_cns_info) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat perm_bn_eqs) val prod_simps = @{thms prod.inject HOL.simp_thms} - val lthy' = Local_Theory.subtarget (Function.add_function all_fun_names all_fun_eqs - Function_Common.default_config (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) - #> snd) lthy + val lthy' = + lthy + |> Local_Theory.begin_nested + |> snd + |> Function.add_function all_fun_names all_fun_eqs + Function_Common.default_config (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) + |> snd + |> Local_Theory.end_nested; val ({fs, simps, ...}, lthy'') = prove_termination_fun raw_size_thms lthy' val morphism = Proof_Context.export_morphism lthy'' (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy) val simps_exp = map (Morphism.thm morphism) (the simps) in (fs, simps_exp, lthy'') end (*** raw permutation functions ***) (** proves the two pt-type class properties **) fun prove_permute_zero induct bnfs perm_defs perm_fns ctxt = let val perm_types = map (body_type o fastype_of) perm_fns val perm_indnames = Old_Datatype_Prop.make_tnames perm_types fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) val goals = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) val map_ids = map BNF_Def.map_ident_of_bnf bnfs val rules = @{thm permute_zero} :: perm_defs @ map_ids val congs = map BNF_Def.map_cong0_of_bnf bnfs in Goal.prove ctxt perm_indnames [] goals (fn {context = ctxt', ...} => (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW asm_simp_tac (fold Simplifier.add_cong congs (put_simpset HOL_basic_ss ctxt' addsimps rules))) 1) |> Old_Datatype_Aux.split_conj_thm end fun prove_permute_plus induct bnfs perm_defs perm_fns ctxt = let val p = Free ("p", @{typ perm}) val q = Free ("q", @{typ perm}) val perm_types = map (body_type o fastype_of) perm_fns val perm_indnames = Old_Datatype_Prop.make_tnames perm_types fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) val goals = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) val map_comps = map BNF_Def.map_comp_of_bnf bnfs val rules = @{thms permute_plus o_def} @ perm_defs @ map_comps val congs = map BNF_Def.map_cong0_of_bnf bnfs in Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (fn {context = ctxt', ...} => (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW asm_simp_tac (fold Simplifier.add_cong congs (put_simpset HOL_basic_ss ctxt' addsimps rules))) 1) |> Old_Datatype_Aux.split_conj_thm end (* Return the map operator for the given type, along with its list of argument types, if a map operator exists; otherwise return NONE *) fun mk_map_of_type lthy (Type (c, tys)) = let fun mk_map bnf = let val live = BNF_Def.live_of_bnf bnf val t = BNF_Def.mk_map live tys tys (BNF_Def.map_of_bnf bnf) val (map_arg_tys, _) = BNF_Util.strip_typeN live (fastype_of t) in (t, map domain_type map_arg_tys) end in Option.map mk_map (BNF_Def.bnf_of lthy c) end | mk_map_of_type _ _ = NONE fun mk_perm_eq lthy ty_perm_assoc cnstr = let (* permute function with boolean flag indicating recursion *) fun mk_perm p ty = case (AList.lookup (op=) ty_perm_assoc ty) of SOME perm => (perm $ p, true) | NONE => (case mk_map_of_type lthy ty of SOME (t, tys) => let val (ts, recs) = split_list (map (mk_perm p) tys) in if exists I recs then (list_comb (t, ts), true) else (perm_const ty $ p, false) end | NONE => (perm_const ty $ p, false)) fun lookup_perm p (ty, arg) = fst (mk_perm p ty) $ arg val p = Free ("p", @{typ perm}) val (arg_tys, ty) = strip_type (fastype_of cnstr) val arg_names = Name.variant_list ["p"] (Old_Datatype_Prop.make_tnames arg_tys) val args = map Free (arg_names ~~ arg_tys) val lhs = lookup_perm p (ty, list_comb (cnstr, args)) val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) in ((Binding.empty_atts, eq), [], []) end fun define_raw_perms raw_dt_info lthy = let val RawDtInfo {raw_dt_names, raw_fp_sugars, raw_tys, raw_ty_args, raw_all_cns, raw_induct_thm, ...} = raw_dt_info val bnfs = (#fp_nesting_bnfs o hd) raw_fp_sugars val perm_fn_names = raw_dt_names |> map Long_Name.base_name |> map (prefix "permute_") val perm_fn_types = map perm_ty raw_tys val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names val perm_eqs = map (mk_perm_eq lthy (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns) fun tac ctxt (_, _, simps) = Class.intro_classes_tac ctxt [] THEN ALLGOALS (resolve_tac ctxt simps) fun morphism phi (fvs, dfs, simps) = (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); val ((perm_funs, perm_eq_thms), lthy') = lthy |> Local_Theory.exit_global |> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt}) |> BNF_LFP_Compat.primrec perm_fn_binds perm_eqs val perm_zero_thms = prove_permute_zero raw_induct_thm bnfs perm_eq_thms perm_funs lthy' val perm_plus_thms = prove_permute_plus raw_induct_thm bnfs perm_eq_thms perm_funs lthy' in lthy' |> Class.prove_instantiation_exit_result morphism tac (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) ||> Named_Target.theory_init end (** equivarance proofs **) val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} fun subproof_tac const_names simps = SUBPROOF (fn {prems, context = ctxt, ...} => HEADGOAL (simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) THEN' eqvt_tac ctxt (eqvt_relaxed_config addexcls const_names) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps (prems @ [eqvt_apply_sym])))) fun prove_eqvt_tac insts ind_thms const_names simps ctxt = HEADGOAL (Object_Logic.full_atomize_tac ctxt THEN' (DETERM o (Induct_Tacs.induct_tac ctxt insts (SOME ind_thms))) THEN_ALL_NEW subproof_tac const_names simps ctxt) fun mk_eqvt_goal pi const arg = let val lhs = mk_perm pi (const $ arg) val rhs = const $ (mk_perm pi arg) in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end fun raw_prove_eqvt consts ind_thms simps ctxt = if null consts then [] else let val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) val arg_tys = consts |> map fastype_of |> map domain_type val (arg_names, ctxt'') = Variable.variant_fixes (Old_Datatype_Prop.make_tnames arg_tys) ctxt' val args = map Free (arg_names ~~ arg_tys) val goals = map2 (mk_eqvt_goal p) consts args val insts = map (single o SOME) arg_names val const_names = map (fst o dest_Const) consts in Goal.prove_common ctxt'' NONE [] [] goals (fn {context, ...} => prove_eqvt_tac insts ind_thms const_names simps context) |> Proof_Context.export ctxt'' ctxt end end (* structure *) diff --git a/thys/Show/show_generator.ML b/thys/Show/show_generator.ML --- a/thys/Show/show_generator.ML +++ b/thys/Show/show_generator.ML @@ -1,430 +1,445 @@ (* Title: Show Author: Christian Sternagel Author: René Thiemann Maintainer: Christian Sternagel Maintainer: René Thiemann Generate/register show functions for arbitrary types. Precedence is used to determine parenthesization of subexpressions. In the automatically generated functions 0 means "no parentheses" and 1 means "parenthesize". *) signature SHOW_GENERATOR = sig (*generate show functions for the given datatype*) val generate_showsp : string -> local_theory -> local_theory val register_foreign_partial_and_full_showsp : string -> (*type name*) int -> (*default precedence for type parameters*) term -> (*partial show function*) term -> (*show function*) thm option -> (*definition of show function via partial show function*) term -> (*map function*) thm option -> (*compositionality theorem of map function*) bool list -> (*indicate which positions of type parameters are used*) thm -> (*show law intro rule*) local_theory -> local_theory (*for type constants (i.e., nullary type constructors) partial and full show functions coincide and no other information is necessary.*) val register_foreign_showsp : typ -> term -> thm -> local_theory -> local_theory (*automatically derive a "show" class instance for the given datatype*) val show_instance : string -> theory -> theory end structure Show_Generator : SHOW_GENERATOR = struct open Generator_Aux val mk_prec = HOLogic.mk_number @{typ nat} val prec0 = mk_prec 0 val prec1 = mk_prec 1 val showS = @{sort "show"} val showsT = @{typ "shows"} fun showspT T = @{typ nat} --> T --> showsT val showsify_typ = map_atyps (K showsT) val showsify = map_types showsify_typ fun show_law_const T = Const (@{const_name show_law}, showspT T --> T --> HOLogic.boolT) fun shows_prec_const T = Const (@{const_name shows_prec}, showspT T) fun shows_list_const T = Const (@{const_name shows_list}, HOLogic.listT T --> showsT) fun showsp_list_const T = Const (@{const_name showsp_list}, showspT T --> showspT (HOLogic.listT T)) val dest_showspT = binder_types #> tl #> hd type info = {prec : int, pshowsp : term, showsp : term, show_def : thm option, map : term, map_comp : thm option, used_positions : bool list, show_law_intro : thm} structure Data = Generic_Data (type T = info Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.merge (fn (info1, info2) => #pshowsp info1 = #pshowsp info2)) fun add_info tyco info = Data.map (Symtab.update_new (tyco, info)) val get_info = Context.Proof #> Data.get #> Symtab.lookup fun the_info ctxt tyco = (case get_info ctxt tyco of SOME info => info | NONE => error ("no show function available for type " ^ quote tyco)) fun declare_info tyco p pshow show show_def m m_comp used_pos law_thm = Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => add_info tyco {prec = p, pshowsp = Morphism.term phi pshow, showsp = Morphism.term phi show, show_def = Option.map (Morphism.thm phi) show_def, map = Morphism.term phi m, map_comp = Option.map (Morphism.thm phi) m_comp, used_positions = used_pos, show_law_intro = Morphism.thm phi law_thm}) val register_foreign_partial_and_full_showsp = declare_info fun register_foreign_showsp T show = let val tyco = (case T of Type (tyco, []) => tyco | _ => error "expected type constant") in register_foreign_partial_and_full_showsp tyco 0 show show NONE (HOLogic.id_const T) NONE [] end fun shows_string c = @{const "shows_string"} $ HOLogic.mk_string (Long_Name.base_name c) fun mk_shows_parens _ [t] = t | mk_shows_parens p ts = Library.foldl1 HOLogic.mk_comp (@{const shows_pl} $ p :: separate @{const shows_space} ts @ [@{const shows_pr} $ p]) fun simp_only_tac ctxt ths = CHANGED o full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths) fun generate_showsp tyco lthy = let val (tycos, Ts) = mutual_recursive_types tyco lthy val _ = map (fn tyco => "generating show function for type " ^ quote tyco) tycos |> cat_lines |> writeln val maps = Bnf_Access.map_terms lthy tycos val map_simps = Bnf_Access.map_simps lthy tycos val map_comps = Bnf_Access.map_comps lthy tycos val (tfrees, used_tfrees) = type_parameters (hd Ts) lthy val used_positions = map (member (op =) used_tfrees o TFree) tfrees val ss = map (subT "show") used_tfrees val show_Ts = map showspT used_tfrees val arg_shows = map Free (ss ~~ show_Ts) val dep_tycos = fold (add_used_tycos lthy) tycos [] fun mk_pshowsp (tyco, T) = ("pshowsp_" ^ Long_Name.base_name tyco, showspT T |> showsify_typ) fun default_show T = absdummy T (mk_id @{typ string}) fun constr_terms lthy = Bnf_Access.constr_terms lthy #> map (apsnd (fst o strip_type) o dest_Const) (* primrec definitions of partial show functions *) fun generate_pshow_eqs lthy (tyco, T) = let val constrs = constr_terms lthy tyco |> map (fn (c, Ts) => let val Ts' = map showsify_typ Ts in (Const (c, Ts' ---> T) |> showsify, Ts') end) fun shows_arg (x, T) = let val m = Generator_Aux.create_map default_show (fn (tyco, T) => fn p => Free (mk_pshowsp (tyco, T)) $ p) prec1 (equal @{typ "shows"}) (#used_positions oo the_info) (#map oo the_info) (curry (op $) o #pshowsp oo the_info) tycos (mk_prec o #prec oo the_info) T lthy val pshow = Generator_Aux.create_partial prec1 (equal @{typ "shows"}) (#used_positions oo the_info) (#map oo the_info) (curry (op $) o #pshowsp oo the_info) tycos (mk_prec o #prec oo the_info) T lthy in pshow $ (m $ Free (x, T)) |> infer_type lthy end fun generate_eq lthy (c, arg_Ts) = let val (p, xs) = Name.variant "p" (Variable.names_of lthy) |>> Free o rpair @{typ nat} ||> (fn ctxt => Name.invent_names ctxt "x" arg_Ts) val lhs = Free (mk_pshowsp (tyco, T)) $ p $ list_comb (c, map Free xs) val rhs = shows_string (dest_Const c |> fst) :: map shows_arg xs |> mk_shows_parens p in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end in map (generate_eq lthy) constrs end val eqs = map (generate_pshow_eqs lthy) (tycos ~~ Ts) |> flat val bindings = tycos ~~ Ts |> map mk_pshowsp |> map (fn (name, T) => (Binding.name name, T |> showsify_typ |> SOME, NoSyn)) - val ((pshows, pshow_simps), lthy) = Local_Theory.subtarget_result - (fn phi => fn (pshows, _, pshow_simps) => (map (Morphism.term phi) pshows, map (Morphism.fact phi) pshow_simps)) - (BNF_LFP_Rec_Sugar.primrec false [] bindings - (map (fn t => ((Binding.empty_atts, t), [], [])) eqs)) lthy + val ((pshows, pshow_simps), lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> BNF_LFP_Rec_Sugar.primrec false [] bindings + (map (fn t => ((Binding.empty_atts, t), [], [])) eqs) + |> Local_Theory.end_nested_result + (fn phi => fn (pshows, _, pshow_simps) => (map (Morphism.term phi) pshows, map (Morphism.fact phi) pshow_simps)) (* definitions of show functions via partial show functions and map *) fun generate_show_defs tyco lthy = let val ss = map (subT "show") used_tfrees val arg_Ts = map showspT used_tfrees val arg_shows = map Free (ss ~~ arg_Ts) val p = Name.invent (Variable.names_of lthy) "p" 1 |> the_single |> Free o rpair @{typ nat} val (pshow, m) = AList.lookup (op =) (tycos ~~ (pshows ~~ maps)) tyco |> the val ts = tfrees |> map TFree |> map (fn T => AList.lookup (op =) (used_tfrees ~~ map (fn x => x $ prec1) arg_shows) T |> the_default (default_show T)) val args = arg_shows @ [p] val rhs = HOLogic.mk_comp (pshow $ p, list_comb (m, ts)) |> infer_type lthy val abs_def = fold_rev lambda args rhs val name = "showsp_" ^ Long_Name.base_name tyco val ((showsp, (_, prethm)), lthy) = Local_Theory.define ((Binding.name name, NoSyn), (Binding.empty_atts, abs_def)) lthy val eq = Logic.mk_equals (list_comb (showsp, args), rhs) val thm = Goal.prove_future lthy (map (fst o dest_Free) args) [] eq (K (unfold_tac lthy [prethm])) in Local_Theory.note ((Binding.name (name ^ "_def"), []), [thm]) lthy |>> the_single o snd |>> `(K showsp) end - val ((shows, show_defs), lthy) = Local_Theory.subtarget_result - (fn phi => fn (shows, show_defs) => (map (Morphism.term phi) shows, map (Morphism.thm phi) show_defs)) - (fold_map generate_show_defs tycos #>> split_list) lthy + val ((shows, show_defs), lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map generate_show_defs tycos + |>> split_list + |> Local_Theory.end_nested_result + (fn phi => fn (shows, show_defs) => (map (Morphism.term phi) shows, map (Morphism.thm phi) show_defs)) (* alternative simp-rules for show functions *) fun generate_show_simps (tyco, T) lthy = let val constrs = constr_terms lthy tyco |> map (apsnd (map freeify_tvars)) |> map (fn (c, Ts) => (Const (c, Ts ---> T), Ts)) fun shows_arg (x, T) = let fun create_show (T as TFree _) = AList.lookup (op =) (used_tfrees ~~ arg_shows) T |> the | create_show (Type (tyco, Ts)) = (case AList.lookup (op =) (tycos ~~ shows) tyco of SOME show_const => list_comb (show_const, arg_shows) | NONE => let val {showsp = s, used_positions = up, ...} = the_info lthy tyco val ts = (up ~~ Ts) |> map_filter (fn (b, T) => if b then SOME (create_show T) else NONE) in list_comb (s, ts) end) | create_show T = error ("unexpected schematic variable " ^ quote (Syntax.string_of_typ lthy T)) val show = create_show T |> infer_type lthy in show $ prec1 $ Free (x, T) end fun generate_eq_thm lthy (c, arg_Ts) = let val (p, xs) = Name.variant "p" (Variable.names_of lthy) |>> Free o rpair @{typ nat} ||> (fn ctxt => Name.invent_names ctxt "x" arg_Ts) val show_const = AList.lookup (op =) (tycos ~~ shows) tyco |> the val lhs = list_comb (show_const, arg_shows) $ p $ list_comb (c, map Free xs) val rhs = shows_string (dest_Const c |> fst) :: map shows_arg xs |> mk_shows_parens p val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |> infer_type lthy val dep_show_defs = map_filter (#show_def o the_info lthy) dep_tycos val dep_map_comps = map_filter (#map_comp o the_info lthy) dep_tycos val thm = Goal.prove_future lthy (fst (dest_Free p) :: map fst xs @ ss) [] eq (fn {context = ctxt, ...} => unfold_tac ctxt (@{thms id_def o_def} @ flat pshow_simps @ dep_map_comps @ show_defs @ dep_show_defs @ flat map_simps)) in thm end val thms = map (generate_eq_thm lthy) constrs val name = "showsp_" ^ Long_Name.base_name tyco in lthy |> Local_Theory.note ((Binding.name (name ^ "_simps"), @{attributes [simp, code]}), thms) |> apfst snd end - val (show_simps, lthy) = Local_Theory.subtarget_result - (fn phi => map (Morphism.fact phi)) - (fold_map generate_show_simps (tycos ~~ Ts)) lthy + val (show_simps, lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map generate_show_simps (tycos ~~ Ts) + |> Local_Theory.end_nested_result + (fn phi => map (Morphism.fact phi)) (* show law theorems *) val induct_thms = Bnf_Access.induct_thms lthy tycos val set_simps = Bnf_Access.set_simps lthy tycos val sets = Bnf_Access.set_terms lthy tycos fun generate_show_law_thms (tyco, x) = let val sets = AList.lookup (op =) (tycos ~~ sets) tyco |> the val used_sets = map (the o AList.lookup (op =) (map TFree tfrees ~~ sets)) used_tfrees fun mk_prem ((show, set), T) = let (*val y = singleton (Name.variant_list [fst x]) "y" |> Free o rpair T*) val y = Free (subT "x" T, T) val lhs = HOLogic.mk_mem (y, set $ Free x) |> HOLogic.mk_Trueprop val rhs = show_law_const T $ show $ y |> HOLogic.mk_Trueprop in Logic.all y (Logic.mk_implies (lhs, rhs)) end val prems = map mk_prem (arg_shows ~~ used_sets ~~ used_tfrees) val (show_const, T) = AList.lookup (op =) (tycos ~~ (shows ~~ Ts)) tyco |> the val concl = show_law_const T $ list_comb (show_const, arg_shows) $ Free x |> HOLogic.mk_Trueprop in Logic.list_implies (prems, concl) |> infer_type lthy end val xs = Name.invent_names (Variable.names_of lthy) "x" Ts val show_law_prethms = map generate_show_law_thms (tycos ~~ xs) val rec_info = (the_info lthy, #used_positions, tycos) val split_IHs = split_IHs rec_info val recursor_tac = std_recursor_tac rec_info used_tfrees #show_law_intro fun show_law_tac ctxt xs = let val constr_Ts = tycos |> map (#ctrXs_Tss o #fp_ctr_sugar o the o BNF_FP_Def_Sugar.fp_sugar_of ctxt) val ind_case_to_idxs = let fun number n (i, j) ((_ :: xs) :: ys) = (n, (i, j)) :: number (n + 1) (i, j + 1) (xs :: ys) | number n (i, _) ([] :: ys) = number n (i + 1, 0) ys | number _ _ [] = [] in AList.lookup (op =) (number 0 (0, 0) constr_Ts) #> the end fun instantiate_IHs IHs assms = map (fn IH => OF_option IH (replicate (Thm.nprems_of IH - length assms) NONE @ map SOME assms)) IHs fun induct_tac ctxt f = (DETERM o Induction.induction_tac ctxt false (map (fn x => [SOME (NONE, (x, false))]) xs) [] [] (SOME induct_thms) []) THEN_ALL_NEW (fn st => Subgoal.SUBPROOF (fn {context = ctxt, prems, params, ...} => f ctxt (st - 1) prems params) ctxt st) (*do not use full "show_law_simps" here, since otherwise too many subgoals might be solved (so that the number of subgoals does no longer match the number of IHs)*) val show_law_simps_less = @{thms shows_string_append shows_pl_append shows_pr_append shows_space_append} fun o_append_intro_tac ctxt f = HEADGOAL ( K (Method.try_intros_tac ctxt @{thms o_append} []) THEN_ALL_NEW K (unfold_tac ctxt show_law_simps_less) THEN_ALL_NEW (fn i => Subgoal.SUBPROOF (fn {context = ctxt', ...} => f (i - 1) ctxt') ctxt i)) fun solve_tac ctxt case_num prems params = let val (i, _) = ind_case_to_idxs case_num (*(constructor number, argument number)*) val k = length prems - length used_tfrees val (IHs, assms) = chop k prems in resolve_tac ctxt @{thms show_lawI} 1 THEN Subgoal.FOCUS (fn {context = ctxt, ...} => let val assms = map (Local_Defs.unfold ctxt (nth set_simps i)) assms val Ts = map (fastype_of o Thm.term_of o snd) params val IHs = instantiate_IHs IHs assms |> split_IHs Ts in unfold_tac ctxt (nth show_simps i) THEN o_append_intro_tac ctxt (fn i => fn ctxt' => resolve_tac ctxt' @{thms show_lawD} 1 THEN recursor_tac assms (nth Ts i) (nth IHs i) ctxt') end) ctxt 1 end in induct_tac ctxt solve_tac end val show_law_thms = prove_multi_future lthy (map fst xs @ ss) [] show_law_prethms (fn {context = ctxt, ...} => HEADGOAL (show_law_tac ctxt (map Free xs))) - val (show_law_thms, lthy) = Local_Theory.subtarget_result Morphism.fact - (fold_map (fn (tyco, thm) => - let val name = Long_Name.base_name tyco - in - Local_Theory.note - ((Binding.name ("show_law_" ^ name), @{attributes [show_law_intros]}), [thm]) - #> apfst (the_single o snd) - end) (tycos ~~ show_law_thms)) lthy + val (show_law_thms, lthy) = + lthy + |> Local_Theory.begin_nested + |> snd + |> fold_map (fn (tyco, thm) => + Local_Theory.note + ((Binding.name ("show_law_" ^ Long_Name.base_name tyco), @{attributes [show_law_intros]}), [thm]) + #> apfst (the_single o snd)) (tycos ~~ show_law_thms) + |> Local_Theory.end_nested_result Morphism.fact + in lthy |> fold (fn ((((((tyco, pshow), show), show_def), m), m_comp), law_thm) => declare_info tyco 1 pshow show (SOME show_def) m (SOME m_comp) used_positions law_thm) (tycos ~~ pshows ~~ shows ~~ show_defs ~~ maps ~~ map_comps ~~ show_law_thms) end fun ensure_info tyco lthy = (case get_info lthy tyco of SOME _ => lthy | NONE => generate_showsp tyco lthy) (* proving show instances *) fun dest_showsp showsp = dest_Const showsp ||> ( binder_types #> chop_prefix (fn T => T <> @{typ nat}) #>> map (freeify_tvars o dest_showspT) ##> map (dest_TFree o freeify_tvars) o snd o dest_Type o hd o tl) fun show_instance tyco thy = let val _ = Sorts.has_instance (Sign.classes_of thy) tyco showS andalso error ("type " ^ quote tyco ^ " is already an instance of class \"show\"") val _ = writeln ("deriving \"show\" instance for type " ^ quote tyco) val thy = Named_Target.theory_map (ensure_info tyco) thy val lthy = Named_Target.theory_init thy val {showsp, ...} = the_info lthy tyco val (showspN, (used_tfrees, tfrees)) = dest_showsp showsp val tfrees' = tfrees |> map (fn (x, S) => if member (op =) used_tfrees (TFree (x, S)) then (x, showS) else (x, S)) val used_tfrees' = map (dest_TFree #> fst #> rpair showS #> TFree) used_tfrees val T = Type (tyco, map TFree tfrees') val arg_Ts = map showspT used_tfrees' val showsp' = Const (showspN, arg_Ts ---> showspT T) val shows_prec_def = Logic.mk_equals (shows_prec_const T, list_comb (showsp', map shows_prec_const used_tfrees')) val shows_list_def = Logic.mk_equals (shows_list_const T, showsp_list_const T $ shows_prec_const T $ prec0) val name = Long_Name.base_name tyco val ((shows_prec_thm, shows_list_thm), lthy) = Class.instantiation ([tyco], tfrees', showS) thy |> Generator_Aux.define_overloaded_generic ((Binding.name ("shows_prec_" ^ name ^ "_def"), @{attributes [code]}), shows_prec_def) ||>> Generator_Aux.define_overloaded_generic ((Binding.name ("shows_list_" ^ name ^ "_def"), @{attributes [code]}), shows_list_def) in Class.prove_instantiation_exit (fn ctxt => let val show_law_intros = Named_Theorems.get ctxt @{named_theorems "show_law_intros"} val show_law_simps = Named_Theorems.get ctxt @{named_theorems "show_law_simps"} val show_append_tac = resolve_tac ctxt @{thms show_lawD} THEN' REPEAT_ALL_NEW (resolve_tac ctxt show_law_intros) THEN_ALL_NEW ( resolve_tac ctxt @{thms show_lawI} THEN' simp_only_tac ctxt show_law_simps) in Class.intro_classes_tac ctxt [] THEN unfold_tac ctxt [shows_prec_thm, shows_list_thm] THEN REPEAT1 (HEADGOAL show_append_tac) end) lthy end val _ = Theory.setup (Derive_Manager.register_derive "show" "generate show instance" (K o show_instance)) end