diff --git a/thys/CakeML_Codegen/Preproc/embed.ML b/thys/CakeML_Codegen/Preproc/embed.ML --- a/thys/CakeML_Codegen/Preproc/embed.ML +++ b/thys/CakeML_Codegen/Preproc/embed.ML @@ -1,362 +1,362 @@ signature EMBED = sig val eval_typ: typ -> typ datatype embed_proof = No_Auto | Simp | Eval datatype cert_proof = Cert | Skip type embed_opts = {proof: embed_proof, cert: cert_proof} val default_opts: embed_opts val embed_def: (binding * Attrib.binding) -> term list -> embed_opts -> local_theory -> ((term * thm * term * thm option) * local_theory) val embed_def_cmd: Attrib.binding -> binding -> string list -> embed_opts -> local_theory -> Proof.state type fun_info = {rs: term, rs_def: thm, base_embeds: thm list, consts: (string * int) list, inducts: thm list option, simps: thm list} val embed_tac: fun_info -> cert_proof -> Proof.context -> int -> tactic val embed_ext_tac: fun_info -> cert_proof -> Proof.context -> int -> tactic val debug: bool Config.T end structure Embed: EMBED = struct (* FIXME copied from skip_proof.ML *) val (_, make_thm_cterm) = Context.>>> (Context.map_theory_result (Thm.add_oracle (@{binding eval_oracle}, I))) fun make_thm ctxt prop = make_thm_cterm (Thm.cterm_of ctxt prop) fun cheat_tac ctxt i st = resolve_tac ctxt [make_thm ctxt (Var (("A", 0), propT))] i st (** utilities **) (* FIXME copied from dict_construction.ML *) val debug = Attrib.setup_config_bool @{binding "embed_debug"} (K false) fun if_debug ctxt f = if Config.get ctxt debug then f () else () fun ALLGOALS' ctxt = if Config.get ctxt debug then ALLGOALS else PARALLEL_ALLGOALS fun prove' ctxt = if Config.get ctxt debug then Goal.prove ctxt else Goal.prove_future ctxt fun prove_common' ctxt = Goal.prove_common ctxt (if Config.get ctxt debug then NONE else SOME ~1) fun eval_typ typ = @{typ "rule fset"} --> @{typ term} --> typ --> @{typ bool} datatype embed_proof = No_Auto | Simp | Eval datatype cert_proof = Cert | Skip type embed_opts = {proof: embed_proof, cert: cert_proof} val default_opts = {proof = Simp, cert = Cert} open Dict_Construction_Util fun all_typs (Type (typ, args)) = typ :: maps all_typs args | all_typs _ = [] val code_tac = Code_Simp.static_tac {consts = [@{const_name rules'}, @{const_name fmdom}, @{const_name fmempty}, @{const_name fmupd}], ctxt = @{context}, simpset = NONE} type fun_info = {rs: term, rs_def: thm, base_embeds: thm list, consts: (string * int) list, inducts: thm list option, simps: thm list} fun embed_ext_tac {inducts, simps, rs_def, base_embeds, consts, ...} cert = Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl, ...} => let val _ = if_debug ctxt (fn () => tracing ("Proving " ^ Syntax.string_of_term ctxt (Thm.term_of concl))); val elims = Named_Theorems.get ctxt @{named_theorems eval_data_elims} val names = map fst consts fun get_vars t = case t of Const (@{const_name eval'}, _) $ _ $ t $ x => (map Free (Term.add_frees t []), rev (map Free (Term.add_frees x []))) val (tss, xss) = Logic.dest_conjunctions (Thm.term_of concl) |> map (HOLogic.dest_Trueprop o Logic.strip_imp_concl) |> map get_vars |> split_list val conv = Refine_Util.HOL_concl_conv (K (Conv.arg_conv (Conv.rewrs_conv (map safe_mk_meta_eq simps)))) ctxt val cert_tac = case cert of Skip => cheat_tac ctxt | Cert => SOLVED' (Tactics.eval_tac ctxt base_embeds) in maybe_induct_tac inducts xss tss ctxt THEN ALLGOALS' ctxt (CONVERSION conv THEN' TRY' (REPEAT_ALL_NEW (eresolve_tac ctxt elims)) THEN' resolve_tac ctxt @{thms eval_compose} CONTINUE_WITH_FW [Tactics.wellformed_tac ctxt, (* requires full rewriting: rule from ruleset may apply only if arguments are rewritten first *) Tactics.rewrite1_tac ctxt (SOME {rs_def = rs_def, simps = simps, restrict = SOME names}), cert_tac]) end) fun embed_tac info cert ctxt = let val {consts, ...} = info fun loop 0 = K all_tac | loop n = fo_rtac @{thm eval'_ext} ctxt CONTINUE_WITH_FW [Tactics.wellformed_tac ctxt, loop (n - 1)] val loops = map (loop o snd) consts in SELECT_GOAL (HEADGOAL (Goal.conjunction_tac CONTINUE_WITH loops) THEN Goal.recover_conjunction_tac) CONTINUE_WITH [TRY' (norm_all_conjunction_tac ctxt) THEN' embed_ext_tac info cert ctxt] end fun extend ctxt thm = let val (lhs, _) = Logic.dest_equals (Thm.prop_of thm) val (head, args) = Term.strip_comb lhs val pretty = Syntax.string_of_term ctxt (Thm.prop_of thm) val fun_type = can (Term.dest_funT o fastype_of) head in if not fun_type then error ("Implementation restriction: can't deal with non-function constant: " ^ pretty) else if null args then @{thm embed_ext} OF [thm] else thm end fun embed_def (binding, def_binding) terms {proof, cert} lthy = let val (consts, _) = Syntax.check_terms lthy terms |> map dest_Const |> split_list val _ = Pretty.block (Pretty.str "Defining the embedding(s) of " :: Pretty.separate "" (map (pretty_const lthy) consts)) |> Pretty.writeln val config_ctxt = lthy |> Config.put Constructor_Funs.enabled true |> Config.put Pattern_Compatibility.enabled true |> Config.put Dynamic_Unfold.enabled true val code_eqss = Dict_Construction.group_code_eqs config_ctxt consts val raw_eqs = flat code_eqss |> maps (snd o snd) |> map snd |> cat_options |> map (Thm.prop_of o extend lthy o Conv.fconv_rule (Dict_Construction.normalizer_conv lthy)) val eqs = map HOL_Term.mk_eq raw_eqs val rs = mk_fset @{typ "term \ term"} eqs val C_info = maps all_consts raw_eqs |> map snd |> maps all_typs |> distinct op = |> map (fn typ => Option.map (pair typ) (try (HOL_Datatype.mk_dt_def lthy) typ)) |> cat_options |> map (apfst mk_name) |> mk_fmap (@{typ name}, @{typ dt_def}) val C_info_binding = Binding.qualify_name true binding "C_info" val ((rs_term, (_, rs_def)), lthy') = Local_Theory.define ((binding, NoSyn), (def_binding, rs)) lthy val ((C_info_term, (_, C_info_def)), lthy') = Local_Theory.define ((C_info_binding, NoSyn), ((Thm.def_binding C_info_binding, []), C_info)) lthy' val prop = HOLogic.mk_Trueprop (@{term rules} $ C_info_term $ rs_term) fun tac eval ctxt = HEADGOAL (fo_rtac @{thm rules_approx} ctxt) THEN Local_Defs.unfold_tac ctxt [rs_def, C_info_def] THEN (if eval then HEADGOAL (eval_tac ctxt) else Local_Defs.unfold_tac ctxt @{thms rules'_def} THEN HEADGOAL (REPEAT_ALL_NEW (resolve_tac ctxt @{thms conjI})) THEN ALLGOALS' ctxt (code_tac ctxt)) val thm = case proof of No_Auto => NONE | Eval => SOME (prove' lthy' [] [] prop (fn {context = ctxt, ...} => tac true ctxt)) | Simp => SOME (prove' lthy' [] [] prop (fn {context = ctxt, ...} => tac false ctxt)) val _ = Option.map (on_thms_complete (fn () => writeln "Proved wellformedness") o single) thm fun prove_embed code_eqs (base_simps, base_embeds) = if exists (null o snd o snd) code_eqs then (* constructor *) (base_simps, base_embeds) else (* proper definition *) let val (consts, simps) = map (fn (name, (_, eqs)) => let val (count, eqs) = split_list (map (apfst (length o fst)) eqs) |>> distinct op = |>> the_single ||> cat_options in ((name, count), eqs) end) code_eqs |> split_list ||> flat ||> map (Conv.fconv_rule (Dict_Construction.normalizer_conv lthy')) (* FIXME the whole treatment of type variables here is probably wrong *) val const_terms = map (Const o rpair dummyT o fst) consts |> Syntax.check_terms lthy' val fun_induct = Option.mapPartial #inducts (try (Function.get_info lthy') (hd const_terms)) val bnf_induct = induct_of_bnf_const lthy' (hd const_terms) val inducts = merge_options (fun_induct, bnf_induct) val _ = if is_none inducts andalso length simps > 1 then warning ("No induction rule found (could be problematic). Did you run this through declassify?") else () val info: fun_info = {rs = rs_term, rs_def = rs_def, base_embeds = base_embeds, consts = consts, simps = simps @ base_simps, inducts = inducts} fun mk_goal (const, _) = Term.list_comb (Const (@{const_name eval'}, eval_typ dummyT), [rs_term, @{const Const} $ mk_name const, Const (const, dummyT)]) |> HOLogic.mk_Trueprop val goals = Syntax.check_terms lthy' (map mk_goal consts) val embeds = prove_common' lthy' [] [] goals (fn {context = ctxt, ...} => HEADGOAL (embed_tac info cert ctxt)) val msg = Pretty.block (Pretty.str "Proved the embedding(s) of " :: Pretty.separate "" (map (pretty_const lthy') (map fst consts))) |> Pretty.string_of val _ = on_thms_complete (fn () => writeln msg) embeds in (simps @ base_simps, embeds @ base_embeds) end val (_, embeds) = fold prove_embed code_eqss ([], []) val (_, lthy'') = note_thms binding embeds lthy' in ((rs_term, rs_def, C_info_term, thm), lthy'') end fun method_text_of_tac tac = Method.Basic (fn ctxt => fn _ => Context_Tactic.CONTEXT_TACTIC (tac ctxt)) fun embed_def_cmd def_binding binding raw_consts opts lthy = let val _ = if #cert opts = Skip then warning "Skipping certificate proofs" else () - val lthy' = Local_Theory.open_target lthy + val lthy' = (snd o Local_Theory.begin_nested) lthy val def_binding = if Binding.is_empty_atts def_binding then (Thm.def_binding binding, @{attributes [code]}) else apsnd (fn attribs => @{attributes [code]} @ attribs) def_binding val terms = map (Syntax.parse_term lthy') raw_consts val ((rs_term, _, C_term, thm), lthy'') = embed_def (binding, def_binding) terms opts lthy' - val lthy''' = Local_Theory.close_target lthy'' + val lthy''' = Local_Theory.end_nested lthy'' val phi = Proof_Context.export_morphism lthy'' lthy''' val rs_term' = Morphism.term phi rs_term val C_term' = Morphism.term phi C_term val expr = (@{const_name rules}, ((Binding.name_of binding, true), (Expression.Positional [SOME C_term', SOME rs_term'], []))) val goal = HOLogic.mk_Trueprop (@{const rules} $ C_term' $ rs_term') val meth = method_text_of_tac (fn ctxt => case thm of SOME thm => HEADGOAL (resolve_tac ctxt [Morphism.thm phi thm]) | NONE => all_tac) val interp = if Named_Target.is_theory lthy then Interpretation.global_interpretation ([expr], []) [] else Interpretation.sublocale ([expr], []) [] fun after_qed [[proof]] lthy = let in lthy |> interp |> Proof.refine_singleton (method_text_of_tac (fn ctxt => HEADGOAL (resolve_tac ctxt [proof]))) |> Proof.global_immediate_proof end in lthy''' |> Proof.theorem NONE after_qed [[(goal, [])]] |> Proof.refine_singleton meth end (** setup **) val parse_flag = (Parse.reserved "skip" >> (fn _ => fn {proof, ...} => {cert = Skip, proof = proof}) || Parse.reserved "eval" >> (fn _ => fn {cert, ...} => {cert = cert, proof = Eval}) || Parse.reserved "no_auto" >> (fn _ => fn {cert, ...} => {cert = cert, proof = No_Auto})) val parse_flags = Scan.optional (Args.parens (Parse.list parse_flag >> (fn fs => fold (curry op o) fs I))) I val _ = Outer_Syntax.local_theory_to_proof @{command_keyword "embed"} "redefines a constant using a deep embedding of term rewriting in HOL" ((parse_flags -- Parse_Spec.opt_thm_name ":" -- Parse.binding --| @{keyword "is"} -- Scan.repeat1 Parse.const) >> (fn (((opts, def_binding), binding), const) => embed_def_cmd def_binding binding const (opts default_opts))) end diff --git a/thys/CakeML_Codegen/Preproc/eval_instances.ML b/thys/CakeML_Codegen/Preproc/eval_instances.ML --- a/thys/CakeML_Codegen/Preproc/eval_instances.ML +++ b/thys/CakeML_Codegen/Preproc/eval_instances.ML @@ -1,189 +1,189 @@ signature EVAL_INSTANCES = sig val make: string -> theory -> theory val make_cmd: string -> theory -> theory val setup: theory -> theory val intro_tac: Proof.context -> {intros: thm list} -> tactic val elim_tac: Proof.context -> {distincts: thm list, elims: thm list, injects: thm list} -> tactic end structure Eval_Instances: EVAL_INSTANCES = struct open Dict_Construction_Util fun intro_tac ctxt {intros} = REPEAT (HEADGOAL (eresolve_tac ctxt @{thms eval'E})) THEN HEADGOAL (fo_rtac @{thm eval'I} ctxt CONTINUE_WITH_FW [Method.assm_tac ctxt, SOLVED' (Tactics.rewrite_tac ctxt NONE), SOLVED' (fo_resolve_tac intros ctxt THEN_ALL_NEW Method.assm_tac ctxt)]) fun elim_tac ctxt {elims, distincts, injects} = let fun is_vareq prop = case prop of @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => true | _ => false val tac = eresolve_tac ctxt @{thms eval'E} THEN' eresolve_tac ctxt elims THEN_ALL_NEW (econtr_tac distincts ctxt ORELSE' Subgoal.FOCUS (fn {context = ctxt, prems, ...} => let val that :: wf :: rewr :: term_eq :: constr_eq :: eval = prems val eqs = Tactics.elims_injects ctxt injects constr_eq |> filter (is_vareq o Thm.prop_of) val subst_in_rewr = Drule.infer_instantiate ctxt [(("P", 0), @{cterm "\t'. rs \ t \* t'"})] @{thm subst} val rewr' = subst_in_rewr OF [term_eq, rewr] val tac = fo_rtac (that OF [wf]) ctxt THEN_ALL_NEW (SOLVED' (fo_rtac rewr' ctxt) ORELSE' (fo_rtac @{thm eval_trivI} ctxt THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt eqs) THEN' resolve_tac ctxt eval)) in HEADGOAL tac end) ctxt) in HEADGOAL tac end val ind_flags = {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false} fun make typ_name thy = let val ctxt = Proof_Context.init_global thy val {ctrs, T, distincts, injects, ...} = the (Ctr_Sugar.ctr_sugar_of ctxt typ_name) val len = length (snd (dest_Type (unvarify_typ T))) val tparams = map (rpair @{sort evaluate}) (Name.invent Name.context Name.aT len) val typ = Embed.eval_typ (Type (typ_name, map TFree tparams)) (* FIXME use name mangling *) val name = "eval_" ^ Long_Name.base_name typ_name val ind_head = Free (name, typ) val rs = Free ("rs", @{typ "rule fset"}) val t = Free ("t", @{typ term}) val thesis = Free ("thesis", @{typ bool}) fun mk_parts ctr = let val (ctr_name, typ) = dest_Const (sortify @{sort evaluate} (Logic.unvarify_global ctr)) val (arg_typs, _) = strip_type typ val term_params = length arg_typs |> Name.invent Name.context "t0" |> map (Free o rpair @{typ term}) val ctr_params = map Free (Name.invent_names Name.context "a0" arg_typs) in (ctr_name, typ, term_params, ctr_params) end val parts = map mk_parts ctrs fun mk_ind_rule (ctr_name, ctr_typ, term_params, ctr_params) = let val term_applied = HOL_Term.list_comb (@{term term.Const} $ mk_name ctr_name, term_params) val ctr_applied = list_comb (Const (ctr_name, ctr_typ), ctr_params) val concl = HOLogic.mk_Trueprop (ind_head $ rs $ term_applied $ ctr_applied) fun mk_prem term_param ctr_param = HOLogic.mk_Trueprop (Const (@{const_name eval}, Embed.eval_typ (fastype_of ctr_param)) $ rs $ term_param $ ctr_param) val prems = map2 mk_prem term_params ctr_params in fold Logic.all (term_params @ ctr_params) (prems ===> concl) end val lthy = Class.instantiation ([typ_name], tparams, @{sort evaluate}) thy val ind_rules = map (pair (Binding.empty, [])) (Syntax.check_terms lthy (map mk_ind_rule parts)) val (info, (lthy', lthy)) = - Local_Theory.open_target lthy + (snd o Local_Theory.begin_nested) lthy |> Inductive.add_ind_def ind_flags [ind_head] ind_rules [] [rs] [(Binding.name name, NoSyn)] - ||> `Local_Theory.close_target + ||> `Local_Theory.end_nested val phi = Proof_Context.export_morphism lthy lthy' val info' = Inductive.transform_result phi info fun inst_tac ctxt = Class.intro_classes_tac ctxt [] THEN HEADGOAL (Subgoal.FOCUS (fn {context = ctxt, prems, ...} => DETERM (HEADGOAL (resolve_tac ctxt [#induct info' OF prems])) THEN PARALLEL_ALLGOALS (Tactics.wellformed_tac ctxt)) ctxt) val lthy'' = Class.prove_instantiation_instance inst_tac lthy' fun mk_intro_elim (ctr_name, ctr_typ, term_params, ctr_params) = let val term_applied = HOL_Term.list_comb (@{term term.Const} $ mk_name ctr_name, term_params) val ctr_applied = list_comb (Const (ctr_name, ctr_typ), ctr_params) fun mk_prem term_param ctr_param = (Const (@{const_name eval'}, Embed.eval_typ (fastype_of ctr_param)) $ rs $ term_param $ ctr_param) val prems = map HOLogic.mk_Trueprop ((@{term wellformed} $ t) :: (@{term rewrite_rt} $ rs $ t $ term_applied) :: map2 mk_prem term_params ctr_params) val concl = HOLogic.mk_Trueprop (Const (@{const_name eval'}, typ) $ rs $ t $ ctr_applied) val intro = fold Logic.all (term_params @ ctr_params) (prems ===> concl) val thesis = HOLogic.mk_Trueprop thesis val elim = fold Logic.all ctr_params (concl ==> (fold Logic.all term_params (prems ===> thesis)) ==> thesis) in (intro, elim) end fun prove_intro goal = Goal.prove_future lthy'' ["rs", "t"] [] goal (fn {context = ctxt, ...} => intro_tac ctxt {intros = #intrs info'}) fun prove_elim goal = Goal.prove_future lthy'' ["rs", "t", "thesis"] [] goal (fn {context = ctxt, ...} => elim_tac ctxt {elims = #elims info', distincts = distincts, injects = injects}) val (intros, elims) = map mk_intro_elim parts |> split_list |>> map prove_intro ||> map prove_elim in lthy'' |> Local_Theory.note ((Binding.empty, @{attributes [eval_data_intros]}), intros) |> snd |> Local_Theory.note ((Binding.empty, @{attributes [eval_data_elims]}), elims) |> snd |> Local_Theory.exit_global end fun make_cmd s thy = let val ctxt = Proof_Context.init_global thy val typ_name = Proof_Context.read_type_name {proper = true, strict = false} ctxt s |> dest_Type |> fst in make typ_name thy end (** setup **) val setup = Derive_Manager.register_derive "evaluate" "derives an embedding relation for a datatype" (fn typ_name => fn param => if param = "" then make typ_name else error "unknown parameter, expected no parameter") end \ No newline at end of file diff --git a/thys/Collections/ICF/tools/ICF_Tools.thy b/thys/Collections/ICF/tools/ICF_Tools.thy --- a/thys/Collections/ICF/tools/ICF_Tools.thy +++ b/thys/Collections/ICF/tools/ICF_Tools.thy @@ -1,312 +1,312 @@ section \General ML-level tools\ theory ICF_Tools imports Main begin lemma meta_same_imp_rule: "(\PROP P; PROP P\ \ PROP Q) \ (PROP P \ PROP Q)" by rule (* TODO: Replace by distinct_prems_rl *) ML \ infix 0 ##; fun (f ## g) (a,b) = (f a, g b) signature ICF_TOOLS = sig (* Generic *) val gen_variant: (string -> bool) -> string -> string val map_option: ('a -> 'b) -> 'a option -> 'b option val parse_cpat: cterm context_parser val rename_cterm: (cterm * cterm) -> ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list val renames_cterm: (cterm * cterm) -> bool val import_cterm: cterm -> Proof.context -> cterm * Proof.context val inst_meta_cong: Proof.context -> cterm -> thm (* val thms_from_main: string -> thm list val thm_from_main: string -> thm *) val sss_add: thm list -> Proof.context -> Proof.context val changed_conv: conv -> conv val repeat_top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv val rem_dup_prems: Proof.context -> thm -> thm (* Definition Theorems *) val dest_def_eq: term -> term * term val norm_def_thm: thm -> thm val dthm_lhs: thm -> term val dthm_rhs: thm -> term val dthm_params: thm -> term list val dthm_head: thm -> term val dt_lhs: term -> term val dt_rhs: term -> term val dt_params: term -> term list val dt_head: term -> term val chead_of: cterm -> cterm val chead_of_thm: thm -> cterm (* Simple definition: name\term, fixes variables *) val define_simple: string -> term -> local_theory -> ((term * thm) * local_theory) (* Wrapping stuff inside local theory context *) val wrap_lthy_result_global: (local_theory -> 'a * local_theory) -> (morphism -> 'a -> 'b) -> theory -> 'b * theory val wrap_lthy_global: (local_theory -> local_theory) -> theory -> theory val wrap_lthy_result_local: (local_theory -> 'a * local_theory) -> (morphism -> 'a -> 'b) -> local_theory -> 'b * local_theory val wrap_lthy_local: (local_theory -> local_theory) -> local_theory -> local_theory (* Wrapped versions of simple definition *) val define_simple_global: string -> term -> theory -> ((term * thm) * theory) val define_simple_local: string -> term -> local_theory -> ((term * thm) * local_theory) (* Revert abbreviations matching pattern (TODO/FIXME: HACK) *) val revert_abbrevs: string -> theory -> theory end; structure ICF_Tools: ICF_TOOLS = struct fun gen_variant decl s = let fun search s = if not (decl s) then s else search (Symbol.bump_string s); in if not (decl s) then s else search (Symbol.bump_init s) end; val parse_cpat = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, str) => Proof_Context.read_term_pattern ctxt str |> Thm.cterm_of ctxt ); (* Renaming first-order match *) fun rename_cterm (ct1,ct2) = ( Thm.first_order_match (ct2,ct1); Thm.first_order_match (ct1,ct2)); val renames_cterm = can rename_cterm; fun import_cterm ct ctxt = let val (t', ctxt') = yield_singleton (Variable.import_terms true) (Thm.term_of ct) ctxt; val ct' = Thm.cterm_of ctxt' t'; in (ct', ctxt') end (* Get theorem by name, that is visible in HOL.Main. Moreover, the theory of this theorem will be HOL.Main, which is required to avoid non-trivial theory merges as they may occur when using thm-antiquotation. (cf. post https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00175.html on Isabelle mailing list) *)(* fun thms_from_main name = let val xthmref = Facts.named name; val thy = @{theory Main}; val name = Facts.ref_name xthmref |> Global_Theory.intern_fact thy; val name = case name of "_" => "Pure.asm_rl" | name => name; val fs = Global_Theory.facts_of thy; val thms = Facts.lookup (Context.Theory thy) fs name |> the |> #2 |> map (Thm.transfer thy); in thms end fun thm_from_main name = thms_from_main name |> Facts.the_single (name, Position.none) *) (* Unfold with simpset fun unfold_ss ss = let val simple_prover = SINGLE o (fn ss => ALLGOALS (resolve_tac (Raw_Simplifier.prems_of ss))); in Raw_Simplifier.rewrite_thm (true,false,false) simple_prover ss end; *) local fun sss_add_single thm ss = let val simps = Raw_Simplifier.dest_ss (simpset_of ss) |> #simps |> map #2; val ess = ss delsimps simps; val thm' = simplify ss thm; val new_simps = simps |> map (simplify (ess addsimps [thm'])); val ss' = ess addsimps (thm'::new_simps) in ss' end in val sss_add = fold sss_add_single end local open Conv; in fun changed_conv cnv = (fn (ct:cterm) => let val thm = cnv ct in if Thm.is_reflexive thm then raise THM ("changed_conv: Not changed",~1,[thm]) else thm end) fun repeat_top_sweep_conv cnv ctxt = repeat_conv (changed_conv (top_sweep_conv cnv ctxt)); end (* Remove duplicate premises (stable) *) fun rem_dup_prems ctxt thm = let val prems = Thm.prems_of thm; val perm = prems |> tag_list 0 |> map swap |> Termtab.make_list |> Termtab.dest |> map snd |> sort (int_ord o apply2 hd) |> flat; val thm' = Drule.rearrange_prems perm thm |> Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true @{thms meta_same_imp_rule}); in thm' end; fun dest_def_eq (Const (@{const_name Pure.eq},_)$l$r) = (l,r) | dest_def_eq (Const (@{const_name HOL.Trueprop},_) $(Const (@{const_name HOL.eq},_)$l$r)) = (l,r) | dest_def_eq t = raise TERM ("No definitional equation",[t]); fun norm_def_thm thm = case Thm.concl_of thm of (Const (@{const_name Pure.eq},_)$_$_) => thm | _ => thm RS eq_reflection; val dt_lhs = dest_def_eq #> fst; val dt_rhs = dest_def_eq #> snd; val dt_params = dt_lhs #> strip_comb #> snd; val dt_head = dt_lhs #> head_of; val dthm_lhs = Thm.concl_of #> dt_lhs; val dthm_rhs = Thm.concl_of #> dt_rhs; val dthm_params = Thm.concl_of #> dt_params; val dthm_head = Thm.concl_of #> dt_head; (* Head of function application (cterm) *) fun chead_of ct = case Thm.term_of ct of (_$_) => chead_of (Thm.dest_fun ct) | _ => ct; val chead_of_thm = norm_def_thm #> Thm.lhs_of #> chead_of; val meta_cong_rl = @{thm "eq_reflection"} OF @{thms "arg_cong"} OF @{thms "meta_eq_to_obj_eq"} fun inst_meta_cong ctxt ct = let val (ct, ctxt') = import_cterm ct ctxt; val mc_thm = meta_cong_rl; val fpat = mc_thm |> Thm.cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg1 |> chead_of; val inst = infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of fpat)), ct)] mc_thm; val inst' = singleton (Variable.export ctxt' ctxt) inst; in inst' end (* Define name\rhs, generate _def theorem. *) fun define_simple name rhs lthy = let (* Import type variables *) val (rhs,lthy) = yield_singleton Variable.importT_terms rhs lthy; val ((ft,(_,def_thm)),lthy) = Local_Theory.define ((Binding.name name,NoSyn), ((Binding.name (Thm.def_name name),[]),rhs)) lthy; in ((ft,def_thm),lthy) end; fun wrap_lthy_result_global f rmap thy = let val lthy = Named_Target.theory_init thy; val (r,lthy) = f lthy; val (r,thy) = Local_Theory.exit_result_global rmap (r,lthy); in (r,thy) end fun wrap_lthy_global f = wrap_lthy_result_global (pair () o f) (K I) #> #2; fun wrap_lthy_result_local f rmap lthy = let - val lthy = Local_Theory.open_target lthy; + val lthy = (snd o Local_Theory.begin_nested) lthy; val (r,lthy) = f lthy; val m = Local_Theory.target_morphism lthy; - val lthy = Local_Theory.close_target lthy; + val lthy = Local_Theory.end_nested lthy; val r = rmap m r; in (r,lthy) end fun wrap_lthy_local f = wrap_lthy_result_local (pair () o f) (K I) #> #2; (* Define name\rhs, yielding constant *) fun define_simple_global name rhs thy = let val lthy = Named_Target.theory_init thy; val (r,lthy) = define_simple name rhs lthy; fun map_res m (t,thm) = (Morphism.term m t,Morphism.thm m thm); val (r,thy) = Local_Theory.exit_result_global (map_res) (r,lthy); in (r,thy) end; (* Define name\rhs, yielding constant *) fun define_simple_local name rhs lthy = let - val lthy = Local_Theory.open_target lthy; + val lthy = (snd o Local_Theory.begin_nested) lthy; val (r,lthy) = define_simple name rhs lthy; val m = Local_Theory.target_morphism lthy; - val lthy = Local_Theory.close_target lthy; + val lthy = Local_Theory.end_nested lthy; fun map_res m (t,thm) = (Morphism.term m t,Morphism.thm m thm); val (r,lthy) = (map_res m r,lthy); in (r,lthy) end; fun map_option _ NONE = NONE | map_option f (SOME a) = SOME (f a); fun revert_abbrevs mpat thy = let val ctxt = Proof_Context.init_global thy; val match_prefix = if Long_Name.is_qualified mpat then mpat else Long_Name.qualify (Context.theory_name thy) mpat; val {const_space, constants, ...} = Sign.consts_of thy |> Consts.dest; val names = Name_Space.extern_entries true ctxt const_space constants |> map_filter (fn ((name, _), (_, SOME _)) => if Long_Name.qualifier name = match_prefix then SOME name else NONE | _ => NONE) val _ = if null names then warning ("ICF_Tools.revert_abbrevs: No names with prefix: " ^ match_prefix) else (); in fold (Sign.revert_abbrev "") names thy end end; \ attribute_setup rem_dup_prems = \ Scan.succeed (Thm.rule_attribute [] (ICF_Tools.rem_dup_prems o Context.proof_of)) \ "Remove duplicate premises" method_setup dup_subgoals = \ Scan.succeed (fn ctxt => SIMPLE_METHOD (PRIMITIVE (ICF_Tools.rem_dup_prems ctxt))) \ "Remove duplicate subgoals" end diff --git a/thys/Constructor_Funs/constructor_funs.ML b/thys/Constructor_Funs/constructor_funs.ML --- a/thys/Constructor_Funs/constructor_funs.ML +++ b/thys/Constructor_Funs/constructor_funs.ML @@ -1,184 +1,184 @@ signature CONSTRUCTOR_FUNS = sig val mk_funs: Ctr_Sugar.ctr_sugar -> local_theory -> local_theory val mk_funs_typ: typ -> local_theory -> local_theory val mk_funs_cmd: string -> local_theory -> local_theory val enabled: bool Config.T val conv: Proof.context -> conv val constructor_funs_plugin: string val setup: theory -> theory end structure Constructor_Funs : CONSTRUCTOR_FUNS = struct val enabled = Attrib.setup_config_bool @{binding "constructor_funs"} (K false) structure Data = Generic_Data ( type T = term list * (int * thm) list * Symtab.set val empty = ([], [], Symtab.empty) fun merge ((ts1, unfolds1, s1), (ts2, unfolds2, s2)) = (ts1 @ ts2, unfolds1 @ unfolds2, Symtab.merge op = (s1, s2)) val extend = I ) fun lenient_unvarify t = (* type variables in records are not schematic *) Logic.unvarify_global t handle TERM _ => t fun mk_funs {T, ctrs, ...} lthy = let val typ_name = fst (dest_Type T) fun mk_fun ctr lthy = let val (name, typ) = dest_Const (lenient_unvarify ctr) val (typs, _) = strip_type typ val len = length typs in if len > 0 then let val base_name = Long_Name.base_name name val binding = Binding.name base_name val args = Name.invent_names (Name.make_context [base_name]) Name.uu typs |> map Free val lhs = list_comb (Free (base_name, typ), args) val rhs = list_comb (Const (name, typ), args) val def = Logic.mk_equals (lhs, rhs) val ((term, (_, def_thm)), lthy') = Specification.definition NONE [] [] ((binding, []), def) lthy val unfold_thm = @{thm Pure.symmetric} OF [Local_Defs.abs_def_rule lthy' def_thm] in (SOME (term, (len, unfold_thm)), lthy') end else (NONE, lthy) end fun morph_unfold phi (len, thm) = (len, Morphism.thm phi thm) fun upd (ts', unfolds') = Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (fn (ts, unfolds, s) => (map (Morphism.term phi) ts' @ ts, map (morph_unfold phi) unfolds' @ unfolds, Symtab.update_new (typ_name, ()) s))) val exists = Symtab.defined (#3 (Data.get (Context.Proof lthy))) typ_name val warn = Pretty.separate "" [Syntax.pretty_typ lthy T, Pretty.str "already processed"] |> Pretty.block val _ = if exists then warning (Pretty.string_of warn) else () in if exists then lthy else - Local_Theory.open_target lthy + (snd o Local_Theory.begin_nested) lthy |> Proof_Context.concealed |> Local_Theory.map_background_naming (Name_Space.mandatory_path typ_name #> Name_Space.mandatory_path "constructor_fun") |> fold_map mk_fun ctrs |>> map_filter I |>> split_list |-> upd - |> Local_Theory.close_target + |> Local_Theory.end_nested end fun mk_funs_typ typ lthy = mk_funs (the (Ctr_Sugar.ctr_sugar_of lthy (fst (dest_Type typ)))) lthy fun mk_funs_cmd s lthy = mk_funs_typ (Proof_Context.read_type_name {proper = true, strict = false} lthy s) lthy fun comb_conv ctxt cv1 cv2 ct = let val (f, xs) = strip_comb (Thm.term_of ct) val f = Thm.cterm_of ctxt f val xs = map (Thm.cterm_of ctxt) xs val f' = cv1 f val xs' = map cv2 xs in fold (fn x => fn f => Thm.combination f x) xs' f' end fun conv ctxt = let val (_, unfolds, _) = Data.get (Context.Proof ctxt) val unfolds = map (apsnd (Thm.transfer' ctxt)) unfolds fun full_conv ct = let val (_, xs) = strip_comb (Thm.term_of ct) val actual_len = length xs fun head_conv ct = let fun can_rewrite (len, thm) = Option.map (pair len) (try (Conv.rewr_conv thm) ct) val _ = get_first can_rewrite unfolds in case get_first can_rewrite unfolds of NONE => Conv.all_conv ct | SOME (target_len, thm) => if target_len = actual_len then Conv.all_conv ct else thm end in comb_conv ctxt head_conv full_conv ct end in full_conv end fun functrans ctxt thms = let val (consts, _, _) = Data.get (Context.Proof ctxt) val conv = Conv.arg_conv (conv ctxt) fun apply_conv thm = let val thm' = Conv.fconv_rule conv thm val prop = Thm.prop_of thm val head = Logic.dest_equals prop |> fst |> strip_comb |> fst val protected = exists (fn const => Pattern.matches (Proof_Context.theory_of ctxt) (const, head)) consts in if protected orelse Thm.prop_of thm aconv Thm.prop_of thm' then (false, thm) else (true, thm') end val (changeds, thms') = split_list (map apply_conv thms) in if exists I changeds then SOME thms' else NONE end val code_functrans = Code_Preproc.simple_functrans (fn ctxt => if Config.get ctxt enabled then functrans ctxt else K NONE) val constructor_funs_plugin = Plugin_Name.declare_setup @{binding constructor_funs} (** setup **) val _ = Outer_Syntax.local_theory @{command_keyword "constructor_funs"} "defines constructor functions for a datatype and sets up the code generator" (Scan.repeat1 Args.embedded_inner_syntax >> fold mk_funs_cmd) val setup = Code_Preproc.add_functrans ("constructor_funs", code_functrans) #> Ctr_Sugar.ctr_sugar_interpretation constructor_funs_plugin (mk_funs_typ o #T) end \ No newline at end of file diff --git a/thys/Dict_Construction/class_graph.ML b/thys/Dict_Construction/class_graph.ML --- a/thys/Dict_Construction/class_graph.ML +++ b/thys/Dict_Construction/class_graph.ML @@ -1,340 +1,340 @@ signature CLASS_GRAPH = sig type selector = typ -> term type node = {class: string, qname: string, selectors: selector Symtab.table, make: typ -> term, data_thms: thm list, cert: typ -> term, cert_thms: thm * thm * thm list} val dict_typ: node -> typ -> typ type edge = {super_selector: selector, subclass: thm} type path = edge list type ev val class_of: ev -> class val node_of: ev -> node val parents_of: ev -> (edge * ev) Symtab.table val find_path': ev -> (ev -> 'a option) -> (path * 'a) option val find_path: ev -> class -> path option val fold_path: path -> typ -> term -> term val ensure_class: class -> local_theory -> (ev * local_theory) val edges: local_theory -> class -> edge Symtab.table option val node: local_theory -> class -> node option val all_edges: local_theory -> edge Symreltab.table val all_nodes: local_theory -> node Symtab.table val pretty_ev: Proof.context -> ev -> Pretty.T (* utilities *) val mangle: string -> string val param_sorts: string -> class -> theory -> class list list val super_classes: class -> theory -> string list end structure Class_Graph: CLASS_GRAPH = struct open Dict_Construction_Util val mangle = translate_string (fn x => if x = "." then "_" else if x = "_" then "__" else x) fun param_sorts tyco class thy = let val algebra = Sign.classes_of thy in Sorts.mg_domain algebra tyco [class] |> map (filter (Class.is_class thy)) end fun super_classes class thy = let val algebra = Sign.classes_of thy in Sorts.super_classes algebra class |> Sorts.minimize_sort algebra |> filter (Class.is_class thy) |> sort fast_string_ord end type selector = typ -> term type node = {class: string, qname: string, selectors: selector Symtab.table, make: typ -> term, data_thms: thm list, cert: typ -> term, cert_thms: thm * thm * thm list} type edge = {super_selector: selector, subclass: thm} type path = edge list abstype ev = Evidence of class * node * (edge * ev) Symtab.table with fun class_of (Evidence (class, _, _)) = class fun node_of (Evidence (_, node, _)) = node fun parents_of (Evidence (_, _, tab)) = tab fun mk_evidence class node tab = Evidence (class, node, tab) fun find_path' ev is_goal = case is_goal ev of SOME a => SOME ([], a) | NONE => let fun f (_, (edge, ev)) = Option.map (apfst (cons edge)) (find_path' ev is_goal) in Symtab.get_first f (parents_of ev) end fun find_path ev goal = find_path' ev (fn ev => if class_of ev = goal then SOME () else NONE) |> Option.map fst fun pretty_ev ctxt (Evidence (class, {qname, ...}, tab)) = let val typ = @{typ 'a} fun mk_super ({super_selector, ...}, super_ev) = Pretty.block [Pretty.str "selector:", Pretty.brk 1, Syntax.pretty_term ctxt (super_selector typ), Pretty.fbrk, pretty_ev ctxt super_ev] val supers = Symtab.dest tab |> map (fn (_, super) => mk_super super) |> Pretty.big_list "super classes" in Pretty.block [Pretty.str "Evidence for ", Syntax.pretty_sort ctxt [class], Pretty.str ": ", Syntax.pretty_typ ctxt (Type (qname, [typ])), Pretty.str (" (qname = " ^ qname ^ ")"), Pretty.fbrk, supers] end end structure Classes = Generic_Data ( type T = (edge Symtab.table * node) Symtab.table val empty = Symtab.empty fun merge (t1, t2) = if Symtab.is_empty t1 andalso Symtab.is_empty t2 then Symtab.empty else error "merging not supported" val extend = I ) fun node lthy class = Symtab.lookup (Classes.get (Context.Proof lthy)) class |> Option.map snd fun edges lthy class = Symtab.lookup (Classes.get (Context.Proof lthy)) class |> Option.map fst val all_nodes = Context.Proof #> Classes.get #> Symtab.map (K snd) val all_edges = Context.Proof #> Classes.get #> Symtab.map (K fst) #> symreltab_of_symtab fun dict_typ {qname, ...} typ = Type (qname, [typ]) fun fold_path path typ = fold (fn {super_selector = s, ...} => fn acc => s typ $ acc) path fun mk_super_selector' qualified qname super_ev typ = let val {class = super_class, qname = super_qname, ...} = node_of super_ev val raw_name = mangle super_class ^ "__super" val name = if qualified then Long_Name.append qname raw_name else raw_name in (name, Type (qname, [typ]) --> Type (super_qname, [typ])) end fun mk_node class info super_evs lthy = let fun print_info ctxt = Pretty.block [Pretty.str "Defining record for class ", Syntax.pretty_sort ctxt [class]] |> Pretty.writeln val name = mangle class ^ "__dict" val qname = Local_Theory.full_name lthy (Binding.name name) val tvar = @{typ 'a} val typ = Type (qname, [tvar]) fun mk_field name ftyp = (Binding.name name, ftyp) val params = #params info |> map (fn (name', ftyp) => let val ftyp' = typ_subst_atomic [(TFree ("'a", [class]), @{typ 'a})] ftyp val field_name = mangle name' ^ "__field" val field = mk_field field_name ftyp' fun sel tvar' = Const (Long_Name.append qname field_name, typ_subst_atomic [(tvar, tvar')] (typ --> ftyp')) in (field, (name', sel)) end) val (fields, selectors) = split_list params val super_params = Symtab.dest super_evs |> map (fn (_, super_ev) => let val {cert = raw_super_cert, qname = super_qname, ...} = node_of super_ev val (field_name, _) = mk_super_selector' false qname super_ev tvar val field = mk_field field_name (Type (super_qname, [tvar])) fun sel typ = Const (mk_super_selector' true qname super_ev typ) fun super_cert dict = raw_super_cert tvar $ (sel tvar $ dict) val raw_edge = (class_of super_ev, sel) in (field, raw_edge, super_cert) end) val (super_fields, raw_edges, super_certs) = split_list3 super_params val all_fields = super_fields @ fields fun make typ' = Const (Long_Name.append qname "Dict", typ_subst_atomic [(tvar, typ')] (map #2 all_fields ---> typ)) val cert_name = name ^ "__cert" val cert_binding = Binding.name cert_name val cert_body = let fun local_param_eq ((_, typ), (name, sel)) dict = HOLogic.mk_eq (sel tvar $ dict, Const (name, typ)) in map local_param_eq params @ super_certs end val cert_var_name = "dict" val cert_term = Abs (cert_var_name, typ, List.foldr HOLogic.mk_conj @{term True} (map (fn x => x (Bound 0)) cert_body)) fun prove_thms (cert, cert_def) lthy = let val var = Free (cert_var_name, typ) fun tac ctxt = Local_Defs.unfold_tac ctxt [cert_def] THEN blast_tac ctxt 1 fun prove prop = Goal.prove_future lthy [cert_var_name] [] prop (fn {context, ...} => tac context) fun mk_dest_props raw_prop = HOLogic.mk_Trueprop (cert $ var) ==> HOLogic.mk_Trueprop (raw_prop var) fun mk_intro_cond raw_prop = HOLogic.mk_Trueprop (raw_prop var) val dests = map (fn raw_prop => prove (mk_dest_props raw_prop)) cert_body val intro = prove (map mk_intro_cond cert_body ===> HOLogic.mk_Trueprop (cert $ var)) val (dests', (intro', lthy')) = note_thms Binding.empty dests lthy ||> note_thm Binding.empty intro val (param_dests, super_dests) = chop (length params) dests' fun pre_edges phi = let fun mk_edge thm (sc, sel) = (sc, {super_selector = sel, subclass = Morphism.thm phi thm}) in Symtab.make (map2 mk_edge super_dests raw_edges) end in ((param_dests, pre_edges, intro'), lthy') end val constructor = (((Binding.empty, Binding.name "Dict"), all_fields), NoSyn) val datatyp = (([(NONE, (@{typ 'a}, @{sort type}))], Binding.name name), NoSyn) val dtspec = (Ctr_Sugar.default_ctr_options, [(((datatyp, [constructor]), (Binding.empty, Binding.empty, Binding.empty)), [])]) val (((raw_cert, raw_cert_def), (param_dests, pre_edges, intro)), (lthy', lthy)) = lthy |> tap print_info |> BNF_FP_Def_Sugar.co_datatypes BNF_Util.Least_FP BNF_LFP.construct_lfp dtspec (* FIXME ideally BNF would return a fp_sugar value right here so that I can avoid constructing long names by hand above *) - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> Local_Theory.define ((cert_binding, NoSyn), ((Thm.def_binding cert_binding, []), cert_term)) |>> apsnd snd |> (fn (raw_cert, lthy) => prove_thms raw_cert lthy |>> pair raw_cert) - ||> `Local_Theory.close_target + ||> `Local_Theory.end_nested val phi = Proof_Context.export_morphism lthy lthy' fun cert typ = subst_TVars [(("'a", 0), typ)] (Morphism.term phi raw_cert) val cert_def = Morphism.thm phi raw_cert_def val edges = pre_edges phi val param_dests' = map (Morphism.thm phi) param_dests val intro' = Morphism.thm phi intro val data_thms = BNF_FP_Def_Sugar.fp_sugar_of lthy' qname |> the |> #fp_ctr_sugar |> #ctr_sugar |> #sel_thmss |> flat |> map safe_mk_meta_eq val node = {class = class, qname = qname, selectors = Symtab.make selectors, make = make, data_thms = data_thms, cert = cert, cert_thms = (cert_def, intro', param_dests')} in (node, edges, lthy') end fun ensure_class class lthy = if not (Class.is_class (Proof_Context.theory_of lthy) class) then error ("not a proper class: " ^ class) else let val thy = Proof_Context.theory_of lthy val super_classes = super_classes class thy fun collect_super mk_node = let val (super_evs, lthy') = fold_map ensure_class super_classes lthy val raw_tab = Symtab.make (super_classes ~~ super_evs) val (node, edges, lthy'') = mk_node raw_tab lthy' val tab = zip_symtabs pair edges raw_tab val ev = mk_evidence class node tab in (ev, edges, lthy'') end in case Symtab.lookup (Classes.get (Context.Proof lthy)) class of SOME (edge_tab, node) => if super_classes = Symtab.keys edge_tab then let val (ev, _, lthy') = collect_super (fn _ => fn lthy => (node, edge_tab, lthy)) in (ev, lthy') end else (* This happens when a new subclass relationship is established which subsumes or augments previous superclasses. *) error "class with different super classes" | NONE => let val ax_info = Axclass.get_info thy class val (ev, edges, lthy') = collect_super (mk_node class ax_info) val upd = Symtab.update_new (class, (edges, node_of ev)) in (ev, Local_Theory.declaration {pervasive = false, syntax = false} (K (Classes.map upd)) lthy') end end end diff --git a/thys/Dict_Construction/dict_construction.ML b/thys/Dict_Construction/dict_construction.ML --- a/thys/Dict_Construction/dict_construction.ML +++ b/thys/Dict_Construction/dict_construction.ML @@ -1,935 +1,935 @@ signature DICT_CONSTRUCTION = sig datatype cert_proof = Cert | Skip type const type 'a sccs = (string * 'a) list list val annotate_code_eqs: local_theory -> string list -> (const sccs * local_theory) val new_names: local_theory -> const sccs -> (string * const) sccs val symtab_of_sccs: 'a sccs -> 'a Symtab.table val axclass: class -> local_theory -> Class_Graph.node * local_theory val instance: (string * const) Symtab.table -> string -> class -> local_theory -> term * local_theory val term: term Symreltab.table -> (string * const) Symtab.table -> term -> local_theory -> (term * local_theory) val consts: (string * const) Symtab.table -> cert_proof -> (string * const) list -> local_theory -> local_theory (* certification *) type const_info = {fun_info: Function.info option, inducts: thm list option, base_thms: thm list, base_certs: thm list, simps: thm list, code_thms: thm list, (* old defining theorems *) congs: thm list option} type fun_target = (string * class) list * (term * term) type dict_thms = {base_thms: thm list, def_thm: thm} type dict_target = (string * class) list * (term * string * class) val prove_fun_cert: fun_target list -> const_info -> cert_proof -> local_theory -> thm list val prove_dict_cert: dict_target -> dict_thms -> local_theory -> thm val the_info: Proof.context -> string -> const_info (* utilities *) val normalizer_conv: Proof.context -> conv val cong_of_const: Proof.context -> string -> thm option val get_code_eqs: Proof.context -> string -> thm list val group_code_eqs: Proof.context -> string list -> (string * (((string * sort) list * typ) * ((term list * term) * thm option) list)) list list end structure Dict_Construction: DICT_CONSTRUCTION = struct open Class_Graph open Dict_Construction_Util (* FIXME copied from skip_proof.ML *) val (_, make_thm_cterm) = Context.>>> (Context.map_theory_result (Thm.add_oracle (@{binding cert_oracle}, I))) fun make_thm ctxt prop = make_thm_cterm (Thm.cterm_of ctxt prop) fun cheat_tac ctxt i st = resolve_tac ctxt [make_thm ctxt (Var (("A", 0), propT))] i st (** utilities **) val normalizer_conv = Axclass.overload_conv fun cong_of_const ctxt name = let val head = Thm.concl_of #> Logic.dest_equals #> fst #> strip_comb #> fst #> dest_Const #> fst fun applicable thm = try head thm = SOME name in Function_Context_Tree.get_function_congs ctxt |> filter applicable |> try hd end fun group_code_eqs ctxt consts = let val thy = Proof_Context.theory_of ctxt val graph = #eqngr (Code_Preproc.obtain true { ctxt = ctxt, consts = consts, terms = [] }) fun mk_eqs name = name |> Code_Preproc.cert graph |> Code.equations_of_cert thy ||> these ||> map (apsnd fst o apfst (apsnd fst o apfst (map fst))) |> pair name in map (map mk_eqs) (rev (Graph.strong_conn graph)) end fun get_code_eqs ctxt const = AList.lookup op = (flat (group_code_eqs ctxt [const])) const |> the |> snd |> map snd |> cat_options |> map (Conv.fconv_rule (normalizer_conv ctxt)) (** certification **) datatype cert_proof = Cert | Skip type const_info = {fun_info: Function.info option, inducts: thm list option, base_thms: thm list, base_certs: thm list, simps: thm list, code_thms: thm list, congs: thm list option} fun map_const_info f1 f2 f3 f4 f5 f6 f7 {fun_info, inducts, base_thms, base_certs, simps, code_thms, congs} = {fun_info = f1 fun_info, inducts = f2 inducts, base_thms = f3 base_thms, base_certs = f4 base_certs, simps = f5 simps, code_thms = f6 code_thms, congs = f7 congs} fun morph_const_info phi = map_const_info (Option.map (Function_Common.transform_function_data phi)) (Option.map (map (Morphism.thm phi))) (map (Morphism.thm phi)) (map (Morphism.thm phi)) (map (Morphism.thm phi)) I (* sic *) (Option.map (map (Morphism.thm phi))) type fun_target = (string * class) list * (term * term) type dict_thms = {base_thms: thm list, def_thm: thm} type dict_target = (string * class) list * (term * string * class) fun fun_cert_tac base_thms base_certs simps code_thms = SOLVED' o Subgoal.FOCUS (fn {prems, context = ctxt, concl, ...} => let val _ = if_debug ctxt (fn () => tracing ("Proving " ^ Syntax.string_of_term ctxt (Thm.term_of concl))) fun is_ih prem = Thm.prop_of prem |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |> can HOLogic.dest_eq val (ihs, certs) = partition is_ih prems val super_certs = all_edges ctxt |> Symreltab.dest |> map (#subclass o snd) val param_dests = all_nodes ctxt |> Symtab.dest |> maps (#3 o #cert_thms o snd) val congs = Function_Context_Tree.get_function_congs ctxt @ map safe_mk_meta_eq @{thms cong} val simp_context = (clear_simpset ctxt) addsimps (certs @ super_certs @ base_certs @ base_thms @ param_dests) addloop ("overload", CONVERSION o changed_conv o Axclass.overload_conv) val ihs = map (Simplifier.asm_full_simplify simp_context) ihs val ih_tac = resolve_tac ctxt ihs THEN_ALL_NEW (TRY' (SOLVED' (Simplifier.asm_full_simp_tac simp_context))) val unfold_new = ANY' (map (CONVERSION o rewr_lhs_head_conv) simps) val normalize = CONVERSION (normalizer_conv ctxt) val unfold_old = ANY' (map (CONVERSION o rewr_rhs_head_conv) code_thms) val simp = CONVERSION (lhs_conv (Simplifier.asm_full_rewrite simp_context)) fun walk_congs i = i |> ((resolve_tac ctxt @{thms refl} ORELSE' SOLVED' (Simplifier.asm_full_simp_tac simp_context) ORELSE' ih_tac ORELSE' Method.assm_tac ctxt ORELSE' (resolve_tac ctxt @{thms meta_eq_to_obj_eq} THEN' fo_resolve_tac congs ctxt)) THEN_ALL_NEW walk_congs) val tacs = [unfold_new, normalize, unfold_old, simp, walk_congs] in EVERY' tacs 1 end) fun dict_cert_tac class def_thm base_thms = SOLVED' o Subgoal.FOCUS (fn {prems, context = ctxt, ...} => let val (intro, sels) = case node ctxt class of SOME {cert_thms = (_, intro, _), data_thms = sels, ...} => (intro, sels) | NONE => error ("class " ^ class ^ " is not defined") val apply_intro = resolve_tac ctxt [intro] val unfold_dict = CONVERSION (Conv.rewr_conv def_thm |> Conv.arg_conv |> lhs_conv) val normalize = CONVERSION (normalizer_conv ctxt) val smash_sels = CONVERSION (lhs_conv (Conv.rewrs_conv sels)) val solve = resolve_tac ctxt (@{thm HOL.refl} :: base_thms) val finally = resolve_tac ctxt prems val tacs = [apply_intro, unfold_dict, normalize, smash_sels, solve, finally] in EVERY (map (ALLGOALS' ctxt) tacs) end) fun prepare_dicts classes names lthy = let val sorts = Symtab.make_list classes fun mk_dicts (param_name, (tvar, class)) = case node lthy class of NONE => error ("unknown class " ^ class) | SOME {cert, qname, ...} => let val sort = the (Symtab.lookup sorts tvar) val param = Free (param_name, Type (qname, [TFree (tvar, sort)])) in (param, HOLogic.mk_Trueprop (cert dummyT $ param)) end val dict_names = Name.invent_names names "a" classes val names = fold Name.declare (map fst dict_names) names val (dict_params, prems) = split_list (map mk_dicts dict_names) in (dict_params, prems, names) end fun prepare_fun_goal targets lthy = let fun mk_eq (classes, (lhs, rhs)) names = let val (lhs_name, _) = dest_Const lhs val (rhs_name, rhs_typ) = dest_Const rhs val (dict_params, prems, names) = prepare_dicts classes names lthy val param_names = fst (strip_type rhs_typ) |> map (K dummyT) |> Name.invent_names names "a" val names = fold Name.declare (map fst param_names) names val params = map Free param_names val lhs = list_comb (Const (lhs_name, dummyT), dict_params @ params) val rhs = list_comb (Const (rhs_name, dummyT), params) val eq = Const (@{const_name HOL.eq}, dummyT) $ lhs $ rhs val all_params = dict_params @ params val eq :: rest = Syntax.check_terms lthy (eq :: prems @ all_params) val (prems, all_params) = unappend (prems, all_params) rest val eq = if is_some (Axclass.inst_of_param (Proof_Context.theory_of lthy) rhs_name) then Thm.cterm_of lthy eq |> conv_result (Conv.arg_conv (normalizer_conv lthy)) else eq val prop = prems ===> HOLogic.mk_Trueprop eq in ((all_params, prop), names) end in fold_map mk_eq targets Name.context |> fst |> split_list end fun prepare_dict_goal (classes, (term, _, class)) lthy = let val cert = case node lthy class of NONE => error ("unknown class " ^ class) | SOME {cert, ...} => cert dummyT val names = Name.context val (dict_params, prems, _) = prepare_dicts classes names lthy val (term_name, _) = dest_Const term val dict = list_comb (Const (term_name, dummyT), dict_params) val prop = prems ===> HOLogic.mk_Trueprop (cert $ dict) val prop :: dict_params = Syntax.check_terms lthy (prop :: dict_params) in (dict_params, prop) end fun prove_fun_cert targets {inducts, base_thms, base_certs, simps, code_thms, ...} proof lthy = let (* the props contain dictionary certs as prems we can't exclude them from the induction because the dicts are part of the function definition excluding them would mean that applying the induction rules becomes tricky or impossible proper fix would be if fun, akin to inductive, supported a "for" clause that marks parameters as "not changing" *) val (argss, props) = prepare_fun_goal targets lthy val frees = flat argss |> map (fst o dest_Free) (* we first prove the extensional variant (easier to prove), and then derive the contracted variant abs_def can't deal with premises, so we use our own version here *) val tac = case proof of Cert => fun_cert_tac base_thms base_certs simps code_thms | Skip => cheat_tac val long_thms = prove_common' lthy frees [] props (fn {context, ...} => maybe_induct_tac inducts argss [] context THEN ALLGOALS' context (tac context)) in map (contract lthy) long_thms end fun prove_dict_cert target {base_thms, def_thm} lthy = let val (args, prop) = prepare_dict_goal target lthy val frees = map (fst o dest_Free) args val (_, (_, _, class)) = target in prove' lthy frees [] prop (fn {context, ...} => dict_cert_tac class def_thm base_thms context 1) end (** background data **) type definitions = {instantiations: (term * thm) Symreltab.table, (* key: (class, tyco) *) constants: (string * (thm option * const_info)) Symtab.table (* key: constant name *) } structure Definitions = Generic_Data ( type T = definitions val empty = {instantiations = Symreltab.empty, constants = Symtab.empty} val extend = I fun merge ({instantiations = i1, constants = c1}, {instantiations = i2, constants = c2}) = if Symreltab.is_empty i1 andalso Symtab.is_empty c1 andalso Symreltab.is_empty i2 andalso Symtab.is_empty c2 then empty else error "merging not supported" ) fun map_definitions map_insts map_consts = Definitions.map (fn {instantiations, constants} => {instantiations = map_insts instantiations, constants = map_consts constants}) fun the_info ctxt name = Symtab.lookup (#constants (Definitions.get (Context.Proof ctxt))) name |> the |> snd |> snd fun add_instantiation (class, tyco) term cert = let fun upd phi = map_definitions (fn tab => if Symreltab.defined tab (class, tyco) then error ("Duplicate instantiation " ^ quote tyco ^ " :: " ^ quote class) else tab |> Symreltab.update ((class, tyco), (Morphism.term phi term, Morphism.thm phi cert))) I in Local_Theory.declaration {pervasive = false, syntax = false} upd end fun add_constant name name' (cert, info) lthy = let val qname = Local_Theory.full_name lthy (Binding.name name') fun upd phi = map_definitions I (fn tab => if Symtab.defined tab name then error ("Duplicate constant " ^ quote name) else tab |> Symtab.update (name, (qname, (Option.map (Morphism.thm phi) cert, morph_const_info phi info)))) in Local_Theory.declaration {pervasive = false, syntax = false} upd lthy |> Local_Theory.note ((Binding.empty, @{attributes [dict_construction_specs]}), #simps info) |> snd end (** classes **) fun axclass class = ensure_class class #>> node_of (** grouping and annotating constants **) datatype const = Fun of {dicts: ((string * class) * typ) list, certs: term list, param_typs: typ list, typ: typ, (* typified *) new_typ: typ, eqs: {params: term list, rhs: term, thm: thm} list, info: Function_Common.info option, cong: thm option} | Constructor | Classparam of {class: class, typ: typ, (* varified *) selector: term (* varified *)} type 'a sccs = (string * 'a) list list fun symtab_of_sccs x = Symtab.make (flat x) fun raw_dict_params tparams lthy = let fun mk_dict tparam class lthy = let val (node, lthy') = axclass class lthy val targ = TFree (tparam, @{sort type}) val typ = dict_typ node targ val cert = #cert node targ in ((((tparam, class), typ), cert), lthy') end fun mk_dicts (tparam, sort) = fold_map (mk_dict tparam) (filter (Class.is_class (Proof_Context.theory_of lthy)) sort) in fold_map mk_dicts tparams lthy |>> flat end fun dict_params context dicts = let fun dict_param ((_, class), typ) = Name.variant (mangle class) #>> rpair typ #>> Free in fold_map dict_param dicts context end fun get_sel class param typ lthy = let val ({selectors, ...}, lthy') = axclass class lthy in case Symtab.lookup selectors param of NONE => error ("unknown class parameter " ^ param) | SOME sel => (sel typ, lthy') end fun annotate_const name ((tparams, typ), raw_eqs) lthy = if Code.is_constr (Proof_Context.theory_of lthy) name then ((name, Constructor), lthy) else if null raw_eqs then (* this detection is reliable, because code equations with overloaded heads are not allowed *) let val (_, class) = the_single tparams ||> the_single val (selector, thy') = get_sel class name (TVar (("'a", 0), @{sort type})) lthy val typ = range_type (fastype_of selector) in ((name, Classparam {class = class, typ = typ, selector = selector}), thy') end else let val info = try (Function.get_info lthy) (Const (name, typ)) val cong = cong_of_const lthy name val ((raw_dicts, certs), lthy') = raw_dict_params tparams lthy |>> split_list val dict_typs = map snd raw_dicts val typ' = typify_typ typ fun mk_eq ((raw_params, rhs), SOME thm) = let val norm = normalizer_conv lthy' val transform = Thm.cterm_of lthy' #> conv_result norm #> typify val params = map transform raw_params in if has_duplicates (op =) (flat (map all_frees' params)) then (warning "ignoring code equation with non-linear pattern"; NONE) else SOME {params = params, rhs = rhs, thm = Conv.fconv_rule norm thm} end | mk_eq _ = error "no theorem" val const = Fun {dicts = raw_dicts, certs = certs, typ = typ', param_typs = binder_types typ', new_typ = dict_typs ---> typ', eqs = map_filter mk_eq raw_eqs, info = info, cong = cong} in ((name, const), lthy') end fun annotate_code_eqs lthy consts = fold_map (fold_map (uncurry annotate_const)) (group_code_eqs lthy consts) lthy (** instances and terms **) fun mk_path [] _ _ lthy = (NONE, lthy) | mk_path ((class, term) :: rest) typ goal lthy = let val (ev, lthy') = ensure_class class lthy in case find_path ev goal of SOME path => (SOME (fold_path path typ term), lthy') | NONE => mk_path rest typ goal lthy' end fun instance consts tyco class lthy = case Symreltab.lookup (#instantiations (Definitions.get (Context.Proof lthy))) (class, tyco) of SOME (inst, _) => (inst, lthy) | NONE => let val thy = Proof_Context.theory_of lthy val tparam_sorts = param_sorts tyco class thy fun print_info ctxt = let val tvars = Name.invent_list [] Name.aT (length tparam_sorts) ~~ tparam_sorts |> map TFree in [Pretty.str "Defining instance ", Syntax.pretty_typ ctxt (Type (tyco, tvars)), Pretty.str " :: ", Syntax.pretty_sort ctxt [class]] |> Pretty.block |> Pretty.writeln end val ({make, ...}, lthy) = axclass class lthy val name = mangle class ^ "__instance__" ^ mangle tyco val tparams = Name.invent_names Name.context Name.aT tparam_sorts val ((dict_params, _), lthy) = raw_dict_params tparams lthy |>> map fst |>> dict_params (Name.make_context [name]) val dict_context = Symreltab.make (flat_right tparams ~~ dict_params) val {params, ...} = Axclass.get_info thy class val (super_fields, lthy) = fold_map (obtain_dict dict_context consts (Type (tyco, map TFree tparams))) (super_classes class thy) lthy val tparams' = map (TFree o rpair @{sort type} o fst) tparams val typ_inst = (TFree ("'a", [class]), Type (tyco, tparams')) fun mk_field (field, typ) = let val param = Axclass.param_of_inst thy (field, tyco) (* check: did we already define all required fields? *) (* if not: abort (else we would run into an infinite loop) *) val _ = case Symtab.lookup (#constants (Definitions.get (Context.Proof lthy))) param of NONE => (* necessary for zero_nat *) if Code.is_constr thy param then () else error ("cyclic dependency: " ^ param ^ " not yet defined in the definition of " ^ tyco ^ " :: " ^ class) | SOME _ => () in term dict_context consts (Const (param, typ_subst_atomic [typ_inst] typ)) end val (fields, lthy) = fold_map mk_field params lthy val rhs = list_comb (make (Type (tyco, tparams')), super_fields @ fields) val typ = map fastype_of dict_params ---> fastype_of rhs val head = Free (name, typ) val lhs = list_comb (head, dict_params) val term = Logic.mk_equals (lhs, rhs) val (def, (lthy', lthy)) = lthy |> tap print_info - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> define_params_nosyn term - ||> `Local_Theory.close_target + ||> `Local_Theory.end_nested val phi = Proof_Context.export_morphism lthy lthy' val def = Morphism.thm phi def val base_thms = Definitions.get (Context.Proof lthy') |> #constants |> Symtab.dest |> map (apsnd fst o snd) |> map_filter snd val target = (flat_right tparams, (Morphism.term phi head, tyco, class)) val args = {base_thms = base_thms, def_thm = def} val thm = prove_dict_cert target args lthy' val const = Const (Local_Theory.full_name lthy' (Binding.name name), typ) in (const, add_instantiation (class, tyco) const thm lthy') end and obtain_dict dict_context consts = let val dict_context' = Symreltab.dest dict_context fun for_class (Type (tyco, args)) class lthy = let val inst_param_sorts = param_sorts tyco class (Proof_Context.theory_of lthy) val (raw_inst, lthy') = instance consts tyco class lthy val (const_name, _) = dest_Const raw_inst val (inst_args, lthy'') = fold_map for_sort (inst_param_sorts ~~ args) lthy' val head = Sign.mk_const (Proof_Context.theory_of lthy'') (const_name, args) in (list_comb (head, flat inst_args), lthy'') end | for_class (TFree (name, _)) class lthy = let val available = map_filter (fn ((tp, class), term) => if tp = name then SOME (class, term) else NONE) dict_context' val (path, lthy') = mk_path available (TFree (name, @{sort type})) class lthy in case path of SOME term => (term, lthy') | NONE => error "no path found" end | for_class (TVar _) _ _ = error "unexpected type variable" and for_sort (sort, typ) = fold_map (for_class typ) sort in for_class end and term dict_context consts term lthy = let fun traverse (t as Const (name, typ)) lthy = (case Symtab.lookup consts name of NONE => error ("unknown constant " ^ name) | SOME (_, Constructor) => (typify t, lthy) | SOME (_, Classparam {class, typ = typ', selector}) => let val subst = Sign.typ_match (Proof_Context.theory_of lthy) (typ', typ) Vartab.empty val (_, targ) = the (Vartab.lookup subst ("'a", 0)) val (dict, lthy') = obtain_dict dict_context consts targ class lthy in (subst_TVars [(("'a", 0), targ)] selector $ dict, lthy') end | SOME (name', Fun {dicts = dicts, typ = typ', new_typ, ...}) => let val subst = Type.raw_match (Logic.varifyT_global typ', typ) Vartab.empty |> Vartab.dest |> map (apsnd snd) fun lookup tparam = the (AList.lookup (op =) subst (tparam, 0)) val (dicts, lthy') = fold_map (uncurry (obtain_dict dict_context consts o lookup)) (map fst dicts) lthy val typ = typ_subst_TVars subst (Logic.varifyT_global new_typ) val head = case Symtab.lookup (#constants (Definitions.get (Context.Proof lthy))) name of NONE => Free (name', typ) | SOME (n, _) => Const (n, typ) val res = list_comb (head, dicts) in (res, lthy') end) | traverse (f $ x) lthy = let val (f', lthy') = traverse f lthy val (x', lthy'') = traverse x lthy' in (f' $ x', lthy'') end | traverse (Abs (name, typ, term)) lthy = let val (term', lthy') = traverse term lthy in (Abs (name, typify_typ typ, term'), lthy') end | traverse (Free (name, typ)) lthy = (Free (name, typify_typ typ), lthy) | traverse (Var (name, typ)) lthy = (Var (name, typify_typ typ), lthy) | traverse (Bound n) lthy = (Bound n, lthy) in traverse term lthy end (** group of constants **) fun new_names lthy consts = let val (all_names, all_consts) = split_list (flat consts) val all_frees = map (fn Fun {eqs, ...} => eqs | _ => []) all_consts |> flat |> map #params |> flat |> map all_frees' |> flat val context = fold Name.declare (all_names @ all_frees) (Variable.names_of lthy) fun new_name (name, const) context = let val (name', context') = Name.variant (mangle name) context in ((name, (name', const)), context') end in fst (fold_map (fold_map new_name) consts context) end fun consts consts proof group lthy = let val fun_config = Function_Common.FunctionConfig {sequential=true, default=NONE, domintros=false, partials=false} fun pat_completeness_auto ctxt = Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt val all_names = map fst group val pretty_consts = map (pretty_const lthy) all_names |> Pretty.commas fun print_info msg = Pretty.str (msg ^ " ") :: pretty_consts |> Pretty.block |> Pretty.writeln val _ = print_info "Redefining constant(s)" fun process_eqs (name, Fun {dicts, param_typs, new_typ, eqs, info, cong, ...}) lthy = let val new_name = case Symtab.lookup consts name of NONE => error ("no new name for " ^ name) | SOME (n, _) => n val all_frees = map #params eqs |> flat |> map all_frees' |> flat val context = Name.make_context (all_names @ all_frees) val (dict_params, context') = dict_params context dicts fun adapt_params param_typs params = let val real_params = dict_params @ params val ext_params = drop (length params) param_typs |> map typify_typ |> Name.invent_names context' "e0" |> map Free in (real_params, ext_params) end fun mk_eq {params, rhs, thm} lthy = let val (real_params, ext_params) = adapt_params param_typs params val lhs' = list_comb (Free (new_name, new_typ), real_params @ ext_params) val (rhs', lthy') = term (Symreltab.make (map fst dicts ~~ dict_params)) consts rhs lthy val rhs'' = list_comb (rhs', ext_params) in ((HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'')), thm), lthy') end val is_fun = length param_typs + length dicts > 0 in fold_map mk_eq eqs lthy |>> rpair (new_typ, is_fun) |>> SOME |>> pair ((name, new_name, map fst dicts), {info = info, cong = cong}) end | process_eqs (name, _) lthy = ((((name, name, []), {info = NONE, cong = NONE}), NONE), lthy) val (items, lthy') = fold_map process_eqs group lthy val ((metas, infos), ((eqs, code_thms), (new_typs, is_funs))) = items |> map_filter (fn (meta, eqs) => Option.map (pair meta) eqs) |> split_list ||> split_list ||> apfst (flat #> split_list #>> map typify) ||> apsnd split_list |>> split_list val _ = if_debug lthy (fn () => if null code_thms then () else map (Syntax.pretty_term lthy o Thm.prop_of) code_thms |> Pretty.big_list "Equations:" |> Pretty.string_of |> tracing) val is_fun = case distinct (op =) is_funs of [b] => b | [] => false | _ => error "unsupported feature: mixed non-function and function definitions" fun mk_binding (_, new_name, _) typ = (Binding.name new_name, SOME typ, NoSyn) val bindings = map2 mk_binding metas new_typs val {constants, instantiations} = Definitions.get (Context.Proof lthy') val base_thms = Symtab.dest constants |> map (apsnd fst o snd) |> map_filter snd val base_certs = Symreltab.dest instantiations |> map (snd o snd) val consts = Sign.consts_of (Proof_Context.theory_of lthy') fun prove_eq_fun (info as {simps = SOME simps, fs, inducts = SOME inducts, ...}) lthy = let fun mk_target (name, _, classes) new = (classes, (new, Const (Consts.the_const consts name))) val targets = map2 mk_target metas fs val args = {fun_info = SOME info, inducts = SOME inducts, simps = simps, base_thms = base_thms, base_certs = base_certs, code_thms = code_thms, congs = NONE} in (prove_fun_cert targets args proof lthy, args) end fun prove_eq_def defs lthy = let fun mk_target (name, _, classes) new = (classes, (new, Const (Consts.the_const consts name))) val targets = map2 mk_target metas (map (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) defs) val args = {fun_info = NONE, inducts = NONE, simps = defs, base_thms = base_thms, base_certs = base_certs, code_thms = code_thms, congs = NONE} in (prove_fun_cert targets args proof lthy, args) end fun add_constants ((((name, name', _), _), SOME _) :: xs) ((thm :: thms), info) = add_constant name name' (SOME thm, info) #> add_constants xs (thms, info) | add_constants ((((name, name', _), _), NONE) :: xs) (thms, info) = add_constant name name' (NONE, info) #> add_constants xs (thms, info) | add_constants [] _ = I fun prove_termination new_info ctxt = let val termination_ctxt = ctxt addsimps (@{thms equal} @ base_thms) addloop ("overload", CONVERSION o changed_conv o Axclass.overload_conv) val fallback_tac = Function_Common.termination_prover_tac true termination_ctxt val tac = case try hd (cat_options (map #info infos)) of SOME old_info => HEADGOAL (Transfer_Termination.termination_tac new_info old_info ctxt) | NONE => no_tac in Function.prove_termination NONE (tac ORELSE fallback_tac) ctxt end fun prove_cong data lthy = let fun rewr_cong thm cong = if Thm.nprems_of thm > 0 then (warning "No fundef_cong rule can be derived; this will likely not work later"; NONE) else (print_info "Porting fundef_cong rule for "; SOME (Local_Defs.fold lthy [thm] cong)) val congs' = map2 (Option.mapPartial o rewr_cong) (fst data) (map #cong infos) |> cat_options fun add_congs phi = fold Function_Context_Tree.add_function_cong (map (Morphism.thm phi) congs') val data' = apsnd (map_const_info I I I I I I (K (SOME congs'))) data in (data', Local_Theory.declaration {pervasive = false, syntax = false} add_congs lthy) end fun mk_fun lthy = let val specs = map (fn eq => (((Binding.empty, []), eq), [], [])) eqs val (info, lthy') = Function.add_function bindings specs fun_config pat_completeness_auto lthy |-> prove_termination val simps = the (#simps info) val (_, lthy'') = (* [simp del] is required because otherwise non-matching function definitions (e.g. divmod_nat) make the simplifier loop separate step because otherwise we'll get tons of warnings because the psimp rules are not added to the simpset *) Local_Theory.note ((Binding.empty, @{attributes [simp del]}), simps) lthy' fun prove_eq phi = prove_eq_fun (Function_Common.transform_function_data phi info) in (((simps, #inducts info), prove_eq), lthy'') end fun mk_def lthy = let val (defs, lthy') = fold_map define_params_nosyn eqs lthy fun prove_eq phi = prove_eq_def (map (Morphism.thm phi) defs) in (((defs, NONE), prove_eq), lthy') end in if null eqs then lthy' else let (* the redefinition itself doesn't have a sort constraint, but the equality prop may have one; hence the proof needs to happen after exiting the local theory target conceptually, everything happening locally would be great, but the type checker won't allow us to add sort constraints to TFrees after they have been declared *) val ((side, prove_eq), (lthy', lthy)) = lthy' - |> Local_Theory.open_target + |> (snd o Local_Theory.begin_nested) |> (if is_fun then mk_fun else mk_def) |-> (fn ((simps, inducts), prove_eq) => apfst (rpair prove_eq) o Side_Conditions.mk_side simps inducts) - ||> `Local_Theory.close_target + ||> `Local_Theory.end_nested val phi = Proof_Context.export_morphism lthy lthy' in lthy' |> `(prove_eq phi) |>> apfst (on_thms_complete (fn () => print_info "Proved equivalence for")) |-> prove_cong |-> add_constants items end end fun const_raw (binding, raw_consts) proof lthy = let val _ = if proof = Skip then warning "Skipping certificate proofs" else () val (name, _) = Syntax.read_terms lthy raw_consts |> map dest_Const |> split_list val (eqs, lthy) = annotate_code_eqs lthy name val tab = symtab_of_sccs (new_names lthy eqs) val lthy = fold (consts tab proof) eqs lthy val {instantiations, constants} = Definitions.get (Context.Proof lthy) val thms = map (snd o snd) (Symreltab.dest instantiations) @ map_filter (fst o snd o snd) (Symtab.dest constants) in snd (Local_Theory.note (binding, thms) lthy) end (** setup **) val parse_flags = Scan.optional (Args.parens (Parse.reserved "skip" >> K Skip)) Cert val _ = Outer_Syntax.local_theory @{command_keyword "declassify"} "redefines a constant after applying the dictionary construction" (parse_flags -- Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.const >> (fn ((flags, def_binding), consts) => const_raw (def_binding, consts) flags)) end \ No newline at end of file diff --git a/thys/Lazy_Case/lazy_case.ML b/thys/Lazy_Case/lazy_case.ML --- a/thys/Lazy_Case/lazy_case.ML +++ b/thys/Lazy_Case/lazy_case.ML @@ -1,193 +1,193 @@ signature LAZY_CASE = sig val lazify: Ctr_Sugar.ctr_sugar -> local_theory -> local_theory val lazify_typ: typ -> local_theory -> local_theory val lazify_cmd: string -> local_theory -> local_theory val lazy_case_plugin: string val setup: theory -> theory end structure Lazy_Case : LAZY_CASE = struct structure Data = Generic_Data ( type T = Symtab.set val empty = Symtab.empty val extend = I val merge = Symtab.merge op = ) fun init [] = error "empty list" | init [_] = [] | init (x :: xs) = x :: init xs fun lazify {T, casex, ctrs, case_thms, case_cong, ...} lthy = let val is_fun = can dest_funT val typ_name = fst (dest_Type T) val len = length ctrs val idxs = 0 upto len - 1 val (name, typ) = dest_Const casex ||> Logic.unvarifyT_global val (typs, _) = strip_type typ val exists = Symtab.defined (Data.get (Context.Proof lthy)) typ_name val warn = Pretty.separate "" [Syntax.pretty_typ lthy T, Pretty.str "already lazified"] |> Pretty.block val _ = if exists then warning (Pretty.string_of warn) else () in (* for records, casex is the dummy pattern *) if Term.is_dummy_pattern casex orelse forall is_fun (init typs) orelse exists then lthy else let val arg_typs = init typs fun apply_to_unit typ idx = if is_fun typ then (typ, Bound idx) else (@{typ unit} --> typ, Bound idx $ @{term "()"}) val (arg_typs', args) = split_list (map2 apply_to_unit arg_typs (rev idxs)) val def = list_comb (Const (name, typ), args) |> fold_rev Term.abs (map (pair "c") arg_typs') val binding = Binding.name "case_lazy" val ((term, thm), (lthy', lthy)) = - Local_Theory.open_target lthy + (snd o Local_Theory.begin_nested) lthy |> Proof_Context.concealed |> Local_Theory.map_background_naming (Name_Space.mandatory_path typ_name) |> Local_Theory.define ((binding, NoSyn), ((Thm.def_binding binding, []), def)) |>> apsnd snd - ||> `Local_Theory.close_target + ||> `Local_Theory.end_nested val phi = Proof_Context.export_morphism lthy lthy' val thm' = Morphism.thm phi thm val term' = Logic.unvarify_global (Morphism.term phi term) fun defs_tac ctxt idx = Local_Defs.unfold_tac ctxt [thm', nth case_thms idx] THEN HEADGOAL (resolve_tac ctxt @{thms refl}) val frees = fastype_of term' |> strip_type |> fst |> init val frees_f = Name.invent_names Name.context "f0" frees val frees_g = Name.invent_names Name.context "g0" frees val fs = map Free frees_f val gs = map Free frees_g fun mk_def_goal ctr idx = let val (name, len) = dest_Const ctr ||> strip_type ||> fst ||> length val frees = Name.invent Name.context "p0" len val args = map (Free o rpair dummyT) frees val ctr_val = list_comb (Const (name, dummyT), args) val lhs = list_comb (term', fs) $ ctr_val val rhs = if len = 0 then nth fs idx $ @{term "()"} else list_comb (nth fs idx, args) in (frees, HOLogic.mk_Trueprop (Syntax.check_term lthy' (HOLogic.mk_eq (lhs, rhs)))) end fun prove_defs (frees', goal) idx = Goal.prove_future lthy' (map fst frees_f @ frees') [] goal (fn {context, ...} => defs_tac context idx) val def_thms = map2 prove_defs (map2 mk_def_goal ctrs idxs) idxs val frees = Name.invent_names Name.context "q0" arg_typs val unfold_goal = let val lhs = list_comb (Const (name, typ), map Free frees) fun mk_abs (name, typ) = if is_fun typ then Free (name, typ) else Abs ("u", @{typ unit}, Free (name, typ)) val rhs = list_comb (Const (fst (dest_Const term'), dummyT), map mk_abs frees) in HOLogic.mk_Trueprop (Syntax.check_term lthy' (HOLogic.mk_eq (lhs, rhs))) end fun unfold_tac ctxt = Local_Defs.unfold_tac ctxt [thm'] THEN HEADGOAL (resolve_tac ctxt @{thms refl}) val unfold_thm = Goal.prove_future lthy' (map fst frees) [] unfold_goal (fn {context, ...} => unfold_tac context) fun mk_cong_prem t ctr (f, g) = let (* FIXME get rid of dummyT here *) fun mk_all t = Logic.all_const dummyT $ Abs ("", dummyT, t) val len = dest_Const ctr |> snd |> strip_type |> fst |> length val args = map Bound (len - 1 downto 0) val ctr_val = list_comb (Logic.unvarify_global ctr, args) val args' = if len = 0 then [Bound 0] else args val lhs = list_comb (f, args') val rhs = list_comb (g, args') val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, ctr_val)) in fold (K mk_all) args' (Logic.mk_implies (prem, concl)) end val cong_goal = let val t1 = Free ("t1", Logic.unvarifyT_global T) val t2 = Free ("t2", Logic.unvarifyT_global T) val prems = HOLogic.mk_Trueprop (HOLogic.mk_eq (t1, t2)) :: map2 (mk_cong_prem t2) ctrs (fs ~~ gs) val lhs = list_comb (term', fs) $ t1 val rhs = list_comb (term', gs) $ t2 val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) in Logic.list_implies (prems, concl) |> Syntax.check_term lthy' end fun cong_tac ctxt = Local_Defs.unfold_tac ctxt [thm'] THEN HEADGOAL (eresolve_tac ctxt [case_cong]) THEN ALLGOALS (ctxt |> Subgoal.FOCUS (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt prems THEN' resolve_tac ctxt prems))) val cong_thm = Goal.prove_future lthy' ("t1" :: "t2" :: map fst frees_f @ map fst frees_g) [] cong_goal (fn {context, ...} => cong_tac context) val upd = Data.map (Symtab.update_new (typ_name, ())) in lthy' |> Local_Theory.note ((Binding.empty, @{attributes [code]}), def_thms) |> snd |> Local_Theory.note ((Binding.empty, @{attributes [code_unfold]}), [unfold_thm]) |> snd |> Local_Theory.note ((Binding.empty, @{attributes [fundef_cong]}), [cong_thm]) |> snd |> Local_Theory.declaration {syntax = false, pervasive = true} (K upd) end end fun lazify_typ typ lthy = lazify (the (Ctr_Sugar.ctr_sugar_of lthy (fst (dest_Type typ)))) lthy fun lazify_cmd s lthy = lazify_typ (Proof_Context.read_type_name {proper = true, strict = false} lthy s) lthy val lazy_case_plugin = Plugin_Name.declare_setup @{binding lazy_case} (** setup **) val _ = Outer_Syntax.local_theory @{command_keyword "lazify"} "defines a lazy case constant and sets up the code generator" (Scan.repeat1 Args.embedded_inner_syntax >> fold lazify_cmd) val setup = Ctr_Sugar.ctr_sugar_interpretation lazy_case_plugin (lazify_typ o #T) end \ No newline at end of file diff --git a/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy b/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy --- a/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy @@ -1,1378 +1,1378 @@ section \Utilities for Interface Specifications and Implementations\ theory Sepref_Intf_Util imports Sepref_Rules Sepref_Translate "Lib/Term_Synth" Sepref_Combinator_Setup "Lib/Concl_Pres_Clarification" keywords "sepref_decl_op" :: thy_goal and "sepref_decl_impl" :: thy_goal begin subsection \Relation Interface Binding\ definition INTF_OF_REL :: "('a\'b) set \ 'c itself \ bool" where [simp]: "INTF_OF_REL R I \ True" lemma intf_of_relI: "INTF_OF_REL (R::(_\'a) set) TYPE('a)" by simp declare intf_of_relI[synth_rules] \ \Declare as fallback rule\ lemma [synth_rules]: "INTF_OF_REL unit_rel TYPE(unit)" "INTF_OF_REL nat_rel TYPE(nat)" "INTF_OF_REL int_rel TYPE(int)" "INTF_OF_REL bool_rel TYPE(bool)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\option_rel) TYPE('a option)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\list_rel) TYPE('a list)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\nres_rel) TYPE('a nres)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (R\\<^sub>rS) TYPE('a\'b)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (\R,S\sum_rel) TYPE('a+'b)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (R\S) TYPE('a\'b)" by simp_all lemma synth_intf_of_relI: "INTF_OF_REL R I \ SYNTH_TERM R I" by simp subsection \Operations with Precondition\ definition mop :: "('a\bool) \ ('a\'b nres) \ 'a \ 'b nres" \ \Package operation with precondition\ where [simp]: "mop P f \ \x. ASSERT (P x) \ f x" lemma param_op_mop_iff: assumes "(Q,P)\R\bool_rel" shows "(f, g) \ [P]\<^sub>f R \ \S\nres_rel \ (mop Q f, mop P g) \ R \\<^sub>f \S\nres_rel " using assms by (auto simp: mop_def fref_def pw_nres_rel_iff refine_pw_simps dest: fun_relD) lemma param_mopI: assumes "(f,g) \ [P]\<^sub>f R \ \S\nres_rel" assumes "(Q,P) \ R \ bool_rel" shows "(mop Q f, mop P g) \ R \\<^sub>f \S\nres_rel" using assms by (simp add: param_op_mop_iff) lemma mop_spec_rl: "P x \ mop P f x \ f x" by simp lemma mop_spec_rl_from_def: assumes "f \ mop P g" assumes "P x" assumes "g x \ z" shows "f x \ z" using assms mop_spec_rl by simp lemma mop_leof_rl_from_def: assumes "f \ mop P g" assumes "P x \ g x \\<^sub>n z" shows "f x \\<^sub>n z" using assms by (simp add: pw_leof_iff refine_pw_simps) lemma assert_true_bind_conv: "ASSERT True \ m = m" by simp lemmas mop_alt_unfolds = curry_def curry0_def mop_def uncurry_apply uncurry0_apply o_apply assert_true_bind_conv subsection \Constraints\ lemma add_is_pure_constraint: "\PROP P; CONSTRAINT is_pure A\ \ PROP P" . lemma sepref_relpropI: "P R = CONSTRAINT P R" by simp subsubsection \Purity\ lemmas [constraint_simps] = the_pure_pure definition [constraint_abbrevs]: "IS_PURE P R \ is_pure R \ P (the_pure R)" lemma IS_PURE_pureI: "P R \ IS_PURE P (pure R)" by (auto simp: IS_PURE_def) lemma [fcomp_norm_simps]: "CONSTRAINT (IS_PURE \) P \ pure (the_pure P) = P" by (simp add: IS_PURE_def) lemma [fcomp_norm_simps]: "CONSTRAINT (IS_PURE P) A \ P (the_pure A)" by (auto simp: IS_PURE_def) lemma handle_purity1: "CONSTRAINT (IS_PURE \) A \ CONSTRAINT \ (the_pure A)" by (auto simp: IS_PURE_def) lemma handle_purity2: "CONSTRAINT (IS_PURE \) A \ CONSTRAINT is_pure A" by (auto simp: IS_PURE_def) subsection \Composition\ (* TODO/FIXME: Overlaps with FCOMP! *) subsubsection \Preconditions\ definition [simp]: "tcomp_pre Q T P \ \a. Q a \ (\a'. (a', a) \ T \ P a')" definition "and_pre P1 P2 \ \x. P1 x \ P2 x" definition "imp_pre P1 P2 \ \x. P1 x \ P2 x" lemma and_pre_beta: "PP \ P x \ Q x \ PP \ and_pre P Q x" by (auto simp: and_pre_def) lemma imp_pre_beta: "PP \ P x \ Q x \ PP \ imp_pre P Q x" by (auto simp: imp_pre_def) definition "IMP_PRE P1 P2 \ \x. P1 x \ P2 x" lemma IMP_PRED: "IMP_PRE P1 P2 \ P1 x \ P2 x" unfolding IMP_PRE_def by auto lemma IMP_PRE_refl: "IMP_PRE P P" unfolding IMP_PRE_def by auto definition "IMP_PRE_CUSTOM \ IMP_PRE" lemma IMP_PRE_CUSTOMD: "IMP_PRE_CUSTOM P1 P2 \ IMP_PRE P1 P2" by (simp add: IMP_PRE_CUSTOM_def) lemma IMP_PRE_CUSTOMI: "\\x. P1 x \ P2 x\ \ IMP_PRE_CUSTOM P1 P2" by (simp add: IMP_PRE_CUSTOM_def IMP_PRE_def) lemma imp_and_triv_pre: "IMP_PRE P (and_pre (\_. True) P)" unfolding IMP_PRE_def and_pre_def by auto subsubsection \Premises\ definition "ALL_LIST A \ (\x\set A. x)" definition "IMP_LIST A B \ ALL_LIST A \ B" lemma to_IMP_LISTI: "P \ IMP_LIST [] P" by (auto simp: IMP_LIST_def) lemma to_IMP_LIST: "(P \ IMP_LIST Ps Q) \ Trueprop (IMP_LIST (P#Ps) Q)" by (auto simp: IMP_LIST_def ALL_LIST_def intro!: equal_intr_rule) lemma from_IMP_LIST: "Trueprop (IMP_LIST As B) \ (ALL_LIST As \ B)" "(ALL_LIST [] \ B) \ Trueprop B" "(ALL_LIST (A#As) \ B) \ (A \ ALL_LIST As \ B)" by (auto simp: IMP_LIST_def ALL_LIST_def intro!: equal_intr_rule) lemma IMP_LIST_trivial: "IMP_LIST A B \ IMP_LIST A B" . subsubsection \Composition Rules\ lemma hfcomp_tcomp_pre: assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" shows "(f,h) \ [tcomp_pre Q T P]\<^sub>a hrp_comp RR' T \ hr_comp S U" using hfcomp[OF A B] by simp lemma transform_pre_param: assumes A: "IMP_LIST Cns ((f, h) \ [tcomp_pre Q T P]\<^sub>a hrp_comp RR' T \ hr_comp S U)" assumes P: "IMP_LIST Cns ((P,P') \ T \ bool_rel)" assumes C: "IMP_PRE PP' (and_pre P' Q)" shows "IMP_LIST Cns ((f,h) \ [PP']\<^sub>a hrp_comp RR' T \ hr_comp S U)" unfolding from_IMP_LIST apply (rule hfref_cons) apply (rule A[unfolded from_IMP_LIST]) apply assumption apply (drule IMP_PRED[OF C]) using P[unfolded from_IMP_LIST] unfolding and_pre_def apply (auto dest: fun_relD) [] by simp_all lemma hfref_mop_conv: "((g,mop P f) \ [Q]\<^sub>a R \ S) \ (g,f) \ [\x. P x \ Q x]\<^sub>a R \ S" apply (simp add: hfref_to_ASSERT_conv) apply (fo_rule arg_cong fun_cong)+ by (auto intro!: ext simp: pw_eq_iff refine_pw_simps) lemma hfref_op_to_mop: assumes R: "(impl,f) \ [Q]\<^sub>a R \ S" assumes DEF: "mf \ mop P f" assumes C: "IMP_PRE PP' (imp_pre P Q)" shows "(impl,mf) \ [PP']\<^sub>a R \ S" unfolding DEF hfref_mop_conv apply (rule hfref_cons[OF R]) using C by (auto simp: IMP_PRE_def imp_pre_def) lemma hfref_mop_to_op: assumes R: "(impl,mf) \ [Q]\<^sub>a R \ S" assumes DEF: "mf \ mop P f" assumes C: "IMP_PRE PP' (and_pre Q P)" shows "(impl,f) \ [PP']\<^sub>a R \ S" using R unfolding DEF hfref_mop_conv apply (rule hfref_cons) using C apply (auto simp: and_pre_def IMP_PRE_def) done subsubsection \Precondition Simplification\ lemma IMP_PRE_eqI: assumes "\x. P x \ Q x" assumes "CNV P P'" shows "IMP_PRE P' Q" using assms by (auto simp: IMP_PRE_def) lemma simp_and1: assumes "Q \ CNV P P'" assumes "PP \ P' \ Q" shows "PP \ P \ Q" using assms by auto lemma simp_and2: assumes "P \ CNV Q Q'" assumes "PP \ P \ Q'" shows "PP \ P \ Q" using assms by auto lemma triv_and1: "Q \ True \ Q" by blast lemma simp_imp: assumes "P \ CNV Q Q'" assumes "PP \ Q'" shows "PP \ (P \ Q)" using assms by auto lemma CNV_split: assumes "CNV A A'" assumes "CNV B B'" shows "CNV (A \ B) (A' \ B')" using assms by auto lemma CNV_prove: assumes "P" shows "CNV P True" using assms by auto lemma simp_pre_final_simp: assumes "CNV P P'" shows "P' \ P" using assms by auto lemma auto_weaken_pre_uncurry_step': assumes "PROTECT f a \ f'" shows "PROTECT (uncurry f) (a,b) \ f' b" using assms by (auto simp: curry_def dest!: meta_eq_to_obj_eq intro!: eq_reflection) subsection \Protected Constants\ lemma add_PR_CONST_to_def: "x\y \ PR_CONST x \ y" by simp subsection \Rule Collections\ named_theorems_rev sepref_mop_def_thms \Sepref: mop - definition theorems\ named_theorems_rev sepref_fref_thms \Sepref: fref-theorems\ named_theorems sepref_relprops_transform \Sepref: Simp-rules to transform relator properties\ named_theorems sepref_relprops \Sepref: Simp-rules to add CONSTRAINT-tags to relator properties\ named_theorems sepref_relprops_simps \Sepref: Simp-rules to simplify relator properties\ subsubsection \Default Setup\ subsection \ML-Level Declarations\ ML \ signature SEPREF_INTF_UTIL = sig (* Miscellaneous*) val list_filtered_subterms: (term -> 'a option) -> term -> 'a list (* Interface types for relations *) val get_intf_of_rel: Proof.context -> term -> typ (* Constraints *) (* Convert relations to pure assertions *) val to_assns_rl: bool -> Proof.context -> thm -> thm (* Recognize, summarize and simplify CONSTRAINT - premises *) val cleanup_constraints: Proof.context -> thm -> thm (* Preconditions *) (* Simplify precondition. Goal must be in IMP_PRE or IMP_PRE_CUSTOM form. *) val simp_precond_tac: Proof.context -> tactic' (* Configuration options *) val cfg_def: bool Config.T (* decl_op: Define constant *) val cfg_ismop: bool Config.T (* decl_op: Specified term is mop *) val cfg_mop: bool Config.T (* decl_op, decl_impl: Derive mop *) val cfg_rawgoals: bool Config.T (* decl_op, decl_impl: Do not pre-process/solve goals *) (* TODO: Make do_cmd usable from ML-level! *) end structure Sepref_Intf_Util: SEPREF_INTF_UTIL = struct val cfg_debug = Attrib.setup_config_bool @{binding sepref_debug_intf_util} (K false) val dbg_trace = Sepref_Debugging.dbg_trace_msg cfg_debug val dbg_msg_tac = Sepref_Debugging.dbg_msg_tac cfg_debug fun list_filtered_subterms f t = let fun r t = case f t of SOME a => [a] | NONE => ( case t of t1$t2 => r t1 @ r t2 | Abs (_,_,t) => r t | _ => [] ) in r t end fun get_intf_of_rel ctxt R = Term_Synth.synth_term @{thms synth_intf_of_relI} ctxt R |> fastype_of |> Refine_Util.dest_itselfT local fun add_is_pure_constraint ctxt v thm = let val v = Thm.cterm_of ctxt v val rl = Drule.infer_instantiate' ctxt [NONE, SOME v] @{thm add_is_pure_constraint} in thm RS rl end in fun to_assns_rl add_pure_constr ctxt thm = let val orig_ctxt = ctxt val (thm,ctxt) = yield_singleton (apfst snd oo Variable.importT) thm ctxt val (R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\fref _ ?R ?S)"} => (R,S) | _ => raise THM("to_assns_rl: expected fref-thm",~1,[thm]) fun mk_cn_subst (fname,(iname,C,A)) = let val T' = A --> C --> @{typ assn} val v' = Free (fname,T') val ct' = @{mk_term "the_pure ?v'"} |> Thm.cterm_of ctxt in (v',(iname,ct')) end fun relation_flt (name,Type (@{type_name set},[Type (@{type_name prod},[C,A])])) = SOME (name,C,A) | relation_flt _ = NONE val vars = [] |> Term.add_vars R |> Term.add_vars S |> map_filter (relation_flt) val (names,ctxt) = Variable.variant_fixes (map (#1 #> fst) vars) ctxt val cn_substs = map mk_cn_subst (names ~~ vars) val thm = Drule.infer_instantiate ctxt (map snd cn_substs) thm val thm = thm |> add_pure_constr ? fold (fn (v,_) => fn thm => add_is_pure_constraint ctxt v thm) cn_substs val thm = singleton (Variable.export ctxt orig_ctxt) thm in thm end fun cleanup_constraints ctxt thm = let val orig_ctxt = ctxt val (thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) thm ctxt val xform_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops_transform} val rprops_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops} val simp_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops_simps} fun simp thms = Conv.fconv_rule ( Simplifier.asm_full_rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)) (* Check for pure (the_pure R) - patterns *) local val (_,R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\hfref ?P ?R ?S)"} => (P,R,S) | @{mpat "Trueprop (_\fref ?P ?R ?S)"} => (P,R,S) | _ => raise THM("cleanup_constraints: Expected hfref or fref-theorem",~1,[thm]) fun flt_pat @{mpat "pure (the_pure ?A)"} = SOME A | flt_pat _ = NONE val purify_terms = (list_filtered_subterms flt_pat R @ list_filtered_subterms flt_pat S) |> distinct op aconv val thm = fold (add_is_pure_constraint ctxt) purify_terms thm in val thm = thm end val thm = thm |> Local_Defs.unfold0 ctxt xform_thms |> Local_Defs.unfold0 ctxt rprops_thms val insts = map (fn @{mpat "Trueprop (CONSTRAINT _ (the_pure _))"} => @{thm handle_purity1} | _ => asm_rl ) (Thm.prems_of thm) val thm = (thm OF insts) |> Conv.fconv_rule Thm.eta_conversion |> simp @{thms handle_purity2} |> simp simp_thms val thm = singleton (Variable.export ctxt orig_ctxt) thm in thm end end fun simp_precond_tac ctxt = let fun simp_only thms = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps thms) val rtac = resolve_tac ctxt val cnv_ss = ctxt delsimps @{thms CNV_def} (*val uncurry_tac = SELECT_GOAL (ALLGOALS (DETERM o SOLVED' ( REPEAT' (rtac @{thms auto_weaken_pre_uncurry_step'}) THEN' rtac @{thms auto_weaken_pre_uncurry_finish} )))*) val prove_cnv_tac = SOLVED' (rtac @{thms CNV_prove} THEN' SELECT_GOAL (auto_tac ctxt)) val do_cnv_tac = (cp_clarsimp_tac cnv_ss) THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms CNV_split})) THEN_ALL_NEW (prove_cnv_tac ORELSE' rtac @{thms CNV_I}) val final_simp_tac = rtac @{thms simp_pre_final_simp} THEN' cp_clarsimp_tac cnv_ss THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "final_simp_tac: Before CNV_I") ctxt THEN' rtac @{thms CNV_I} THEN' dbg_msg_tac (Sepref_Debugging.msg_text "Final-Simp done") ctxt (*val curry_tac = let open Conv in CONVERSION (Refine_Util.HOL_concl_conv (fn ctxt => arg1_conv ( top_conv ( fn _ => try_conv (rewr_conv @{thm uncurry_def})) ctxt)) ctxt) THEN' REPEAT' (EqSubst.eqsubst_tac ctxt [1] @{thms case_prod_eta}) THEN' rtac @{thms CNV_I} end*) val simp_tupled_pre_tac = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms prod_casesK uncurry0_hfref_post}) THEN' REPEAT' (EqSubst.eqsubst_tac ctxt [1] @{thms case_prod_eta}) THEN' rtac @{thms CNV_I} val unfold_and_tac = rtac @{thms and_pre_beta} THEN_ALL_NEW simp_only @{thms split} val simp_and1_tac = rtac @{thms simp_and1} THEN' do_cnv_tac val simp_and2_tac = rtac @{thms simp_and2} THEN' do_cnv_tac val and_plan_tac = simp_and1_tac THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "State after and1") ctxt THEN' ( rtac @{thms triv_and1} ORELSE' dbg_msg_tac (Sepref_Debugging.msg_subgoal "Invoking and2 on") ctxt THEN' simp_and2_tac THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "State before final_simp_tac") ctxt THEN' final_simp_tac ) val unfold_imp_tac = rtac @{thms imp_pre_beta} THEN_ALL_NEW simp_only @{thms split} val simp_imp1_tac = rtac @{thms simp_imp} THEN' do_cnv_tac val imp_plan_tac = simp_imp1_tac THEN' final_simp_tac val imp_pre_tac = APPLY_LIST [ simp_only @{thms split_tupled_all} THEN' Refine_Util.instantiate_tuples_subgoal_tac ctxt THEN' CASES' [ (unfold_and_tac, ALLGOALS and_plan_tac), (unfold_imp_tac, ALLGOALS imp_plan_tac) ] , simp_tupled_pre_tac ] val imp_pre_custom_tac = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms and_pre_def}) THEN' TRY o SOLVED' (SELECT_GOAL (auto_tac ctxt)) in CASES' [ (rtac @{thms IMP_PRE_eqI}, imp_pre_tac 1), (rtac @{thms IMP_PRE_CUSTOMI}, ALLGOALS imp_pre_custom_tac) ] end local fun inf_bn_aux name = case String.tokens (fn c => c = #".") name of [] => NONE | [a] => SOME (Binding.name a) | (_::a::_) => SOME (Binding.name a) in fun infer_basename (Const ("_type_constraint_",_)$t) = infer_basename t | infer_basename (Const (name,_)) = inf_bn_aux name | infer_basename (Free (name,_)) = inf_bn_aux name | infer_basename _ = NONE end val cfg_mop = Attrib.setup_config_bool @{binding sepref_register_mop} (K true) val cfg_ismop = Attrib.setup_config_bool @{binding sepref_register_ismop} (K false) val cfg_rawgoals = Attrib.setup_config_bool @{binding sepref_register_rawgoals} (K false) val cfg_transfer = Attrib.setup_config_bool @{binding sepref_decl_impl_transfer} (K true) val cfg_def = Attrib.setup_config_bool @{binding sepref_register_def} (K true) val cfg_register = Attrib.setup_config_bool @{binding sepref_decl_impl_register} (K true) local open Refine_Util val flags = parse_bool_config' "mop" cfg_mop || parse_bool_config' "ismop" cfg_ismop || parse_bool_config' "rawgoals" cfg_rawgoals || parse_bool_config' "def" cfg_def val parse_flags = parse_paren_list' flags val parse_name = Scan.option (Parse.binding --| @{keyword ":"}) val parse_relconds = Scan.optional (@{keyword "where"} |-- Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat) [] in val do_parser = parse_flags -- parse_name -- Parse.term --| @{keyword "::"} -- Parse.term -- parse_relconds end fun do_cmd ((((flags,name),opt_raw), relt_raw),relconds_raw) lthy = let local val ctxt = Refine_Util.apply_configs flags lthy in val flag_ismop = Config.get ctxt cfg_ismop val flag_mop = Config.get ctxt cfg_mop andalso not flag_ismop val flag_rawgoals = Config.get ctxt cfg_rawgoals val flag_def = Config.get ctxt cfg_def end open Sepref_Basic Sepref_Rules val relt = Syntax.parse_term lthy relt_raw val relconds = map (Syntax.parse_prop lthy) relconds_raw val _ = dbg_trace lthy "Parse relation and relation conditions together" val relt = Const (@{const_name "Pure.term"}, dummyT) $ relt local val l = Syntax.check_props lthy (relt::relconds) in val (relt, relconds) = (hd l, tl l) end val relt = Logic.dest_term relt val opt_pre = Syntax.parse_term lthy opt_raw val _ = dbg_trace lthy "Infer basename" val name = case name of SOME name => name | NONE => ( case infer_basename opt_pre of NONE => (error "Could not infer basename: You have to specify a basename"; Binding.empty) | SOME name => name ) fun qname s n = Binding.qualify true (Binding.name_of n) (Binding.name s) fun def name t_pre attribs lthy = let val t = Syntax.check_term lthy t_pre (*|> Thm.cterm_of lthy |> Drule.mk_term |> Local_Defs.unfold0 lthy @{thms PR_CONST_def} |> Drule.dest_term |> Thm.term_of*) - val lthy = Local_Theory.open_target lthy + val lthy = (snd o Local_Theory.begin_nested) lthy val ((dt,(_,thm)),lthy) = Local_Theory.define ((name,Mixfix.NoSyn),((Thm.def_binding name,@{attributes [code]}@attribs),t)) lthy; - val (lthy, lthy_old) = `Local_Theory.close_target lthy + val (lthy, lthy_old) = `Local_Theory.end_nested lthy val phi = Proof_Context.export_morphism lthy_old lthy val thm = Morphism.thm phi thm val dt = Morphism.term phi dt in ((dt,thm),lthy) end val _ = dbg_trace lthy "Analyze Relation" val (pre,args,res) = analyze_rel relt val specified_pre = is_some pre val pre = the_default (mk_triv_precond args) pre val def_thms = @{thms PR_CONST_def} val _ = dbg_trace lthy "Define op" val op_name = Binding.prefix_name (if flag_ismop then "mop_" else "op_") name val (def_thms,opc,lthy) = if flag_def then let val ((opc,op_def_thm),lthy) = def op_name opt_pre @{attributes [simp]} lthy val opc = Refine_Util.dummify_tvars opc val def_thms = op_def_thm::def_thms in (def_thms,opc,lthy) end else let val _ = dbg_trace lthy "Refine type of opt_pre to get opc" val opc = Syntax.check_term lthy opt_pre val new_ctxt = Variable.declare_term opc lthy val opc = singleton (Variable.export_terms new_ctxt lthy) opc |> Refine_Util.dummify_tvars in (def_thms,opc,lthy) end (* PR_CONST Heuristics *) fun pr_const_heuristics basename c_pre lthy = let val _ = dbg_trace lthy ("PR_CONST heuristics " ^ @{make_string} c_pre) val c = Syntax.check_term lthy c_pre in case c of @{mpat "PR_CONST _"} => ((c_pre,false),lthy) | Const _ => ((c_pre,false),lthy) | _ => let val (f,args) = strip_comb c val lthy = case f of Const _ => let val ctxt = Variable.declare_term c lthy val lhs = Autoref_Tagging.list_APP (f,args) val rhs = @{mk_term "UNPROTECT ?c"} val goal = Logic.mk_equals (lhs,rhs) |> Thm.cterm_of ctxt val tac = Local_Defs.unfold0_tac ctxt @{thms APP_def UNPROTECT_def} THEN ALLGOALS (simp_tac (put_simpset HOL_basic_ss ctxt)) val thm = Goal.prove_internal ctxt [] goal (K tac) |> singleton (Variable.export ctxt lthy) val (_,lthy) = Local_Theory.note ((Binding.suffix_name "_def_pat" basename,@{attributes [def_pat_rules]}),[thm]) lthy val _ = Thm.pretty_thm lthy thm |> Pretty.string_of |> writeln in lthy end | _ => ( Pretty.block [ Pretty.str "Complex operation pattern. Added PR_CONST but no pattern rules:", Pretty.brk 1,Syntax.pretty_term lthy c] |> Pretty.string_of |> warning ; lthy) val c_pre = Const(@{const_name PR_CONST},dummyT)$c_pre in ((c_pre,true),lthy) end end val ((opc,_),lthy) = pr_const_heuristics op_name opc lthy (* Register *) val arg_intfs = map (get_intf_of_rel lthy) args val res_intf = get_intf_of_rel lthy res fun register basename c lthy = let val _ = dbg_trace lthy "Register" open Sepref_Basic val c = Syntax.check_term lthy c val ri = case (is_nresT (body_type (fastype_of c)), is_nresT res_intf) of (true,false) => mk_nresT res_intf | (false,true) => dest_nresT res_intf | _ => res_intf val iT = arg_intfs ---> ri val ((_,itype_thm),lthy) = Sepref_Combinator_Setup.sepref_register_single (Binding.name_of basename) c iT lthy val _ = Thy_Output.pretty_thm lthy itype_thm |> Pretty.string_of |> writeln in lthy end val lthy = register op_name opc lthy val _ = dbg_trace lthy "Define pre" val pre_name = Binding.prefix_name "pre_" name val ((prec,pre_def_thm),lthy) = def pre_name pre @{attributes [simp]} lthy val prec = Refine_Util.dummify_tvars prec val def_thms = pre_def_thm::def_thms (* Re-integrate pre-constant into type-context of relation. TODO: This is probably not clean/robust *) val pre = constrain_type_pre (fastype_of pre) prec |> Syntax.check_term lthy val _ = dbg_trace lthy "Convert both, relation and operation to uncurried form, and add nres" val _ = dbg_trace lthy "Convert relation (arguments have already been separated by analyze-rel)" val res = case res of @{mpat "\_\nres_rel"} => res | _ => @{mk_term "\?res\nres_rel"} val relt = mk_rel (SOME pre,args,res) val _ = dbg_trace lthy "Convert operation" val opcT = fastype_of (Syntax.check_term lthy opc) val op_is_nres = Sepref_Basic.is_nresT (body_type opcT) val (opcu, op_ar) = let val arity = binder_types #> length (* Arity of operation is number of arguments before result (which may be a fun-type! )*) val res_ar = arity (Relators.rel_absT res |> not op_is_nres ? dest_nresT) val op_ar = arity opcT - res_ar val _ = op_ar = length args orelse raise TERM("Operation/relation arity mismatch: " ^ string_of_int op_ar ^ " vs " ^ string_of_int (length args),[opc,relt]) (* Add RETURN o...o if necessary*) val opc = if op_is_nres then opc else mk_compN_pre op_ar (Const(@{const_name Refine_Basic.RETURN},dummyT)) opc (* Add uncurry if necessary *) val opc = mk_uncurryN_pre op_ar opc in (opc, op_ar) end (* Build mop-variant *) val declare_mop = (specified_pre orelse not op_is_nres) andalso flag_mop val (mop_data,lthy) = if declare_mop then let val _ = dbg_trace lthy "mop definition" val mop_rhs = Const(@{const_name mop},dummyT) $ prec $ opcu |> mk_curryN_pre op_ar val mop_name = Binding.prefix_name "mop_" name val ((mopc,mop_def_thm),lthy) = def mop_name mop_rhs [] lthy val mopc = Refine_Util.dummify_tvars mopc val ((mopc,added_pr_const),lthy) = pr_const_heuristics mop_name mopc lthy val mop_def_thm' = if added_pr_const then mop_def_thm RS @{thm add_PR_CONST_to_def} else mop_def_thm val (_,lthy) = Local_Theory.note ((Binding.empty, @{attributes [sepref_mop_def_thms]}),[mop_def_thm']) lthy val _ = dbg_trace lthy "mop alternative definition" val alt_unfolds = @{thms mop_alt_unfolds} |> not specified_pre ? curry op :: pre_def_thm val mop_alt_thm = Local_Defs.unfold0 lthy alt_unfolds mop_def_thm |> Refine_Util.shift_lambda_leftN op_ar val (_,lthy) = Local_Theory.note ((Binding.suffix_name "_alt" mop_name,@{attributes [simp]}),[mop_alt_thm]) lthy val _ = dbg_trace lthy "mop: register" val lthy = register mop_name mopc lthy val _ = dbg_trace lthy "mop: vcg theorem" local val Ts = map Relators.rel_absT args val ctxt = Variable.declare_thm mop_def_thm lthy val ctxt = fold Variable.declare_typ Ts ctxt val (x,ctxt) = Refine_Util.fix_left_tuple_from_Ts "x" Ts ctxt val mop_def_thm = mop_def_thm |> Local_Defs.unfold0 ctxt @{thms curry_shl} fun prep_thm thm = (thm OF [mop_def_thm]) |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt x)] |> Local_Defs.unfold0 ctxt @{thms uncurry_apply uncurry0_apply o_apply} |> Local_Defs.unfold0 ctxt (def_thms @ @{thms Product_Type.split HOL.True_implies_equals}) |> singleton (Variable.export ctxt lthy) val thms = map prep_thm @{thms mop_spec_rl_from_def mop_leof_rl_from_def} in val (_,lthy) = Local_Theory.note ((qname "vcg" mop_name,@{attributes [refine_vcg]}),thms) lthy end in (SOME (mop_name,mopc,mop_def_thm),lthy) end else (NONE,lthy) val _ = dbg_trace lthy "Build Parametricity Theorem" val param_t = mk_pair_in_pre opcu opcu relt |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds val _ = dbg_trace lthy "Build Parametricity Theorem for Precondition" val param_pre_t = let val pre_relt = Relators.mk_fun_rel (Relators.list_prodrel_left args) @{term bool_rel} val param_pre_t = mk_pair_in_pre prec prec pre_relt |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds in param_pre_t end val _ = dbg_trace lthy "Build goals" val goals = [[ (param_t, []), (param_pre_t, []) ]] fun after_qed [[p_thm, pp_thm]] _ (*ctxt*) = let val _ = dbg_trace lthy "after_qed" val p_thm' = p_thm |> not specified_pre ? Local_Defs.unfold0 lthy [pre_def_thm] val (_,lthy) = Local_Theory.note ((qname "fref" op_name,@{attributes [sepref_fref_thms]}), [p_thm']) lthy val (_,lthy) = Local_Theory.note ((qname "param" pre_name,@{attributes [param]}), [pp_thm]) lthy val p'_unfolds = pre_def_thm :: @{thms True_implies_equals} val (_,lthy) = Local_Theory.note ((qname "fref'" op_name,[]), [Local_Defs.unfold0 lthy p'_unfolds p_thm]) lthy val lthy = case mop_data of NONE => lthy | SOME (mop_name,mopc,mop_def_thm) => let val _ = dbg_trace lthy "Build and prove mop-stuff" (* mop - parametricity theorem: (uncurry\<^sup>n mopc,uncurry\<^sup>n mopc) \ args \\<^sub>f res *) val mopcu = mk_uncurryN_pre op_ar mopc val param_mop_t = mk_pair_in_pre mopcu mopcu (mk_rel (NONE,args,res)) |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds val ctxt = Proof_Context.augment param_mop_t lthy val tac = let val p_thm = Local_Defs.unfold0 ctxt @{thms PR_CONST_def} p_thm in Local_Defs.unfold0_tac ctxt (mop_def_thm :: @{thms PR_CONST_def uncurry_curry_id uncurry_curry0_id}) THEN FIRSTGOAL ( dbg_msg_tac (Sepref_Debugging.msg_subgoal "Mop-param thm goal after unfolding") ctxt THEN' resolve_tac ctxt @{thms param_mopI} THEN' SOLVED' (resolve_tac ctxt [p_thm] THEN_ALL_NEW assume_tac ctxt) THEN' SOLVED' (resolve_tac ctxt [pp_thm] THEN_ALL_NEW assume_tac ctxt) ) end val pm_thm = Goal.prove_internal lthy [] (Thm.cterm_of ctxt param_mop_t) (K tac) |> singleton (Variable.export ctxt lthy) val (_,lthy) = Local_Theory.note ((qname "fref" mop_name,@{attributes [sepref_fref_thms]}), [pm_thm]) lthy val (_,lthy) = Local_Theory.note ((qname "fref'" mop_name,[]), [Local_Defs.unfold0 lthy p'_unfolds pm_thm]) lthy in lthy end in lthy end | after_qed thmss _ = raise THM ("After-qed: Wrong thmss structure",~1,flat thmss) fun std_tac ctxt = let val ptac = REPEAT_ALL_NEW_FWD (Parametricity.net_tac (Parametricity.get_dflt ctxt) ctxt) (* Massage simpset a bit *) val ctxt = ctxt |> Context_Position.set_visible false |> Context.proof_map (Thm.attribute_declaration Clasimp.iff_del @{thm pair_in_Id_conv}) in if flag_rawgoals then all_tac else Local_Defs.unfold0_tac ctxt def_thms THEN ALLGOALS ( TRY o SOLVED' ( TRY o resolve_tac ctxt @{thms frefI} THEN' TRY o REPEAT_ALL_NEW (ematch_tac ctxt @{thms prod_relE}) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split uncurry_apply uncurry0_apply}) THEN' ( SOLVED' (ptac THEN_ALL_NEW asm_full_simp_tac ctxt) ORELSE' SOLVED' (cp_clarsimp_tac ctxt THEN_ALL_NEW_FWD ptac THEN_ALL_NEW SELECT_GOAL (auto_tac ctxt)) ) ) ) end val rf_std = Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (std_tac ctxt))) #> Seq.the_result "do_cmd: Standard proof tactic returned empty result sequence" in Proof.theorem NONE after_qed goals lthy |> rf_std end val _ = Outer_Syntax.local_theory_to_proof @{command_keyword "sepref_decl_op"} "" (do_parser >> do_cmd) local fun unfold_PR_CONST_tac ctxt = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms PR_CONST_def}) fun transfer_precond_rl ctxt t R = let (*val tfrees = Term.add_tfreesT (fastype_of t) [] val t' = map_types (map_type_tfree (fn x => if member op= tfrees x then dummyT else TFree x)) t *) (* TODO: Brute force approach, that may generalize too much! *) val t' = map_types (K dummyT) t val goal = Sepref_Basic.mk_pair_in_pre t t' R |> Syntax.check_term ctxt |> Thm.cterm_of ctxt val thm = Drule.infer_instantiate' ctxt [NONE,SOME goal] @{thm IMP_LIST_trivial} in thm end (* Generate a hnr-thm for mop given one for op *) fun generate_mop_thm ctxt op_thm = let val orig_ctxt = ctxt val (op_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) op_thm ctxt (* Convert mop_def_thms to form uncurry^n f \ mop P g *) val mop_def_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_mop_def_thms} |> map (Local_Defs.unfold0 ctxt @{thms curry_shl}) fun fail_hnr_tac _ _ = raise THM("Invalid hnr-theorem",~1,[op_thm]) fun fail_mop_def_tac i st = let val g = nth (Thm.prems_of st) (i-1) in raise TERM("Found no matching mop-definition",[g]) end (* Tactic to solve preconditions of hfref_op_to_mop *) val tac = APPLY_LIST [ resolve_tac ctxt [op_thm] ORELSE' fail_hnr_tac, ((*unfold_PR_CONST_tac ctxt THEN'*) resolve_tac ctxt mop_def_thms) ORELSE' fail_mop_def_tac, simp_precond_tac ctxt ORELSE' Sepref_Debugging.error_tac' "precond simplification failed" ctxt ] 1 (* Do synthesis *) val st = @{thm hfref_op_to_mop} val st = Goal.protect (Thm.nprems_of st) st val mop_thm = tac st |> Seq.hd |> Goal.conclude val mop_thm = singleton (Variable.export ctxt orig_ctxt) mop_thm |> Sepref_Rules.norm_fcomp_rule orig_ctxt in mop_thm end (* Generate a hnr-thm for op given one for mop *) fun generate_op_thm ctxt mop_thm = let (* TODO: Almost-clone of generate_mop_thm *) val orig_ctxt = ctxt val (mop_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) mop_thm ctxt (* Convert mop_def_thms to form uncurry^n f \ mop P g *) val mop_def_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_mop_def_thms} |> map (Local_Defs.unfold0 ctxt @{thms curry_shl}) fun fail_hnr_tac _ _ = raise THM("Invalid hnr-theorem",~1,[mop_thm]) fun fail_mop_def_tac i st = let val g = nth (Thm.prems_of st) (i-1) in raise TERM("Found no matching mop-definition",[g]) end (* Tactic to solve preconditions of hfref_mop_to_op *) val tac = APPLY_LIST [ resolve_tac ctxt [mop_thm] ORELSE' fail_hnr_tac, ((*unfold_PR_CONST_tac ctxt THEN'*) resolve_tac ctxt mop_def_thms) ORELSE' fail_mop_def_tac, simp_precond_tac ctxt ORELSE' Sepref_Debugging.error_tac' "precond simplification failed" ctxt ] 1 (* Do synthesis *) val st = @{thm hfref_mop_to_op} val st = Goal.protect (Thm.nprems_of st) st val op_thm = tac st |> Seq.hd |> Goal.conclude val op_thm = singleton (Variable.export ctxt orig_ctxt) op_thm |> Sepref_Rules.norm_fcomp_rule orig_ctxt in op_thm end fun chk_result ctxt thm = let val (_,R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\hfref ?P ?R ?S)"} => (P,R,S) | _ => raise THM("chk_result: Expected hfref-theorem",~1,[thm]) fun err t = let val ts = Syntax.pretty_term ctxt t |> Pretty.string_of in raise THM ("chk_result: Invalid pattern left in assertions: " ^ ts,~1,[thm]) end fun check_invalid (t as @{mpat "hr_comp _ _"}) = err t | check_invalid (t as @{mpat "hrp_comp _ _"}) = err t | check_invalid (t as @{mpat "pure (the_pure _)"}) = err t | check_invalid (t as @{mpat "_ O _"}) = err t | check_invalid _ = false val _ = exists_subterm check_invalid R val _ = exists_subterm check_invalid S in () end fun to_IMP_LIST ctxt thm = (thm RS @{thm to_IMP_LISTI}) |> Local_Defs.unfold0 ctxt @{thms to_IMP_LIST} fun from_IMP_LIST ctxt thm = thm |> Local_Defs.unfold0 ctxt @{thms from_IMP_LIST} in local open Refine_Util val flags = parse_bool_config' "mop" cfg_mop || parse_bool_config' "ismop" cfg_ismop || parse_bool_config' "transfer" cfg_transfer || parse_bool_config' "rawgoals" cfg_rawgoals || parse_bool_config' "register" cfg_register val parse_flags = parse_paren_list' flags val parse_precond = Scan.option (@{keyword "["} |-- Parse.term --| @{keyword "]"}) val parse_fref_thm = Scan.option (@{keyword "uses"} |-- Parse.thm) in val di_parser = parse_flags -- Scan.optional (Parse.binding --| @{keyword ":"}) Binding.empty -- parse_precond -- Parse.thm -- parse_fref_thm end fun di_cmd ((((flags,name), precond_raw), i_thm_raw), p_thm_raw) lthy = let val i_thm = singleton (Attrib.eval_thms lthy) i_thm_raw val p_thm = map_option (singleton (Attrib.eval_thms lthy)) p_thm_raw local val ctxt = Refine_Util.apply_configs flags lthy in val flag_mop = Config.get ctxt cfg_mop val flag_ismop = Config.get ctxt cfg_ismop val flag_rawgoals = Config.get ctxt cfg_rawgoals val flag_transfer = Config.get ctxt cfg_transfer val flag_register = Config.get ctxt cfg_register end val fr_attribs = if flag_register then @{attributes [sepref_fr_rules]} else [] val ctxt = lthy (* Compose with fref-theorem *) val _ = dbg_trace lthy "Compose with fref" local val hf_tcomp_pre = @{thm hfcomp_tcomp_pre} OF [asm_rl,i_thm] fun compose p_thm = let val p_thm = p_thm |> to_assns_rl false lthy in hf_tcomp_pre OF [p_thm] end in val thm = case p_thm of SOME p_thm => compose p_thm | NONE => let val p_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_fref_thms} fun err () = let val prem_s = nth (Thm.prems_of hf_tcomp_pre) 0 |> Syntax.pretty_term ctxt |> Pretty.string_of in error ("Found no fref-theorem matching " ^ prem_s) end in case get_first (try compose) p_thms of NONE => err () | SOME thm => thm end end val (thm,ctxt) = yield_singleton (apfst snd oo Variable.import true) thm ctxt val _ = dbg_trace lthy "Transfer Precond" val thm = to_IMP_LIST ctxt thm val thm = thm RS @{thm transform_pre_param} local val (pre,R,pp_name,pp_type) = case Thm.prems_of thm of [@{mpat "Trueprop (IMP_LIST _ ((?pre,_)\?R))"}, @{mpat "Trueprop (IMP_PRE (mpaq_STRUCT (mpaq_Var ?pp_name ?pp_type)) _)"}] => (pre,R,pp_name,pp_type) | _ => raise THM("di_cmd: Cannot recognize first prems of transform_pre_param: ", ~1,[thm]) in val thm = if flag_transfer then thm OF [transfer_precond_rl ctxt pre R] else thm val thm = case precond_raw of NONE => thm | SOME precond_raw => let val precond = Syntax.parse_term ctxt precond_raw |> Sepref_Basic.constrain_type_pre pp_type |> Syntax.check_term ctxt |> Thm.cterm_of ctxt val thm = Drule.infer_instantiate ctxt [(pp_name,precond)] thm val thm = thm OF [asm_rl,@{thm IMP_PRE_CUSTOMD}] in thm end end val _ = dbg_trace lthy "Build goals" val goals = [map (fn x => (x,[])) (Thm.prems_of thm)] fun after_qed thmss _ = let val _ = dbg_trace lthy "After QED" val prems_thms = hd thmss val thm = thm OF prems_thms val thm = from_IMP_LIST ctxt thm (* Two rounds of cleanup-constraints, norm_fcomp *) val _ = dbg_trace lthy "Cleanup" val thm = thm |> cleanup_constraints ctxt |> Sepref_Rules.norm_fcomp_rule ctxt |> cleanup_constraints ctxt |> Sepref_Rules.norm_fcomp_rule ctxt val thm = thm |> singleton (Variable.export ctxt lthy) |> zero_var_indexes val _ = dbg_trace lthy "Check Result" val _ = chk_result lthy thm fun qname suffix = if Binding.is_empty name then name else Binding.suffix_name suffix name val thm_name = if flag_ismop then qname "_hnr_mop" else qname "_hnr" val (_,lthy) = Local_Theory.note ((thm_name,fr_attribs),[thm]) lthy val _ = Thm.pretty_thm lthy thm |> Pretty.string_of |> writeln (* Create mop theorem from op-theorem *) val cr_mop_thm = flag_mop andalso not flag_ismop val lthy = if cr_mop_thm then let val _ = dbg_trace lthy "Create mop-thm" val mop_thm = thm |> generate_mop_thm lthy |> zero_var_indexes val (_,lthy) = Local_Theory.note ((qname "_hnr_mop",fr_attribs),[mop_thm]) lthy val _ = Thm.pretty_thm lthy mop_thm |> Pretty.string_of |> writeln in lthy end else lthy (* Create op theorem from mop-theorem *) val cr_op_thm = flag_ismop val lthy = if cr_op_thm then let val _ = dbg_trace lthy "Create op-thm" val op_thm = thm |> generate_op_thm lthy |> zero_var_indexes val (_,lthy) = Local_Theory.note ((qname "_hnr",fr_attribs),[op_thm]) lthy val _ = Thm.pretty_thm lthy op_thm |> Pretty.string_of |> writeln in lthy end else lthy in lthy end fun std_tac ctxt = let val ptac = REPEAT_ALL_NEW_FWD ( Parametricity.net_tac (Parametricity.get_dflt ctxt) ctxt ORELSE' assume_tac ctxt ) in if flag_rawgoals orelse not flag_transfer then all_tac else APPLY_LIST [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms from_IMP_LIST}) THEN' TRY o SOLVED' ptac, simp_precond_tac ctxt ] 1 end val rf_std = Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (std_tac ctxt))) #> Seq.the_result "di_cmd: Standard proof tactic returned empty result sequence" in Proof.theorem NONE after_qed goals ctxt |> rf_std end val _ = Outer_Syntax.local_theory_to_proof @{command_keyword "sepref_decl_impl"} "" (di_parser >> di_cmd) end end \ subsection \Obsolete Manual Specification Helpers\ (* Generate VCG-rules for operations *) lemma vcg_of_RETURN_np: assumes "f \ RETURN r" shows "SPEC (\x. x=r) \ m \ f \ m" and "SPEC (\x. x=r) \\<^sub>n m \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff) lemma vcg_of_RETURN: assumes "f \ do { ASSERT \; RETURN r }" shows "\\; SPEC (\x. x=r) \ m\ \ f \ m" and "\\ \ SPEC (\x. x=r) \\<^sub>n m\ \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps) lemma vcg_of_SPEC: assumes "f \ do { ASSERT pre; SPEC post }" shows "\pre; SPEC post \ m\ \ f \ m" and "\pre \ SPEC post \\<^sub>n m\ \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps) lemma vcg_of_SPEC_np: assumes "f \ SPEC post" shows "SPEC post \ m \ f \ m" and "SPEC post \\<^sub>n m \ f \\<^sub>n m" using assms by auto (* Generate parametricity rules to generalize plain operations to monadic ones. Use with FCOMP. *) lemma mk_mop_rl1: assumes "\x. mf x \ ASSERT (P x) \ RETURN (f x)" shows "(RETURN o f, mf) \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl2: assumes "\x y. mf x y \ ASSERT (P x y) \ RETURN (f x y)" shows "(RETURN oo f, mf) \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl3: assumes "\x y z. mf x y z \ ASSERT (P x y z) \ RETURN (f x y z)" shows "(RETURN ooo f, mf) \ Id \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl0_np: assumes "mf \ RETURN f" shows "(RETURN f, mf) \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl1_np: assumes "\x. mf x \ RETURN (f x)" shows "(RETURN o f, mf) \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl2_np: assumes "\x y. mf x y \ RETURN (f x y)" shows "(RETURN oo f, mf) \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl3_np: assumes "\x y z. mf x y z \ RETURN (f x y z)" shows "(RETURN ooo f, mf) \ Id \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_op_rl0_np: assumes "mf \ RETURN f" shows "(uncurry0 mf, uncurry0 (RETURN f)) \ unit_rel \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl1: assumes "\x. mf x \ ASSERT (P x) \ RETURN (f x)" shows "(mf, RETURN o f) \ [P]\<^sub>f Id \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl1_np: assumes "\x. mf x \ RETURN (f x)" shows "(mf, (RETURN o f)) \ Id \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl2: assumes "\x y. mf x y \ ASSERT (P x y) \ RETURN (f x y)" shows "(uncurry mf, uncurry (RETURN oo f)) \ [uncurry P]\<^sub>f Id\\<^sub>rId \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl2_np: assumes "\x y. mf x y \ RETURN (f x y)" shows "(uncurry mf, uncurry (RETURN oo f)) \ Id\\<^sub>rId \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl3: assumes "\x y z. mf x y z \ ASSERT (P x y z) \ RETURN (f x y z)" shows "(uncurry2 mf, uncurry2 (RETURN ooo f)) \ [uncurry2 P]\<^sub>f (Id\\<^sub>rId)\\<^sub>rId \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl3_np: assumes "\x y z. mf x y z \ RETURN (f x y z)" shows "(uncurry2 mf, uncurry2 (RETURN ooo f)) \ (Id\\<^sub>rId)\\<^sub>rId \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done end