diff --git a/thys/Collections/ICF/tools/Locale_Code.thy b/thys/Collections/ICF/tools/Locale_Code.thy --- a/thys/Collections/ICF/tools/Locale_Code.thy +++ b/thys/Collections/ICF/tools/Locale_Code.thy @@ -1,386 +1,387 @@ section \Code Generation from Locales\ theory Locale_Code imports ICF_Tools Ord_Code_Preproc begin text \ Provides a simple mechanism to prepare code equations for constants stemming from locale interpretations. The usage pattern is as follows: \setup Locale_Code.checkpoint\ is called before a series of interpretations, and afterwards, \setup Locale_Code.prepare\ is called. Afterwards, the code generator will correctly recognize expressions involving terms from the locale interpretation. \ text \Tag to indicate pattern deletion\ definition LC_DEL :: "'a \ unit" where "LC_DEL a \ ()" ML \ signature LOCALE_CODE = sig type pat_eq = cterm * thm list val open_block: theory -> theory val close_block: theory -> theory val del_pat: cterm -> theory -> theory val add_pat_eq: cterm -> thm list -> theory -> theory val lc_decl_eq: thm list -> local_theory -> local_theory val lc_decl_del: term -> local_theory -> local_theory val setup: theory -> theory val get_unf_ss: theory -> simpset val tracing_enabled: bool Unsynchronized.ref end structure Locale_Code :LOCALE_CODE = struct open ICF_Tools val tracing_enabled = Unsynchronized.ref false; type pat_eq = cterm * thm list type block_data = {idx:int, del_pats: cterm list, add_pateqs: pat_eq list} val closed_block = {idx = ~1, del_pats=[], add_pateqs=[]}; fun init_block idx = {idx = idx, del_pats=[], add_pateqs=[]}; fun is_open ({idx,...}:block_data) = idx <> ~1; fun assert_open bd = if is_open bd then () else error "Locale_Code: No open block"; fun assert_closed bd = if is_open bd then error "Locale_Code: Block already open" else (); fun merge_bd (bd1,bd2) = ( if is_open bd1 orelse is_open bd2 then error "Locale_Code: Merge with open block" else (); closed_block ); fun bd_add_del_pats ps {idx,del_pats,add_pateqs} = {idx = idx, del_pats = ps@del_pats, add_pateqs = add_pateqs}; fun bd_add_add_pateqs pes {idx,del_pats,add_pateqs} = {idx = idx, del_pats = del_pats, add_pateqs = pes@add_pateqs}; structure BlockData = Theory_Data ( type T = block_data val empty = (closed_block) val extend = I val merge = merge_bd ); structure FoldSSData = Oc_Simpset ( val prio = 5; val name = "Locale_Code"; ); fun add_unf_thms thms thy = let val ctxt = Proof_Context.init_global thy val thms = map Thm.symmetric thms in FoldSSData.map (fn ss => put_simpset ss ctxt |> sss_add thms |> simpset_of ) thy end val get_unf_ss = FoldSSData.get; (* First order match with fixed head *) fun match_fixed_head (pat,obj) = let (* Match heads *) val inst = Thm.first_order_match (chead_of pat, chead_of obj); val pat = Thm.instantiate_cterm inst pat; (* Now match whole pattern *) val inst = Thm.first_order_match (pat, obj); in inst end; val matches_fixed_head = can match_fixed_head; (* First order match of heads only *) fun match_heads (pat,obj) = Thm.first_order_match (chead_of pat, chead_of obj); val matches_heads = can match_heads; val pat_nargs = Thm.term_of #> strip_comb #> #2 #> length; (* Adjust a theorem to exactly match pattern *) fun norm_thm_pat (thm,pat) = let val thm = norm_def_thm thm; val na_pat = pat_nargs pat; val lhs = Thm.lhs_of thm; val na_lhs = pat_nargs lhs; val lhs' = if na_lhs > na_pat then funpow (na_lhs - na_pat) Thm.dest_fun lhs else lhs; val inst = Thm.first_order_match (lhs',pat); in Thm.instantiate inst thm end; fun del_pat_matches cpat (epat,_) = if pat_nargs cpat = 0 then matches_heads (cpat,epat) else matches_fixed_head (cpat,epat); (* Pattern-Eqs from specification *) local datatype action = ADD of (cterm * thm list) | DEL of cterm fun filter_pat_eq thy thms pat = let val cpat = Thm.global_cterm_of thy pat; in if (pat_nargs cpat = 0) then NONE else let val thms' = fold (fn thm => fn acc => case try norm_thm_pat (thm, cpat) of NONE => acc | SOME thm => thm::acc ) thms []; in case thms' of [] => NONE | _ => SOME (ADD (cpat,thms')) end end; fun process_actions acc [] = acc | process_actions acc (ADD peq::acts) = process_actions (peq::acc) acts | process_actions acc (DEL cpat::acts) = let val acc' = filter (not o curry renames_cterm cpat o fst) acc; val _ = if length acc = length acc' then warning ("Locale_Code: LC_DEL without effect: " ^ @{make_string} cpat) else (); in process_actions acc' acts end; fun pat_eqs_of_spec thy {rough_classification = Spec_Rules.Equational _, terms = pats, rules = thms, ...} = map_filter (filter_pat_eq thy thms) pats | pat_eqs_of_spec thy {rough_classification = Spec_Rules.Unknown, terms = [Const (@{const_name LC_DEL},_)$pat], ...} = [(DEL (Thm.global_cterm_of thy pat))] | pat_eqs_of_spec _ _ = []; in fun pat_eqs_of_specs thy specs = map (pat_eqs_of_spec thy) specs |> flat |> rev |> process_actions []; end; fun is_proper_pat cpat = let val pat = Thm.term_of cpat; val (f,args) = strip_comb pat; in is_Const f andalso args <> [] andalso not (is_Var (hd (rev args))) end; (* Instantiating pattern-eq *) local (* Get constant name for instantiation pattern *) fun inst_name lthy pat = let val (fname,params) = case strip_comb pat of ((Const (fname,_)),params) => (fname,params) | _ => raise TERM ("inst_name: Expected pattern",[pat]); fun pname (Const (n,_)) = Long_Name.base_name n | pname (s$t) = pname s ^ "_" ^ pname t | pname _ = Name.uu; in space_implode "_" (Long_Name.base_name fname::map pname params) |> gen_variant (can (Proof_Context.read_const {proper = true, strict = false} lthy)) end; in fun inst_pat_eq (cpat,thms) = wrap_lthy_result_global (fn lthy => let - val ((inst,thms),lthy) = Variable.import true thms lthy; - val cpat = Thm.instantiate_cterm inst cpat; + val (((instT,inst),thms),lthy) = Variable.import true thms lthy; + val cpat = + Thm.instantiate_cterm (Term_Subst.TVars.dest instT, Term_Subst.Vars.dest inst) cpat; val pat = Thm.term_of cpat; val name = inst_name lthy pat; val ((_,(_,def_thm)),lthy) = Local_Theory.define ((Binding.name name,NoSyn), ((Binding.name (Thm.def_name name),[]),pat)) lthy; val thms' = map (Local_Defs.fold lthy [def_thm]) thms; in ((def_thm,thms'),lthy) end) (fn m => fn (def_thm,thms') => (Morphism.thm m def_thm, map (Morphism.thm m) thms')) #> (fn ((def_thm,thms'),thy) => let val thy = thy |> add_unf_thms [def_thm] |> Code.declare_default_eqns_global (map (rpair true) thms'); in thy end) end (* Bookkeeping *) fun new_specs thy = let val bd = BlockData.get thy; val _ = assert_open bd; val ctxt = Proof_Context.init_global thy; val srules = Spec_Rules.get ctxt; val res = take (length srules - #idx bd) srules; in res end fun open_block thy = let val bd = BlockData.get thy; val _ = assert_closed bd; val ctxt = Proof_Context.init_global thy; val idx = length (Spec_Rules.get ctxt); val thy = BlockData.map (K (init_block idx)) thy; in thy end; fun process_block bd thy = let fun filter_del_pats cpat peqs = let val peqs' = filter (not o del_pat_matches cpat) peqs val _ = if length peqs = length peqs' then warning ("Locale_Code: No pattern-eqs matching filter: " ^ @{make_string} cpat) else (); in peqs' end; fun filter_add_pats (orig_pat,_) = forall (fn (add_pat,_) => not (renames_cterm (orig_pat,add_pat))) (#add_pateqs bd); val specs = new_specs thy; val peqs = pat_eqs_of_specs thy specs |> fold filter_del_pats (#del_pats bd) |> filter filter_add_pats; val peqs = peqs @ #add_pateqs bd; val peqs = rev peqs; (* Important: Process equations in the order in that they have been added! *) val _ = if !tracing_enabled then map (fn peq => (tracing (@{make_string} peq); ())) peqs else []; val thy = thy |> fold inst_pat_eq peqs; in thy end; fun close_block thy = let val bd = BlockData.get thy; val _ = assert_open bd; val thy = process_block bd thy |> BlockData.map (K closed_block); in thy end; fun del_pat cpat thy = let val bd = BlockData.get thy; val _ = assert_open bd; val bd = bd_add_del_pats [cpat] bd; val thy = BlockData.map (K bd) thy; in thy end; fun add_pat_eq cpat thms thy = let val _ = is_proper_pat cpat orelse raise CTERM ("add_pat_eq: Not a proper pattern",[cpat]); fun ntp thm = case try norm_thm_pat (thm,cpat) of NONE => raise THM ("add_pat_eq: Theorem does not match pattern",~1,[thm]) | SOME thm => thm; val thms = map ntp thms; val thy = BlockData.map (bd_add_add_pateqs [(cpat,thms)]) thy; in thy end; local fun cpat_of_thm thm = let fun strip ct = case Thm.term_of ct of (_$Var _) => strip (Thm.dest_fun ct) | _ => ct; in strip (Thm.lhs_of thm) end; fun adjust_length (cpat1,cpat2) = let val n1 = cpat1 |> Thm.term_of |> strip_comb |> #2 |> length; val n2 = cpat2 |> Thm.term_of |> strip_comb |> #2 |> length; in if n1>n2 then (funpow (n1-n2) Thm.dest_fun cpat1, cpat2) else (cpat1, funpow (n2-n1) Thm.dest_fun cpat2) end fun find_match cpat cpat' = SOME (cpat,rename_cterm (cpat',cpat)) handle Pattern.MATCH => (case Thm.term_of cpat' of _$_ => find_match (Thm.dest_fun cpat) (Thm.dest_fun cpat') | _ => NONE ); (* Common head of definitional theorems *) fun comp_head thms = case map norm_def_thm thms of [] => NONE | thm::thms => let fun ch [] r = SOME r | ch (thm::thms) (cpat,acc) = let val cpat' = cpat_of_thm thm; val (cpat,cpat') = adjust_length (cpat,cpat') in case find_match cpat cpat' of NONE => NONE | SOME (cpat,inst) => ch thms (cpat, Drule.instantiate_normalize inst thm :: acc) end; in ch thms (cpat_of_thm thm,[thm]) end; in fun lc_decl_eq thms lthy = case comp_head thms of SOME (cpat,thms) => let val _ = if !tracing_enabled then tracing ("decl_eq: " ^ @{make_string} cpat ^ ": " ^ @{make_string} thms) else (); fun decl m = let val cpat'::thms' = Morphism.fact m (Drule.mk_term cpat :: thms); val cpat' = Drule.dest_term cpat'; in Context.mapping (BlockData.map (bd_add_add_pateqs [(cpat',thms')])) I end in lthy |> Local_Theory.declaration {syntax = false, pervasive = false} decl end | NONE => raise THM ("Locale_Code.lc_decl_eq: No common pattern",~1,thms); end; fun lc_decl_del pat = let val ty = fastype_of pat; val dpat = Const (@{const_name LC_DEL},ty --> @{typ unit})$pat; in Spec_Rules.add Binding.empty Spec_Rules.Unknown [dpat] [] end (* Package setup *) val setup = FoldSSData.setup; end \ setup Locale_Code.setup attribute_setup lc_delete = \ Parse.and_list1' ICF_Tools.parse_cpat >> (fn cpats => Thm.declaration_attribute (K (Context.mapping (fold Locale_Code.del_pat cpats) I))) \ "Locale_Code: Delete patterns for current block" attribute_setup lc_add = \ Parse.and_list1' (ICF_Tools.parse_cpat -- Attrib.thms) >> (fn peqs => Thm.declaration_attribute (K (Context.mapping (fold (uncurry Locale_Code.add_pat_eq) peqs) I))) \ "Locale_Code: Add pattern-eqs for current block" end diff --git a/thys/Forcing/ROOT b/thys/Forcing/ROOT --- a/thys/Forcing/ROOT +++ b/thys/Forcing/ROOT @@ -1,21 +1,21 @@ chapter AFP -session Forcing (AFP) = "ZF-Constructible" + +session Forcing (AFP) = "ZF-Constructible" + description " Formalization of Forcing in Isabelle/ZF We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. " - options [timeout=300] + options [timeout = 300] theories [document = false] Utils theories "Rasiowa_Sikorski" "Forcing_Main" document_files "root.tex" "root.bib" "root.bst" diff --git a/thys/Forcing/Synthetic_Definition.thy b/thys/Forcing/Synthetic_Definition.thy --- a/thys/Forcing/Synthetic_Definition.thy +++ b/thys/Forcing/Synthetic_Definition.thy @@ -1,126 +1,128 @@ section\Automatic synthesis of formulas\ theory Synthetic_Definition imports Utils keywords "synthesize" :: thy_decl % "ML" and "synthesize_notc" :: thy_decl % "ML" and "from_schematic" begin ML\ val $` = curry ((op $) o swap) infix $` fun pair f g x = (f x, g x) fun display kind pos (thms,thy) = let val _ = Proof_Display.print_results true pos thy ((kind,""),[thms]) in thy end fun prove_tc_form goal thms ctxt = Goal.prove ctxt [] [] goal (fn _ => rewrite_goal_tac ctxt thms 1 THEN TypeCheck.typecheck_tac ctxt) fun prove_sats goal thms thm_auto ctxt = let val ctxt' = ctxt |> Simplifier.add_simp (thm_auto |> hd) in Goal.prove ctxt [] [] goal (fn _ => rewrite_goal_tac ctxt thms 1 THEN PARALLEL_ALLGOALS (asm_simp_tac ctxt') THEN TypeCheck.typecheck_tac ctxt') end fun is_mem (@{const mem} $ _ $ _) = true | is_mem _ = false fun synth_thm_sats def_name term lhs set env hyps vars vs pos thm_auto lthy = let val (_,tm,ctxt1) = Utils.thm_concl_tm lthy term val (thm_refs,ctxt2) = Variable.import true [Proof_Context.get_thm lthy term] ctxt1 |>> #2 val vs' = map (Thm.term_of o #2) vs val vars' = map (Thm.term_of o #2) vars val r_tm = tm |> Utils.dest_lhs_def |> fold (op $`) vs' val sats = @{const apply} $ (@{const satisfies} $ set $ r_tm) $ env val rhs = @{const IFOL.eq(i)} $ sats $ (@{const succ} $ @{const zero}) val concl = @{const IFOL.iff} $ lhs $ rhs val g_iff = Logic.list_implies(hyps, Utils.tp concl) val thm = prove_sats g_iff thm_refs thm_auto ctxt2 val name = Binding.name (def_name ^ "_iff_sats") val thm = Utils.fix_vars thm (map (#1 o dest_Free) vars') lthy in Local_Theory.note ((name, []), [thm]) lthy |> display "theorem" pos end fun synth_thm_tc def_name term hyps vars pos lthy = let val (_,tm,ctxt1) = Utils.thm_concl_tm lthy term val (thm_refs,ctxt2) = Variable.import true [Proof_Context.get_thm lthy term] ctxt1 |>> #2 val vars' = map (Thm.term_of o #2) vars val tc_attrib = @{attributes [TC]} val r_tm = tm |> Utils.dest_lhs_def |> fold (op $`) vars' val concl = @{const mem} $ r_tm $ @{const formula} val g = Logic.list_implies(hyps, Utils.tp concl) val thm = prove_tc_form g thm_refs ctxt2 val name = Binding.name (def_name ^ "_type") val thm = Utils.fix_vars thm (map (#1 o dest_Free) vars') ctxt2 in Local_Theory.note ((name, tc_attrib), [thm]) lthy |> display "theorem" pos end fun synthetic_def def_name thmref pos tc auto thy = let val (thm_ref,_) = thmref |>> Facts.ref_name - val (((_,vars),thm_tms),_) = Variable.import true [Proof_Context.get_thm thy thm_ref] thy + val thm = Proof_Context.get_thm thy thm_ref; + val thm_vars = rev (Term.add_vars (Thm.full_prop_of thm) []); + val (((_,inst),thm_tms),_) = Variable.import true [thm] thy + val vars = map (fn v => (v, the (Term_Subst.Vars.lookup inst v))) thm_vars; val (tm,hyps) = thm_tms |> hd |> pair Thm.concl_of Thm.prems_of val (lhs,rhs) = tm |> Utils.dest_iff_tms o Utils.dest_trueprop val ((set,t),env) = rhs |> Utils.dest_sats_frm - fun olist t = Ord_List.make String.compare (Term.add_free_names t []) fun relevant ts (@{const mem} $ t $ _) = not (Term.is_Free t) orelse - Ord_List.member String.compare ts (t |> Term.dest_Free |> #1) + member (op =) ts (t |> Term.dest_Free |> #1) | relevant _ _ = false - val t_vars = olist t - val vs = List.filter (fn (((v,_),_),_) => Utils.inList v t_vars) vars - val at = List.foldr (fn ((_,var),t') => lambda (Thm.term_of var) t') t vs - val hyps' = List.filter (relevant t_vars o Utils.dest_trueprop) hyps + val t_vars = sort_strings (Term.add_free_names t []) + val vs = filter (member (op =) t_vars o #1 o #1 o #1) vars + val at = fold_rev (lambda o Thm.term_of o #2) vs t + val hyps' = filter (relevant t_vars o Utils.dest_trueprop) hyps in Local_Theory.define ((Binding.name def_name, NoSyn), ((Binding.name (def_name ^ "_def"), []), at)) thy |> #2 |> (if tc then synth_thm_tc def_name (def_name ^ "_def") hyps' vs pos else I) |> (if auto then synth_thm_sats def_name (def_name ^ "_def") lhs set env hyps vars vs pos thm_tms else I) end \ ML\ local val synth_constdecl = Parse.position (Parse.string -- ((Parse.$$$ "from_schematic" |-- Parse.thm))); val _ = Outer_Syntax.local_theory \<^command_keyword>\synthesize\ "ML setup for synthetic definitions" (synth_constdecl >> (fn ((bndg,thm),p) => synthetic_def bndg thm p true true)) val _ = Outer_Syntax.local_theory \<^command_keyword>\synthesize_notc\ "ML setup for synthetic definitions" (synth_constdecl >> (fn ((bndg,thm),p) => synthetic_def bndg thm p false false)) in end \ text\The \<^ML>\synthetic_def\ function extracts definitions from schematic goals. A new definition is added to the context. \ (* example of use *) (* schematic_goal mem_formula_ex : assumes "m\nat" "n\ nat" "env \ list(M)" shows "nth(m,env) \ nth(n,env) \ sats(M,?frm,env)" by (insert assms ; (rule sep_rules empty_iff_sats cartprod_iff_sats | simp del:sats_cartprod_fm)+) synthesize "\" from_schematic mem_formula_ex *) end diff --git a/thys/Forcing/utils.ML b/thys/Forcing/utils.ML --- a/thys/Forcing/utils.ML +++ b/thys/Forcing/utils.ML @@ -1,126 +1,124 @@ signature UTILS = sig val binop : term -> term -> term -> term val add_: term -> term -> term val app_: term -> term -> term val concat_: term -> term -> term val dest_apply: term -> term * term val dest_iff_lhs: term -> term val dest_iff_rhs: term -> term val dest_iff_tms: term -> term * term val dest_lhs_def: term -> term val dest_rhs_def: term -> term val dest_satisfies_tms: term -> term * term val dest_satisfies_frm: term -> term val dest_eq_tms: term -> term * term val dest_sats_frm: term -> (term * term) * term val dest_trueprop: term -> term val eq_: term -> term -> term val fix_vars: thm -> string list -> Proof.context -> thm val formula_: term val freeName: term -> string - val inList: ''a -> ''a list -> bool val isFree: term -> bool val length_: term -> term val list_: term -> term val lt_: term -> term -> term val mem_: term -> term -> term val mk_FinSet: term list -> term val mk_Pair: term -> term -> term val mk_ZFlist: ('a -> term) -> 'a list -> term val mk_ZFnat: int -> term val nat_: term val nth_: term -> term -> term val subset_: term -> term -> term val thm_concl_tm : Proof.context -> xstring -> - ((indexname * typ) * cterm) list * term * Proof.context + cterm Term_Subst.Vars.table * term * Proof.context val to_ML_list: term -> term list val tp: term -> term end structure Utils : UTILS = struct (* Smart constructors for ZF-terms *) -fun inList a = exists (fn b => a = b) - fun binop h t u = h $ t $ u val mk_Pair = binop @{const Pair} fun mk_FinSet nil = @{const zero} | mk_FinSet (e :: es) = @{const cons} $ e $ mk_FinSet es fun mk_ZFnat 0 = @{const zero} | mk_ZFnat n = @{const succ} $ mk_ZFnat (n-1) fun mk_ZFlist _ nil = @{const "Nil"} | mk_ZFlist f (t :: ts) = @{const "Cons"} $ f t $ mk_ZFlist f ts fun to_ML_list (@{const Nil}) = nil | to_ML_list (@{const Cons} $ t $ ts) = t :: to_ML_list ts | to_ML_list _ = nil fun isFree (Free (_,_)) = true | isFree _ = false fun freeName (Free (n,_)) = n | freeName _ = error "Not a free variable" val app_ = binop @{const apply} fun tp x = @{const Trueprop} $ x fun length_ env = @{const length} $ env val nth_ = binop @{const nth} val add_ = binop @{const add} val mem_ = binop @{const mem} val subset_ = binop @{const Subset} val lt_ = binop @{const lt} val concat_ = binop @{const app} val eq_ = binop @{const IFOL.eq(i)} (* Abbreviation for sets *) fun list_ set = @{const list} $ set val nat_ = @{const nat} val formula_ = @{const formula} (** Destructors of terms **) fun dest_eq_tms (Const (@{const_name IFOL.eq},_) $ t $ u) = (t, u) | dest_eq_tms t = raise TERM ("dest_eq_tms", [t]) fun dest_lhs_def (Const (@{const_name Pure.eq},_) $ x $ _) = x | dest_lhs_def t = raise TERM ("dest_lhs_def", [t]) fun dest_rhs_def (Const (@{const_name Pure.eq},_) $ _ $ y) = y | dest_rhs_def t = raise TERM ("dest_rhs_def", [t]) fun dest_apply (@{const apply} $ t $ u) = (t,u) | dest_apply t = raise TERM ("dest_applies_op", [t]) fun dest_satisfies_tms (@{const Formula.satisfies} $ A $ f) = (A,f) | dest_satisfies_tms t = raise TERM ("dest_satisfies_tms", [t]); val dest_satisfies_frm = #2 o dest_satisfies_tms fun dest_sats_frm t = t |> dest_eq_tms |> #1 |> dest_apply |>> dest_satisfies_tms ; fun dest_trueprop (@{const IFOL.Trueprop} $ t) = t | dest_trueprop t = t fun dest_iff_tms (@{const IFOL.iff} $ t $ u) = (t, u) | dest_iff_tms t = raise TERM ("dest_iff_tms", [t]) val dest_iff_lhs = #1 o dest_iff_tms val dest_iff_rhs = #2 o dest_iff_tms fun thm_concl_tm ctxt thm_ref = - let val (((_,vars),thm_tms),ctxt1) = Variable.import true [Proof_Context.get_thm ctxt thm_ref] ctxt + let + val (((_,vars),thm_tms),ctxt1) = Variable.import true [Proof_Context.get_thm ctxt thm_ref] ctxt in (vars, thm_tms |> hd |> Thm.concl_of, ctxt1) end fun fix_vars thm vars ctxt = let val (_, ctxt1) = Variable.add_fixes vars ctxt in singleton (Proof_Context.export ctxt1 ctxt) thm end end ; diff --git a/thys/IMP2/lib/subgoal_focus_some.ML b/thys/IMP2/lib/subgoal_focus_some.ML --- a/thys/IMP2/lib/subgoal_focus_some.ML +++ b/thys/IMP2/lib/subgoal_focus_some.ML @@ -1,181 +1,181 @@ (* Generalized version of Subgoal.FOCUS, where the premises to be be focused on can be selected by a filter function. This generalizes the do_prems from bool to Proof.context -> cterm -> bool Author: Peter Lammich. Derived from subgoal_focus.ML. *) signature SUBGOAL_FOCUS_SOME = sig type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: (bool * cterm) list, concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list} type prem_filter = Proof.context -> cterm -> bool val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm val focus: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_some_prems: prem_filter -> Proof.context -> int -> binding list option -> thm -> focus * thm val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> (bool * cterm) list -> int -> thm -> thm -> thm Seq.seq val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic val FOCUS_SOME_PREMS: prem_filter -> (focus -> tactic) -> Proof.context -> int -> tactic end structure Subgoal_Focus_Some : SUBGOAL_FOCUS_SOME = struct type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: (bool * cterm) list, concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list} type prem_filter = Proof.context -> cterm -> bool fun partition P l = (filter P l, filter_out P l) fun invert_perm l = tag_list 0 l |> map swap |> order_list fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st = let val st = raw_st |> Thm.transfer (Proof_Context.theory_of ctxt) |> Raw_Simplifier.norm_hhf_protect ctxt; val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1; val (asms, concl) = (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) val asms = map (`(do_prems ctxt2)) asms val fasms = filter fst asms |> map snd val nasms = filter_out fst asms |> map snd val concl = Drule.list_implies (nasms, concl) val text = fasms @ (if do_concl then [concl] else []); - val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2; - val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst); + val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2; + val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst []; - val schematics = (schematic_types, schematic_terms); + val schematics = (Term_Subst.TVars.dest schematic_types, schematic_terms); val asms' = map (apsnd (Thm.instantiate_cterm schematics)) asms; val fasms' = filter fst asms' |> map snd val concl' = Thm.instantiate_cterm schematics concl; val (prems, context) = Assumption.add_assumes fasms' ctxt3; in ({context = context, params = params, prems = prems, asms = asms', concl = concl', schematics = schematics}, Goal.init concl') end; val focus_params = gen_focus (K (K false), false); val focus_params_fixed = gen_focus (K (K false), true); val focus_prems = gen_focus (K (K true), false); val focus = gen_focus (K (K true), true); fun focus_some_prems flt = gen_focus (flt,false) (* B [?'b, ?y] ---------------- B ['b, y params] *) fun lift_import idx params th ctxt = let val ((_, [th']), ctxt') = Variable.importT [th] ctxt; val Ts = map Thm.typ_of_cterm params; val ts = map Thm.term_of params; val prop = Thm.full_prop_of th'; val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []; val vars = rev (Term.add_vars prop []); val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt'; fun var_inst v y = let val ((x, i), T) = v; val (U, args) = if member (op =) concl_vars v then (T, []) else (Ts ---> T, ts); val u = Free (y, U); in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; val (inst1, inst2) = split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys)); val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th'; in ((inst2, th''), ctxt'') end; (* [x, A x] : B x ==> C ------------------ [!!x. A x ==> B x] : C *) fun lift_subgoals ctxt params asms th = let fun lift ct = fold_rev (Thm.all_name ctxt) params (Drule.list_implies (asms, ct)); val unlift = fold (Thm.elim_implies o Thm.assume) asms o Drule.forall_elim_list (map #2 params) o Thm.assume; val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th)); val th' = fold (Thm.elim_implies o unlift) subgoals th; in (subgoals, th') end; fun retrofit ctxt1 ctxt0 params all_asms i st1 st0 = let val asms = filter fst all_asms |> map snd val perm = tag_list 0 all_asms |> partition (fst o snd) |> op @ |> map fst val perm = invert_perm perm val idx = Thm.maxidx_of st0 + 1; val ps = map #2 params; val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1; val (subgoals, st3) = lift_subgoals ctxt2 params asms st2; val result = st3 |> Goal.conclude |> Drule.implies_intr_list asms |> Drule.rearrange_prems perm |> Drule.forall_intr_list ps |> Drule.implies_intr_list subgoals |> fold_rev (Thm.forall_intr o #1) subgoal_inst |> fold (Thm.forall_elim o #2) subgoal_inst |> Thm.adjust_maxidx_thm idx |> singleton (Variable.export ctxt2 ctxt0); in Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false} (false, result, Thm.nprems_of st1) i st0 end; fun GEN_FOCUS flags tac ctxt i st = if Thm.nprems_of st < i then Seq.empty else let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags (ctxt |> Variable.set_bound_focus true) i NONE st; in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end; val FOCUS_PARAMS = GEN_FOCUS (K (K false), false); val FOCUS_PARAMS_FIXED = GEN_FOCUS (K (K false), true); val FOCUS_PREMS = GEN_FOCUS (K (K true), false); val FOCUS = GEN_FOCUS (K (K true), true); fun FOCUS_SOME_PREMS flt = GEN_FOCUS (flt, true); end diff --git a/thys/Nominal2/nominal_dt_alpha.ML b/thys/Nominal2/nominal_dt_alpha.ML --- a/thys/Nominal2/nominal_dt_alpha.ML +++ b/thys/Nominal2/nominal_dt_alpha.ML @@ -1,878 +1,878 @@ (* Title: nominal_dt_alpha.ML Author: Cezary Kaliszyk Author: Christian Urban Definitions and proofs for the alpha-relations. *) signature NOMINAL_DT_ALPHA = sig val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list -> Proof.context -> alpha_result * local_theory val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> thm list * thm list val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> thm list -> thm list val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list val mk_funs_rsp: Proof.context -> thm -> thm val mk_alpha_permute_rsp: Proof.context -> thm -> thm end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = struct open Nominal_Permeq open Nominal_Dt_Data fun lookup xs x = the (AList.lookup (op=) xs x) fun group xs = AList.group (op=) xs (** definition of the inductive rules for alpha and alpha_bn **) (* construct the compound terms for prod_fv and prod_alpha *) fun mk_prod_fv (t1, t2) = let val ty1 = fastype_of t1 val ty2 = fastype_of t2 val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"} in Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2 end fun mk_prod_alpha (t1, t2) = let val ty1 = fastype_of t1 val ty2 = fastype_of t2 val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) val resT = [prodT, prodT] ---> @{typ "bool"} in Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 end (* generates the compound binder terms *) fun comb_binders lthy bmode args binders = let fun bind_set lthy args (NONE, i) = setify lthy (nth args i) | bind_set _ args (SOME bn, i) = bn $ (nth args i) fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) | bind_lst _ args (SOME bn, i) = bn $ (nth args i) val (combine_fn, bind_fn) = case bmode of Lst => (mk_append, bind_lst) | Set => (mk_union, bind_set) | Res => (mk_union, bind_set) in binders |> map (bind_fn lthy args) |> foldl1 combine_fn end (* produces the term for an alpha with abstraction *) fun mk_alpha_term bmode fv alpha args args' binders binders' = let val (alpha_name, binder_ty) = case bmode of Lst => (@{const_name "alpha_lst"}, @{typ "atom list"}) | Set => (@{const_name "alpha_set"}, @{typ "atom set"}) | Res => (@{const_name "alpha_res"}, @{typ "atom set"}) val ty = fastype_of args val pair_ty = HOLogic.mk_prodT (binder_ty, ty) val alpha_ty = [ty, ty] ---> @{typ "bool"} val fv_ty = ty --> @{typ "atom set"} val pair_lhs = HOLogic.mk_prod (binders, args) val pair_rhs = HOLogic.mk_prod (binders', args') in HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs) end (* for non-recursive binders we have to produce alpha_bn premises *) fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = case binder of (NONE, _) => [] | (SOME bn, i) => if member (op=) bodies i then [] else [lookup alpha_bn_map bn $ nth args i $ nth args' i] (* generate the premises for an alpha rule; mk_frees is used if no binders are present *) fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = let fun mk_frees i = let val arg = nth args i val arg' = nth args' i val ty = fastype_of arg in if nth is_rec i then fst (lookup alpha_map ty) $ arg $ arg' else HOLogic.mk_eq (arg, arg') end fun mk_alpha_fv i = let val ty = fastype_of (nth args i) in case AList.lookup (op=) alpha_map ty of NONE => (HOLogic.eq_const ty, supp_const ty) | SOME (alpha, fv) => (alpha, fv) end in case bclause of BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies | BC (bmode, binders, bodies) => let val (alphas, fvs) = split_list (map mk_alpha_fv bodies) val comp_fv = foldl1 mk_prod_fv fvs val comp_alpha = foldl1 mk_prod_alpha alphas val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) val comp_binders = comb_binders lthy bmode args binders val comp_binders' = comb_binders lthy bmode args' binders val alpha_prem = mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) in map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems) end end (* produces the introduction rule for an alpha rule *) fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) val alpha = fst (lookup alpha_map ty) val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses in Library.foldr Logic.mk_implies (flat prems, concl) end (* produces the premise of an alpha-bn rule; we only need to treat the case special where the binding clause is empty; - if the body is not included in the bn_info, then we either produce an equation or an alpha-premise - if the body is included in the bn_info, then we create either a recursive call to alpha-bn, or no premise *) fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause = let fun mk_alpha_bn_prem i = let val arg = nth args i val arg' = nth args' i val ty = fastype_of arg in case AList.lookup (op=) bn_args i of NONE => (case (AList.lookup (op=) alpha_map ty) of NONE => [HOLogic.mk_eq (arg, arg')] | SOME (alpha, _) => [alpha $ arg $ arg']) | SOME (NONE) => [] | SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg'] end in case bclause of BC (_, [], bodies) => map HOLogic.mk_Trueprop (flat (map mk_alpha_bn_prem bodies)) | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause end fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) val alpha_bn = lookup alpha_bn_map bn_trm val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses in Library.foldr Logic.mk_implies (flat prems, concl) end fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let val nth_constrs_info = nth constrs_info bn_n val nth_bclausess = nth bclausesss bn_n in map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy = let val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_names val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys val alpha_frees = map Free (alpha_names ~~ alpha_tys) val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs) val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val alpha_bn_names = map (prefix "alpha_") bn_names val alpha_bn_arg_tys = map (nth raw_tys) bn_tys val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) val alpha_bn_map = bns ~~ alpha_bn_frees val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) val all_alpha_intros = map (pair Binding.empty_atts) (flat alpha_intros @ flat alpha_bn_intros) val (alpha_info, lthy') = lthy |> Local_Theory.begin_nested |> snd |> Inductive.add_inductive {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false} all_alpha_names [] all_alpha_intros [] |> Local_Theory.end_nested_result Inductive.transform_result; val phi = Proof_Context.export_morphism lthy' (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy); val alpha_info_global = Inductive.transform_result phi alpha_info; val all_alpha_trms = #preds alpha_info_global |> map Type.legacy_freeze (*FIXME*) val alpha_raw_induct = #raw_induct alpha_info_global val alpha_intros = #intrs alpha_info_global; val alpha_cases = #elims alpha_info_global; val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms val alpha_tys = map (domain_type o fastype_of) alpha_trms val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms val alpha_names = map (fst o dest_Const) alpha_trms val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms in (AlphaResult {alpha_names = alpha_names, alpha_trms = alpha_trms, alpha_tys = alpha_tys, alpha_bn_names = alpha_bn_names, alpha_bn_trms = alpha_bn_trms, alpha_bn_tys = alpha_bn_tys, alpha_intros = alpha_intros, alpha_cases = alpha_cases, alpha_raw_induct = alpha_raw_induct}, lthy') end (** induction proofs **) (* proof by structural induction over data types *) fun induct_prove tys props induct_thm cases_tac ctxt = let val (arg_names, ctxt') = Variable.variant_fixes (replicate (length tys) "x") ctxt val args = map2 (curry Free) arg_names tys val true_trms = replicate (length tys) (K @{term True}) fun apply_all x fs = map (fn f => f x) fs val goals = group (props @ (tys ~~ true_trms)) |> map snd |> map2 apply_all args |> map fold_conj |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop fun tac ctxt = HEADGOAL (DETERM o (resolve_tac ctxt [induct_thm]) THEN_ALL_NEW (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt]))) in Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map Old_Datatype_Aux.split_conj_thm |> flat |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end (* proof by rule induction over the alpha-definitions *) fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt = let val arg_tys = map (domain_type o fastype_of) alphas val ((arg_names1, arg_names2), ctxt') = ctxt |> Variable.variant_fixes (replicate (length alphas) "x") ||>> Variable.variant_fixes (replicate (length alphas) "y") val args1 = map2 (curry Free) arg_names1 arg_tys val args2 = map2 (curry Free) arg_names2 arg_tys val true_trms = replicate (length alphas) (K @{term True}) fun apply_all x fs = map (fn f => f x) fs val goals_rhs = group (props @ (alphas ~~ true_trms)) |> map snd |> map2 apply_all (args1 ~~ args2) |> map fold_conj fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2 val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2) val goals = (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs) |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop fun tac ctxt = HEADGOAL (DETERM o (resolve_tac ctxt [alpha_induct_thm]) THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt]) in Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map (fn th => th RS mp) |> map Old_Datatype_Aux.split_conj_thm |> flat |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end (** produces the distinctness theorems **) (* transforms the distinctness theorems of the constructors into "not-alphas" of the constructors *) fun mk_distinct_goal ty_trm_assoc neq = let val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = HOLogic.dest_not (HOLogic.dest_Trueprop neq) val ty_str = fst (dest_Type (domain_type ty_eq)) in Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |> HOLogic.mk_not |> HOLogic.mk_Trueprop end fun distinct_tac ctxt cases_thms distinct_thms = resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info val ty_trm_assoc = raw_dt_names ~~ alpha_names fun mk_alpha_distinct raw_distinct_trm = let val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm in Goal.prove ctxt [] [] goal (K (distinct_tac ctxt alpha_cases raw_distinct_thms 1)) end in map (mk_alpha_distinct o Thm.prop_of) raw_distinct_thms end (** produces the alpha_eq_iff simplification rules **) (* in case a theorem is of the form (Rel Const Const), it will be rewritten to ((Rel Const = Const) = True) *) fun mk_simp_rule thm = case Thm.prop_of thm of @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} | _ => thm fun alpha_eq_iff_tac ctxt dist_inj intros elims = SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' (resolve_tac ctxt @{thms iffI} THEN' RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) fun mk_alpha_eq_iff_goal thm = let val prop = Thm.prop_of thm; val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); fun list_conj l = foldr1 HOLogic.mk_conj l; in if hyps = [] then HOLogic.mk_Trueprop concl else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) end; fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; val goals = map mk_alpha_eq_iff_goal thms_imp; val tac = alpha_eq_iff_tac ctxt (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; in Variable.export ctxt' ctxt thms |> map mk_simp_rule end (** reflexivity proof for the alphas **) val exi_zero = @{lemma "P (0::perm) \ (\x. P x)" by auto} fun cases_tac intros ctxt = let val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv} val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt val bound_tac = EVERY' [ resolve_tac ctxt [exi_zero], resolve_tac ctxt @{thms alpha_refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] in resolve_tac ctxt intros THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac] end fun raw_prove_refl ctxt alpha_result raw_dt_induct = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} = alpha_result val props = map (fn (ty, c) => (ty, fn x => c $ x $ x)) ((alpha_tys ~~ alpha_trms) @ (alpha_bn_tys ~~ alpha_bn_trms)) in induct_prove alpha_tys props raw_dt_induct (cases_tac alpha_intros) ctxt end (** symmetry proof for the alphas **) val exi_neg = @{lemma "(\(p::perm). P p) \ (\q. P q \ Q (- q)) \ \p. Q p" by (erule exE, rule_tac x="-p" in exI, auto)} (* for premises that contain binders *) fun prem_bound_tac pred_names alpha_eqvt ctxt = let fun trans_prem_tac pred_names ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val prems' = map (transform_prem1 ctxt' pred_names) prems in resolve_tac ctxt' prems' 1 end) ctxt val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas} in EVERY' [ eresolve_tac ctxt [exi_neg], resolve_tac ctxt @{thms alpha_sym_eqvt}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' resolve_tac ctxt @{thms refl}, trans_prem_tac pred_names ctxt] end fun raw_prove_sym ctxt alpha_result alpha_eqvt = let val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, alpha_intros, alpha_raw_induct, ...} = alpha_result val alpha_trms = alpha_trms @ alpha_bn_trms val alpha_names = alpha_names @ alpha_bn_names val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms fun tac ctxt = resolve_tac ctxt alpha_intros THEN_ALL_NEW FIRST' [assume_tac ctxt, resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt, prem_bound_tac alpha_names alpha_eqvt ctxt] in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt end (** transitivity proof for alphas **) (* applies cases rules and resolves them with the last premise *) fun ecases_tac cases = Subgoal.FOCUS (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems])) fun aatac pred_names = SUBPROOF (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems))) (* instantiates exI with the permutation p + q *) val perm_inst_tac = Subgoal.FOCUS (fn {context = ctxt, params, ...} => let val (p, q) = apply2 snd (last2 params) val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q] val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} in HEADGOAL (resolve_tac ctxt [exi_inst]) end) fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = let val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv} in resolve_tac ctxt intros THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' TRY o EVERY' (* if binders are present *) [ eresolve_tac ctxt @{thms exE}, eresolve_tac ctxt @{thms exE}, perm_inst_tac ctxt, resolve_tac ctxt @{thms alpha_trans_eqvt}, assume_tac ctxt, aatac pred_names ctxt, eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' resolve_tac ctxt @{thms refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) end fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result val alpha_names = alpha_names @ alpha_bn_names fun all_cases ctxt = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt in EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms impI}, ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] end fun prep_trans_goal alpha_trm (arg1, arg2) = let val arg_ty = fastype_of arg1 val mid = alpha_trm $ arg2 $ (Bound 0) val rhs = alpha_trm $ arg1 $ (Bound 0) in HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) end fun raw_prove_trans ctxt alpha_result raw_dt_thms alpha_eqvt = let val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val alpha_trms = alpha_trms @ alpha_bn_trms val props = map prep_trans_goal alpha_trms in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct (prove_trans_tac alpha_result raw_dt_thms alpha_eqvt) ctxt end (** proves the equivp predicate for all alphas **) val reflp_def' = @{lemma "reflp R == \x. R x x" by (simp add: reflp_def refl_on_def)} val symp_def' = @{lemma "symp R \ \x y . R x y --> R y x" by (simp add: symp_def sym_def)} val transp_def' = @{lemma "transp R \ \x y. R x y \ (\z. R y z \ R x z)" by (rule eq_reflection, auto simp add: trans_def transp_def)} fun raw_prove_equivp ctxt alpha_result refl symm trans = let val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result val refl' = map (fold_rule ctxt [reflp_def'] o atomize ctxt) refl val symm' = map (fold_rule ctxt [symp_def'] o atomize ctxt) symm val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans fun prep_goal t = HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) in Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN' RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans'])))) |> chop (length alpha_trms) end (* proves that alpha_raw implies alpha_bn *) fun raw_prove_bn_imp_tac alpha_result ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 ctxt' alpha_names) prems' in HEADGOAL (REPEAT_ALL_NEW (FIRST' [ resolve_tac ctxt' @{thms TrueI}, resolve_tac ctxt' @{thms conjI}, resolve_tac ctxt' prems', resolve_tac ctxt' prems'', resolve_tac ctxt' alpha_intros ])) end) ctxt fun raw_prove_bn_imp ctxt alpha_result = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val arg_ty = domain_type o fastype_of val ty_assoc = alpha_tys ~~ alpha_trms val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (raw_prove_bn_imp_tac alpha_result) ctxt end (* respectfulness for fv_raw / bn_raw *) fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val arg_ty = domain_type o fastype_of val ty_assoc = alpha_tys ~~ alpha_trms fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns val simpset = put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set_simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) in alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct (K (asm_full_simp_tac simpset)) ctxt end (* respectfulness for size *) fun raw_size_rsp_aux ctxt alpha_result simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = alpha_result fun mk_prop ty (x, y) = HOLogic.mk_eq (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) val simpset = put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv permute_prod_def prod.case prod.rec}) val tac = (TRY o REPEAT o eresolve_tac ctxt @{thms exE}) THEN' asm_full_simp_tac simpset in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt end (* respectfulness for constructors *) fun raw_constr_rsp_tac ctxt alpha_intros simps = let val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def} val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_conv prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps in asm_full_simp_tac pre_simpset THEN' REPEAT o (resolve_tac ctxt @{thms allI impI}) THEN' resolve_tac ctxt alpha_intros THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset) end fun raw_constrs_rsp ctxt alpha_result constrs simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result fun lookup ty = case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of NONE => HOLogic.eq_const ty | SOME alpha => alpha fun rel_fun_app (t1, t2) = Const (@{const_name "rel_fun"}, dummyT) $ t1 $ t2 fun prep_goal trm = trm |> strip_type o fastype_of |> (fn (tys, ty) => tys @ [ty]) |> map lookup |> foldr1 rel_fun_app |> (fn t => t $ trm $ trm) |> Syntax.check_term ctxt |> HOLogic.mk_Trueprop in map (fn constrs => Goal.prove_common ctxt NONE [] [] (map prep_goal constrs) (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs end (* rsp lemmas for alpha_bn relations *) val rsp_equivp = @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> (=)) Q Q" by (simp only: rel_fun_def equivp_def, metis)} (* we have to reorder the alpha_bn_imps theorems in order to be in order with alpha_bn_trms *) fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps = let val AlphaResult {alpha_bn_trms, ...} = alpha_result fun mk_map thm = thm |> `Thm.prop_of |>> List.last o snd o strip_comb |>> HOLogic.dest_Trueprop |>> head_of |>> fst o dest_Const val alpha_bn_imps' = map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms fun mk_thm thm1 thm2 = - (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) + (Thm.forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) in map2 mk_thm alpha_bn_equivp alpha_bn_imps' end (* rsp for permute_bn functions *) val perm_bn_rsp = @{lemma "(\x y p. R x y \ R (f p x) (f p y)) \ ((=) ===> R ===> R) f f" by (simp add: rel_fun_def)} fun raw_prove_perm_bn_tac alpha_result simps ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems' in HEADGOAL (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems')) THEN' TRY o REPEAT_ALL_NEW (FIRST' [ resolve_tac ctxt' @{thms TrueI}, resolve_tac ctxt' @{thms conjI}, resolve_tac ctxt' @{thms refl}, resolve_tac ctxt' prems', resolve_tac ctxt' prems'', resolve_tac ctxt' alpha_intros ])) end) ctxt fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = alpha_result val perm_bn_ty = range_type o range_type o fastype_of val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms) val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) fun mk_prop t = let val alpha_trm = lookup ty_assoc (perm_bn_ty t) in (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y)) end val goals = map mk_prop perm_bns in alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct (raw_prove_perm_bn_tac alpha_result simps) ctxt |> Proof_Context.export ctxt' ctxt |> map (atomize ctxt) |> map single |> map (curry (op OF) perm_bn_rsp) end (* transformation of the natural rsp-lemmas into standard form *) val fun_rsp = @{lemma "(\x y. R x y \ f x = f y) \ (R ===> (=)) f f" by (simp add: rel_fun_def)} fun mk_funs_rsp ctxt thm = thm |> atomize ctxt |> single |> curry (op OF) fun_rsp val permute_rsp = @{lemma "(\x y p. R x y \ R (permute p x) (permute p y)) ==> ((=) ===> R ===> R) permute permute" by (simp add: rel_fun_def)} fun mk_alpha_permute_rsp ctxt thm = thm |> atomize ctxt |> single |> curry (op OF) permute_rsp end (* structure *) diff --git a/thys/Nominal2/nominal_function_core.ML b/thys/Nominal2/nominal_function_core.ML --- a/thys/Nominal2/nominal_function_core.ML +++ b/thys/Nominal2/nominal_function_core.ML @@ -1,1104 +1,1104 @@ (* Nominal Function Core Author: Christian Urban heavily based on the code of Alexander Krauss (code forked on 14 January 2011) Core of the nominal function package. *) signature NOMINAL_FUNCTION_CORE = sig val trace: bool Unsynchronized.ref val prepare_nominal_function : Nominal_Function_Common.nominal_function_config -> string (* defname *) -> ((bstring * typ) * mixfix) list (* defined symbol *) -> ((bstring * typ) list * term list * term * term) list (* specification *) -> local_theory -> (term (* f *) * term (* G(raph) *) * thm list (* GIntros *) * thm (* Ginduct *) * thm (* goalstate *) * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* continuation *) ) * local_theory val inductive_def : (binding * typ) * mixfix -> term list -> local_theory -> (term * thm list * thm * thm) * local_theory end structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE = struct val trace = Unsynchronized.ref false fun trace_msg msg = if ! trace then tracing (msg ()) else () val boolT = HOLogic.boolT val mk_eq = HOLogic.mk_eq open Function_Lib open Function_Common open Nominal_Function_Common datatype globals = Globals of {fvar: term, domT: typ, ranT: typ, h: term, y: term, x: term, z: term, a: term, P: term, D: term, Pbool:term} datatype rec_call_info = RCInfo of {RIvs: (string * typ) list, (* Call context: fixes and assumes *) CCas: thm list, rcarg: term, (* The recursive argument *) llRI: thm, h_assum: term} datatype clause_context = ClauseContext of {ctxt : Proof.context, qs : term list, gs : term list, lhs: term, rhs: term, cqs: cterm list, ags: thm list, case_hyp : thm} fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = ClauseContext { ctxt = Proof_Context.transfer thy ctxt, qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } datatype clause_info = ClauseInfo of {no: int, qglr : ((string * typ) list * term list * term * term), cdata : clause_context, tree: Function_Context_Tree.ctx_tree, lGI: thm, RCs: rec_call_info list} (* Theory dependencies. *) val acc_induct_rule = @{thm accp_induct_rule} val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence} val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness} val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff} val acc_downward = @{thm accp_downward} val accI = @{thm accp.accI} val case_split = @{thm HOL.case_split} val fundef_default_value = @{thm Fun_Def.fundef_default_value} val not_acc_down = @{thm not_accp_down} fun find_calls tree = let fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs) | add_Ri _ _ _ _ = raise Match in rev (Function_Context_Tree.traverse_tree add_Ri tree []) end (* nominal *) fun mk_eqvt_at (f_trm, arg_trm) = let val f_ty = fastype_of f_trm val arg_ty = domain_type f_ty in Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm |> HOLogic.mk_Trueprop end fun mk_eqvt trm = let val ty = fastype_of trm in Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm |> HOLogic.mk_Trueprop end fun mk_inv inv (f_trm, arg_trm) = betapplys (inv, [arg_trm, (f_trm $ arg_trm)]) |> HOLogic.mk_Trueprop fun mk_invariant (Globals {x, y, ...}) G invariant = let val prem = HOLogic.mk_Trueprop (G $ x $ y) val concl = HOLogic.mk_Trueprop (betapplys (invariant, [x, y])) in Logic.mk_implies (prem, concl) |> mk_forall_rename ("y", y) |> mk_forall_rename ("x", x) end (** building proof obligations *) fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = mk_eqvt_at (fvar, arg) |> curry Logic.list_implies (map Thm.prop_of assms) |> fold_rev (Logic.all o Free) vs |> fold_rev absfree qs |> strip_abs_body fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = mk_inv inv (fvar, arg) |> curry Logic.list_implies (map Thm.prop_of assms) |> fold_rev (Logic.all o Free) vs |> fold_rev absfree qs |> strip_abs_body (** building proof obligations *) fun mk_compat_proof_obligations domT ranT fvar f RCss inv glrs = let fun mk_impl (((qs, gs, lhs, rhs), RCs_lhs), ((qs', gs', lhs', rhs'), RCs_rhs)) = let val shift = incr_boundvars (length qs') val eqvts_obligations_lhs = map (shift o mk_eqvt_proof_obligation qs fvar) RCs_lhs val eqvts_obligations_rhs = map (mk_eqvt_proof_obligation qs' fvar) RCs_rhs val invs_obligations_lhs = map (shift o mk_inv_proof_obligation inv qs fvar) RCs_lhs val invs_obligations_rhs = map (mk_inv_proof_obligation inv qs' fvar) RCs_rhs in Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |> fold_rev (curry Logic.mk_implies) invs_obligations_rhs (* nominal *) |> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *) |> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *) |> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* nominal *) |> fold_rev (fn (n,T) => fn b => Logic.all_const T $ Abs(n,T,b)) (qs @ qs') |> curry abstract_over fvar |> curry subst_bound f end in map mk_impl (unordered_pairs (glrs ~~ RCss)) end fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = let fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = HOLogic.mk_Trueprop Pbool |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) |> fold_rev (curry Logic.mk_implies) gs |> fold_rev mk_forall_rename (map fst oqs ~~ qs) in HOLogic.mk_Trueprop Pbool |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |> mk_forall_rename ("x", x) |> mk_forall_rename ("P", Pbool) end (** making a context with it's own local bindings **) fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = let val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs fun inst t = subst_bounds (rev qs, t) val gs = map inst pre_gs val lhs = inst pre_lhs val rhs = inst pre_rhs val cqs = map (Thm.cterm_of ctxt') qs val ags = map (Thm.assume o Thm.cterm_of ctxt') gs val case_hyp = Thm.assume (Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) in ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } end (* lowlevel term function. FIXME: remove *) fun abstract_over_list vs body = let fun abs lev v tm = if v aconv tm then Bound lev else (case tm of Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) | t $ u => abs lev v t $ abs lev v u | t => t) in fold_index (fn (i, v) => fn t => abs i v t) vs body end fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = let val Globals {h, ...} = globals val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata val cert = Thm.cterm_of ctxt (* Instantiate the GIntro thm with "f" and import into the clause context. *) val lGI = GIntro_thm |> Thm.forall_elim (cert f) |> fold Thm.forall_elim cqs |> fold Thm.elim_implies ags fun mk_call_info (rcfix, rcassm, rcarg) RI = let val llRI = RI |> fold Thm.forall_elim cqs |> fold (Thm.forall_elim o cert o Free) rcfix |> fold Thm.elim_implies ags |> fold Thm.elim_implies rcassm val h_assum = HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (Logic.all o Free) rcfix |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] [] |> abstract_over_list (rev qs) in RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} end val RC_infos = map2 mk_call_info RCs RIntro_thms in ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos, tree=tree} end fun store_compat_thms 0 thms = [] | store_compat_thms n thms = let val (thms1, thms2) = chop n thms in (thms1 :: store_compat_thms (n - 1) thms2) end (* expects i <= j *) fun lookup_compat_thm i j cts = nth (nth cts (i - 1)) (j - i) (* nominal *) (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) (* if j < i, then turn around *) fun get_compat_thm ctxt cts eqvtsi eqvtsj invsi invsj i j ctxi ctxj = let val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,case_hyp=case_hypi,...} = ctxi val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = ctxj val lhsi_eq_lhsj = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) in if j < i then let val compat = lookup_compat_thm j i cts in compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold Thm.elim_implies eqvtsj (* nominal *) |> fold Thm.elim_implies eqvtsi (* nominal *) |> fold Thm.elim_implies invsj (* nominal *) |> fold Thm.elim_implies invsi (* nominal *) |> fold Thm.elim_implies agsj |> fold Thm.elim_implies agsi |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) end else let val compat = lookup_compat_thm i j cts in compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold Thm.elim_implies eqvtsi (* nominal *) |> fold Thm.elim_implies eqvtsj (* nominal *) |> fold Thm.elim_implies invsi (* nominal *) |> fold Thm.elim_implies invsj (* nominal *) |> fold Thm.elim_implies agsi |> fold Thm.elim_implies agsj |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) end end (* Generates the replacement lemma in fully quantified form. *) fun mk_replacement_lemma ctxt h ih_elim clause = let val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause local open Conv in val ih_conv = arg1_conv o arg_conv o arg_conv end val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs val h_assums = map (fn RCInfo {h_assum, ...} => Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qs, h_assum)))) RCs val (eql, _) = Function_Context_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree val replace_lemma = (eql RS meta_eq_to_obj_eq) |> Thm.implies_intr (Thm.cprop_of case_hyp) |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs |> Thm.close_derivation \<^here> in replace_lemma end (* nominal *) (* Generates the eqvt lemmas for each clause *) fun mk_eqvt_lemma ctxt ih_eqvt clause = let val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause local open Conv in val ih_conv = arg1_conv o arg_conv o arg_conv end val ih_eqvt_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_eqvt_case) |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs in map prep_eqvt RCs |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags) |> map (Thm.implies_intr (Thm.cprop_of case_hyp)) |> map (fold_rev Thm.forall_intr cqs) |> map (Thm.close_derivation \<^here>) end (* nominal *) fun mk_invariant_lemma ctxt ih_inv clause = let val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause local open Conv in val ih_conv = arg1_conv o arg_conv o arg_conv end val ih_inv_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_inv fun prep_inv (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_inv_case) |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs in map prep_inv RCs |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags) |> map (Thm.implies_intr (Thm.cprop_of case_hyp)) |> map (fold_rev Thm.forall_intr cqs) |> map (Thm.close_derivation \<^here>) end (* nominal *) fun mk_uniqueness_clause ctxt globals compat_store eqvts invs clausei clausej RLj = let val thy = Proof_Context.theory_of ctxt val Globals {h, y, x, fvar, ...} = globals val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, ags = agsi, ...}, ...} = clausei val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} = mk_clause_context x ctxti cdescj val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' val Ghsj' = map (fn RCInfo {h_assum, ...} => Thm.assume (Thm.cterm_of ctxt (subst_bounds (rev qsj', h_assum)))) RCsj val y_eq_rhsj'h = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) val lhsi_eq_lhsj' = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj'] val RLj_import = RLj |> fold Thm.forall_elim cqsj' |> fold Thm.elim_implies agsj' |> fold Thm.elim_implies Ghsj' val eqvtsi = nth eqvts (i - 1) |> map (fold Thm.forall_elim cqsi) |> map (fold Thm.elim_implies [case_hyp]) |> map (fold Thm.elim_implies agsi) val eqvtsj = nth eqvts (j - 1) |> map (fold Thm.forall_elim cqsj') |> map (fold Thm.elim_implies [case_hypj']) |> map (fold Thm.elim_implies agsj') val invsi = nth invs (i - 1) |> map (fold Thm.forall_elim cqsi) |> map (fold Thm.elim_implies [case_hyp]) |> map (fold Thm.elim_implies agsi) val invsj = nth invs (j - 1) |> map (fold Thm.forall_elim cqsj') |> map (fold Thm.elim_implies [case_hypj']) |> map (fold Thm.elim_implies agsj') val compat = get_compat_thm ctxt compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj in (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |> Thm.implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |> fold_rev (Thm.implies_intr o Thm.cprop_of) Ghsj' |> fold_rev (Thm.implies_intr o Thm.cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h) |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj') |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj') end (* nominal *) fun mk_uniqueness_case ctxt globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems clausei = let val thy = Proof_Context.theory_of ctxt val Globals {x, y, ranT, fvar, ...} = globals val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs val ih_intro_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ih_intro fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs val existence = fold (curry op COMP o prep_RC) RCs lGI val P = Thm.cterm_of ctxt (mk_eq (y, rhsC)) val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y))) val unique_clauses = map2 (mk_uniqueness_clause ctxt globals compat_store eqvtlems invlems clausei) clauses replems fun elim_implies_eta A AB = Thm.bicompose NONE {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB |> Seq.list_of |> the_single val uniqueness = G_cases |> Thm.forall_elim (Thm.cterm_of ctxt lhs) |> Thm.forall_elim (Thm.cterm_of ctxt y) |> Thm.forall_elim P |> Thm.elim_implies G_lhs_y |> fold elim_implies_eta unique_clauses |> Thm.implies_intr (Thm.cprop_of G_lhs_y) |> Thm.forall_intr (Thm.cterm_of ctxt y) val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) val exactly_one = ex1I |> Thm.instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)] |> curry (op COMP) existence |> curry (op COMP) uniqueness |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym]) |> Thm.implies_intr (Thm.cprop_of case_hyp) |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs val function_value = existence |> Thm.implies_intr ihyp |> Thm.implies_intr (Thm.cprop_of case_hyp) |> Thm.forall_intr (Thm.cterm_of ctxt x) |> Thm.forall_elim (Thm.cterm_of ctxt lhs) |> curry (op RS) refl in (exactly_one, function_value) end (* nominal *) fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def = let val Globals {h, domT, ranT, x, ...} = globals (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |> Thm.cterm_of ctxt val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)] val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at})) val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop})) val _ = trace_msg (K "Proving Replacement lemmas...") val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses val _ = trace_msg (K "Proving Equivariance lemmas...") val eqvtLemmas = map (mk_eqvt_lemma ctxt ih_eqvt) clauses val _ = trace_msg (K "Proving Invariance lemmas...") val invLemmas = map (mk_invariant_lemma ctxt ih_inv) clauses val _ = trace_msg (K "Proving cases for unique existence...") val (ex1s, values) = split_list (map (mk_uniqueness_case ctxt globals G f ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses) val _ = trace_msg (K "Proving: Graph is a function") val graph_is_function = complete |> Thm.forall_elim_vars 0 |> fold (curry op COMP) ex1s |> Thm.implies_intr ihyp |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |> Thm.forall_intr (Thm.cterm_of ctxt x) |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |> (fn it => fold (Thm.forall_intr o Thm.cterm_of ctxt o Var) (Term.add_vars (Thm.prop_of it) []) it) val goalstate = Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt |> Thm.close_derivation \<^here> |> Goal.protect 0 |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat |> Thm.implies_intr (Thm.cprop_of complete) |> Thm.implies_intr (Thm.cprop_of invariant) |> Thm.implies_intr (Thm.cprop_of G_eqvt) in (goalstate, values) end (* wrapper -- restores quantifiers in rule specifications *) fun inductive_def (binding as ((R, T), _)) intrs lthy = let val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = lthy |> Config.put Inductive.inductive_internals true |> Proof_Context.concealed |> Inductive.add_inductive {quiet_mode = true, verbose = ! trace, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = true} [binding] (* relation *) [] (* no parameters *) (map (fn t => (Binding.empty_atts, t)) intrs) (* intro rules *) [] (* no special monos *) ||> Proof_Context.restore_naming lthy ||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals) val cert = Thm.cterm_of lthy fun requantify orig_intro thm = let val (qs, t) = dest_all_all orig_intro val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T) val vars = Term.add_vars (Thm.prop_of thm) [] val varmap = AList.lookup (op =) (frees ~~ map fst vars) #> the_default ("",0) in fold_rev (fn Free (n, T) => forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm end in - ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) + ((Rdef, map2 requantify intrs intrs_gen, Thm.forall_intr_vars elim_gen, induct), lthy) end (* nominal *) fun define_graph Gname fvar domT ranT clauses RCss lthy = let val GT = domT --> ranT --> boolT val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT) fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = let fun mk_h_assm (rcfix, rcassm, rcarg) = HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg)) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (Logic.all o Free) rcfix in HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs) |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |> fold_rev (curry Logic.mk_implies) gs |> fold_rev Logic.all (fvar :: qs) end val G_intros = map2 mk_GIntro clauses RCss in inductive_def ((Binding.name n, T), NoSyn) G_intros lthy end fun define_function fdefname (fname, mixfix) domT ranT G default lthy = let val f_def = Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |> Syntax.check_term lthy in Local_Theory.define ((Binding.name (fname ^ "C"), mixfix), ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy end (* nominal *) fun define_recursion_relation Rname domT qglrs clauses RCss lthy = let val RT = domT --> domT --> boolT val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT) fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (curry Logic.mk_implies) gs |> fold_rev (Logic.all o Free) rcfix |> fold_rev mk_forall_rename (map fst oqs ~~ qs) (* "!!qs xs. CS ==> G => (r, lhs) : R" *) val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss val ((R, RIntro_thms, R_elim, _), lthy) = inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy in ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy) end fun fix_globals domT ranT fvar ctxt = let val ([h, y, x, z, a, D, P, Pbool], ctxt') = Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt in (Globals {h = Free (h, domT --> ranT), y = Free (y, ranT), x = Free (x, domT), z = Free (z, domT), a = Free (a, domT), D = Free (D, domT --> boolT), P = Free (P, domT --> boolT), Pbool = Free (Pbool, boolT), fvar = fvar, domT = domT, ranT = ranT}, ctxt') end fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) = let fun inst_term t = subst_bound(f, abstract_over (fvar, t)) in (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg) end (********************************************************** * PROVING THE RULES **********************************************************) fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function = let val Globals {domT, z, ...} = globals fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = let val lhs_acc = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) val z_smaller = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) in ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) |> (fn it => it COMP graph_is_function) |> Thm.implies_intr z_smaller |> Thm.forall_intr (Thm.cterm_of ctxt z) |> (fn it => it COMP valthm) |> Thm.implies_intr lhs_acc |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff]) |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end in map2 mk_psimp clauses valthms end (** Induction rule **) val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} fun mk_partial_induct_rule ctxt globals R complete_thm clauses = let val Globals {domT, x, z, a, P, D, ...} = globals val acc_R = mk_acc domT R val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x))) val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a)) val D_subset = Thm.cterm_of ctxt (Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), HOLogic.mk_Trueprop (D $ z))))) |> Thm.cterm_of ctxt (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), HOLogic.mk_Trueprop (P $ Bound 0))) |> Thm.cterm_of ctxt val aihyp = Thm.assume ihyp fun prove_case clause = let val ClauseInfo {cdata = ClauseContext {ctxt = ctxt', qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, qglr = (oqs, _, _, _), ...} = clause val case_hyp_conv = K (case_hyp RS eq_reflection) local open Conv in val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D val sih = fconv_rule (Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt') aihyp end fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih |> Thm.forall_elim (Thm.cterm_of ctxt rcarg) |> Thm.elim_implies llRI |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) val step = HOLogic.mk_Trueprop (P $ lhs) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs |> fold_rev (curry Logic.mk_implies) gs |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> Thm.cterm_of ctxt val P_lhs = Thm.assume step |> fold Thm.forall_elim cqs |> Thm.elim_implies lhs_D |> fold Thm.elim_implies ags |> fold Thm.elim_implies P_recs val res = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x)) |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |> Thm.symmetric (* P lhs == P x *) |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) |> Thm.implies_intr (Thm.cprop_of case_hyp) |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |> fold_rev Thm.forall_intr cqs in (res, step) end val (cases, steps) = split_list (map prove_case clauses) val istep = complete_thm |> Thm.forall_elim_vars 0 |> fold (curry op COMP) cases (* P x *) |> Thm.implies_intr ihyp |> Thm.implies_intr (Thm.cprop_of x_D) |> Thm.forall_intr (Thm.cterm_of ctxt x) val subset_induct_rule = acc_subset_induct |> (curry op COMP) (Thm.assume D_subset) |> (curry op COMP) (Thm.assume D_dcl) |> (curry op COMP) (Thm.assume a_D) |> (curry op COMP) istep |> fold_rev Thm.implies_intr steps |> Thm.implies_intr a_D |> Thm.implies_intr D_dcl |> Thm.implies_intr D_subset val simple_induct_rule = subset_induct_rule |> Thm.forall_intr (Thm.cterm_of ctxt D) |> Thm.forall_elim (Thm.cterm_of ctxt acc_R) |> assume_tac ctxt 1 |> Seq.hd |> (curry op COMP) (acc_downward |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)] (map (SOME o Thm.cterm_of ctxt) [R, x, z])) |> Thm.forall_intr (Thm.cterm_of ctxt z) |> Thm.forall_intr (Thm.cterm_of ctxt x)) |> Thm.forall_intr (Thm.cterm_of ctxt a) |> Thm.forall_intr (Thm.cterm_of ctxt P) in simple_induct_rule end (* FIXME: broken by design *) fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = let val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, qglr = (oqs, _, _, _), ...} = clause val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |> fold_rev (curry Logic.mk_implies) gs |> Thm.cterm_of ctxt in Goal.init goal |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1)) |> the |> (SINGLE (auto_tac ctxt)) |> the |> Goal.conclude |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end (** Termination rule **) val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} val wf_in_rel = @{thm Fun_Def.wf_in_rel} val in_rel_def = @{thm Fun_Def.in_rel_def} fun mk_nest_term_case ctxt globals R' ihyp clause = let val Globals {z, ...} = globals val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, qglr=(oqs, _, _, _), ...} = clause val ih_case = full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) ihyp fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = let val used = (u @ sub) |> map (fn (ctx,thm) => Function_Context_Tree.export_thm ctxt ctx thm) val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *) |> Function_Context_Tree.export_term (fixes, assumes) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> Thm.cterm_of ctxt val thm = Thm.assume hyp |> fold Thm.forall_elim cqs |> fold Thm.elim_implies ags |> Function_Context_Tree.import_thm ctxt (fixes, assumes) |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) |> Thm.cterm_of ctxt |> Thm.assume val acc = thm COMP ih_case val z_acc_local = acc |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) val ethm = z_acc_local |> Function_Context_Tree.export_thm ctxt (fixes, z_eq_arg :: case_hyp :: ags @ assumes) |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) val sub' = sub @ [(([],[]), acc)] in (sub', (hyp :: hyps, ethm :: thms)) end | step _ _ _ _ = raise Match in Function_Context_Tree.traverse_tree step tree end fun mk_nest_term_rule ctxt globals R R_cases clauses = let val Globals { domT, x, z, ... } = globals val acc_R = mk_acc domT R val R' = Free ("R", fastype_of R) val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) val inrel_R = Const (@{const_name Fun_Def.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R') |> Thm.cterm_of ctxt (* "wf R'" *) (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) val ihyp = Logic.all_const domT $ Abs ("z", domT, Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), HOLogic.mk_Trueprop (acc_R $ Bound 0))) |> Thm.cterm_of ctxt val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 val R_z_x = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x)) val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], []) in R_cases |> Thm.forall_elim (Thm.cterm_of ctxt z) |> Thm.forall_elim (Thm.cterm_of ctxt x) |> Thm.forall_elim (Thm.cterm_of ctxt (acc_R $ z)) |> curry op COMP (Thm.assume R_z_x) |> fold_rev (curry op COMP) cases |> Thm.implies_intr R_z_x |> Thm.forall_intr (Thm.cterm_of ctxt z) |> (fn it => it COMP accI) |> Thm.implies_intr ihyp |> Thm.forall_intr (Thm.cterm_of ctxt x) |> (fn it => Drule.compose (it, 2, wf_induct_rule)) |> curry op RS (Thm.assume wfR') - |> forall_intr_vars + |> Thm.forall_intr_vars |> (fn it => it COMP allI) |> fold Thm.implies_intr hyps |> Thm.implies_intr wfR' |> Thm.forall_intr (Thm.cterm_of ctxt R') |> Thm.forall_elim (Thm.cterm_of ctxt (inrel_R)) |> curry op RS wf_in_rel |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def]) |> Thm.forall_intr (Thm.cterm_of ctxt Rrel) end (* nominal *) fun prepare_nominal_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = let val NominalFunctionConfig {domintros, default=default_opt, inv=invariant_opt,...} = config val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) val invariant_str = the_default "%x y. True" invariant_opt val fvar = Free (fname, fT) val domT = domain_type fT val ranT = range_type fT val default = Syntax.parse_term lthy default_str |> Type.constraint fT |> Syntax.check_term lthy val invariant_trm = Syntax.parse_term lthy invariant_str |> Type.constraint ([domT, ranT] ---> @{typ bool}) |> Syntax.check_term lthy val (globals, ctxt') = fix_globals domT ranT fvar lthy val Globals { x, h, ... } = globals val clauses = map (mk_clause_context x ctxt') abstract_qglrs val n = length abstract_qglrs fun build_tree (ClauseContext { ctxt, rhs, ...}) = Function_Context_Tree.mk_tree (Free (fname, fT)) h ctxt rhs val trees = map build_tree clauses val RCss = map find_calls trees val ((G, GIntro_thms, G_elim, G_induct), lthy) = PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy val RCss = map (map (inst_RC lthy fvar f)) RCss val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees val ((R, RIntro_thmss, R_elim), lthy) = PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT abstract_qglrs clauses RCss) lthy val (_, lthy) = Local_Theory.abbrev Syntax.mode_default ((Binding.name (defname ^ "_dom"), NoSyn), mk_acc domT R) lthy val newthy = Proof_Context.theory_of lthy val clauses = map (transfer_clause_ctx newthy) clauses val cert = Thm.cterm_of lthy val xclauses = PROFILE "xclauses" (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss val complete = mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume val compat = mk_compat_proof_obligations domT ranT fvar f RCss invariant_trm abstract_qglrs |> map (cert #> Thm.assume) val G_eqvt = mk_eqvt G |> cert |> Thm.assume val invariant = mk_invariant globals G invariant_trm |> cert |> Thm.assume val compat_store = store_compat_thms n compat val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim G_eqvt invariant) f_defthm fun mk_partial_rules newctxt provedgoal = let val ((graph_is_function, complete_thm), graph_is_eqvt) = provedgoal |> Conjunction.elim |>> fst o Conjunction.elim |>> Conjunction.elim |>> apfst (Thm.forall_elim_vars 0) val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt})) val psimps = PROFILE "Proving simplification rules" (mk_psimps newctxt globals R xclauses values f_iff) graph_is_function val simple_pinduct = PROFILE "Proving partial induction rule" (mk_partial_induct_rule newctxt globals R complete_thm) xclauses val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newctxt globals R R_elim) xclauses val dom_intros = if domintros then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses) else NONE in NominalFunctionResult {fs=[f], G=G, R=R, cases=complete_thm, psimps=psimps, simple_pinducts=[simple_pinduct], termination=total_intro, domintros=dom_intros, eqvts=[f_eqvt]} end in ((f, G, GIntro_thms, G_induct, goalstate, mk_partial_rules), lthy) end end diff --git a/thys/Nominal2/nominal_inductive.ML b/thys/Nominal2/nominal_inductive.ML --- a/thys/Nominal2/nominal_inductive.ML +++ b/thys/Nominal2/nominal_inductive.ML @@ -1,445 +1,445 @@ (* Title: nominal_inductive.ML Author: Christian Urban Author: Tjark Weber Infrastructure for proving strong induction theorems for inductive predicates involving nominal datatypes. Code based on an earlier version by Stefan Berghofer. *) signature NOMINAL_INDUCTIVE = sig val prove_strong_inductive: string list -> string list -> term list list -> thm -> thm list -> Proof.context -> Proof.state val prove_strong_inductive_cmd: xstring * (string * string list) list -> Proof.context -> Proof.state end structure Nominal_Inductive : NOMINAL_INDUCTIVE = struct fun mk_cplus p q = Thm.apply (Thm.apply @{cterm "plus :: perm => perm => perm"} p) q fun mk_cminus p = Thm.apply @{cterm "uminus :: perm => perm"} p fun minus_permute_intro_tac ctxt p = resolve_tac ctxt [Thm.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}] fun minus_permute_elim p thm = thm RS (Thm.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) (* fixme: move to nominal_library *) fun real_head_of (@{term Trueprop} $ t) = real_head_of t | real_head_of (Const (@{const_name Pure.imp}, _) $ _ $ t) = real_head_of t | real_head_of (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of (Const (@{const_name HOL.induct_forall}, _) $ Abs (_, _, t)) = real_head_of t | real_head_of t = head_of t fun mk_vc_compat (avoid, avoid_trm) prems concl_args params = if null avoid then [] else let val vc_goal = concl_args |> HOLogic.mk_tuple |> mk_fresh_star avoid_trm |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> fold_rev (Logic.all o Free) params val finite_goal = avoid_trm |> mk_finite |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> fold_rev (Logic.all o Free) params in [vc_goal, finite_goal] end (* fixme: move to nominal_library *) fun map_term prop f trm = if prop trm then f trm else case trm of (t1 $ t2) => map_term prop f t1 $ map_term prop f t2 | Abs (x, T, t) => Abs (x, T, map_term prop f t) | _ => trm fun add_p_c p (c, c_ty) trm = let val (P, args) = strip_comb trm val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty val args' = map (mk_perm p) args in list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |> (fn t => HOLogic.all_const c_ty $ lambda c t ) |> (fn t => HOLogic.all_const @{typ perm} $ lambda p t) end fun induct_forall_const T = Const (@{const_name HOL.induct_forall}, (T --> @{typ bool}) --> @{typ bool}) fun mk_induct_forall (a, T) t = induct_forall_const T $ Abs (a, T, t) fun add_c_prop qnt Ps (c, c_name, c_ty) trm = let fun add t = let val (P, args) = strip_comb t val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty val args' = args |> qnt ? map (incr_boundvars 1) in list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |> qnt ? mk_induct_forall (c_name, c_ty) end in map_term (member (op =) Ps o head_of) add trm end fun prep_prem Ps c_name c_ty (avoid, avoid_trm) (params, prems, concl) = let val prems' = prems |> map (incr_boundvars 1) |> map (add_c_prop true Ps (Bound 0, c_name, c_ty)) val avoid_trm' = avoid_trm |> fold_rev absfree (params @ [(c_name, c_ty)]) |> strip_abs_body |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |> HOLogic.mk_Trueprop val prems'' = if null avoid then prems' else avoid_trm' :: prems' val concl' = concl |> incr_boundvars 1 |> add_c_prop false Ps (Bound 0, c_name, c_ty) in mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' end (* fixme: move to nominal_library *) fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2) | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2) | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2) | same_name _ = false (* fixme: move to nominal_library *) fun map7 _ [] [] [] [] [] [] [] = [] | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) = f x y z u v r s :: map7 f xs ys zs us vs rs ss (* local abbreviations *) local open Nominal_Permeq in (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel} fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig end val all_elims = let fun spec' ct = Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec} in fold (fn ct => fn th => th RS spec' ct) end fun helper_tac flag prm p ctxt = Subgoal.SUBPROOF (fn {context = ctxt', prems, ...} => let val prems' = prems |> map (minus_permute_elim p) |> map (eqvt_srule ctxt') val prm' = (prems' MRS prm) |> flag ? (all_elims [p]) |> flag ? (eqvt_srule ctxt') in asm_full_simp_tac (put_simpset HOL_ss ctxt' addsimps (prm' :: @{thms HOL.induct_forall_def})) 1 end) ctxt fun non_binder_tac prem intr_cvars Ps ctxt = Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} => let val (prms, p, _) = split_last2 (map snd params) val prm_tys = map (fastype_of o Thm.term_of) prms val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms val prem' = prem |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms) |> eqvt_srule ctxt' (* for inductive-premises*) fun tac1 prm = helper_tac true prm p ctxt' (* for non-inductive premises *) fun tac2 prm = EVERY' [ minus_permute_intro_tac ctxt' p, eqvt_stac ctxt', helper_tac false prm p ctxt' ] fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i in EVERY1 [ eqvt_stac ctxt', resolve_tac ctxt' [prem'], RANGE (map (SUBGOAL o select) prems) ] end) ctxt fun fresh_thm ctxt user_thm p c concl_args avoid_trm = let val conj1 = mk_fresh_star (mk_perm (Bound 0) (mk_perm p avoid_trm)) c val conj2 = mk_fresh_star_ty @{typ perm} (mk_supp (HOLogic.mk_tuple (map (mk_perm p) concl_args))) (Bound 0) val fresh_goal = mk_exists ("q", @{typ perm}) (HOLogic.mk_conj (conj1, conj2)) |> HOLogic.mk_Trueprop val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ @{thms fresh_star_Pair fresh_star_permute_iff} val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) in Goal.prove ctxt [] [] fresh_goal (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2} THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o eresolve_tac ctxt @{thms conjE}, simp]))) end val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x" by (simp add: supp_perm_eq)} val fresh_star_plus = @{lemma "fresh_star (permute q (permute p x)) c ==> fresh_star (permute (q + p) x) c" by (simp add: permute_plus)} fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => let val (prms, p, c) = split_last2 (map snd params) val prm_trms = map Thm.term_of prms val prm_tys = map fastype_of prm_trms val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args val user_thm' = map (infer_instantiate ctxt (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ prms)) user_thm |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems))) val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm' val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result (K (EVERY1 [eresolve_tac ctxt @{thms exE}, full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms supp_Pair fresh_star_Un}), REPEAT o eresolve_tac ctxt @{thms conjE}, dresolve_tac ctxt [fresh_star_plus], REPEAT o dresolve_tac ctxt [supp_perm_eq']])) [fthm] ctxt val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms val prem' = prem |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms) |> eqvt_srule ctxt' val fprop' = eqvt_srule ctxt' fprop val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop']) (* for inductive-premises*) fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' (* for non-inductive premises *) fun tac2 prm = EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p), eqvt_stac ctxt', helper_tac false prm (mk_cplus q p) ctxt' ] fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl) (fn {context = ctxt'', ...} => EVERY1 [ CONVERSION (expand_conv_bot ctxt''), eqvt_stac ctxt'', resolve_tac ctxt'' [prem'], RANGE (tac_fresh :: map (SUBGOAL o select) prems) ]) |> singleton (Proof_Context.export ctxt' ctxt) in resolve_tac ctxt [side_thm] 1 end) ctxt fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = let val tac1 = non_binder_tac prem intr_cvars Ps ctxt val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt in EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms allI}, if null avoid then tac1 else tac2 ] end fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args {prems, context = ctxt} = let val cases_tac = map7 (case_tac ctxt Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args in EVERY1 [ DETERM o resolve_tac ctxt [raw_induct], RANGE cases_tac ] end val normalise = @{lemma "(Q \ (\p c. P p c)) \ (\c. Q \ P (0::perm) c)" by simp} fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt = let val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt val (ind_prems, ind_concl) = raw_induct' |> Thm.prop_of |> Logic.strip_horn |>> map strip_full_horn val params = map (fn (x, _, _) => x) ind_prems val param_trms = (map o map) Free params val intr_vars_tys = map (fn t => rev (Term.add_vars (Thm.prop_of t) [])) intrs val intr_vars = (map o map) fst intr_vars_tys val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms val intr_cvars = (map o map) (Thm.cterm_of ctxt o Var) intr_vars_tys val (intr_prems, intr_concls) = intrs |> map Thm.prop_of |> map2 subst_Vars intr_vars_substs |> map Logic.strip_horn |> split_list val intr_concls_args = map (snd o fixed_nonfixed_args ctxt' o HOLogic.dest_Trueprop) intr_concls val avoid_trms = avoids |> (map o map) (setify ctxt') |> map fold_union val vc_compat_goals = map4 mk_vc_compat (avoids ~~ avoid_trms) intr_prems intr_concls_args params val ([c_name, a, p], ctxt'') = Variable.variant_fixes ["c", "'a", "p"] ctxt' val c_ty = TFree (a, @{sort fs}) val c = Free (c_name, c_ty) val p = Free (p, @{typ perm}) val (preconds, ind_concls) = ind_concl |> HOLogic.dest_Trueprop |> HOLogic.dest_conj |> map HOLogic.dest_imp |> split_list val Ps = map (fst o strip_comb) ind_concls val ind_concl' = ind_concls |> map (add_p_c p (c, c_ty)) |> (curry (op ~~)) preconds |> map HOLogic.mk_imp |> fold_conj |> HOLogic.mk_Trueprop val ind_prems' = ind_prems |> map2 (prep_prem Ps c_name c_ty) (avoids ~~ avoid_trms) fun after_qed ctxt_outside user_thms ctxt = let val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |> singleton (Proof_Context.export ctxt ctxt_outside) |> Old_Datatype_Aux.split_conj_thm |> map (fn thm => thm RS normalise) |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms permute_zero induct_rulify})) |> map (Drule.rotate_prems (length ind_prems')) |> map zero_var_indexes val qualified_thm_name = pred_names |> map Long_Name.base_name |> space_implode "_" |> (fn s => Binding.qualify false s (Binding.name "strong_induct")) val attrs = [ Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Rule_Cases.case_names rule_names)) ] in ctxt |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms) |> snd end in Proof.theorem NONE (after_qed ctxt) ((map o map) (rpair []) vc_compat_goals) ctxt'' end fun prove_strong_inductive_cmd (pred_name, avoids) ctxt = let val ({names, ...}, {raw_induct, intrs, ...}) = Inductive.the_inductive_global ctxt (long_name ctxt pred_name) val rule_names = hd names |> the o Induct.lookup_inductP ctxt |> fst o Rule_Cases.get |> map (fst o fst) val case_names = map fst avoids val _ = case duplicates (op =) case_names of [] => () | xs => error ("Duplicate case names: " ^ commas_quote xs) val _ = case subtract (op =) rule_names case_names of [] => () | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs) val avoids_ordered = order_default (op =) [] rule_names avoids fun read_avoids avoid_trms intr = let (* fixme hack *) - val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt - val trms = map (Thm.term_of o snd) ctrms + val (((_, inst), _), ctxt') = Variable.import true [intr] ctxt + val trms = build (inst |> Term_Subst.Vars.fold (cons o Thm.term_of o snd)) val ctxt'' = fold Variable.declare_term trms ctxt' in map (Syntax.read_term ctxt'') avoid_trms end val avoid_trms = map2 read_avoids avoids_ordered intrs in prove_strong_inductive names rule_names avoid_trms raw_induct intrs ctxt end (* outer syntax *) local val single_avoid_parser = Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term) val avoids_parser = Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] val main_parser = Parse.name -- avoids_parser in val _ = Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} "prove strong induction theorem for inductive predicate involving nominal datatypes" (main_parser >> prove_strong_inductive_cmd) end end diff --git a/thys/Nominal2/nominal_library.ML b/thys/Nominal2/nominal_library.ML --- a/thys/Nominal2/nominal_library.ML +++ b/thys/Nominal2/nominal_library.ML @@ -1,516 +1,516 @@ (* Title: nominal_library.ML Author: Christian Urban Library functions for nominal. *) signature NOMINAL_LIBRARY = sig val mk_sort_of: term -> term val atom_ty: typ -> typ val atom_const: typ -> term val mk_atom_ty: typ -> term -> term val mk_atom: term -> term val mk_atom_set_ty: typ -> term -> term val mk_atom_set: term -> term val mk_atom_fset_ty: typ -> term -> term val mk_atom_fset: term -> term val mk_atom_list_ty: typ -> term -> term val mk_atom_list: term -> term val is_atom: Proof.context -> typ -> bool val is_atom_set: Proof.context -> typ -> bool val is_atom_fset: Proof.context -> typ -> bool val is_atom_list: Proof.context -> typ -> bool val to_set_ty: typ -> term -> term val to_set: term -> term val atomify_ty: Proof.context -> typ -> term -> term val atomify: Proof.context -> term -> term val setify_ty: Proof.context -> typ -> term -> term val setify: Proof.context -> term -> term val listify_ty: Proof.context -> typ -> term -> term val listify: Proof.context -> term -> term val fresh_ty: typ -> typ val fresh_const: typ -> term val mk_fresh_ty: typ -> term -> term -> term val mk_fresh: term -> term -> term val fresh_star_ty: typ -> typ val fresh_star_const: typ -> term val mk_fresh_star_ty: typ -> term -> term -> term val mk_fresh_star: term -> term -> term val supp_ty: typ -> typ val supp_const: typ -> term val mk_supp_ty: typ -> term -> term val mk_supp: term -> term val supp_rel_ty: typ -> typ val supp_rel_const: typ -> term val mk_supp_rel_ty: typ -> term -> term -> term val mk_supp_rel: term -> term -> term val supports_const: typ -> term val mk_supports_ty: typ -> term -> term -> term val mk_supports: term -> term -> term val finite_const: typ -> term val mk_finite_ty: typ -> term -> term val mk_finite: term -> term val mk_diff: term * term -> term val mk_append: term * term -> term val mk_union: term * term -> term val fold_union: term list -> term val fold_append: term list -> term val mk_conj: term * term -> term val fold_conj: term list -> term val fold_conj_balanced: term list -> term (* functions for de-Bruijn open terms *) val mk_binop_env: typ list -> string -> term * term -> term val mk_union_env: typ list -> term * term -> term val fold_union_env: typ list -> term list -> term (* fresh arguments for a term *) val fresh_args: Proof.context -> term -> term list (* some logic operations *) val strip_full_horn: term -> (string * typ) list * term list * term val mk_full_horn: (string * typ) list -> term list -> term -> term (* datatype operations *) type cns_info = (term * typ * typ list * bool list) list val all_dtyp_constrs_types: Old_Datatype_Aux.descr -> cns_info list (* tactics for function package *) val size_ss: simpset val pat_completeness_simp: thm list -> Proof.context -> tactic val prove_termination_ind: Proof.context -> int -> tactic val prove_termination_fun: thm list -> Proof.context -> Function.info * local_theory (* transformations of premises in inductions *) val transform_prem1: Proof.context -> string list -> thm -> thm val transform_prem2: Proof.context -> string list -> thm -> thm (* transformation into the object logic *) val atomize: Proof.context -> thm -> thm val atomize_rule: Proof.context -> int -> thm -> thm val atomize_concl: Proof.context -> thm -> thm (* applies a tactic to a formula composed of conjunctions *) val conj_tac: Proof.context -> (int -> tactic) -> int -> tactic end structure Nominal_Library: NOMINAL_LIBRARY = struct fun mk_sort_of t = @{term "sort_of"} $ t; fun atom_ty ty = ty --> @{typ "atom"}; fun atom_const ty = Const (@{const_name "atom"}, atom_ty ty) fun mk_atom_ty ty t = atom_const ty $ t; fun mk_atom t = mk_atom_ty (fastype_of t) t; fun mk_atom_set_ty ty t = let val atom_ty = HOLogic.dest_setT ty val img_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom set"}; in Const (@{const_name image}, img_ty) $ atom_const atom_ty $ t end fun mk_atom_fset_ty ty t = let val atom_ty = dest_fsetT ty val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; in Const (@{const_name fimage}, fmap_ty) $ atom_const atom_ty $ t end fun mk_atom_list_ty ty t = let val atom_ty = dest_listT ty val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"} in Const (@{const_name map}, map_ty) $ atom_const atom_ty $ t end fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t (* coerces a list into a set *) fun to_set_ty ty t = case ty of @{typ "atom list"} => @{term "set :: atom list => atom set"} $ t | @{typ "atom fset"} => @{term "fset :: atom fset => atom set"} $ t | _ => t fun to_set t = to_set_ty (fastype_of t) t (* testing for concrete atom types *) fun is_atom ctxt ty = Sign.of_sort (Proof_Context.theory_of ctxt) (ty, @{sort at_base}) fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty | is_atom_set _ _ = false; fun is_atom_fset ctxt (Type (@{type_name "fset"}, [ty])) = is_atom ctxt ty | is_atom_fset _ _ = false; fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty | is_atom_list _ _ = false (* functions that coerce singletons, sets, fsets and lists of concrete atoms into general atoms sets / lists *) fun atomify_ty ctxt ty t = if is_atom ctxt ty then mk_atom_ty ty t else if is_atom_set ctxt ty then mk_atom_set_ty ty t else if is_atom_fset ctxt ty then mk_atom_fset_ty ty t else if is_atom_list ctxt ty then mk_atom_list_ty ty t else raise TERM ("atomify: term is not an atom, set or list of atoms", [t]) fun setify_ty ctxt ty t = if is_atom ctxt ty then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] else if is_atom_set ctxt ty then mk_atom_set_ty ty t else if is_atom_fset ctxt ty then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t else if is_atom_list ctxt ty then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t else raise TERM ("setify: term is not an atom, set or list of atoms", [t]) fun listify_ty ctxt ty t = if is_atom ctxt ty then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] else if is_atom_list ctxt ty then mk_atom_list_ty ty t else raise TERM ("listify: term is not an atom or list of atoms", [t]) fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t fun setify ctxt t = setify_ty ctxt (fastype_of t) t fun listify ctxt t = listify_ty ctxt (fastype_of t) t fun fresh_ty ty = [@{typ atom}, ty] ---> @{typ bool} fun fresh_const ty = Const (@{const_name fresh}, fresh_ty ty) fun mk_fresh_ty ty t1 t2 = fresh_const ty $ t1 $ t2 fun mk_fresh t1 t2 = mk_fresh_ty (fastype_of t2) t1 t2 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool} fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty) fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2 fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2 fun supp_ty ty = ty --> @{typ "atom set"}; fun supp_const ty = Const (@{const_name supp}, supp_ty ty) fun mk_supp_ty ty t = supp_const ty $ t fun mk_supp t = mk_supp_ty (fastype_of t) t fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"}; fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty) fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool}) fun mk_finite_ty ty t = finite_const ty $ t fun mk_finite t = mk_finite_ty (fastype_of t) t (* functions that construct differences, appends and unions but avoid producing empty atom sets or empty atom lists *) fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} | mk_diff (t1, @{term "{}::atom set"}) = t1 | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"} | mk_diff (t1, @{term "set ([]::atom list)"}) = t1 | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) fun mk_append (t1, @{term "[]::atom list"}) = t1 | mk_append (@{term "[]::atom list"}, t2) = t2 | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) fun mk_union (t1, @{term "{}::atom set"}) = t1 | mk_union (@{term "{}::atom set"}, t2) = t2 | mk_union (t1, @{term "set ([]::atom list)"}) = t1 | mk_union (@{term "set ([]::atom list)"}, t2) = t2 | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"} fun mk_conj (t1, @{term "True"}) = t1 | mk_conj (@{term "True"}, t2) = t2 | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} fun fold_conj_balanced ts = Balanced_Tree.make HOLogic.mk_conj ts (* functions for de-Bruijn open terms *) fun mk_binop_env tys c (t, u) = let val ty = fastype_of1 (tys, t) in Const (c, [ty, ty] ---> ty) $ t $ u end fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} (* produces fresh arguments for a term *) fun fresh_args ctxt f = f |> fastype_of |> binder_types |> map (pair "z") |> Variable.variant_frees ctxt [f] |> map Free (** some logic operations **) (* decompses a formula into params, premises and a conclusion *) fun strip_full_horn trm = let fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) | strip_outer_params B = ([], B) val (params, body) = strip_outer_params trm val (prems, concl) = Logic.strip_horn body in (params, prems, concl) end (* composes a formula out of params, premises and a conclusion *) fun mk_full_horn params prems concl = Logic.list_implies (prems, concl) |> fold_rev mk_all params (** datatypes **) (* constructor infos *) type cns_info = (term * typ * typ list * bool list) list (* - term for constructor constant - type of the constructor - types of the arguments - flags indicating whether the argument is recursive *) (* returns info about constructors in a datatype *) fun all_dtyp_constrs_info descr = map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr (* returns the constants of the constructors plus the corresponding type and types of arguments *) fun all_dtyp_constrs_types descr = let fun aux ((ty_name, vs), (cname, args)) = let val vs_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) vs val ty = Type (ty_name, vs_tys) val arg_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) args val is_rec = map Old_Datatype_Aux.is_rec_type args in (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) end in map (map aux) (all_dtyp_constrs_info descr) end (** function package tactics **) fun pat_completeness_simp simps ctxt = let val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thms sum.inject sum.distinct} @ simps) in Pat_Completeness.pat_completeness_tac ctxt 1 THEN ALLGOALS (asm_full_simp_tac simpset) end (* simpset for size goals *) val size_ss = simpset_of (put_simpset HOL_ss @{context} addsimprocs [@{simproc natless_cancel_numerals}] addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral zero_less_Suc prod.size(1) mult_Suc_right}) val natT = @{typ nat} fun size_prod_const T1 T2 = let val T1_fun = T1 --> natT val T2_fun = T2 --> natT val prodT = HOLogic.mk_prodT (T1, T2) in Const (@{const_name size_prod}, [T1_fun, T2_fun, prodT] ---> natT) end fun snd_const T1 T2 = Const (@{const_name Product_Type.snd}, HOLogic.mk_prodT (T1, T2) --> T2) fun mk_measure_trm f ctxt T = HOLogic.dest_setT T |> fst o HOLogic.dest_prodT |> f |> curry (op $) (Const (@{const_name "measure"}, dummyT)) |> Syntax.check_term ctxt (* wf-goal arising in induction_schema *) fun prove_termination_ind ctxt = let fun mk_size_measure T = case T of (Type (@{type_name Sum_Type.sum}, [T1, T2])) => Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) | (Type (@{type_name Product_Type.prod}, [T1, T2])) => HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2) | _ => HOLogic.size_const T val measure_trm = mk_measure_trm (mk_size_measure) ctxt in Function_Relation.relation_tac ctxt measure_trm end (* wf-goal arising in function definitions *) fun prove_termination_fun size_simps ctxt = let fun mk_size_measure T = case T of (Type (@{type_name Sum_Type.sum}, [T1, T2])) => Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) | (Type (@{type_name Product_Type.prod}, [T1, T2])) => size_prod_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) | _ => HOLogic.size_const T val measure_trm = mk_measure_trm (mk_size_measure) ctxt val tac = Function_Relation.relation_tac ctxt measure_trm THEN_ALL_NEW simp_tac (put_simpset size_ss ctxt addsimps size_simps) in Function.prove_termination NONE (HEADGOAL tac) ctxt end (** transformations of premises (in inductive proofs) **) (* given the theorem F[t]; proves the theorem F[f t] - F needs to be monotone - f returns either SOME for a term it fires on and NONE elsewhere *) fun map_term f t = (case f t of NONE => map_term' f t | x => x) and map_term' f (t $ u) = (case (map_term f t, map_term f u) of (NONE, NONE) => NONE | (SOME t'', NONE) => SOME (t'' $ u) | (NONE, SOME u'') => SOME (t $ u'') | (SOME t'', SOME u'') => SOME (t'' $ u'')) | map_term' f (Abs (s, T, t)) = (case map_term f t of NONE => NONE | SOME t'' => SOME (Abs (s, T, t''))) | map_term' _ _ = NONE; fun map_thm_tac ctxt tac thm = let val monos = Inductive.get_monos ctxt val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} in EVERY [cut_facts_tac [thm] 1, eresolve_tac ctxt [rev_mp] 1, REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)), REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))] end fun map_thm ctxt f tac thm = let val opt_goal_trm = map_term f (Thm.prop_of thm) in case opt_goal_trm of NONE => thm | SOME goal => Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) end (* inductive premises can be of the form R ... /\ P ...; split_conj_i picks out the part R or P part *) fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = (case head_of f1 of Const (name, _) => if member (op =) names name then SOME f1 else NONE | _ => NONE) | split_conj1 _ _ = NONE; fun split_conj2 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = (case head_of f1 of Const (name, _) => if member (op =) names name then SOME f2 else NONE | _ => NONE) | split_conj2 _ _ = NONE; fun transform_prem1 ctxt names thm = map_thm ctxt (split_conj1 names) (eresolve_tac ctxt [conjunct1] 1) thm fun transform_prem2 ctxt names thm = map_thm ctxt (split_conj2 names) (eresolve_tac ctxt [conjunct2] 1) thm (* transforms a theorem into one of the object logic *) -fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; +fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o Thm.forall_intr_vars; fun atomize_rule ctxt i thm = Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm (* applies a tactic to a formula composed of conjunctions *) fun conj_tac ctxt tac i = let fun select (trm, i) = case trm of @{term "Trueprop"} $ t' => select (t', i) | @{term "(&)"} $ _ $ _ => EVERY' [resolve_tac ctxt @{thms conjI}, RANGE [conj_tac ctxt tac, conj_tac ctxt tac]] i | _ => tac i in SUBGOAL select i end end (* structure *) open Nominal_Library; diff --git a/thys/Refine_Imperative_HOL/Sepref_Rules.thy b/thys/Refine_Imperative_HOL/Sepref_Rules.thy --- a/thys/Refine_Imperative_HOL/Sepref_Rules.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Rules.thy @@ -1,1745 +1,1745 @@ section \Refinement Rule Management\ theory Sepref_Rules imports Sepref_Basic Sepref_Constraints begin text \This theory contains tools for managing the refinement rules used by Sepref\ text \The theories are based on uncurried functions, i.e., every function has type @{typ "'a\'b"}, where @{typ 'a} is the tuple of parameters, or unit if there are none. \ subsection \Assertion Interface Binding\ text \Binding of interface types to refinement assertions\ definition intf_of_assn :: "('a \ _ \ assn) \ 'b itself \ bool" where [simp]: "intf_of_assn a b = True" lemma intf_of_assnI: "intf_of_assn R TYPE('a)" by simp named_theorems_rev intf_of_assn \Links between refinement assertions and interface types\ lemma intf_of_assn_fallback: "intf_of_assn (R :: 'a \ _ \ assn) TYPE('a)" by simp subsection \Function Refinement with Precondition\ definition fref :: "('c \ bool) \ ('a \ 'c) set \ ('b \ 'd) set \ (('a \ 'b) \ ('c \ 'd)) set" ("[_]\<^sub>f _ \ _" [0,60,60] 60) where "[P]\<^sub>f R \ S \ {(f,g). \x y. P y \ (x,y)\R \ (f x, g y)\S}" abbreviation freft ("_ \\<^sub>f _" [60,60] 60) where "R \\<^sub>f S \ ([\_. True]\<^sub>f R \ S)" lemma rel2p_fref[rel2p]: "rel2p (fref P R S) = (\f g. (\x y. P y \ rel2p R x y \ rel2p S (f x) (g y)))" by (auto simp: fref_def rel2p_def[abs_def]) lemma fref_cons: assumes "(f,g) \ [P]\<^sub>f R \ S" assumes "\c a. (c,a)\R' \ Q a \ P a" assumes "R' \ R" assumes "S \ S'" shows "(f,g) \ [Q]\<^sub>f R' \ S'" using assms unfolding fref_def by fastforce lemmas fref_cons' = fref_cons[OF _ _ order_refl order_refl] lemma frefI[intro?]: assumes "\x y. \P y; (x,y)\R\ \ (f x, g y)\S" shows "(f,g)\fref P R S" using assms unfolding fref_def by auto lemma fref_ncI: "(f,g)\R\S \ (f,g)\R\\<^sub>fS" apply (rule frefI) apply parametricity done lemma frefD: assumes "(f,g)\fref P R S" shows "\P y; (x,y)\R\ \ (f x, g y)\S" using assms unfolding fref_def by auto lemma fref_ncD: "(f,g)\R\\<^sub>fS \ (f,g)\R\S" apply (rule fun_relI) apply (drule frefD) apply simp apply assumption+ done lemma fref_compI: "fref P R1 R2 O fref Q S1 S2 \ fref (\x. Q x \ (\y. (y,x)\S1 \ P y)) (R1 O S1) (R2 O S2)" unfolding fref_def apply (auto) apply blast done lemma fref_compI': "\ (f,g)\fref P R1 R2; (g,h)\fref Q S1 S2 \ \ (f,h) \ fref (\x. Q x \ (\y. (y,x)\S1 \ P y)) (R1 O S1) (R2 O S2)" using fref_compI[of P R1 R2 Q S1 S2] by auto lemma fref_unit_conv: "(\_. c, \_. a) \ fref P unit_rel S \ (P () \ (c,a)\S)" by (auto simp: fref_def) lemma fref_uncurry_conv: "(uncurry c, uncurry a) \ fref P (R1\\<^sub>rR2) S \ (\x1 y1 x2 y2. P (y1,y2) \ (x1,y1)\R1 \ (x2,y2)\R2 \ (c x1 x2, a y1 y2) \ S)" by (auto simp: fref_def) lemma fref_mono: "\ \x. P' x \ P x; R' \ R; S \ S' \ \ fref P R S \ fref P' R' S'" unfolding fref_def by auto blast lemma fref_composeI: assumes FR1: "(f,g)\fref P R1 R2" assumes FR2: "(g,h)\fref Q S1 S2" assumes C1: "\x. P' x \ Q x" assumes C2: "\x y. \P' x; (y,x)\S1\ \ P y" assumes R1: "R' \ R1 O S1" assumes R2: "R2 O S2 \ S'" assumes FH: "f'=f" "h'=h" shows "(f',h') \ fref P' R' S'" unfolding FH apply (rule subsetD[OF fref_mono fref_compI'[OF FR1 FR2]]) using C1 C2 apply blast using R1 apply blast using R2 apply blast done lemma fref_triv: "A\Id \ (f,f)\[P]\<^sub>f A \ Id" by (auto simp: fref_def) subsection \Heap-Function Refinement\ text \ The following relates a heap-function with a pure function. It contains a precondition, a refinement assertion for the arguments before and after execution, and a refinement relation for the result. \ (* TODO: We only use this with keep/destroy information, so we could model the parameter relations as such (('a\'ai \ assn) \ bool) *) definition hfref :: " ('a \ bool) \ (('a \ 'ai \ assn) \ ('a \ 'ai \ assn)) \ ('b \ 'bi \ assn) \ (('ai \ 'bi Heap) \ ('a\'b nres)) set" ("[_]\<^sub>a _ \ _" [0,60,60] 60) where "[P]\<^sub>a RS \ T \ { (f,g) . \c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)}" abbreviation hfreft ("_ \\<^sub>a _" [60,60] 60) where "RS \\<^sub>a T \ ([\_. True]\<^sub>a RS \ T)" lemma hfrefI[intro?]: assumes "\c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)" shows "(f,g)\hfref P RS T" using assms unfolding hfref_def by blast lemma hfrefD: assumes "(f,g)\hfref P RS T" shows "\c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)" using assms unfolding hfref_def by blast lemma hfref_to_ASSERT_conv: "NO_MATCH (\_. True) P \ (a,b)\[P]\<^sub>a R \ S \ (a,\x. ASSERT (P x) \ b x) \ R \\<^sub>a S" unfolding hfref_def apply (clarsimp; safe; clarsimp?) apply (rule hn_refine_nofailI) apply (simp add: refine_pw_simps) subgoal for xc xa apply (drule spec[of _ xc]) apply (drule spec[of _ xa]) by simp done text \ A pair of argument refinement assertions can be created by the input assertion and the information whether the parameter is kept or destroyed by the function. \ primrec hf_pres :: "('a \ 'b \ assn) \ bool \ ('a \ 'b \ assn)\('a \ 'b \ assn)" where "hf_pres R True = (R,R)" | "hf_pres R False = (R,invalid_assn R)" abbreviation hfkeep :: "('a \ 'b \ assn) \ ('a \ 'b \ assn)\('a \ 'b \ assn)" ("(_\<^sup>k)" [1000] 999) where "R\<^sup>k \ hf_pres R True" abbreviation hfdrop :: "('a \ 'b \ assn) \ ('a \ 'b \ assn)\('a \ 'b \ assn)" ("(_\<^sup>d)" [1000] 999) where "R\<^sup>d \ hf_pres R False" abbreviation "hn_kede R kd \ hn_ctxt (snd (hf_pres R kd))" abbreviation "hn_keep R \ hn_kede R True" abbreviation "hn_dest R \ hn_kede R False" lemma keep_drop_sels[simp]: "fst (R\<^sup>k) = R" "snd (R\<^sup>k) = R" "fst (R\<^sup>d) = R" "snd (R\<^sup>d) = invalid_assn R" by auto lemma hf_pres_fst[simp]: "fst (hf_pres R k) = R" by (cases k) auto text \ The following operator combines multiple argument assertion-pairs to argument assertion-pairs for the product. It is required to state argument assertion-pairs for uncurried functions. \ definition hfprod :: " (('a \ 'b \ assn)\('a \ 'b \ assn)) \ (('c \ 'd \ assn)\('c \ 'd \ assn)) \ ((('a\'c) \ ('b \ 'd) \ assn) \ (('a\'c) \ ('b \ 'd) \ assn))" (infixl "*\<^sub>a" 65) where "RR *\<^sub>a SS \ (prod_assn (fst RR) (fst SS), prod_assn (snd RR) (snd SS))" lemma hfprod_fst_snd[simp]: "fst (A *\<^sub>a B) = prod_assn (fst A) (fst B)" "snd (A *\<^sub>a B) = prod_assn (snd A) (snd B)" unfolding hfprod_def by auto subsubsection \Conversion from fref to hfref\ (* TODO: Variant of import-param! Automate this! *) lemma fref_to_pure_hfref': assumes "(f,g) \ [P]\<^sub>f R\\S\nres_rel" assumes "\x. x\Domain R \ R\``Collect P \ f x = RETURN (f' x)" shows "(return o f', g) \ [P]\<^sub>a (pure R)\<^sup>k\pure S" apply (rule hfrefI) apply (rule hn_refineI) using assms apply ((sep_auto simp: fref_def pure_def pw_le_iff pw_nres_rel_iff refine_pw_simps eintros del: exI)) apply force done subsubsection \Conversion from hfref to hnr\ text \This section contains the lemmas. The ML code is further down. \ lemma hf2hnr: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "\x xi. P x \ hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" using assms unfolding hfref_def by (auto simp: hn_ctxt_def) (*lemma hf2hnr_new: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "\x xi. (\h. h\fst R x xi \ P x) \ hn_refine (emp * hn_ctxt (fst R) x xi) (f xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" using assms unfolding hfref_def by (auto simp: hn_ctxt_def intro: hn_refine_preI) *) (* Products that stem from currying are tagged by a special refinement relation *) definition [simp]: "to_hnr_prod \ prod_assn" lemma to_hnr_prod_fst_snd: "fst (A *\<^sub>a B) = to_hnr_prod (fst A) (fst B)" "snd (A *\<^sub>a B) = to_hnr_prod (snd A) (snd B)" unfolding hfprod_def by auto (* Warning: This lemma is carefully set up to be applicable as an unfold rule, for more than one level of uncurrying*) lemma hnr_uncurry_unfold: " (\x xi. P x \ hn_refine (\ * hn_ctxt (to_hnr_prod A B) x xi) (fi xi) (\' * hn_ctxt (to_hnr_prod A' B') x xi) R (f x)) \ (\b bi a ai. P (a,b) \ hn_refine (\ * hn_ctxt B b bi * hn_ctxt A a ai) (fi (ai,bi)) (\' * hn_ctxt B' b bi * hn_ctxt A' a ai) R (f (a,b)) )" by (auto simp: hn_ctxt_def prod_assn_def star_aci) lemma hnr_intro_dummy: "\x xi. P x \ hn_refine (\ x xi) (c xi) (\' x xi) R (a x) \ \x xi. P x \ hn_refine (emp*\ x xi) (c xi) (emp*\' x xi) R (a x)" by simp lemma hn_ctxt_ctxt_fix_conv: "hn_ctxt (hn_ctxt R) = hn_ctxt R" by (simp add: hn_ctxt_def[abs_def]) lemma uncurry_APP: "uncurry f$(a,b) = f$a$b" by auto (* TODO: Replace by more general rule. *) lemma norm_RETURN_o: "\f. (RETURN o f)$x = (RETURN$(f$x))" "\f. (RETURN oo f)$x$y = (RETURN$(f$x$y))" "\f. (RETURN ooo f)$x$y$z = (RETURN$(f$x$y$z))" "\f. (\x. RETURN ooo f x)$x$y$z$a = (RETURN$(f$x$y$z$a))" "\f. (\x y. RETURN ooo f x y)$x$y$z$a$b = (RETURN$(f$x$y$z$a$b))" by auto lemma norm_return_o: "\f. (return o f)$x = (return$(f$x))" "\f. (return oo f)$x$y = (return$(f$x$y))" "\f. (return ooo f)$x$y$z = (return$(f$x$y$z))" "\f. (\x. return ooo f x)$x$y$z$a = (return$(f$x$y$z$a))" "\f. (\x y. return ooo f x y)$x$y$z$a$b = (return$(f$x$y$z$a$b))" by auto lemma hn_val_unit_conv_emp[simp]: "hn_val unit_rel x y = emp" by (auto simp: hn_ctxt_def pure_def) subsubsection \Conversion from hnr to hfref\ text \This section contains the lemmas. The ML code is further down. \ abbreviation "id_assn \ pure Id" abbreviation "unit_assn \ id_assn :: unit \ _" lemma pure_unit_rel_eq_empty: "unit_assn x y = emp" by (auto simp: pure_def) lemma uc_hfprod_sel: "fst (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \ fst A a1 c1 * fst B a2 c2)" "snd (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \ snd A a1 c1 * snd B a2 c2)" unfolding hfprod_def prod_assn_def[abs_def] by auto subsubsection \Conversion from relation to fref\ text \This section contains the lemmas. The ML code is further down. \ definition "CURRY R \ { (f,g). (uncurry f, uncurry g) \ R }" lemma fref_param1: "R\S = fref (\_. True) R S" by (auto simp: fref_def fun_relD) lemma fref_nest: "fref P1 R1 (fref P2 R2 S) \ CURRY (fref (\(a,b). P1 a \ P2 b) (R1\\<^sub>rR2) S)" apply (rule eq_reflection) by (auto simp: fref_def CURRY_def) lemma in_CURRY_conv: "(f,g) \ CURRY R \ (uncurry f, uncurry g) \ R" unfolding CURRY_def by auto lemma uncurry0_APP[simp]: "uncurry0 c $ x = c" by auto lemma fref_param0I: "(c,a)\R \ (uncurry0 c, uncurry0 a) \ fref (\_. True) unit_rel R" by (auto simp: fref_def) subsubsection \Composition\ definition hr_comp :: "('b \ 'c \ assn) \ ('b \ 'a) set \ 'a \ 'c \ assn" \ \Compose refinement assertion with refinement relation\ where "hr_comp R1 R2 a c \ \\<^sub>Ab. R1 b c * \((b,a)\R2)" definition hrp_comp :: "('d \ 'b \ assn) \ ('d \ 'c \ assn) \ ('d \ 'a) set \ ('a \ 'b \ assn) \ ('a \ 'c \ assn)" \ \Compose argument assertion-pair with refinement relation\ where "hrp_comp RR' S \ (hr_comp (fst RR') S, hr_comp (snd RR') S) " lemma hr_compI: "(b,a)\R2 \ R1 b c \\<^sub>A hr_comp R1 R2 a c" unfolding hr_comp_def by sep_auto lemma hr_comp_Id1[simp]: "hr_comp (pure Id) R = pure R" unfolding hr_comp_def[abs_def] pure_def apply (intro ext ent_iffI) by sep_auto+ lemma hr_comp_Id2[simp]: "hr_comp R Id = R" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) by sep_auto+ (*lemma hr_comp_invalid[simp]: "hr_comp (\a c. true) R a c = true * \(\b. (b,a)\R)" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) apply sep_auto+ done*) lemma hr_comp_emp[simp]: "hr_comp (\a c. emp) R a c = \(\b. (b,a)\R)" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) apply sep_auto+ done lemma hr_comp_prod_conv[simp]: "hr_comp (prod_assn Ra Rb) (Ra' \\<^sub>r Rb') = prod_assn (hr_comp Ra Ra') (hr_comp Rb Rb')" unfolding hr_comp_def[abs_def] prod_assn_def[abs_def] apply (intro ext ent_iffI) apply solve_entails apply clarsimp apply sep_auto apply clarsimp apply (intro ent_ex_preI) apply (rule ent_ex_postI) apply (sep_auto split: prod.splits) done lemma hr_comp_pure: "hr_comp (pure R) S = pure (R O S)" apply (intro ext) apply (rule ent_iffI) unfolding hr_comp_def[abs_def] apply (sep_auto simp: pure_def)+ done lemma hr_comp_is_pure[safe_constraint_rules]: "is_pure A \ is_pure (hr_comp A B)" by (auto simp: hr_comp_pure is_pure_conv) lemma hr_comp_the_pure: "is_pure A \ the_pure (hr_comp A B) = the_pure A O B" unfolding is_pure_conv by (clarsimp simp: hr_comp_pure) lemma rdomp_hrcomp_conv: "rdomp (hr_comp A R) x \ (\y. rdomp A y \ (y,x)\R)" by (auto simp: rdomp_def hr_comp_def) lemma hn_rel_compI: "\nofail a; (b,a)\\R2\nres_rel\ \ hn_rel R1 b c \\<^sub>A hn_rel (hr_comp R1 R2) a c" unfolding hr_comp_def hn_rel_def nres_rel_def apply (clarsimp intro!: ent_ex_preI) apply (drule (1) order_trans) apply (simp add: ret_le_down_conv) by sep_auto lemma hr_comp_precise[constraint_rules]: assumes [safe_constraint_rules]: "precise R" assumes SV: "single_valued S" shows "precise (hr_comp R S)" apply (rule preciseI) unfolding hr_comp_def apply clarsimp by (metis SV assms(1) preciseD single_valuedD) lemma hr_comp_assoc: "hr_comp (hr_comp R S) T = hr_comp R (S O T)" apply (intro ext) unfolding hr_comp_def apply (rule ent_iffI; clarsimp) apply sep_auto apply (rule ent_ex_preI; clarsimp) (* TODO: sep_auto/solve_entails is too eager splitting the subgoal here! *) apply sep_auto done lemma hnr_comp: assumes R: "\b1 c1. P b1 \ hn_refine (R1 b1 c1 * \) (c c1) (R1p b1 c1 * \') R (b b1)" assumes S: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ (b b1,a a1)\\R'\nres_rel" assumes PQ: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ P b1" assumes Q: "Q a1" shows "hn_refine (hr_comp R1 R1' a1 c1 * \) (c c1) (hr_comp R1p R1' a1 c1 * \') (hr_comp R R') (a a1)" unfolding hn_refine_alt proof clarsimp assume NF: "nofail (a a1)" show " > c c1 <\r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \')>\<^sub>t" apply (subst hr_comp_def) apply (clarsimp intro!: norm_pre_ex_rule) proof - fix b1 assume R1: "(b1, a1) \ R1'" from S R1 Q have R': "(b b1, a a1) \ \R'\nres_rel" by blast with NF have NFB: "nofail (b b1)" by (simp add: nres_rel_def pw_le_iff refine_pw_simps) from PQ R1 Q have P: "P b1" by blast with NFB R have "> c c1 <\r. hn_rel R (b b1) r * (R1p b1 c1 * \')>\<^sub>t" unfolding hn_refine_alt by auto thus "> c c1 <\r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \')>\<^sub>t" apply (rule cons_post_rule) apply (solve_entails) by (intro ent_star_mono hn_rel_compI[OF NF R'] hr_compI[OF R1] ent_refl) qed qed lemma hnr_comp1_aux: assumes R: "\b1 c1. P b1 \ hn_refine (hn_ctxt R1 b1 c1) (c c1) (hn_ctxt R1p b1 c1) R (b$b1)" assumes S: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ (b$b1,a$a1)\\R'\nres_rel" assumes PQ: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ P b1" assumes Q: "Q a1" shows "hn_refine (hr_comp R1 R1' a1 c1) (c c1) (hr_comp R1p R1' a1 c1) (hr_comp R R') (a a1)" using assms hnr_comp[where \=emp and \'=emp and a=a and b=b and c=c and P=P and Q=Q] unfolding hn_ctxt_def by auto lemma hfcomp: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [\a. Q a \ (\a'. (a',a)\T \ P a')]\<^sub>a hrp_comp RR' T \ hr_comp S U" using assms unfolding fref_def hfref_def hrp_comp_def apply clarsimp apply (rule hnr_comp1_aux[of P "fst RR'" f "snd RR'" S g "\a. Q a \ (\a'. (a',a)\T \ P a')" T h U]) apply (auto simp: hn_ctxt_def) done lemma hfref_weaken_pre_nofail: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "(f,g) \ [\x. nofail (g x) \ P x]\<^sub>a R \ S" using assms unfolding hfref_def hn_refine_def by auto lemma hfref_cons: assumes "(f,g) \ [P]\<^sub>a R \ S" assumes "\x. P' x \ P x" assumes "\x y. fst R' x y \\<^sub>t fst R x y" assumes "\x y. snd R x y \\<^sub>t snd R' x y" assumes "\x y. S x y \\<^sub>t S' x y" shows "(f,g) \ [P']\<^sub>a R' \ S'" unfolding hfref_def apply clarsimp apply (rule hn_refine_cons) apply (rule assms(3)) defer apply (rule entt_trans[OF assms(4)]; sep_auto) apply (rule assms(5)) apply (frule assms(2)) using assms(1) unfolding hfref_def apply auto done subsubsection \Composition Automation\ text \This section contains the lemmas. The ML code is further down. \ lemma prod_hrp_comp: "hrp_comp (A *\<^sub>a B) (C \\<^sub>r D) = hrp_comp A C *\<^sub>a hrp_comp B D" unfolding hrp_comp_def hfprod_def by simp lemma hrp_comp_keep: "hrp_comp (A\<^sup>k) B = (hr_comp A B)\<^sup>k" by (auto simp: hrp_comp_def) lemma hr_comp_invalid: "hr_comp (invalid_assn R1) R2 = invalid_assn (hr_comp R1 R2)" apply (intro ent_iffI entailsI ext) unfolding invalid_assn_def hr_comp_def by auto lemma hrp_comp_dest: "hrp_comp (A\<^sup>d) B = (hr_comp A B)\<^sup>d" by (auto simp: hrp_comp_def hr_comp_invalid) definition "hrp_imp RR RR' \ \a b. (fst RR' a b \\<^sub>t fst RR a b) \ (snd RR a b \\<^sub>t snd RR' a b)" lemma hfref_imp: "hrp_imp RR RR' \ [P]\<^sub>a RR \ S \ [P]\<^sub>a RR' \ S" apply clarsimp apply (erule hfref_cons) apply (simp_all add: hrp_imp_def) done lemma hrp_imp_refl: "hrp_imp RR RR" unfolding hrp_imp_def by auto lemma hrp_imp_reflI: "RR = RR' \ hrp_imp RR RR'" unfolding hrp_imp_def by auto lemma hrp_comp_cong: "hrp_imp A A' \ B=B' \ hrp_imp (hrp_comp A B) (hrp_comp A' B')" by (sep_auto simp: hrp_imp_def hrp_comp_def hr_comp_def entailst_def) lemma hrp_prod_cong: "hrp_imp A A' \ hrp_imp B B' \ hrp_imp (A*\<^sub>aB) (A'*\<^sub>aB')" by (sep_auto simp: hrp_imp_def prod_assn_def intro: entt_star_mono) lemma hrp_imp_trans: "hrp_imp A B \ hrp_imp B C \ hrp_imp A C" unfolding hrp_imp_def by (fastforce intro: entt_trans) lemma fcomp_norm_dflt_init: "x\[P]\<^sub>a R \ T \ hrp_imp R S \ x\[P]\<^sub>a S \ T" apply (erule rev_subsetD) by (rule hfref_imp) definition "comp_PRE R P Q S \ \x. S x \ (P x \ (\y. (y,x)\R \ Q x y))" lemma comp_PRE_cong[cong]: assumes "R\R'" assumes "\x. P x \ P' x" assumes "\x. S x \ S' x" assumes "\x y. \P x; (y,x)\R; y\Domain R; S' x \ \ Q x y \ Q' x y" shows "comp_PRE R P Q S \ comp_PRE R' P' Q' S'" using assms by (fastforce simp: comp_PRE_def intro!: eq_reflection ext) lemma fref_compI_PRE: "\ (f,g)\fref P R1 R2; (g,h)\fref Q S1 S2 \ \ (f,h) \ fref (comp_PRE S1 Q (\_. P) (\_. True)) (R1 O S1) (R2 O S2)" using fref_compI[of P R1 R2 Q S1 S2] unfolding comp_PRE_def by auto lemma PRE_D1: "(Q x \ P x) \ comp_PRE S1 Q (\x _. P x) S x" by (auto simp: comp_PRE_def) lemma PRE_D2: "(Q x \ (\y. (y,x)\S1 \ S x \ P x y)) \ comp_PRE S1 Q P S x" by (auto simp: comp_PRE_def) lemma fref_weaken_pre: assumes "\x. P x \ P' x" assumes "(f,h) \ fref P' R S" shows "(f,h) \ fref P R S" apply (rule rev_subsetD[OF assms(2) fref_mono]) using assms(1) by auto lemma fref_PRE_D1: assumes "(f,h) \ fref (comp_PRE S1 Q (\x _. P x) X) R S" shows "(f,h) \ fref (\x. Q x \ P x) R S" by (rule fref_weaken_pre[OF PRE_D1 assms]) lemma fref_PRE_D2: assumes "(f,h) \ fref (comp_PRE S1 Q P X) R S" shows "(f,h) \ fref (\x. Q x \ (\y. (y,x)\S1 \ X x \ P x y)) R S" by (rule fref_weaken_pre[OF PRE_D2 assms]) lemmas fref_PRE_D = fref_PRE_D1 fref_PRE_D2 lemma hfref_weaken_pre: assumes "\x. P x \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" using assms by (auto simp: hfref_def) lemma hfref_weaken_pre': assumes "\x. \P x; rdomp (fst R) x\ \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" apply (rule hfrefI) apply (rule hn_refine_preI) using assms by (auto simp: hfref_def rdomp_def) lemma hfref_weaken_pre_nofail': assumes "(f,g) \ [P]\<^sub>a R \ S" assumes "\x. \nofail (g x); Q x\ \ P x" shows "(f,g) \ [Q]\<^sub>a R \ S" apply (rule hfref_weaken_pre[OF _ assms(1)[THEN hfref_weaken_pre_nofail]]) using assms(2) by blast lemma hfref_compI_PRE_aux: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [comp_PRE T Q (\_. P) (\_. True)]\<^sub>a hrp_comp RR' T \ hr_comp S U" apply (rule hfref_weaken_pre[OF _ hfcomp[OF A B]]) by (auto simp: comp_PRE_def) lemma hfref_compI_PRE: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [comp_PRE T Q (\x y. P y) (\x. nofail (h x))]\<^sub>a hrp_comp RR' T \ hr_comp S U" using hfref_compI_PRE_aux[OF A B, THEN hfref_weaken_pre_nofail] apply (rule hfref_weaken_pre[rotated]) apply (auto simp: comp_PRE_def) done lemma hfref_PRE_D1: assumes "(f,h) \ hfref (comp_PRE S1 Q (\x _. P x) X) R S" shows "(f,h) \ hfref (\x. Q x \ P x) R S" by (rule hfref_weaken_pre[OF PRE_D1 assms]) lemma hfref_PRE_D2: assumes "(f,h) \ hfref (comp_PRE S1 Q P X) R S" shows "(f,h) \ hfref (\x. Q x \ (\y. (y,x)\S1 \ X x \ P x y)) R S" by (rule hfref_weaken_pre[OF PRE_D2 assms]) lemma hfref_PRE_D3: assumes "(f,h) \ hfref (comp_PRE S1 Q P X) R S" shows "(f,h) \ hfref (comp_PRE S1 Q P X) R S" using assms . lemmas hfref_PRE_D = hfref_PRE_D1 hfref_PRE_D3 subsection \Automation\ text \Purity configuration for constraint solver\ lemmas [safe_constraint_rules] = pure_pure text \Configuration for hfref to hnr conversion\ named_theorems to_hnr_post \to_hnr converter: Postprocessing unfold rules\ lemma uncurry0_add_app_tag: "uncurry0 (RETURN c) = uncurry0 (RETURN$c)" by simp lemmas [to_hnr_post] = norm_RETURN_o norm_return_o uncurry0_add_app_tag uncurry0_apply uncurry0_APP hn_val_unit_conv_emp mult_1[of "x::assn" for x] mult_1_right[of "x::assn" for x] named_theorems to_hfref_post \to_hfref converter: Postprocessing unfold rules\ lemma prod_casesK[to_hfref_post]: "case_prod (\_ _. k) = (\_. k)" by auto lemma uncurry0_hfref_post[to_hfref_post]: "hfref (uncurry0 True) R S = hfref (\_. True) R S" apply (fo_rule arg_cong fun_cong)+ by auto (* Currently not used, we keep it in here anyway. *) text \Configuration for relation normalization after composition\ named_theorems fcomp_norm_unfold \fcomp-normalizer: Unfold theorems\ named_theorems fcomp_norm_simps \fcomp-normalizer: Simplification theorems\ named_theorems fcomp_norm_init "fcomp-normalizer: Initialization rules" named_theorems fcomp_norm_trans "fcomp-normalizer: Transitivity rules" named_theorems fcomp_norm_cong "fcomp-normalizer: Congruence rules" named_theorems fcomp_norm_norm "fcomp-normalizer: Normalization rules" named_theorems fcomp_norm_refl "fcomp-normalizer: Reflexivity rules" text \Default Setup\ lemmas [fcomp_norm_unfold] = prod_rel_comp nres_rel_comp Id_O_R R_O_Id lemmas [fcomp_norm_unfold] = hr_comp_Id1 hr_comp_Id2 lemmas [fcomp_norm_unfold] = hr_comp_prod_conv lemmas [fcomp_norm_unfold] = prod_hrp_comp hrp_comp_keep hrp_comp_dest hr_comp_pure (*lemmas [fcomp_norm_unfold] = prod_casesK uncurry0_hfref_post*) lemma [fcomp_norm_simps]: "CONSTRAINT is_pure P \ pure (the_pure P) = P" by simp lemmas [fcomp_norm_simps] = True_implies_equals lemmas [fcomp_norm_init] = fcomp_norm_dflt_init lemmas [fcomp_norm_trans] = hrp_imp_trans lemmas [fcomp_norm_cong] = hrp_comp_cong hrp_prod_cong (*lemmas [fcomp_norm_norm] = hrp_comp_dest*) lemmas [fcomp_norm_refl] = refl hrp_imp_refl lemma ensure_fref_nresI: "(f,g)\[P]\<^sub>f R\S \ (RETURN o f, RETURN o g)\[P]\<^sub>f R\\S\nres_rel" by (auto intro: nres_relI simp: fref_def) lemma ensure_fref_nres_unfold: "\f. RETURN o (uncurry0 f) = uncurry0 (RETURN f)" "\f. RETURN o (uncurry f) = uncurry (RETURN oo f)" "\f. (RETURN ooo uncurry) f = uncurry (RETURN ooo f)" by auto text \Composed precondition normalizer\ named_theorems fcomp_prenorm_simps \fcomp precondition-normalizer: Simplification theorems\ text \Support for preconditions of the form \_\Domain R\, where \R\ is the relation of the next more abstract level.\ declare DomainI[fcomp_prenorm_simps] lemma auto_weaken_pre_init_hf: assumes "\x. PROTECT P x \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" using assms by (auto simp: hfref_def) lemma auto_weaken_pre_init_f: assumes "\x. PROTECT P x \ P' x" assumes "(f,h) \ fref P' R S" shows "(f,h) \ fref P R S" using assms by (auto simp: fref_def) lemmas auto_weaken_pre_init = auto_weaken_pre_init_hf auto_weaken_pre_init_f lemma auto_weaken_pre_uncurry_step: assumes "PROTECT f a \ f'" shows "PROTECT (\(x,y). f x y) (a,b) \ f' b" using assms by (auto simp: curry_def dest!: meta_eq_to_obj_eq intro!: eq_reflection) lemma auto_weaken_pre_uncurry_finish: "PROTECT f x \ f x" by (auto) lemma auto_weaken_pre_uncurry_start: assumes "P \ P'" assumes "P'\Q" shows "P\Q" using assms by (auto) lemma auto_weaken_pre_comp_PRE_I: assumes "S x \ P x" assumes "\y. \(y,x)\R; P x; S x\ \ Q x y" shows "comp_PRE R P Q S x" using assms by (auto simp: comp_PRE_def) lemma auto_weaken_pre_to_imp_nf: "(A\B\C) = (A\B \ C)" "((A\B)\C) = (A\B\C)" by auto lemma auto_weaken_pre_add_dummy_imp: "P \ True \ P" by simp text \Synthesis for hfref statements\ definition hfsynth_ID_R :: "('a \ _ \ assn) \ 'a \ bool" where [simp]: "hfsynth_ID_R _ _ \ True" lemma hfsynth_ID_R_D: fixes I :: "'a itself" assumes "hfsynth_ID_R R a" assumes "intf_of_assn R I" shows "a ::\<^sub>i I" by simp lemma hfsynth_hnr_from_hfI: assumes "\x xi. P x \ hfsynth_ID_R (fst R) x \ hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" shows "(f,g) \ [P]\<^sub>a R \ S" using assms unfolding hfref_def by (auto simp: hn_ctxt_def) lemma hfsynth_ID_R_uncurry_unfold: "hfsynth_ID_R (to_hnr_prod R S) (a,b) \ hfsynth_ID_R R a \ hfsynth_ID_R S b" "hfsynth_ID_R (fst (hf_pres R k)) \ hfsynth_ID_R R" by (auto intro!: eq_reflection) ML \ signature SEPREF_RULES = sig (* Analysis of relations, both fref and fun_rel *) (* "R1\...\Rn\_" / "[_]\<^sub>f ((R1\\<^sub>rR2)...\\<^sub>rRn)" \ "[R1,...,Rn]" *) val binder_rels: term -> term list (* "_\...\_\S" / "[_]\<^sub>f _ \ S" \ "S" *) val body_rel: term -> term (* Map \/fref to (precond,args,res). NONE if no/trivial precond. *) val analyze_rel: term -> term option * term list * term (* Make trivial ("\_. True") precond *) val mk_triv_precond: term list -> term (* Make "[P]\<^sub>f ((R1\\<^sub>rR2)...\\<^sub>rRn) \ S". Insert trivial precond if NONE. *) val mk_rel: term option * term list * term -> term (* Map relation to (args,res) *) val strip_rel: term -> term list * term (* Make hfprod (op *\<^sub>a) *) val mk_hfprod : term * term -> term val mk_hfprods : term list -> term (* Determine interface type of refinement assertion, using default fallback if necessary. Use named_thms intf_of_assn for configuration. *) val intf_of_assn : Proof.context -> term -> typ (* Convert a parametricity theorem in higher-order form to uncurried fref-form. For functions without arguments, a unit-argument is added. TODO/FIXME: Currently this only works for higher-order theorems, i.e., theorems of the form (f,g)\R1\\\Rn. First-order theorems are silently treated as refinement theorems for functions with zero arguments, i.e., a unit-argument is added. *) val to_fref : Proof.context -> thm -> thm (* Convert a parametricity or fref theorem to first order form *) val to_foparam : Proof.context -> thm -> thm (* Convert schematic hfref goal to hnr-goal *) val prepare_hfref_synth_tac : Proof.context -> tactic' (* Convert theorem in hfref-form to hnr-form *) val to_hnr : Proof.context -> thm -> thm (* Convert theorem in hnr-form to hfref-form *) val to_hfref: Proof.context -> thm -> thm (* Convert theorem to given form, if not yet in this form *) val ensure_fref : Proof.context -> thm -> thm val ensure_fref_nres : Proof.context -> thm -> thm val ensure_hfref : Proof.context -> thm -> thm val ensure_hnr : Proof.context -> thm -> thm type hnr_analysis = { thm: thm, (* Original theorem, may be normalized *) precond: term, (* Precondition, abstracted over abs-arguments *) prems : term list, (* Premises not depending on arguments *) ahead: term * bool, (* Abstract function, has leading RETURN *) chead: term * bool, (* Concrete function, has leading return *) argrels: (term * bool) list, (* Argument relations, preserved (keep-flag) *) result_rel: term (* Result relation *) } val analyze_hnr: Proof.context -> thm -> hnr_analysis val pretty_hnr_analysis: Proof.context -> hnr_analysis -> Pretty.T val mk_hfref_thm: Proof.context -> hnr_analysis -> thm (* Simplify precondition of fref/hfref-theorem *) val simplify_precond: Proof.context -> thm -> thm (* Normalize hfref-theorem after composition *) val norm_fcomp_rule: Proof.context -> thm -> thm (* Replace "pure ?A" by "?A'" and is_pure constraint, then normalize *) val add_pure_constraints_rule: Proof.context -> thm -> thm (* Compose fref/hfref and fref theorem, to produce hfref theorem. The input theorems may also be in ho-param or hnr form, and are converted accordingly. *) val gen_compose : Proof.context -> thm -> thm -> thm (* FCOMP-attribute *) val fcomp_attrib: attribute context_parser end structure Sepref_Rules: SEPREF_RULES = struct local open Refine_Util Relators in fun binder_rels @{mpat "?F \ ?G"} = F::binder_rels G | binder_rels @{mpat "fref _ ?F _"} = strip_prodrel_left F | binder_rels _ = [] local fun br_aux @{mpat "_ \ ?G"} = br_aux G | br_aux R = R in fun body_rel @{mpat "fref _ _ ?G"} = G | body_rel R = br_aux R end fun strip_rel R = (binder_rels R, body_rel R) fun analyze_rel @{mpat "fref (\_. True) ?R ?S"} = (NONE,strip_prodrel_left R,S) | analyze_rel @{mpat "fref ?P ?R ?S"} = (SOME P,strip_prodrel_left R,S) | analyze_rel R = let val (args,res) = strip_rel R in (NONE,args,res) end fun mk_triv_precond Rs = absdummy (map rel_absT Rs |> list_prodT_left) @{term True} fun mk_rel (P,Rs,S) = let val R = list_prodrel_left Rs val P = case P of SOME P => P | NONE => mk_triv_precond Rs in @{mk_term "fref ?P ?R ?S"} end end fun mk_hfprod (a, b) = @{mk_term "?a*\<^sub>a?b"} local fun mk_hfprods_rev [] = @{mk_term "unit_assn\<^sup>k"} | mk_hfprods_rev [Rk] = Rk | mk_hfprods_rev (Rkn::Rks) = mk_hfprod (mk_hfprods_rev Rks, Rkn) in val mk_hfprods = mk_hfprods_rev o rev end fun intf_of_assn ctxt t = let val orig_ctxt = ctxt val (t,ctxt) = yield_singleton (Variable.import_terms false) t ctxt val v = TVar (("T",0),Proof_Context.default_sort ctxt ("T",0)) |> Logic.mk_type val goal = @{mk_term "Trueprop (intf_of_assn ?t ?v)"} val i_of_assn_rls = Named_Theorems_Rev.get ctxt @{named_theorems_rev intf_of_assn} @ @{thms intf_of_assn_fallback} fun tac ctxt = REPEAT_ALL_NEW (resolve_tac ctxt i_of_assn_rls) val thm = Goal.prove ctxt [] [] goal (fn {context,...} => ALLGOALS (tac context)) val intf = case Thm.concl_of thm of @{mpat "Trueprop (intf_of_assn _ (?v AS\<^sub>p TYPE (_)))"} => v | _ => raise THM("Intf_of_assn: Proved a different theorem?",~1,[thm]) val intf = singleton (Variable.export_terms ctxt orig_ctxt) intf |> Logic.dest_type in intf end datatype rthm_type = RT_HOPARAM (* (_,_) \ _ \ \ \ _ *) | RT_FREF (* (_,_) \ [_]\<^sub>f _ \ _ *) | RT_HNR (* hn_refine _ _ _ _ _ *) | RT_HFREF (* (_,_) \ [_]\<^sub>a _ \ _ *) | RT_OTHER fun rthm_type thm = case Thm.concl_of thm |> HOLogic.dest_Trueprop of @{mpat "(_,_) \ fref _ _ _"} => RT_FREF | @{mpat "(_,_) \ hfref _ _ _"} => RT_HFREF | @{mpat "hn_refine _ _ _ _ _"} => RT_HNR | @{mpat "(_,_) \ _"} => RT_HOPARAM (* TODO: Distinction between ho-param and fo-param *) | _ => RT_OTHER fun to_fref ctxt thm = let open Conv in case Thm.concl_of thm |> HOLogic.dest_Trueprop of @{mpat "(_,_)\_\_"} => Local_Defs.unfold0 ctxt @{thms fref_param1} thm |> fconv_rule (repeat_conv (Refine_Util.ftop_conv (K (rewr_conv @{thm fref_nest})) ctxt)) |> Local_Defs.unfold0 ctxt @{thms in_CURRY_conv} | @{mpat "(_,_)\_"} => thm RS @{thm fref_param0I} | _ => raise THM ("to_fref: Expected theorem of form (_,_)\_",~1,[thm]) end fun to_foparam ctxt thm = let val unf_thms = @{thms split_tupled_all prod_rel_simp uncurry_apply cnv_conj_to_meta Product_Type.split} in case Thm.concl_of thm of @{mpat "Trueprop ((_,_) \ fref _ _ _)"} => (@{thm frefD} OF [thm]) - |> forall_intr_vars + |> Thm.forall_intr_vars |> Local_Defs.unfold0 ctxt unf_thms |> Variable.gen_all ctxt | @{mpat "Trueprop ((_,_) \ _)"} => Parametricity.fo_rule thm | _ => raise THM("Expected parametricity or fref theorem",~1,[thm]) end fun to_hnr ctxt thm = (thm RS @{thm hf2hnr}) |> Local_Defs.unfold0 ctxt @{thms to_hnr_prod_fst_snd keep_drop_sels} (* Resolve fst and snd over *\<^sub>a and R\<^sup>k, R\<^sup>d *) |> Local_Defs.unfold0 ctxt @{thms hnr_uncurry_unfold} (* Resolve products for uncurried parameters *) |> Local_Defs.unfold0 ctxt @{thms uncurry_apply uncurry_APP assn_one_left split} (* Remove the uncurry modifiers, the emp-dummy, and unfold product cases *) |> Local_Defs.unfold0 ctxt @{thms hn_ctxt_ctxt_fix_conv} (* Remove duplicate hn_ctxt tagging *) |> Local_Defs.unfold0 ctxt @{thms all_to_meta imp_to_meta HOL.True_implies_equals HOL.implies_True_equals Pure.triv_forall_equality cnv_conj_to_meta} (* Convert to meta-level, remove vacuous condition *) |> Local_Defs.unfold0 ctxt (Named_Theorems.get ctxt @{named_theorems to_hnr_post}) (* Post-Processing *) |> Goal.norm_result ctxt |> Conv.fconv_rule Thm.eta_conversion (* Convert schematic hfref-goal to hn_refine goal *) fun prepare_hfref_synth_tac ctxt = let val i_of_assn_rls = Named_Theorems_Rev.get ctxt @{named_theorems_rev intf_of_assn} @ @{thms intf_of_assn_fallback} val to_hnr_post_rls = Named_Theorems.get ctxt @{named_theorems to_hnr_post} val i_of_assn_tac = ( REPEAT' ( DETERM o dresolve_tac ctxt @{thms hfsynth_ID_R_D} THEN' DETERM o SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt i_of_assn_rls)) ) ) in (* Note: To re-use the to_hnr infrastructure, we first work with $-tags on the abstract function, which are finally removed. *) resolve_tac ctxt @{thms hfsynth_hnr_from_hfI} THEN_ELSE' ( SELECT_GOAL ( unfold_tac ctxt @{thms to_hnr_prod_fst_snd keep_drop_sels hf_pres_fst} (* Distribute fst,snd over product and hf_pres *) THEN unfold_tac ctxt @{thms hnr_uncurry_unfold hfsynth_ID_R_uncurry_unfold} (* Curry parameters *) THEN unfold_tac ctxt @{thms uncurry_apply uncurry_APP assn_one_left split} (* Curry parameters (II) and remove emp assertion *) (*THEN unfold_tac ctxt @{thms hn_ctxt_ctxt_fix_conv} (* Remove duplicate hn_ctxt (Should not be necessary) *)*) THEN unfold_tac ctxt @{thms all_to_meta imp_to_meta HOL.True_implies_equals HOL.implies_True_equals Pure.triv_forall_equality cnv_conj_to_meta} (* Convert precondition to meta-level *) THEN ALLGOALS i_of_assn_tac (* Generate _::\<^sub>i_ premises*) THEN unfold_tac ctxt to_hnr_post_rls (* Postprocessing *) THEN unfold_tac ctxt @{thms APP_def} (* Get rid of $ - tags *) ) , K all_tac ) end (************************************) (* Analyze hnr *) structure Termtab2 = Table( type key = term * term val ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord); type hnr_analysis = { thm: thm, precond: term, prems : term list, ahead: term * bool, chead: term * bool, argrels: (term * bool) list, result_rel: term } fun analyze_hnr (ctxt:Proof.context) thm = let (* Debug information: Stores string*term pairs, which are pretty-printed on error *) val dbg = Unsynchronized.ref [] fun add_dbg msg ts = ( dbg := (msg,ts) :: !dbg; () ) fun pretty_dbg (msg,ts) = Pretty.block [ Pretty.str msg, Pretty.str ":", Pretty.brk 1, Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) ts) ] fun pretty_dbgs l = map pretty_dbg l |> Pretty.fbreaks |> Pretty.block fun trace_dbg msg = Pretty.block [Pretty.str msg, Pretty.fbrk, pretty_dbgs (rev (!dbg))] |> Pretty.string_of |> tracing fun fail msg = (trace_dbg msg; raise THM(msg,~1,[thm])) fun assert cond msg = cond orelse fail msg; (* Heads may have a leading return/RETURN. The following code strips off the leading return, unless it has the form "return x" for an argument x *) fun check_strip_leading args t f = (* Handle the case RETURN x, where x is an argument *) if Termtab.defined args f then (t,false) else (f,true) fun strip_leading_RETURN args (t as @{mpat "RETURN$(?f)"}) = check_strip_leading args t f | strip_leading_RETURN args (t as @{mpat "RETURN ?f"}) = check_strip_leading args t f | strip_leading_RETURN _ t = (t,false) fun strip_leading_return args (t as @{mpat "return$(?f)"}) = check_strip_leading args t f | strip_leading_return args (t as @{mpat "return ?f"}) = check_strip_leading args t f | strip_leading_return _ t = (t,false) (* The following code strips the arguments of the concrete or abstract function. It knows how to handle APP-tags ($), and stops at PR_CONST-tags. Moreover, it only strips actual arguments that occur in the precondition-section of the hn_refine-statement. This ensures that non-arguments, like maxsize, are treated correctly. *) fun strip_fun _ (t as @{mpat "PR_CONST _"}) = (t,[]) | strip_fun s (t as @{mpat "?f$?x"}) = check_arg s t f x | strip_fun s (t as @{mpat "?f ?x"}) = check_arg s t f x | strip_fun _ f = (f,[]) and check_arg s t f x = if Termtab.defined s x then strip_fun s f |> apsnd (curry op :: x) else (t,[]) (* Arguments in the pre/postcondition are wrapped into hn_ctxt tags. This function strips them off. *) fun dest_hn_ctxt @{mpat "hn_ctxt ?R ?a ?c"} = ((a,c),R) | dest_hn_ctxt _ = fail "Invalid hn_ctxt parameter in pre or postcondition" fun dest_hn_refine @{mpat "(hn_refine ?G ?c ?G' ?R ?a)"} = (G,c,G',R,a) | dest_hn_refine _ = fail "Conclusion is not a hn_refine statement" (* Strip separation conjunctions. Special case for "emp", which is ignored. *) fun is_emp @{mpat emp} = true | is_emp _ = false val strip_star' = Sepref_Basic.strip_star #> filter (not o is_emp) (* Compare Termtab2s for equality of keys *) fun pairs_eq pairs1 pairs2 = Termtab2.forall (Termtab2.defined pairs1 o fst) pairs2 andalso Termtab2.forall (Termtab2.defined pairs2 o fst) pairs1 fun atomize_prem @{mpat "Trueprop ?p"} = p | atomize_prem _ = fail "Non-atomic premises" (* Make HOL conjunction list *) fun mk_conjs [] = @{const True} | mk_conjs [p] = p | mk_conjs (p::ps) = HOLogic.mk_binop @{const_name "HOL.conj"} (p,mk_conjs ps) (***********************) (* Start actual analysis *) val _ = add_dbg "thm" [Thm.prop_of thm] val prems = Thm.prems_of thm val concl = Thm.concl_of thm |> HOLogic.dest_Trueprop val (G,c,G',R,a) = dest_hn_refine concl val pre_pairs = G |> strip_star' |> tap (add_dbg "precondition") |> map dest_hn_ctxt |> Termtab2.make val post_pairs = G' |> strip_star' |> tap (add_dbg "postcondition") |> map dest_hn_ctxt |> Termtab2.make val _ = assert (pairs_eq pre_pairs post_pairs) "Parameters in precondition do not match postcondition" val aa_set = pre_pairs |> Termtab2.keys |> map fst |> Termtab.make_set val ca_set = pre_pairs |> Termtab2.keys |> map snd |> Termtab.make_set val (a,leading_RETURN) = strip_leading_RETURN aa_set a val (c,leading_return) = strip_leading_return ca_set c val _ = add_dbg "stripped abstract term" [a] val _ = add_dbg "stripped concrete term" [c] val (ahead,aargs) = strip_fun aa_set a; val (chead,cargs) = strip_fun ca_set c; val _ = add_dbg "abstract head" [ahead] val _ = add_dbg "abstract args" aargs val _ = add_dbg "concrete head" [chead] val _ = add_dbg "concrete args" cargs val _ = assert (length cargs = length aargs) "Different number of abstract and concrete arguments"; val _ = assert (not (has_duplicates op aconv aargs)) "Duplicate abstract arguments" val _ = assert (not (has_duplicates op aconv cargs)) "Duplicate concrete arguments" val argpairs = aargs ~~ cargs val ap_set = Termtab2.make_set argpairs val _ = assert (pairs_eq pre_pairs ap_set) "Arguments from pre/postcondition do not match operation's arguments" val pre_rels = map (the o (Termtab2.lookup pre_pairs)) argpairs val post_rels = map (the o (Termtab2.lookup post_pairs)) argpairs val _ = add_dbg "pre-rels" pre_rels val _ = add_dbg "post-rels" post_rels fun adjust_hf_pres @{mpat "snd (?R\<^sup>k)"} = R | adjust_hf_pres t = t val post_rels = map adjust_hf_pres post_rels fun is_invalid R @{mpat "invalid_assn ?R'"} = R aconv R' | is_invalid _ @{mpat "snd (_\<^sup>d)"} = true | is_invalid _ _ = false fun is_keep (R,R') = if R aconv R' then true else if is_invalid R R' then false else fail "Mismatch between pre and post relation for argument" val keep = map is_keep (pre_rels ~~ post_rels) val argrels = pre_rels ~~ keep val aa_set = Termtab.make_set aargs val ca_set = Termtab.make_set cargs fun is_precond t = (exists_subterm (Termtab.defined ca_set) t andalso fail "Premise contains concrete argument") orelse exists_subterm (Termtab.defined aa_set) t val (preconds, prems) = split is_precond prems val precond = map atomize_prem preconds |> mk_conjs |> fold lambda aargs val _ = add_dbg "precond" [precond] val _ = add_dbg "prems" prems in { thm = thm, precond = precond, prems = prems, ahead = (ahead,leading_RETURN), chead = (chead,leading_return), argrels = argrels, result_rel = R } end fun pretty_hnr_analysis ctxt ({thm,precond,ahead,chead,argrels,result_rel,...}) : Pretty.T = let val _ = thm (* Suppress unused warning for thm *) fun pretty_argrel (R,k) = Pretty.block [ Syntax.pretty_term ctxt R, if k then Pretty.str "\<^sup>k" else Pretty.str "\<^sup>d" ] val pretty_chead = case chead of (t,false) => Syntax.pretty_term ctxt t | (t,true) => Pretty.block [Pretty.str "return ", Syntax.pretty_term ctxt t] val pretty_ahead = case ahead of (t,false) => Syntax.pretty_term ctxt t | (t,true) => Pretty.block [Pretty.str "RETURN ", Syntax.pretty_term ctxt t] in Pretty.fbreaks [ (*Display.pretty_thm ctxt thm,*) Pretty.block [ Pretty.enclose "[" "]" [pretty_chead, pretty_ahead], Pretty.enclose "[" "]" [Syntax.pretty_term ctxt precond], Pretty.brk 1, Pretty.block (Pretty.separate " \" (map pretty_argrel argrels @ [Syntax.pretty_term ctxt result_rel])) ] ] |> Pretty.block end fun mk_hfref_thm ctxt ({thm,precond,prems,ahead,chead,argrels,result_rel}) = let fun mk_keep (R,true) = @{mk_term "?R\<^sup>k"} | mk_keep (R,false) = @{mk_term "?R\<^sup>d"} (* TODO: Move, this is of general use! *) fun mk_uncurry f = @{mk_term "uncurry ?f"} (* Uncurry function for the given number of arguments. For zero arguments, add a unit-parameter. *) fun rpt_uncurry n t = if n=0 then @{mk_term "uncurry0 ?t"} else if n=1 then t else funpow (n-1) mk_uncurry t (* Rewrite uncurried lambda's to \(_,_). _ form. Use top-down rewriting to correctly handle nesting to the left. TODO: Combine with abstraction and uncurry-procedure, and mark the deviation about uncurry as redundant intermediate step to be eliminated. *) fun rew_uncurry_lambda t = let val rr = map (Logic.dest_equals o Thm.prop_of) @{thms uncurry_def uncurry0_def} val thy = Proof_Context.theory_of ctxt in Pattern.rewrite_term_top thy rr [] t end (* Shortcuts for simplification tactics *) fun gsimp_only ctxt sec = let val ss = put_simpset HOL_basic_ss ctxt |> sec in asm_full_simp_tac ss end fun simp_only ctxt thms = gsimp_only ctxt (fn ctxt => ctxt addsimps thms) (********************************) (* Build theorem statement *) (* \prems\ \ (chead,ahead) \ [precond] rels \ R *) (* Uncurry precondition *) val num_args = length argrels val precond = precond |> rpt_uncurry num_args |> rew_uncurry_lambda (* Convert to nicer \((...,_),_) - form*) (* Re-attach leading RETURN/return *) fun mk_RETURN (t,r) = if r then let val T = funpow num_args range_type (fastype_of (fst ahead)) val tRETURN = Const (@{const_name RETURN}, T --> Type(@{type_name nres},[T])) in Refine_Util.mk_compN num_args tRETURN t end else t fun mk_return (t,r) = if r then let val T = funpow num_args range_type (fastype_of (fst chead)) val tRETURN = Const (@{const_name return}, T --> Type(@{type_name Heap},[T])) in Refine_Util.mk_compN num_args tRETURN t end else t (* Hrmpf!: Gone for good from 2015\2016. Inserting ctxt-based substitute here. *) fun certify_inst ctxt (instT, inst) = (map (apsnd (Thm.ctyp_of ctxt)) (Term_Subst.TVars.dest instT), map (apsnd (Thm.cterm_of ctxt)) (Term_Subst.Vars.dest inst)); (* fun mk_RETURN (t,r) = if r then @{mk_term "RETURN o ?t"} else t fun mk_return (t,r) = if r then @{mk_term "return o ?t"} else t *) (* Uncurry abstract and concrete function, append leading return *) val ahead = ahead |> mk_RETURN |> rpt_uncurry num_args val chead = chead |> mk_return |> rpt_uncurry num_args (* Add keep-flags and summarize argument relations to product *) val argrel = map mk_keep argrels |> rev (* TODO: Why this rev? *) |> mk_hfprods (* Produce final result statement *) val result = @{mk_term "Trueprop ((?chead,?ahead) \ [?precond]\<^sub>a ?argrel \ ?result_rel)"} val result = Logic.list_implies (prems,result) (********************************) (* Prove theorem *) (* Create context and import result statement and original theorem *) val orig_ctxt = ctxt (*val thy = Proof_Context.theory_of ctxt*) val (insts, ctxt) = Variable.import_inst true [result] ctxt val insts' = certify_inst ctxt insts val result = Term_Subst.instantiate insts result val thm = Thm.instantiate insts' thm (* Unfold APP tags. This is required as some APP-tags have also been unfolded by analysis *) val thm = Local_Defs.unfold0 ctxt @{thms APP_def} thm (* Tactic to prove the theorem. A first step uses hfrefI to get a hnr-goal. This is then normalized in several consecutive steps, which get rid of uncurrying. Finally, the original theorem is used for resolution, where the pre- and postcondition, and result relation are connected with a consequence rule, to handle unfolded hn_ctxt-tags, re-ordered relations, and introduced unit-parameters (TODO: Mark artificially introduced unit-parameter specially, it may get confused with intentional unit-parameter, e.g., functional empty_set ()!) *) fun tac ctxt = resolve_tac ctxt @{thms hfrefI} THEN' gsimp_only ctxt (fn c => c addsimps @{thms uncurry_def hn_ctxt_def uncurry0_def keep_drop_sels uc_hfprod_sel o_apply APP_def} |> Splitter.add_split @{thm prod.split} ) THEN' TRY o ( REPEAT_ALL_NEW (match_tac ctxt @{thms allI impI}) THEN' simp_only ctxt @{thms Product_Type.split prod.inject}) THEN' TRY o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE}) THEN' TRY o hyp_subst_tac ctxt THEN' simp_only ctxt @{thms triv_forall_equality} THEN' ( resolve_tac ctxt @{thms hn_refine_cons[rotated]} THEN' (resolve_tac ctxt [thm] THEN_ALL_NEW assume_tac ctxt)) THEN_ALL_NEW simp_only ctxt @{thms hn_ctxt_def entt_refl pure_unit_rel_eq_empty mult_ac mult_1 mult_1_right keep_drop_sels} (* Prove theorem *) val result = Thm.cterm_of ctxt result val rthm = Goal.prove_internal ctxt [] result (fn _ => ALLGOALS (tac ctxt)) (* Export statement to original context *) val rthm = singleton (Variable.export ctxt orig_ctxt) rthm (* Post-processing *) val rthm = Local_Defs.unfold0 ctxt (Named_Theorems.get ctxt @{named_theorems to_hfref_post}) rthm in rthm end fun to_hfref ctxt = analyze_hnr ctxt #> mk_hfref_thm ctxt (***********************************) (* Composition *) local fun norm_set_of ctxt = { trans_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_trans}, cong_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_cong}, norm_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_norm}, refl_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_refl} } fun init_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_init} fun unfold_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_unfold} fun simp_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_simps} in fun norm_fcomp_rule ctxt = let open PO_Normalizer Refine_Util val norm1 = gen_norm_rule (init_rules_of ctxt) (norm_set_of ctxt) ctxt val norm2 = Local_Defs.unfold0 ctxt (unfold_rules_of ctxt) val norm3 = Conv.fconv_rule ( Simplifier.asm_full_rewrite (put_simpset HOL_basic_ss ctxt addsimps simp_rules_of ctxt)) val norm = changed_rule (try_rule norm1 o try_rule norm2 o try_rule norm3) in repeat_rule norm end end fun add_pure_constraints_rule ctxt thm = let val orig_ctxt = ctxt val t = Thm.prop_of thm fun cnv (@{mpat (typs) "pure (mpaq_STRUCT (mpaq_Var ?x _) :: (?'v_c\?'v_a) set)"}) = let val T = a --> c --> @{typ assn} val t = Var (x,T) val t = @{mk_term "(the_pure ?t)"} in [(x,T,t)] end | cnv (t$u) = union op= (cnv t) (cnv u) | cnv (Abs (_,_,t)) = cnv t | cnv _ = [] val pvars = cnv t val _ = (pvars |> map #1 |> has_duplicates op=) andalso raise TERM ("Duplicate indexname with different type",[t]) (* This should not happen *) val substs = map (fn (x,_,t) => (x,t)) pvars val t' = subst_Vars substs t fun mk_asm (x,T,_) = let val t = Var (x,T) val t = @{mk_term "Trueprop (CONSTRAINT is_pure ?t)"} in t end val assms = map mk_asm pvars fun add_prems prems t = let val prems' = Logic.strip_imp_prems t val concl = Logic.strip_imp_concl t in Logic.list_implies (prems@prems', concl) end val t' = add_prems assms t' val (t',ctxt) = yield_singleton (Variable.import_terms true) t' ctxt val thm' = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt t') (fn _ => ALLGOALS (resolve_tac ctxt [thm] THEN_ALL_NEW assume_tac ctxt)) val thm' = norm_fcomp_rule ctxt thm' val thm' = singleton (Variable.export ctxt orig_ctxt) thm' in thm' end val cfg_simp_precond = Attrib.setup_config_bool @{binding fcomp_simp_precond} (K true) local fun mk_simp_thm ctxt t = let val st = t |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Goal.init val ctxt = Context_Position.set_visible false ctxt val ctxt = ctxt addsimps ( refine_pw_simps.get ctxt @ Named_Theorems.get ctxt @{named_theorems fcomp_prenorm_simps} @ @{thms split_tupled_all cnv_conj_to_meta} ) val trace_incomplete_transfer_tac = COND (Thm.prems_of #> exists (strip_all_body #> Logic.strip_imp_concl #> Term.is_open)) (print_tac ctxt "Failed transfer from intermediate level:") all_tac val tac = ALLGOALS (resolve_tac ctxt @{thms auto_weaken_pre_comp_PRE_I} ) THEN ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN trace_incomplete_transfer_tac THEN ALLGOALS (TRY o filter_prems_tac ctxt (K false)) THEN Local_Defs.unfold0_tac ctxt [Drule.triv_forall_equality] val st' = tac st |> Seq.take 1 |> Seq.list_of val thm = case st' of [st'] => Goal.conclude st' | _ => raise THM("Simp_Precond: Simp-Tactic failed",~1,[st]) (* Check generated premises for leftover intermediate stuff *) val _ = exists (Logic.is_all) (Thm.prems_of thm) andalso raise THM("Simp_Precond: Transfer from intermediate level failed",~1,[thm]) val thm = thm (*|> map (Simplifier.asm_full_simplify ctxt)*) |> Conv.fconv_rule (Object_Logic.atomize ctxt) |> Local_Defs.unfold0 ctxt @{thms auto_weaken_pre_to_imp_nf} val thm = case Thm.concl_of thm of @{mpat "Trueprop (_ \ _)"} => thm | @{mpat "Trueprop _"} => thm RS @{thm auto_weaken_pre_add_dummy_imp} | _ => raise THM("Simp_Precond: Generated odd theorem, expected form 'P\Q'",~1,[thm]) in thm end in fun simplify_precond ctxt thm = let val orig_ctxt = ctxt val thm = Refine_Util.OF_fst @{thms auto_weaken_pre_init} [asm_rl,thm] val thm = Local_Defs.unfold0 ctxt @{thms split_tupled_all} thm OF @{thms auto_weaken_pre_uncurry_start} fun rec_uncurry thm = case try (fn () => thm OF @{thms auto_weaken_pre_uncurry_step}) () of NONE => thm OF @{thms auto_weaken_pre_uncurry_finish} | SOME thm => rec_uncurry thm val thm = rec_uncurry thm |> Conv.fconv_rule Thm.eta_conversion val t = case Thm.prems_of thm of t::_ => t | _ => raise THM("Simp-Precond: Expected at least one premise",~1,[thm]) val (t,ctxt) = yield_singleton (Variable.import_terms false) t ctxt val ((_,t),ctxt) = Variable.focus NONE t ctxt val t = case t of @{mpat "Trueprop (_ \ ?t)"} => t | _ => raise TERM("Simp_Precond: Expected implication",[t]) val simpthm = mk_simp_thm ctxt t |> singleton (Variable.export ctxt orig_ctxt) val thm = thm OF [simpthm] val thm = Local_Defs.unfold0 ctxt @{thms prod_casesK} thm in thm end fun simplify_precond_if_cfg ctxt = if Config.get ctxt cfg_simp_precond then simplify_precond ctxt else I end (* fref O fref *) fun compose_ff ctxt A B = (@{thm fref_compI_PRE} OF [A,B]) |> norm_fcomp_rule ctxt |> simplify_precond_if_cfg ctxt |> Conv.fconv_rule Thm.eta_conversion (* hfref O fref *) fun compose_hf ctxt A B = (@{thm hfref_compI_PRE} OF [A,B]) |> norm_fcomp_rule ctxt |> simplify_precond_if_cfg ctxt |> Conv.fconv_rule Thm.eta_conversion |> add_pure_constraints_rule ctxt |> Conv.fconv_rule Thm.eta_conversion fun ensure_fref ctxt thm = case rthm_type thm of RT_HOPARAM => to_fref ctxt thm | RT_FREF => thm | _ => raise THM("Expected parametricity or fref theorem",~1,[thm]) fun ensure_fref_nres ctxt thm = let val thm = ensure_fref ctxt thm in case Thm.concl_of thm of @{mpat (typs) "Trueprop (_\fref _ _ (_::(_ nres\_)set))"} => thm | @{mpat "Trueprop ((_,_)\fref _ _ _)"} => (thm RS @{thm ensure_fref_nresI}) |> Local_Defs.unfold0 ctxt @{thms ensure_fref_nres_unfold} | _ => raise THM("Expected fref-theorem",~1,[thm]) end fun ensure_hfref ctxt thm = case rthm_type thm of RT_HNR => to_hfref ctxt thm | RT_HFREF => thm | _ => raise THM("Expected hnr or hfref theorem",~1,[thm]) fun ensure_hnr ctxt thm = case rthm_type thm of RT_HNR => thm | RT_HFREF => to_hnr ctxt thm | _ => raise THM("Expected hnr or hfref theorem",~1,[thm]) fun gen_compose ctxt A B = let val rtA = rthm_type A in if rtA = RT_HOPARAM orelse rtA = RT_FREF then compose_ff ctxt (ensure_fref ctxt A) (ensure_fref ctxt B) else compose_hf ctxt (ensure_hfref ctxt A) ((ensure_fref_nres ctxt B)) end val parse_fcomp_flags = Refine_Util.parse_paren_lists (Refine_Util.parse_bool_config "prenorm" cfg_simp_precond) val fcomp_attrib = parse_fcomp_flags |-- Attrib.thm >> (fn B => Thm.rule_attribute [] (fn context => fn A => let val ctxt = Context.proof_of context in gen_compose ctxt A B end)) end \ attribute_setup to_fref = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_fref o Context.proof_of)) \ "Convert parametricity theorem to uncurried fref-form" attribute_setup to_foparam = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_foparam o Context.proof_of)) \ \Convert param or fref rule to first order rule\ (* Overloading existing param_fo - attribute from Parametricity.thy *) attribute_setup param_fo = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_foparam o Context.proof_of)) \ \Convert param or fref rule to first order rule\ attribute_setup to_hnr = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_hnr o Context.proof_of)) \ "Convert hfref-rule to hnr-rule" attribute_setup to_hfref = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.to_hfref) )\ \Convert hnr to hfref theorem\ attribute_setup ensure_fref_nres = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.ensure_fref_nres) )\ attribute_setup sepref_dbg_norm_fcomp_rule = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.norm_fcomp_rule) )\ attribute_setup sepref_simplify_precond = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.simplify_precond) )\ \Simplify precondition of fref/hfref-theorem\ attribute_setup FCOMP = Sepref_Rules.fcomp_attrib "Composition of refinement rules" end diff --git a/thys/Refine_Imperative_HOL/Sepref_Translate.thy b/thys/Refine_Imperative_HOL/Sepref_Translate.thy --- a/thys/Refine_Imperative_HOL/Sepref_Translate.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Translate.thy @@ -1,927 +1,927 @@ section \Translation\ theory Sepref_Translate imports Sepref_Monadify Sepref_Constraints Sepref_Frame "Lib/Pf_Mono_Prover" Sepref_Rules Sepref_Combinator_Setup "Lib/User_Smashing" begin text \ This theory defines the translation phase. The main functionality of the translation phase is to apply refinement rules. Thereby, the linearity information is exploited to create copies of parameters that are still required, but would be destroyed by a synthesized operation. These \emph{frame-based} rules are in the named theorem collection \sepref_fr_rules\, and the collection \sepref_copy_rules\ contains rules to handle copying of parameters. Apart from the frame-based rules described above, there is also a set of rules for combinators, in the collection \sepref_comb_rules\, where no automatic copying of parameters is applied. Moreover, this theory contains \begin{itemize} \item A setup for the basic monad combinators and recursion. \item A tool to import parametricity theorems. \item Some setup to identify pure refinement relations, i.e., those not involving the heap. \item A preprocessor that identifies parameters in refinement goals, and flags them with a special tag, that allows their correct handling. \end{itemize} \ (*subsection \Basic Translation Tool\ definition COPY -- "Copy operation" where [simp]: "COPY \ RETURN" lemma tagged_nres_monad1: "Refine_Basic.bind$(RETURN$x)$(\\<^sub>2x. f x) = f x" by simp text \The PREPARED-tag is used internally, to flag a refinement goal with the index of the refinement rule to be used\ definition PREPARED_TAG :: "'a => nat => 'a" where [simp]: "PREPARED_TAG x i == x" lemma PREPARED_TAG_I: "hn_refine \ c \' R a \ hn_refine \ c \' R (PREPARED_TAG a i)" by simp lemmas prepare_refine_simps = tagged_nres_monad1 COPY_def PREPARED_TAG_def lemma mono_trigger: "mono_Heap F \ mono_Heap F" . *) text \Tag to keep track of abstract bindings. Required to recover information for side-condition solving.\ definition "bind_ref_tag x m \ RETURN x \ m" (* abbreviation DEP_SIDE_PRECOND -- \Precondition that depends on information from relators, like maximum size. It must be processed after frame inference, when the relator variables have been fixed.\ where "DEP_SIDE_PRECOND \ \ DEFER_tag (PRECOND_tag \)" lemma DEP_SIDE_PRECOND_D: "DEP_SIDE_PRECOND P \ P" by simp *) text \Tag to keep track of preconditions in assertions\ definition "vassn_tag \ \ \h. h\\" lemma vassn_tagI: "h\\ \ vassn_tag \" unfolding vassn_tag_def .. lemma vassn_dest[dest!]: "vassn_tag (\\<^sub>1 * \\<^sub>2) \ vassn_tag \\<^sub>1 \ vassn_tag \\<^sub>2" "vassn_tag (hn_ctxt R a b) \ a\rdom R" unfolding vassn_tag_def rdomp_def[abs_def] by (auto simp: mod_star_conv hn_ctxt_def) lemma entails_preI: assumes "vassn_tag A \ A \\<^sub>A B" shows "A \\<^sub>A B" using assms by (auto simp: entails_def vassn_tag_def) lemma invalid_assn_const: "invalid_assn (\_ _. P) x y = \(vassn_tag P) * true" by (simp_all add: invalid_assn_def vassn_tag_def) lemma vassn_tag_simps[simp]: "vassn_tag emp" "vassn_tag true" by (sep_auto simp: vassn_tag_def mod_emp)+ definition "GEN_ALGO f \ \ \ f" \ \Tag to synthesize @{term f} with property @{term \}.\ lemma is_GEN_ALGO: "GEN_ALGO f \ \ GEN_ALGO f \" . text \Tag for side-condition solver to discharge by assumption\ definition RPREM :: "bool \ bool" where [simp]: "RPREM P = P" lemma RPREMI: "P \ RPREM P" by simp lemma trans_frame_rule: assumes "RECOVER_PURE \ \'" assumes "vassn_tag \' \ hn_refine \' c \'' R a" shows "hn_refine (F*\) c (F*\'') R a" apply (rule hn_refine_frame[OF _ entt_refl]) applyF (rule hn_refine_cons_pre) focus using assms(1) unfolding RECOVER_PURE_def apply assumption solved apply1 (rule hn_refine_preI) apply1 (rule assms) applyS (auto simp add: vassn_tag_def) solved done lemma recover_pure_cons: \ \Used for debugging\ assumes "RECOVER_PURE \ \'" assumes "hn_refine \' c \'' R a" shows "hn_refine (\) c (\'') R a" using trans_frame_rule[where F=emp, OF assms] by simp \ \Tag to align structure of refinement assertions for consequence rule\ definition CPR_TAG :: "assn \ assn \ bool" where [simp]: "CPR_TAG y x \ True" lemma CPR_TAG_starI: assumes "CPR_TAG P1 Q1" assumes "CPR_TAG P2 Q2" shows "CPR_TAG (P1*P2) (Q1*Q2)" by simp lemma CPR_tag_ctxtI: "CPR_TAG (hn_ctxt R x xi) (hn_ctxt R' x xi)" by simp lemma CPR_tag_fallbackI: "CPR_TAG P Q" by simp lemmas CPR_TAG_rules = CPR_TAG_starI CPR_tag_ctxtI CPR_tag_fallbackI lemma cons_pre_rule: \ \Consequence rule to be applied if no direct operation rule matches\ assumes "CPR_TAG P P'" assumes "P \\<^sub>t P'" assumes "hn_refine P' c Q R m" shows "hn_refine P c Q R m" using assms(2-) by (rule hn_refine_cons_pre) named_theorems_rev sepref_gen_algo_rules \Sepref: Generic algorithm rules\ ML \ structure Sepref_Translate = struct val cfg_debug = Attrib.setup_config_bool @{binding sepref_debug_translate} (K false) val dbg_msg_tac = Sepref_Debugging.dbg_msg_tac cfg_debug fun gen_msg_analyze t ctxt = let val t = Logic.strip_assums_concl t in case t of @{mpat "Trueprop ?t"} => (case t of @{mpat "_ \\<^sub>A _ \\<^sub>t _"} => "t_merge" | @{mpat "_ \\<^sub>t _"} => "t_frame" | @{mpat "INDEP _"} => "t_indep" | @{mpat "CONSTRAINT _ _"} => "t_constraint" | @{mpat "mono_Heap _"} => "t_mono" | @{mpat "PREFER_tag _"} => "t_prefer" | @{mpat "DEFER_tag _"} => "t_defer" | @{mpat "RPREM _"} => "t_rprem" | @{mpat "hn_refine _ _ _ _ ?a"} => Pretty.block [Pretty.str "t_hnr: ",Pretty.brk 1, Syntax.pretty_term ctxt a] |> Pretty.string_of | _ => "Unknown goal type" ) | _ => "Non-Trueprop goal" end fun msg_analyze msg = Sepref_Debugging.msg_from_subgoal msg gen_msg_analyze fun check_side_conds thm = let open Sepref_Basic (* Check that term is no binary operator on assertions *) fun is_atomic (Const (_,@{typ "assn\assn\assn"})$_$_) = false | is_atomic _ = true val is_atomic_star_list = ("Expected atoms separated by star",forall is_atomic o strip_star) val is_trueprop = ("Expected Trueprop conclusion",can HOLogic.dest_Trueprop) fun assert t' (msg,p) t = if p t then () else raise TERM(msg,[t',t]) fun chk_prem t = let val assert = assert t fun chk @{mpat "?l \\<^sub>A ?r \\<^sub>t ?m"} = ( assert is_atomic_star_list l; assert is_atomic_star_list r; assert is_atomic_star_list m ) | chk (t as @{mpat "_ \\<^sub>A _"}) = raise TERM("Invalid frame side condition (old-style ent)",[t]) | chk @{mpat "?l \\<^sub>t ?r"} = ( assert is_atomic_star_list l; assert is_atomic_star_list r ) | chk _ = () val t = Logic.strip_assums_concl t in assert is_trueprop t; chk (HOLogic.dest_Trueprop t) end in map chk_prem (Thm.prems_of thm) end structure sepref_comb_rules = Named_Sorted_Thms ( val name = @{binding "sepref_comb_rules"} val description = "Sepref: Combinator rules" val sort = K I fun transform _ thm = let val _ = check_side_conds thm in [thm] end ) structure sepref_fr_rules = Named_Sorted_Thms ( val name = @{binding "sepref_fr_rules"} val description = "Sepref: Frame-based rules" val sort = K I fun transform context thm = let val ctxt = Context.proof_of context val thm = Sepref_Rules.ensure_hnr ctxt thm |> Conv.fconv_rule (Sepref_Frame.align_rl_conv ctxt) val _ = check_side_conds thm val _ = case try (Sepref_Rules.analyze_hnr ctxt) thm of NONE => (Pretty.block [ Pretty.str "hnr-analysis failed", Pretty.str ":", Pretty.brk 1, Thm.pretty_thm ctxt thm]) |> Pretty.string_of |> error | SOME ana => let val _ = Sepref_Combinator_Setup.is_valid_abs_op ctxt (fst (#ahead ana)) orelse Pretty.block [ Pretty.str "Invalid abstract head:", Pretty.brk 1, Pretty.enclose "(" ")" [Syntax.pretty_term ctxt (fst (#ahead ana))], Pretty.brk 1, Pretty.str "in thm", Pretty.brk 1, Thm.pretty_thm ctxt thm ] |> Pretty.string_of |> error in () end in [thm] end ) (***** Side Condition Solving *) local open Sepref_Basic in fun side_unfold_tac ctxt = let (*val ctxt = put_simpset HOL_basic_ss ctxt addsimps sepref_prep_side_simps.get ctxt*) in CONVERSION (Id_Op.unprotect_conv ctxt) THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms bind_ref_tag_def}) (*THEN' asm_full_simp_tac ctxt*) end fun side_fallback_tac ctxt = side_unfold_tac ctxt THEN' TRADE (SELECT_GOAL o auto_tac) ctxt val side_frame_tac = Sepref_Frame.frame_tac side_fallback_tac val side_merge_tac = Sepref_Frame.merge_tac side_fallback_tac fun side_constraint_tac ctxt = Sepref_Constraints.constraint_tac ctxt fun side_mono_tac ctxt = side_unfold_tac ctxt THEN' TRADE Pf_Mono_Prover.mono_tac ctxt fun side_gen_algo_tac ctxt = side_unfold_tac ctxt THEN' resolve_tac ctxt (Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_gen_algo_rules}) fun side_pref_def_tac ctxt = side_unfold_tac ctxt THEN' TRADE (fn ctxt => resolve_tac ctxt @{thms PREFER_tagI DEFER_tagI} THEN' (Sepref_Debugging.warning_tac' "Obsolete PREFER/DEFER side condition" ctxt THEN' Tagged_Solver.solve_tac ctxt) ) ctxt fun side_rprem_tac ctxt = resolve_tac ctxt @{thms RPREMI} THEN' Refine_Util.rprems_tac ctxt THEN' (K (smash_new_rule ctxt)) (* Solve side condition, or invoke hnr_tac on hn_refine goal. In debug mode, side-condition solvers are allowed to not completely solve the side condition, but must change the goal. *) fun side_cond_dispatch_tac dbg hnr_tac ctxt = let fun MK tac = if dbg then CHANGED o tac ctxt else SOLVED' (tac ctxt) val t_merge = MK side_merge_tac val t_frame = MK side_frame_tac val t_indep = MK Indep_Vars.indep_tac val t_constraint = MK side_constraint_tac val t_mono = MK side_mono_tac val t_pref_def = MK side_pref_def_tac val t_rprem = MK side_rprem_tac val t_gen_algo = side_gen_algo_tac ctxt val t_fallback = MK side_fallback_tac in WITH_concl (fn @{mpat "Trueprop ?t"} => (case t of @{mpat "_ \\<^sub>A _ \\<^sub>t _"} => t_merge | @{mpat "_ \\<^sub>t _"} => t_frame | @{mpat "_ \\<^sub>A _"} => Sepref_Debugging.warning_tac' "Old-style frame side condition" ctxt THEN' (K no_tac) | @{mpat "INDEP _"} => t_indep (* TODO: Get rid of this!? *) | @{mpat "CONSTRAINT _ _"} => t_constraint | @{mpat "mono_Heap _"} => t_mono | @{mpat "PREFER_tag _"} => t_pref_def | @{mpat "DEFER_tag _"} => t_pref_def | @{mpat "RPREM _"} => t_rprem | @{mpat "GEN_ALGO _ _"} => t_gen_algo | @{mpat "hn_refine _ _ _ _ _"} => hnr_tac | _ => t_fallback ) | _ => K no_tac ) end end (***** Main Translation Tactic *) local open Sepref_Basic STactical (* ATTENTION: Beware of evaluation order, as some initialization operations on context are expensive, and should not be repeated during proof search! *) in (* Translate combinator, yields new translation goals and side conditions which must be processed in order. *) fun trans_comb_tac ctxt = let val comb_rl_net = sepref_comb_rules.get ctxt |> Tactic.build_net in DETERM o ( resolve_from_net_tac ctxt comb_rl_net ORELSE' ( Sepref_Frame.norm_goal_pre_tac ctxt THEN' resolve_from_net_tac ctxt comb_rl_net ) ) end (* Translate operator. Only succeeds if it finds an operator rule such that all resulting side conditions can be solved. Takes the first such rule. In debug mode, it returns a sequence of the unsolved side conditions of each applicable rule. *) fun gen_trans_op_tac dbg ctxt = let val fr_rl_net = sepref_fr_rules.get ctxt |> Tactic.build_net val fr_rl_tac = resolve_from_net_tac ctxt fr_rl_net (* Try direct match *) ORELSE' ( Sepref_Frame.norm_goal_pre_tac ctxt (* Normalize precondition *) THEN' ( resolve_from_net_tac ctxt fr_rl_net ORELSE' ( resolve_tac ctxt @{thms cons_pre_rule} (* Finally, generate a frame condition *) THEN_ALL_NEW_LIST [ SOLVED' (REPEAT_ALL_NEW_FWD (DETERM o resolve_tac ctxt @{thms CPR_TAG_rules})), K all_tac, (* Frame remains unchanged as first goal, even if fr_rl creates side-conditions *) resolve_from_net_tac ctxt fr_rl_net ] ) ) ) val side_tac = REPEAT_ALL_NEW_FWD (side_cond_dispatch_tac false (K no_tac) ctxt) val fr_tac = if dbg then (* Present all possibilities with (partially resolved) side conditions *) fr_rl_tac THEN_ALL_NEW_FWD (TRY o side_tac) else (* Choose first rule that solves all side conditions *) DETERM o SOLVED' (fr_rl_tac THEN_ALL_NEW_FWD (SOLVED' side_tac)) in PHASES' [ ("Align goal",Sepref_Frame.align_goal_tac, 0), ("Frame rule",fn ctxt => resolve_tac ctxt @{thms trans_frame_rule}, 1), (* RECOVER_PURE goal *) ("Recover pure",Sepref_Frame.recover_pure_tac, ~1), (* hn-refine goal with stripped precondition *) ("Apply rule",K fr_tac,~1) ] (flag_phases_ctrl dbg) ctxt end (* Translate combinator, operator, or side condition. *) fun gen_trans_step_tac dbg ctxt = side_cond_dispatch_tac dbg (trans_comb_tac ctxt ORELSE' gen_trans_op_tac dbg ctxt) ctxt val trans_step_tac = gen_trans_step_tac false val trans_step_keep_tac = gen_trans_step_tac true fun gen_trans_tac dbg ctxt = PHASES' [ ("Translation steps",REPEAT_DETERM' o trans_step_tac,~1), ("Constraint solving",fn ctxt => fn _ => Sepref_Constraints.process_constraint_slot ctxt, 0) ] (flag_phases_ctrl dbg) ctxt val trans_tac = gen_trans_tac false val trans_keep_tac = gen_trans_tac true end val setup = I #> sepref_fr_rules.setup #> sepref_comb_rules.setup end \ setup Sepref_Translate.setup subsubsection \Basic Setup\ lemma hn_pass[sepref_fr_rules]: shows "hn_refine (hn_ctxt P x x') (return x') (hn_invalid P x x') P (PASS$x)" apply rule apply (sep_auto simp: hn_ctxt_def invalidate_clone') done (*lemma hn_pass_pure[sepref_fr_rules]: shows "hn_refine (hn_val P x x') (return x') (hn_val P x x') (pure P) (PASS$x)" by rule (sep_auto simp: hn_ctxt_def pure_def) *) lemma hn_bind[sepref_comb_rules]: assumes D1: "hn_refine \ m' \1 Rh m" assumes D2: "\x x'. bind_ref_tag x m \ hn_refine (\1 * hn_ctxt Rh x x') (f' x') (\2 x x') R (f x)" assumes IMP: "\x x'. \2 x x' \\<^sub>t \' * hn_ctxt Rx x x'" shows "hn_refine \ (m'\f') \' R (Refine_Basic.bind$m$(\\<^sub>2x. f x))" using assms unfolding APP_def PROTECT2_def bind_ref_tag_def by (rule hnr_bind) lemma hn_RECT'[sepref_comb_rules]: assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'" assumes FR: "P \\<^sub>t hn_ctxt Rx ax px * F" assumes S: "\cf af ax px. \ \ax px. hn_refine (hn_ctxt Rx ax px * F) (cf px) (hn_ctxt Rx' ax px * F) Ry (RCALL$af$ax)\ \ hn_refine (hn_ctxt Rx ax px * F) (cB cf px) (F' ax px) Ry (aB af ax)" assumes FR': "\ax px. F' ax px \\<^sub>t hn_ctxt Rx' ax px * F" assumes M: "(\x. mono_Heap (\f. cB f x))" (*assumes PREC[unfolded CONSTRAINT_def]: "CONSTRAINT precise Ry"*) shows "hn_refine (P) (heap.fixp_fun cB px) (hn_ctxt Rx' ax px * F) Ry (RECT$(\\<^sub>2D x. aB D x)$ax)" unfolding APP_def PROTECT2_def apply (rule hn_refine_cons_pre[OF FR]) apply (rule hnr_RECT) apply (rule hn_refine_cons_post[OF _ FR']) apply (rule S[unfolded RCALL_def APP_def]) apply assumption apply fact+ done lemma hn_RCALL[sepref_comb_rules]: assumes "RPREM (hn_refine P' c Q' R (RCALL $ a $ b))" and "P \\<^sub>t F * P'" shows "hn_refine P c (F * Q') R (RCALL $ a $ b)" using assms hn_refine_frame[where m="RCALL$a$b"] by simp definition "monadic_WHILEIT I b f s \ do { RECT (\D s. do { ASSERT (I s); bv \ b s; if bv then do { s \ f s; D s } else do {RETURN s} }) s }" definition "heap_WHILET b f s \ do { heap.fixp_fun (\D s. do { bv \ b s; if bv then do { s \ f s; D s } else do {return s} }) s }" lemma heap_WHILET_unfold[code]: "heap_WHILET b f s = do { bv \ b s; if bv then do { s \ f s; heap_WHILET b f s } else return s }" unfolding heap_WHILET_def apply (subst heap.mono_body_fixp) apply pf_mono apply simp done lemma WHILEIT_to_monadic: "WHILEIT I b f s = monadic_WHILEIT I (\s. RETURN (b s)) f s" unfolding WHILEIT_def monadic_WHILEIT_def unfolding WHILEI_body_def bind_ASSERT_eq_if by (simp cong: if_cong) lemma WHILEIT_pat[def_pat_rules]: "WHILEIT$I \ UNPROTECT (WHILEIT I)" "WHILET \ PR_CONST (WHILEIT (\_. True))" by (simp_all add: WHILET_def) lemma id_WHILEIT[id_rules]: "PR_CONST (WHILEIT I) ::\<^sub>i TYPE(('a \ bool) \ ('a \ 'a nres) \ 'a \ 'a nres)" by simp lemma WHILE_arities[sepref_monadify_arity]: (*"WHILET \ WHILEIT$(\\<^sub>2_. True)"*) "PR_CONST (WHILEIT I) \ \\<^sub>2b f s. SP (PR_CONST (WHILEIT I))$(\\<^sub>2s. b$s)$(\\<^sub>2s. f$s)$s" by (simp_all add: WHILET_def) lemma WHILEIT_comb[sepref_monadify_comb]: "PR_CONST (WHILEIT I)$(\\<^sub>2x. b x)$f$s \ Refine_Basic.bind$(EVAL$s)$(\\<^sub>2s. SP (PR_CONST (monadic_WHILEIT I))$(\\<^sub>2x. (EVAL$(b x)))$f$s )" by (simp_all add: WHILEIT_to_monadic) lemma hn_monadic_WHILE_aux: assumes FR: "P \\<^sub>t \ * hn_ctxt Rs s' s" assumes b_ref: "\s s'. I s' \ hn_refine (\ * hn_ctxt Rs s' s) (b s) (\b s' s) (pure bool_rel) (b' s')" assumes b_fr: "\s' s. \b s' s \\<^sub>t \ * hn_ctxt Rs s' s" assumes f_ref: "\s' s. \I s'\ \ hn_refine (\ * hn_ctxt Rs s' s) (f s) (\f s' s) Rs (f' s')" assumes f_fr: "\s' s. \f s' s \\<^sub>t \ * hn_ctxt (\_ _. true) s' s" (*assumes PREC: "precise Rs"*) shows "hn_refine (P) (heap_WHILET b f s) (\ * hn_invalid Rs s' s) Rs (monadic_WHILEIT I b' f' s')" unfolding monadic_WHILEIT_def heap_WHILET_def apply1 (rule hn_refine_cons_pre[OF FR]) apply weaken_hnr_post focus (rule hn_refine_cons_pre[OF _ hnr_RECT]) applyS (subst mult_ac(2)[of \]; rule entt_refl; fail) apply1 (rule hnr_ASSERT) focus (rule hnr_bind) focus (rule hn_refine_cons[OF _ b_ref b_fr entt_refl]) applyS (simp add: star_aci) applyS assumption solved focus (rule hnr_If) applyS (sep_auto; fail) focus (rule hnr_bind) focus (rule hn_refine_cons[OF _ f_ref f_fr entt_refl]) apply (sep_auto simp: hn_ctxt_def pure_def intro!: enttI; fail) apply assumption solved focus (rule hn_refine_frame) applyS rprems applyS (rule enttI; solve_entails) solved apply (sep_auto intro!: enttI; fail) solved applyF (sep_auto,rule hn_refine_frame) applyS (rule hnr_RETURN_pass) (*apply (tactic {* Sepref_Frame.frame_tac @{context} 1*})*) apply (rule enttI) apply (fr_rot_rhs 1) apply (fr_rot 1, rule fr_refl) apply (rule fr_refl) apply solve_entails solved apply (rule entt_refl) solved apply (rule enttI) applyF (rule ent_disjE) apply1 (sep_auto simp: hn_ctxt_def pure_def) apply1 (rule ent_true_drop) apply1 (rule ent_true_drop) applyS (rule ent_refl) applyS (sep_auto simp: hn_ctxt_def pure_def) solved solved apply pf_mono solved done lemma hn_monadic_WHILE_lin[sepref_comb_rules]: assumes "INDEP Rs" assumes FR: "P \\<^sub>t \ * hn_ctxt Rs s' s" assumes b_ref: "\s s'. I s' \ hn_refine (\ * hn_ctxt Rs s' s) (b s) (\b s' s) (pure bool_rel) (b' s')" assumes b_fr: "\s' s. TERM (monadic_WHILEIT,''cond'') \ \b s' s \\<^sub>t \ * hn_ctxt Rs s' s" assumes f_ref: "\s' s. I s' \ hn_refine (\ * hn_ctxt Rs s' s) (f s) (\f s' s) Rs (f' s')" assumes f_fr: "\s' s. TERM (monadic_WHILEIT,''body'') \ \f s' s \\<^sub>t \ * hn_ctxt (\_ _. true) s' s" shows "hn_refine P (heap_WHILET b f s) (\ * hn_invalid Rs s' s) Rs (PR_CONST (monadic_WHILEIT I)$(\\<^sub>2s'. b' s')$(\\<^sub>2s'. f' s')$(s'))" using assms(2-) unfolding APP_def PROTECT2_def CONSTRAINT_def PR_CONST_def by (rule hn_monadic_WHILE_aux) lemma monadic_WHILEIT_refine[refine]: assumes [refine]: "(s',s) \ R" assumes [refine]: "\s' s. \ (s',s)\R; I s \ \ I' s'" assumes [refine]: "\s' s. \ (s',s)\R; I s; I' s' \ \ b' s' \\bool_rel (b s)" assumes [refine]: "\s' s. \ (s',s)\R; I s; I' s'; nofail (b s); inres (b s) True \ \ f' s' \\R (f s)" shows "monadic_WHILEIT I' b' f' s' \\R (monadic_WHILEIT I b f s)" unfolding monadic_WHILEIT_def by (refine_rcg bind_refine'; assumption?; auto) lemma monadic_WHILEIT_refine_WHILEIT[refine]: assumes [refine]: "(s',s) \ R" assumes [refine]: "\s' s. \ (s',s)\R; I s \ \ I' s'" assumes [THEN order_trans,refine_vcg]: "\s' s. \ (s',s)\R; I s; I' s' \ \ b' s' \ SPEC (\r. r = b s)" assumes [refine]: "\s' s. \ (s',s)\R; I s; I' s'; b s \ \ f' s' \\R (f s)" shows "monadic_WHILEIT I' b' f' s' \\R (WHILEIT I b f s)" unfolding WHILEIT_to_monadic by (refine_vcg; assumption?; auto) lemma monadic_WHILEIT_refine_WHILET[refine]: assumes [refine]: "(s',s) \ R" assumes [THEN order_trans,refine_vcg]: "\s' s. \ (s',s)\R \ \ b' s' \ SPEC (\r. r = b s)" assumes [refine]: "\s' s. \ (s',s)\R; b s \ \ f' s' \\R (f s)" shows "monadic_WHILEIT (\_. True) b' f' s' \\R (WHILET b f s)" unfolding WHILET_def by (refine_vcg; assumption?) lemma monadic_WHILEIT_pat[def_pat_rules]: "monadic_WHILEIT$I \ UNPROTECT (monadic_WHILEIT I)" by auto lemma id_monadic_WHILEIT[id_rules]: "PR_CONST (monadic_WHILEIT I) ::\<^sub>i TYPE(('a \ bool nres) \ ('a \ 'a nres) \ 'a \ 'a nres)" by simp lemma monadic_WHILEIT_arities[sepref_monadify_arity]: "PR_CONST (monadic_WHILEIT I) \ \\<^sub>2b f s. SP (PR_CONST (monadic_WHILEIT I))$(\\<^sub>2s. b$s)$(\\<^sub>2s. f$s)$s" by (simp) lemma monadic_WHILEIT_comb[sepref_monadify_comb]: "PR_CONST (monadic_WHILEIT I)$b$f$s \ Refine_Basic.bind$(EVAL$s)$(\\<^sub>2s. SP (PR_CONST (monadic_WHILEIT I))$b$f$s )" by (simp) definition [simp]: "op_ASSERT_bind I m \ Refine_Basic.bind (ASSERT I) (\_. m)" lemma pat_ASSERT_bind[def_pat_rules]: "Refine_Basic.bind$(ASSERT$I)$(\\<^sub>2_. m) \ UNPROTECT (op_ASSERT_bind I)$m" by simp term "PR_CONST (op_ASSERT_bind I)" lemma id_op_ASSERT_bind[id_rules]: "PR_CONST (op_ASSERT_bind I) ::\<^sub>i TYPE('a nres \ 'a nres)" by simp lemma arity_ASSERT_bind[sepref_monadify_arity]: "PR_CONST (op_ASSERT_bind I) \ \\<^sub>2m. SP (PR_CONST (op_ASSERT_bind I))$m" apply (rule eq_reflection) by auto lemma hn_ASSERT_bind[sepref_comb_rules]: assumes "I \ hn_refine \ c \' R m" shows "hn_refine \ c \' R (PR_CONST (op_ASSERT_bind I)$m)" using assms apply (cases I) apply auto done definition [simp]: "op_ASSUME_bind I m \ Refine_Basic.bind (ASSUME I) (\_. m)" lemma pat_ASSUME_bind[def_pat_rules]: "Refine_Basic.bind$(ASSUME$I)$(\\<^sub>2_. m) \ UNPROTECT (op_ASSUME_bind I)$m" by simp lemma id_op_ASSUME_bind[id_rules]: "PR_CONST (op_ASSUME_bind I) ::\<^sub>i TYPE('a nres \ 'a nres)" by simp lemma arity_ASSUME_bind[sepref_monadify_arity]: "PR_CONST (op_ASSUME_bind I) \ \\<^sub>2m. SP (PR_CONST (op_ASSUME_bind I))$m" apply (rule eq_reflection) by auto lemma hn_ASSUME_bind[sepref_comb_rules]: assumes "vassn_tag \ \ I" assumes "I \ hn_refine \ c \' R m" shows "hn_refine \ c \' R (PR_CONST (op_ASSUME_bind I)$m)" apply (rule hn_refine_preI) using assms apply (cases I) apply (auto simp: vassn_tag_def) done subsection "Import of Parametricity Theorems" lemma pure_hn_refineI: assumes "Q \ (c,a)\R" shows "hn_refine (\Q) (return c) (\Q) (pure R) (RETURN a)" unfolding hn_refine_def using assms by (sep_auto simp: pure_def) lemma pure_hn_refineI_no_asm: assumes "(c,a)\R" shows "hn_refine emp (return c) emp (pure R) (RETURN a)" unfolding hn_refine_def using assms by (sep_auto simp: pure_def) lemma import_param_0: "(P\Q) \ Trueprop (PROTECT P \ Q)" apply (rule, simp+)+ done lemma import_param_1: "(P\Q) \ Trueprop (P\Q)" "(P\Q\R) \ (P\Q \ R)" "PROTECT (P \ Q) \ PROTECT P \ PROTECT Q" "(P \ Q) \ R \ P \ Q \ R" "(a,c)\Rel \ PROTECT P \ PROTECT P \ (a,c)\Rel" apply (rule, simp+)+ done lemma import_param_2: "Trueprop (PROTECT P \ Q \ R) \ (P \ Q\R)" apply (rule, simp+)+ done lemma import_param_3: "\(P \ Q) = \P*\Q" "\((c,a)\R) = hn_val R a c" by (simp_all add: hn_ctxt_def pure_def) named_theorems_rev sepref_import_rewrite \Rewrite rules on importing parametricity theorems\ lemma to_import_frefD: assumes "(f,g)\fref P R S" shows "\PROTECT (P y); (x,y)\R\ \ (f x, g y)\S" using assms unfolding fref_def by auto lemma add_PR_CONST: "(c,a)\R \ (c,PR_CONST a)\R" by simp ML \ structure Sepref_Import_Param = struct (* TODO: Almost clone of Sepref_Rules.to_foparam*) fun to_import_fo ctxt thm = let val unf_thms = @{thms split_tupled_all prod_rel_simp uncurry_apply cnv_conj_to_meta Product_Type.split} in case Thm.concl_of thm of @{mpat "Trueprop ((_,_) \ fref _ _ _)"} => (@{thm to_import_frefD} OF [thm]) - |> forall_intr_vars + |> Thm.forall_intr_vars |> Local_Defs.unfold0 ctxt unf_thms |> Variable.gen_all ctxt | @{mpat "Trueprop ((_,_) \ _)"} => Parametricity.fo_rule thm | _ => raise THM("Expected parametricity or fref theorem",~1,[thm]) end fun add_PR_CONST thm = case Thm.concl_of thm of @{mpat "Trueprop ((_,_) \ fref _ _ _)"} => thm (* TODO: Hack. Need clean interfaces for fref and param rules. Also add PR_CONST to fref rules! *) | @{mpat "Trueprop ((_,PR_CONST _) \ _)"} => thm | @{mpat "Trueprop ((_,?a) \ _)"} => if is_Const a orelse is_Free a orelse is_Var a then thm else thm RS @{thm add_PR_CONST} | _ => thm fun import ctxt thm = let open Sepref_Basic val thm = thm |> Conv.fconv_rule Thm.eta_conversion |> add_PR_CONST |> Local_Defs.unfold0 ctxt @{thms import_param_0} |> Local_Defs.unfold0 ctxt @{thms imp_to_meta} |> to_import_fo ctxt |> Local_Defs.unfold0 ctxt @{thms import_param_1} |> Local_Defs.unfold0 ctxt @{thms import_param_2} val thm = case Thm.concl_of thm of @{mpat "Trueprop (_\_)"} => thm RS @{thm pure_hn_refineI} | _ => thm RS @{thm pure_hn_refineI_no_asm} val thm = Local_Defs.unfold0 ctxt @{thms import_param_3} thm |> Conv.fconv_rule (hn_refine_concl_conv_a (K (Id_Op.protect_conv ctxt)) ctxt) val thm = Local_Defs.unfold0 ctxt (Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_import_rewrite}) thm val thm = Sepref_Rules.add_pure_constraints_rule ctxt thm in thm end val import_attr = Scan.succeed (Thm.mixed_attribute (fn (context,thm) => let val thm = import (Context.proof_of context) thm val context = Sepref_Translate.sepref_fr_rules.add_thm thm context in (context,thm) end )) val import_attr_rl = Scan.succeed (Thm.rule_attribute [] (fn context => import (Context.proof_of context) #> Sepref_Rules.ensure_hfref (Context.proof_of context) )) val setup = I #> Attrib.setup @{binding sepref_import_param} import_attr "Sepref: Import parametricity rule" #> Attrib.setup @{binding sepref_param} import_attr_rl "Sepref: Transform parametricity rule to sepref rule" #> Attrib.setup @{binding sepref_dbg_import_rl_only} (Scan.succeed (Thm.rule_attribute [] (import o Context.proof_of))) "Sepref: Parametricity to hnr-rule, no conversion to hfref" end \ setup Sepref_Import_Param.setup subsection "Purity" definition "import_rel1 R \ \A c ci. \(is_pure A \ (ci,c)\\the_pure A\R)" definition "import_rel2 R \ \A B c ci. \(is_pure A \ is_pure B \ (ci,c)\\the_pure A, the_pure B\R)" lemma import_rel1_pure_conv: "import_rel1 R (pure A) = pure (\A\R)" unfolding import_rel1_def apply simp apply (simp add: pure_def) done lemma import_rel2_pure_conv: "import_rel2 R (pure A) (pure B) = pure (\A,B\R)" unfolding import_rel2_def apply simp apply (simp add: pure_def) done lemma precise_pure[constraint_rules]: "single_valued R \ precise (pure R)" unfolding precise_def pure_def by (auto dest: single_valuedD) lemma precise_pure_iff_sv: "precise (pure R) \ single_valued R" apply (auto simp: precise_pure) using preciseD[where R="pure R" and F=emp and F'=emp] by (sep_auto simp: mod_and_dist intro: single_valuedI) lemma pure_precise_iff_sv: "\is_pure R\ \ precise R \ single_valued (the_pure R)" by (auto simp: is_pure_conv precise_pure_iff_sv) lemmas [safe_constraint_rules] = single_valued_Id br_sv end diff --git a/thys/Refine_Monadic/Refine_Automation.thy b/thys/Refine_Monadic/Refine_Automation.thy --- a/thys/Refine_Monadic/Refine_Automation.thy +++ b/thys/Refine_Monadic/Refine_Automation.thy @@ -1,555 +1,555 @@ section "More Automation" theory Refine_Automation imports Refine_Basic Refine_Transfer keywords "concrete_definition" :: thy_decl and "prepare_code_thms" :: thy_decl and "uses" begin text \ This theory provides a tool for extracting definitions from terms, and for generating code equations for recursion combinators. \ ML \ signature REFINE_AUTOMATION = sig type extraction = { pattern: term, (* Pattern to be defined as own constant *) gen_thm: thm, (* Code eq generator: [| c==rhs; ... |] ==> c == ... *) gen_tac: local_theory -> tactic' (* Solves remaining premises of gen_thm *) } val extract_as_def: (string * typ) list -> string -> term -> local_theory -> ((term * thm) * local_theory) val extract_recursion_eqs: extraction list -> string -> thm -> local_theory -> local_theory val add_extraction: string -> extraction -> theory -> theory val prepare_code_thms_cmd: string list -> thm -> local_theory -> local_theory val define_concrete_fun: extraction list option -> binding -> Token.src list -> indexname list -> thm -> cterm list -> local_theory -> (thm * thm) * local_theory val mk_qualified: string -> bstring -> binding val prepare_cd_pattern: Proof.context -> cterm -> cterm val add_cd_pattern: cterm -> Context.generic -> Context.generic val del_cd_pattern: cterm -> Context.generic -> Context.generic val get_cd_patterns: Proof.context -> cterm list val add_vc_rec_thm: thm -> Context.generic -> Context.generic val del_vc_rec_thm: thm -> Context.generic -> Context.generic val get_vc_rec_thms: Proof.context -> thm list val add_vc_solve_thm: thm -> Context.generic -> Context.generic val del_vc_solve_thm: thm -> Context.generic -> Context.generic val get_vc_solve_thms: Proof.context -> thm list val vc_solve_tac: Proof.context -> bool -> tactic' val vc_solve_modifiers: Method.modifier parser list val setup: theory -> theory end structure Refine_Automation :REFINE_AUTOMATION = struct type extraction = { pattern: term, (* Pattern to be defined as own constant *) gen_thm: thm, (* Code eq generator: [| c==rhs; ... |] ==> c == ... *) gen_tac: local_theory -> tactic' (* Solves remaining premises of gen_thm *) } structure extractions = Generic_Data ( type T = extraction list Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.merge_list ((op =) o apply2 #pattern) ) fun add_extraction name ex = Context.theory_map (extractions.map ( Symtab.update_list ((op =) o apply2 #pattern) (name,ex))) (* Define new constant name for subterm t in context bnd. Returns replacement for t using the new constant and definition theorem. *) fun extract_as_def bnd name t lthy = let val loose = rev (loose_bnos t); val rnames = #1 (Variable.names_of lthy |> fold_map (Name.variant o #1) bnd); val rfrees = map (fn (name,(_,typ)) => Free (name,typ)) (rnames ~~ bnd); val t' = subst_bounds (rfrees,t); val params = map Bound (rev loose); val param_vars = (Library.foldl (fn (l,i) => nth rfrees i :: l) ([],loose)); val param_types = map fastype_of param_vars; val def_t = Logic.mk_equals (list_comb (Free (name,param_types ---> fastype_of t'),param_vars),t'); val ((lhs_t,(_,def_thm)),lthy) = Specification.definition NONE [] [] (Binding.empty_atts,def_t) lthy; (*val _ = tracing "xxxx";*) val app_t = list_comb (lhs_t, params); in ((app_t,def_thm),lthy) end; fun mk_qualified basename q = Binding.qualify true basename (Binding.name q); fun extract_recursion_eqs exs basename orig_def_thm lthy = let val thy = Proof_Context.theory_of lthy val pat_net : extraction Item_Net.T = Item_Net.init ((op =) o apply2 #pattern) (fn {pattern, ...} => [pattern]) |> fold Item_Net.update exs local fun tr env t ctx = let (* Recurse for subterms *) val (t,ctx) = case t of t1$t2 => let val (t1,ctx) = tr env t1 ctx val (t2,ctx) = tr env t2 ctx in (t1$t2,ctx) end | Abs (x,T,t) => let val (t',ctx) = tr ((x,T)::env) t ctx in (Abs (x,T,t'),ctx) end | _ => (t,ctx) (* Check if we match a pattern *) val ex = Item_Net.retrieve_matching pat_net t |> get_first (fn ex => case try (Pattern.first_order_match thy (#pattern ex,t)) (Vartab.empty,Vartab.empty) of NONE => NONE | SOME _ => SOME ex ) in case ex of NONE => (t,ctx) | SOME ex => let (* Extract as new constant *) val (idx,defs,lthy) = ctx val name = (basename ^ "_" ^ string_of_int idx) val ((t,def_thm),lthy) = extract_as_def env name t lthy val ctx = (idx+1,(def_thm,ex)::defs,lthy) in (t,ctx) end end in fun transform t lthy = let val (t,(_,defs,lthy)) = tr [] t (0,[],lthy) in ((t,defs),lthy) end end (* Import theorem and extract RHS *) val ((_,orig_def_thm'),lthy) = yield_singleton2 (Variable.import true) orig_def_thm lthy; val (lhs,rhs) = orig_def_thm' |> Thm.prop_of |> Logic.dest_equals; (* Transform RHS, generating new constants *) val ((rhs',defs),lthy) = transform rhs lthy; val def_thms = map #1 defs (* Register definitions of generated constants *) val (_,lthy) = Local_Theory.note ((mk_qualified basename "defs",[]),def_thms) lthy; (* Obtain new def_thm *) val def_unfold_ss = put_simpset HOL_basic_ss lthy addsimps (orig_def_thm::def_thms) val new_def_thm = Goal.prove_internal lthy [] (Logic.mk_equals (lhs,rhs') |> Thm.cterm_of lthy) (K (simp_tac def_unfold_ss 1)) (* Obtain new theorem by folding with defs of generated constants *) (* TODO: Maybe cleaner to generate eq-thm and prove by "unfold, refl" *) (*val new_def_thm = Library.foldr (fn (dt,t) => Local_Defs.fold lthy [dt] t) (def_thms,orig_def_thm');*) (* Prepare code equations *) fun mk_code_thm lthy (def_thm,{gen_thm, gen_tac, ...}) = let val ((_,def_thm),lthy') = yield_singleton2 (Variable.import true) def_thm lthy; val thm = def_thm RS gen_thm; val tac = SOLVED' (gen_tac lthy') ORELSE' (simp_tac def_unfold_ss THEN' gen_tac lthy') val thm = the (SINGLE (ALLGOALS tac) thm); val thm = singleton (Variable.export lthy' lthy) thm; in thm end; val code_thms = map (mk_code_thm lthy) defs; val _ = if forall Thm.no_prems code_thms then () else warning "Unresolved premises in code theorems" val (_,lthy) = Local_Theory.note ((mk_qualified basename "code",@{attributes [code]}),new_def_thm::code_thms) lthy; in lthy end; fun prepare_code_thms_cmd names thm lthy = let fun name_of (Const (n,_)) = n | name_of (Free (n,_)) = n | name_of _ = raise (THM ("No definitional theorem",0,[thm])); val (lhs,_) = thm |> Thm.prop_of |> Logic.dest_equals; val basename = lhs |> strip_comb |> #1 |> name_of |> Long_Name.base_name; val exs_tab = extractions.get (Context.Proof lthy) fun get_exs name = case Symtab.lookup exs_tab name of NONE => error ("No such extraction mode: " ^ name) | SOME exs => exs val exs = case names of [] => Symtab.dest_list exs_tab |> map #2 | _ => map get_exs names |> flat val _ = case exs of [] => error "No extraction patterns selected" | _ => () val lthy = extract_recursion_eqs exs basename thm lthy in lthy end; fun extract_concrete_fun _ [] concl = raise TERM ("Conclusion does not match any extraction pattern",[concl]) | extract_concrete_fun thy (pat::pats) concl = ( case Refine_Util.fo_matchp thy pat concl of NONE => extract_concrete_fun thy pats concl | SOME [t] => t | SOME (t::_) => ( warning ("concrete_definition: Pattern has multiple holes, taking " ^ "first one: " ^ @{make_string} pat ); t) | _ => (warning ("concrete_definition: Ignoring invalid pattern " ^ @{make_string} pat); extract_concrete_fun thy pats concl) ) (* Define concrete function from refinement lemma *) fun define_concrete_fun gen_code fun_name attribs_raw param_names thm pats (orig_lthy:local_theory) = let val lthy = orig_lthy; - val ((inst,thm'),lthy) = yield_singleton2 (Variable.import true) thm lthy; + val (((_,inst),thm'),lthy) = yield_singleton2 (Variable.import true) thm lthy; val concl = thm' |> Thm.concl_of (*val ((typ_subst,term_subst),lthy) = Variable.import_inst true [concl] lthy; val concl = Term_Subst.instantiate (typ_subst,term_subst) concl; *) - val term_subst = #2 inst |> map (apsnd Thm.term_of) + val term_subst = build (inst |> Term_Subst.Vars.fold (cons o apsnd Thm.term_of)) val param_terms = map (fn name => case AList.lookup (fn (n,v) => n = #1 v) term_subst name of NONE => raise TERM ("No such variable: " ^Term.string_of_vname name,[concl]) | SOME t => t ) param_names; val f_term = extract_concrete_fun (Proof_Context.theory_of lthy) pats concl; val lhs_type = map Term.fastype_of param_terms ---> Term.fastype_of f_term; val lhs_term = list_comb ((Free (Binding.name_of fun_name,lhs_type)),param_terms); val def_term = Logic.mk_equals (lhs_term,f_term) |> fold Logic.all param_terms; val attribs = map (Attrib.check_src lthy) attribs_raw; val ((_,(_,def_thm)),lthy) = Specification.definition (SOME (fun_name,NONE,Mixfix.NoSyn)) [] [] ((Binding.empty,attribs),def_term) lthy; val folded_thm = Local_Defs.fold lthy [def_thm] thm'; val (_,lthy) = Local_Theory.note ((mk_qualified (Binding.name_of fun_name) "refine",[]),[folded_thm]) lthy; val lthy = case gen_code of NONE => lthy | SOME modes => extract_recursion_eqs modes (Binding.name_of fun_name) def_thm lthy in ((def_thm,folded_thm),lthy) end; val cd_pat_eq = apply2 (Thm.term_of #> Refine_Util.anorm_term) #> (op aconv) structure cd_patterns = Generic_Data ( type T = cterm list val empty = [] val extend = I val merge = merge cd_pat_eq ) fun prepare_cd_pattern ctxt pat = case Thm.term_of pat |> fastype_of of @{typ bool} => Thm.term_of pat |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt | _ => pat fun add_cd_pattern pat context = cd_patterns.map (insert cd_pat_eq (prepare_cd_pattern (Context.proof_of context) pat)) context fun del_cd_pattern pat context = cd_patterns.map (remove cd_pat_eq (prepare_cd_pattern (Context.proof_of context) pat)) context val get_cd_patterns = cd_patterns.get o Context.Proof structure rec_thms = Named_Thms ( val name = @{binding vcs_rec} val description = "VC-Solver: Recursive intro rules" ) structure solve_thms = Named_Thms ( val name = @{binding vcs_solve} val description = "VC-Solver: Solve rules" ) val add_vc_rec_thm = rec_thms.add_thm val del_vc_rec_thm = rec_thms.del_thm val get_vc_rec_thms = rec_thms.get val add_vc_solve_thm = solve_thms.add_thm val del_vc_solve_thm = solve_thms.del_thm val get_vc_solve_thms = solve_thms.get val rec_modifiers = [ Args.$$$ "rec" -- Scan.option Args.add -- Args.colon >> K (Method.modifier rec_thms.add \<^here>), Args.$$$ "rec" -- Scan.option Args.del -- Args.colon >> K (Method.modifier rec_thms.del \<^here>) ]; val solve_modifiers = [ Args.$$$ "solve" -- Scan.option Args.add -- Args.colon >> K (Method.modifier solve_thms.add \<^here>), Args.$$$ "solve" -- Scan.option Args.del -- Args.colon >> K (Method.modifier solve_thms.del \<^here>) ]; val vc_solve_modifiers = clasimp_modifiers @ rec_modifiers @ solve_modifiers; fun vc_solve_tac ctxt no_pre = let val rthms = rec_thms.get ctxt val sthms = solve_thms.get ctxt val pre_tac = if no_pre then K all_tac else clarsimp_tac ctxt val tac = SELECT_GOAL (auto_tac ctxt) in TRY o pre_tac THEN_ALL_NEW_FWD (TRY o REPEAT_ALL_NEW_FWD (resolve_tac ctxt rthms)) THEN_ALL_NEW_FWD (TRY o SOLVED' (resolve_tac ctxt sthms THEN_ALL_NEW_FWD tac)) end val setup = I #> rec_thms.setup #> solve_thms.setup end; \ setup Refine_Automation.setup setup \ let fun parse_cpat cxt = let val (t, (context, tks)) = Scan.lift Args.embedded_inner_syntax cxt val ctxt = Context.proof_of context val t = Proof_Context.read_term_pattern ctxt t in (Thm.cterm_of ctxt t, (context, tks)) end fun do_p f = Scan.repeat1 parse_cpat >> (fn pats => Thm.declaration_attribute (K (fold f pats))) in Attrib.setup @{binding "cd_patterns"} ( Scan.lift Args.add |-- do_p Refine_Automation.add_cd_pattern || Scan.lift Args.del |-- do_p Refine_Automation.del_cd_pattern || do_p Refine_Automation.add_cd_pattern ) "Add/delete concrete_definition pattern" end \ (* Command setup *) (* TODO: Folding of .refine-lemma seems not to work, if the function has parameters on which it does not depend *) ML \Outer_Syntax.local_theory @{command_keyword concrete_definition} "Define function from refinement theorem" (Parse.binding -- Parse.opt_attribs -- Scan.optional (@{keyword "for"} |-- Scan.repeat1 Args.var) [] --| @{keyword "uses"} -- Parse.thm -- Scan.optional (@{keyword "is"} |-- Scan.repeat1 Args.embedded_inner_syntax) [] >> (fn ((((name,attribs),params),raw_thm),pats) => fn lthy => let val thm = case Attrib.eval_thms lthy [raw_thm] of [thm] => thm | _ => error "Expecting exactly one theorem"; val pats = case pats of [] => Refine_Automation.get_cd_patterns lthy | l => map (Proof_Context.read_term_pattern lthy #> Thm.cterm_of lthy #> Refine_Automation.prepare_cd_pattern lthy) l in Refine_Automation.define_concrete_fun NONE name attribs params thm pats lthy |> snd end)) \ text \ Command: \concrete_definition name [attribs] for params uses thm is patterns\ where \attribs\, \for\, and \is\-parts are optional. Declares a new constant \name\ by matching the theorem \thm\ against a pattern. If the \for\ clause is given, it lists variables in the theorem, and thus determines the order of parameters of the defined constant. Otherwise, parameters will be in order of occurrence. If the \is\ clause is given, it lists patterns. The conclusion of the theorem will be matched against each of these patterns. For the first matching pattern, the constant will be declared to be the term that matches the first non-dummy variable of the pattern. If no \is\-clause is specified, the default patterns will be tried. Attribute: \cd_patterns pats\. Declaration attribute. Declares default patterns for the \concrete_definition\ command. \ declare [[ cd_patterns "(?f,_)\_"]] declare [[ cd_patterns "RETURN ?f \ _" "nres_of ?f \ _"]] declare [[ cd_patterns "(RETURN ?f,_)\_" "(nres_of ?f,_)\_"]] declare [[ cd_patterns "_ = ?f" "_ == ?f" ]] ML \ let val modes = (Scan.optional (@{keyword "("} |-- Parse.list1 Parse.name --| @{keyword ")"}) []) in Outer_Syntax.local_theory @{command_keyword prepare_code_thms} "Refinement framework: Prepare theorems for code generation" (modes -- Parse.thms1 >> (fn (modes,raw_thms) => fn lthy => let val thms = Attrib.eval_thms lthy raw_thms in fold (Refine_Automation.prepare_code_thms_cmd modes) thms lthy end) ) end \ text \ Command: \prepare_code_thms (modes) thm\ where the \(mode)\-part is optional. Set up code-equations for recursions in constant defined by \thm\. The optional \modes\ is a comma-separated list of extraction modes. \ lemma gen_code_thm_RECT: fixes x assumes D: "f \ RECT B" assumes M: "trimono B" shows "f x \ B f x" unfolding D apply (subst RECT_unfold) by (rule M) lemma gen_code_thm_REC: fixes x assumes D: "f \ REC B" assumes M: "trimono B" shows "f x \ B f x" unfolding D apply (subst REC_unfold) by (rule M) setup \ Refine_Automation.add_extraction "nres" { pattern = Logic.varify_global @{term "REC x"}, gen_thm = @{thm gen_code_thm_REC}, gen_tac = Refine_Mono_Prover.mono_tac } #> Refine_Automation.add_extraction "nres" { pattern = Logic.varify_global @{term "RECT x"}, gen_thm = @{thm gen_code_thm_RECT}, gen_tac = Refine_Mono_Prover.mono_tac } \ text \ Method \vc_solve (no_pre) clasimp_modifiers rec (add/del): ... solve (add/del): ...\ Named theorems \vcs_rec\ and \vcs_solve\. This method is specialized to solve verification conditions. It first clarsimps all goals, then it tries to apply a set of safe introduction rules (\vcs_rec\, \rec add\). Finally, it applies introduction rules (\vcs_solve\, \solve add\) and tries to discharge all emerging subgoals by auto. If this does not succeed, it backtracks over the application of the solve-rule. \ method_setup vc_solve = \Scan.lift (Args.mode "nopre") --| Method.sections Refine_Automation.vc_solve_modifiers >> (fn (nopre) => fn ctxt => SIMPLE_METHOD ( CHANGED (ALLGOALS (Refine_Automation.vc_solve_tac ctxt nopre)) ))\ "Try to solve verification conditions" end